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