----- Eq-prover 0.3, Jan. 1996 ----- The job began on dopey.mcs.anl.gov, Thu Jun 13 14:32:31 1996 The command was "/home/mccune/ntp/eqp-ibm". UNIT CONFLICT from 3733 and 1 at 608688.73 seconds. ---------------- PROOF ---------------- 1 (wt=5) [] -(x + y = x). 2 (wt=7) [] n(D + C) = n(C). 3 (wt=13) [] n(n(n(x) + y) + n(x + y)) = y. 4 (wt=15) [para(2,3)] n(n(D + C + x) + n(n(C) + x)) = x. 5 (wt=11) [para(2,3)] n(n(C) + n(D + n(C))) = D. 7 (wt=19) [para(5,3)] n(n(D + x) + n(n(C) + n(D + n(C)) + x)) = x. 9 (wt=17) [para(5,3)] n(D + n(C + n(D + n(C)))) = n(D + n(C)). 18 (wt=19) [para(3,3)] n(n(n(n(x) + y) + x + y) + y) = n(n(x) + y). 25 (wt=21) [para(2,18),demod([2])] n(n(D + C + n(n(C) + x) + x) + x) = n(n(C) + x). 35 (wt=23) [para(4,3)] n(n(n(D + C + x) + n(n(C) + x) + y) + n(x + y)) = y. 64 (wt=19) [para(9,3)] n(n(D + n(C)) + n(D + C + n(D + n(C)))) = D. 141 (wt=21) [para(18,3)] n(n(n(n(x) + y) + x + y + y) + n(n(x) + y)) = y. 145 (wt=26) [para(3,18),demod([3])] n(n(n(n(x) + y) + n(x + y) + n(y + z) + z) + z) = n(y + z). 170 (wt=30) [para(64,3)] n(D + n(D + n(C) + n(D + C + n(D + n(C))))) = n(D + C + n(D + n(C))). 287 (wt=29) [para(141,3)] n(n(n(n(n(x) + y) + x + y + y) + n(n(x) + y) + z) + n(y + z)) = z. 298 (wt=13) [para(5,35),demod([5,170])] n(D + C + n(D + n(C))) = n(C). 826 (wt=30) [para(5,145),demod([5])] n(n(D + n(C)) + n(D + n(D + n(C)) + n(n(C) + n(x)) + n(n(C) + x))) = D. 1234 (wt=34) [para(145,3)] n(n(n(n(n(x) + y) + n(x + y) + n(y + z) + z) + z + u) + n(n(y + z) + u)) = u. 1475 (wt=15) [para(25,7),demod([287]),flip(1)] n(D + D + C + n(D + n(C))) = n(C). 1498 (wt=29) [para(1475,18),demod([1475])] n(n(D + D + C + n(D + n(C)) + n(n(C) + x) + x) + x) = n(n(C) + x). 3318 (wt=33) [para(5,1234)] n(D + n(D + n(C) + n(D + n(D + n(C)) + n(n(C) + n(x)) + n(n(C) + x)))) = n(C). 3707 (wt=24) [para(826,35),demod([298,5,3318]),flip(1)] n(D + n(D + n(C)) + n(n(C) + n(x)) + n(n(C) + x)) = n(C). 3708 (wt=26) [para(2,3707)] n(D + n(D + n(C)) + n(D + C + n(C)) + n(n(C) + n(C))) = n(C). 3733 (wt=21) [para(3708,3),demod([1498]),flip(1)] D + n(D + n(C)) + n(n(C) + n(C)) = n(n(C) + n(C)). ------------ end of proof ------------- ------------- memory usage ------------ Memory dynamically allocated (tp_alloc): 5859. type (bytes each) gets frees in use avail bytes sym_ent ( 96) 51 0 51 0 4.8 K term ( 16) 363555280 363438977 116303 39 2257.7 K gen_ptr ( 8) 1704934 1682970 21964 24 171.8 K context ( 808) 254394917 254394914 3 23 20.5 K trail ( 12) 0 0 0 0 0.0 K bt_node ( 68) 809417357 809417350 7 33 2.7 K ac_position (285432) 2457887 2457886 1 5 1672.5 K ac_match_pos (14044) 333366694 333366694 0 9 123.4 K ac_match_free_vars_pos (4020) 252273455 252273455 0 4 15.7 K discrim ( 12) 14 0 14 0 0.2 K flat ( 40) 37253112 37253112 0 4 0.2 K discrim_pos ( 12) 4314261 4314261 0 1 0.0 K fpa_head ( 12) 0 0 0 0 0.0 K fpa_tree ( 28) 0 0 0 0 0.0 K fpa_pos ( 36) 0 0 0 0 0.0 K literal ( 12) 354480 350747 3733 0 43.7 K clause ( 24) 354480 350747 3733 0 87.5 K list ( 12) 3790 3734 56 3 0.7 K list_pos ( 20) 15021 237 14784 0 288.8 K pair_index ( 40) 2 0 2 0 0.1 K -------------- statistics ------------- Clauses input 3 Usable input 0 Sos input 2 Demodulators input 0 Passive input 1 Processed BS (before search) 2 Forward subsumed BS 0 Kept BS 3 New demodulators BS 2 Back demodulated BS 0 Clauses or pairs given 294433 Clauses generated 354477 Forward subsumed 15949 Deleted by weight 334798 Deleted by variable count 0 Kept 3730 New demodulators 3729 Back demodulated 47 Ordered paramod prunes 0 Basic paramod prunes 0 Prime paramod prunes 0 Semantic prunes 0 Rewrite attmepts 19969701 Rewrites 260101 FPA overloads 0 FPA underloads 0 Usable size 0 Sos size 3684 Demodulators size 3684 Passive size 1 Disabled size 47 Proofs found 1 ----------- times (seconds) ----------- Thu Jun 20 19:10:45 1996 user time 608688.75 (169 hr, 4 min, 48 sec) system time 59.89 (0 hr, 0 min, 59 sec) wall-clock time 621494 (172 hr, 38 min, 14 sec) input time 0.00 paramodulation time 723.68 demodulation time 604150.66 orient time 16.29 weigh time 11.89 forward subsume time 465.76 back demod find time 3256.27 conflict time 8.31 LRPO time 0.00 store clause time 4.18 disable clause time 0.09 prime paramod time 0.00 semantics time 0.00