%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX230-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n014.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.04s 2.21s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX230-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.16/0.34 % Computer : n014.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue May 5 13:00:06 EDT 2026 % 0.16/0.34 % CPUTime : % 1.99/2.19 ----- Otter 3.3f, August 2004 ----- % 1.99/2.19 The process was started by sandbox2 on n014.cluster.edu, % 1.99/2.19 Tue May 5 13:00:06 2026 % 1.99/2.19 The command was "./otter". The process ID is 6074. % 1.99/2.19 % 1.99/2.19 set(prolog_style_variables). % 1.99/2.19 set(auto). % 1.99/2.19 dependent: set(auto1). % 1.99/2.19 dependent: set(process_input). % 1.99/2.19 dependent: clear(print_kept). % 1.99/2.19 dependent: clear(print_new_demod). % 1.99/2.19 dependent: clear(print_back_demod). % 1.99/2.19 dependent: clear(print_back_sub). % 1.99/2.19 dependent: set(control_memory). % 1.99/2.19 dependent: assign(max_mem, 12000). % 1.99/2.19 dependent: assign(pick_given_ratio, 4). % 1.99/2.19 dependent: assign(stats_level, 1). % 1.99/2.19 dependent: assign(max_seconds, 10800). % 1.99/2.19 clear(print_given). % 1.99/2.19 % 1.99/2.19 list(usable). % 1.99/2.19 0 [] A=A. % 1.99/2.19 0 [] aux(X,Y,btrue)=nil2. % 1.99/2.19 0 [] aux(X,Y,bfalse)=cons2(X,enumFromToNat(suc(X),Y)). % 1.99/2.19 0 [] aux2(A,Z,V,C1,nothing)=cons3(bfalse,colouring(A,Z)). % 1.99/2.19 0 [] aux2(A,Z,V,C1,just(C2))=cons3(notb(e_q(C1,C2)),colouring(A,Z)). % 1.99/2.19 0 [] aux3(A,Z,U,V,nothing)=cons3(bfalse,colouring(A,Z)). % 1.99/2.19 0 [] aux3(A,Z,U,V,just(C1))=aux2(A,Z,V,C1,index(A,V)). % 1.99/2.19 0 [] predNat(zero)=zero. % 1.99/2.19 0 [] predNat(suc(Y))=Y. % 1.99/2.19 0 [] one=suc(zero). % 1.99/2.19 0 [] two=suc(one). % 1.99/2.19 0 [] three=suc(two). % 1.99/2.19 0 [] notb(btrue)=bfalse. % 1.99/2.19 0 [] notb(bfalse)=btrue. % 1.99/2.19 0 [] lt(zero,zero)=bfalse. % 1.99/2.19 0 [] lt(zero,suc(Z))=btrue. % 1.99/2.19 0 [] lt(suc(X2),zero)=bfalse. % 1.99/2.19 0 [] lt(suc(X2),suc(Y2))=lt(X2,Y2). % 1.99/2.19 0 [] prop_d5(nil2)=nil3. % 1.99/2.19 0 [] prop_d5(cons2(Y,Z))=cons3(lt(Y,three),prop_d5(Z)). % 1.99/2.19 0 [] index(nil2,Y)=nothing. % 1.99/2.19 0 [] index(cons2(Z,X2),zero)=just(Z). % 1.99/2.19 0 [] index(cons2(Z,X2),suc(N))=index(X2,N). % 1.99/2.19 0 [] four=suc(three). % 1.99/2.19 0 [] five=suc(four). % 1.99/2.19 0 [] enumFromToNat(X,Y)=aux(X,Y,lt(Y,X)). % 1.99/2.19 0 [] dodeca(nil2)=nil. % 1.99/2.19 0 [] dodeca(cons2(Y,Z))=cons(pair2(Y,suc(Y)),dodeca(Z)). % 1.99/2.19 0 [] colouring(A,nil)=nil3. % 1.99/2.19 0 [] colouring(A,cons(pair2(U,V),Z))=aux3(A,Z,U,V,index(A,U)). % 1.99/2.19 0 [] append(nil,Y)=Y. % 1.99/2.19 0 [] append(cons(Z,Xs),Y)=cons(Z,append(Xs,Y)). % 1.99/2.19 0 [] andb(btrue,Q)=Q. % 1.99/2.19 0 [] andb(bfalse,Q)=bfalse. % 1.99/2.19 0 [] and2(nil3)=btrue. % 1.99/2.19 0 [] and2(cons3(Y,Xs))=andb(Y,and2(Xs)). % 1.99/2.19 0 [] colouring2(X,Y)=and2(colouring(Y,X)). % 1.99/2.19 0 [] add(zero,Y)=Y. % 1.99/2.19 0 [] add(suc(Z),Y)=suc(add(Z,Y)). % 1.99/2.19 0 [] dodeca2(X,nil2)=nil. % 1.99/2.19 0 [] dodeca2(X,cons2(Z,X2))=cons(pair2(Z,add(suc(X),Z)),dodeca2(X,X2)). % 1.99/2.19 0 [] dodeca3(X,nil2)=nil. % 1.99/2.19 0 [] dodeca3(X,cons2(Z,X2))=cons(pair2(add(suc(X),Z),add(add(suc(X),suc(X)),Z)),dodeca3(X,X2)). % 1.99/2.19 0 [] dodeca4(X,nil2)=nil. % 1.99/2.19 0 [] dodeca4(X,cons2(Z,X2))=cons(pair2(add(suc(X),suc(Z)),add(add(suc(X),suc(X)),Z)),dodeca4(X,X2)). % 1.99/2.19 0 [] dodeca5(X,nil2)=nil. % 1.99/2.19 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)). % 1.99/2.19 0 [] dodeca6(X,nil2)=nil. % 1.99/2.19 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)). % 1.99/2.19 0 [] dodeca7(zero)=nil. % 1.99/2.19 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)))))))). % 1.99/2.19 0 [] prop_d52(X)=notb(andb(colouring2(dodeca7(five),X),and2(prop_d5(X)))). % 1.99/2.19 0 [] e_q2(bfalse,btrue)=bfalse. % 1.99/2.19 0 [] e_q2(btrue,bfalse)=bfalse. % 1.99/2.19 0 [] e_q(suc(X),suc(Y))=e_q(X,Y). % 1.99/2.19 0 [] e_q(zero,suc(X))=bfalse. % 1.99/2.19 0 [] e_q(suc(X),zero)=bfalse. % 1.99/2.19 0 [] e_q(X,X)=btrue. % 1.99/2.19 0 [] e_q2(X,X)=btrue. % 1.99/2.19 0 [] e_q2(prop_d52(X),bfalse)!=btrue. % 1.99/2.19 end_of_list. % 1.99/2.19 % 1.99/2.19 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. % 1.99/2.19 % 1.99/2.19 All clauses are units, and equality is present; the % 1.99/2.19 strategy will be Knuth-Bendix with positive clauses in sos. % 1.99/2.19 % 1.99/2.19 dependent: set(knuth_bendix). % 1.99/2.19 dependent: set(anl_eq). % 1.99/2.19 dependent: set(para_from). % 1.99/2.19 dependent: set(para_into). % 1.99/2.19 dependent: clear(para_from_right). % 1.99/2.19 dependent: clear(para_into_right). % 1.99/2.19 dependent: set(para_from_vars). % 1.99/2.19 dependent: set(eq_units_both_ways). % 1.99/2.19 dependent: set(dynamic_demod_all). % 1.99/2.19 dependent: set(dynamic_demod). % 1.99/2.19 dependent: set(order_eq). % 1.99/2.19 dependent: set(back_demod). % 1.99/2.19 dependent: set(lrpo). % 1.99/2.19 % 1.99/2.19 ------------> process usable: % 1.99/2.19 ** KEPT (pick-wt=6): 1 [] e_q2(prop_d52(A),bfalse)!=btrue. % 1.99/2.19 % 1.99/2.19 ------------> process sos: % 1.99/2.19 ** KEPT (pick-wt=3): 2 [] A=A. % 1.99/2.19 ** KEPT (pick-wt=6): 3 [] aux(A,B,btrue)=nil2. % 1.99/2.19 ---> New Demodulator: 4 [new_demod,3] aux(A,B,btrue)=nil2. % 1.99/2.19 ** KEPT (pick-wt=11): 6 [copy,5,flip.1] cons2(A,enumFromToNat(suc(A),B))=aux(A,B,bfalse). % 1.99/2.19 ---> New Demodulator: 7 [new_demod,6] cons2(A,enumFromToNat(suc(A),B))=aux(A,B,bfalse). % 1.99/2.19 ** KEPT (pick-wt=12): 8 [] aux2(A,B,C,D,nothing)=cons3(bfalse,colouring(A,B)). % 1.99/2.19 ** KEPT (pick-wt=16): 9 [] aux2(A,B,C,D,just(E))=cons3(notb(e_q(D,E)),colouring(A,B)). % 1.99/2.19 ** KEPT (pick-wt=12): 10 [] aux3(A,B,C,D,nothing)=cons3(bfalse,colouring(A,B)). % 1.99/2.19 ** KEPT (pick-wt=16): 11 [] aux3(A,B,C,D,just(E))=aux2(A,B,D,E,index(A,D)). % 1.99/2.19 ** KEPT (pick-wt=4): 12 [] predNat(zero)=zero. % 1.99/2.19 ---> New Demodulator: 13 [new_demod,12] predNat(zero)=zero. % 1.99/2.19 ** KEPT (pick-wt=5): 14 [] predNat(suc(A))=A. % 1.99/2.19 ---> New Demodulator: 15 [new_demod,14] predNat(suc(A))=A. % 1.99/2.19 ** KEPT (pick-wt=4): 17 [copy,16,flip.1] suc(zero)=one. % 1.99/2.19 ---> New Demodulator: 18 [new_demod,17] suc(zero)=one. % 1.99/2.19 ** KEPT (pick-wt=4): 20 [copy,19,flip.1] suc(one)=two. % 1.99/2.19 ---> New Demodulator: 21 [new_demod,20] suc(one)=two. % 1.99/2.19 ** KEPT (pick-wt=4): 23 [copy,22,flip.1] suc(two)=three. % 1.99/2.19 ---> New Demodulator: 24 [new_demod,23] suc(two)=three. % 1.99/2.19 ** KEPT (pick-wt=4): 25 [] notb(btrue)=bfalse. % 1.99/2.19 ---> New Demodulator: 26 [new_demod,25] notb(btrue)=bfalse. % 1.99/2.19 ** KEPT (pick-wt=4): 27 [] notb(bfalse)=btrue. % 1.99/2.19 ---> New Demodulator: 28 [new_demod,27] notb(bfalse)=btrue. % 1.99/2.19 ** KEPT (pick-wt=5): 29 [] lt(zero,zero)=bfalse. % 1.99/2.19 ---> New Demodulator: 30 [new_demod,29] lt(zero,zero)=bfalse. % 1.99/2.19 ** KEPT (pick-wt=6): 31 [] lt(zero,suc(A))=btrue. % 1.99/2.19 ---> New Demodulator: 32 [new_demod,31] lt(zero,suc(A))=btrue. % 1.99/2.19 ** KEPT (pick-wt=6): 33 [] lt(suc(A),zero)=bfalse. % 1.99/2.19 ---> New Demodulator: 34 [new_demod,33] lt(suc(A),zero)=bfalse. % 1.99/2.19 ** KEPT (pick-wt=9): 35 [] lt(suc(A),suc(B))=lt(A,B). % 1.99/2.19 ---> New Demodulator: 36 [new_demod,35] lt(suc(A),suc(B))=lt(A,B). % 1.99/2.19 ** KEPT (pick-wt=4): 37 [] prop_d5(nil2)=nil3. % 1.99/2.19 ---> New Demodulator: 38 [new_demod,37] prop_d5(nil2)=nil3. % 1.99/2.19 ** KEPT (pick-wt=11): 39 [] prop_d5(cons2(A,B))=cons3(lt(A,three),prop_d5(B)). % 1.99/2.19 ---> New Demodulator: 40 [new_demod,39] prop_d5(cons2(A,B))=cons3(lt(A,three),prop_d5(B)). % 1.99/2.19 ** KEPT (pick-wt=5): 41 [] index(nil2,A)=nothing. % 1.99/2.19 ---> New Demodulator: 42 [new_demod,41] index(nil2,A)=nothing. % 1.99/2.19 ** KEPT (pick-wt=8): 43 [] index(cons2(A,B),zero)=just(A). % 1.99/2.19 ** KEPT (pick-wt=10): 44 [] index(cons2(A,B),suc(C))=index(B,C). % 1.99/2.19 ---> New Demodulator: 45 [new_demod,44] index(cons2(A,B),suc(C))=index(B,C). % 1.99/2.19 ** KEPT (pick-wt=4): 47 [copy,46,flip.1] suc(three)=four. % 1.99/2.19 ---> New Demodulator: 48 [new_demod,47] suc(three)=four. % 1.99/2.19 ** KEPT (pick-wt=4): 50 [copy,49,flip.1] suc(four)=five. % 1.99/2.19 ---> New Demodulator: 51 [new_demod,50] suc(four)=five. % 1.99/2.19 ** KEPT (pick-wt=10): 53 [copy,52,flip.1] aux(A,B,lt(B,A))=enumFromToNat(A,B). % 1.99/2.19 ---> New Demodulator: 54 [new_demod,53] aux(A,B,lt(B,A))=enumFromToNat(A,B). % 1.99/2.19 ** KEPT (pick-wt=4): 55 [] dodeca(nil2)=nil. % 1.99/2.19 ---> New Demodulator: 56 [new_demod,55] dodeca(nil2)=nil. % 1.99/2.19 ** KEPT (pick-wt=12): 57 [] dodeca(cons2(A,B))=cons(pair2(A,suc(A)),dodeca(B)). % 1.99/2.19 ** KEPT (pick-wt=5): 58 [] colouring(A,nil)=nil3. % 1.99/2.19 ---> New Demodulator: 59 [new_demod,58] colouring(A,nil)=nil3. % 1.99/2.19 ** KEPT (pick-wt=16): 60 [] colouring(A,cons(pair2(B,C),D))=aux3(A,D,B,C,index(A,B)). % 1.99/2.19 ** KEPT (pick-wt=5): 61 [] append(nil,A)=A. % 1.99/2.19 ---> New Demodulator: 62 [new_demod,61] append(nil,A)=A. % 1.99/2.19 ** KEPT (pick-wt=11): 64 [copy,63,flip.1] cons(A,append(B,C))=append(cons(A,B),C). % 1.99/2.19 ---> New Demodulator: 65 [new_demod,64] cons(A,append(B,C))=append(cons(A,B),C). % 1.99/2.19 ** KEPT (pick-wt=5): 66 [] andb(btrue,A)=A. % 1.99/2.19 ---> New Demodulator: 67 [new_demod,66] andb(btrue,A)=A. % 1.99/2.19 ** KEPT (pick-wt=5): 68 [] andb(bfalse,A)=bfalse. % 1.99/2.19 ---> New Demodulator: 69 [new_demod,68] andb(bfalse,A)=bfalse. % 1.99/2.19 ** KEPT (pick-wt=4): 70 [] and2(nil3)=btrue. % 1.99/2.19 ---> New Demodulator: 71 [new_demod,70] and2(nil3)=btrue. % 1.99/2.19 ** KEPT (pick-wt=9): 72 [] and2(cons3(A,B))=andb(A,and2(B)). % 1.99/2.19 ---> New Demodulator: 73 [new_demod,72] and2(cons3(A,B))=andb(A,and2(B)). % 1.99/2.19 ** KEPT (pick-wt=8): 75 [copy,74,flip.1] and2(colouring(A,B))=colouring2(B,A). % 1.99/2.19 ---> New Demodulator: 76 [new_demod,75] and2(colouring(A,B))=colouring2(B,A). % 1.99/2.19 ** KEPT (pick-wt=5): 77 [] add(zero,A)=A. % 1.99/2.19 ---> New Demodulator: 78 [new_demod,77] add(zero,A)=A. % 1.99/2.19 ** KEPT (pick-wt=9): 80 [copy,79,flip.1] suc(add(A,B))=add(suc(A),B). % 1.99/2.19 ---> New Demodulator: 81 [new_demod,80] suc(add(A,B))=add(suc(A),B). % 1.99/2.19 ** KEPT (pick-wt=5): 82 [] dodeca2(A,nil2)=nil. % 1.99/2.19 ---> New Demodulator: 83 [new_demod,82] dodeca2(A,nil2)=nil. % 1.99/2.19 ** KEPT (pick-wt=16): 84 [] dodeca2(A,cons2(B,C))=cons(pair2(B,add(suc(A),B)),dodeca2(A,C)). % 1.99/2.19 ** KEPT (pick-wt=5): 85 [] dodeca3(A,nil2)=nil. % 1.99/2.19 ---> New Demodulator: 86 [new_demod,85] dodeca3(A,nil2)=nil. % 1.99/2.19 ** KEPT (pick-wt=22): 87 [] dodeca3(A,cons2(B,C))=cons(pair2(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C)). % 1.99/2.19 ** KEPT (pick-wt=5): 88 [] dodeca4(A,nil2)=nil. % 1.99/2.19 ---> New Demodulator: 89 [new_demod,88] dodeca4(A,nil2)=nil. % 1.99/2.19 ** KEPT (pick-wt=23): 90 [] dodeca4(A,cons2(B,C))=cons(pair2(add(suc(A),suc(B)),add(add(suc(A),suc(A)),B)),dodeca4(A,C)). % 1.99/2.19 ** KEPT (pick-wt=5): 91 [] dodeca5(A,nil2)=nil. % 1.99/2.19 ---> New Demodulator: 92 [new_demod,91] dodeca5(A,nil2)=nil. % 1.99/2.19 ** KEPT (pick-wt=28): 93 [] 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)). % 1.99/2.19 ** KEPT (pick-wt=5): 94 [] dodeca6(A,nil2)=nil. % 1.99/2.19 ---> New Demodulator: 95 [new_demod,94] dodeca6(A,nil2)=nil. % 1.99/2.19 ** KEPT (pick-wt=32): 96 [] 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)). % 1.99/2.19 ** KEPT (pick-wt=4): 97 [] dodeca7(zero)=nil. % 1.99/2.19 ---> New Demodulator: 98 [new_demod,97] dodeca7(zero)=nil. % 1.99/2.19 ** KEPT (pick-wt=78): 99 [] 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)))))))). % 1.99/2.19 ---> New Demodulator: 100 [new_demod,99] 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)))))))). % 1.99/2.19 ** KEPT (pick-wt=12): 101 [] prop_d52(A)=notb(andb(colouring2(dodeca7(five),A),and2(prop_d5(A)))). % 1.99/2.19 ---> New Demodulator: 102 [new_demod,101] prop_d52(A)=notb(andb(colouring2(dodeca7(five),A),and2(prop_d5(A)))). % 1.99/2.19 ** KEPT (pick-wt=5): 103 [] e_q2(bfalse,btrue)=bfalse. % 1.99/2.19 ---> New Demodulator: 104 [new_demod,103] e_q2(bfalse,btrue)=bfalse. % 1.99/2.19 ** KEPT (pick-wt=5): 105 [] e_q2(btrue,bfalse)=bfalse. % 1.99/2.19 ---> New Demodulator: 106 [new_demod,105] e_q2(btrue,bfalse)=bfalse. % 1.99/2.19 ** KEPT (pick-wt=9): 107 [] e_q(suc(A),suc(B))=e_q(A,B). % 1.99/2.19 ---> New Demodulator: 108 [new_demod,107] e_q(suc(A),suc(B))=e_q(A,B). % 1.99/2.19 ** KEPT (pick-wt=6): 109 [] e_q(zero,suc(A))=bfalse. % 1.99/2.19 ---> New Demodulator: 110 [new_demod,109] e_q(zero,suc(A))=bfalse. % 1.99/2.19 ** KEPT (pick-wt=6): 111 [] e_q(suc(A),zero)=bfalse. % 1.99/2.19 ---> New Demodulator: 112 [new_demod,111] e_q(suc(A),zero)=bfalse. % 1.99/2.19 ** KEPT (pick-wt=5): 113 [] e_q(A,A)=btrue. % 1.99/2.19 ---> New Demodulator: 114 [new_demod,113] e_q(A,A)=btrue. % 1.99/2.19 ** KEPT (pick-wt=5): 115 [] e_q2(A,A)=btrue. % 1.99/2.19 ---> New Demodulator: 116 [new_demod,115] e_q2(A,A)=btrue. % 1.99/2.19 Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] A=A. % 1.99/2.19 >>>> Starting back demodulation with 4. % 1.99/2.19 >>>> Starting back demodulation with 7. % 1.99/2.19 ** KEPT (pick-wt=12): 117 [copy,8,flip.1] cons3(bfalse,colouring(A,B))=aux2(A,B,C,D,nothing). % 1.99/2.19 ** KEPT (pick-wt=16): 118 [copy,9,flip.1] cons3(notb(e_q(A,B)),colouring(C,D))=aux2(C,D,E,A,just(B)). % 1.99/2.19 ** KEPT (pick-wt=12): 119 [copy,10,flip.1] cons3(bfalse,colouring(A,B))=aux3(A,B,C,D,nothing). % 1.99/2.19 ** KEPT (pick-wt=16): 120 [copy,11,flip.1] aux2(A,B,C,D,index(A,C))=aux3(A,B,E,C,just(D)). % 1.99/2.19 >>>> Starting back demodulation with 13. % 1.99/2.19 >>>> Starting back demodulation with 15. % 1.99/2.19 >>>> Starting back demodulation with 18. % 1.99/2.19 >>>> Starting back demodulation with 21. % 1.99/2.19 >>>> Starting back demodulation with 24. % 1.99/2.19 >>>> Starting back demodulation with 26. % 1.99/2.19 >>>> Starting back demodulation with 28. % 1.99/2.19 >>>> Starting back demodulation with 30. % 1.99/2.19 >>>> Starting back demodulation with 32. % 1.99/2.19 >>>> Starting back demodulation with 34. % 1.99/2.19 >>>> Starting back demodulation with 36. % 1.99/2.19 >>>> Starting back demodulation with 38. % 1.99/2.19 >>>> Starting back demodulation with 40. % 1.99/2.19 >>>> Starting back demodulation with 42. % 1.99/2.19 ** KEPT (pick-wt=8): 121 [copy,43,flip.1] just(A)=index(cons2(A,B),zero). % 1.99/2.19 >>>> Starting back demodulation with 45. % 1.99/2.19 >>>> Starting back demodulation with 48. % 1.99/2.19 >>>> Starting back demodulation with 51. % 1.99/2.19 >>>> Starting back demodulation with 54. % 1.99/2.19 >>>> Starting back demodulation with 56. % 1.99/2.19 ** KEPT (pick-wt=12): 122 [copy,57,flip.1] cons(pair2(A,suc(A)),dodeca(B))=dodeca(cons2(A,B)). % 1.99/2.19 >>>> Starting back demodulation with 59. % 1.99/2.19 ** KEPT (pick-wt=16): 123 [copy,60,flip.1] aux3(A,B,C,D,index(A,C))=colouring(A,cons(pair2(C,D),B)). % 1.99/2.19 >>>> Starting back demodulation with 62. % 1.99/2.19 >>>> Starting back demodulation with 65. % 1.99/2.19 >>>> Starting back demodulation with 67. % 1.99/2.19 >>>> Starting back demodulation with 69. % 1.99/2.19 >>>> Starting back demodulation with 71. % 1.99/2.19 >>>> Starting back demodulation with 73. % 1.99/2.19 >>>> Starting back demodulation with 76. % 1.99/2.19 >>>> Starting back demodulation with 78. % 1.99/2.19 >>>> Starting back demodulation with 81. % 1.99/2.19 >>>> Starting back demodulation with 83. % 1.99/2.19 ** KEPT (pick-wt=16): 124 [copy,84,flip.1] cons(pair2(A,add(suc(B),A)),dodeca2(B,C))=dodeca2(B,cons2(A,C)). % 1.99/2.19 >>>> Starting back demodulation with 86. % 1.99/2.19 ** KEPT (pick-wt=22): 125 [copy,87,flip.1] cons(pair2(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C))=dodeca3(A,cons2(B,C)). % 1.99/2.19 >>>> Starting back demodulation with 89. % 1.99/2.19 ** KEPT (pick-wt=23): 126 [copy,90,flip.1] cons(pair2(add(suc(A),suc(B)),add(add(suc(A),suc(A)),B)),dodeca4(A,C))=dodeca4(A,cons2(B,C)). % 1.99/2.19 >>>> Starting back demodulation with 92. % 1.99/2.19 ** KEPT (pick-wt=28): 127 [copy,93,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)). % 1.99/2.19 >>>> Starting back demodulation with 95. % 1.99/2.19 ** KEPT (pick-wt=32): 128 [copy,96,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)). % 1.99/2.19 >>>> Starting back demodulation with 98. % 1.99/2.19 >>>> Starting back demodulation with 100. % 1.99/2.19 >>>> Starting back demodulation with 102. % 1.99/2.19 >> back demodulating 1 with 102. % 1.99/2.19 >>>> Starting back demodulation with 104. % 1.99/2.19 >>>> Starting back demodulation with 106. % 1.99/2.19 >>>> Starting back demodulation with 108. % 1.99/2.19 >>>> Starting back demodulation with 110. % 1.99/2.19 >>>> Starting back demodulation with 112. % 1.99/2.19 >>>> Starting back demodulation with 114. % 1.99/2.19 >>>> Starting back demodulation with 116. % 1.99/2.19 Following clause subsumed by 8 during input processing: 0 [copy,117,flip.1] aux2(A,B,C,D,nothing)=cons3(bfalse,colouring(A,B)). % 1.99/2.19 Following clause subsumed by 9 during input processing: 0 [copy,118,flip.1] aux2(A,B,C,D,just(E))=cons3(notb(e_q(D,E)),colouring(A,B)). % 1.99/2.19 Following clause subsumed by 10 during input processing: 0 [copy,119,flip.1] aux3(A,B,C,D,nothing)=cons3(bfalse,colouring(A,B)). % 1.99/2.19 Following clause subsumed by 11 during input processing: 0 [copy,120,flip.1] aux3(A,B,C,D,just(E))=aux2(A,B,D,E,index(A,D)). % 1.99/2.19 Following clause subsumed by 43 during input processing: 0 [copy,121,flip.1] index(cons2(A,B),zero)=just(A). % 1.99/2.19 Following clause subsumed by 57 during input processing: 0 [copy,122,flip.1] dodeca(cons2(A,B))=cons(pair2(A,suc(A)),dodeca(B)). % 1.99/2.19 Following clause subsumed by 60 during input processing: 0 [copy,123,flip.1] colouring(A,cons(pair2(B,C),D))=aux3(A,D,B,C,index(A,B)). % 1.99/2.19 Following clause subsumed by 84 during input processing: 0 [copy,124,flip.1] dodeca2(A,cons2(B,C))=cons(pair2(B,add(suc(A),B)),dodeca2(A,C)). % 1.99/2.19 Following clause subsumed by 87 during input processing: 0 [copy,125,flip.1] dodeca3(A,cons2(B,C))=cons(pair2(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C)). % 1.99/2.19 Following clause subsumed by 90 during input processing: 0 [copy,126,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.04/2.21 Following clause subsumed by 93 during input processing: 0 [copy,127,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.04/2.21 Following clause subsumed by 96 during input processing: 0 [copy,128,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.04/2.21 % 2.04/2.21 ======= end of input processing ======= % 2.04/2.21 % 2.04/2.21 =========== start of search =========== % 2.04/2.21 % 2.04/2.21 % 2.04/2.21 Resetting weight limit to 5. % 2.04/2.21 % 2.04/2.21 % 2.04/2.21 Resetting weight limit to 5. % 2.04/2.21 % 2.04/2.21 sos_size=94 % 2.04/2.21 % 2.04/2.21 Search stopped because sos empty. % 2.04/2.21 % 2.04/2.21 % 2.04/2.21 Search stopped because sos empty. % 2.04/2.21 % 2.04/2.21 ============ end of search ============ % 2.04/2.21 % 2.04/2.21 -------------- statistics ------------- % 2.04/2.21 clauses given 187 % 2.04/2.21 clauses generated 1061 % 2.04/2.21 clauses kept 252 % 2.04/2.21 clauses forward subsumed 340 % 2.04/2.21 clauses back subsumed 0 % 2.04/2.21 Kbytes malloced 6835 % 2.04/2.21 % 2.04/2.21 ----------- times (seconds) ----------- % 2.04/2.21 user CPU time 0.02 (0 hr, 0 min, 0 sec) % 2.04/2.21 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.04/2.21 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.04/2.21 % 2.04/2.21 Process 6074 finished Tue May 5 13:00:08 2026 % 2.04/2.21 Otter interrupted % 2.04/2.21 PROOF NOT FOUND %------------------------------------------------------------------------------