%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX237-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n016.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:29 PM UTC 2026 % Result : Unknown 2.23s 2.48s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX237-1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n016.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue May 5 13:15:36 EDT 2026 % 0.13/0.34 % CPUTime : % 2.18/2.37 ----- Otter 3.3f, August 2004 ----- % 2.18/2.37 The process was started by sandbox on n016.cluster.edu, % 2.18/2.37 Tue May 5 13:15:36 2026 % 2.18/2.37 The command was "./otter". The process ID is 4548. % 2.18/2.37 % 2.18/2.37 set(prolog_style_variables). % 2.18/2.37 set(auto). % 2.18/2.37 dependent: set(auto1). % 2.18/2.37 dependent: set(process_input). % 2.18/2.37 dependent: clear(print_kept). % 2.18/2.37 dependent: clear(print_new_demod). % 2.18/2.37 dependent: clear(print_back_demod). % 2.18/2.37 dependent: clear(print_back_sub). % 2.18/2.37 dependent: set(control_memory). % 2.18/2.37 dependent: assign(max_mem, 12000). % 2.18/2.37 dependent: assign(pick_given_ratio, 4). % 2.18/2.37 dependent: assign(stats_level, 1). % 2.18/2.37 dependent: assign(max_seconds, 10800). % 2.18/2.37 clear(print_given). % 2.18/2.37 % 2.18/2.37 list(usable). % 2.18/2.37 0 [] A=A. % 2.18/2.37 0 [] aux(Y,B,btrue)=eps. % 2.18/2.37 0 [] aux(Y,B,bfalse)=nil4. % 2.18/2.37 0 [] aux2(Y,R,Q2,btrue)=x(y(step(R,Y),Q2),step(Q2,Y)). % 2.18/2.37 0 [] aux2(Y,R,Q2,bfalse)=x(y(step(R,Y),Q2),nil4). % 2.18/2.37 0 [] aux3(P2,X6,X7,btrue)=rec(y(P2,star(P2)),cons2(X6,X7)). % 2.18/2.37 0 [] aux3(P2,X6,X7,bfalse)=bfalse. % 2.18/2.37 0 [] z(nil4,Y)=nil4. % 2.18/2.37 0 [] z(eps,Y)=Y. % 2.18/2.37 0 [] z(atom(X),nil4)=nil4. % 2.18/2.37 0 [] z(atom(X),eps)=atom(X). % 2.18/2.37 0 [] z(atom(X),atom(X2))=y(atom(X),atom(X2)). % 2.18/2.37 0 [] z(atom(X),x(X2,X3))=y(atom(X),x(X2,X3)). % 2.18/2.37 0 [] z(atom(X),y(X2,X3))=y(atom(X),y(X2,X3)). % 2.18/2.37 0 [] z(atom(X),star(X2))=y(atom(X),star(X2)). % 2.18/2.37 0 [] z(x(X,X2),nil4)=nil4. % 2.18/2.37 0 [] z(x(X,X2),eps)=x(X,X2). % 2.18/2.37 0 [] z(x(X,X2),atom(X3))=y(x(X,X2),atom(X3)). % 2.18/2.37 0 [] z(x(X,X2),x(X3,X4))=y(x(X,X2),x(X3,X4)). % 2.18/2.37 0 [] z(x(X,X2),y(X3,X4))=y(x(X,X2),y(X3,X4)). % 2.18/2.37 0 [] z(x(X,X2),star(X3))=y(x(X,X2),star(X3)). % 2.18/2.37 0 [] z(y(X,X2),nil4)=nil4. % 2.18/2.37 0 [] z(y(X,X2),eps)=y(X,X2). % 2.18/2.37 0 [] z(y(X,X2),atom(X3))=y(y(X,X2),atom(X3)). % 2.18/2.37 0 [] z(y(X,X2),x(X3,X4))=y(y(X,X2),x(X3,X4)). % 2.18/2.37 0 [] z(y(X,X2),y(X3,X4))=y(y(X,X2),y(X3,X4)). % 2.18/2.37 0 [] z(y(X,X2),star(X3))=y(y(X,X2),star(X3)). % 2.18/2.37 0 [] z(star(X),nil4)=nil4. % 2.18/2.37 0 [] z(star(X),eps)=star(X). % 2.18/2.37 0 [] z(star(X),atom(X2))=y(star(X),atom(X2)). % 2.18/2.37 0 [] z(star(X),x(X2,X3))=y(star(X),x(X2,X3)). % 2.18/2.37 0 [] z(star(X),y(X2,X3))=y(star(X),y(X2,X3)). % 2.18/2.37 0 [] z(star(X),star(X2))=y(star(X),star(X2)). % 2.18/2.37 0 [] x2(nil4,Y)=Y. % 2.18/2.37 0 [] x2(eps,nil4)=eps. % 2.18/2.37 0 [] x2(eps,eps)=x(eps,eps). % 2.18/2.37 0 [] x2(eps,atom(X))=x(eps,atom(X)). % 2.18/2.37 0 [] x2(eps,x(X,X2))=x(eps,x(X,X2)). % 2.18/2.37 0 [] x2(eps,y(X,X2))=x(eps,y(X,X2)). % 2.18/2.37 0 [] x2(eps,star(X))=x(eps,star(X)). % 2.18/2.37 0 [] x2(atom(X),nil4)=atom(X). % 2.18/2.37 0 [] x2(atom(X),eps)=x(atom(X),eps). % 2.18/2.37 0 [] x2(atom(X),atom(X2))=x(atom(X),atom(X2)). % 2.18/2.37 0 [] x2(atom(X),x(X2,X3))=x(atom(X),x(X2,X3)). % 2.18/2.37 0 [] x2(atom(X),y(X2,X3))=x(atom(X),y(X2,X3)). % 2.18/2.37 0 [] x2(atom(X),star(X2))=x(atom(X),star(X2)). % 2.18/2.37 0 [] x2(x(X,X2),nil4)=x(X,X2). % 2.18/2.37 0 [] x2(x(X,X2),eps)=x(x(X,X2),eps). % 2.18/2.37 0 [] x2(x(X,X2),atom(X3))=x(x(X,X2),atom(X3)). % 2.18/2.37 0 [] x2(x(X,X2),x(X3,X4))=x(x(X,X2),x(X3,X4)). % 2.18/2.37 0 [] x2(x(X,X2),y(X3,X4))=x(x(X,X2),y(X3,X4)). % 2.18/2.37 0 [] x2(x(X,X2),star(X3))=x(x(X,X2),star(X3)). % 2.18/2.37 0 [] x2(y(X,X2),nil4)=y(X,X2). % 2.18/2.37 0 [] x2(y(X,X2),eps)=x(y(X,X2),eps). % 2.18/2.37 0 [] x2(y(X,X2),atom(X3))=x(y(X,X2),atom(X3)). % 2.18/2.37 0 [] x2(y(X,X2),x(X3,X4))=x(y(X,X2),x(X3,X4)). % 2.18/2.37 0 [] x2(y(X,X2),y(X3,X4))=x(y(X,X2),y(X3,X4)). % 2.18/2.37 0 [] x2(y(X,X2),star(X3))=x(y(X,X2),star(X3)). % 2.18/2.37 0 [] x2(star(X),nil4)=star(X). % 2.18/2.37 0 [] x2(star(X),eps)=x(star(X),eps). % 2.18/2.37 0 [] x2(star(X),atom(X2))=x(star(X),atom(X2)). % 2.18/2.37 0 [] x2(star(X),x(X2,X3))=x(star(X),x(X2,X3)). % 2.18/2.37 0 [] x2(star(X),y(X2,X3))=x(star(X),y(X2,X3)). % 2.18/2.37 0 [] x2(star(X),star(X2))=x(star(X),star(X2)). % 2.18/2.37 0 [] splits(X,nil)=nil. % 2.18/2.37 0 [] splits(X,cons(pair2(Bs,Cs),X2))=cons(pair2(cons2(X,Bs),Cs),splits(X,X2)). % 2.18/2.37 0 [] splits2(nil2)=cons(pair2(nil2,nil2),nil). % 2.18/2.37 0 [] splits2(cons2(Y,Xs))=cons(pair2(nil2,cons2(Y,Xs)),splits(Y,splits2(Xs))). % 2.18/2.37 0 [] orb(btrue,Q)=btrue. % 2.18/2.37 0 [] orb(bfalse,Q)=Q. % 2.18/2.37 0 [] or2(nil3)=bfalse. % 2.18/2.37 0 [] or2(cons3(Y,Xs))=orb(Y,or2(Xs)). % 2.18/2.37 0 [] notb(btrue)=bfalse. % 2.18/2.37 0 [] notb(bfalse)=btrue. % 2.18/2.37 0 [] andb(btrue,Q)=Q. % 2.18/2.37 0 [] andb(bfalse,Q)=bfalse. % 2.18/2.37 0 [] eps2(eps)=btrue. % 2.18/2.37 0 [] eps2(x(P,Q))=orb(eps2(P),eps2(Q)). % 2.18/2.37 0 [] eps2(y(R,Q2))=andb(eps2(R),eps2(Q2)). % 2.18/2.37 0 [] eps2(star(Y))=btrue. % 2.18/2.37 0 [] eps2(nil4)=bfalse. % 2.18/2.37 0 [] eps2(atom(X))=bfalse. % 2.18/2.37 0 [] step(atom(B),Y)=aux(Y,B,e_q(B,Y)). % 2.18/2.37 0 [] step(x(P,Q),Y)=x(step(P,Y),step(Q,Y)). % 2.18/2.37 0 [] step(y(R,Q2),Y)=aux2(Y,R,Q2,eps2(R)). % 2.18/2.37 0 [] step(star(P2),Y)=y(step(P2,Y),star(P2)). % 2.18/2.37 0 [] step(nil4,Y)=nil4. % 2.18/2.37 0 [] step(eps,Y)=nil4. % 2.18/2.37 0 [] rec(X,nil2)=eps2(X). % 2.18/2.37 0 [] rec(X,cons2(Z,Xs))=rec(step(X,Z),Xs). % 2.18/2.37 0 [] reck(P,Q,nil)=nil3. % 2.18/2.37 0 [] reck(P,Q,cons(pair2(L,R),Z))=cons3(andb(reck2(P,L),rec(Q,R)),reck(P,Q,Z)). % 2.18/2.37 0 [] reck2(nil4,Y)=bfalse. % 2.18/2.37 0 [] reck2(eps,nil2)=btrue. % 2.18/2.37 0 [] reck2(eps,cons2(Z,X2))=bfalse. % 2.18/2.37 0 [] reck2(atom(C),nil2)=bfalse. % 2.18/2.37 0 [] reck2(atom(C),cons2(B2,nil2))=e_q(C,B2). % 2.18/2.37 0 [] reck2(atom(C),cons2(B2,cons2(X4,X5)))=bfalse. % 2.18/2.37 0 [] reck2(x(P,Q),Y)=orb(reck2(P,Y),reck2(Q,Y)). % 2.18/2.37 0 [] reck2(y(R,Q2),Y)=or2(reck(R,Q2,splits2(Y))). % 2.18/2.37 0 [] reck2(star(P2),nil2)=btrue. % 2.18/2.37 0 [] reck2(star(P2),cons2(X6,X7))=aux3(P2,X6,X7,notb(eps2(P2))). % 2.18/2.37 0 [] prop_kfind4(X)=notb(reck2(X,cons2(a,cons2(b,cons2(b,cons2(a,nil2)))))). % 2.18/2.37 0 [] e_q(a,b)=bfalse. % 2.18/2.37 0 [] e_q(a,c)=bfalse. % 2.18/2.37 0 [] e_q(b,a)=bfalse. % 2.18/2.37 0 [] e_q(b,c)=bfalse. % 2.18/2.37 0 [] e_q(c,a)=bfalse. % 2.18/2.37 0 [] e_q(c,b)=bfalse. % 2.18/2.37 0 [] e_q2(bfalse,btrue)=bfalse. % 2.18/2.37 0 [] e_q2(btrue,bfalse)=bfalse. % 2.18/2.37 0 [] e_q(X,X)=btrue. % 2.18/2.37 0 [] e_q2(X,X)=btrue. % 2.18/2.37 0 [] e_q2(prop_kfind4(X),bfalse)!=btrue. % 2.18/2.37 end_of_list. % 2.18/2.37 % 2.18/2.37 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. % 2.18/2.37 % 2.18/2.37 All clauses are units, and equality is present; the % 2.18/2.37 strategy will be Knuth-Bendix with positive clauses in sos. % 2.18/2.37 % 2.18/2.37 dependent: set(knuth_bendix). % 2.18/2.37 dependent: set(anl_eq). % 2.18/2.37 dependent: set(para_from). % 2.18/2.37 dependent: set(para_into). % 2.18/2.37 dependent: clear(para_from_right). % 2.18/2.37 dependent: clear(para_into_right). % 2.18/2.37 dependent: set(para_from_vars). % 2.18/2.37 dependent: set(eq_units_both_ways). % 2.18/2.37 dependent: set(dynamic_demod_all). % 2.18/2.37 dependent: set(dynamic_demod). % 2.18/2.37 dependent: set(order_eq). % 2.18/2.37 dependent: set(back_demod). % 2.18/2.37 dependent: set(lrpo). % 2.18/2.37 % 2.18/2.37 ------------> process usable: % 2.18/2.37 ** KEPT (pick-wt=6): 1 [] e_q2(prop_kfind4(A),bfalse)!=btrue. % 2.18/2.37 % 2.18/2.37 ------------> process sos: % 2.18/2.37 ** KEPT (pick-wt=3): 2 [] A=A. % 2.18/2.37 ** KEPT (pick-wt=6): 3 [] aux(A,B,btrue)=eps. % 2.18/2.37 ---> New Demodulator: 4 [new_demod,3] aux(A,B,btrue)=eps. % 2.18/2.37 ** KEPT (pick-wt=6): 5 [] aux(A,B,bfalse)=nil4. % 2.18/2.37 ---> New Demodulator: 6 [new_demod,5] aux(A,B,bfalse)=nil4. % 2.18/2.37 ** KEPT (pick-wt=15): 8 [copy,7,flip.1] x(y(step(A,B),C),step(C,B))=aux2(B,A,C,btrue). % 2.18/2.37 ---> New Demodulator: 9 [new_demod,8] x(y(step(A,B),C),step(C,B))=aux2(B,A,C,btrue). % 2.18/2.37 ** KEPT (pick-wt=13): 11 [copy,10,flip.1] x(y(step(A,B),C),nil4)=aux2(B,A,C,bfalse). % 2.18/2.37 ---> New Demodulator: 12 [new_demod,11] x(y(step(A,B),C),nil4)=aux2(B,A,C,bfalse). % 2.18/2.37 ** KEPT (pick-wt=14): 14 [copy,13,flip.1] rec(y(A,star(A)),cons2(B,C))=aux3(A,B,C,btrue). % 2.18/2.37 ---> New Demodulator: 15 [new_demod,14] rec(y(A,star(A)),cons2(B,C))=aux3(A,B,C,btrue). % 2.18/2.37 ** KEPT (pick-wt=7): 16 [] aux3(A,B,C,bfalse)=bfalse. % 2.18/2.37 ---> New Demodulator: 17 [new_demod,16] aux3(A,B,C,bfalse)=bfalse. % 2.18/2.37 ** KEPT (pick-wt=5): 18 [] z(nil4,A)=nil4. % 2.18/2.37 ---> New Demodulator: 19 [new_demod,18] z(nil4,A)=nil4. % 2.18/2.37 ** KEPT (pick-wt=5): 20 [] z(eps,A)=A. % 2.18/2.37 ---> New Demodulator: 21 [new_demod,20] z(eps,A)=A. % 2.18/2.37 ** KEPT (pick-wt=6): 22 [] z(atom(A),nil4)=nil4. % 2.18/2.37 ---> New Demodulator: 23 [new_demod,22] z(atom(A),nil4)=nil4. % 2.18/2.37 ** KEPT (pick-wt=7): 24 [] z(atom(A),eps)=atom(A). % 2.18/2.37 ---> New Demodulator: 25 [new_demod,24] z(atom(A),eps)=atom(A). % 2.18/2.37 ** KEPT (pick-wt=11): 26 [] z(atom(A),atom(B))=y(atom(A),atom(B)). % 2.18/2.37 ---> New Demodulator: 27 [new_demod,26] z(atom(A),atom(B))=y(atom(A),atom(B)). % 2.18/2.37 ** KEPT (pick-wt=13): 28 [] z(atom(A),x(B,C))=y(atom(A),x(B,C)). % 2.18/2.37 ---> New Demodulator: 29 [new_demod,28] z(atom(A),x(B,C))=y(atom(A),x(B,C)). % 2.18/2.37 ** KEPT (pick-wt=13): 30 [] z(atom(A),y(B,C))=y(atom(A),y(B,C)). % 2.18/2.37 ---> New Demodulator: 31 [new_demod,30] z(atom(A),y(B,C))=y(atom(A),y(B,C)). % 2.18/2.37 ** KEPT (pick-wt=11): 32 [] z(atom(A),star(B))=y(atom(A),star(B)). % 2.18/2.37 ---> New Demodulator: 33 [new_demod,32] z(atom(A),star(B))=y(atom(A),star(B)). % 2.18/2.37 ** KEPT (pick-wt=7): 34 [] z(x(A,B),nil4)=nil4. % 2.18/2.37 ---> New Demodulator: 35 [new_demod,34] z(x(A,B),nil4)=nil4. % 2.18/2.37 ** KEPT (pick-wt=9): 36 [] z(x(A,B),eps)=x(A,B). % 2.18/2.37 ---> New Demodulator: 37 [new_demod,36] z(x(A,B),eps)=x(A,B). % 2.18/2.37 ** KEPT (pick-wt=13): 38 [] z(x(A,B),atom(C))=y(x(A,B),atom(C)). % 2.18/2.37 ---> New Demodulator: 39 [new_demod,38] z(x(A,B),atom(C))=y(x(A,B),atom(C)). % 2.18/2.37 ** KEPT (pick-wt=15): 40 [] z(x(A,B),x(C,D))=y(x(A,B),x(C,D)). % 2.18/2.37 ---> New Demodulator: 41 [new_demod,40] z(x(A,B),x(C,D))=y(x(A,B),x(C,D)). % 2.18/2.37 ** KEPT (pick-wt=15): 42 [] z(x(A,B),y(C,D))=y(x(A,B),y(C,D)). % 2.18/2.37 ---> New Demodulator: 43 [new_demod,42] z(x(A,B),y(C,D))=y(x(A,B),y(C,D)). % 2.18/2.37 ** KEPT (pick-wt=13): 44 [] z(x(A,B),star(C))=y(x(A,B),star(C)). % 2.18/2.37 ---> New Demodulator: 45 [new_demod,44] z(x(A,B),star(C))=y(x(A,B),star(C)). % 2.18/2.37 ** KEPT (pick-wt=7): 46 [] z(y(A,B),nil4)=nil4. % 2.18/2.37 ---> New Demodulator: 47 [new_demod,46] z(y(A,B),nil4)=nil4. % 2.18/2.37 ** KEPT (pick-wt=9): 48 [] z(y(A,B),eps)=y(A,B). % 2.18/2.37 ---> New Demodulator: 49 [new_demod,48] z(y(A,B),eps)=y(A,B). % 2.18/2.37 ** KEPT (pick-wt=13): 50 [] z(y(A,B),atom(C))=y(y(A,B),atom(C)). % 2.18/2.37 ---> New Demodulator: 51 [new_demod,50] z(y(A,B),atom(C))=y(y(A,B),atom(C)). % 2.18/2.37 ** KEPT (pick-wt=15): 52 [] z(y(A,B),x(C,D))=y(y(A,B),x(C,D)). % 2.18/2.37 ---> New Demodulator: 53 [new_demod,52] z(y(A,B),x(C,D))=y(y(A,B),x(C,D)). % 2.18/2.37 ** KEPT (pick-wt=15): 54 [] z(y(A,B),y(C,D))=y(y(A,B),y(C,D)). % 2.18/2.37 ---> New Demodulator: 55 [new_demod,54] z(y(A,B),y(C,D))=y(y(A,B),y(C,D)). % 2.18/2.37 ** KEPT (pick-wt=13): 56 [] z(y(A,B),star(C))=y(y(A,B),star(C)). % 2.18/2.37 ---> New Demodulator: 57 [new_demod,56] z(y(A,B),star(C))=y(y(A,B),star(C)). % 2.18/2.37 ** KEPT (pick-wt=6): 58 [] z(star(A),nil4)=nil4. % 2.18/2.37 ---> New Demodulator: 59 [new_demod,58] z(star(A),nil4)=nil4. % 2.18/2.37 ** KEPT (pick-wt=7): 60 [] z(star(A),eps)=star(A). % 2.18/2.37 ---> New Demodulator: 61 [new_demod,60] z(star(A),eps)=star(A). % 2.18/2.37 ** KEPT (pick-wt=11): 62 [] z(star(A),atom(B))=y(star(A),atom(B)). % 2.18/2.37 ---> New Demodulator: 63 [new_demod,62] z(star(A),atom(B))=y(star(A),atom(B)). % 2.18/2.37 ** KEPT (pick-wt=13): 64 [] z(star(A),x(B,C))=y(star(A),x(B,C)). % 2.18/2.37 ---> New Demodulator: 65 [new_demod,64] z(star(A),x(B,C))=y(star(A),x(B,C)). % 2.18/2.37 ** KEPT (pick-wt=13): 66 [] z(star(A),y(B,C))=y(star(A),y(B,C)). % 2.18/2.37 ---> New Demodulator: 67 [new_demod,66] z(star(A),y(B,C))=y(star(A),y(B,C)). % 2.18/2.37 ** KEPT (pick-wt=11): 68 [] z(star(A),star(B))=y(star(A),star(B)). % 2.18/2.37 ---> New Demodulator: 69 [new_demod,68] z(star(A),star(B))=y(star(A),star(B)). % 2.18/2.37 ** KEPT (pick-wt=5): 70 [] x2(nil4,A)=A. % 2.18/2.37 ---> New Demodulator: 71 [new_demod,70] x2(nil4,A)=A. % 2.18/2.37 ** KEPT (pick-wt=5): 72 [] x2(eps,nil4)=eps. % 2.18/2.37 ---> New Demodulator: 73 [new_demod,72] x2(eps,nil4)=eps. % 2.18/2.37 ** KEPT (pick-wt=7): 74 [] x2(eps,eps)=x(eps,eps). % 2.18/2.37 ---> New Demodulator: 75 [new_demod,74] x2(eps,eps)=x(eps,eps). % 2.18/2.37 ** KEPT (pick-wt=9): 76 [] x2(eps,atom(A))=x(eps,atom(A)). % 2.18/2.37 ---> New Demodulator: 77 [new_demod,76] x2(eps,atom(A))=x(eps,atom(A)). % 2.18/2.37 ** KEPT (pick-wt=11): 78 [] x2(eps,x(A,B))=x(eps,x(A,B)). % 2.18/2.37 ---> New Demodulator: 79 [new_demod,78] x2(eps,x(A,B))=x(eps,x(A,B)). % 2.18/2.37 ** KEPT (pick-wt=11): 80 [] x2(eps,y(A,B))=x(eps,y(A,B)). % 2.18/2.37 ---> New Demodulator: 81 [new_demod,80] x2(eps,y(A,B))=x(eps,y(A,B)). % 2.18/2.37 ** KEPT (pick-wt=9): 82 [] x2(eps,star(A))=x(eps,star(A)). % 2.18/2.37 ---> New Demodulator: 83 [new_demod,82] x2(eps,star(A))=x(eps,star(A)). % 2.18/2.37 ** KEPT (pick-wt=7): 84 [] x2(atom(A),nil4)=atom(A). % 2.18/2.37 ---> New Demodulator: 85 [new_demod,84] x2(atom(A),nil4)=atom(A). % 2.18/2.37 ** KEPT (pick-wt=9): 86 [] x2(atom(A),eps)=x(atom(A),eps). % 2.18/2.37 ---> New Demodulator: 87 [new_demod,86] x2(atom(A),eps)=x(atom(A),eps). % 2.18/2.37 ** KEPT (pick-wt=11): 88 [] x2(atom(A),atom(B))=x(atom(A),atom(B)). % 2.18/2.37 ---> New Demodulator: 89 [new_demod,88] x2(atom(A),atom(B))=x(atom(A),atom(B)). % 2.18/2.37 ** KEPT (pick-wt=13): 90 [] x2(atom(A),x(B,C))=x(atom(A),x(B,C)). % 2.18/2.37 ---> New Demodulator: 91 [new_demod,90] x2(atom(A),x(B,C))=x(atom(A),x(B,C)). % 2.18/2.37 ** KEPT (pick-wt=13): 92 [] x2(atom(A),y(B,C))=x(atom(A),y(B,C)). % 2.18/2.37 ---> New Demodulator: 93 [new_demod,92] x2(atom(A),y(B,C))=x(atom(A),y(B,C)). % 2.18/2.37 ** KEPT (pick-wt=11): 94 [] x2(atom(A),star(B))=x(atom(A),star(B)). % 2.18/2.37 ---> New Demodulator: 95 [new_demod,94] x2(atom(A),star(B))=x(atom(A),star(B)). % 2.18/2.37 ** KEPT (pick-wt=9): 96 [] x2(x(A,B),nil4)=x(A,B). % 2.18/2.37 ---> New Demodulator: 97 [new_demod,96] x2(x(A,B),nil4)=x(A,B). % 2.18/2.37 ** KEPT (pick-wt=11): 98 [] x2(x(A,B),eps)=x(x(A,B),eps). % 2.18/2.37 ---> New Demodulator: 99 [new_demod,98] x2(x(A,B),eps)=x(x(A,B),eps). % 2.18/2.37 ** KEPT (pick-wt=13): 100 [] x2(x(A,B),atom(C))=x(x(A,B),atom(C)). % 2.18/2.37 ---> New Demodulator: 101 [new_demod,100] x2(x(A,B),atom(C))=x(x(A,B),atom(C)). % 2.18/2.37 ** KEPT (pick-wt=15): 102 [] x2(x(A,B),x(C,D))=x(x(A,B),x(C,D)). % 2.18/2.37 ---> New Demodulator: 103 [new_demod,102] x2(x(A,B),x(C,D))=x(x(A,B),x(C,D)). % 2.18/2.37 ** KEPT (pick-wt=15): 104 [] x2(x(A,B),y(C,D))=x(x(A,B),y(C,D)). % 2.18/2.37 ---> New Demodulator: 105 [new_demod,104] x2(x(A,B),y(C,D))=x(x(A,B),y(C,D)). % 2.18/2.37 ** KEPT (pick-wt=13): 106 [] x2(x(A,B),star(C))=x(x(A,B),star(C)). % 2.18/2.37 ---> New Demodulator: 107 [new_demod,106] x2(x(A,B),star(C))=x(x(A,B),star(C)). % 2.18/2.37 ** KEPT (pick-wt=9): 108 [] x2(y(A,B),nil4)=y(A,B). % 2.18/2.37 ---> New Demodulator: 109 [new_demod,108] x2(y(A,B),nil4)=y(A,B). % 2.18/2.37 ** KEPT (pick-wt=11): 110 [] x2(y(A,B),eps)=x(y(A,B),eps). % 2.18/2.37 ---> New Demodulator: 111 [new_demod,110] x2(y(A,B),eps)=x(y(A,B),eps). % 2.18/2.37 ** KEPT (pick-wt=13): 112 [] x2(y(A,B),atom(C))=x(y(A,B),atom(C)). % 2.18/2.37 ---> New Demodulator: 113 [new_demod,112] x2(y(A,B),atom(C))=x(y(A,B),atom(C)). % 2.18/2.37 ** KEPT (pick-wt=15): 114 [] x2(y(A,B),x(C,D))=x(y(A,B),x(C,D)). % 2.18/2.37 ---> New Demodulator: 115 [new_demod,114] x2(y(A,B),x(C,D))=x(y(A,B),x(C,D)). % 2.18/2.37 ** KEPT (pick-wt=15): 116 [] x2(y(A,B),y(C,D))=x(y(A,B),y(C,D)). % 2.18/2.37 ---> New Demodulator: 117 [new_demod,116] x2(y(A,B),y(C,D))=x(y(A,B),y(C,D)). % 2.18/2.37 ** KEPT (pick-wt=13): 118 [] x2(y(A,B),star(C))=x(y(A,B),star(C)). % 2.18/2.37 ---> New Demodulator: 119 [new_demod,118] x2(y(A,B),star(C))=x(y(A,B),star(C)). % 2.18/2.37 ** KEPT (pick-wt=7): 120 [] x2(star(A),nil4)=star(A). % 2.18/2.37 ---> New Demodulator: 121 [new_demod,120] x2(star(A),nil4)=star(A). % 2.18/2.37 ** KEPT (pick-wt=9): 122 [] x2(star(A),eps)=x(star(A),eps). % 2.18/2.37 ---> New Demodulator: 123 [new_demod,122] x2(star(A),eps)=x(star(A),eps). % 2.18/2.37 ** KEPT (pick-wt=11): 124 [] x2(star(A),atom(B))=x(star(A),atom(B)). % 2.18/2.37 ---> New Demodulator: 125 [new_demod,124] x2(star(A),atom(B))=x(star(A),atom(B)). % 2.18/2.37 ** KEPT (pick-wt=13): 126 [] x2(star(A),x(B,C))=x(star(A),x(B,C)). % 2.18/2.37 ---> New Demodulator: 127 [new_demod,126] x2(star(A),x(B,C))=x(star(A),x(B,C)). % 2.18/2.37 ** KEPT (pick-wt=13): 128 [] x2(star(A),y(B,C))=x(star(A),y(B,C)). % 2.18/2.37 ---> New Demodulator: 129 [new_demod,128] x2(star(A),y(B,C))=x(star(A),y(B,C)). % 2.18/2.37 ** KEPT (pick-wt=11): 130 [] x2(star(A),star(B))=x(star(A),star(B)). % 2.18/2.37 ---> New Demodulator: 131 [new_demod,130] x2(star(A),star(B))=x(star(A),star(B)). % 2.18/2.37 ** KEPT (pick-wt=5): 132 [] splits(A,nil)=nil. % 2.18/2.37 ---> New Demodulator: 133 [new_demod,132] splits(A,nil)=nil. % 2.18/2.37 ** KEPT (pick-wt=17): 134 [] splits(A,cons(pair2(B,C),D))=cons(pair2(cons2(A,B),C),splits(A,D)). % 2.18/2.37 ---> New Demodulator: 135 [new_demod,134] splits(A,cons(pair2(B,C),D))=cons(pair2(cons2(A,B),C),splits(A,D)). % 2.18/2.37 ** KEPT (pick-wt=8): 136 [] splits2(nil2)=cons(pair2(nil2,nil2),nil). % 2.18/2.37 ---> New Demodulator: 137 [new_demod,136] splits2(nil2)=cons(pair2(nil2,nil2),nil). % 2.18/2.37 ** KEPT (pick-wt=15): 138 [] splits2(cons2(A,B))=cons(pair2(nil2,cons2(A,B)),splits(A,splits2(B))). % 2.18/2.37 ---> New Demodulator: 139 [new_demod,138] splits2(cons2(A,B))=cons(pair2(nil2,cons2(A,B)),splits(A,splits2(B))). % 2.18/2.37 ** KEPT (pick-wt=5): 140 [] orb(btrue,A)=btrue. % 2.18/2.37 ---> New Demodulator: 141 [new_demod,140] orb(btrue,A)=btrue. % 2.18/2.37 ** KEPT (pick-wt=5): 142 [] orb(bfalse,A)=A. % 2.18/2.37 ---> New Demodulator: 143 [new_demod,142] orb(bfalse,A)=A. % 2.18/2.37 ** KEPT (pick-wt=4): 144 [] or2(nil3)=bfalse. % 2.18/2.37 ---> New Demodulator: 145 [new_demod,144] or2(nil3)=bfalse. % 2.18/2.37 ** KEPT (pick-wt=9): 146 [] or2(cons3(A,B))=orb(A,or2(B)). % 2.18/2.37 ---> New Demodulator: 147 [new_demod,146] or2(cons3(A,B))=orb(A,or2(B)). % 2.18/2.37 ** KEPT (pick-wt=4): 148 [] notb(btrue)=bfalse. % 2.18/2.37 ---> New Demodulator: 149 [new_demod,148] notb(btrue)=bfalse. % 2.18/2.37 ** KEPT (pick-wt=4): 150 [] notb(bfalse)=btrue. % 2.18/2.37 ---> New Demodulator: 151 [new_demod,150] notb(bfalse)=btrue. % 2.18/2.37 ** KEPT (pick-wt=5): 152 [] andb(btrue,A)=A. % 2.18/2.37 ---> New Demodulator: 153 [new_demod,152] andb(btrue,A)=A. % 2.18/2.37 ** KEPT (pick-wt=5): 154 [] andb(bfalse,A)=bfalse. % 2.18/2.37 ---> New Demodulator: 155 [new_demod,154] andb(bfalse,A)=bfalse. % 2.18/2.37 ** KEPT (pick-wt=4): 156 [] eps2(eps)=btrue. % 2.18/2.37 ---> New Demodulator: 157 [new_demod,156] eps2(eps)=btrue. % 2.18/2.37 ** KEPT (pick-wt=10): 158 [] eps2(x(A,B))=orb(eps2(A),eps2(B)). % 2.18/2.37 ---> New Demodulator: 159 [new_demod,158] eps2(x(A,B))=orb(eps2(A),eps2(B)). % 2.18/2.37 ** KEPT (pick-wt=10): 160 [] eps2(y(A,B))=andb(eps2(A),eps2(B)). % 2.18/2.37 ---> New Demodulator: 161 [new_demod,160] eps2(y(A,B))=andb(eps2(A),eps2(B)). % 2.18/2.37 ** KEPT (pick-wt=5): 162 [] eps2(star(A))=btrue. % 2.18/2.37 ---> New Demodulator: 163 [new_demod,162] eps2(star(A))=btrue. % 2.18/2.37 ** KEPT (pick-wt=4): 164 [] eps2(nil4)=bfalse. % 2.18/2.37 ---> New Demodulator: 165 [new_demod,164] eps2(nil4)=bfalse. % 2.18/2.37 ** KEPT (pick-wt=5): 166 [] eps2(atom(A))=bfalse. % 2.18/2.37 ---> New Demodulator: 167 [new_demod,166] eps2(atom(A))=bfalse. % 2.18/2.37 ** KEPT (pick-wt=11): 168 [] step(atom(A),B)=aux(B,A,e_q(A,B)). % 2.18/2.38 ---> New Demodulator: 169 [new_demod,168] step(atom(A),B)=aux(B,A,e_q(A,B)). % 2.18/2.38 ** KEPT (pick-wt=13): 171 [copy,170,flip.1] x(step(A,B),step(C,B))=step(x(A,C),B). % 2.18/2.38 ---> New Demodulator: 172 [new_demod,171] x(step(A,B),step(C,B))=step(x(A,C),B). % 2.18/2.38 ** KEPT (pick-wt=12): 173 [] step(y(A,B),C)=aux2(C,A,B,eps2(A)). % 2.18/2.38 ** KEPT (pick-wt=11): 175 [copy,174,flip.1] y(step(A,B),star(A))=step(star(A),B). % 2.18/2.38 ---> New Demodulator: 176 [new_demod,175] y(step(A,B),star(A))=step(star(A),B). % 2.18/2.38 ** KEPT (pick-wt=5): 177 [] step(nil4,A)=nil4. % 2.18/2.38 ---> New Demodulator: 178 [new_demod,177] step(nil4,A)=nil4. % 2.18/2.38 ** KEPT (pick-wt=5): 179 [] step(eps,A)=nil4. % 2.18/2.38 ---> New Demodulator: 180 [new_demod,179] step(eps,A)=nil4. % 2.18/2.38 ** KEPT (pick-wt=6): 182 [copy,181,flip.1] eps2(A)=rec(A,nil2). % 2.18/2.38 ---> New Demodulator: 183 [new_demod,182] eps2(A)=rec(A,nil2). % 2.18/2.38 ** KEPT (pick-wt=11): 185 [copy,184,flip.1] rec(step(A,B),C)=rec(A,cons2(B,C)). % 2.18/2.38 ---> New Demodulator: 186 [new_demod,185] rec(step(A,B),C)=rec(A,cons2(B,C)). % 2.18/2.38 ** KEPT (pick-wt=6): 187 [] reck(A,B,nil)=nil3. % 2.18/2.38 ---> New Demodulator: 188 [new_demod,187] reck(A,B,nil)=nil3. % 2.18/2.38 ** KEPT (pick-wt=21): 189 [] reck(A,B,cons(pair2(C,D),E))=cons3(andb(reck2(A,C),rec(B,D)),reck(A,B,E)). % 2.18/2.38 ** KEPT (pick-wt=5): 190 [] reck2(nil4,A)=bfalse. % 2.18/2.38 ---> New Demodulator: 191 [new_demod,190] reck2(nil4,A)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 192 [] reck2(eps,nil2)=btrue. % 2.18/2.38 ---> New Demodulator: 193 [new_demod,192] reck2(eps,nil2)=btrue. % 2.18/2.38 ** KEPT (pick-wt=7): 194 [] reck2(eps,cons2(A,B))=bfalse. % 2.18/2.38 ---> New Demodulator: 195 [new_demod,194] reck2(eps,cons2(A,B))=bfalse. % 2.18/2.38 ** KEPT (pick-wt=6): 196 [] reck2(atom(A),nil2)=bfalse. % 2.18/2.38 ---> New Demodulator: 197 [new_demod,196] reck2(atom(A),nil2)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=10): 198 [] reck2(atom(A),cons2(B,nil2))=e_q(A,B). % 2.18/2.38 ---> New Demodulator: 199 [new_demod,198] reck2(atom(A),cons2(B,nil2))=e_q(A,B). % 2.18/2.38 ** KEPT (pick-wt=10): 200 [] reck2(atom(A),cons2(B,cons2(C,D)))=bfalse. % 2.18/2.38 ---> New Demodulator: 201 [new_demod,200] reck2(atom(A),cons2(B,cons2(C,D)))=bfalse. % 2.18/2.38 ** KEPT (pick-wt=13): 202 [] reck2(x(A,B),C)=orb(reck2(A,C),reck2(B,C)). % 2.18/2.38 ---> New Demodulator: 203 [new_demod,202] reck2(x(A,B),C)=orb(reck2(A,C),reck2(B,C)). % 2.18/2.38 ** KEPT (pick-wt=12): 205 [copy,204,flip.1] or2(reck(A,B,splits2(C)))=reck2(y(A,B),C). % 2.18/2.38 ---> New Demodulator: 206 [new_demod,205] or2(reck(A,B,splits2(C)))=reck2(y(A,B),C). % 2.18/2.38 ** KEPT (pick-wt=6): 207 [] reck2(star(A),nil2)=btrue. % 2.18/2.38 ---> New Demodulator: 208 [new_demod,207] reck2(star(A),nil2)=btrue. % 2.18/2.38 ** KEPT (pick-wt=15): 210 [copy,209,demod,183] reck2(star(A),cons2(B,C))=aux3(A,B,C,notb(rec(A,nil2))). % 2.18/2.38 ---> New Demodulator: 211 [new_demod,210] reck2(star(A),cons2(B,C))=aux3(A,B,C,notb(rec(A,nil2))). % 2.18/2.38 ** KEPT (pick-wt=15): 212 [] prop_kfind4(A)=notb(reck2(A,cons2(a,cons2(b,cons2(b,cons2(a,nil2)))))). % 2.18/2.38 ---> New Demodulator: 213 [new_demod,212] prop_kfind4(A)=notb(reck2(A,cons2(a,cons2(b,cons2(b,cons2(a,nil2)))))). % 2.18/2.38 ** KEPT (pick-wt=5): 214 [] e_q(a,b)=bfalse. % 2.18/2.38 ---> New Demodulator: 215 [new_demod,214] e_q(a,b)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 216 [] e_q(a,c)=bfalse. % 2.18/2.38 ---> New Demodulator: 217 [new_demod,216] e_q(a,c)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 218 [] e_q(b,a)=bfalse. % 2.18/2.38 ---> New Demodulator: 219 [new_demod,218] e_q(b,a)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 220 [] e_q(b,c)=bfalse. % 2.18/2.38 ---> New Demodulator: 221 [new_demod,220] e_q(b,c)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 222 [] e_q(c,a)=bfalse. % 2.18/2.38 ---> New Demodulator: 223 [new_demod,222] e_q(c,a)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 224 [] e_q(c,b)=bfalse. % 2.18/2.38 ---> New Demodulator: 225 [new_demod,224] e_q(c,b)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 226 [] e_q2(bfalse,btrue)=bfalse. % 2.18/2.38 ---> New Demodulator: 227 [new_demod,226] e_q2(bfalse,btrue)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 228 [] e_q2(btrue,bfalse)=bfalse. % 2.18/2.38 ---> New Demodulator: 229 [new_demod,228] e_q2(btrue,bfalse)=bfalse. % 2.18/2.38 ** KEPT (pick-wt=5): 230 [] e_q(A,A)=btrue. % 2.18/2.38 ---> New Demodulator: 231 [new_demod,230] e_q(A,A)=btrue. % 2.18/2.38 ** KEPT (pick-wt=5): 232 [] e_q2(A,A)=btrue. % 2.18/2.38 ---> New Demodulator: 233 [new_demod,232] e_q2(A,A)=btrue. % 2.18/2.38 Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] A=A. % 2.18/2.38 >>>> Starting back demodulation with 4. % 2.18/2.38 >>>> Starting back demodulation with 6. % 2.18/2.38 >>>> Starting back demodulation with 9. % 2.18/2.38 >>>> Starting back demodulation with 12. % 2.18/2.38 >>>> Starting back demodulation with 15. % 2.18/2.38 >>>> Starting back demodulation with 17. % 2.18/2.38 >>>> Starting back demodulation with 19. % 2.18/2.38 >>>> Starting back demodulation with 21. % 2.18/2.38 >>>> Starting back demodulation with 23. % 2.18/2.38 >>>> Starting back demodulation with 25. % 2.18/2.38 >>>> Starting back demodulation with 27. % 2.18/2.38 >>>> Starting back demodulation with 29. % 2.18/2.38 >>>> Starting back demodulation with 31. % 2.18/2.38 >>>> Starting back demodulation with 33. % 2.18/2.38 >>>> Starting back demodulation with 35. % 2.18/2.38 >>>> Starting back demodulation with 37. % 2.18/2.38 >>>> Starting back demodulation with 39. % 2.18/2.38 >>>> Starting back demodulation with 41. % 2.18/2.38 >>>> Starting back demodulation with 43. % 2.18/2.38 >>>> Starting back demodulation with 45. % 2.18/2.38 >>>> Starting back demodulation with 47. % 2.18/2.38 >>>> Starting back demodulation with 49. % 2.18/2.38 >>>> Starting back demodulation with 51. % 2.18/2.38 >>>> Starting back demodulation with 53. % 2.18/2.38 >>>> Starting back demodulation with 55. % 2.18/2.38 >>>> Starting back demodulation with 57. % 2.18/2.38 >>>> Starting back demodulation with 59. % 2.18/2.38 >>>> Starting back demodulation with 61. % 2.18/2.38 >>>> Starting back demodulation with 63. % 2.18/2.38 >>>> Starting back demodulation with 65. % 2.18/2.38 >>>> Starting back demodulation with 67. % 2.18/2.38 >>>> Starting back demodulation with 69. % 2.18/2.38 >>>> Starting back demodulation with 71. % 2.18/2.38 >>>> Starting back demodulation with 73. % 2.18/2.38 >>>> Starting back demodulation with 75. % 2.18/2.38 >>>> Starting back demodulation with 77. % 2.18/2.38 >>>> Starting back demodulation with 79. % 2.18/2.38 >>>> Starting back demodulation with 81. % 2.18/2.38 >>>> Starting back demodulation with 83. % 2.18/2.38 >>>> Starting back demodulation with 85. % 2.18/2.38 >>>> Starting back demodulation with 87. % 2.18/2.38 >>>> Starting back demodulation with 89. % 2.18/2.38 >>>> Starting back demodulation with 91. % 2.18/2.38 >>>> Starting back demodulation with 93. % 2.18/2.38 >>>> Starting back demodulation with 95. % 2.18/2.38 >>>> Starting back demodulation with 97. % 2.18/2.38 >>>> Starting back demodulation with 99. % 2.18/2.38 >>>> Starting back demodulation with 101. % 2.18/2.38 >>>> Starting back demodulation with 103. % 2.18/2.38 >>>> Starting back demodulation with 105. % 2.18/2.38 >>>> Starting back demodulation with 107. % 2.18/2.38 >>>> Starting back demodulation with 109. % 2.18/2.38 >>>> Starting back demodulation with 111. % 2.18/2.38 >>>> Starting back demodulation with 113. % 2.18/2.38 >>>> Starting back demodulation with 115. % 2.18/2.38 >>>> Starting back demodulation with 117. % 2.18/2.38 >>>> Starting back demodulation with 119. % 2.18/2.38 >>>> Starting back demodulation with 121. % 2.18/2.38 >>>> Starting back demodulation with 123. % 2.18/2.38 >>>> Starting back demodulation with 125. % 2.18/2.38 >>>> Starting back demodulation with 127. % 2.18/2.38 >>>> Starting back demodulation with 129. % 2.18/2.38 >>>> Starting back demodulation with 131. % 2.18/2.38 >>>> Starting back demodulation with 133. % 2.18/2.38 >>>> Starting back demodulation with 135. % 2.18/2.38 >>>> Starting back demodulation with 137. % 2.18/2.38 >>>> Starting back demodulation with 139. % 2.18/2.38 >>>> Starting back demodulation with 141. % 2.18/2.38 >>>> Starting back demodulation with 143. % 2.18/2.38 >>>> Starting back demodulation with 145. % 2.18/2.38 >>>> Starting back demodulation with 147. % 2.18/2.38 >>>> Starting back demodulation with 149. % 2.18/2.38 >>>> Starting back demodulation with 151. % 2.18/2.38 >>>> Starting back demodulation with 153. % 2.18/2.38 >>>> Starting back demodulation with 155. % 2.18/2.38 >>>> Starting back demodulation with 157. % 2.18/2.38 >>>> Starting back demodulation with 159. % 2.18/2.38 >>>> Starting back demodulation with 161. % 2.18/2.38 >>>> Starting back demodulation with 163. % 2.18/2.38 >>>> Starting back demodulation with 165. % 2.18/2.38 >>>> Starting back demodulation with 167. % 2.18/2.38 >>>> Starting back demodulation with 169. % 2.18/2.38 >>>> Starting back demodulation with 172. % 2.18/2.38 ** KEPT (pick-wt=13): 234 [copy,173,flip.1,demod,183,flip.1] step(y(A,B),C)=aux2(C,A,B,rec(A,nil2)). % 2.18/2.38 ---> New Demodulator: 235 [new_demod,234] step(y(A,B),C)=aux2(C,A,B,rec(A,nil2)). % 2.18/2.38 >>>> Starting back demodulation with 176. % 2.18/2.38 >>>> Starting back demodulation with 178. % 2.18/2.38 >>>> Starting back demodulation with 180. % 2.18/2.38 >>>> Starting back demodulation with 183. % 2.18/2.38 >> back demodulating 173 with 183. % 2.18/2.38 >> back demodulating 166 with 183. % 2.18/2.38 >> back demodulating 164 with 183. % 2.18/2.38 >> back demodulating 162 with 183. % 2.18/2.38 >> back demodulating 160 with 183. % 2.18/2.38 >> back demodulating 158 with 183. % 2.18/2.38 >> back demodulating 156 with 183. % 2.18/2.38 >>>> Starting back demodulation with 186. % 2.18/2.38 >>>> Starting back demodulation with 188. % 2.23/2.48 ** KEPT (pick-wt=21): 248 [copy,189,flip.1] cons3(andb(reck2(A,B),rec(C,D)),reck(A,C,E))=reck(A,C,cons(pair2(B,D),E)). % 2.23/2.48 >>>> Starting back demodulation with 191. % 2.23/2.48 >>>> Starting back demodulation with 193. % 2.23/2.48 >>>> Starting back demodulation with 195. % 2.23/2.48 >>>> Starting back demodulation with 197. % 2.23/2.48 >>>> Starting back demodulation with 199. % 2.23/2.48 >>>> Starting back demodulation with 201. % 2.23/2.48 >>>> Starting back demodulation with 203. % 2.23/2.48 >>>> Starting back demodulation with 206. % 2.23/2.48 >>>> Starting back demodulation with 208. % 2.23/2.48 >>>> Starting back demodulation with 211. % 2.23/2.48 >>>> Starting back demodulation with 213. % 2.23/2.48 >> back demodulating 1 with 213. % 2.23/2.48 >>>> Starting back demodulation with 215. % 2.23/2.48 >>>> Starting back demodulation with 217. % 2.23/2.48 >>>> Starting back demodulation with 219. % 2.23/2.48 >>>> Starting back demodulation with 221. % 2.23/2.48 >>>> Starting back demodulation with 223. % 2.23/2.48 >>>> Starting back demodulation with 225. % 2.23/2.48 >>>> Starting back demodulation with 227. % 2.23/2.48 >>>> Starting back demodulation with 229. % 2.23/2.48 >>>> Starting back demodulation with 231. % 2.23/2.48 >>>> Starting back demodulation with 233. % 2.23/2.48 >>>> Starting back demodulation with 235. % 2.23/2.48 >>>> Starting back demodulation with 237. % 2.23/2.48 >>>> Starting back demodulation with 239. % 2.23/2.48 >>>> Starting back demodulation with 241. % 2.23/2.48 >>>> Starting back demodulation with 243. % 2.23/2.48 >>>> Starting back demodulation with 245. % 2.23/2.48 >>>> Starting back demodulation with 247. % 2.23/2.48 Following clause subsumed by 189 during input processing: 0 [copy,248,flip.1] reck(A,B,cons(pair2(C,D),E))=cons3(andb(reck2(A,C),rec(B,D)),reck(A,B,E)). % 2.23/2.48 % 2.23/2.48 ======= end of input processing ======= % 2.23/2.48 % 2.23/2.48 =========== start of search =========== % 2.23/2.48 % 2.23/2.48 % 2.23/2.48 Resetting weight limit to 13. % 2.23/2.48 % 2.23/2.48 % 2.23/2.48 Resetting weight limit to 13. % 2.23/2.48 % 2.23/2.48 sos_size=187 % 2.23/2.48 % 2.23/2.48 % 2.23/2.48 Resetting weight limit to 12. % 2.23/2.48 % 2.23/2.48 % 2.23/2.48 Resetting weight limit to 12. % 2.23/2.48 % 2.23/2.48 sos_size=121 % 2.23/2.48 % 2.23/2.48 Search stopped because sos empty. % 2.23/2.48 % 2.23/2.48 % 2.23/2.48 Search stopped because sos empty. % 2.23/2.48 % 2.23/2.48 ============ end of search ============ % 2.23/2.48 % 2.23/2.48 -------------- statistics ------------- % 2.23/2.48 clauses given 450 % 2.23/2.48 clauses generated 10466 % 2.23/2.48 clauses kept 490 % 2.23/2.48 clauses forward subsumed 1952 % 2.23/2.48 clauses back subsumed 8 % 2.23/2.48 Kbytes malloced 7812 % 2.23/2.48 % 2.23/2.48 ----------- times (seconds) ----------- % 2.23/2.48 user CPU time 0.11 (0 hr, 0 min, 0 sec) % 2.23/2.48 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.23/2.48 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.23/2.48 % 2.23/2.48 Process 4548 finished Tue May 5 13:15:38 2026 % 2.23/2.48 Otter interrupted % 2.23/2.48 PROOF NOT FOUND %------------------------------------------------------------------------------