%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX196+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:05:23 PM UTC 2026 % Result : Unknown 3.41s 3.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX196+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.16/0.34 % Computer : n011.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue May 5 11:00:02 EDT 2026 % 0.16/0.34 % CPUTime : % 2.05/2.27 ----- Otter 3.3f, August 2004 ----- % 2.05/2.27 The process was started by sandbox2 on n011.cluster.edu, % 2.05/2.27 Tue May 5 11:00:02 2026 % 2.05/2.27 The command was "./otter". The process ID is 14444. % 2.05/2.27 % 2.05/2.27 set(prolog_style_variables). % 2.05/2.27 set(auto). % 2.05/2.27 dependent: set(auto1). % 2.05/2.27 dependent: set(process_input). % 2.05/2.27 dependent: clear(print_kept). % 2.05/2.27 dependent: clear(print_new_demod). % 2.05/2.27 dependent: clear(print_back_demod). % 2.05/2.27 dependent: clear(print_back_sub). % 2.05/2.27 dependent: set(control_memory). % 2.05/2.27 dependent: assign(max_mem, 12000). % 2.05/2.27 dependent: assign(pick_given_ratio, 4). % 2.05/2.27 dependent: assign(stats_level, 1). % 2.05/2.27 dependent: assign(max_seconds, 10800). % 2.05/2.27 clear(print_given). % 2.05/2.27 % 2.05/2.27 formula_list(usable). % 2.05/2.27 all A (A=A). % 2.05/2.27 all X X2 (head(cons(X,X2))=X). % 2.05/2.27 all X X2 (tail(cons(X,X2))=X2). % 2.05/2.27 all X X2 (nil!=cons(X,X2)). % 2.05/2.27 all X (proj1Suc(suc(X))=X). % 2.05/2.27 all X (zero!=suc(X)). % 2.05/2.27 all X (proj1N(n(X))=X). % 2.05/2.27 all X X2 (proj1Add(add(X,X2))=X). % 2.05/2.27 all X X2 (proj2Add(add(X,X2))=X2). % 2.05/2.27 all X X2 (proj1Mul(mul(X,X2))=X). % 2.05/2.27 all X X2 (proj2Mul(mul(X,X2))=X2). % 2.05/2.27 all X X2 (proj1Eq(e_q(X,X2))=X). % 2.05/2.27 all X X2 (proj2Eq(e_q(X,X2))=X2). % 2.05/2.27 all X (proj1V(v(X))=X). % 2.05/2.27 all X X2 X3 (n(X)!=add(X2,X3)). % 2.05/2.27 all X X2 X3 (n(X)!=mul(X2,X3)). % 2.05/2.27 all X X2 X3 (n(X)!=e_q(X2,X3)). % 2.05/2.27 all X X2 (n(X)!=v(X2)). % 2.05/2.27 all X X2 X3 X4 (add(X,X2)!=mul(X3,X4)). % 2.05/2.27 all X X2 X3 X4 (add(X,X2)!=e_q(X3,X4)). % 2.05/2.27 all X X2 X3 (add(X,X2)!=v(X3)). % 2.05/2.27 all X X2 X3 X4 (mul(X,X2)!=e_q(X3,X4)). % 2.05/2.27 all X X2 X3 (mul(X,X2)!=v(X3)). % 2.05/2.27 all X X2 X3 (e_q(X,X2)!=v(X3)). % 2.05/2.27 all Y B (Y=B->fail1(Y,B)=mul(n(suc(suc(zero))),Y)). % 2.05/2.27 all Y B (Y!=B-> (Y!=add(proj1Add(Y),proj2Add(Y))->fail1(Y,B)=add(Y,B))). % 2.05/2.27 all B A B1 (add(A,B1)!=B->fail1(add(A,B1),B)=add(A,add(B1,B))). % 2.05/2.27 all Y B (B!=n(proj1N(B))->fail(Y,B)=fail1(Y,B)). % 2.05/2.27 all Y (fail(Y,n(zero))=Y). % 2.05/2.27 all Y X2 (fail(Y,n(suc(X2)))=fail1(Y,n(suc(X2)))). % 2.05/2.27 all X5 C (X5!=mul(proj1Mul(X5),proj2Mul(X5))->fail3(X5,C)=mul(X5,C)). % 2.05/2.27 all C A2 B12 (fail3(mul(A2,B12),C)=mul(A2,mul(B12,C))). % 2.05/2.27 all X5 C (C!=n(proj1N(C))->fail22(X5,C)=fail3(X5,C)). % 2.05/2.27 all X5 (fail22(X5,n(zero))=fail3(X5,n(zero))). % 2.05/2.27 all X5 (fail22(X5,n(suc(zero)))=X5). % 2.05/2.27 all X5 X8 (fail22(X5,n(suc(suc(X8))))=fail3(X5,n(suc(suc(X8))))). % 2.05/2.27 all X5 C (X5!=n(proj1N(X5))->fail12(X5,C)=fail22(X5,C)). % 2.05/2.27 all C (fail12(n(zero),C)=fail22(n(zero),C)). % 2.05/2.27 all C (fail12(n(suc(zero)),C)=C). % 2.05/2.27 all C X11 (fail12(n(suc(suc(X11))),C)=fail22(n(suc(suc(X11))),C)). % 2.05/2.27 all X5 C (C!=n(proj1N(C))->fail2(X5,C)=fail12(X5,C)). % 2.05/2.27 all X5 (fail2(X5,n(zero))=n(zero)). % 2.05/2.27 all X5 X13 (fail2(X5,n(suc(X13)))=fail12(X5,n(suc(X13)))). % 2.05/2.27 all X (X!=add(proj1Add(X),proj2Add(X))-> (X!=mul(proj1Mul(X),proj2Mul(X))-> (X!=e_q(proj1Eq(X),proj2Eq(X))->step4(X)=X))). % 2.05/2.27 all Y B (Y!=n(proj1N(Y))->step4(add(Y,B))=fail(Y,B)). % 2.05/2.27 all B (step4(add(n(zero),B))=B). % 2.05/2.27 all B X4 (step4(add(n(suc(X4)),B))=fail(n(suc(X4)),B)). % 2.05/2.27 all X5 C (X5!=n(proj1N(X5))->step4(mul(X5,C))=fail2(X5,C)). % 2.05/2.27 all C (step4(mul(n(zero),C))=n(zero)). % 2.05/2.27 all C X15 (step4(mul(n(suc(X15)),C))=fail2(n(suc(X15)),C)). % 2.05/2.27 all A3 B2 (A3=B2->step4(e_q(A3,B2))=n(suc(zero))). % 2.05/2.27 all A3 B2 (A3!=B2->step4(e_q(A3,B2))=e_q(A3,B2)). % 2.05/2.27 all X (X!=add(proj1Add(X),proj2Add(X))-> (X!=mul(proj1Mul(X),proj2Mul(X))-> (X!=e_q(proj1Eq(X),proj2Eq(X))->simp4(X)=step4(X)))). % 2.05/2.27 all A B (simp4(add(A,B))=step4(add(simp4(A),simp4(B)))). % 2.05/2.27 all C B2 (simp4(mul(C,B2))=step4(mul(simp4(C),simp4(B2)))). % 2.05/2.27 all A2 B3 (simp4(e_q(A2,B3))=step4(e_q(simp4(A2),simp4(B3)))). % 2.05/2.27 all Y (fetch(nil,Y)=zero). % 2.05/2.27 all N St (fetch(cons(N,St),zero)=N). % 2.05/2.27 all N St Z (fetch(cons(N,St),suc(Z))=fetch(St,Z)). % 2.05/2.27 all Y (addNat(zero,Y)=Y). % 2.05/2.27 all Y Z (addNat(suc(Z),Y)=suc(addNat(Z,Y))). % 2.05/2.27 all Y (mulNat(zero,Y)=zero). % 2.05/2.27 all Y Z (mulNat(suc(Z),Y)=addNat(Y,mulNat(Z,Y))). % 2.05/2.27 all X N (eval(X,n(N))=N). % 2.05/2.27 all X A B (eval(X,add(A,B))=addNat(eval(X,A),eval(X,B))). % 2.05/2.27 all X C B2 (eval(X,mul(C,B2))=mulNat(eval(X,C),eval(X,B2))). % 2.05/2.27 all X A2 B3 (eval(X,A2)=eval(X,B3)->eval(X,e_q(A2,B3))=suc(zero)). % 2.05/2.27 all X A2 B3 (eval(X,A2)!=eval(X,B3)->eval(X,e_q(A2,B3))=zero). % 2.05/2.27 all X Z (eval(X,v(Z))=fetch(X,Z)). % 2.05/2.27 -(exists St A (eval(St,A)!=eval(St,simp4(A)))). % 2.05/2.27 end_of_list. % 2.05/2.27 % 2.05/2.27 -------> usable clausifies to: % 2.05/2.27 % 2.05/2.27 list(usable). % 2.05/2.27 0 [] A=A. % 2.05/2.27 0 [] head(cons(X,X2))=X. % 2.05/2.27 0 [] tail(cons(X,X2))=X2. % 2.05/2.27 0 [] nil!=cons(X,X2). % 2.05/2.27 0 [] proj1Suc(suc(X))=X. % 2.05/2.27 0 [] zero!=suc(X). % 2.05/2.27 0 [] proj1N(n(X))=X. % 2.05/2.27 0 [] proj1Add(add(X,X2))=X. % 2.05/2.27 0 [] proj2Add(add(X,X2))=X2. % 2.05/2.27 0 [] proj1Mul(mul(X,X2))=X. % 2.05/2.27 0 [] proj2Mul(mul(X,X2))=X2. % 2.05/2.27 0 [] proj1Eq(e_q(X,X2))=X. % 2.05/2.27 0 [] proj2Eq(e_q(X,X2))=X2. % 2.05/2.27 0 [] proj1V(v(X))=X. % 2.05/2.27 0 [] n(X)!=add(X2,X3). % 2.05/2.27 0 [] n(X)!=mul(X2,X3). % 2.05/2.27 0 [] n(X)!=e_q(X2,X3). % 2.05/2.27 0 [] n(X)!=v(X2). % 2.05/2.27 0 [] add(X,X2)!=mul(X3,X4). % 2.05/2.27 0 [] add(X,X2)!=e_q(X3,X4). % 2.05/2.27 0 [] add(X,X2)!=v(X3). % 2.05/2.27 0 [] mul(X,X2)!=e_q(X3,X4). % 2.05/2.27 0 [] mul(X,X2)!=v(X3). % 2.05/2.27 0 [] e_q(X,X2)!=v(X3). % 2.05/2.27 0 [] Y!=B|fail1(Y,B)=mul(n(suc(suc(zero))),Y). % 2.05/2.27 0 [] Y=B|Y=add(proj1Add(Y),proj2Add(Y))|fail1(Y,B)=add(Y,B). % 2.05/2.27 0 [] add(A,B1)=B|fail1(add(A,B1),B)=add(A,add(B1,B)). % 2.05/2.27 0 [] B=n(proj1N(B))|fail(Y,B)=fail1(Y,B). % 2.05/2.27 0 [] fail(Y,n(zero))=Y. % 2.05/2.27 0 [] fail(Y,n(suc(X2)))=fail1(Y,n(suc(X2))). % 2.05/2.27 0 [] X5=mul(proj1Mul(X5),proj2Mul(X5))|fail3(X5,C)=mul(X5,C). % 2.05/2.27 0 [] fail3(mul(A2,B12),C)=mul(A2,mul(B12,C)). % 2.05/2.27 0 [] C=n(proj1N(C))|fail22(X5,C)=fail3(X5,C). % 2.05/2.27 0 [] fail22(X5,n(zero))=fail3(X5,n(zero)). % 2.05/2.27 0 [] fail22(X5,n(suc(zero)))=X5. % 2.05/2.27 0 [] fail22(X5,n(suc(suc(X8))))=fail3(X5,n(suc(suc(X8)))). % 2.05/2.27 0 [] X5=n(proj1N(X5))|fail12(X5,C)=fail22(X5,C). % 2.05/2.27 0 [] fail12(n(zero),C)=fail22(n(zero),C). % 2.05/2.27 0 [] fail12(n(suc(zero)),C)=C. % 2.05/2.27 0 [] fail12(n(suc(suc(X11))),C)=fail22(n(suc(suc(X11))),C). % 2.05/2.27 0 [] C=n(proj1N(C))|fail2(X5,C)=fail12(X5,C). % 2.05/2.27 0 [] fail2(X5,n(zero))=n(zero). % 2.05/2.27 0 [] fail2(X5,n(suc(X13)))=fail12(X5,n(suc(X13))). % 2.05/2.27 0 [] X=add(proj1Add(X),proj2Add(X))|X=mul(proj1Mul(X),proj2Mul(X))|X=e_q(proj1Eq(X),proj2Eq(X))|step4(X)=X. % 2.05/2.27 0 [] Y=n(proj1N(Y))|step4(add(Y,B))=fail(Y,B). % 2.05/2.27 0 [] step4(add(n(zero),B))=B. % 2.05/2.27 0 [] step4(add(n(suc(X4)),B))=fail(n(suc(X4)),B). % 2.05/2.27 0 [] X5=n(proj1N(X5))|step4(mul(X5,C))=fail2(X5,C). % 2.05/2.27 0 [] step4(mul(n(zero),C))=n(zero). % 2.05/2.27 0 [] step4(mul(n(suc(X15)),C))=fail2(n(suc(X15)),C). % 2.05/2.27 0 [] A3!=B2|step4(e_q(A3,B2))=n(suc(zero)). % 2.05/2.27 0 [] A3=B2|step4(e_q(A3,B2))=e_q(A3,B2). % 2.05/2.27 0 [] X=add(proj1Add(X),proj2Add(X))|X=mul(proj1Mul(X),proj2Mul(X))|X=e_q(proj1Eq(X),proj2Eq(X))|simp4(X)=step4(X). % 2.05/2.27 0 [] simp4(add(A,B))=step4(add(simp4(A),simp4(B))). % 2.05/2.27 0 [] simp4(mul(C,B2))=step4(mul(simp4(C),simp4(B2))). % 2.05/2.27 0 [] simp4(e_q(A2,B3))=step4(e_q(simp4(A2),simp4(B3))). % 2.05/2.27 0 [] fetch(nil,Y)=zero. % 2.05/2.27 0 [] fetch(cons(N,St),zero)=N. % 2.05/2.27 0 [] fetch(cons(N,St),suc(Z))=fetch(St,Z). % 2.05/2.27 0 [] addNat(zero,Y)=Y. % 2.05/2.27 0 [] addNat(suc(Z),Y)=suc(addNat(Z,Y)). % 2.05/2.27 0 [] mulNat(zero,Y)=zero. % 2.05/2.27 0 [] mulNat(suc(Z),Y)=addNat(Y,mulNat(Z,Y)). % 2.05/2.27 0 [] eval(X,n(N))=N. % 2.05/2.27 0 [] eval(X,add(A,B))=addNat(eval(X,A),eval(X,B)). % 2.05/2.27 0 [] eval(X,mul(C,B2))=mulNat(eval(X,C),eval(X,B2)). % 2.05/2.27 0 [] eval(X,A2)!=eval(X,B3)|eval(X,e_q(A2,B3))=suc(zero). % 2.05/2.27 0 [] eval(X,A2)=eval(X,B3)|eval(X,e_q(A2,B3))=zero. % 2.05/2.27 0 [] eval(X,v(Z))=fetch(X,Z). % 2.05/2.27 0 [] eval(St,A)=eval(St,simp4(A)). % 2.05/2.27 end_of_list. % 2.05/2.27 % 2.05/2.27 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4. % 2.05/2.27 % 2.05/2.27 This ia a non-Horn set with equality. The strategy will be % 2.05/2.27 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.05/2.27 deletion, with positive clauses in sos and nonpositive % 2.05/2.27 clauses in usable. % 2.05/2.27 % 2.05/2.27 dependent: set(knuth_bendix). % 2.05/2.27 dependent: set(anl_eq). % 2.05/2.27 dependent: set(para_from). % 2.05/2.27 dependent: set(para_into). % 2.05/2.27 dependent: clear(para_from_right). % 2.05/2.27 dependent: clear(para_into_right). % 2.05/2.27 dependent: set(para_from_vars). % 2.05/2.27 dependent: set(eq_units_both_ways). % 2.05/2.27 dependent: set(dynamic_demod_all). % 2.05/2.27 dependent: set(dynamic_demod). % 2.05/2.27 dependent: set(order_eq). % 2.05/2.27 dependent: set(back_demod). % 2.05/2.27 dependent: set(lrpo). % 2.05/2.27 dependent: set(hyper_res). % 2.05/2.27 dependent: set(unit_deletion). % 2.05/2.27 dependent: set(factor). % 2.05/2.27 % 2.05/2.27 ------------> process usable: % 2.05/2.27 ** KEPT (pick-wt=5): 2 [copy,1,flip.1] cons(A,B)!=nil. % 2.05/2.27 ** KEPT (pick-wt=4): 4 [copy,3,flip.1] suc(A)!=zero. % 2.05/2.27 ** KEPT (pick-wt=6): 5 [] n(A)!=add(B,C). % 2.05/2.27 ** KEPT (pick-wt=6): 6 [] n(A)!=mul(B,C). % 2.05/2.27 ** KEPT (pick-wt=6): 7 [] n(A)!=e_q(B,C). % 2.05/2.27 ** KEPT (pick-wt=5): 8 [] n(A)!=v(B). % 2.05/2.27 ** KEPT (pick-wt=7): 9 [] add(A,B)!=mul(C,D). % 2.05/2.27 ** KEPT (pick-wt=7): 10 [] add(A,B)!=e_q(C,D). % 2.05/2.27 ** KEPT (pick-wt=6): 11 [] add(A,B)!=v(C). % 2.05/2.27 ** KEPT (pick-wt=7): 12 [] mul(A,B)!=e_q(C,D). % 2.05/2.27 ** KEPT (pick-wt=6): 13 [] mul(A,B)!=v(C). % 2.05/2.27 ** KEPT (pick-wt=6): 14 [] e_q(A,B)!=v(C). % 2.05/2.27 ** KEPT (pick-wt=13): 15 [] A!=B|fail1(A,B)=mul(n(suc(suc(zero))),A). % 2.05/2.27 ** KEPT (pick-wt=11): 16 [] A!=B|step4(e_q(A,B))=n(suc(zero)). % 2.05/2.27 ** KEPT (pick-wt=15): 17 [] eval(A,B)!=eval(A,C)|eval(A,e_q(B,C))=suc(zero). % 2.05/2.27 ** KEPT (pick-wt=6): 18 [copy,5,flip.1] add(A,B)!=n(C). % 2.05/2.27 ** KEPT (pick-wt=6): 19 [copy,6,flip.1] mul(A,B)!=n(C). % 2.05/2.27 ** KEPT (pick-wt=6): 20 [copy,7,flip.1] e_q(A,B)!=n(C). % 2.05/2.27 ** KEPT (pick-wt=5): 21 [copy,8,flip.1] v(A)!=n(B). % 2.05/2.27 ** KEPT (pick-wt=7): 22 [copy,9,flip.1] mul(A,B)!=add(C,D). % 2.05/2.27 ** KEPT (pick-wt=7): 23 [copy,10,flip.1] e_q(A,B)!=add(C,D). % 2.05/2.27 ** KEPT (pick-wt=6): 24 [copy,11,flip.1] v(A)!=add(B,C). % 2.05/2.27 ** KEPT (pick-wt=7): 25 [copy,12,flip.1] e_q(A,B)!=mul(C,D). % 2.05/2.27 ** KEPT (pick-wt=6): 26 [copy,13,flip.1] v(A)!=mul(B,C). % 2.05/2.27 ** KEPT (pick-wt=6): 27 [copy,14,flip.1] v(A)!=e_q(B,C). % 2.05/2.27 Following clause subsumed by 5 during input processing: 0 [copy,18,flip.1] n(A)!=add(B,C). % 2.05/2.27 Following clause subsumed by 6 during input processing: 0 [copy,19,flip.1] n(A)!=mul(B,C). % 2.05/2.27 Following clause subsumed by 7 during input processing: 0 [copy,20,flip.1] n(A)!=e_q(B,C). % 2.05/2.27 Following clause subsumed by 8 during input processing: 0 [copy,21,flip.1] n(A)!=v(B). % 2.05/2.27 Following clause subsumed by 9 during input processing: 0 [copy,22,flip.1] add(A,B)!=mul(C,D). % 2.05/2.27 Following clause subsumed by 10 during input processing: 0 [copy,23,flip.1] add(A,B)!=e_q(C,D). % 2.05/2.27 Following clause subsumed by 11 during input processing: 0 [copy,24,flip.1] add(A,B)!=v(C). % 2.05/2.27 Following clause subsumed by 12 during input processing: 0 [copy,25,flip.1] mul(A,B)!=e_q(C,D). % 2.05/2.27 Following clause subsumed by 13 during input processing: 0 [copy,26,flip.1] mul(A,B)!=v(C). % 2.05/2.27 Following clause subsumed by 14 during input processing: 0 [copy,27,flip.1] e_q(A,B)!=v(C). % 2.05/2.27 % 2.05/2.27 ------------> process sos: % 2.05/2.27 ** KEPT (pick-wt=3): 28 [] A=A. % 2.05/2.27 ** KEPT (pick-wt=6): 29 [] head(cons(A,B))=A. % 2.05/2.27 ---> New Demodulator: 30 [new_demod,29] head(cons(A,B))=A. % 2.05/2.27 ** KEPT (pick-wt=6): 31 [] tail(cons(A,B))=B. % 2.05/2.27 ---> New Demodulator: 32 [new_demod,31] tail(cons(A,B))=B. % 2.05/2.27 ** KEPT (pick-wt=5): 33 [] proj1Suc(suc(A))=A. % 2.05/2.27 ---> New Demodulator: 34 [new_demod,33] proj1Suc(suc(A))=A. % 2.05/2.27 ** KEPT (pick-wt=5): 35 [] proj1N(n(A))=A. % 2.05/2.27 ---> New Demodulator: 36 [new_demod,35] proj1N(n(A))=A. % 2.05/2.27 ** KEPT (pick-wt=6): 37 [] proj1Add(add(A,B))=A. % 2.05/2.27 ---> New Demodulator: 38 [new_demod,37] proj1Add(add(A,B))=A. % 2.05/2.27 ** KEPT (pick-wt=6): 39 [] proj2Add(add(A,B))=B. % 2.05/2.27 ---> New Demodulator: 40 [new_demod,39] proj2Add(add(A,B))=B. % 2.05/2.27 ** KEPT (pick-wt=6): 41 [] proj1Mul(mul(A,B))=A. % 2.05/2.27 ---> New Demodulator: 42 [new_demod,41] proj1Mul(mul(A,B))=A. % 2.05/2.27 ** KEPT (pick-wt=6): 43 [] proj2Mul(mul(A,B))=B. % 2.05/2.27 ---> New Demodulator: 44 [new_demod,43] proj2Mul(mul(A,B))=B. % 2.05/2.27 ** KEPT (pick-wt=6): 45 [] proj1Eq(e_q(A,B))=A. % 2.05/2.27 ---> New Demodulator: 46 [new_demod,45] proj1Eq(e_q(A,B))=A. % 2.05/2.27 ** KEPT (pick-wt=6): 47 [] proj2Eq(e_q(A,B))=B. % 2.05/2.27 ---> New Demodulator: 48 [new_demod,47] proj2Eq(e_q(A,B))=B. % 2.05/2.27 ** KEPT (pick-wt=5): 49 [] proj1V(v(A))=A. % 2.05/2.27 ---> New Demodulator: 50 [new_demod,49] proj1V(v(A))=A. % 2.05/2.27 ** KEPT (pick-wt=17): 52 [copy,51,flip.2] A=B|add(proj1Add(A),proj2Add(A))=A|fail1(A,B)=add(A,B). % 2.05/2.27 ** KEPT (pick-wt=16): 53 [] add(A,B)=C|fail1(add(A,B),C)=add(A,add(B,C)). % 2.05/2.27 ** KEPT (pick-wt=12): 55 [copy,54,flip.1,flip.2] n(proj1N(A))=A|fail1(B,A)=fail(B,A). % 2.05/2.27 ** KEPT (pick-wt=6): 56 [] fail(A,n(zero))=A. % 2.05/2.27 ---> New Demodulator: 57 [new_demod,56] fail(A,n(zero))=A. % 2.05/2.27 ** KEPT (pick-wt=11): 59 [copy,58,flip.1] fail1(A,n(suc(B)))=fail(A,n(suc(B))). % 2.05/2.27 ---> New Demodulator: 60 [new_demod,59] fail1(A,n(suc(B)))=fail(A,n(suc(B))). % 2.05/2.27 ** KEPT (pick-wt=14): 62 [copy,61,flip.1,flip.2] mul(proj1Mul(A),proj2Mul(A))=A|mul(A,B)=fail3(A,B). % 2.05/2.27 ** KEPT (pick-wt=11): 64 [copy,63,flip.1] mul(A,mul(B,C))=fail3(mul(A,B),C). % 2.05/2.27 ---> New Demodulator: 65 [new_demod,64] mul(A,mul(B,C))=fail3(mul(A,B),C). % 2.05/2.27 ** KEPT (pick-wt=12): 67 [copy,66,flip.1,flip.2] n(proj1N(A))=A|fail3(B,A)=fail22(B,A). % 2.05/2.27 ** KEPT (pick-wt=9): 69 [copy,68,flip.1] fail3(A,n(zero))=fail22(A,n(zero)). % 2.05/2.27 ---> New Demodulator: 70 [new_demod,69] fail3(A,n(zero))=fail22(A,n(zero)). % 2.05/2.27 ** KEPT (pick-wt=7): 71 [] fail22(A,n(suc(zero)))=A. % 2.05/2.27 ---> New Demodulator: 72 [new_demod,71] fail22(A,n(suc(zero)))=A. % 2.05/2.27 ** KEPT (pick-wt=13): 74 [copy,73,flip.1] fail3(A,n(suc(suc(B))))=fail22(A,n(suc(suc(B)))). % 2.05/2.27 ---> New Demodulator: 75 [new_demod,74] fail3(A,n(suc(suc(B))))=fail22(A,n(suc(suc(B)))). % 2.05/2.27 ** KEPT (pick-wt=12): 77 [copy,76,flip.1,flip.2] n(proj1N(A))=A|fail22(A,B)=fail12(A,B). % 2.05/2.27 ** KEPT (pick-wt=9): 79 [copy,78,flip.1] fail22(n(zero),A)=fail12(n(zero),A). % 2.05/2.27 ---> New Demodulator: 80 [new_demod,79] fail22(n(zero),A)=fail12(n(zero),A). % 2.05/2.27 ** KEPT (pick-wt=7): 81 [] fail12(n(suc(zero)),A)=A. % 2.05/2.27 ---> New Demodulator: 82 [new_demod,81] fail12(n(suc(zero)),A)=A. % 2.05/2.27 ** KEPT (pick-wt=13): 84 [copy,83,flip.1] fail22(n(suc(suc(A))),B)=fail12(n(suc(suc(A))),B). % 2.05/2.27 ---> New Demodulator: 85 [new_demod,84] fail22(n(suc(suc(A))),B)=fail12(n(suc(suc(A))),B). % 2.05/2.27 ** KEPT (pick-wt=12): 87 [copy,86,flip.1] n(proj1N(A))=A|fail2(B,A)=fail12(B,A). % 2.05/2.27 ** KEPT (pick-wt=7): 88 [] fail2(A,n(zero))=n(zero). % 2.05/2.27 ---> New Demodulator: 89 [new_demod,88] fail2(A,n(zero))=n(zero). % 2.05/2.27 ** KEPT (pick-wt=11): 90 [] fail2(A,n(suc(B)))=fail12(A,n(suc(B))). % 2.05/2.27 ---> New Demodulator: 91 [new_demod,90] fail2(A,n(suc(B)))=fail12(A,n(suc(B))). % 2.05/2.27 ** KEPT (pick-wt=25): 93 [copy,92,flip.1,flip.2,flip.3] add(proj1Add(A),proj2Add(A))=A|mul(proj1Mul(A),proj2Mul(A))=A|e_q(proj1Eq(A),proj2Eq(A))=A|step4(A)=A. % 2.05/2.27 ** KEPT (pick-wt=13): 95 [copy,94,flip.1] n(proj1N(A))=A|step4(add(A,B))=fail(A,B). % 2.05/2.27 ** KEPT (pick-wt=7): 96 [] step4(add(n(zero),A))=A. % 2.05/2.27 ---> New Demodulator: 97 [new_demod,96] step4(add(n(zero),A))=A. % 2.05/2.27 ** KEPT (pick-wt=12): 98 [] step4(add(n(suc(A)),B))=fail(n(suc(A)),B). % 2.05/2.27 ---> New Demodulator: 99 [new_demod,98] step4(add(n(suc(A)),B))=fail(n(suc(A)),B). % 2.05/2.27 ** KEPT (pick-wt=13): 101 [copy,100,flip.1] n(proj1N(A))=A|step4(mul(A,B))=fail2(A,B). % 2.05/2.27 ** KEPT (pick-wt=8): 102 [] step4(mul(n(zero),A))=n(zero). % 2.05/2.27 ---> New Demodulator: 103 [new_demod,102] step4(mul(n(zero),A))=n(zero). % 2.05/2.27 ** KEPT (pick-wt=12): 104 [] step4(mul(n(suc(A)),B))=fail2(n(suc(A)),B). % 2.05/2.27 ---> New Demodulator: 105 [new_demod,104] step4(mul(n(suc(A)),B))=fail2(n(suc(A)),B). % 2.05/2.27 ** KEPT (pick-wt=11): 106 [] A=B|step4(e_q(A,B))=e_q(A,B). % 2.05/2.27 ** KEPT (pick-wt=26): 108 [copy,107,flip.1,flip.2,flip.3,flip.4] add(proj1Add(A),proj2Add(A))=A|mul(proj1Mul(A),proj2Mul(A))=A|e_q(proj1Eq(A),proj2Eq(A))=A|step4(A)=simp4(A). % 2.05/2.27 ** KEPT (pick-wt=11): 110 [copy,109,flip.1] step4(add(simp4(A),simp4(B)))=simp4(add(A,B)). % 2.05/2.27 ---> New Demodulator: 111 [new_demod,110] step4(add(simp4(A),simp4(B)))=simp4(add(A,B)). % 2.05/2.27 ** KEPT (pick-wt=11): 113 [copy,112,flip.1] step4(mul(simp4(A),simp4(B)))=simp4(mul(A,B)). % 2.05/2.27 ---> New Demodulator: 114 [new_demod,113] step4(mul(simp4(A),simp4(B)))=simp4(mul(A,B)). % 2.05/2.27 ** KEPT (pick-wt=11): 116 [copy,115,flip.1] step4(e_q(simp4(A),simp4(B)))=simp4(e_q(A,B)). % 2.05/2.27 ---> New Demodulator: 117 [new_demod,116] step4(e_q(simp4(A),simp4(B)))=simp4(e_q(A,B)). % 2.05/2.27 ** KEPT (pick-wt=5): 118 [] fetch(nil,A)=zero. % 2.05/2.27 ---> New Demodulator: 119 [new_demod,118] fetch(nil,A)=zero. % 2.05/2.27 ** KEPT (pick-wt=7): 120 [] fetch(cons(A,B),zero)=A. % 2.05/2.27 ---> New Demodulator: 121 [new_demod,120] fetch(cons(A,B),zero)=A. % 2.05/2.27 ** KEPT (pick-wt=10): 122 [] fetch(cons(A,B),suc(C))=fetch(B,C). % 2.05/2.27 ---> New Demodulator: 123 [new_demod,122] fetch(cons(A,B),suc(C))=fetch(B,C). % 2.05/2.27 ** KEPT (pick-wt=5): 124 [] addNat(zero,A)=A. % 2.05/2.27 ---> New Demodulator: 125 [new_demod,124] addNat(zero,A)=A. % 2.05/2.27 ** KEPT (pick-wt=9): 127 [copy,126,flip.1] suc(addNat(A,B))=addNat(suc(A),B). % 2.05/2.27 ---> New Demodulator: 128 [new_demod,127] suc(addNat(A,B))=addNat(suc(A),B). % 2.05/2.27 ** KEPT (pick-wt=5): 129 [] mulNat(zero,A)=zero. % 2.05/2.27 ---> New Demodulator: 130 [new_demod,129] mulNat(zero,A)=zero. % 2.05/2.27 ** KEPT (pick-wt=10): 131 [] mulNat(suc(A),B)=addNat(B,mulNat(A,B)). % 2.05/2.27 ---> New Demodulator: 132 [new_demod,131] mulNat(suc(A),B)=addNat(B,mulNat(A,B)). % 2.05/2.27 ** KEPT (pick-wt=6): 133 [] eval(A,n(B))=B. % 2.05/2.27 ---> New Demodulator: 134 [new_demod,133] eval(A,n(B))=B. % 2.05/2.27 ** KEPT (pick-wt=13): 135 [] eval(A,add(B,C))=addNat(eval(A,B),eval(A,C)). % 2.05/2.27 ---> New Demodulator: 136 [new_demod,135] eval(A,add(B,C))=addNat(eval(A,B),eval(A,C)). % 2.05/2.27 ** KEPT (pick-wt=13): 138 [copy,137,flip.1] mulNat(eval(A,B),eval(A,C))=eval(A,mul(B,C)). % 2.05/2.27 ---> New Demodulator: 139 [new_demod,138] mulNat(eval(A,B),eval(A,C))=eval(A,mul(B,C)). % 2.05/2.27 ** KEPT (pick-wt=14): 140 [] eval(A,B)=eval(A,C)|eval(A,e_q(B,C))=zero. % 2.05/2.27 ** KEPT (pick-wt=8): 141 [] eval(A,v(B))=fetch(A,B). % 2.05/2.27 ** KEPT (pick-wt=8): 143 [copy,142,flip.1] eval(A,simp4(B))=eval(A,B). % 2.05/2.27 ---> New Demodulator: 144 [new_demod,143] eval(A,simp4(B))=eval(A,B). % 3.41/3.64 Following clause subsumed by 28 during input processing: 0 [copy,28,flip.1] A=A. % 3.41/3.64 >>>> Starting back demodulation with 30. % 3.41/3.64 >>>> Starting back demodulation with 32. % 3.41/3.64 >>>> Starting back demodulation with 34. % 3.41/3.64 >>>> Starting back demodulation with 36. % 3.41/3.64 >>>> Starting back demodulation with 38. % 3.41/3.64 >>>> Starting back demodulation with 40. % 3.41/3.64 >>>> Starting back demodulation with 42. % 3.41/3.64 >>>> Starting back demodulation with 44. % 3.41/3.64 >>>> Starting back demodulation with 46. % 3.41/3.64 >>>> Starting back demodulation with 48. % 3.41/3.64 >>>> Starting back demodulation with 50. % 3.41/3.64 >>>> Starting back demodulation with 57. % 3.41/3.64 >>>> Starting back demodulation with 60. % 3.41/3.64 >>>> Starting back demodulation with 65. % 3.41/3.64 >>>> Starting back demodulation with 70. % 3.41/3.64 >>>> Starting back demodulation with 72. % 3.41/3.64 >>>> Starting back demodulation with 75. % 3.41/3.64 >>>> Starting back demodulation with 80. % 3.41/3.64 >>>> Starting back demodulation with 82. % 3.41/3.64 >>>> Starting back demodulation with 85. % 3.41/3.64 >>>> Starting back demodulation with 89. % 3.41/3.64 >>>> Starting back demodulation with 91. % 3.41/3.64 >>>> Starting back demodulation with 97. % 3.41/3.64 >>>> Starting back demodulation with 99. % 3.41/3.64 >>>> Starting back demodulation with 103. % 3.41/3.64 >>>> Starting back demodulation with 105. % 3.41/3.64 >>>> Starting back demodulation with 111. % 3.41/3.64 >>>> Starting back demodulation with 114. % 3.41/3.64 >>>> Starting back demodulation with 117. % 3.41/3.64 >>>> Starting back demodulation with 119. % 3.41/3.64 >>>> Starting back demodulation with 121. % 3.41/3.64 >>>> Starting back demodulation with 123. % 3.41/3.64 >>>> Starting back demodulation with 125. % 3.41/3.64 >>>> Starting back demodulation with 128. % 3.41/3.64 >>>> Starting back demodulation with 130. % 3.41/3.64 >>>> Starting back demodulation with 132. % 3.41/3.64 >>>> Starting back demodulation with 134. % 3.41/3.64 >>>> Starting back demodulation with 136. % 3.41/3.64 >>>> Starting back demodulation with 139. % 3.41/3.64 ** KEPT (pick-wt=8): 145 [copy,141,flip.1] fetch(A,B)=eval(A,v(B)). % 3.41/3.64 >>>> Starting back demodulation with 144. % 3.41/3.64 Following clause subsumed by 141 during input processing: 0 [copy,145,flip.1] eval(A,v(B))=fetch(A,B). % 3.41/3.64 % 3.41/3.64 ======= end of input processing ======= % 3.41/3.64 % 3.41/3.64 =========== start of search =========== % 3.41/3.64 % 3.41/3.64 % 3.41/3.64 Resetting weight limit to 9. % 3.41/3.64 % 3.41/3.64 % 3.41/3.64 Resetting weight limit to 9. % 3.41/3.64 % 3.41/3.64 sos_size=215 % 3.41/3.64 % 3.41/3.64 % 3.41/3.64 Resetting weight limit to 8. % 3.41/3.64 % 3.41/3.64 % 3.41/3.64 Resetting weight limit to 8. % 3.41/3.64 % 3.41/3.64 sos_size=158 % 3.41/3.64 % 3.41/3.64 Search stopped because sos empty. % 3.41/3.64 % 3.41/3.64 % 3.41/3.64 Search stopped because sos empty. % 3.41/3.64 % 3.41/3.64 ============ end of search ============ % 3.41/3.64 % 3.41/3.64 -------------- statistics ------------- % 3.41/3.64 clauses given 615 % 3.41/3.64 clauses generated 115843 % 3.41/3.64 clauses kept 663 % 3.41/3.64 clauses forward subsumed 1702 % 3.41/3.64 clauses back subsumed 90 % 3.41/3.64 Kbytes malloced 10742 % 3.41/3.64 % 3.41/3.64 ----------- times (seconds) ----------- % 3.41/3.64 user CPU time 1.36 (0 hr, 0 min, 1 sec) % 3.41/3.64 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 3.41/3.64 wall-clock time 3 (0 hr, 0 min, 3 sec) % 3.41/3.64 % 3.41/3.64 Process 14444 finished Tue May 5 11:00:05 2026 % 3.41/3.64 Otter interrupted % 3.41/3.64 PROOF NOT FOUND %------------------------------------------------------------------------------