WATCH: 0.00 CPU 0.01 WC ----- Otter 3.3f, August 2004 ----- The process was started by sutcliff on cl5-009, Wed Aug 3 10:34:24 2011 The command was "/CW/home-0/sutcliff/Systems/Otter---3.3/otter". The process ID is 2775. set(prolog_style_variables). set(tptp_eq). 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). formula_list(usable). all X equal(X,X). exists Z W all X Y (equal(Y,W)&equal(Z,X)<->big_f(X,Y)). -(exists W all Y ((exists Z all X (equal(X,Z)<->big_f(X,Y)))<->equal(Y,W))). end_of_list. -------> usable clausifies to: list(usable). 0 [] equal(X,X). 0 [] -equal(Y,$c1)| -equal($c2,X)|big_f(X,Y). 0 [] equal(Y,$c1)| -big_f(X,Y). 0 [] equal($c2,X)| -big_f(X,Y). 0 [] -equal(X,$f1(W))|big_f(X,$f3(W))|equal($f3(W),W). 0 [] equal(X,$f1(W))| -big_f(X,$f3(W))|equal($f3(W),W). 0 [] equal($f2(W,Z),Z)|big_f($f2(W,Z),$f3(W))| -equal($f3(W),W). 0 [] -equal($f2(W,Z),Z)| -big_f($f2(W,Z),$f3(W))| -equal($f3(W),W). end_of_list. SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. This ia a non-Horn set with equality. The strategy will be Knuth-Bendix, ordered hyper_res, factoring, and unit deletion, with positive clauses in sos and nonpositive clauses in usable. dependent: set(knuth_bendix). dependent: set(anl_eq). 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: set(unit_deletion). dependent: set(factor). ------------> process usable: ** KEPT (pick-wt=9): 1 [] -equal(A,$c1)| -equal($c2,B)|big_f(B,A). ** KEPT (pick-wt=6): 2 [] equal(A,$c1)| -big_f(B,A). ** KEPT (pick-wt=6): 3 [] equal($c2,A)| -big_f(A,B). ** KEPT (pick-wt=12): 4 [] -equal(A,$f1(B))|big_f(A,$f3(B))|equal($f3(B),B). ** KEPT (pick-wt=12): 5 [] equal(A,$f1(B))| -big_f(A,$f3(B))|equal($f3(B),B). ** KEPT (pick-wt=15): 6 [] equal($f2(A,B),B)|big_f($f2(A,B),$f3(A))| -equal($f3(A),A). ** KEPT (pick-wt=15): 7 [] -equal($f2(A,B),B)| -big_f($f2(A,B),$f3(A))| -equal($f3(A),A). ------------> process sos: ** KEPT (pick-wt=3): 9 [] equal(A,A). Following clause subsumed by 9 during input processing: 0 [copy,9,flip.1] equal(A,A). ======= end of input processing ======= =========== start of search =========== WATCH: 2.79 CPU 3.02 WC WATCH: 5.79 CPU 6.04 WC  Resetting weight limit to 14. Resetting weight limit to 14. sos_size=4038 -------- PROOF -------- -----> EMPTY CLAUSE at 7.06 sec ----> 4766 [para_from,4751.1.1,87.2.1,demod,4752,unit_del,9,11] $F. Length of proof is 11. Level of proof is 9. ---------------- PROOF ---------------- 1 [] -equal(A,$c1)| -equal($c2,B)|big_f(B,A). 2 [] equal(A,$c1)| -big_f(B,A). 3 [] equal($c2,A)| -big_f(A,B). 4 [] -equal(A,$f1(B))|big_f(A,$f3(B))|equal($f3(B),B). 6 [] equal($f2(A,B),B)|big_f($f2(A,B),$f3(A))| -equal($f3(A),A). 7 [] -equal($f2(A,B),B)| -big_f($f2(A,B),$f3(A))| -equal($f3(A),A). 9 [] equal(A,A). 10 [hyper,9,4] big_f($f1(A),$f3(A))|equal($f3(A),A). 11 [hyper,9,1,9] big_f($c2,$c1). 25 [hyper,10,1,9] big_f($f1($c1),$f3($c1))|big_f($c2,$f3($c1)). 37 [hyper,25,3,flip.2] big_f($c2,$f3($c1))|equal($f1($c1),$c2). 68 [para_from,37.2.1,25.1.1,factor_simp,factor_simp] big_f($c2,$f3($c1)). 83,82 [hyper,68,2] equal($f3($c1),$c1). 84 [hyper,82,6,demod,83] equal($f2($c1,A),A)|big_f($f2($c1,A),$c1). 87 [para_from,82.1.1,7.3.1,demod,83,unit_del,9] -equal($f2($c1,A),A)| -big_f($f2($c1,A),$c1). 95 [para_from,84.1.1,7.2.1,demod,83,83,unit_del,9] -equal($f2($c1,A),A)| -big_f(A,$c1)|big_f($f2($c1,A),$c1). 4749 [hyper,95,84,11,factor_simp] big_f($f2($c1,$c2),$c1). 4752,4751 [hyper,4749,3,flip.1] equal($f2($c1,$c2),$c2). 4766 [para_from,4751.1.1,87.2.1,demod,4752,unit_del,9,11] $F. ------------ end of proof ------------- Search stopped by max_proofs option. Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 158 clauses generated 12785 clauses kept 4763 clauses forward subsumed 6384 clauses back subsumed 525 Kbytes malloced 4882 ----------- times (seconds) ----------- user CPU time 7.06 (0 hr, 0 min, 7 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 7 (0 hr, 0 min, 7 sec) That finishes the proof of the theorem. Process 2775 finished Wed Aug 3 10:34:31 2011 Otter interrupted PROOF FOUND WATCH: 7.34 CPU 7.61 WC FINAL WATCH: 7.34 CPU 7.61 WC