%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX232-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n019.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:28 PM UTC 2026 % Result : Unknown 2.03s 2.25s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX232-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.17/0.34 % Computer : n019.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.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue May 5 13:04:59 EDT 2026 % 0.17/0.35 % CPUTime : % 2.03/2.24 ----- Otter 3.3f, August 2004 ----- % 2.03/2.24 The process was started by sandbox on n019.cluster.edu, % 2.03/2.24 Tue May 5 13:04:59 2026 % 2.03/2.24 The command was "./otter". The process ID is 30463. % 2.03/2.24 % 2.03/2.24 set(prolog_style_variables). % 2.03/2.24 set(auto). % 2.03/2.24 dependent: set(auto1). % 2.03/2.24 dependent: set(process_input). % 2.03/2.24 dependent: clear(print_kept). % 2.03/2.24 dependent: clear(print_new_demod). % 2.03/2.24 dependent: clear(print_back_demod). % 2.03/2.24 dependent: clear(print_back_sub). % 2.03/2.24 dependent: set(control_memory). % 2.03/2.24 dependent: assign(max_mem, 12000). % 2.03/2.24 dependent: assign(pick_given_ratio, 4). % 2.03/2.24 dependent: assign(stats_level, 1). % 2.03/2.24 dependent: assign(max_seconds, 10800). % 2.03/2.24 clear(print_given). % 2.03/2.24 % 2.03/2.24 list(usable). % 2.03/2.24 0 [] A=A. % 2.03/2.24 0 [] aux(X,Y,btrue)=Y. % 2.03/2.24 0 [] aux(X,Y,bfalse)=X. % 2.03/2.24 0 [] aux2(X,Y,btrue)=nil2. % 2.03/2.24 0 [] aux2(X,Y,bfalse)=cons2(X,enumFromToNat(suc(X),Y)). % 2.03/2.24 0 [] aux3(Y,Xs,btrue)=bfalse. % 2.03/2.24 0 [] aux3(Y,Xs,bfalse)=unique(Xs). % 2.03/2.24 0 [] predNat(zero)=zero. % 2.03/2.24 0 [] predNat(suc(Y))=Y. % 2.03/2.24 0 [] orb(btrue,Q)=btrue. % 2.03/2.24 0 [] orb(bfalse,Q)=Q. % 2.03/2.24 0 [] or2(nil3)=bfalse. % 2.03/2.24 0 [] or2(cons3(Y,Xs))=orb(Y,or2(Xs)). % 2.03/2.24 0 [] one=suc(zero). % 2.03/2.24 0 [] two=suc(one). % 2.03/2.24 0 [] three=suc(two). % 2.03/2.24 0 [] notb(btrue)=bfalse. % 2.03/2.24 0 [] notb(bfalse)=btrue. % 2.03/2.24 0 [] lt(zero,zero)=bfalse. % 2.03/2.24 0 [] lt(zero,suc(Z))=btrue. % 2.03/2.24 0 [] lt(suc(X2),zero)=bfalse. % 2.03/2.24 0 [] lt(suc(X2),suc(Y2))=lt(X2,Y2). % 2.03/2.24 0 [] maxNat(X,Y)=aux(X,Y,lt(X,Y)). % 2.03/2.24 0 [] maximum(X,nil)=X. % 2.03/2.24 0 [] maximum(X,cons(pair2(Y2,Z2),Yzs))=maximum(maxNat(X,maxNat(Y2,Z2)),Yzs). % 2.03/2.24 0 [] len(nil2)=zero. % 2.03/2.24 0 [] len(cons2(Y,Xs))=suc(len(Xs)). % 2.03/2.24 0 [] last(X,nil2)=X. % 2.03/2.24 0 [] last(X,cons2(Z,Ys))=last(Z,Ys). % 2.03/2.24 0 [] enumFromToNat(X,Y)=aux2(X,Y,lt(Y,X)). % 2.03/2.24 0 [] elem(X,nil2)=bfalse. % 2.03/2.24 0 [] elem(X,cons2(Z,Xs))=orb(e_q(Z,X),elem(X,Xs)). % 2.03/2.24 0 [] unique(nil2)=btrue. % 2.03/2.24 0 [] unique(cons2(Y,Xs))=aux3(Y,Xs,elem(Y,Xs)). % 2.03/2.24 0 [] dodeca(nil2)=nil. % 2.03/2.24 0 [] dodeca(cons2(Y,Z))=cons(pair2(Y,suc(Y)),dodeca(Z)). % 2.03/2.24 0 [] append(nil,Y)=Y. % 2.03/2.24 0 [] append(cons(Z,Xs),Y)=cons(Z,append(Xs,Y)). % 2.03/2.24 0 [] andb(btrue,Q)=Q. % 2.03/2.24 0 [] andb(bfalse,Q)=bfalse. % 2.03/2.24 0 [] path(X,Y,nil)=nil3. % 2.03/2.24 0 [] path(X,Y,cons(pair2(U,V),X3))=cons3(orb(andb(e_q(U,X),e_q(V,Y)),andb(e_q(U,Y),e_q(V,X))),path(X,Y,X3)). % 2.03/2.24 0 [] path2(nil2,Y)=btrue. % 2.03/2.24 0 [] path2(cons2(Z,nil2),Y)=btrue. % 2.03/2.24 0 [] path2(cons2(Z,cons2(Y2,Xs)),Y)=andb(or2(path(Z,Y2,Y)),path2(cons2(Y2,Xs),Y)). % 2.03/2.24 0 [] add(zero,Y)=Y. % 2.03/2.24 0 [] add(suc(Z),Y)=suc(add(Z,Y)). % 2.03/2.24 0 [] dodeca2(X,nil2)=nil. % 2.03/2.24 0 [] dodeca2(X,cons2(Z,X2))=cons(pair2(Z,add(suc(X),Z)),dodeca2(X,X2)). % 2.03/2.24 0 [] dodeca3(X,nil2)=nil. % 2.03/2.24 0 [] dodeca3(X,cons2(Z,X2))=cons(pair2(add(suc(X),Z),add(add(suc(X),suc(X)),Z)),dodeca3(X,X2)). % 2.03/2.24 0 [] dodeca4(X,nil2)=nil. % 2.03/2.24 0 [] dodeca4(X,cons2(Z,X2))=cons(pair2(add(suc(X),suc(Z)),add(add(suc(X),suc(X)),Z)),dodeca4(X,X2)). % 2.03/2.24 0 [] dodeca5(X,nil2)=nil. % 2.03/2.24 0 [] dodeca5(X,cons2(Z,X2))=cons(pair2(add(add(suc(X),suc(X)),Z),add(add(add(suc(X),suc(X)),suc(X)),Z)),dodeca5(X,X2)). % 2.03/2.24 0 [] dodeca6(X,nil2)=nil. % 2.03/2.24 0 [] dodeca6(X,cons2(Z,X2))=cons(pair2(add(add(add(suc(X),suc(X)),suc(X)),Z),add(add(add(suc(X),suc(X)),suc(X)),suc(Z))),dodeca6(X,X2)). % 2.03/2.24 0 [] dodeca7(zero)=nil. % 2.03/2.24 0 [] dodeca7(suc(Y))=append(cons(pair2(Y,zero),dodeca(enumFromToNat(zero,Y))),append(dodeca2(Y,enumFromToNat(zero,suc(Y))),append(dodeca3(Y,enumFromToNat(zero,suc(Y))),append(cons(pair2(suc(Y),add(add(suc(Y),suc(Y)),Y)),dodeca4(Y,enumFromToNat(zero,Y))),append(dodeca5(Y,enumFromToNat(zero,suc(Y))),cons(pair2(add(add(add(suc(Y),suc(Y)),suc(Y)),Y),add(add(add(suc(Y),suc(Y)),suc(Y)),zero)),dodeca6(Y,enumFromToNat(zero,Y)))))))). % 2.03/2.24 0 [] tour(nil2,nil)=btrue. % 2.03/2.24 0 [] tour(nil2,cons(Z,X2))=bfalse. % 2.03/2.24 0 [] tour(cons2(X3,X4),nil)=bfalse. % 2.03/2.24 0 [] tour(cons2(X3,X4),cons(pair2(U,V),Vs))=andb(e_q(X3,last(X3,X4)),andb(path2(cons2(X3,X4),cons(pair2(U,V),Vs)),andb(unique(X4),e_q(len(cons2(X3,X4)),add(two,maximum(maxNat(U,V),Vs)))))). % 2.03/2.24 0 [] prop_t3(X)=notb(tour(X,dodeca7(three))). % 2.03/2.24 0 [] e_q2(bfalse,btrue)=bfalse. % 2.03/2.24 0 [] e_q2(btrue,bfalse)=bfalse. % 2.03/2.24 0 [] e_q(suc(X),suc(Y))=e_q(X,Y). % 2.03/2.24 0 [] e_q(zero,suc(X))=bfalse. % 2.03/2.24 0 [] e_q(suc(X),zero)=bfalse. % 2.03/2.24 0 [] e_q(X,X)=btrue. % 2.03/2.24 0 [] e_q2(X,X)=btrue. % 2.03/2.24 0 [] e_q2(prop_t3(X),bfalse)!=btrue. % 2.03/2.24 end_of_list. % 2.03/2.24 % 2.03/2.24 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. % 2.03/2.24 % 2.03/2.24 All clauses are units, and equality is present; the % 2.03/2.24 strategy will be Knuth-Bendix with positive clauses in sos. % 2.03/2.24 % 2.03/2.24 dependent: set(knuth_bendix). % 2.03/2.24 dependent: set(anl_eq). % 2.03/2.24 dependent: set(para_from). % 2.03/2.24 dependent: set(para_into). % 2.03/2.24 dependent: clear(para_from_right). % 2.03/2.24 dependent: clear(para_into_right). % 2.03/2.24 dependent: set(para_from_vars). % 2.03/2.24 dependent: set(eq_units_both_ways). % 2.03/2.24 dependent: set(dynamic_demod_all). % 2.03/2.24 dependent: set(dynamic_demod). % 2.03/2.24 dependent: set(order_eq). % 2.03/2.24 dependent: set(back_demod). % 2.03/2.24 dependent: set(lrpo). % 2.03/2.24 % 2.03/2.24 ------------> process usable: % 2.03/2.24 ** KEPT (pick-wt=6): 1 [] e_q2(prop_t3(A),bfalse)!=btrue. % 2.03/2.24 % 2.03/2.24 ------------> process sos: % 2.03/2.24 ** KEPT (pick-wt=3): 2 [] A=A. % 2.03/2.24 ** KEPT (pick-wt=6): 3 [] aux(A,B,btrue)=B. % 2.03/2.24 ---> New Demodulator: 4 [new_demod,3] aux(A,B,btrue)=B. % 2.03/2.24 ** KEPT (pick-wt=6): 5 [] aux(A,B,bfalse)=A. % 2.03/2.24 ---> New Demodulator: 6 [new_demod,5] aux(A,B,bfalse)=A. % 2.03/2.24 ** KEPT (pick-wt=6): 7 [] aux2(A,B,btrue)=nil2. % 2.03/2.24 ---> New Demodulator: 8 [new_demod,7] aux2(A,B,btrue)=nil2. % 2.03/2.24 ** KEPT (pick-wt=11): 10 [copy,9,flip.1] cons2(A,enumFromToNat(suc(A),B))=aux2(A,B,bfalse). % 2.03/2.24 ---> New Demodulator: 11 [new_demod,10] cons2(A,enumFromToNat(suc(A),B))=aux2(A,B,bfalse). % 2.03/2.24 ** KEPT (pick-wt=6): 12 [] aux3(A,B,btrue)=bfalse. % 2.03/2.24 ---> New Demodulator: 13 [new_demod,12] aux3(A,B,btrue)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=7): 14 [] aux3(A,B,bfalse)=unique(B). % 2.03/2.24 ** KEPT (pick-wt=4): 15 [] predNat(zero)=zero. % 2.03/2.24 ---> New Demodulator: 16 [new_demod,15] predNat(zero)=zero. % 2.03/2.24 ** KEPT (pick-wt=5): 17 [] predNat(suc(A))=A. % 2.03/2.24 ---> New Demodulator: 18 [new_demod,17] predNat(suc(A))=A. % 2.03/2.24 ** KEPT (pick-wt=5): 19 [] orb(btrue,A)=btrue. % 2.03/2.24 ---> New Demodulator: 20 [new_demod,19] orb(btrue,A)=btrue. % 2.03/2.24 ** KEPT (pick-wt=5): 21 [] orb(bfalse,A)=A. % 2.03/2.24 ---> New Demodulator: 22 [new_demod,21] orb(bfalse,A)=A. % 2.03/2.24 ** KEPT (pick-wt=4): 23 [] or2(nil3)=bfalse. % 2.03/2.24 ---> New Demodulator: 24 [new_demod,23] or2(nil3)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=9): 25 [] or2(cons3(A,B))=orb(A,or2(B)). % 2.03/2.24 ---> New Demodulator: 26 [new_demod,25] or2(cons3(A,B))=orb(A,or2(B)). % 2.03/2.24 ** KEPT (pick-wt=4): 28 [copy,27,flip.1] suc(zero)=one. % 2.03/2.24 ---> New Demodulator: 29 [new_demod,28] suc(zero)=one. % 2.03/2.24 ** KEPT (pick-wt=4): 31 [copy,30,flip.1] suc(one)=two. % 2.03/2.24 ---> New Demodulator: 32 [new_demod,31] suc(one)=two. % 2.03/2.24 ** KEPT (pick-wt=4): 34 [copy,33,flip.1] suc(two)=three. % 2.03/2.24 ---> New Demodulator: 35 [new_demod,34] suc(two)=three. % 2.03/2.24 ** KEPT (pick-wt=4): 36 [] notb(btrue)=bfalse. % 2.03/2.24 ---> New Demodulator: 37 [new_demod,36] notb(btrue)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=4): 38 [] notb(bfalse)=btrue. % 2.03/2.24 ---> New Demodulator: 39 [new_demod,38] notb(bfalse)=btrue. % 2.03/2.24 ** KEPT (pick-wt=5): 40 [] lt(zero,zero)=bfalse. % 2.03/2.24 ---> New Demodulator: 41 [new_demod,40] lt(zero,zero)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=6): 42 [] lt(zero,suc(A))=btrue. % 2.03/2.24 ---> New Demodulator: 43 [new_demod,42] lt(zero,suc(A))=btrue. % 2.03/2.24 ** KEPT (pick-wt=6): 44 [] lt(suc(A),zero)=bfalse. % 2.03/2.24 ---> New Demodulator: 45 [new_demod,44] lt(suc(A),zero)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=9): 46 [] lt(suc(A),suc(B))=lt(A,B). % 2.03/2.24 ---> New Demodulator: 47 [new_demod,46] lt(suc(A),suc(B))=lt(A,B). % 2.03/2.24 ** KEPT (pick-wt=10): 48 [] maxNat(A,B)=aux(A,B,lt(A,B)). % 2.03/2.24 ---> New Demodulator: 49 [new_demod,48] maxNat(A,B)=aux(A,B,lt(A,B)). % 2.03/2.24 ** KEPT (pick-wt=5): 50 [] maximum(A,nil)=A. % 2.03/2.24 ---> New Demodulator: 51 [new_demod,50] maximum(A,nil)=A. % 2.03/2.24 ** KEPT (pick-wt=26): 53 [copy,52,demod,49,49] maximum(A,cons(pair2(B,C),D))=maximum(aux(A,aux(B,C,lt(B,C)),lt(A,aux(B,C,lt(B,C)))),D). % 2.03/2.24 ** KEPT (pick-wt=4): 54 [] len(nil2)=zero. % 2.03/2.24 ---> New Demodulator: 55 [new_demod,54] len(nil2)=zero. % 2.03/2.24 ** KEPT (pick-wt=8): 56 [] len(cons2(A,B))=suc(len(B)). % 2.03/2.24 ** KEPT (pick-wt=5): 57 [] last(A,nil2)=A. % 2.03/2.24 ---> New Demodulator: 58 [new_demod,57] last(A,nil2)=A. % 2.03/2.24 ** KEPT (pick-wt=9): 59 [] last(A,cons2(B,C))=last(B,C). % 2.03/2.24 ** KEPT (pick-wt=10): 61 [copy,60,flip.1] aux2(A,B,lt(B,A))=enumFromToNat(A,B). % 2.03/2.24 ---> New Demodulator: 62 [new_demod,61] aux2(A,B,lt(B,A))=enumFromToNat(A,B). % 2.03/2.24 ** KEPT (pick-wt=5): 63 [] elem(A,nil2)=bfalse. % 2.03/2.24 ---> New Demodulator: 64 [new_demod,63] elem(A,nil2)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=13): 66 [copy,65,flip.1] orb(e_q(A,B),elem(B,C))=elem(B,cons2(A,C)). % 2.03/2.24 ---> New Demodulator: 67 [new_demod,66] orb(e_q(A,B),elem(B,C))=elem(B,cons2(A,C)). % 2.03/2.24 ** KEPT (pick-wt=4): 68 [] unique(nil2)=btrue. % 2.03/2.24 ---> New Demodulator: 69 [new_demod,68] unique(nil2)=btrue. % 2.03/2.24 ** KEPT (pick-wt=11): 70 [] unique(cons2(A,B))=aux3(A,B,elem(A,B)). % 2.03/2.24 ---> New Demodulator: 71 [new_demod,70] unique(cons2(A,B))=aux3(A,B,elem(A,B)). % 2.03/2.24 ** KEPT (pick-wt=4): 72 [] dodeca(nil2)=nil. % 2.03/2.24 ---> New Demodulator: 73 [new_demod,72] dodeca(nil2)=nil. % 2.03/2.24 ** KEPT (pick-wt=12): 74 [] dodeca(cons2(A,B))=cons(pair2(A,suc(A)),dodeca(B)). % 2.03/2.24 ** KEPT (pick-wt=5): 75 [] append(nil,A)=A. % 2.03/2.24 ---> New Demodulator: 76 [new_demod,75] append(nil,A)=A. % 2.03/2.24 ** KEPT (pick-wt=11): 78 [copy,77,flip.1] cons(A,append(B,C))=append(cons(A,B),C). % 2.03/2.24 ---> New Demodulator: 79 [new_demod,78] cons(A,append(B,C))=append(cons(A,B),C). % 2.03/2.24 ** KEPT (pick-wt=5): 80 [] andb(btrue,A)=A. % 2.03/2.24 ---> New Demodulator: 81 [new_demod,80] andb(btrue,A)=A. % 2.03/2.24 ** KEPT (pick-wt=5): 82 [] andb(bfalse,A)=bfalse. % 2.03/2.24 ---> New Demodulator: 83 [new_demod,82] andb(bfalse,A)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=6): 84 [] path(A,B,nil)=nil3. % 2.03/2.24 ---> New Demodulator: 85 [new_demod,84] path(A,B,nil)=nil3. % 2.03/2.24 ** KEPT (pick-wt=29): 86 [] path(A,B,cons(pair2(C,D),E))=cons3(orb(andb(e_q(C,A),e_q(D,B)),andb(e_q(C,B),e_q(D,A))),path(A,B,E)). % 2.03/2.24 ** KEPT (pick-wt=5): 87 [] path2(nil2,A)=btrue. % 2.03/2.24 ---> New Demodulator: 88 [new_demod,87] path2(nil2,A)=btrue. % 2.03/2.24 ** KEPT (pick-wt=7): 89 [] path2(cons2(A,nil2),B)=btrue. % 2.03/2.24 ---> New Demodulator: 90 [new_demod,89] path2(cons2(A,nil2),B)=btrue. % 2.03/2.24 ** KEPT (pick-wt=19): 91 [] path2(cons2(A,cons2(B,C)),D)=andb(or2(path(A,B,D)),path2(cons2(B,C),D)). % 2.03/2.24 ** KEPT (pick-wt=5): 92 [] add(zero,A)=A. % 2.03/2.24 ---> New Demodulator: 93 [new_demod,92] add(zero,A)=A. % 2.03/2.24 ** KEPT (pick-wt=9): 95 [copy,94,flip.1] suc(add(A,B))=add(suc(A),B). % 2.03/2.24 ---> New Demodulator: 96 [new_demod,95] suc(add(A,B))=add(suc(A),B). % 2.03/2.24 ** KEPT (pick-wt=5): 97 [] dodeca2(A,nil2)=nil. % 2.03/2.24 ---> New Demodulator: 98 [new_demod,97] dodeca2(A,nil2)=nil. % 2.03/2.24 ** KEPT (pick-wt=16): 99 [] dodeca2(A,cons2(B,C))=cons(pair2(B,add(suc(A),B)),dodeca2(A,C)). % 2.03/2.24 ** KEPT (pick-wt=5): 100 [] dodeca3(A,nil2)=nil. % 2.03/2.24 ---> New Demodulator: 101 [new_demod,100] dodeca3(A,nil2)=nil. % 2.03/2.24 ** KEPT (pick-wt=22): 102 [] dodeca3(A,cons2(B,C))=cons(pair2(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C)). % 2.03/2.24 ** KEPT (pick-wt=5): 103 [] dodeca4(A,nil2)=nil. % 2.03/2.24 ---> New Demodulator: 104 [new_demod,103] dodeca4(A,nil2)=nil. % 2.03/2.24 ** KEPT (pick-wt=23): 105 [] dodeca4(A,cons2(B,C))=cons(pair2(add(suc(A),suc(B)),add(add(suc(A),suc(A)),B)),dodeca4(A,C)). % 2.03/2.24 ** KEPT (pick-wt=5): 106 [] dodeca5(A,nil2)=nil. % 2.03/2.24 ---> New Demodulator: 107 [new_demod,106] dodeca5(A,nil2)=nil. % 2.03/2.24 ** KEPT (pick-wt=28): 108 [] dodeca5(A,cons2(B,C))=cons(pair2(add(add(suc(A),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),B)),dodeca5(A,C)). % 2.03/2.24 ** KEPT (pick-wt=5): 109 [] dodeca6(A,nil2)=nil. % 2.03/2.24 ---> New Demodulator: 110 [new_demod,109] dodeca6(A,nil2)=nil. % 2.03/2.24 ** KEPT (pick-wt=32): 111 [] dodeca6(A,cons2(B,C))=cons(pair2(add(add(add(suc(A),suc(A)),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),suc(B))),dodeca6(A,C)). % 2.03/2.24 ** KEPT (pick-wt=4): 112 [] dodeca7(zero)=nil. % 2.03/2.24 ---> New Demodulator: 113 [new_demod,112] dodeca7(zero)=nil. % 2.03/2.24 ** KEPT (pick-wt=78): 114 [] dodeca7(suc(A))=append(cons(pair2(A,zero),dodeca(enumFromToNat(zero,A))),append(dodeca2(A,enumFromToNat(zero,suc(A))),append(dodeca3(A,enumFromToNat(zero,suc(A))),append(cons(pair2(suc(A),add(add(suc(A),suc(A)),A)),dodeca4(A,enumFromToNat(zero,A))),append(dodeca5(A,enumFromToNat(zero,suc(A))),cons(pair2(add(add(add(suc(A),suc(A)),suc(A)),A),add(add(add(suc(A),suc(A)),suc(A)),zero)),dodeca6(A,enumFromToNat(zero,A)))))))). % 2.03/2.24 ---> New Demodulator: 115 [new_demod,114] dodeca7(suc(A))=append(cons(pair2(A,zero),dodeca(enumFromToNat(zero,A))),append(dodeca2(A,enumFromToNat(zero,suc(A))),append(dodeca3(A,enumFromToNat(zero,suc(A))),append(cons(pair2(suc(A),add(add(suc(A),suc(A)),A)),dodeca4(A,enumFromToNat(zero,A))),append(dodeca5(A,enumFromToNat(zero,suc(A))),cons(pair2(add(add(add(suc(A),suc(A)),suc(A)),A),add(add(add(suc(A),suc(A)),suc(A)),zero)),dodeca6(A,enumFromToNat(zero,A)))))))). % 2.03/2.24 ** KEPT (pick-wt=5): 116 [] tour(nil2,nil)=btrue. % 2.03/2.24 ---> New Demodulator: 117 [new_demod,116] tour(nil2,nil)=btrue. % 2.03/2.24 ** KEPT (pick-wt=7): 118 [] tour(nil2,cons(A,B))=bfalse. % 2.03/2.24 ---> New Demodulator: 119 [new_demod,118] tour(nil2,cons(A,B))=bfalse. % 2.03/2.24 ** KEPT (pick-wt=7): 120 [] tour(cons2(A,B),nil)=bfalse. % 2.03/2.24 ---> New Demodulator: 121 [new_demod,120] tour(cons2(A,B),nil)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=44): 123 [copy,122,demod,49] tour(cons2(A,B),cons(pair2(C,D),E))=andb(e_q(A,last(A,B)),andb(path2(cons2(A,B),cons(pair2(C,D),E)),andb(unique(B),e_q(len(cons2(A,B)),add(two,maximum(aux(C,D,lt(C,D)),E)))))). % 2.03/2.24 ** KEPT (pick-wt=8): 124 [] prop_t3(A)=notb(tour(A,dodeca7(three))). % 2.03/2.24 ---> New Demodulator: 125 [new_demod,124] prop_t3(A)=notb(tour(A,dodeca7(three))). % 2.03/2.24 ** KEPT (pick-wt=5): 126 [] e_q2(bfalse,btrue)=bfalse. % 2.03/2.24 ---> New Demodulator: 127 [new_demod,126] e_q2(bfalse,btrue)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=5): 128 [] e_q2(btrue,bfalse)=bfalse. % 2.03/2.24 ---> New Demodulator: 129 [new_demod,128] e_q2(btrue,bfalse)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=9): 130 [] e_q(suc(A),suc(B))=e_q(A,B). % 2.03/2.24 ---> New Demodulator: 131 [new_demod,130] e_q(suc(A),suc(B))=e_q(A,B). % 2.03/2.24 ** KEPT (pick-wt=6): 132 [] e_q(zero,suc(A))=bfalse. % 2.03/2.24 ---> New Demodulator: 133 [new_demod,132] e_q(zero,suc(A))=bfalse. % 2.03/2.24 ** KEPT (pick-wt=6): 134 [] e_q(suc(A),zero)=bfalse. % 2.03/2.24 ---> New Demodulator: 135 [new_demod,134] e_q(suc(A),zero)=bfalse. % 2.03/2.24 ** KEPT (pick-wt=5): 136 [] e_q(A,A)=btrue. % 2.03/2.24 ---> New Demodulator: 137 [new_demod,136] e_q(A,A)=btrue. % 2.03/2.24 ** KEPT (pick-wt=5): 138 [] e_q2(A,A)=btrue. % 2.03/2.24 ---> New Demodulator: 139 [new_demod,138] e_q2(A,A)=btrue. % 2.03/2.24 Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] A=A. % 2.03/2.24 >>>> Starting back demodulation with 4. % 2.03/2.24 >>>> Starting back demodulation with 6. % 2.03/2.24 >>>> Starting back demodulation with 8. % 2.03/2.24 >>>> Starting back demodulation with 11. % 2.03/2.24 >>>> Starting back demodulation with 13. % 2.03/2.24 ** KEPT (pick-wt=7): 140 [copy,14,flip.1] unique(A)=aux3(B,A,bfalse). % 2.03/2.24 >>>> Starting back demodulation with 16. % 2.03/2.24 >>>> Starting back demodulation with 18. % 2.03/2.24 >>>> Starting back demodulation with 20. % 2.03/2.24 >>>> Starting back demodulation with 22. % 2.03/2.24 >>>> Starting back demodulation with 24. % 2.03/2.24 >>>> Starting back demodulation with 26. % 2.03/2.24 >>>> Starting back demodulation with 29. % 2.03/2.24 >>>> Starting back demodulation with 32. % 2.03/2.24 >>>> Starting back demodulation with 35. % 2.03/2.24 >>>> Starting back demodulation with 37. % 2.03/2.24 >>>> Starting back demodulation with 39. % 2.03/2.24 >>>> Starting back demodulation with 41. % 2.03/2.24 >>>> Starting back demodulation with 43. % 2.03/2.24 >>>> Starting back demodulation with 45. % 2.03/2.24 >>>> Starting back demodulation with 47. % 2.03/2.24 >>>> Starting back demodulation with 49. % 2.03/2.24 >>>> Starting back demodulation with 51. % 2.03/2.24 ** KEPT (pick-wt=26): 141 [copy,53,flip.1] maximum(aux(A,aux(B,C,lt(B,C)),lt(A,aux(B,C,lt(B,C)))),D)=maximum(A,cons(pair2(B,C),D)). % 2.03/2.24 >>>> Starting back demodulation with 55. % 2.03/2.24 ** KEPT (pick-wt=8): 142 [copy,56,flip.1] suc(len(A))=len(cons2(B,A)). % 2.03/2.24 >>>> Starting back demodulation with 58. % 2.03/2.24 ** KEPT (pick-wt=9): 143 [copy,59,flip.1] last(A,B)=last(C,cons2(A,B)). % 2.03/2.24 >>>> Starting back demodulation with 62. % 2.03/2.24 >>>> Starting back demodulation with 64. % 2.03/2.24 >>>> Starting back demodulation with 67. % 2.03/2.24 >>>> Starting back demodulation with 69. % 2.03/2.24 >>>> Starting back demodulation with 71. % 2.03/2.24 >>>> Starting back demodulation with 73. % 2.03/2.24 ** KEPT (pick-wt=12): 144 [copy,74,flip.1] cons(pair2(A,suc(A)),dodeca(B))=dodeca(cons2(A,B)). % 2.03/2.24 >>>> Starting back demodulation with 76. % 2.03/2.24 >>>> Starting back demodulation with 79. % 2.03/2.24 >>>> Starting back demodulation with 81. % 2.03/2.24 >>>> Starting back demodulation with 83. % 2.03/2.24 >>>> Starting back demodulation with 85. % 2.03/2.24 ** KEPT (pick-wt=29): 145 [copy,86,flip.1] cons3(orb(andb(e_q(A,B),e_q(C,D)),andb(e_q(A,D),e_q(C,B))),path(B,D,E))=path(B,D,cons(pair2(A,C),E)). % 2.03/2.24 >>>> Starting back demodulation with 88. % 2.03/2.24 >>>> Starting back demodulation with 90. % 2.03/2.24 ** KEPT (pick-wt=19): 146 [copy,91,flip.1] andb(or2(path(A,B,C)),path2(cons2(B,D),C))=path2(cons2(A,cons2(B,D)),C). % 2.03/2.24 >>>> Starting back demodulation with 93. % 2.03/2.24 >>>> Starting back demodulation with 96. % 2.03/2.24 >>>> Starting back demodulation with 98. % 2.03/2.24 ** KEPT (pick-wt=16): 147 [copy,99,flip.1] cons(pair2(A,add(suc(B),A)),dodeca2(B,C))=dodeca2(B,cons2(A,C)). % 2.03/2.24 >>>> Starting back demodulation with 101. % 2.03/2.24 ** KEPT (pick-wt=22): 148 [copy,102,flip.1] cons(pair2(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C))=dodeca3(A,cons2(B,C)). % 2.03/2.24 >>>> Starting back demodulation with 104. % 2.03/2.24 ** KEPT (pick-wt=23): 149 [copy,105,flip.1] cons(pair2(add(suc(A),suc(B)),add(add(suc(A),suc(A)),B)),dodeca4(A,C))=dodeca4(A,cons2(B,C)). % 2.03/2.25 >>>> Starting back demodulation with 107. % 2.03/2.25 ** KEPT (pick-wt=28): 150 [copy,108,flip.1] cons(pair2(add(add(suc(A),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),B)),dodeca5(A,C))=dodeca5(A,cons2(B,C)). % 2.03/2.25 >>>> Starting back demodulation with 110. % 2.03/2.25 ** KEPT (pick-wt=32): 151 [copy,111,flip.1] cons(pair2(add(add(add(suc(A),suc(A)),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),suc(B))),dodeca6(A,C))=dodeca6(A,cons2(B,C)). % 2.03/2.25 >>>> Starting back demodulation with 113. % 2.03/2.25 >>>> Starting back demodulation with 115. % 2.03/2.25 >>>> Starting back demodulation with 117. % 2.03/2.25 >>>> Starting back demodulation with 119. % 2.03/2.25 >>>> Starting back demodulation with 121. % 2.03/2.25 ** KEPT (pick-wt=44): 152 [copy,123,flip.1] andb(e_q(A,last(A,B)),andb(path2(cons2(A,B),cons(pair2(C,D),E)),andb(unique(B),e_q(len(cons2(A,B)),add(two,maximum(aux(C,D,lt(C,D)),E))))))=tour(cons2(A,B),cons(pair2(C,D),E)). % 2.03/2.25 >>>> Starting back demodulation with 125. % 2.03/2.25 >> back demodulating 1 with 125. % 2.03/2.25 >>>> Starting back demodulation with 127. % 2.03/2.25 >>>> Starting back demodulation with 129. % 2.03/2.25 >>>> Starting back demodulation with 131. % 2.03/2.25 >>>> Starting back demodulation with 133. % 2.03/2.25 >>>> Starting back demodulation with 135. % 2.03/2.25 >>>> Starting back demodulation with 137. % 2.03/2.25 >>>> Starting back demodulation with 139. % 2.03/2.25 Following clause subsumed by 14 during input processing: 0 [copy,140,flip.1] aux3(A,B,bfalse)=unique(B). % 2.03/2.25 Following clause subsumed by 53 during input processing: 0 [copy,141,flip.1] maximum(A,cons(pair2(B,C),D))=maximum(aux(A,aux(B,C,lt(B,C)),lt(A,aux(B,C,lt(B,C)))),D). % 2.03/2.25 Following clause subsumed by 56 during input processing: 0 [copy,142,flip.1] len(cons2(A,B))=suc(len(B)). % 2.03/2.25 Following clause subsumed by 59 during input processing: 0 [copy,143,flip.1] last(A,cons2(B,C))=last(B,C). % 2.03/2.25 Following clause subsumed by 74 during input processing: 0 [copy,144,flip.1] dodeca(cons2(A,B))=cons(pair2(A,suc(A)),dodeca(B)). % 2.03/2.25 Following clause subsumed by 86 during input processing: 0 [copy,145,flip.1] path(A,B,cons(pair2(C,D),E))=cons3(orb(andb(e_q(C,A),e_q(D,B)),andb(e_q(C,B),e_q(D,A))),path(A,B,E)). % 2.03/2.25 Following clause subsumed by 91 during input processing: 0 [copy,146,flip.1] path2(cons2(A,cons2(B,C)),D)=andb(or2(path(A,B,D)),path2(cons2(B,C),D)). % 2.03/2.25 Following clause subsumed by 99 during input processing: 0 [copy,147,flip.1] dodeca2(A,cons2(B,C))=cons(pair2(B,add(suc(A),B)),dodeca2(A,C)). % 2.03/2.25 Following clause subsumed by 102 during input processing: 0 [copy,148,flip.1] dodeca3(A,cons2(B,C))=cons(pair2(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C)). % 2.03/2.25 Following clause subsumed by 105 during input processing: 0 [copy,149,flip.1] dodeca4(A,cons2(B,C))=cons(pair2(add(suc(A),suc(B)),add(add(suc(A),suc(A)),B)),dodeca4(A,C)). % 2.03/2.25 Following clause subsumed by 108 during input processing: 0 [copy,150,flip.1] dodeca5(A,cons2(B,C))=cons(pair2(add(add(suc(A),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),B)),dodeca5(A,C)). % 2.03/2.25 Following clause subsumed by 111 during input processing: 0 [copy,151,flip.1] dodeca6(A,cons2(B,C))=cons(pair2(add(add(add(suc(A),suc(A)),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),suc(B))),dodeca6(A,C)). % 2.03/2.25 Following clause subsumed by 123 during input processing: 0 [copy,152,flip.1] tour(cons2(A,B),cons(pair2(C,D),E))=andb(e_q(A,last(A,B)),andb(path2(cons2(A,B),cons(pair2(C,D),E)),andb(unique(B),e_q(len(cons2(A,B)),add(two,maximum(aux(C,D,lt(C,D)),E)))))). % 2.03/2.25 % 2.03/2.25 ======= end of input processing ======= % 2.03/2.25 % 2.03/2.25 =========== start of search =========== % 2.03/2.25 % 2.03/2.25 % 2.03/2.25 Resetting weight limit to 8. % 2.03/2.25 % 2.03/2.25 % 2.03/2.25 Resetting weight limit to 8. % 2.03/2.25 % 2.03/2.25 sos_size=53 % 2.03/2.25 % 2.03/2.25 % 2.03/2.25 Resetting weight limit to 7. % 2.03/2.25 % 2.03/2.25 % 2.03/2.25 Resetting weight limit to 7. % 2.03/2.25 % 2.03/2.25 sos_size=40 % 2.03/2.25 % 2.03/2.25 Search stopped because sos empty. % 2.03/2.25 % 2.03/2.25 % 2.03/2.25 Search stopped because sos empty. % 2.03/2.25 % 2.03/2.25 ============ end of search ============ % 2.03/2.25 % 2.03/2.25 -------------- statistics ------------- % 2.03/2.25 clauses given 155 % 2.03/2.25 clauses generated 705 % 2.03/2.25 clauses kept 177 % 2.03/2.25 clauses forward subsumed 326 % 2.03/2.25 clauses back subsumed 0 % 2.03/2.25 Kbytes malloced 5859 % 2.03/2.25 % 2.03/2.25 ----------- times (seconds) ----------- % 2.03/2.25 user CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.03/2.25 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 2.03/2.25 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.03/2.25 % 2.03/2.25 Process 30463 finished Tue May 5 13:05:01 2026 % 2.03/2.25 Otter interrupted % 2.03/2.25 PROOF NOT FOUND %------------------------------------------------------------------------------