----- Otter 3.2, August 2001 ----- The process was started by ??? on ???, Sun Nov 30 18:22:54 2003 The command was "otter". set(auto). dependent: set(auto1). dependent: set(process_input). dependent: clear(print_kept). dependent: clear(print_new_demod). dependent: clear(print_back_demod). dependent: clear(print_back_sub). dependent: set(control_memory). dependent: assign(max_mem, 12000). dependent: assign(pick_given_ratio, 4). dependent: assign(stats_level, 1). dependent: assign(max_seconds, 10800). clear(print_given). assign(max_distinct_vars,3). assign(max_literals,1). assign(max_mem,64000). assign(max_weight,19). formula_list(usable). all x (x=x). end_of_list. -------> usable clausifies to: list(usable). 0 [] x=x. end_of_list. include("booleanAx.txt"). ------- start included file booleanAx.txt------- include("1_2booleanAx.txt"). ------- start included file 1_2booleanAx.txt------- formula_list(usable). all x y (u(x,y)=u(y,x)). all x y z (u(x,u(y,z))=u(u(x,y),z)). end_of_list. -------> usable clausifies to: list(usable). 0 [] u(x,y)=u(y,x). 0 [] u(x,u(y,z))=u(u(x,y),z). end_of_list. ------- end included file 1_2booleanAx.txt------- include("3booleanAx.txt"). ------- start included file 3booleanAx.txt------- formula_list(usable). all x y (u(c(u(c(x),y)),c(u(c(x),c(y))))=x). end_of_list. -------> usable clausifies to: list(usable). 0 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. end_of_list. ------- end included file 3booleanAx.txt------- ------- end included file booleanAx.txt------- include("iDef.txt"). ------- start included file iDef.txt------- formula_list(usable). all x y (i(x,y)<->u(x,y)=y). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,y)|u(x,y)=y. 0 [] i(x,y)|u(x,y)!=y. end_of_list. ------- end included file iDef.txt------- include("nDef.txt"). ------- start included file nDef.txt------- formula_list(usable). all x y (n(x,y)=c(u(c(x),c(y)))). end_of_list. -------> usable clausifies to: list(usable). 0 [] n(x,y)=c(u(c(x),c(y))). end_of_list. ------- end included file nDef.txt------- include("monotLaws.txt"). ------- start included file monotLaws.txt------- include("1To3monotLaws.txt"). ------- start included file 1To3monotLaws.txt------- formula_list(usable). all x y z (u(x,y)=y->u(k(z,x),k(z,y))=k(z,y)). all x y z (u(x,y)=y->u(c(u(z,y)),c(x))=c(x)). all x y z (u(x,y)=y->u(k(x,z),k(y,z))=k(y,z)). end_of_list. -------> usable clausifies to: list(usable). 0 [] u(x,y)!=y|u(k(z,x),k(z,y))=k(z,y). 0 [] u(x,y)!=y|u(c(u(z,y)),c(x))=c(x). 0 [] u(x,y)!=y|u(k(x,z),k(y,z))=k(y,z). end_of_list. ------- end included file 1To3monotLaws.txt------- include("4_5monotLaws.txt"). ------- start included file 4_5monotLaws.txt------- formula_list(usable). all x y w v i(k(n(x,w),n(y,v)),k(x,y)). all x y w v i(k(n(x,w),n(y,v)),k(w,v)). end_of_list. -------> usable clausifies to: list(usable). 0 [] i(k(n(x,w),n(y,v)),k(x,y)). 0 [] i(k(n(x,w),n(y,v)),k(w,v)). end_of_list. ------- end included file 4_5monotLaws.txt------- ------- end included file monotLaws.txt------- include("i.txt"). ------- start included file i.txt------- formula_list(usable). all x y (i(x,y)->i(r(x),r(y))). all x y (r(u(x,y))=u(r(x),r(y))). all x (r(c(x))=c(r(x))). all x y (r(n(x,y))=n(r(x),r(y))). all x (r(r(x))=x). all x y (r(d(x,y))=d(r(y),r(x))). all x y (r(k(x,y))=k(r(y),r(x))). r(I)=I. r(Z)=Z. r(U)=U. end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(x,y)|i(r(x),r(y)). 0 [] r(u(x,y))=u(r(x),r(y)). 0 [] r(c(x))=c(r(x)). 0 [] r(n(x,y))=n(r(x),r(y)). 0 [] r(r(x))=x. 0 [] r(d(x,y))=d(r(y),r(x)). 0 [] r(k(x,y))=k(r(y),r(x)). 0 [] r(I)=I. 0 [] r(Z)=Z. 0 [] r(U)=U. end_of_list. ------- end included file i.txt------- include("xxix_ghost.txt"). ------- start included file xxix_ghost.txt------- formula_list(usable). all x i(k(x,c(I)),c(n(x,c(k(x,c(I)))))). all x i(k(r(x),n(x,d(c(x),I))),I). end_of_list. -------> usable clausifies to: list(usable). 0 [] i(k(x,c(I)),c(n(x,c(k(x,c(I)))))). 0 [] i(k(r(x),n(x,d(c(x),I))),I). end_of_list. ------- end included file xxix_ghost.txt------- include("xxix_b_ghost.txt"). ------- start included file xxix_b_ghost.txt------- formula_list(usable). -(all x y i(k(r(n(x,d(c(x),I))),y),k(r(x),y))). end_of_list. -------> usable clausifies to: list(usable). 0 [] -i(k(r(n($c2,d(c($c2),I))),$c1),k(r($c2),$c1)). end_of_list. ------- end included file xxix_b_ghost.txt------- SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. This is a Horn set with equality. The strategy will be Knuth-Bendix and hyper_res, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(lrpo). dependent: set(hyper_res). dependent: clear(order_hyper). ------------> process usable: ** KEPT (pick-wt=8): 1 [] -i(x,y)|u(x,y)=y. ** KEPT (pick-wt=8): 2 [] i(x,y)|u(x,y)!=y. ** KEPT (pick-wt=16): 3 [] u(x,y)!=y|u(k(z,x),k(z,y))=k(z,y). ** KEPT (pick-wt=15): 4 [] u(x,y)!=y|u(c(u(z,y)),c(x))=c(x). ** KEPT (pick-wt=16): 5 [] u(x,y)!=y|u(k(x,z),k(y,z))=k(y,z). ** KEPT (pick-wt=8): 6 [] -i(x,y)|i(r(x),r(y)). ** KEPT (pick-wt=14): 7 [] -i(k(r(n($c2,d(c($c2),I))),$c1),k(r($c2),$c1)). ------------> process sos: ** KEPT (pick-wt=3): 8 [] x=x. ** KEPT (pick-wt=7): 9 [] u(x,y)=u(y,x). ** KEPT (pick-wt=11): 11 [copy,10,flip.1] u(u(x,y),z)=u(x,u(y,z)). ---> New Demodulator: 12 [new_demod,11] u(u(x,y),z)=u(x,u(y,z)). ** KEPT (pick-wt=14): 13 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ---> New Demodulator: 14 [new_demod,13] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. ** KEPT (pick-wt=10): 16 [copy,15,flip.1] c(u(c(x),c(y)))=n(x,y). ---> New Demodulator: 17 [new_demod,16] c(u(c(x),c(y)))=n(x,y). ** KEPT (pick-wt=11): 18 [] i(k(n(x,y),n(z,u)),k(x,z)). ** KEPT (pick-wt=11): 19 [] i(k(n(x,y),n(z,u)),k(y,u)). ** KEPT (pick-wt=10): 20 [] r(u(x,y))=u(r(x),r(y)). ---> New Demodulator: 21 [new_demod,20] r(u(x,y))=u(r(x),r(y)). ** KEPT (pick-wt=7): 22 [] r(c(x))=c(r(x)). ---> New Demodulator: 23 [new_demod,22] r(c(x))=c(r(x)). ** KEPT (pick-wt=10): 24 [] r(n(x,y))=n(r(x),r(y)). ---> New Demodulator: 25 [new_demod,24] r(n(x,y))=n(r(x),r(y)). ** KEPT (pick-wt=5): 26 [] r(r(x))=x. ---> New Demodulator: 27 [new_demod,26] r(r(x))=x. ** KEPT (pick-wt=10): 28 [] r(d(x,y))=d(r(y),r(x)). ---> New Demodulator: 29 [new_demod,28] r(d(x,y))=d(r(y),r(x)). ** KEPT (pick-wt=10): 30 [] r(k(x,y))=k(r(y),r(x)). ---> New Demodulator: 31 [new_demod,30] r(k(x,y))=k(r(y),r(x)). ** KEPT (pick-wt=4): 32 [] r(I)=I. ---> New Demodulator: 33 [new_demod,32] r(I)=I. ** KEPT (pick-wt=4): 34 [] r(Z)=Z. ---> New Demodulator: 35 [new_demod,34] r(Z)=Z. ** KEPT (pick-wt=4): 36 [] r(U)=U. ---> New Demodulator: 37 [new_demod,36] r(U)=U. ** KEPT (pick-wt=13): 38 [] i(k(x,c(I)),c(n(x,c(k(x,c(I)))))). ** KEPT (pick-wt=11): 39 [] i(k(r(x),n(x,d(c(x),I))),I). Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] x=x. Following clause subsumed by 9 during input processing: 0 [copy,9,flip.1] u(x,y)=u(y,x). >>>> Starting back demodulation with 12. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 17. >> back demodulating 13 with 17. >>>> Starting back demodulation with 21. >>>> Starting back demodulation with 23. >>>> Starting back demodulation with 25. >> back demodulating 7 with 25. >>>> Starting back demodulation with 27. >>>> Starting back demodulation with 29. >>>> Starting back demodulation with 31. >>>> Starting back demodulation with 33. >>>> Starting back demodulation with 35. >>>> Starting back demodulation with 37. >>>> Starting back demodulation with 41. ======= end of input processing ======= =========== start of search =========== ----> UNIT CONFLICT at 1.35 sec ----> 7231 [binary,7230.1,109.1] $F. Length of proof is 108. Level of proof is 31. ---------------- PROOF ---------------- 1 [] -i(x,y)|u(x,y)=y. 2 [] i(x,y)|u(x,y)!=y. 7 [] -i(k(r(n($c2,d(c($c2),I))),$c1),k(r($c2),$c1)). 9 [] u(x,y)=u(y,x). 10 [] u(x,u(y,z))=u(u(x,y),z). 12,11 [copy,10,flip.1] u(u(x,y),z)=u(x,u(y,z)). 13 [] u(c(u(c(x),y)),c(u(c(x),c(y))))=x. 15 [] n(x,y)=c(u(c(x),c(y))). 17,16 [copy,15,flip.1] c(u(c(x),c(y)))=n(x,y). 19 [] i(k(n(x,y),n(z,u)),k(y,u)). 23,22 [] r(c(x))=c(r(x)). 25,24 [] r(n(x,y))=n(r(x),r(y)). 29,28 [] r(d(x,y))=d(r(y),r(x)). 33,32 [] r(I)=I. 40 [back_demod,13,demod,17] u(c(u(c(x),y)),n(x,y))=x. 42 [back_demod,7,demod,25,29,33,23] -i(k(n(r($c2),d(I,c(r($c2)))),$c1),k(r($c2),$c1)). 43 [para_into,16.1.1.1.1,16.1.1] c(u(n(x,y),c(z)))=n(u(c(x),c(y)),z). 45 [para_into,16.1.1.1.2,16.1.1] c(u(c(x),n(y,z)))=n(x,u(c(y),c(z))). 47 [para_into,16.1.1.1,9.1.1,demod,17] n(x,y)=n(y,x). 48 [para_into,11.1.1.1,9.1.1,demod,12] u(x,u(y,z))=u(y,u(x,z)). 49 [para_into,11.1.1,9.1.1] u(x,u(y,z))=u(y,u(z,x)). 50 [copy,49,flip.1] u(x,u(y,z))=u(z,u(x,y)). 90 [para_into,40.1.1.1.1,9.1.1] u(c(u(x,c(y))),n(y,x))=y. 92 [para_into,40.1.1.1,16.1.1] u(n(x,y),n(x,c(y)))=x. 94 [para_into,40.1.1.2,47.1.1] u(c(u(c(x),y)),n(y,x))=x. 97,96 [para_into,40.1.1,9.1.1] u(n(x,y),c(u(c(x),y)))=x. 98 [para_from,40.1.1,11.1.1.1,flip.1] u(c(u(c(x),y)),u(n(x,y),z))=u(x,z). 109 [para_into,42.1.1.1,47.1.1] -i(k(n(d(I,c(r($c2))),r($c2)),$c1),k(r($c2),$c1)). 110 [para_into,92.1.1.1,47.1.1] u(n(x,y),n(y,c(x)))=y. 114 [para_into,92.1.1.2,47.1.1] u(n(x,y),n(c(y),x))=x. 124 [para_into,110.1.1.2,47.1.1] u(n(x,y),n(c(x),y))=y. 126 [para_into,110.1.1,9.1.1] u(n(x,c(y)),n(y,x))=x. 128 [para_from,110.1.1,11.1.1.1,flip.1] u(n(x,y),u(n(y,c(x)),z))=u(y,z). 132 [para_into,114.1.1,9.1.1] u(n(c(x),y),n(y,x))=y. 134 [para_from,114.1.1,11.1.1.1,flip.1] u(n(x,y),u(n(c(y),x),z))=u(x,z). 143 [para_into,124.1.1,9.1.1] u(n(c(x),y),n(x,y))=y. 149 [para_from,126.1.1,11.1.1.1,flip.1] u(n(x,c(y)),u(n(y,x),z))=u(x,z). 156 [para_into,45.1.1.1,40.1.1,flip.1] n(u(c(x),y),u(c(x),c(y)))=c(x). 175,174 [para_into,48.1.1.2,110.1.1,flip.1] u(n(x,y),u(z,n(y,c(x))))=u(z,y). 180 [para_into,48.1.1,9.1.1,demod,12] u(x,u(y,z))=u(x,u(z,y)). 183 [para_into,49.1.1.2,9.1.1] u(x,u(y,z))=u(z,u(y,x)). 203 [para_into,90.1.1.2,47.1.1] u(c(u(x,c(y))),n(x,y))=y. 205 [para_into,90.1.1,9.1.1] u(n(x,y),c(u(y,c(x))))=x. 207 [para_from,90.1.1,45.1.1.1,flip.1] n(u(x,c(y)),u(c(y),c(x)))=c(y). 230 [para_into,94.1.1,9.1.1] u(n(x,y),c(u(c(y),x)))=y. 255 [para_from,96.1.1,43.1.1.1,flip.1] n(u(c(x),c(y)),u(c(x),y))=c(x). 305 [para_from,203.1.1,45.1.1.1,flip.1] n(u(x,c(y)),u(c(x),c(y)))=c(y). 330 [para_from,205.1.1,43.1.1.1,flip.1] n(u(c(x),c(y)),u(y,c(x)))=c(x). 352 [para_from,230.1.1,43.1.1.1,flip.1] n(u(c(x),c(y)),u(c(y),x))=c(y). 665,664 [para_into,98.1.1.2,143.1.1] u(c(u(c(c(x)),y)),y)=u(c(x),n(x,y)). 666 [para_into,98.1.1.2,132.1.1,demod,665] u(c(x),n(x,y))=u(c(x),n(y,x)). 668,667 [para_into,98.1.1.2,126.1.1,demod,17] u(n(x,y),x)=u(x,n(y,x)). 670,669 [para_into,98.1.1.2,124.1.1] u(c(u(c(x),y)),y)=u(x,n(c(x),y)). 674 [para_into,98.1.1.2,110.1.1,demod,670] u(x,n(c(x),y))=u(x,n(y,c(x))). 687 [copy,674,flip.1] u(x,n(y,c(x)))=u(x,n(c(x),y)). 966 [para_into,666.1.1,9.1.1] u(n(x,y),c(x))=u(c(x),n(y,x)). 967 [copy,966,flip.1] u(c(x),n(y,x))=u(n(x,y),c(x)). 998,997 [para_into,128.1.1.2,143.1.1] u(n(x,c(y)),c(x))=u(c(y),n(y,c(x))). 1062 [para_into,687.1.1,9.1.1] u(n(x,c(y)),y)=u(y,n(c(y),x)). 1173 [para_into,967.1.1,9.1.1] u(n(x,y),c(y))=u(n(y,x),c(y)). 1268 [para_from,1173.1.1,134.1.1.2,demod,998,175] u(c(x),x)=u(y,c(y)). 1269 [copy,1268,flip.1] u(x,c(x))=u(c(y),y). 1272 [para_into,1268.1.1,1268.1.1] u(x,c(x))=u(y,c(y)). 1288 [para_from,1268.1.1,330.1.1.2] n(u(c(x),c(c(c(x)))),u(y,c(y)))=c(x). 1293,1292 [para_from,1268.1.1,207.1.1.2] n(u(x,c(c(x))),u(y,c(y)))=c(c(x)). 1319 [para_from,1268.1.1,156.1.1.2] n(u(c(c(x)),x),u(y,c(y)))=c(c(x)). 1326 [para_from,1268.1.1,16.1.1.1] c(u(x,c(x)))=n(c(y),y). 1331 [para_from,1268.1.1,94.1.1.1.1] u(c(u(x,c(x))),n(y,y))=y. 1333 [para_from,1268.1.1,183.1.1.2] u(x,u(y,c(y)))=u(z,u(c(z),x)). 1337 [para_from,1268.1.1,48.1.1.2] u(x,u(y,c(y)))=u(c(z),u(x,z)). 1338 [para_from,1268.1.1,11.1.1.1,demod,12] u(x,u(c(x),y))=u(c(z),u(z,y)). 1339 [back_demod,1288,demod,1293] c(c(c(x)))=c(x). 1343 [copy,1326,flip.1] n(c(x),x)=c(u(y,c(y))). 1347 [copy,1337,flip.1] u(c(x),u(y,x))=u(y,u(z,c(z))). 1417,1416 [para_from,1339.1.1,16.1.1.1.1,demod,17,flip.1] n(c(c(x)),y)=n(x,y). 1421,1420 [para_from,1339.1.1,96.1.1.2.1.1,demod,1417,97,flip.1] c(c(x))=x. 1438 [back_demod,1319,demod,1421,1421] n(u(x,x),u(y,c(y)))=x. 1513,1512 [para_into,1420.1.1.1,16.1.1] c(n(x,y))=u(c(x),c(y)). 1607 [para_from,1420.1.1,352.1.1.2.1,demod,1421,1421] n(u(c(x),y),u(y,x))=y. 1615 [para_from,1420.1.1,305.1.1.1.2,demod,1421,1421] n(u(x,y),u(c(x),y))=y. 1634 [para_from,1420.1.1,16.1.1.1.2] c(u(c(x),y))=n(x,c(y)). 1646 [para_from,1420.1.1,255.1.1.1.1,demod,1421,1421] n(u(x,c(y)),u(x,y))=x. 1648 [para_from,1420.1.1,156.1.1.2.1,demod,1421,1421] n(u(x,y),u(x,c(y)))=x. 1656,1655 [para_from,1420.1.1,16.1.1.1.1] c(u(x,c(y)))=n(c(x),y). 1723 [back_demod,1343,demod,1656] n(c(x),x)=n(c(y),y). 1725 [back_demod,1331,demod,1656] u(n(c(x),x),n(y,y))=y. 1741 [para_into,1269.1.1.2,1420.1.1] u(c(x),x)=u(c(y),y). 1762 [para_from,1269.1.1,50.1.1.2] u(x,u(c(y),y))=u(c(z),u(x,z)). 1770 [copy,1762,flip.1] u(c(x),u(y,x))=u(y,u(c(z),z)). 1787 [para_from,1272.1.1,180.1.1.2] u(x,u(y,c(y)))=u(x,u(c(z),z)). 1794 [para_into,1723.1.1.1,1420.1.1] n(x,c(x))=n(c(y),y). 1795 [copy,1794,flip.1] n(c(x),x)=n(y,c(y)). 1801 [para_from,1723.1.1,1062.1.1.1,demod,1421] u(n(c(x),x),y)=u(y,n(c(y),y)). 1836 [para_into,1741.1.1,180.1.1] u(c(u(x,y)),u(y,x))=u(c(z),z). 1895,1894 [para_into,149.1.1.2,149.1.1] u(n(c(x),c(y)),u(y,z))=u(c(x),u(n(x,y),z)). 1938 [para_into,1438.1.1.2.2,1420.1.1] n(u(x,x),u(c(y),y))=x. 2390,2389 [para_into,1634.1.1.1.1,1420.1.1] c(u(x,y))=n(c(x),c(y)). 2433 [back_demod,1836,demod,2390,1895,668] u(c(x),u(x,n(y,x)))=u(c(z),z). 2690,2689 [para_from,1725.1.1,149.1.1.2,demod,1421] u(n(x,x),y)=u(x,n(y,y)). 2706 [para_from,1725.1.1,1615.1.1.1,demod,1513,1421,12] n(x,u(y,u(c(y),n(x,x))))=n(x,x). 2747 [para_into,1938.1.1.1,48.1.1,demod,12] n(u(x,u(x,u(y,y))),u(c(z),z))=u(x,y). 3118,3117 [para_from,2689.1.1,11.1.1.1,demod,12,2690,2690] u(x,u(y,n(z,z)))=u(x,n(u(y,z),u(y,z))). 3130 [back_demod,2706,demod,3118] n(x,u(y,n(u(c(y),x),u(c(y),x))))=n(x,x). 3507 [para_from,1333.1.1,1646.1.1.2,demod,2390,1421] n(u(x,n(c(y),y)),u(z,u(c(z),x)))=x. 3914 [hyper,1347,2,demod,2390,1421] i(n(c(x),x),u(y,u(x,c(x)))). 3928 [para_into,3914.1.1,1795.1.1] i(n(x,c(x)),u(y,u(z,c(z)))). 3962 [para_into,3928.1.2,1338.1.1,demod,1421] i(n(x,c(x)),u(c(y),u(y,z))). 4026,4025 [hyper,3962,1] u(n(x,c(x)),u(c(y),u(y,z)))=u(c(y),u(y,z)). 5335 [para_from,1770.1.1,1607.1.1.1,demod,12] n(u(x,u(c(y),y)),u(x,u(z,z)))=u(x,z). 5372 [para_from,1787.1.1,1648.1.1.1,demod,2390,1421] n(u(x,u(c(y),y)),u(x,n(c(z),z)))=x. 5645 [para_from,1801.1.1,149.1.1.2,demod,1421,2690] u(x,n(u(y,n(c(y),y)),u(y,n(c(y),y))))=u(x,y). 6818 [para_into,2433.1.1.2.2,1938.1.1,demod,2390,1421,12,4026] u(c(x),u(x,y))=u(c(z),z). 6967,6966 [para_from,6818.1.1,1615.1.1.2] n(u(x,u(x,y)),u(c(z),z))=u(x,y). 6982,6981 [back_demod,2747,demod,6967] u(x,u(y,y))=u(x,y). 6999,6998 [back_demod,5335,demod,6982] n(u(x,u(c(y),y)),u(x,z))=u(x,z). 7049,7048 [back_demod,5372,demod,6999] u(x,n(c(y),y))=x. 7087,7086 [back_demod,5645,demod,7049,7049] u(x,n(y,y))=u(x,y). 7119,7118 [back_demod,3507,demod,7049] n(x,u(y,u(c(y),x)))=x. 7173 [back_demod,3130,demod,7087,7119,flip.1] n(x,x)=x. 7230 [para_from,7173.1.1,19.1.1.2] i(k(n(x,y),z),k(y,z)). 7231 [binary,7230.1,109.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 358 clauses generated 23325 clauses kept 5111 clauses forward subsumed 13063 clauses back subsumed 379 Kbytes malloced 4470 ----------- times (seconds) ----------- user CPU time 1.55 (0 hr, 0 min, 1 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 2 (0 hr, 0 min, 2 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.00 demod time 0.00 That finishes the proof of the theorem. Process 0 finished Sun Nov 30 18:22:56 2003