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