----- Eq-prover 0.3, Jan. 1996 ----- The job began on sneezy.mcs.anl.gov, Thu Jun 13 16:29:55 1996 The command was "/home/mccune/ntp/eqp-ibm". UNIT CONFLICT from 1802 and 1 at 1902.89 seconds. ---------------- PROOF ---------------- 1 (wt=5) [] -(x + x = x). 2 (wt=5) [] D + C = C. 3 (wt=13) [] n(n(n(x) + y) + n(x + y)) = y. 4 (wt=11) [para(2,3)] n(n(C) + n(D + n(C))) = D. 8 (wt=21) [para(2',3)] n(n(D + n(C + x) + y) + n(C + x + y)) = D + y. 20 (wt=17) [para(4,3)] n(D + n(C + n(D + n(C)))) = n(D + n(C)). 34 (wt=21) [para(3,3)] n(n(n(n(x) + y) + n(x + y) + z) + n(y + z)) = z. 35 (wt=19) [para(3,3)] n(n(n(n(x) + y) + x + y) + y) = n(n(x) + y). 56 (wt=19) [para(2,34)] n(n(C) + n(D + n(C + n(x)) + n(C + x))) = D. 151 (wt=25) [para(20,3)] n(n(D + n(C + n(D + n(C))) + x) + n(n(D + n(C)) + x)) = x. 152 (wt=17) [para(20,3),demod([2])] n(n(D + n(C)) + n(C + n(D + n(C)))) = D. 173 (wt=26) [para(152,3)] n(D + n(D + n(C) + n(C + n(D + n(C))))) = n(C + n(D + n(C))). 197 (wt=23) [para(2',151)] n(n(C + n(D + n(C))) + n(C + n(C + n(D + n(C))))) = C. 280 (wt=27) [para(35,3)] n(n(n(n(n(x) + y) + x + y) + y + z) + n(n(n(x) + y) + z)) = z. 837 (wt=11) [para(4,151),demod([173])] n(C + n(D + n(C))) = n(C). 839 (wt=11) [back_demod(197),demod([837,837])] n(n(C) + n(C + n(C))) = C. 842 (wt=19) [para(839,3)] n(n(C + x) + n(n(C) + n(C + n(C)) + x)) = x. 844 (wt=17) [para(839,3)] n(C + n(C + n(C + n(C)))) = n(C + n(C)). 883 (wt=19) [para(844,3)] n(n(C + n(C)) + n(C + C + n(C + n(C)))) = C. 946 (wt=30) [para(883,3)] n(C + n(C + n(C) + n(C + C + n(C + n(C))))) = n(C + C + n(C + n(C))). 1706 (wt=13) [para(839,280),demod([946])] n(C + C + n(C + n(C))) = n(C). 1734 (wt=9) [para(1706,8),demod([56]),flip(1)] D + n(C + n(C)) = D. 1745 (wt=9) [para(2',1734'),demod([2])] C + n(C + n(C)) = C. 1802 (wt=9) [para(1745',3),demod([842]),flip(1)] n(C + n(C)) + x = x. ------------ end of proof ------------- ------------- memory usage ------------ Memory dynamically allocated (tp_alloc): 2929. type (bytes each) gets frees in use avail bytes sym_ent ( 96) 54 0 54 0 5.1 K term ( 16) 1509430 1462430 47000 32 911.6 K gen_ptr ( 8) 30395 21281 9114 24 71.4 K context ( 808) 41021757 41021754 3 20 18.1 K trail ( 12) 0 0 0 0 0.0 K bt_node ( 68) 215807175 215807173 2 30 2.1 K ac_position (285432) 50135 50134 1 3 1115.0 K ac_match_pos (14044) 50118395 50118395 0 8 109.7 K ac_match_free_vars_pos (4020) 996280 996280 0 3 11.8 K discrim ( 12) 18 0 18 0 0.2 K flat ( 40) 347417 347417 0 4 0.2 K discrim_pos ( 12) 64075 64075 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) 5612 3810 1802 0 21.1 K clause ( 24) 5612 3810 1802 0 42.2 K list ( 12) 1857 1801 56 3 0.7 K list_pos ( 20) 7619 1047 6572 332 134.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 11579 Clauses generated 5609 Forward subsumed 1796 Deleted by weight 2014 Deleted by variable count 0 Kept 1799 New demodulators 1796 Back demodulated 209 Ordered paramod prunes 0 Basic paramod prunes 229228 Prime paramod prunes 0 Semantic prunes 0 Rewrite attmepts 154061 Rewrites 5451 FPA overloads 0 FPA underloads 0 Usable size 0 Sos size 1591 Demodulators size 1589 Passive size 1 Disabled size 209 Proofs found 1 ----------- times (seconds) ----------- Thu Jun 13 17:01:56 1996 user time 1902.90 (0 hr, 31 min, 42 sec) system time 2.24 (0 hr, 0 min, 2 sec) wall-clock time 1921 (0 hr, 32 min, 1 sec) input time 0.01 paramodulation time 9.59 demodulation time 1172.86 orient time 0.12 weigh time 0.12 forward subsume time 101.08 back demod find time 613.02 conflict time 1.89 LRPO time 0.00 store clause time 0.71 disable clause time 0.27 prime paramod time 0.00 semantics time 0.00