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