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