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