%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX229-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n025.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.11s 2.32s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX229-1 : TPTP v9.3.0. Released v9.3.0. % 0.13/0.12 % Command : otter-tptp-script %s % 0.16/0.33 % Computer : n025.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 12:57:58 EDT 2026 % 0.16/0.33 % CPUTime : % 2.11/2.30 ----- Otter 3.3f, August 2004 ----- % 2.11/2.30 The process was started by sandbox on n025.cluster.edu, % 2.11/2.30 Tue May 5 12:57:58 2026 % 2.11/2.30 The command was "./otter". The process ID is 24027. % 2.11/2.30 % 2.11/2.30 set(prolog_style_variables). % 2.11/2.30 set(auto). % 2.11/2.30 dependent: set(auto1). % 2.11/2.30 dependent: set(process_input). % 2.11/2.30 dependent: clear(print_kept). % 2.11/2.30 dependent: clear(print_new_demod). % 2.11/2.30 dependent: clear(print_back_demod). % 2.11/2.30 dependent: clear(print_back_sub). % 2.11/2.30 dependent: set(control_memory). % 2.11/2.30 dependent: assign(max_mem, 12000). % 2.11/2.30 dependent: assign(pick_given_ratio, 4). % 2.11/2.30 dependent: assign(stats_level, 1). % 2.11/2.30 dependent: assign(max_seconds, 10800). % 2.11/2.30 clear(print_given). % 2.11/2.30 % 2.11/2.30 list(usable). % 2.11/2.30 0 [] A=A. % 2.11/2.30 0 [] aux(X,Y,btrue)=Y. % 2.11/2.30 0 [] aux(X,Y,bfalse)=X. % 2.11/2.30 0 [] aux2(X,Y,btrue)=nil4. % 2.11/2.30 0 [] aux2(X,Y,bfalse)=cons4(X,enumFromToNat(suc(X),Y)). % 2.11/2.30 0 [] aux3(Y,btrue)=cons6(o,bin(halfNat(suc(Y)))). % 2.11/2.30 0 [] aux3(Y,bfalse)=cons6(i,bin(halfNat(suc(Y)))). % 2.11/2.30 0 [] predNat(zero)=zero. % 2.11/2.30 0 [] predNat(suc(Y))=Y. % 2.11/2.30 0 [] orb(btrue,Q)=btrue. % 2.11/2.30 0 [] orb(bfalse,Q)=Q. % 2.11/2.30 0 [] or2(nil5)=bfalse. % 2.11/2.30 0 [] or2(cons5(Y,Xs))=orb(Y,or2(Xs)). % 2.11/2.30 0 [] one=suc(zero). % 2.11/2.30 0 [] two=suc(one). % 2.11/2.30 0 [] three=suc(two). % 2.11/2.30 0 [] notb(btrue)=bfalse. % 2.11/2.30 0 [] notb(bfalse)=btrue. % 2.11/2.30 0 [] lt(zero,zero)=bfalse. % 2.11/2.30 0 [] lt(zero,suc(Z))=btrue. % 2.11/2.30 0 [] lt(suc(X2),zero)=bfalse. % 2.11/2.30 0 [] lt(suc(X2),suc(Y2))=lt(X2,Y2). % 2.11/2.30 0 [] maxNat(X,Y)=aux(X,Y,lt(X,Y)). % 2.11/2.30 0 [] maximum(X,nil2)=X. % 2.11/2.30 0 [] maximum(X,cons2(pair22(Y2,Z2),Yzs))=maximum(maxNat(X,maxNat(Y2,Z2)),Yzs). % 2.11/2.30 0 [] len(nil3)=zero. % 2.11/2.30 0 [] len(cons3(Y,Xs))=suc(len(Xs)). % 2.11/2.30 0 [] last(X,nil3)=X. % 2.11/2.30 0 [] last(X,cons3(Z,Ys))=last(Z,Ys). % 2.11/2.30 0 [] halfNat(zero)=zero. % 2.11/2.30 0 [] halfNat(suc(zero))=zero. % 2.11/2.30 0 [] halfNat(suc(suc(N)))=suc(halfNat(N)). % 2.11/2.30 0 [] evenNat(zero)=btrue. % 2.11/2.30 0 [] evenNat(suc(zero))=bfalse. % 2.11/2.30 0 [] evenNat(suc(suc(N)))=evenNat(N). % 2.11/2.30 0 [] enumFromToNat(X,Y)=aux2(X,Y,lt(Y,X)). % 2.11/2.30 0 [] dodeca(nil4)=nil2. % 2.11/2.30 0 [] dodeca(cons4(Y,Z))=cons2(pair22(Y,suc(Y)),dodeca(Z)). % 2.11/2.30 0 [] bin(zero)=nil6. % 2.11/2.30 0 [] bin(suc(Y))=aux3(Y,evenNat(suc(Y))). % 2.11/2.30 0 [] bgraph(nil2)=nil. % 2.11/2.30 0 [] bgraph(cons2(pair22(U,V),Z))=cons(pair2(bin(U),bin(V)),bgraph(Z)). % 2.11/2.30 0 [] be_q(nil6,nil6)=btrue. % 2.11/2.30 0 [] be_q(nil6,cons6(Z,X2))=bfalse. % 2.11/2.30 0 [] be_q(cons6(i,Xs),nil6)=bfalse. % 2.11/2.30 0 [] be_q(cons6(i,Xs),cons6(i,Ys))=be_q(Xs,Ys). % 2.11/2.30 0 [] be_q(cons6(i,Xs),cons6(o,Ys))=bfalse. % 2.11/2.30 0 [] be_q(cons6(o,Xs),nil6)=bfalse. % 2.11/2.30 0 [] be_q(cons6(o,Xs),cons6(i,Zs))=bfalse. % 2.11/2.30 0 [] be_q(cons6(o,Xs),cons6(o,Zs))=be_q(Xs,Zs). % 2.11/2.30 0 [] belem(X,nil3)=nil5. % 2.11/2.30 0 [] belem(X,cons3(Z,X2))=cons5(be_q(X,Z),belem(X,X2)). % 2.11/2.30 0 [] belem2(X,Y)=or2(belem(X,Y)). % 2.11/2.30 0 [] append(nil2,Y)=Y. % 2.11/2.30 0 [] append(cons2(Z,Xs),Y)=cons2(Z,append(Xs,Y)). % 2.11/2.30 0 [] andb(btrue,Q)=Q. % 2.11/2.30 0 [] andb(bfalse,Q)=bfalse. % 2.11/2.30 0 [] bpath(X,Y,nil)=nil5. % 2.11/2.30 0 [] bpath(X,Y,cons(pair2(U,V),X3))=cons5(orb(andb(be_q(U,X),be_q(V,Y)),andb(be_q(U,Y),be_q(V,X))),bpath(X,Y,X3)). % 2.11/2.30 0 [] bpath2(nil3,Y)=btrue. % 2.11/2.30 0 [] bpath2(cons3(Z,nil3),Y)=btrue. % 2.11/2.30 0 [] bpath2(cons3(Z,cons3(Y2,Xs)),Y)=andb(or2(bpath(Z,Y2,Y)),bpath2(cons3(Y2,Xs),Y)). % 2.11/2.30 0 [] bunique(nil3)=btrue. % 2.11/2.30 0 [] bunique(cons3(Y,Xs))=andb(notb(belem2(Y,Xs)),bunique(Xs)). % 2.11/2.30 0 [] add(zero,Y)=Y. % 2.11/2.30 0 [] add(suc(Z),Y)=suc(add(Z,Y)). % 2.11/2.30 0 [] btour(nil3,nil2)=btrue. % 2.11/2.30 0 [] btour(nil3,cons2(Z,X2))=bfalse. % 2.11/2.30 0 [] btour(cons3(X3,X4),nil2)=bfalse. % 2.11/2.30 0 [] btour(cons3(X3,X4),cons2(pair22(U,V),Vs))=andb(be_q(X3,last(X3,X4)),andb(bpath2(cons3(X3,X4),bgraph(cons2(pair22(U,V),Vs))),andb(bunique(X4),e_q(len(cons3(X3,X4)),add(two,maximum(maxNat(U,V),Vs)))))). % 2.11/2.30 0 [] dodeca2(X,nil4)=nil2. % 2.11/2.30 0 [] dodeca2(X,cons4(Z,X2))=cons2(pair22(Z,add(suc(X),Z)),dodeca2(X,X2)). % 2.11/2.30 0 [] dodeca3(X,nil4)=nil2. % 2.11/2.30 0 [] dodeca3(X,cons4(Z,X2))=cons2(pair22(add(suc(X),Z),add(add(suc(X),suc(X)),Z)),dodeca3(X,X2)). % 2.11/2.30 0 [] dodeca4(X,nil4)=nil2. % 2.11/2.30 0 [] dodeca4(X,cons4(Z,X2))=cons2(pair22(add(suc(X),suc(Z)),add(add(suc(X),suc(X)),Z)),dodeca4(X,X2)). % 2.11/2.30 0 [] dodeca5(X,nil4)=nil2. % 2.11/2.30 0 [] dodeca5(X,cons4(Z,X2))=cons2(pair22(add(add(suc(X),suc(X)),Z),add(add(add(suc(X),suc(X)),suc(X)),Z)),dodeca5(X,X2)). % 2.11/2.30 0 [] dodeca6(X,nil4)=nil2. % 2.11/2.30 0 [] dodeca6(X,cons4(Z,X2))=cons2(pair22(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.11/2.30 0 [] dodeca7(zero)=nil2. % 2.11/2.30 0 [] dodeca7(suc(Y))=append(cons2(pair22(Y,zero),dodeca(enumFromToNat(zero,Y))),append(dodeca2(Y,enumFromToNat(zero,suc(Y))),append(dodeca3(Y,enumFromToNat(zero,suc(Y))),append(cons2(pair22(suc(Y),add(add(suc(Y),suc(Y)),Y)),dodeca4(Y,enumFromToNat(zero,Y))),append(dodeca5(Y,enumFromToNat(zero,suc(Y))),cons2(pair22(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.11/2.31 0 [] prop_bt3(X)=notb(btour(X,dodeca7(three))). % 2.11/2.31 0 [] e_q2(bfalse,btrue)=bfalse. % 2.11/2.31 0 [] e_q2(btrue,bfalse)=bfalse. % 2.11/2.31 0 [] e_q3(i,o)=bfalse. % 2.11/2.31 0 [] e_q3(o,i)=bfalse. % 2.11/2.31 0 [] e_q(suc(X),suc(Y))=e_q(X,Y). % 2.11/2.31 0 [] e_q(zero,suc(X))=bfalse. % 2.11/2.31 0 [] e_q(suc(X),zero)=bfalse. % 2.11/2.31 0 [] e_q(X,X)=btrue. % 2.11/2.31 0 [] e_q2(X,X)=btrue. % 2.11/2.31 0 [] e_q3(X,X)=btrue. % 2.11/2.31 0 [] e_q2(prop_bt3(X),bfalse)!=btrue. % 2.11/2.31 end_of_list. % 2.11/2.31 % 2.11/2.31 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. % 2.11/2.31 % 2.11/2.31 All clauses are units, and equality is present; the % 2.11/2.31 strategy will be Knuth-Bendix with positive clauses in sos. % 2.11/2.31 % 2.11/2.31 dependent: set(knuth_bendix). % 2.11/2.31 dependent: set(anl_eq). % 2.11/2.31 dependent: set(para_from). % 2.11/2.31 dependent: set(para_into). % 2.11/2.31 dependent: clear(para_from_right). % 2.11/2.31 dependent: clear(para_into_right). % 2.11/2.31 dependent: set(para_from_vars). % 2.11/2.31 dependent: set(eq_units_both_ways). % 2.11/2.31 dependent: set(dynamic_demod_all). % 2.11/2.31 dependent: set(dynamic_demod). % 2.11/2.31 dependent: set(order_eq). % 2.11/2.31 dependent: set(back_demod). % 2.11/2.31 dependent: set(lrpo). % 2.11/2.31 % 2.11/2.31 ------------> process usable: % 2.11/2.31 ** KEPT (pick-wt=6): 1 [] e_q2(prop_bt3(A),bfalse)!=btrue. % 2.11/2.31 % 2.11/2.31 ------------> process sos: % 2.11/2.31 ** KEPT (pick-wt=3): 2 [] A=A. % 2.11/2.31 ** KEPT (pick-wt=6): 3 [] aux(A,B,btrue)=B. % 2.11/2.31 ---> New Demodulator: 4 [new_demod,3] aux(A,B,btrue)=B. % 2.11/2.31 ** KEPT (pick-wt=6): 5 [] aux(A,B,bfalse)=A. % 2.11/2.31 ---> New Demodulator: 6 [new_demod,5] aux(A,B,bfalse)=A. % 2.11/2.31 ** KEPT (pick-wt=6): 7 [] aux2(A,B,btrue)=nil4. % 2.11/2.31 ---> New Demodulator: 8 [new_demod,7] aux2(A,B,btrue)=nil4. % 2.11/2.31 ** KEPT (pick-wt=11): 10 [copy,9,flip.1] cons4(A,enumFromToNat(suc(A),B))=aux2(A,B,bfalse). % 2.11/2.31 ---> New Demodulator: 11 [new_demod,10] cons4(A,enumFromToNat(suc(A),B))=aux2(A,B,bfalse). % 2.11/2.31 ** KEPT (pick-wt=10): 13 [copy,12,flip.1] cons6(o,bin(halfNat(suc(A))))=aux3(A,btrue). % 2.11/2.31 ---> New Demodulator: 14 [new_demod,13] cons6(o,bin(halfNat(suc(A))))=aux3(A,btrue). % 2.11/2.31 ** KEPT (pick-wt=10): 16 [copy,15,flip.1] cons6(i,bin(halfNat(suc(A))))=aux3(A,bfalse). % 2.11/2.31 ---> New Demodulator: 17 [new_demod,16] cons6(i,bin(halfNat(suc(A))))=aux3(A,bfalse). % 2.11/2.31 ** KEPT (pick-wt=4): 18 [] predNat(zero)=zero. % 2.11/2.31 ---> New Demodulator: 19 [new_demod,18] predNat(zero)=zero. % 2.11/2.31 ** KEPT (pick-wt=5): 20 [] predNat(suc(A))=A. % 2.11/2.31 ---> New Demodulator: 21 [new_demod,20] predNat(suc(A))=A. % 2.11/2.31 ** KEPT (pick-wt=5): 22 [] orb(btrue,A)=btrue. % 2.11/2.31 ---> New Demodulator: 23 [new_demod,22] orb(btrue,A)=btrue. % 2.11/2.31 ** KEPT (pick-wt=5): 24 [] orb(bfalse,A)=A. % 2.11/2.31 ---> New Demodulator: 25 [new_demod,24] orb(bfalse,A)=A. % 2.11/2.31 ** KEPT (pick-wt=4): 26 [] or2(nil5)=bfalse. % 2.11/2.31 ---> New Demodulator: 27 [new_demod,26] or2(nil5)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=9): 28 [] or2(cons5(A,B))=orb(A,or2(B)). % 2.11/2.31 ---> New Demodulator: 29 [new_demod,28] or2(cons5(A,B))=orb(A,or2(B)). % 2.11/2.31 ** KEPT (pick-wt=4): 31 [copy,30,flip.1] suc(zero)=one. % 2.11/2.31 ---> New Demodulator: 32 [new_demod,31] suc(zero)=one. % 2.11/2.31 ** KEPT (pick-wt=4): 34 [copy,33,flip.1] suc(one)=two. % 2.11/2.31 ---> New Demodulator: 35 [new_demod,34] suc(one)=two. % 2.11/2.31 ** KEPT (pick-wt=4): 37 [copy,36,flip.1] suc(two)=three. % 2.11/2.31 ---> New Demodulator: 38 [new_demod,37] suc(two)=three. % 2.11/2.31 ** KEPT (pick-wt=4): 39 [] notb(btrue)=bfalse. % 2.11/2.31 ---> New Demodulator: 40 [new_demod,39] notb(btrue)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=4): 41 [] notb(bfalse)=btrue. % 2.11/2.31 ---> New Demodulator: 42 [new_demod,41] notb(bfalse)=btrue. % 2.11/2.31 ** KEPT (pick-wt=5): 43 [] lt(zero,zero)=bfalse. % 2.11/2.31 ---> New Demodulator: 44 [new_demod,43] lt(zero,zero)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=6): 45 [] lt(zero,suc(A))=btrue. % 2.11/2.31 ---> New Demodulator: 46 [new_demod,45] lt(zero,suc(A))=btrue. % 2.11/2.31 ** KEPT (pick-wt=6): 47 [] lt(suc(A),zero)=bfalse. % 2.11/2.31 ---> New Demodulator: 48 [new_demod,47] lt(suc(A),zero)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=9): 49 [] lt(suc(A),suc(B))=lt(A,B). % 2.11/2.31 ---> New Demodulator: 50 [new_demod,49] lt(suc(A),suc(B))=lt(A,B). % 2.11/2.31 ** KEPT (pick-wt=10): 51 [] maxNat(A,B)=aux(A,B,lt(A,B)). % 2.11/2.31 ---> New Demodulator: 52 [new_demod,51] maxNat(A,B)=aux(A,B,lt(A,B)). % 2.11/2.31 ** KEPT (pick-wt=5): 53 [] maximum(A,nil2)=A. % 2.11/2.31 ---> New Demodulator: 54 [new_demod,53] maximum(A,nil2)=A. % 2.11/2.31 ** KEPT (pick-wt=26): 56 [copy,55,demod,52,52] maximum(A,cons2(pair22(B,C),D))=maximum(aux(A,aux(B,C,lt(B,C)),lt(A,aux(B,C,lt(B,C)))),D). % 2.11/2.31 ** KEPT (pick-wt=4): 57 [] len(nil3)=zero. % 2.11/2.31 ---> New Demodulator: 58 [new_demod,57] len(nil3)=zero. % 2.11/2.31 ** KEPT (pick-wt=8): 59 [] len(cons3(A,B))=suc(len(B)). % 2.11/2.31 ** KEPT (pick-wt=5): 60 [] last(A,nil3)=A. % 2.11/2.31 ---> New Demodulator: 61 [new_demod,60] last(A,nil3)=A. % 2.11/2.31 ** KEPT (pick-wt=9): 62 [] last(A,cons3(B,C))=last(B,C). % 2.11/2.31 ** KEPT (pick-wt=4): 63 [] halfNat(zero)=zero. % 2.11/2.31 ---> New Demodulator: 64 [new_demod,63] halfNat(zero)=zero. % 2.11/2.31 ** KEPT (pick-wt=4): 66 [copy,65,demod,32] halfNat(one)=zero. % 2.11/2.31 ---> New Demodulator: 67 [new_demod,66] halfNat(one)=zero. % 2.11/2.31 ** KEPT (pick-wt=8): 68 [] halfNat(suc(suc(A)))=suc(halfNat(A)). % 2.11/2.31 ---> New Demodulator: 69 [new_demod,68] halfNat(suc(suc(A)))=suc(halfNat(A)). % 2.11/2.31 ** KEPT (pick-wt=4): 70 [] evenNat(zero)=btrue. % 2.11/2.31 ---> New Demodulator: 71 [new_demod,70] evenNat(zero)=btrue. % 2.11/2.31 ** KEPT (pick-wt=4): 73 [copy,72,demod,32] evenNat(one)=bfalse. % 2.11/2.31 ---> New Demodulator: 74 [new_demod,73] evenNat(one)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=7): 75 [] evenNat(suc(suc(A)))=evenNat(A). % 2.11/2.31 ---> New Demodulator: 76 [new_demod,75] evenNat(suc(suc(A)))=evenNat(A). % 2.11/2.31 ** KEPT (pick-wt=10): 78 [copy,77,flip.1] aux2(A,B,lt(B,A))=enumFromToNat(A,B). % 2.11/2.31 ---> New Demodulator: 79 [new_demod,78] aux2(A,B,lt(B,A))=enumFromToNat(A,B). % 2.11/2.31 ** KEPT (pick-wt=4): 80 [] dodeca(nil4)=nil2. % 2.11/2.31 ---> New Demodulator: 81 [new_demod,80] dodeca(nil4)=nil2. % 2.11/2.31 ** KEPT (pick-wt=12): 82 [] dodeca(cons4(A,B))=cons2(pair22(A,suc(A)),dodeca(B)). % 2.11/2.31 ** KEPT (pick-wt=4): 83 [] bin(zero)=nil6. % 2.11/2.31 ---> New Demodulator: 84 [new_demod,83] bin(zero)=nil6. % 2.11/2.31 ** KEPT (pick-wt=9): 86 [copy,85,flip.1] aux3(A,evenNat(suc(A)))=bin(suc(A)). % 2.11/2.31 ---> New Demodulator: 87 [new_demod,86] aux3(A,evenNat(suc(A)))=bin(suc(A)). % 2.11/2.31 ** KEPT (pick-wt=4): 88 [] bgraph(nil2)=nil. % 2.11/2.31 ---> New Demodulator: 89 [new_demod,88] bgraph(nil2)=nil. % 2.11/2.31 ** KEPT (pick-wt=15): 90 [] bgraph(cons2(pair22(A,B),C))=cons(pair2(bin(A),bin(B)),bgraph(C)). % 2.11/2.31 ** KEPT (pick-wt=5): 91 [] be_q(nil6,nil6)=btrue. % 2.11/2.31 ---> New Demodulator: 92 [new_demod,91] be_q(nil6,nil6)=btrue. % 2.11/2.31 ** KEPT (pick-wt=7): 93 [] be_q(nil6,cons6(A,B))=bfalse. % 2.11/2.31 ---> New Demodulator: 94 [new_demod,93] be_q(nil6,cons6(A,B))=bfalse. % 2.11/2.31 ** KEPT (pick-wt=7): 95 [] be_q(cons6(i,A),nil6)=bfalse. % 2.11/2.31 ---> New Demodulator: 96 [new_demod,95] be_q(cons6(i,A),nil6)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=11): 97 [] be_q(cons6(i,A),cons6(i,B))=be_q(A,B). % 2.11/2.31 ---> New Demodulator: 98 [new_demod,97] be_q(cons6(i,A),cons6(i,B))=be_q(A,B). % 2.11/2.31 ** KEPT (pick-wt=9): 99 [] be_q(cons6(i,A),cons6(o,B))=bfalse. % 2.11/2.31 ---> New Demodulator: 100 [new_demod,99] be_q(cons6(i,A),cons6(o,B))=bfalse. % 2.11/2.31 ** KEPT (pick-wt=7): 101 [] be_q(cons6(o,A),nil6)=bfalse. % 2.11/2.31 ---> New Demodulator: 102 [new_demod,101] be_q(cons6(o,A),nil6)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=9): 103 [] be_q(cons6(o,A),cons6(i,B))=bfalse. % 2.11/2.31 ---> New Demodulator: 104 [new_demod,103] be_q(cons6(o,A),cons6(i,B))=bfalse. % 2.11/2.31 ** KEPT (pick-wt=11): 105 [] be_q(cons6(o,A),cons6(o,B))=be_q(A,B). % 2.11/2.31 ---> New Demodulator: 106 [new_demod,105] be_q(cons6(o,A),cons6(o,B))=be_q(A,B). % 2.11/2.31 ** KEPT (pick-wt=5): 107 [] belem(A,nil3)=nil5. % 2.11/2.31 ---> New Demodulator: 108 [new_demod,107] belem(A,nil3)=nil5. % 2.11/2.31 ** KEPT (pick-wt=13): 110 [copy,109,flip.1] cons5(be_q(A,B),belem(A,C))=belem(A,cons3(B,C)). % 2.11/2.31 ---> New Demodulator: 111 [new_demod,110] cons5(be_q(A,B),belem(A,C))=belem(A,cons3(B,C)). % 2.11/2.31 ** KEPT (pick-wt=8): 113 [copy,112,flip.1] or2(belem(A,B))=belem2(A,B). % 2.11/2.31 ---> New Demodulator: 114 [new_demod,113] or2(belem(A,B))=belem2(A,B). % 2.11/2.31 ** KEPT (pick-wt=5): 115 [] append(nil2,A)=A. % 2.11/2.31 ---> New Demodulator: 116 [new_demod,115] append(nil2,A)=A. % 2.11/2.31 ** KEPT (pick-wt=11): 118 [copy,117,flip.1] cons2(A,append(B,C))=append(cons2(A,B),C). % 2.11/2.31 ---> New Demodulator: 119 [new_demod,118] cons2(A,append(B,C))=append(cons2(A,B),C). % 2.11/2.31 ** KEPT (pick-wt=5): 120 [] andb(btrue,A)=A. % 2.11/2.31 ---> New Demodulator: 121 [new_demod,120] andb(btrue,A)=A. % 2.11/2.31 ** KEPT (pick-wt=5): 122 [] andb(bfalse,A)=bfalse. % 2.11/2.31 ---> New Demodulator: 123 [new_demod,122] andb(bfalse,A)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=6): 124 [] bpath(A,B,nil)=nil5. % 2.11/2.31 ---> New Demodulator: 125 [new_demod,124] bpath(A,B,nil)=nil5. % 2.11/2.31 ** KEPT (pick-wt=29): 126 [] bpath(A,B,cons(pair2(C,D),E))=cons5(orb(andb(be_q(C,A),be_q(D,B)),andb(be_q(C,B),be_q(D,A))),bpath(A,B,E)). % 2.11/2.31 ** KEPT (pick-wt=5): 127 [] bpath2(nil3,A)=btrue. % 2.11/2.31 ---> New Demodulator: 128 [new_demod,127] bpath2(nil3,A)=btrue. % 2.11/2.31 ** KEPT (pick-wt=7): 129 [] bpath2(cons3(A,nil3),B)=btrue. % 2.11/2.31 ---> New Demodulator: 130 [new_demod,129] bpath2(cons3(A,nil3),B)=btrue. % 2.11/2.31 ** KEPT (pick-wt=19): 131 [] bpath2(cons3(A,cons3(B,C)),D)=andb(or2(bpath(A,B,D)),bpath2(cons3(B,C),D)). % 2.11/2.31 ** KEPT (pick-wt=4): 132 [] bunique(nil3)=btrue. % 2.11/2.31 ---> New Demodulator: 133 [new_demod,132] bunique(nil3)=btrue. % 2.11/2.31 ** KEPT (pick-wt=12): 135 [copy,134,flip.1] andb(notb(belem2(A,B)),bunique(B))=bunique(cons3(A,B)). % 2.11/2.31 ---> New Demodulator: 136 [new_demod,135] andb(notb(belem2(A,B)),bunique(B))=bunique(cons3(A,B)). % 2.11/2.31 ** KEPT (pick-wt=5): 137 [] add(zero,A)=A. % 2.11/2.31 ---> New Demodulator: 138 [new_demod,137] add(zero,A)=A. % 2.11/2.31 ** KEPT (pick-wt=9): 140 [copy,139,flip.1] suc(add(A,B))=add(suc(A),B). % 2.11/2.31 ---> New Demodulator: 141 [new_demod,140] suc(add(A,B))=add(suc(A),B). % 2.11/2.31 ** KEPT (pick-wt=5): 142 [] btour(nil3,nil2)=btrue. % 2.11/2.31 ---> New Demodulator: 143 [new_demod,142] btour(nil3,nil2)=btrue. % 2.11/2.31 ** KEPT (pick-wt=7): 144 [] btour(nil3,cons2(A,B))=bfalse. % 2.11/2.31 ---> New Demodulator: 145 [new_demod,144] btour(nil3,cons2(A,B))=bfalse. % 2.11/2.31 ** KEPT (pick-wt=7): 146 [] btour(cons3(A,B),nil2)=bfalse. % 2.11/2.31 ---> New Demodulator: 147 [new_demod,146] btour(cons3(A,B),nil2)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=45): 149 [copy,148,demod,52] btour(cons3(A,B),cons2(pair22(C,D),E))=andb(be_q(A,last(A,B)),andb(bpath2(cons3(A,B),bgraph(cons2(pair22(C,D),E))),andb(bunique(B),e_q(len(cons3(A,B)),add(two,maximum(aux(C,D,lt(C,D)),E)))))). % 2.11/2.31 ** KEPT (pick-wt=5): 150 [] dodeca2(A,nil4)=nil2. % 2.11/2.31 ---> New Demodulator: 151 [new_demod,150] dodeca2(A,nil4)=nil2. % 2.11/2.31 ** KEPT (pick-wt=16): 152 [] dodeca2(A,cons4(B,C))=cons2(pair22(B,add(suc(A),B)),dodeca2(A,C)). % 2.11/2.31 ** KEPT (pick-wt=5): 153 [] dodeca3(A,nil4)=nil2. % 2.11/2.31 ---> New Demodulator: 154 [new_demod,153] dodeca3(A,nil4)=nil2. % 2.11/2.31 ** KEPT (pick-wt=22): 155 [] dodeca3(A,cons4(B,C))=cons2(pair22(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C)). % 2.11/2.31 ** KEPT (pick-wt=5): 156 [] dodeca4(A,nil4)=nil2. % 2.11/2.31 ---> New Demodulator: 157 [new_demod,156] dodeca4(A,nil4)=nil2. % 2.11/2.31 ** KEPT (pick-wt=23): 158 [] dodeca4(A,cons4(B,C))=cons2(pair22(add(suc(A),suc(B)),add(add(suc(A),suc(A)),B)),dodeca4(A,C)). % 2.11/2.31 ** KEPT (pick-wt=5): 159 [] dodeca5(A,nil4)=nil2. % 2.11/2.31 ---> New Demodulator: 160 [new_demod,159] dodeca5(A,nil4)=nil2. % 2.11/2.31 ** KEPT (pick-wt=28): 161 [] dodeca5(A,cons4(B,C))=cons2(pair22(add(add(suc(A),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),B)),dodeca5(A,C)). % 2.11/2.31 ** KEPT (pick-wt=5): 162 [] dodeca6(A,nil4)=nil2. % 2.11/2.31 ---> New Demodulator: 163 [new_demod,162] dodeca6(A,nil4)=nil2. % 2.11/2.31 ** KEPT (pick-wt=32): 164 [] dodeca6(A,cons4(B,C))=cons2(pair22(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.11/2.31 ** KEPT (pick-wt=4): 165 [] dodeca7(zero)=nil2. % 2.11/2.31 ---> New Demodulator: 166 [new_demod,165] dodeca7(zero)=nil2. % 2.11/2.31 ** KEPT (pick-wt=78): 167 [] dodeca7(suc(A))=append(cons2(pair22(A,zero),dodeca(enumFromToNat(zero,A))),append(dodeca2(A,enumFromToNat(zero,suc(A))),append(dodeca3(A,enumFromToNat(zero,suc(A))),append(cons2(pair22(suc(A),add(add(suc(A),suc(A)),A)),dodeca4(A,enumFromToNat(zero,A))),append(dodeca5(A,enumFromToNat(zero,suc(A))),cons2(pair22(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.11/2.31 ---> New Demodulator: 168 [new_demod,167] dodeca7(suc(A))=append(cons2(pair22(A,zero),dodeca(enumFromToNat(zero,A))),append(dodeca2(A,enumFromToNat(zero,suc(A))),append(dodeca3(A,enumFromToNat(zero,suc(A))),append(cons2(pair22(suc(A),add(add(suc(A),suc(A)),A)),dodeca4(A,enumFromToNat(zero,A))),append(dodeca5(A,enumFromToNat(zero,suc(A))),cons2(pair22(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.11/2.31 ** KEPT (pick-wt=8): 169 [] prop_bt3(A)=notb(btour(A,dodeca7(three))). % 2.11/2.31 ---> New Demodulator: 170 [new_demod,169] prop_bt3(A)=notb(btour(A,dodeca7(three))). % 2.11/2.31 ** KEPT (pick-wt=5): 171 [] e_q2(bfalse,btrue)=bfalse. % 2.11/2.31 ---> New Demodulator: 172 [new_demod,171] e_q2(bfalse,btrue)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=5): 173 [] e_q2(btrue,bfalse)=bfalse. % 2.11/2.31 ---> New Demodulator: 174 [new_demod,173] e_q2(btrue,bfalse)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=5): 175 [] e_q3(i,o)=bfalse. % 2.11/2.31 ---> New Demodulator: 176 [new_demod,175] e_q3(i,o)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=5): 177 [] e_q3(o,i)=bfalse. % 2.11/2.31 ---> New Demodulator: 178 [new_demod,177] e_q3(o,i)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=9): 179 [] e_q(suc(A),suc(B))=e_q(A,B). % 2.11/2.31 ---> New Demodulator: 180 [new_demod,179] e_q(suc(A),suc(B))=e_q(A,B). % 2.11/2.31 ** KEPT (pick-wt=6): 181 [] e_q(zero,suc(A))=bfalse. % 2.11/2.31 ---> New Demodulator: 182 [new_demod,181] e_q(zero,suc(A))=bfalse. % 2.11/2.31 ** KEPT (pick-wt=6): 183 [] e_q(suc(A),zero)=bfalse. % 2.11/2.31 ---> New Demodulator: 184 [new_demod,183] e_q(suc(A),zero)=bfalse. % 2.11/2.31 ** KEPT (pick-wt=5): 185 [] e_q(A,A)=btrue. % 2.11/2.31 ---> New Demodulator: 186 [new_demod,185] e_q(A,A)=btrue. % 2.11/2.31 ** KEPT (pick-wt=5): 187 [] e_q2(A,A)=btrue. % 2.11/2.31 ---> New Demodulator: 188 [new_demod,187] e_q2(A,A)=btrue. % 2.11/2.31 ** KEPT (pick-wt=5): 189 [] e_q3(A,A)=btrue. % 2.11/2.31 ---> New Demodulator: 190 [new_demod,189] e_q3(A,A)=btrue. % 2.11/2.31 Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] A=A. % 2.11/2.31 >>>> Starting back demodulation with 4. % 2.11/2.31 >>>> Starting back demodulation with 6. % 2.11/2.31 >>>> Starting back demodulation with 8. % 2.11/2.31 >>>> Starting back demodulation with 11. % 2.11/2.31 >>>> Starting back demodulation with 14. % 2.11/2.31 >>>> Starting back demodulation with 17. % 2.11/2.31 >>>> Starting back demodulation with 19. % 2.11/2.31 >>>> Starting back demodulation with 21. % 2.11/2.31 >>>> Starting back demodulation with 23. % 2.11/2.31 >>>> Starting back demodulation with 25. % 2.11/2.31 >>>> Starting back demodulation with 27. % 2.11/2.31 >>>> Starting back demodulation with 29. % 2.11/2.31 >>>> Starting back demodulation with 32. % 2.11/2.31 >>>> Starting back demodulation with 35. % 2.11/2.31 >>>> Starting back demodulation with 38. % 2.11/2.31 >>>> Starting back demodulation with 40. % 2.11/2.31 >>>> Starting back demodulation with 42. % 2.11/2.31 >>>> Starting back demodulation with 44. % 2.11/2.31 >>>> Starting back demodulation with 46. % 2.11/2.31 >>>> Starting back demodulation with 48. % 2.11/2.31 >>>> Starting back demodulation with 50. % 2.11/2.31 >>>> Starting back demodulation with 52. % 2.11/2.31 >>>> Starting back demodulation with 54. % 2.11/2.31 ** KEPT (pick-wt=26): 191 [copy,56,flip.1] maximum(aux(A,aux(B,C,lt(B,C)),lt(A,aux(B,C,lt(B,C)))),D)=maximum(A,cons2(pair22(B,C),D)). % 2.11/2.31 >>>> Starting back demodulation with 58. % 2.11/2.31 ** KEPT (pick-wt=8): 192 [copy,59,flip.1] suc(len(A))=len(cons3(B,A)). % 2.11/2.31 >>>> Starting back demodulation with 61. % 2.11/2.31 ** KEPT (pick-wt=9): 193 [copy,62,flip.1] last(A,B)=last(C,cons3(A,B)). % 2.11/2.31 >>>> Starting back demodulation with 64. % 2.11/2.31 >>>> Starting back demodulation with 67. % 2.11/2.31 >>>> Starting back demodulation with 69. % 2.11/2.31 >>>> Starting back demodulation with 71. % 2.11/2.31 >>>> Starting back demodulation with 74. % 2.11/2.31 >>>> Starting back demodulation with 76. % 2.11/2.31 >>>> Starting back demodulation with 79. % 2.11/2.31 >>>> Starting back demodulation with 81. % 2.11/2.31 ** KEPT (pick-wt=12): 194 [copy,82,flip.1] cons2(pair22(A,suc(A)),dodeca(B))=dodeca(cons4(A,B)). % 2.11/2.31 >>>> Starting back demodulation with 84. % 2.11/2.31 >>>> Starting back demodulation with 87. % 2.11/2.31 >>>> Starting back demodulation with 89. % 2.11/2.31 ** KEPT (pick-wt=15): 195 [copy,90,flip.1] cons(pair2(bin(A),bin(B)),bgraph(C))=bgraph(cons2(pair22(A,B),C)). % 2.11/2.31 >>>> Starting back demodulation with 92. % 2.11/2.31 >>>> Starting back demodulation with 94. % 2.11/2.31 >>>> Starting back demodulation with 96. % 2.11/2.31 >>>> Starting back demodulation with 98. % 2.11/2.31 >>>> Starting back demodulation with 100. % 2.11/2.31 >>>> Starting back demodulation with 102. % 2.11/2.31 >>>> Starting back demodulation with 104. % 2.11/2.31 >>>> Starting back demodulation with 106. % 2.11/2.31 >>>> Starting back demodulation with 108. % 2.11/2.31 >>>> Starting back demodulation with 111. % 2.11/2.31 >>>> Starting back demodulation with 114. % 2.11/2.31 >>>> Starting back demodulation with 116. % 2.11/2.31 >>>> Starting back demodulation with 119. % 2.11/2.31 >>>> Starting back demodulation with 121. % 2.11/2.31 >>>> Starting back demodulation with 123. % 2.11/2.31 >>>> Starting back demodulation with 125. % 2.11/2.31 ** KEPT (pick-wt=29): 196 [copy,126,flip.1] cons5(orb(andb(be_q(A,B),be_q(C,D)),andb(be_q(A,D),be_q(C,B))),bpath(B,D,E))=bpath(B,D,cons(pair2(A,C),E)). % 2.11/2.31 >>>> Starting back demodulation with 128. % 2.11/2.31 >>>> Starting back demodulation with 130. % 2.11/2.31 ** KEPT (pick-wt=19): 197 [copy,131,flip.1] andb(or2(bpath(A,B,C)),bpath2(cons3(B,D),C))=bpath2(cons3(A,cons3(B,D)),C). % 2.11/2.31 >>>> Starting back demodulation with 133. % 2.11/2.31 >>>> Starting back demodulation with 136. % 2.11/2.31 >>>> Starting back demodulation with 138. % 2.11/2.31 >>>> Starting back demodulation with 141. % 2.11/2.31 >>>> Starting back demodulation with 143. % 2.11/2.31 >>>> Starting back demodulation with 145. % 2.11/2.31 >>>> Starting back demodulation with 147. % 2.11/2.31 ** KEPT (pick-wt=45): 198 [copy,149,flip.1] andb(be_q(A,last(A,B)),andb(bpath2(cons3(A,B),bgraph(cons2(pair22(C,D),E))),andb(bunique(B),e_q(len(cons3(A,B)),add(two,maximum(aux(C,D,lt(C,D)),E))))))=btour(cons3(A,B),cons2(pair22(C,D),E)). % 2.11/2.31 >>>> Starting back demodulation with 151. % 2.11/2.31 ** KEPT (pick-wt=16): 199 [copy,152,flip.1] cons2(pair22(A,add(suc(B),A)),dodeca2(B,C))=dodeca2(B,cons4(A,C)). % 2.11/2.31 >>>> Starting back demodulation with 154. % 2.11/2.31 ** KEPT (pick-wt=22): 200 [copy,155,flip.1] cons2(pair22(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C))=dodeca3(A,cons4(B,C)). % 2.11/2.31 >>>> Starting back demodulation with 157. % 2.11/2.31 ** KEPT (pick-wt=23): 201 [copy,158,flip.1] cons2(pair22(add(suc(A),suc(B)),add(add(suc(A),suc(A)),B)),dodeca4(A,C))=dodeca4(A,cons4(B,C)). % 2.11/2.31 >>>> Starting back demodulation with 160. % 2.11/2.31 ** KEPT (pick-wt=28): 202 [copy,161,flip.1] cons2(pair22(add(add(suc(A),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),B)),dodeca5(A,C))=dodeca5(A,cons4(B,C)). % 2.11/2.31 >>>> Starting back demodulation with 163. % 2.11/2.31 ** KEPT (pick-wt=32): 203 [copy,164,flip.1] cons2(pair22(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,cons4(B,C)). % 2.11/2.31 >>>> Starting back demodulation with 166. % 2.11/2.31 >>>> Starting back demodulation with 168. % 2.11/2.31 >>>> Starting back demodulation with 170. % 2.11/2.31 >> back demodulating 1 with 170. % 2.11/2.31 >>>> Starting back demodulation with 172. % 2.11/2.31 >>>> Starting back demodulation with 174. % 2.11/2.31 >>>> Starting back demodulation with 176. % 2.11/2.31 >>>> Starting back demodulation with 178. % 2.11/2.31 >>>> Starting back demodulation with 180. % 2.11/2.31 >>>> Starting back demodulation with 182. % 2.11/2.31 >>>> Starting back demodulation with 184. % 2.11/2.31 >>>> Starting back demodulation with 186. % 2.11/2.31 >>>> Starting back demodulation with 188. % 2.11/2.31 >>>> Starting back demodulation with 190. % 2.11/2.31 Following clause subsumed by 56 during input processing: 0 [copy,191,flip.1] maximum(A,cons2(pair22(B,C),D))=maximum(aux(A,aux(B,C,lt(B,C)),lt(A,aux(B,C,lt(B,C)))),D). % 2.11/2.31 Following clause subsumed by 59 during input processing: 0 [copy,192,flip.1] len(cons3(A,B))=suc(len(B)). % 2.11/2.31 Following clause subsumed by 62 during input processing: 0 [copy,193,flip.1] last(A,cons3(B,C))=last(B,C). % 2.11/2.31 Following clause subsumed by 82 during input processing: 0 [copy,194,flip.1] dodeca(cons4(A,B))=cons2(pair22(A,suc(A)),dodeca(B)). % 2.11/2.31 Following clause subsumed by 90 during input processing: 0 [copy,195,flip.1] bgraph(cons2(pair22(A,B),C))=cons(pair2(bin(A),bin(B)),bgraph(C)). % 2.11/2.31 Following clause subsumed by 126 during input processing: 0 [copy,196,flip.1] bpath(A,B,cons(pair2(C,D),E))=cons5(orb(andb(be_q(C,A),be_q(D,B)),andb(be_q(C,B),be_q(D,A))),bpath(A,B,E)). % 2.11/2.31 Following clause subsumed by 131 during input processing: 0 [copy,197,flip.1] bpath2(cons3(A,cons3(B,C)),D)=andb(or2(bpath(A,B,D)),bpath2(cons3(B,C),D)). % 2.11/2.31 Following clause subsumed by 149 during input processing: 0 [copy,198,flip.1] btour(cons3(A,B),cons2(pair22(C,D),E))=andb(be_q(A,last(A,B)),andb(bpath2(cons3(A,B),bgraph(cons2(pair22(C,D),E))),andb(bunique(B),e_q(len(cons3(A,B)),add(two,maximum(aux(C,D,lt(C,D)),E)))))). % 2.11/2.31 Following clause subsumed by 152 during input processing: 0 [copy,199,flip.1] dodeca2(A,cons4(B,C))=cons2(pair22(B,add(suc(A),B)),dodeca2(A,C)). % 2.11/2.31 Following clause subsumed by 155 during input processing: 0 [copy,200,flip.1] dodeca3(A,cons4(B,C))=cons2(pair22(add(suc(A),B),add(add(suc(A),suc(A)),B)),dodeca3(A,C)). % 2.11/2.31 Following clause subsumed by 158 during input processing: 0 [copy,201,flip.1] dodeca4(A,cons4(B,C))=cons2(pair22(add(suc(A),suc(B)),add(add(suc(A),suc(A)),B)),dodeca4(A,C)). % 2.11/2.31 Following clause subsumed by 161 during input processing: 0 [copy,202,flip.1] dodeca5(A,cons4(B,C))=cons2(pair22(add(add(suc(A),suc(A)),B),add(add(add(suc(A),suc(A)),suc(A)),B)),dodeca5(A,C)). % 2.11/2.32 Following clause subsumed by 164 during input processing: 0 [copy,203,flip.1] dodeca6(A,cons4(B,C))=cons2(pair22(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.11/2.32 % 2.11/2.32 ======= end of input processing ======= % 2.11/2.32 % 2.11/2.32 =========== start of search =========== % 2.11/2.32 % 2.11/2.32 % 2.11/2.32 Resetting weight limit to 5. % 2.11/2.32 % 2.11/2.32 % 2.11/2.32 Resetting weight limit to 5. % 2.11/2.32 % 2.11/2.32 sos_size=70 % 2.11/2.32 % 2.11/2.32 Search stopped because sos empty. % 2.11/2.32 % 2.11/2.32 % 2.11/2.32 Search stopped because sos empty. % 2.11/2.32 % 2.11/2.32 ============ end of search ============ % 2.11/2.32 % 2.11/2.32 -------------- statistics ------------- % 2.11/2.32 clauses given 152 % 2.11/2.32 clauses generated 797 % 2.11/2.32 clauses kept 157 % 2.11/2.32 clauses forward subsumed 221 % 2.11/2.32 clauses back subsumed 0 % 2.11/2.32 Kbytes malloced 6835 % 2.11/2.32 % 2.11/2.32 ----------- times (seconds) ----------- % 2.11/2.32 user CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.11/2.32 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.11/2.32 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.11/2.32 % 2.11/2.32 Process 24027 finished Tue May 5 12:58:00 2026 % 2.11/2.32 Otter interrupted % 2.11/2.32 PROOF NOT FOUND %------------------------------------------------------------------------------