%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX218-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n025.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:26 PM UTC 2026 % Result : Unknown 2.23s 2.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SWX218-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.10 % Command : otter-tptp-script %s % 0.11/0.30 % Computer : n025.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Tue May 5 12:19:28 EDT 2026 % 0.11/0.30 % CPUTime : % 2.23/2.51 ----- Otter 3.3f, August 2004 ----- % 2.23/2.51 The process was started by sandbox on n025.cluster.edu, % 2.23/2.51 Tue May 5 12:19:28 2026 % 2.23/2.51 The command was "./otter". The process ID is 25200. % 2.23/2.51 % 2.23/2.51 set(prolog_style_variables). % 2.23/2.51 set(auto). % 2.23/2.51 dependent: set(auto1). % 2.23/2.51 dependent: set(process_input). % 2.23/2.51 dependent: clear(print_kept). % 2.23/2.51 dependent: clear(print_new_demod). % 2.23/2.51 dependent: clear(print_back_demod). % 2.23/2.51 dependent: clear(print_back_sub). % 2.23/2.51 dependent: set(control_memory). % 2.23/2.51 dependent: assign(max_mem, 12000). % 2.23/2.51 dependent: assign(pick_given_ratio, 4). % 2.23/2.51 dependent: assign(stats_level, 1). % 2.23/2.51 dependent: assign(max_seconds, 10800). % 2.23/2.51 clear(print_given). % 2.23/2.51 % 2.23/2.51 list(usable). % 2.23/2.51 0 [] A=A. % 2.23/2.51 0 [] aux(Y,Q,Sa,Rhs,btrue)=Rhs. % 2.23/2.51 0 [] aux(Y,Q,Sa,Rhs,bfalse)=apply(Q,Y). % 2.23/2.51 0 [] aux2(Y,Z,X2,S,pair23(Y1,Lft1))=right(tuple2(S,Lft1,cons2(Y1,cons2(Z,X2)))). % 2.23/2.51 0 [] aux3(X,S,Lft,X1,Rgt,pair24(X12,What1))=act(What1,Lft,X12,Rgt). % 2.23/2.51 0 [] aux4(X,S,Lft,Rgt,pair23(X1,Rgt2))=aux3(X,S,Lft,X1,Rgt2,apply(X,pair22(S,X1))). % 2.23/2.51 0 [] aux5(X,Y,left(Tape))=Tape. % 2.23/2.51 0 [] aux5(X,Y,right(St))=steps(X,St). % 2.23/2.51 0 [] aux6(X,nil2)=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,nil2))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,nil2)))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,nil2))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2)))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2)))))))=btrue. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(X14,X15))))))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(o,X13)))))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(a2,X13)))))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(o,X11))))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(a2,X11))))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(o,X9)))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(a2,cons2(b,X9)))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(o,X7))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(a2,cons2(b,X7))))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(o,X5)))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(a2,cons2(b,X5)))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(o,X3))=bfalse. % 2.23/2.51 0 [] aux6(X,cons2(b,X3))=bfalse. % 2.23/2.51 0 [] aux7(X,nil2)=bfalse. % 2.23/2.51 0 [] aux7(X,cons2(a2,nil2))=aux6(X,runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))). % 2.23/2.51 0 [] aux7(X,cons2(a2,cons2(X16,X17)))=bfalse. % 2.23/2.51 0 [] aux7(X,cons2(o,Z))=bfalse. % 2.23/2.51 0 [] aux7(X,cons2(b,Z))=bfalse. % 2.23/2.51 0 [] split(nil2)=pair23(o,nil2). % 2.23/2.51 0 [] split(cons2(Y,Xs))=pair23(Y,Xs). % 2.23/2.51 0 [] rev(nil2,Y)=Y. % 2.23/2.51 0 [] rev(cons2(o,Xs),Y)=Y. % 2.23/2.51 0 [] rev(cons2(a2,Xs),Y)=rev(Xs,cons2(a2,Y)). % 2.23/2.51 0 [] rev(cons2(b,Xs),Y)=rev(Xs,cons2(b,Y)). % 2.23/2.51 0 [] one=succ(zero). % 2.23/2.51 0 [] two=succ(one). % 2.23/2.51 0 [] apply(nil,Y)=pair24(o,stp). % 2.23/2.51 0 [] apply(cons(pair2(Sa,Rhs),Q),Y)=aux(Y,Q,Sa,Rhs,e_q(Sa,Y)). % 2.23/2.51 0 [] act(lft(S),Y,Z,X2)=aux2(Y,Z,X2,S,split(Y)). % 2.23/2.51 0 [] act(rgt(T),Y,Z,X2)=right(tuple2(T,cons2(Z,Y),X2)). % 2.23/2.51 0 [] act(stp,Y,Z,X2)=left(rev(Y,cons2(Z,X2))). % 2.23/2.51 0 [] step(X,tuple2(S,Lft,Rgt))=aux4(X,S,Lft,Rgt,split(Rgt)). % 2.23/2.51 0 [] steps(X,Y)=aux5(X,Y,step(X,Y)). % 2.23/2.51 0 [] runt(X,Y)=steps(X,tuple2(zero,nil2,Y)). % 2.23/2.51 0 [] prog0(X)=aux7(X,runt(X,cons2(a2,nil2))). % 2.23/2.51 0 [] prop_help(X,Y,Z,X2,X3)=e_q3(prog0(cons(pair2(pair22(zero,a2),X),cons(pair2(pair22(zero,b),Y),cons(pair2(pair22(one,a2),Z),cons(pair2(pair22(one,b),X2),cons(pair2(pair22(two,a2),X3),nil)))))),bfalse). % 2.23/2.51 0 [] e_q3(bfalse,btrue)=bfalse. % 2.23/2.51 0 [] e_q3(btrue,bfalse)=bfalse. % 2.23/2.51 0 [] e_q5(o,a2)=bfalse. % 2.23/2.51 0 [] e_q5(o,b)=bfalse. % 2.23/2.51 0 [] e_q5(a2,o)=bfalse. % 2.23/2.51 0 [] e_q5(a2,b)=bfalse. % 2.23/2.51 0 [] e_q5(b,o)=bfalse. % 2.23/2.51 0 [] e_q5(b,a2)=bfalse. % 2.23/2.51 0 [] e_q2(succ(X),succ(Y))=e_q2(X,Y). % 2.23/2.51 0 [] e_q2(zero,succ(X))=bfalse. % 2.23/2.51 0 [] e_q2(succ(X),zero)=bfalse. % 2.23/2.51 0 [] e_q4(lft(X),lft(Y))=e_q2(X,Y). % 2.23/2.51 0 [] e_q4(rgt(X),rgt(Y))=e_q2(X,Y). % 2.23/2.51 0 [] e_q4(lft(X),rgt(Y))=bfalse. % 2.23/2.51 0 [] e_q4(lft(X),stp)=bfalse. % 2.23/2.51 0 [] e_q4(rgt(X),lft(Y))=bfalse. % 2.23/2.51 0 [] e_q4(rgt(X),stp)=bfalse. % 2.23/2.51 0 [] e_q4(stp,lft(X))=bfalse. % 2.23/2.51 0 [] e_q4(stp,rgt(X))=bfalse. % 2.23/2.51 0 [] e_q(X,X)=btrue. % 2.23/2.51 0 [] e_q2(X,X)=btrue. % 2.23/2.51 0 [] e_q3(X,X)=btrue. % 2.23/2.51 0 [] e_q4(X,X)=btrue. % 2.23/2.51 0 [] e_q5(X,X)=btrue. % 2.23/2.51 0 [] e_q2(X,Z)!=bfalse|e_q(pair22(X,Y),pair22(Z,X2))=bfalse. % 2.23/2.51 0 [] e_q2(X,Z)!=btrue|e_q(pair22(X,Y),pair22(Z,X2))=e_q5(Y,X2). % 2.23/2.51 0 [] e_q3(prop_help(X,Y,Z,X2,X3),bfalse)!=btrue. % 2.23/2.51 end_of_list. % 2.23/2.51 % 2.23/2.51 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. % 2.23/2.51 % 2.23/2.51 This is a Horn set with equality. The strategy will be % 2.23/2.51 Knuth-Bendix and hyper_res, with positive clauses in % 2.23/2.51 sos and nonpositive clauses in usable. % 2.23/2.51 % 2.23/2.51 dependent: set(knuth_bendix). % 2.23/2.51 dependent: set(anl_eq). % 2.23/2.51 dependent: set(para_from). % 2.23/2.51 dependent: set(para_into). % 2.23/2.51 dependent: clear(para_from_right). % 2.23/2.51 dependent: clear(para_into_right). % 2.23/2.51 dependent: set(para_from_vars). % 2.23/2.51 dependent: set(eq_units_both_ways). % 2.23/2.51 dependent: set(dynamic_demod_all). % 2.23/2.51 dependent: set(dynamic_demod). % 2.23/2.51 dependent: set(order_eq). % 2.23/2.51 dependent: set(back_demod). % 2.23/2.51 dependent: set(lrpo). % 2.23/2.51 dependent: set(hyper_res). % 2.23/2.51 dependent: clear(order_hyper). % 2.23/2.51 % 2.23/2.51 ------------> process usable: % 2.23/2.51 ** KEPT (pick-wt=14): 1 [] e_q2(A,B)!=bfalse|e_q(pair22(A,C),pair22(B,D))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=16): 2 [] e_q2(A,B)!=btrue|e_q(pair22(A,C),pair22(B,D))=e_q5(C,D). % 2.23/2.51 ** KEPT (pick-wt=10): 3 [] e_q3(prop_help(A,B,C,D,E),bfalse)!=btrue. % 2.23/2.51 % 2.23/2.51 ------------> process sos: % 2.23/2.51 ** KEPT (pick-wt=3): 4 [] A=A. % 2.23/2.51 ** KEPT (pick-wt=8): 5 [] aux(A,B,C,D,btrue)=D. % 2.23/2.51 ---> New Demodulator: 6 [new_demod,5] aux(A,B,C,D,btrue)=D. % 2.23/2.51 ** KEPT (pick-wt=10): 7 [] aux(A,B,C,D,bfalse)=apply(B,A). % 2.23/2.51 ** KEPT (pick-wt=18): 8 [] aux2(A,B,C,D,pair23(E,F))=right(tuple2(D,F,cons2(E,cons2(B,C)))). % 2.23/2.51 ** KEPT (pick-wt=15): 9 [] aux3(A,B,C,D,E,pair24(F,G))=act(G,C,F,E). % 2.23/2.51 ** KEPT (pick-wt=20): 10 [] aux4(A,B,C,D,pair23(E,F))=aux3(A,B,C,E,F,apply(A,pair22(B,E))). % 2.23/2.51 ** KEPT (pick-wt=7): 11 [] aux5(A,B,left(C))=C. % 2.23/2.51 ---> New Demodulator: 12 [new_demod,11] aux5(A,B,left(C))=C. % 2.23/2.51 ** KEPT (pick-wt=9): 13 [] aux5(A,B,right(C))=steps(A,C). % 2.23/2.51 ** KEPT (pick-wt=5): 14 [] aux6(A,nil2)=bfalse. % 2.23/2.51 ---> New Demodulator: 15 [new_demod,14] aux6(A,nil2)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=7): 16 [] aux6(A,cons2(a2,nil2))=bfalse. % 2.23/2.51 ---> New Demodulator: 17 [new_demod,16] aux6(A,cons2(a2,nil2))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=9): 18 [] aux6(A,cons2(a2,cons2(a2,nil2)))=bfalse. % 2.23/2.51 ---> New Demodulator: 19 [new_demod,18] aux6(A,cons2(a2,cons2(a2,nil2)))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=11): 20 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,nil2))))=bfalse. % 2.23/2.51 ---> New Demodulator: 21 [new_demod,20] aux6(A,cons2(a2,cons2(a2,cons2(a2,nil2))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=13): 22 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2)))))=bfalse. % 2.23/2.51 ---> New Demodulator: 23 [new_demod,22] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2)))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=15): 24 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))=bfalse. % 2.23/2.51 ---> New Demodulator: 25 [new_demod,24] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=17): 26 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2)))))))=btrue. % 2.23/2.51 ---> New Demodulator: 27 [new_demod,26] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2)))))))=btrue. % 2.23/2.51 ** KEPT (pick-wt=19): 28 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(B,C))))))))=bfalse. % 2.23/2.51 ---> New Demodulator: 29 [new_demod,28] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(B,C))))))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=17): 30 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(o,B)))))))=bfalse. % 2.23/2.51 ---> New Demodulator: 31 [new_demod,30] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(o,B)))))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=17): 32 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(a2,B)))))))=bfalse. % 2.23/2.51 ---> New Demodulator: 33 [new_demod,32] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(a2,B)))))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=15): 34 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(o,B))))))=bfalse. % 2.23/2.51 ---> New Demodulator: 35 [new_demod,34] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(o,B))))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=15): 36 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(a2,B))))))=bfalse. % 2.23/2.51 ---> New Demodulator: 37 [new_demod,36] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(a2,B))))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=13): 38 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(o,B)))))=bfalse. % 2.23/2.51 ---> New Demodulator: 39 [new_demod,38] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(o,B)))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=13): 40 [] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(b,B)))))=bfalse. % 2.23/2.51 ---> New Demodulator: 41 [new_demod,40] aux6(A,cons2(a2,cons2(a2,cons2(a2,cons2(b,B)))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=11): 42 [] aux6(A,cons2(a2,cons2(a2,cons2(o,B))))=bfalse. % 2.23/2.51 ---> New Demodulator: 43 [new_demod,42] aux6(A,cons2(a2,cons2(a2,cons2(o,B))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=11): 44 [] aux6(A,cons2(a2,cons2(a2,cons2(b,B))))=bfalse. % 2.23/2.51 ---> New Demodulator: 45 [new_demod,44] aux6(A,cons2(a2,cons2(a2,cons2(b,B))))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=9): 46 [] aux6(A,cons2(a2,cons2(o,B)))=bfalse. % 2.23/2.51 ---> New Demodulator: 47 [new_demod,46] aux6(A,cons2(a2,cons2(o,B)))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=9): 48 [] aux6(A,cons2(a2,cons2(b,B)))=bfalse. % 2.23/2.51 ---> New Demodulator: 49 [new_demod,48] aux6(A,cons2(a2,cons2(b,B)))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=7): 50 [] aux6(A,cons2(o,B))=bfalse. % 2.23/2.51 ---> New Demodulator: 51 [new_demod,50] aux6(A,cons2(o,B))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=7): 52 [] aux6(A,cons2(b,B))=bfalse. % 2.23/2.51 ---> New Demodulator: 53 [new_demod,52] aux6(A,cons2(b,B))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 54 [] aux7(A,nil2)=bfalse. % 2.23/2.51 ---> New Demodulator: 55 [new_demod,54] aux7(A,nil2)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=23): 57 [copy,56,flip.1] aux6(A,runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))))=aux7(A,cons2(a2,nil2)). % 2.23/2.51 ---> New Demodulator: 58 [new_demod,57] aux6(A,runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2))))))))=aux7(A,cons2(a2,nil2)). % 2.23/2.51 ** KEPT (pick-wt=9): 59 [] aux7(A,cons2(a2,cons2(B,C)))=bfalse. % 2.23/2.51 ---> New Demodulator: 60 [new_demod,59] aux7(A,cons2(a2,cons2(B,C)))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=7): 61 [] aux7(A,cons2(o,B))=bfalse. % 2.23/2.51 ---> New Demodulator: 62 [new_demod,61] aux7(A,cons2(o,B))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=7): 63 [] aux7(A,cons2(b,B))=bfalse. % 2.23/2.51 ---> New Demodulator: 64 [new_demod,63] aux7(A,cons2(b,B))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=6): 65 [] split(nil2)=pair23(o,nil2). % 2.23/2.51 ---> New Demodulator: 66 [new_demod,65] split(nil2)=pair23(o,nil2). % 2.23/2.51 ** KEPT (pick-wt=8): 67 [] split(cons2(A,B))=pair23(A,B). % 2.23/2.51 ---> New Demodulator: 68 [new_demod,67] split(cons2(A,B))=pair23(A,B). % 2.23/2.51 ** KEPT (pick-wt=5): 69 [] rev(nil2,A)=A. % 2.23/2.51 ---> New Demodulator: 70 [new_demod,69] rev(nil2,A)=A. % 2.23/2.51 ** KEPT (pick-wt=7): 71 [] rev(cons2(o,A),B)=B. % 2.23/2.51 ---> New Demodulator: 72 [new_demod,71] rev(cons2(o,A),B)=B. % 2.23/2.51 ** KEPT (pick-wt=11): 73 [] rev(cons2(a2,A),B)=rev(A,cons2(a2,B)). % 2.23/2.51 ---> New Demodulator: 74 [new_demod,73] rev(cons2(a2,A),B)=rev(A,cons2(a2,B)). % 2.23/2.51 ** KEPT (pick-wt=11): 75 [] rev(cons2(b,A),B)=rev(A,cons2(b,B)). % 2.23/2.51 ---> New Demodulator: 76 [new_demod,75] rev(cons2(b,A),B)=rev(A,cons2(b,B)). % 2.23/2.51 ** KEPT (pick-wt=4): 78 [copy,77,flip.1] succ(zero)=one. % 2.23/2.51 ---> New Demodulator: 79 [new_demod,78] succ(zero)=one. % 2.23/2.51 ** KEPT (pick-wt=4): 81 [copy,80,flip.1] succ(one)=two. % 2.23/2.51 ---> New Demodulator: 82 [new_demod,81] succ(one)=two. % 2.23/2.51 ** KEPT (pick-wt=7): 83 [] apply(nil,A)=pair24(o,stp). % 2.23/2.51 ** KEPT (pick-wt=16): 84 [] apply(cons(pair2(A,B),C),D)=aux(D,C,A,B,e_q(A,D)). % 2.23/2.51 ** KEPT (pick-wt=14): 85 [] act(lft(A),B,C,D)=aux2(B,C,D,A,split(B)). % 2.23/2.51 ** KEPT (pick-wt=14): 87 [copy,86,flip.1] right(tuple2(A,cons2(B,C),D))=act(rgt(A),C,B,D). % 2.23/2.51 ---> New Demodulator: 88 [new_demod,87] right(tuple2(A,cons2(B,C),D))=act(rgt(A),C,B,D). % 2.23/2.51 ** KEPT (pick-wt=12): 90 [copy,89,flip.1] left(rev(A,cons2(B,C)))=act(stp,A,B,C). % 2.23/2.51 ---> New Demodulator: 91 [new_demod,90] left(rev(A,cons2(B,C)))=act(stp,A,B,C). % 2.23/2.51 ** KEPT (pick-wt=14): 92 [] step(A,tuple2(B,C,D))=aux4(A,B,C,D,split(D)). % 2.23/2.51 ** KEPT (pick-wt=10): 93 [] steps(A,B)=aux5(A,B,step(A,B)). % 2.23/2.51 ---> New Demodulator: 94 [new_demod,93] steps(A,B)=aux5(A,B,step(A,B)). % 2.23/2.51 ** KEPT (pick-wt=16): 96 [copy,95,demod,94,flip.1] aux5(A,tuple2(zero,nil2,B),step(A,tuple2(zero,nil2,B)))=runt(A,B). % 2.23/2.51 ---> New Demodulator: 97 [new_demod,96] aux5(A,tuple2(zero,nil2,B),step(A,tuple2(zero,nil2,B)))=runt(A,B). % 2.23/2.51 ** KEPT (pick-wt=10): 98 [] prog0(A)=aux7(A,runt(A,cons2(a2,nil2))). % 2.23/2.51 ---> New Demodulator: 99 [new_demod,98] prog0(A)=aux7(A,runt(A,cons2(a2,nil2))). % 2.23/2.51 ** KEPT (pick-wt=76): 101 [copy,100,demod,99,flip.1] e_q3(aux7(cons(pair2(pair22(zero,a2),A),cons(pair2(pair22(zero,b),B),cons(pair2(pair22(one,a2),C),cons(pair2(pair22(one,b),D),cons(pair2(pair22(two,a2),E),nil))))),runt(cons(pair2(pair22(zero,a2),A),cons(pair2(pair22(zero,b),B),cons(pair2(pair22(one,a2),C),cons(pair2(pair22(one,b),D),cons(pair2(pair22(two,a2),E),nil))))),cons2(a2,nil2))),bfalse)=prop_help(A,B,C,D,E). % 2.23/2.51 ---> New Demodulator: 102 [new_demod,101] e_q3(aux7(cons(pair2(pair22(zero,a2),A),cons(pair2(pair22(zero,b),B),cons(pair2(pair22(one,a2),C),cons(pair2(pair22(one,b),D),cons(pair2(pair22(two,a2),E),nil))))),runt(cons(pair2(pair22(zero,a2),A),cons(pair2(pair22(zero,b),B),cons(pair2(pair22(one,a2),C),cons(pair2(pair22(one,b),D),cons(pair2(pair22(two,a2),E),nil))))),cons2(a2,nil2))),bfalse)=prop_help(A,B,C,D,E). % 2.23/2.51 ** KEPT (pick-wt=5): 103 [] e_q3(bfalse,btrue)=bfalse. % 2.23/2.51 ---> New Demodulator: 104 [new_demod,103] e_q3(bfalse,btrue)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 105 [] e_q3(btrue,bfalse)=bfalse. % 2.23/2.51 ---> New Demodulator: 106 [new_demod,105] e_q3(btrue,bfalse)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 107 [] e_q5(o,a2)=bfalse. % 2.23/2.51 ---> New Demodulator: 108 [new_demod,107] e_q5(o,a2)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 109 [] e_q5(o,b)=bfalse. % 2.23/2.51 ---> New Demodulator: 110 [new_demod,109] e_q5(o,b)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 111 [] e_q5(a2,o)=bfalse. % 2.23/2.51 ---> New Demodulator: 112 [new_demod,111] e_q5(a2,o)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 113 [] e_q5(a2,b)=bfalse. % 2.23/2.51 ---> New Demodulator: 114 [new_demod,113] e_q5(a2,b)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 115 [] e_q5(b,o)=bfalse. % 2.23/2.51 ---> New Demodulator: 116 [new_demod,115] e_q5(b,o)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 117 [] e_q5(b,a2)=bfalse. % 2.23/2.51 ---> New Demodulator: 118 [new_demod,117] e_q5(b,a2)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=9): 119 [] e_q2(succ(A),succ(B))=e_q2(A,B). % 2.23/2.51 ---> New Demodulator: 120 [new_demod,119] e_q2(succ(A),succ(B))=e_q2(A,B). % 2.23/2.51 ** KEPT (pick-wt=6): 121 [] e_q2(zero,succ(A))=bfalse. % 2.23/2.51 ---> New Demodulator: 122 [new_demod,121] e_q2(zero,succ(A))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=6): 123 [] e_q2(succ(A),zero)=bfalse. % 2.23/2.51 ---> New Demodulator: 124 [new_demod,123] e_q2(succ(A),zero)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=9): 125 [] e_q4(lft(A),lft(B))=e_q2(A,B). % 2.23/2.51 ---> New Demodulator: 126 [new_demod,125] e_q4(lft(A),lft(B))=e_q2(A,B). % 2.23/2.51 ** KEPT (pick-wt=9): 127 [] e_q4(rgt(A),rgt(B))=e_q2(A,B). % 2.23/2.51 ---> New Demodulator: 128 [new_demod,127] e_q4(rgt(A),rgt(B))=e_q2(A,B). % 2.23/2.51 ** KEPT (pick-wt=7): 129 [] e_q4(lft(A),rgt(B))=bfalse. % 2.23/2.51 ---> New Demodulator: 130 [new_demod,129] e_q4(lft(A),rgt(B))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=6): 131 [] e_q4(lft(A),stp)=bfalse. % 2.23/2.51 ---> New Demodulator: 132 [new_demod,131] e_q4(lft(A),stp)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=7): 133 [] e_q4(rgt(A),lft(B))=bfalse. % 2.23/2.51 ---> New Demodulator: 134 [new_demod,133] e_q4(rgt(A),lft(B))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=6): 135 [] e_q4(rgt(A),stp)=bfalse. % 2.23/2.51 ---> New Demodulator: 136 [new_demod,135] e_q4(rgt(A),stp)=bfalse. % 2.23/2.51 ** KEPT (pick-wt=6): 137 [] e_q4(stp,lft(A))=bfalse. % 2.23/2.51 ---> New Demodulator: 138 [new_demod,137] e_q4(stp,lft(A))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=6): 139 [] e_q4(stp,rgt(A))=bfalse. % 2.23/2.51 ---> New Demodulator: 140 [new_demod,139] e_q4(stp,rgt(A))=bfalse. % 2.23/2.51 ** KEPT (pick-wt=5): 141 [] e_q(A,A)=btrue. % 2.23/2.51 ---> New Demodulator: 142 [new_demod,141] e_q(A,A)=btrue. % 2.23/2.51 ** KEPT (pick-wt=5): 143 [] e_q2(A,A)=btrue. % 2.23/2.51 ---> New Demodulator: 144 [new_demod,143] e_q2(A,A)=btrue. % 2.23/2.51 ** KEPT (pick-wt=5): 145 [] e_q3(A,A)=btrue. % 2.23/2.51 ---> New Demodulator: 146 [new_demod,145] e_q3(A,A)=btrue. % 2.23/2.51 ** KEPT (pick-wt=5): 147 [] e_q4(A,A)=btrue. % 2.23/2.51 ---> New Demodulator: 148 [new_demod,147] e_q4(A,A)=btrue. % 2.23/2.51 ** KEPT (pick-wt=5): 149 [] e_q5(A,A)=btrue. % 2.23/2.51 ---> New Demodulator: 150 [new_demod,149] e_q5(A,A)=btrue. % 2.23/2.51 Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] A=A. % 2.23/2.51 >>>> Starting back demodulation with 6. % 2.23/2.51 ** KEPT (pick-wt=10): 151 [copy,7,flip.1] apply(A,B)=aux(B,A,C,D,bfalse). % 2.23/2.51 ** KEPT (pick-wt=18): 152 [copy,8,flip.1] right(tuple2(A,B,cons2(C,cons2(D,E))))=aux2(F,D,E,A,pair23(C,B)). % 2.23/2.51 ** KEPT (pick-wt=15): 153 [copy,9,flip.1] act(A,B,C,D)=aux3(E,F,B,G,D,pair24(C,A)). % 2.23/2.51 ** KEPT (pick-wt=20): 154 [copy,10,flip.1] aux3(A,B,C,D,E,apply(A,pair22(B,D)))=aux4(A,B,C,F,pair23(D,E)). % 2.23/2.51 >>>> Starting back demodulation with 12. % 2.23/2.51 ** KEPT (pick-wt=12): 155 [copy,13,flip.1,demod,94] aux5(A,B,step(A,B))=aux5(A,C,right(B)). % 2.23/2.51 >>>> Starting back demodulation with 15. % 2.23/2.51 >>>> Starting back demodulation with 17. % 2.23/2.51 >>>> Starting back demodulation with 19. % 2.23/2.51 >>>> Starting back demodulation with 21. % 2.23/2.51 >>>> Starting back demodulation with 23. % 2.23/2.51 >>>> Starting back demodulation with 25. % 2.23/2.51 >>>> Starting back demodulation with 27. % 2.23/2.51 >>>> Starting back demodulation with 29. % 2.23/2.51 >>>> Starting back demodulation with 31. % 2.23/2.51 >>>> Starting back demodulation with 33. % 2.23/2.51 >>>> Starting back demodulation with 35. % 2.23/2.51 >>>> Starting back demodulation with 37. % 2.23/2.51 >>>> Starting back demodulation with 39. % 2.23/2.51 >>>> Starting back demodulation with 41. % 2.23/2.51 >>>> Starting back demodulation with 43. % 2.23/2.51 >>>> Starting back demodulation with 45. % 2.23/2.51 >>>> Starting back demodulation with 47. % 2.23/2.51 >>>> Starting back demodulation with 49. % 2.23/2.51 >>>> Starting back demodulation with 51. % 2.23/2.51 >>>> Starting back demodulation with 53. % 2.23/2.51 >>>> Starting back demodulation with 55. % 2.23/2.51 >>>> Starting back demodulation with 58. % 2.23/2.51 >>>> Starting back demodulation with 60. % 2.23/2.51 >>>> Starting back demodulation with 62. % 2.23/2.51 >>>> Starting back demodulation with 64. % 2.23/2.51 >>>> Starting back demodulation with 66. % 2.23/2.51 >>>> Starting back demodulation with 68. % 2.23/2.51 >>>> Starting back demodulation with 70. % 2.23/2.51 >>>> Starting back demodulation with 72. % 2.23/2.51 >>>> Starting back demodulation with 74. % 2.23/2.51 >>>> Starting back demodulation with 76. % 2.23/2.51 >>>> Starting back demodulation with 79. % 2.23/2.51 >>>> Starting back demodulation with 82. % 2.23/2.51 ** KEPT (pick-wt=7): 156 [copy,83,flip.1] pair24(o,stp)=apply(nil,A). % 2.23/2.51 ** KEPT (pick-wt=16): 157 [copy,84,flip.1] aux(A,B,C,D,e_q(C,A))=apply(cons(pair2(C,D),B),A). % 2.23/2.51 ** KEPT (pick-wt=14): 158 [copy,85,flip.1] aux2(A,B,C,D,split(A))=act(lft(D),A,B,C). % 2.23/2.51 >>>> Starting back demodulation with 88. % 2.23/2.51 >>>> Starting back demodulation with 91. % 2.23/2.51 ** KEPT (pick-wt=14): 159 [copy,92,flip.1] aux4(A,B,C,D,split(D))=step(A,tuple2(B,C,D)). % 2.23/2.51 >>>> Starting back demodulation with 94. % 2.23/2.51 >> back demodulating 13 with 94. % 2.23/2.51 >>>> Starting back demodulation with 97. % 2.23/2.51 >>>> Starting back demodulation with 99. % 2.23/2.51 >>>> Starting back demodulation with 102. % 2.23/2.51 >>>> Starting back demodulation with 104. % 2.23/2.51 >>>> Starting back demodulation with 106. % 2.23/2.51 >>>> Starting back demodulation with 108. % 2.23/2.51 >>>> Starting back demodulation with 110. % 2.23/2.51 >>>> Starting back demodulation with 112. % 2.23/2.51 >>>> Starting back demodulation with 114. % 2.23/2.51 >>>> Starting back demodulation with 116. % 2.23/2.51 >>>> Starting back demodulation with 118. % 2.23/2.51 >>>> Starting back demodulation with 120. % 2.23/2.51 >>>> Starting back demodulation with 122. % 2.23/2.51 >>>> Starting back demodulation with 124. % 2.23/2.51 >>>> Starting back demodulation with 126. % 2.23/2.51 >>>> Starting back demodulation with 128. % 2.23/2.51 >>>> Starting back demodulation with 130. % 2.23/2.51 >>>> Starting back demodulation with 132. % 2.23/2.51 >>>> Starting back demodulation with 134. % 2.23/2.51 >>>> Starting back demodulation with 136. % 2.23/2.51 >>>> Starting back demodulation with 138. % 2.23/2.51 >>>> Starting back demodulation with 140. % 2.23/2.51 >>>> Starting back demodulation with 142. % 2.23/2.51 >>>> Starting back demodulation with 144. % 2.23/2.51 >>>> Starting back demodulation with 146. % 2.23/2.51 >>>> Starting back demodulation with 148. % 2.23/2.51 >>>> Starting back demodulation with 150. % 2.23/2.51 Following clause subsumed by 7 during input processing: 0 [copy,151,flip.1] aux(A,B,C,D,bfalse)=apply(B,A). % 2.23/2.51 Following clause subsumed by 8 during input processing: 0 [copy,152,flip.1] aux2(A,B,C,D,pair23(E,F))=right(tuple2(D,F,cons2(E,cons2(B,C)))). % 2.23/2.51 Following clause subsumed by 9 during input processing: 0 [copy,153,flip.1] aux3(A,B,C,D,E,pair24(F,G))=act(G,C,F,E). % 2.23/2.51 Following clause subsumed by 10 during input processing: 0 [copy,154,flip.1] aux4(A,B,C,D,pair23(E,F))=aux3(A,B,C,E,F,apply(A,pair22(B,E))). % 2.23/2.51 Following clause subsumed by 160 during input processing: 0 [copy,155,flip.1] aux5(A,B,right(C))=aux5(A,C,step(A,C)). % 2.23/2.51 Following clause subsumed by 83 during input processing: 0 [copy,156,flip.1] apply(nil,A)=pair24(o,stp). % 2.23/2.51 Following clause subsumed by 84 during input processing: 0 [copy,157,flip.1] apply(cons(pair2(A,B),C),D)=aux(D,C,A,B,e_q(A,D)). % 2.23/2.51 Following clause subsumed by 85 during input processing: 0 [copy,158,flip.1] act(lft(A),B,C,D)=aux2(B,C,D,A,split(B)). % 2.23/2.51 Following clause subsumed by 92 during input processing: 0 [copy,159,flip.1] step(A,tuple2(B,C,D))=aux4(A,B,C,D,split(D)). % 2.23/2.54 Following clause subsumed by 155 during input processing: 0 [copy,160,flip.1] aux5(A,B,step(A,B))=aux5(A,C,right(B)). % 2.23/2.54 % 2.23/2.54 ======= end of input processing ======= % 2.23/2.54 % 2.23/2.54 =========== start of search =========== % 2.23/2.54 % 2.23/2.54 % 2.23/2.54 Resetting weight limit to 13. % 2.23/2.54 % 2.23/2.54 % 2.23/2.54 Resetting weight limit to 13. % 2.23/2.54 % 2.23/2.54 sos_size=123 % 2.23/2.54 % 2.23/2.54 Search stopped because sos empty. % 2.23/2.54 % 2.23/2.54 % 2.23/2.54 Search stopped because sos empty. % 2.23/2.54 % 2.23/2.54 ============ end of search ============ % 2.23/2.54 % 2.23/2.54 -------------- statistics ------------- % 2.23/2.54 clauses given 244 % 2.23/2.54 clauses generated 2047 % 2.23/2.54 clauses kept 249 % 2.23/2.54 clauses forward subsumed 1065 % 2.23/2.54 clauses back subsumed 0 % 2.23/2.54 Kbytes malloced 8789 % 2.23/2.54 % 2.23/2.54 ----------- times (seconds) ----------- % 2.23/2.54 user CPU time 0.02 (0 hr, 0 min, 0 sec) % 2.23/2.54 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.23/2.54 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.23/2.54 % 2.23/2.54 Process 25200 finished Tue May 5 12:19:30 2026 % 2.23/2.54 Otter interrupted % 2.23/2.54 PROOF NOT FOUND %------------------------------------------------------------------------------