%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX242-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n006.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 1.95s 2.19s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX242-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.14/0.33 % Computer : n006.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Tue May 5 13:29:15 EDT 2026 % 0.14/0.33 % CPUTime : % 1.95/2.16 ----- Otter 3.3f, August 2004 ----- % 1.95/2.16 The process was started by sandbox on n006.cluster.edu, % 1.95/2.16 Tue May 5 13:29:16 2026 % 1.95/2.16 The command was "./otter". The process ID is 25289. % 1.95/2.16 % 1.95/2.16 set(prolog_style_variables). % 1.95/2.16 set(auto). % 1.95/2.16 dependent: set(auto1). % 1.95/2.16 dependent: set(process_input). % 1.95/2.16 dependent: clear(print_kept). % 1.95/2.16 dependent: clear(print_new_demod). % 1.95/2.16 dependent: clear(print_back_demod). % 1.95/2.16 dependent: clear(print_back_sub). % 1.95/2.16 dependent: set(control_memory). % 1.95/2.16 dependent: assign(max_mem, 12000). % 1.95/2.16 dependent: assign(pick_given_ratio, 4). % 1.95/2.16 dependent: assign(stats_level, 1). % 1.95/2.16 dependent: assign(max_seconds, 10800). % 1.95/2.16 clear(print_given). % 1.95/2.16 % 1.95/2.16 list(usable). % 1.95/2.16 0 [] A=A. % 1.95/2.16 0 [] aux(X,Y,Z,btrue)=Y. % 1.95/2.16 0 [] aux(X,Y,Z,bfalse)=var(Z). % 1.95/2.16 0 [] aux2(X,Y,Z,X2,btrue)=Y. % 1.95/2.16 0 [] aux2(X,Y,Z,X2,bfalse)=apply1(Z,X2). % 1.95/2.16 0 [] aux3(X,Ts,F,Ts2,Us,G,Vs,btrue)=unifyloop(X,append(Ts2,Ts),append(Vs,Us)). % 1.95/2.16 0 [] aux3(X,Ts,F,Ts2,Us,G,Vs,bfalse)=fail(X,cons(app(G,Vs),Us),app(F,Ts2),Ts). % 1.95/2.16 0 [] aux4(X,Y,X2,X3,X4,X5,btrue)=nothing. % 1.95/2.16 0 [] aux4(X,Y,X2,X3,X4,X5,bfalse)=unifybind(X,Y,app(X4,X5),X2,X3). % 1.95/2.16 0 [] aux5(X,Y,X2,X3,Y2,btrue)=unifyloop(X,X2,X3). % 1.95/2.16 0 [] aux5(X,Y,X2,X3,Y2,bfalse)=unifybind(X,Y,var(Y2),X2,X3). % 1.95/2.16 0 [] aux6(X,Y,nothing)=btrue. % 1.95/2.16 0 [] aux6(X,Y,just(Sub))=e_q3(subst(Sub,X),subst(Sub,Y)). % 1.95/2.16 0 [] aux7(X,Y,Z,Y2,btrue)=Z. % 1.95/2.16 0 [] aux7(X,Y,Z,Y2,bfalse)=subst(lam(Y,Z),apply1(X,Y2)). % 1.95/2.16 0 [] fail(X,nil,X4,Ts)=nothing. % 1.95/2.16 0 [] fail(X,cons(app(X6,X7),Us),X4,Ts)=nothing. % 1.95/2.16 0 [] fail(X,cons(var(X8),Us),X4,Ts)=unifyvar(X,X8,X4,Ts,Us). % 1.95/2.16 0 [] sub(X,Y,Z)=lam2(X,Y,Z). % 1.95/2.16 0 [] subst(X,app(F,Xs))=app(F,substList(X,Xs)). % 1.95/2.16 0 [] subst(X,var(Z))=apply1(X,Z). % 1.95/2.16 0 [] substList(Sub,nil)=nil. % 1.95/2.16 0 [] substList(Sub,cons(Y,Xs))=cons(subst(Sub,Y),substList(Sub,Xs)). % 1.95/2.16 0 [] substSubst(X,Y,Z)=subst(X,apply1(Y,Z)). % 1.95/2.16 0 [] singleton(X,Y,Z)=aux(X,Y,Z,e_q2(X,Z)). % 1.95/2.16 0 [] orb(btrue,Q)=btrue. % 1.95/2.16 0 [] orb(bfalse,Q)=Q. % 1.95/2.16 0 [] unify(X,nil)=bfalse. % 1.95/2.16 0 [] unify(X,cons(Z,Xs))=orb(unifyoccurs(X,Z),unify(X,Xs)). % 1.95/2.16 0 [] unifyoccurs(X,app(Z,Ts))=unify(X,Ts). % 1.95/2.16 0 [] unifyoccurs(X,var(Y2))=e_q2(X,Y2). % 1.95/2.16 0 [] extend(X,Y,Z,X2)=aux2(X,Y,Z,X2,e_q2(X,X2)). % 1.95/2.16 0 [] unifyloop(X,nil,nil)=just(X). % 1.95/2.16 0 [] unifyloop(X,nil,cons(X2,X3))=nothing. % 1.95/2.16 0 [] unifyloop(X,cons(app(F,Ts2),Ts),nil)=fail(X,nil,app(F,Ts2),Ts). % 1.95/2.16 0 [] unifyloop(X,cons(app(F,Ts2),Ts),cons(app(G,Vs),Us))=aux3(X,Ts,F,Ts2,Us,G,Vs,e_q2(F,G)). % 1.95/2.16 0 [] unifyloop(X,cons(app(F,Ts2),Ts),cons(var(X10),Us))=fail(X,cons(var(X10),Us),app(F,Ts2),Ts). % 1.95/2.16 0 [] unifyloop(X,cons(var(X11),Ts),nil)=fail(X,nil,var(X11),Ts). % 1.95/2.16 0 [] unifyloop(X,cons(var(X11),Ts),cons(U1,Ws))=unifyvar(X,X11,U1,Ts,Ws). % 1.95/2.16 0 [] unifyvar(X,Y,app(X4,X5),X2,X3)=aux4(X,Y,X2,X3,X4,X5,unifyoccurs(Y,app(X4,X5))). % 1.95/2.16 0 [] unifyvar(X,Y,var(Y2),X2,X3)=aux5(X,Y,X2,X3,Y2,e_q2(Y,Y2)). % 1.95/2.16 0 [] unifybind(X,Y,Z,X2,X3)=unifyloop(sub(X,Y,Z),substList(sub(X,Y,Z),X2),substList(sub(X,Y,Z),X3)). % 1.95/2.16 0 [] unify2(X,Y)=unifyloop(lam3,cons(X,nil),cons(Y,nil)). % 1.95/2.16 0 [] unificationOK(X,Y)=aux6(X,Y,unify2(X,Y)). % 1.95/2.16 0 [] prop_unify_makes_e_qual(X,Y)=e_q4(unificationOK(X,Y),btrue). % 1.95/2.16 0 [] isJust2(nothing)=bfalse. % 1.95/2.16 0 [] isJust2(just(Y))=btrue. % 1.95/2.16 0 [] append(nil,Y)=Y. % 1.95/2.16 0 [] append(cons(Z,Xs),Y)=cons(Z,append(Xs,Y)). % 1.95/2.16 0 [] e_q2(a,b)=bfalse. % 1.95/2.16 0 [] e_q2(a,c)=bfalse. % 1.95/2.16 0 [] e_q2(b,a)=bfalse. % 1.95/2.16 0 [] e_q2(b,c)=bfalse. % 1.95/2.16 0 [] e_q2(c,a)=bfalse. % 1.95/2.16 0 [] e_q2(c,b)=bfalse. % 1.95/2.16 0 [] e_q4(bfalse,btrue)=bfalse. % 1.95/2.16 0 [] e_q4(btrue,bfalse)=bfalse. % 1.95/2.16 0 [] e_q2(X,X)=btrue. % 1.95/2.16 0 [] e_q3(X,X)=btrue. % 1.95/2.16 0 [] e_q4(X,X)=btrue. % 1.95/2.16 0 [] e_q(X,X)=btrue. % 1.95/2.16 0 [] e_q3(X,Z)!=bfalse|e_q(cons(X,Y),cons(Z,X2))=bfalse. % 1.95/2.16 0 [] e_q3(X,Z)!=btrue|e_q(cons(X,Y),cons(Z,X2))=e_q(Y,X2). % 1.95/2.16 0 [] e_q(nil,cons(X,Y))=bfalse. % 1.95/2.16 0 [] e_q(cons(X,Y),nil)=bfalse. % 1.95/2.16 0 [] e_q2(X,Z)!=bfalse|e_q3(app(X,Y),app(Z,X2))=bfalse. % 1.95/2.16 0 [] e_q2(X,Z)!=btrue|e_q3(app(X,Y),app(Z,X2))=e_q(Y,X2). % 1.95/2.16 0 [] e_q3(var(X),var(Y))=e_q2(X,Y). % 1.95/2.16 0 [] e_q3(app(X,Y),var(Z))=bfalse. % 1.95/2.16 0 [] e_q3(var(X),app(Y,Z))=bfalse. % 1.95/2.16 0 [] apply1(lam2(X,Y,Z),Y2)=aux7(X,Y,Z,Y2,e_q2(Y,Y2)). % 1.95/2.16 0 [] apply1(lam(Y,Z),X4)=singleton(Y,Z,X4). % 1.95/2.16 0 [] apply1(lam3,Z)=var(Z). % 1.95/2.16 0 [] e_q4(prop_unify_makes_e_qual(X,Y),bfalse)!=btrue. % 1.95/2.16 end_of_list. % 1.95/2.16 % 1.95/2.16 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. % 1.95/2.16 % 1.95/2.16 This is a Horn set with equality. The strategy will be % 1.95/2.16 Knuth-Bendix and hyper_res, with positive clauses in % 1.95/2.16 sos and nonpositive clauses in usable. % 1.95/2.16 % 1.95/2.16 dependent: set(knuth_bendix). % 1.95/2.16 dependent: set(anl_eq). % 1.95/2.16 dependent: set(para_from). % 1.95/2.16 dependent: set(para_into). % 1.95/2.16 dependent: clear(para_from_right). % 1.95/2.16 dependent: clear(para_into_right). % 1.95/2.16 dependent: set(para_from_vars). % 1.95/2.16 dependent: set(eq_units_both_ways). % 1.95/2.16 dependent: set(dynamic_demod_all). % 1.95/2.16 dependent: set(dynamic_demod). % 1.95/2.16 dependent: set(order_eq). % 1.95/2.16 dependent: set(back_demod). % 1.95/2.16 dependent: set(lrpo). % 1.95/2.16 dependent: set(hyper_res). % 1.95/2.16 dependent: clear(order_hyper). % 1.95/2.16 % 1.95/2.16 ------------> process usable: % 1.95/2.16 ** KEPT (pick-wt=14): 1 [] e_q3(A,B)!=bfalse|e_q(cons(A,C),cons(B,D))=bfalse. % 1.95/2.16 ** KEPT (pick-wt=16): 2 [] e_q3(A,B)!=btrue|e_q(cons(A,C),cons(B,D))=e_q(C,D). % 1.95/2.16 ** KEPT (pick-wt=14): 3 [] e_q2(A,B)!=bfalse|e_q3(app(A,C),app(B,D))=bfalse. % 1.95/2.16 ** KEPT (pick-wt=16): 4 [] e_q2(A,B)!=btrue|e_q3(app(A,C),app(B,D))=e_q(C,D). % 1.95/2.16 ** KEPT (pick-wt=7): 5 [] e_q4(prop_unify_makes_e_qual(A,B),bfalse)!=btrue. % 1.95/2.16 % 1.95/2.16 ------------> process sos: % 1.95/2.16 ** KEPT (pick-wt=3): 6 [] A=A. % 1.95/2.16 ** KEPT (pick-wt=7): 7 [] aux(A,B,C,btrue)=B. % 1.95/2.16 ---> New Demodulator: 8 [new_demod,7] aux(A,B,C,btrue)=B. % 1.95/2.16 ** KEPT (pick-wt=8): 9 [] aux(A,B,C,bfalse)=var(C). % 1.95/2.16 ** KEPT (pick-wt=8): 10 [] aux2(A,B,C,D,btrue)=B. % 1.95/2.16 ---> New Demodulator: 11 [new_demod,10] aux2(A,B,C,D,btrue)=B. % 1.95/2.16 ** KEPT (pick-wt=10): 12 [] aux2(A,B,C,D,bfalse)=apply1(C,D). % 1.95/2.16 ** KEPT (pick-wt=18): 13 [] aux3(A,B,C,D,E,F,G,btrue)=unifyloop(A,append(D,B),append(G,E)). % 1.95/2.16 ** KEPT (pick-wt=21): 15 [copy,14,flip.1] fail(A,cons(app(B,C),D),app(E,F),G)=aux3(A,G,E,F,D,B,C,bfalse). % 1.95/2.16 ---> New Demodulator: 16 [new_demod,15] fail(A,cons(app(B,C),D),app(E,F),G)=aux3(A,G,E,F,D,B,C,bfalse). % 1.95/2.16 ** KEPT (pick-wt=10): 17 [] aux4(A,B,C,D,E,F,btrue)=nothing. % 1.95/2.16 ---> New Demodulator: 18 [new_demod,17] aux4(A,B,C,D,E,F,btrue)=nothing. % 1.95/2.16 ** KEPT (pick-wt=17): 20 [copy,19,flip.1] unifybind(A,B,app(C,D),E,F)=aux4(A,B,E,F,C,D,bfalse). % 1.95/2.16 ---> New Demodulator: 21 [new_demod,20] unifybind(A,B,app(C,D),E,F)=aux4(A,B,E,F,C,D,bfalse). % 1.95/2.16 ** KEPT (pick-wt=12): 22 [] aux5(A,B,C,D,E,btrue)=unifyloop(A,C,D). % 1.95/2.16 ** KEPT (pick-wt=15): 24 [copy,23,flip.1] unifybind(A,B,var(C),D,E)=aux5(A,B,D,E,C,bfalse). % 1.95/2.16 ---> New Demodulator: 25 [new_demod,24] unifybind(A,B,var(C),D,E)=aux5(A,B,D,E,C,bfalse). % 1.95/2.16 ** KEPT (pick-wt=6): 26 [] aux6(A,B,nothing)=btrue. % 1.95/2.16 ---> New Demodulator: 27 [new_demod,26] aux6(A,B,nothing)=btrue. % 1.95/2.16 ** KEPT (pick-wt=13): 28 [] aux6(A,B,just(C))=e_q3(subst(C,A),subst(C,B)). % 1.95/2.16 ** KEPT (pick-wt=8): 29 [] aux7(A,B,C,D,btrue)=C. % 1.95/2.16 ---> New Demodulator: 30 [new_demod,29] aux7(A,B,C,D,btrue)=C. % 1.95/2.16 ** KEPT (pick-wt=14): 32 [copy,31,flip.1] subst(lam(A,B),apply1(C,D))=aux7(C,A,B,D,bfalse). % 1.95/2.16 ---> New Demodulator: 33 [new_demod,32] subst(lam(A,B),apply1(C,D))=aux7(C,A,B,D,bfalse). % 1.95/2.16 ** KEPT (pick-wt=7): 34 [] fail(A,nil,B,C)=nothing. % 1.95/2.16 ---> New Demodulator: 35 [new_demod,34] fail(A,nil,B,C)=nothing. % 1.95/2.16 ** KEPT (pick-wt=11): 36 [] fail(A,cons(app(B,C),D),E,F)=nothing. % 1.95/2.16 ---> New Demodulator: 37 [new_demod,36] fail(A,cons(app(B,C),D),E,F)=nothing. % 1.95/2.16 ** KEPT (pick-wt=15): 38 [] fail(A,cons(var(B),C),D,E)=unifyvar(A,B,D,E,C). % 1.95/2.16 ---> New Demodulator: 39 [new_demod,38] fail(A,cons(var(B),C),D,E)=unifyvar(A,B,D,E,C). % 1.95/2.16 ** KEPT (pick-wt=9): 40 [] sub(A,B,C)=lam2(A,B,C). % 1.95/2.16 ---> New Demodulator: 41 [new_demod,40] sub(A,B,C)=lam2(A,B,C). % 1.95/2.16 ** KEPT (pick-wt=11): 42 [] subst(A,app(B,C))=app(B,substList(A,C)). % 1.95/2.16 ** KEPT (pick-wt=8): 43 [] subst(A,var(B))=apply1(A,B). % 1.95/2.16 ---> New Demodulator: 44 [new_demod,43] subst(A,var(B))=apply1(A,B). % 1.95/2.16 ** KEPT (pick-wt=5): 45 [] substList(A,nil)=nil. % 1.95/2.16 ---> New Demodulator: 46 [new_demod,45] substList(A,nil)=nil. % 1.95/2.16 ** KEPT (pick-wt=13): 47 [] substList(A,cons(B,C))=cons(subst(A,B),substList(A,C)). % 1.95/2.16 ---> New Demodulator: 48 [new_demod,47] substList(A,cons(B,C))=cons(subst(A,B),substList(A,C)). % 1.95/2.16 ** KEPT (pick-wt=10): 50 [copy,49,flip.1] subst(A,apply1(B,C))=substSubst(A,B,C). % 1.95/2.16 ---> New Demodulator: 51 [new_demod,50] subst(A,apply1(B,C))=substSubst(A,B,C). % 1.95/2.16 ** KEPT (pick-wt=12): 52 [] singleton(A,B,C)=aux(A,B,C,e_q2(A,C)). % 1.95/2.16 ** KEPT (pick-wt=5): 53 [] orb(btrue,A)=btrue. % 1.95/2.16 ---> New Demodulator: 54 [new_demod,53] orb(btrue,A)=btrue. % 1.95/2.16 ** KEPT (pick-wt=5): 55 [] orb(bfalse,A)=A. % 1.95/2.16 ---> New Demodulator: 56 [new_demod,55] orb(bfalse,A)=A. % 1.95/2.16 ** KEPT (pick-wt=5): 57 [] unify(A,nil)=bfalse. % 1.95/2.16 ---> New Demodulator: 58 [new_demod,57] unify(A,nil)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=13): 59 [] unify(A,cons(B,C))=orb(unifyoccurs(A,B),unify(A,C)). % 1.95/2.16 ** KEPT (pick-wt=9): 60 [] unifyoccurs(A,app(B,C))=unify(A,C). % 1.95/2.16 ---> New Demodulator: 61 [new_demod,60] unifyoccurs(A,app(B,C))=unify(A,C). % 1.95/2.16 ** KEPT (pick-wt=8): 62 [] unifyoccurs(A,var(B))=e_q2(A,B). % 1.95/2.16 ---> New Demodulator: 63 [new_demod,62] unifyoccurs(A,var(B))=e_q2(A,B). % 1.95/2.16 ** KEPT (pick-wt=14): 64 [] extend(A,B,C,D)=aux2(A,B,C,D,e_q2(A,D)). % 1.95/2.16 ** KEPT (pick-wt=7): 66 [copy,65,flip.1] just(A)=unifyloop(A,nil,nil). % 1.95/2.16 ---> New Demodulator: 67 [new_demod,66] just(A)=unifyloop(A,nil,nil). % 1.95/2.16 ** KEPT (pick-wt=8): 68 [] unifyloop(A,nil,cons(B,C))=nothing. % 1.95/2.16 ---> New Demodulator: 69 [new_demod,68] unifyloop(A,nil,cons(B,C))=nothing. % 1.95/2.16 ** KEPT (pick-wt=10): 71 [copy,70,demod,35] unifyloop(A,cons(app(B,C),D),nil)=nothing. % 1.95/2.16 ---> New Demodulator: 72 [new_demod,71] unifyloop(A,cons(app(B,C),D),nil)=nothing. % 1.95/2.16 ** KEPT (pick-wt=24): 73 [] unifyloop(A,cons(app(B,C),D),cons(app(E,F),G))=aux3(A,D,B,C,G,E,F,e_q2(B,E)). % 1.95/2.16 ** KEPT (pick-wt=20): 75 [copy,74,demod,39] unifyloop(A,cons(app(B,C),D),cons(var(E),F))=unifyvar(A,E,app(B,C),D,F). % 1.95/2.16 ---> New Demodulator: 76 [new_demod,75] unifyloop(A,cons(app(B,C),D),cons(var(E),F))=unifyvar(A,E,app(B,C),D,F). % 1.95/2.16 ** KEPT (pick-wt=9): 78 [copy,77,demod,35] unifyloop(A,cons(var(B),C),nil)=nothing. % 1.95/2.16 ---> New Demodulator: 79 [new_demod,78] unifyloop(A,cons(var(B),C),nil)=nothing. % 1.95/2.16 ** KEPT (pick-wt=16): 80 [] unifyloop(A,cons(var(B),C),cons(D,E))=unifyvar(A,B,D,C,E). % 1.95/2.16 ---> New Demodulator: 81 [new_demod,80] unifyloop(A,cons(var(B),C),cons(D,E))=unifyvar(A,B,D,C,E). % 1.95/2.16 ** KEPT (pick-wt=19): 83 [copy,82,demod,61] unifyvar(A,B,app(C,D),E,F)=aux4(A,B,E,F,C,D,unify(B,D)). % 1.95/2.16 ** KEPT (pick-wt=17): 84 [] unifyvar(A,B,var(C),D,E)=aux5(A,B,D,E,C,e_q2(B,C)). % 1.95/2.16 ** KEPT (pick-wt=24): 86 [copy,85,demod,41,41,41,flip.1] unifyloop(lam2(A,B,C),substList(lam2(A,B,C),D),substList(lam2(A,B,C),E))=unifybind(A,B,C,D,E). % 1.95/2.16 ---> New Demodulator: 87 [new_demod,86] unifyloop(lam2(A,B,C),substList(lam2(A,B,C),D),substList(lam2(A,B,C),E))=unifybind(A,B,C,D,E). % 1.95/2.16 ** KEPT (pick-wt=12): 88 [] unify2(A,B)=unifyloop(lam3,cons(A,nil),cons(B,nil)). % 1.95/2.16 ---> New Demodulator: 89 [new_demod,88] unify2(A,B)=unifyloop(lam3,cons(A,nil),cons(B,nil)). % 1.95/2.16 ** KEPT (pick-wt=15): 91 [copy,90,demod,89] unificationOK(A,B)=aux6(A,B,unifyloop(lam3,cons(A,nil),cons(B,nil))). % 1.95/2.16 ---> New Demodulator: 92 [new_demod,91] unificationOK(A,B)=aux6(A,B,unifyloop(lam3,cons(A,nil),cons(B,nil))). % 1.95/2.16 ** KEPT (pick-wt=17): 94 [copy,93,demod,92] prop_unify_makes_e_qual(A,B)=e_q4(aux6(A,B,unifyloop(lam3,cons(A,nil),cons(B,nil))),btrue). % 1.95/2.16 ---> New Demodulator: 95 [new_demod,94] prop_unify_makes_e_qual(A,B)=e_q4(aux6(A,B,unifyloop(lam3,cons(A,nil),cons(B,nil))),btrue). % 1.95/2.16 ** KEPT (pick-wt=4): 96 [] isJust2(nothing)=bfalse. % 1.95/2.16 ---> New Demodulator: 97 [new_demod,96] isJust2(nothing)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=7): 99 [copy,98,demod,67] isJust2(unifyloop(A,nil,nil))=btrue. % 1.95/2.16 ---> New Demodulator: 100 [new_demod,99] isJust2(unifyloop(A,nil,nil))=btrue. % 1.95/2.16 ** KEPT (pick-wt=5): 101 [] append(nil,A)=A. % 1.95/2.16 ---> New Demodulator: 102 [new_demod,101] append(nil,A)=A. % 1.95/2.16 ** KEPT (pick-wt=11): 104 [copy,103,flip.1] cons(A,append(B,C))=append(cons(A,B),C). % 1.95/2.16 ---> New Demodulator: 105 [new_demod,104] cons(A,append(B,C))=append(cons(A,B),C). % 1.95/2.16 ** KEPT (pick-wt=5): 106 [] e_q2(a,b)=bfalse. % 1.95/2.16 ---> New Demodulator: 107 [new_demod,106] e_q2(a,b)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=5): 108 [] e_q2(a,c)=bfalse. % 1.95/2.16 ---> New Demodulator: 109 [new_demod,108] e_q2(a,c)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=5): 110 [] e_q2(b,a)=bfalse. % 1.95/2.16 ---> New Demodulator: 111 [new_demod,110] e_q2(b,a)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=5): 112 [] e_q2(b,c)=bfalse. % 1.95/2.16 ---> New Demodulator: 113 [new_demod,112] e_q2(b,c)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=5): 114 [] e_q2(c,a)=bfalse. % 1.95/2.16 ---> New Demodulator: 115 [new_demod,114] e_q2(c,a)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=5): 116 [] e_q2(c,b)=bfalse. % 1.95/2.16 ---> New Demodulator: 117 [new_demod,116] e_q2(c,b)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=5): 118 [] e_q4(bfalse,btrue)=bfalse. % 1.95/2.16 ---> New Demodulator: 119 [new_demod,118] e_q4(bfalse,btrue)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=5): 120 [] e_q4(btrue,bfalse)=bfalse. % 1.95/2.16 ---> New Demodulator: 121 [new_demod,120] e_q4(btrue,bfalse)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=5): 122 [] e_q2(A,A)=btrue. % 1.95/2.16 ---> New Demodulator: 123 [new_demod,122] e_q2(A,A)=btrue. % 1.95/2.16 ** KEPT (pick-wt=5): 124 [] e_q3(A,A)=btrue. % 1.95/2.16 ---> New Demodulator: 125 [new_demod,124] e_q3(A,A)=btrue. % 1.95/2.16 ** KEPT (pick-wt=5): 126 [] e_q4(A,A)=btrue. % 1.95/2.16 ---> New Demodulator: 127 [new_demod,126] e_q4(A,A)=btrue. % 1.95/2.16 ** KEPT (pick-wt=5): 128 [] e_q(A,A)=btrue. % 1.95/2.16 ---> New Demodulator: 129 [new_demod,128] e_q(A,A)=btrue. % 1.95/2.16 ** KEPT (pick-wt=7): 130 [] e_q(nil,cons(A,B))=bfalse. % 1.95/2.16 ---> New Demodulator: 131 [new_demod,130] e_q(nil,cons(A,B))=bfalse. % 1.95/2.16 ** KEPT (pick-wt=7): 132 [] e_q(cons(A,B),nil)=bfalse. % 1.95/2.16 ---> New Demodulator: 133 [new_demod,132] e_q(cons(A,B),nil)=bfalse. % 1.95/2.16 ** KEPT (pick-wt=9): 134 [] e_q3(var(A),var(B))=e_q2(A,B). % 1.95/2.16 ---> New Demodulator: 135 [new_demod,134] e_q3(var(A),var(B))=e_q2(A,B). % 1.95/2.16 ** KEPT (pick-wt=8): 136 [] e_q3(app(A,B),var(C))=bfalse. % 1.95/2.16 ---> New Demodulator: 137 [new_demod,136] e_q3(app(A,B),var(C))=bfalse. % 1.95/2.16 ** KEPT (pick-wt=8): 138 [] e_q3(var(A),app(B,C))=bfalse. % 1.95/2.16 ---> New Demodulator: 139 [new_demod,138] e_q3(var(A),app(B,C))=bfalse. % 1.95/2.16 ** KEPT (pick-wt=15): 140 [] apply1(lam2(A,B,C),D)=aux7(A,B,C,D,e_q2(B,D)). % 1.95/2.16 ** KEPT (pick-wt=10): 141 [] apply1(lam(A,B),C)=singleton(A,B,C). % 1.95/2.16 ---> New Demodulator: 142 [new_demod,141] apply1(lam(A,B),C)=singleton(A,B,C). % 1.95/2.16 ** KEPT (pick-wt=6): 144 [copy,143,flip.1] var(A)=apply1(lam3,A). % 1.95/2.16 ---> New Demodulator: 145 [new_demod,144] var(A)=apply1(lam3,A). % 1.95/2.16 Following clause subsumed by 6 during input processing: 0 [copy,6,flip.1] A=A. % 1.95/2.16 >>>> Starting back demodulation with 8. % 1.95/2.16 ** KEPT (pick-wt=9): 146 [copy,9,flip.1,demod,145] apply1(lam3,A)=aux(B,C,A,bfalse). % 1.95/2.16 >>>> Starting back demodulation with 11. % 1.95/2.16 ** KEPT (pick-wt=10): 147 [copy,12,flip.1] apply1(A,B)=aux2(C,D,A,B,bfalse). % 1.95/2.16 ** KEPT (pick-wt=18): 148 [copy,13,flip.1] unifyloop(A,append(B,C),append(D,E))=aux3(A,C,F,B,E,G,D,btrue). % 1.95/2.16 >>>> Starting back demodulation with 16. % 1.95/2.16 >>>> Starting back demodulation with 18. % 1.95/2.16 >>>> Starting back demodulation with 21. % 1.95/2.16 ** KEPT (pick-wt=12): 149 [copy,22,flip.1] unifyloop(A,B,C)=aux5(A,D,B,C,E,btrue). % 1.95/2.16 >>>> Starting back demodulation with 25. % 1.95/2.16 >>>> Starting back demodulation with 27. % 1.95/2.16 ** KEPT (pick-wt=15): 150 [copy,28,flip.1,demod,67] e_q3(subst(A,B),subst(A,C))=aux6(B,C,unifyloop(A,nil,nil)). % 1.95/2.16 ---> New Demodulator: 151 [new_demod,150] e_q3(subst(A,B),subst(A,C))=aux6(B,C,unifyloop(A,nil,nil)). % 1.95/2.16 >>>> Starting back demodulation with 30. % 1.95/2.16 >>>> Starting back demodulation with 33. % 1.95/2.16 >>>> Starting back demodulation with 35. % 1.95/2.16 >>>> Starting back demodulation with 37. % 1.95/2.16 >> back demodulating 15 with 37. % 1.95/2.16 >>>> Starting back demodulation with 39. % 1.95/2.16 >>>> Starting back demodulation with 41. % 1.95/2.16 ** KEPT (pick-wt=11): 154 [copy,42,flip.1] app(A,substList(B,C))=subst(B,app(A,C)). % 1.95/2.16 >>>> Starting back demodulation with 44. % 1.95/2.16 >>>> Starting back demodulation with 46. % 1.95/2.16 >>>> Starting back demodulation with 48. % 1.95/2.16 >>>> Starting back demodulation with 51. % 1.95/2.16 >> back demodulating 32 with 51. % 1.95/2.16 ** KEPT (pick-wt=12): 157 [copy,52,flip.1] aux(A,B,C,e_q2(A,C))=singleton(A,B,C). % 1.95/2.16 >>>> Starting back demodulation with 54. % 1.95/2.16 >>>> Starting back demodulation with 56. % 1.95/2.16 >>>> Starting back demodulation with 58. % 1.95/2.16 ** KEPT (pick-wt=13): 158 [copy,59,flip.1] orb(unifyoccurs(A,B),unify(A,C))=unify(A,cons(B,C)). % 1.95/2.16 >>>> Starting back demodulation with 61. % 1.95/2.16 >>>> Starting back demodulation with 63. % 1.95/2.16 ** KEPT (pick-wt=14): 159 [copy,64,flip.1] aux2(A,B,C,D,e_q2(A,D))=extend(A,B,C,D). % 1.95/2.16 >>>> Starting back demodulation with 67. % 1.95/2.16 >> back demodulating 28 with 67. % 1.95/2.16 >>>> Starting back demodulation with 69. % 1.95/2.16 >>>> Starting back demodulation with 72. % 1.95/2.16 ** KEPT (pick-wt=24): 160 [copy,73,flip.1] aux3(A,B,C,D,E,F,G,e_q2(C,F))=unifyloop(A,cons(app(C,D),B),cons(app(F,G),E)). % 1.95/2.16 >>>> Starting back demodulation with 76. % 1.95/2.16 >>>> Starting back demodulation with 79. % 1.95/2.16 >>>> Starting back demodulation with 81. % 1.95/2.16 ** KEPT (pick-wt=19): 161 [copy,83,flip.1] aux4(A,B,C,D,E,F,unify(B,F))=unifyvar(A,B,app(E,F),C,D). % 1.95/2.16 ** KEPT (pick-wt=18): 162 [copy,84,flip.1,demod,145] aux5(A,B,C,D,E,e_q2(B,E))=unifyvar(A,B,apply1(lam3,E),C,D). % 1.95/2.16 >>>> Starting back demodulation with 87. % 1.95/2.16 >>>> Starting back demodulation with 89. % 1.95/2.16 >>>> Starting back demodulation with 92. % 1.95/2.16 >>>> Starting back demodulation with 95. % 1.95/2.16 >> back demodulating 5 with 95. % 1.95/2.16 >>>> Starting back demodulation with 97. % 1.95/2.16 >>>> Starting back demodulation with 100. % 1.95/2.16 >>>> Starting back demodulation with 102. % 1.95/2.16 >>>> Starting back demodulation with 105. % 1.95/2.16 >>>> Starting back demodulation with 107. % 1.95/2.16 >>>> Starting back demodulation with 109. % 1.95/2.16 >>>> Starting back demodulation with 111. % 1.95/2.16 >>>> Starting back demodulation with 113. % 1.95/2.16 >>>> Starting back demodulation with 115. % 1.95/2.16 >>>> Starting back demodulation with 117. % 1.95/2.16 >>>> Starting back demodulation with 119. % 1.95/2.16 >>>> Starting back demodulation with 121. % 1.95/2.16 >>>> Starting back demodulation with 123. % 1.95/2.16 >>>> Starting back demodulation with 125. % 1.95/2.16 >>>> Starting back demodulation with 127. % 1.95/2.16 >>>> Starting back demodulation with 129. % 1.95/2.16 >>>> Starting back demodulation with 131. % 1.95/2.16 >>>> Starting back demodulation with 133. % 1.95/2.16 >>>> Starting back demodulation with 135. % 1.95/2.16 >>>> Starting back demodulation with 137. % 1.95/2.16 >>>> Starting back demodulation with 139. % 1.95/2.16 ** KEPT (pick-wt=15): 164 [copy,140,flip.1] aux7(A,B,C,D,e_q2(B,D))=apply1(lam2(A,B,C),D). % 1.95/2.16 >>>> Starting back demodulation with 142. % 1.95/2.16 >>>> Starting back demodulation with 145. % 1.95/2.16 >> back demodulating 138 with 145. % 1.95/2.16 >> back demodulating 136 with 145. % 1.95/2.16 >> back demodulating 134 with 145. % 1.95/2.16 >> back demodulating 84 with 145. % 1.95/2.16 >> back demodulating 80 with 145. % 1.95/2.16 >> back demodulating 78 with 145. % 1.95/2.16 >> back demodulating 75 with 145. % 1.95/2.16 >> back demodulating 62 with 145. % 1.95/2.16 >> back demodulating 43 with 145. % 1.95/2.16 >> back demodulating 38 with 145. % 1.95/2.16 >> back demodulating 24 with 145. % 1.95/2.16 >> back demodulating 9 with 145. % 1.95/2.16 Following clause subsumed by 186 during input processing: 0 [copy,146,flip.1,demod,181] aux(A,B,C,bfalse)=substSubst(lam3,lam3,C). % 1.95/2.16 ** KEPT (pick-wt=11): 187 [copy,147,flip.1,demod,181] aux2(A,B,C,D,bfalse)=substSubst(C,lam3,D). % 1.95/2.16 Following clause subsumed by 13 during input processing: 0 [copy,148,flip.1] aux3(A,B,C,D,E,F,G,btrue)=unifyloop(A,append(D,B),append(G,E)). % 1.95/2.16 Following clause subsumed by 22 during input processing: 0 [copy,149,flip.1] aux5(A,B,C,D,E,btrue)=unifyloop(A,C,D). % 1.95/2.16 >>>> Starting back demodulation with 151. % 1.95/2.16 >>>> Starting back demodulation with 153. % 1.95/2.16 Following clause subsumed by 42 during input processing: 0 [copy,154,flip.1] subst(A,app(B,C))=app(B,substList(A,C)). % 1.95/2.16 >>>> Starting back demodulation with 156. % 1.95/2.16 Following clause subsumed by 52 during input processing: 0 [copy,157,flip.1] singleton(A,B,C)=aux(A,B,C,e_q2(A,C)). % 1.95/2.16 Following clause subsumed by 59 during input processing: 0 [copy,158,flip.1] unify(A,cons(B,C))=orb(unifyoccurs(A,B),unify(A,C)). % 1.95/2.16 Following clause subsumed by 64 during input processing: 0 [copy,159,flip.1] extend(A,B,C,D)=aux2(A,B,C,D,e_q2(A,D)). % 1.95/2.16 Following clause subsumed by 73 during input processing: 0 [copy,160,flip.1] unifyloop(A,cons(app(B,C),D),cons(app(E,F),G))=aux3(A,D,B,C,G,E,F,e_q2(B,E)). % 1.95/2.16 Following clause subsumed by 83 during input processing: 0 [copy,161,flip.1] unifyvar(A,B,app(C,D),E,F)=aux4(A,B,E,F,C,D,unify(B,D)). % 1.95/2.16 ** KEPT (pick-wt=19): 188 [copy,162,flip.1,demod,181] unifyvar(A,B,substSubst(lam3,lam3,C),D,E)=aux5(A,B,D,E,C,e_q2(B,C)). % 1.95/2.16 ** KEPT (pick-wt=16): 189 [copy,164,flip.1,demod,181] substSubst(lam2(A,B,C),lam3,D)=aux7(A,B,C,D,e_q2(B,D)). % 1.95/2.16 >>>> Starting back demodulation with 166. % 1.95/2.16 >>>> Starting back demodulation with 168. % 1.95/2.16 >>>> Starting back demodulation with 170. % 1.95/2.16 ** KEPT (pick-wt=19): 190 [copy,171,flip.1,demod,181] aux5(A,B,C,D,E,e_q2(B,E))=unifyvar(A,B,substSubst(lam3,lam3,E),C,D). % 1.95/2.16 >>>> Starting back demodulation with 173. % 1.95/2.16 >>>> Starting back demodulation with 175. % 1.95/2.16 >>>> Starting back demodulation with 177. % 1.95/2.16 >>>> Starting back demodulation with 179. % 1.95/2.16 >>>> Starting back demodulation with 181. % 1.95/2.16 >> back demodulating 178 with 181. % 1.95/2.16 >> back demodulating 176 with 181. % 1.95/2.16 >> back demodulating 174 with 181. % 1.95/2.16 >> back demodulating 172 with 181. % 1.95/2.16 >> back demodulating 171 with 181. % 1.95/2.19 >> back demodulating 169 with 181. % 1.95/2.19 >> back demodulating 167 with 181. % 1.95/2.19 >> back demodulating 165 with 181. % 1.95/2.19 >> back demodulating 164 with 181. % 1.95/2.19 >> back demodulating 162 with 181. % 1.95/2.19 >> back demodulating 147 with 181. % 1.95/2.19 >> back demodulating 146 with 181. % 1.95/2.19 >> back demodulating 144 with 181. % 1.95/2.19 >> back demodulating 141 with 181. % 1.95/2.19 >> back demodulating 140 with 181. % 1.95/2.19 >> back demodulating 50 with 181. % 1.95/2.19 >> back demodulating 12 with 181. % 1.95/2.19 >>>> Starting back demodulation with 183. % 1.95/2.19 >>>> Starting back demodulation with 185. % 1.95/2.19 Following clause subsumed by 207 during input processing: 0 [copy,186,flip.1] substSubst(lam3,lam3,A)=aux(B,C,A,bfalse). % 1.95/2.19 Following clause subsumed by 206 during input processing: 0 [copy,187,flip.1] substSubst(A,lam3,B)=aux2(C,D,A,B,bfalse). % 1.95/2.19 Following clause subsumed by 190 during input processing: 0 [copy,188,flip.1] aux5(A,B,C,D,E,e_q2(B,E))=unifyvar(A,B,substSubst(lam3,lam3,E),C,D). % 1.95/2.19 Following clause subsumed by 205 during input processing: 0 [copy,189,flip.1] aux7(A,B,C,D,e_q2(B,D))=substSubst(lam2(A,B,C),lam3,D). % 1.95/2.19 Following clause subsumed by 188 during input processing: 0 [copy,190,flip.1] unifyvar(A,B,substSubst(lam3,lam3,C),D,E)=aux5(A,B,D,E,C,e_q2(B,C)). % 1.95/2.19 >>>> Starting back demodulation with 192. % 1.95/2.19 >>>> Starting back demodulation with 194. % 1.95/2.19 >>>> Starting back demodulation with 196. % 1.95/2.19 >>>> Starting back demodulation with 198. % 1.95/2.19 >>>> Starting back demodulation with 200. % 1.95/2.19 >>>> Starting back demodulation with 202. % 1.95/2.19 >>>> Starting back demodulation with 204. % 1.95/2.19 Following clause subsumed by 189 during input processing: 0 [copy,205,flip.1] substSubst(lam2(A,B,C),lam3,D)=aux7(A,B,C,D,e_q2(B,D)). % 1.95/2.19 Following clause subsumed by 187 during input processing: 0 [copy,206,flip.1] aux2(A,B,C,D,bfalse)=substSubst(C,lam3,D). % 1.95/2.19 Following clause subsumed by 186 during input processing: 0 [copy,207,flip.1] aux(A,B,C,bfalse)=substSubst(lam3,lam3,C). % 1.95/2.19 >>>> Starting back demodulation with 209. % 1.95/2.19 >>>> Starting back demodulation with 211. % 1.95/2.19 >> back demodulating 157 with 211. % 1.95/2.19 >> back demodulating 52 with 211. % 1.95/2.19 >>>> Starting back demodulation with 213. % 1.95/2.19 >>>> Starting back demodulation with 215. % 1.95/2.19 % 1.95/2.19 ======= end of input processing ======= % 1.95/2.19 % 1.95/2.19 =========== start of search =========== % 1.95/2.19 % 1.95/2.19 % 1.95/2.19 Resetting weight limit to 11. % 1.95/2.19 % 1.95/2.19 % 1.95/2.19 Resetting weight limit to 11. % 1.95/2.19 % 1.95/2.19 sos_size=104 % 1.95/2.19 % 1.95/2.19 Search stopped because sos empty. % 1.95/2.19 % 1.95/2.19 % 1.95/2.19 Search stopped because sos empty. % 1.95/2.19 % 1.95/2.19 ============ end of search ============ % 1.95/2.19 % 1.95/2.19 -------------- statistics ------------- % 1.95/2.19 clauses given 179 % 1.95/2.19 clauses generated 2139 % 1.95/2.19 clauses kept 221 % 1.95/2.19 clauses forward subsumed 584 % 1.95/2.19 clauses back subsumed 0 % 1.95/2.19 Kbytes malloced 6835 % 1.95/2.19 % 1.95/2.19 ----------- times (seconds) ----------- % 1.95/2.19 user CPU time 0.03 (0 hr, 0 min, 0 sec) % 1.95/2.19 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 1.95/2.19 wall-clock time 1 (0 hr, 0 min, 1 sec) % 1.95/2.19 % 1.95/2.19 Process 25289 finished Tue May 5 13:29:17 2026 % 1.95/2.19 Otter interrupted % 1.95/2.19 PROOF NOT FOUND %------------------------------------------------------------------------------