%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX218+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n027.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:26 PM UTC 2026 % Result : Unknown 15.63s 15.88s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX218+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.15/0.33 % Computer : n027.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue May 5 12:17:04 EDT 2026 % 0.15/0.33 % CPUTime : % 2.10/2.31 ----- Otter 3.3f, August 2004 ----- % 2.10/2.31 The process was started by sandbox on n027.cluster.edu, % 2.10/2.31 Tue May 5 12:17:04 2026 % 2.10/2.31 The command was "./otter". The process ID is 25246. % 2.10/2.31 % 2.10/2.31 set(prolog_style_variables). % 2.10/2.31 set(auto). % 2.10/2.31 dependent: set(auto1). % 2.10/2.31 dependent: set(process_input). % 2.10/2.31 dependent: clear(print_kept). % 2.10/2.31 dependent: clear(print_new_demod). % 2.10/2.31 dependent: clear(print_back_demod). % 2.10/2.31 dependent: clear(print_back_sub). % 2.10/2.31 dependent: set(control_memory). % 2.10/2.31 dependent: assign(max_mem, 12000). % 2.10/2.31 dependent: assign(pick_given_ratio, 4). % 2.10/2.31 dependent: assign(stats_level, 1). % 2.10/2.31 dependent: assign(max_seconds, 10800). % 2.10/2.31 clear(print_given). % 2.10/2.31 % 2.10/2.31 formula_list(usable). % 2.10/2.31 all A (A=A). % 2.10/2.31 all X X2 X3 (proj1tuple(tuple2(X,X2,X3))=X). % 2.10/2.31 all X X2 X3 (proj2tuple(tuple2(X,X2,X3))=X2). % 2.10/2.31 all X X2 X3 (proj3tuple(tuple2(X,X2,X3))=X3). % 2.10/2.31 all X X2 (proj1pair(pair22(X,X2))=X). % 2.10/2.31 all X X2 (proj2pair(pair22(X,X2))=X2). % 2.10/2.31 all X X2 (proj1pair2(pair23(X,X2))=X). % 2.10/2.31 all X X2 (proj2pair2(pair23(X,X2))=X2). % 2.10/2.31 all X X2 (proj1pair3(pair24(X,X2))=X). % 2.10/2.31 all X X2 (proj2pair3(pair24(X,X2))=X2). % 2.10/2.31 all X X2 (proj1pair4(pair25(X,X2))=X). % 2.10/2.31 all X X2 (proj2pair4(pair25(X,X2))=X2). % 2.10/2.31 all X X2 (head(cons(X,X2))=X). % 2.10/2.31 all X X2 (tail(cons(X,X2))=X2). % 2.10/2.31 all X X2 (nil!=cons(X,X2)). % 2.10/2.31 all X X2 (head2(cons2(X,X2))=X). % 2.10/2.31 all X X2 (tail2(cons2(X,X2))=X2). % 2.10/2.31 all X X2 (nil2!=cons2(X,X2)). % 2.10/2.31 all X (proj1Succ(succ(X))=X). % 2.10/2.31 all X (zero!=succ(X)). % 2.10/2.31 all X (proj1Left(left(X))=X). % 2.10/2.31 all X (proj1Right(right(X))=X). % 2.10/2.31 all X X2 (left(X)!=right(X2)). % 2.10/2.31 all X (proj1Lft(lft(X))=X). % 2.10/2.31 all X (proj1Rgt(rgt(X))=X). % 2.10/2.31 all X X2 (lft(X)!=rgt(X2)). % 2.10/2.31 all X (lft(X)!=stp). % 2.10/2.31 all X (rgt(X)!=stp). % 2.10/2.31 o!=a2. % 2.10/2.31 o!=b. % 2.10/2.31 a2!=b. % 2.10/2.31 split(nil2)=pair24(o,nil2). % 2.10/2.31 all Y Xs (split(cons2(Y,Xs))=pair24(Y,Xs)). % 2.10/2.31 all Y (rev(nil2,Y)=Y). % 2.10/2.31 all Y Z Xs (Z!=o->rev(cons2(Z,Xs),Y)=rev(Xs,cons2(Z,Y))). % 2.10/2.31 all Y Xs (rev(cons2(o,Xs),Y)=Y). % 2.10/2.31 one=succ(zero). % 2.10/2.31 two=succ(one). % 2.10/2.31 all Y (apply(nil,Y)=pair25(o,stp)). % 2.10/2.31 all Y Q Sa Rhs (Sa=Y->apply(cons(pair22(Sa,Rhs),Q),Y)=Rhs). % 2.10/2.31 all Y Q Sa Rhs (Sa!=Y->apply(cons(pair22(Sa,Rhs),Q),Y)=apply(Q,Y)). % 2.10/2.31 all Y Z X2 S Y1 Lft1 (split(Y)=pair24(Y1,Lft1)->act(lft(S),Y,Z,X2)=right(tuple2(S,Lft1,cons2(Y1,cons2(Z,X2))))). % 2.10/2.31 all Y Z X2 T (act(rgt(T),Y,Z,X2)=right(tuple2(T,cons2(Z,Y),X2))). % 2.10/2.31 all Y Z X2 (act(stp,Y,Z,X2)=left(rev(Y,cons2(Z,X2)))). % 2.10/2.31 all X S Lft Rgt X1 Rgt2 X12 What1 (split(Rgt)=pair24(X1,Rgt2)-> (apply(X,pair23(S,X1))=pair25(X12,What1)->step(X,tuple2(S,Lft,Rgt))=act(What1,Lft,X12,Rgt2))). % 2.10/2.31 all X Y Tape (step(X,Y)=left(Tape)->steps(X,Y)=Tape). % 2.10/2.31 all X Y St (step(X,Y)=right(St)->steps(X,Y)=steps(X,St)). % 2.10/2.31 all X Y (runt(X,Y)=steps(X,tuple2(zero,nil2,Y))). % 2.10/2.31 all X (runt(X,cons2(a2,nil2))=nil2-> -prog0(X)). % 2.10/2.31 all X Y Z (runt(X,cons2(a2,nil2))=cons2(Y,Z)-> (Y!=a2-> -prog0(X))). % 2.10/2.31 all X (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=nil2-> -prog0(X))). % 2.10/2.31 all X X2 X3 (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(X2,X3)-> (X2!=a2-> -prog0(X)))). % 2.10/2.31 all X (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,nil2)-> -prog0(X))). % 2.10/2.31 all X X4 X5 (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(X4,X5))-> (X4!=a2-> -prog0(X)))). % 2.10/2.31 all X (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,nil2))-> -prog0(X))). % 2.10/2.31 all X X6 X7 (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(X6,X7)))-> (X6!=a2-> -prog0(X)))). % 2.10/2.31 all X (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(a2,nil2)))-> -prog0(X))). % 2.10/2.31 all X X8 X9 (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(a2,cons2(X8,X9))))-> (X8!=a2-> -prog0(X)))). % 2.10/2.31 all X (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2))))-> -prog0(X))). % 2.10/2.31 all X X10 X11 (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(X10,X11)))))-> (X10!=b-> -prog0(X)))). % 2.10/2.31 all X (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))-> -prog0(X))). % 2.10/2.31 all X X12 X13 (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(X12,X13))))))-> (X12!=b-> -prog0(X)))). % 2.10/2.31 all X (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2))))))->prog0(X))). % 2.10/2.31 all X X14 X15 (runt(X,cons2(a2,nil2))=cons2(a2,nil2)-> (runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(X14,X15)))))))-> -prog0(X))). % 2.10/2.31 all X X16 X17 (runt(X,cons2(a2,nil2))=cons2(a2,cons2(X16,X17))-> -prog0(X)). % 2.10/2.31 -(exists X Y Z V W prog0(cons(pair22(pair23(zero,a2),X),cons(pair22(pair23(zero,b),Y),cons(pair22(pair23(one,a2),Z),cons(pair22(pair23(one,b),V),cons(pair22(pair23(two,a2),W),nil))))))). % 2.10/2.31 end_of_list. % 2.10/2.31 % 2.10/2.31 -------> usable clausifies to: % 2.10/2.31 % 2.10/2.31 list(usable). % 2.10/2.31 0 [] A=A. % 2.10/2.31 0 [] proj1tuple(tuple2(X,X2,X3))=X. % 2.10/2.31 0 [] proj2tuple(tuple2(X,X2,X3))=X2. % 2.10/2.31 0 [] proj3tuple(tuple2(X,X2,X3))=X3. % 2.10/2.31 0 [] proj1pair(pair22(X,X2))=X. % 2.10/2.31 0 [] proj2pair(pair22(X,X2))=X2. % 2.10/2.31 0 [] proj1pair2(pair23(X,X2))=X. % 2.10/2.31 0 [] proj2pair2(pair23(X,X2))=X2. % 2.10/2.31 0 [] proj1pair3(pair24(X,X2))=X. % 2.10/2.31 0 [] proj2pair3(pair24(X,X2))=X2. % 2.10/2.31 0 [] proj1pair4(pair25(X,X2))=X. % 2.10/2.31 0 [] proj2pair4(pair25(X,X2))=X2. % 2.10/2.31 0 [] head(cons(X,X2))=X. % 2.10/2.31 0 [] tail(cons(X,X2))=X2. % 2.10/2.31 0 [] nil!=cons(X,X2). % 2.10/2.31 0 [] head2(cons2(X,X2))=X. % 2.10/2.31 0 [] tail2(cons2(X,X2))=X2. % 2.10/2.31 0 [] nil2!=cons2(X,X2). % 2.10/2.31 0 [] proj1Succ(succ(X))=X. % 2.10/2.31 0 [] zero!=succ(X). % 2.10/2.31 0 [] proj1Left(left(X))=X. % 2.10/2.31 0 [] proj1Right(right(X))=X. % 2.10/2.31 0 [] left(X)!=right(X2). % 2.10/2.31 0 [] proj1Lft(lft(X))=X. % 2.10/2.31 0 [] proj1Rgt(rgt(X))=X. % 2.10/2.31 0 [] lft(X)!=rgt(X2). % 2.10/2.31 0 [] lft(X)!=stp. % 2.10/2.31 0 [] rgt(X)!=stp. % 2.10/2.31 0 [] o!=a2. % 2.10/2.31 0 [] o!=b. % 2.10/2.31 0 [] a2!=b. % 2.10/2.31 0 [] split(nil2)=pair24(o,nil2). % 2.10/2.31 0 [] split(cons2(Y,Xs))=pair24(Y,Xs). % 2.10/2.31 0 [] rev(nil2,Y)=Y. % 2.10/2.31 0 [] Z=o|rev(cons2(Z,Xs),Y)=rev(Xs,cons2(Z,Y)). % 2.10/2.31 0 [] rev(cons2(o,Xs),Y)=Y. % 2.10/2.31 0 [] one=succ(zero). % 2.10/2.31 0 [] two=succ(one). % 2.10/2.31 0 [] apply(nil,Y)=pair25(o,stp). % 2.10/2.31 0 [] Sa!=Y|apply(cons(pair22(Sa,Rhs),Q),Y)=Rhs. % 2.10/2.31 0 [] Sa=Y|apply(cons(pair22(Sa,Rhs),Q),Y)=apply(Q,Y). % 2.10/2.31 0 [] split(Y)!=pair24(Y1,Lft1)|act(lft(S),Y,Z,X2)=right(tuple2(S,Lft1,cons2(Y1,cons2(Z,X2)))). % 2.10/2.31 0 [] act(rgt(T),Y,Z,X2)=right(tuple2(T,cons2(Z,Y),X2)). % 2.10/2.31 0 [] act(stp,Y,Z,X2)=left(rev(Y,cons2(Z,X2))). % 2.10/2.31 0 [] split(Rgt)!=pair24(X1,Rgt2)|apply(X,pair23(S,X1))!=pair25(X12,What1)|step(X,tuple2(S,Lft,Rgt))=act(What1,Lft,X12,Rgt2). % 2.10/2.31 0 [] step(X,Y)!=left(Tape)|steps(X,Y)=Tape. % 2.10/2.31 0 [] step(X,Y)!=right(St)|steps(X,Y)=steps(X,St). % 2.10/2.31 0 [] runt(X,Y)=steps(X,tuple2(zero,nil2,Y)). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=nil2| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(Y,Z)|Y=a2| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=nil2| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(X2,X3)|X2=a2| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,nil2)| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(X4,X5))|X4=a2| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,nil2))| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(X6,X7)))|X6=a2| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,nil2)))| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(X8,X9))))|X8=a2| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2))))| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(X10,X11)))))|X10=b| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(X12,X13))))))|X12=b| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2))))))|prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,nil2)|runt(X,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(X14,X15)))))))| -prog0(X). % 2.10/2.31 0 [] runt(X,cons2(a2,nil2))!=cons2(a2,cons2(X16,X17))| -prog0(X). % 2.10/2.31 0 [] -prog0(cons(pair22(pair23(zero,a2),X),cons(pair22(pair23(zero,b),Y),cons(pair22(pair23(one,a2),Z),cons(pair22(pair23(one,b),V),cons(pair22(pair23(two,a2),W),nil)))))). % 2.10/2.31 end_of_list. % 2.10/2.31 % 2.10/2.31 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4. % 2.10/2.31 % 2.10/2.31 This ia a non-Horn set with equality. The strategy will be % 2.10/2.31 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.10/2.31 deletion, with positive clauses in sos and nonpositive % 2.10/2.31 clauses in usable. % 2.10/2.31 % 2.10/2.31 dependent: set(knuth_bendix). % 2.10/2.31 dependent: set(anl_eq). % 2.10/2.31 dependent: set(para_from). % 2.10/2.31 dependent: set(para_into). % 2.10/2.31 dependent: clear(para_from_right). % 2.10/2.31 dependent: clear(para_into_right). % 2.10/2.31 dependent: set(para_from_vars). % 2.10/2.31 dependent: set(eq_units_both_ways). % 2.10/2.31 dependent: set(dynamic_demod_all). % 2.10/2.31 dependent: set(dynamic_demod). % 2.10/2.31 dependent: set(order_eq). % 2.10/2.31 dependent: set(back_demod). % 2.10/2.31 dependent: set(lrpo). % 2.10/2.31 dependent: set(hyper_res). % 2.10/2.31 dependent: set(unit_deletion). % 2.10/2.31 dependent: set(factor). % 2.10/2.31 % 2.10/2.31 ------------> process usable: % 2.10/2.31 ** KEPT (pick-wt=5): 2 [copy,1,flip.1] cons(A,B)!=nil. % 2.10/2.31 ** KEPT (pick-wt=5): 4 [copy,3,flip.1] cons2(A,B)!=nil2. % 2.10/2.31 ** KEPT (pick-wt=4): 6 [copy,5,flip.1] succ(A)!=zero. % 2.10/2.31 ** KEPT (pick-wt=5): 7 [] left(A)!=right(B). % 2.10/2.31 ** KEPT (pick-wt=5): 8 [] lft(A)!=rgt(B). % 2.10/2.31 ** KEPT (pick-wt=4): 9 [] lft(A)!=stp. % 2.10/2.31 ** KEPT (pick-wt=4): 10 [] rgt(A)!=stp. % 2.10/2.31 ** KEPT (pick-wt=3): 11 [] o!=a2. % 2.10/2.31 ** KEPT (pick-wt=3): 12 [] o!=b. % 2.10/2.31 ** KEPT (pick-wt=3): 14 [copy,13,flip.1] b!=a2. % 2.10/2.31 ** KEPT (pick-wt=12): 15 [] A!=B|apply(cons(pair22(A,C),D),B)=C. % 2.10/2.31 ** KEPT (pick-wt=22): 16 [] split(A)!=pair24(B,C)|act(lft(D),A,E,F)=right(tuple2(D,C,cons2(B,cons2(E,F)))). % 2.10/2.31 ** KEPT (pick-wt=27): 17 [] split(A)!=pair24(B,C)|apply(D,pair23(E,B))!=pair25(F,G)|step(D,tuple2(E,H,A))=act(G,H,F,C). % 2.10/2.31 ** KEPT (pick-wt=11): 18 [] step(A,B)!=left(C)|steps(A,B)=C. % 2.10/2.31 ** KEPT (pick-wt=13): 19 [] step(A,B)!=right(C)|steps(A,B)=steps(A,C). % 2.10/2.31 ** KEPT (pick-wt=9): 20 [] runt(A,cons2(a2,nil2))!=nil2| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=14): 21 [] runt(A,cons2(a2,nil2))!=cons2(B,C)|B=a2| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=28): 22 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=nil2| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=33): 23 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(B,C)|B=a2| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=30): 24 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,nil2)| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=35): 25 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(B,C))|B=a2| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=32): 26 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,nil2))| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=37): 27 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(B,C)))|B=a2| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=34): 28 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,nil2)))| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=39): 29 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(B,C))))|B=a2| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=36): 30 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,nil2))))| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=41): 31 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(B,C)))))|B=b| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=38): 32 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=43): 33 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(B,C))))))|B=b| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=40): 34 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,nil2))))))|prog0(A). % 2.10/2.31 ** KEPT (pick-wt=42): 35 [] runt(A,cons2(a2,nil2))!=cons2(a2,nil2)|runt(A,cons2(b,cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,nil2)))))))!=cons2(a2,cons2(a2,cons2(a2,cons2(a2,cons2(b,cons2(b,cons2(B,C)))))))| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=13): 36 [] runt(A,cons2(a2,nil2))!=cons2(a2,cons2(B,C))| -prog0(A). % 2.10/2.31 ** KEPT (pick-wt=32): 37 [] -prog0(cons(pair22(pair23(zero,a2),A),cons(pair22(pair23(zero,b),B),cons(pair22(pair23(one,a2),C),cons(pair22(pair23(one,b),D),cons(pair22(pair23(two,a2),E),nil)))))). % 2.10/2.31 ** KEPT (pick-wt=5): 38 [copy,7,flip.1] right(A)!=left(B). % 2.10/2.31 ** KEPT (pick-wt=5): 39 [copy,8,flip.1] rgt(A)!=lft(B). % 2.10/2.31 Following clause subsumed by 7 during input processing: 0 [copy,38,flip.1] left(A)!=right(B). % 2.10/2.31 Following clause subsumed by 8 during input processing: 0 [copy,39,flip.1] lft(A)!=rgt(B). % 2.10/2.31 % 2.10/2.31 ------------> process sos: % 2.10/2.31 ** KEPT (pick-wt=3): 40 [] A=A. % 2.10/2.31 ** KEPT (pick-wt=7): 41 [] proj1tuple(tuple2(A,B,C))=A. % 2.10/2.31 ---> New Demodulator: 42 [new_demod,41] proj1tuple(tuple2(A,B,C))=A. % 2.10/2.31 ** KEPT (pick-wt=7): 43 [] proj2tuple(tuple2(A,B,C))=B. % 2.10/2.31 ---> New Demodulator: 44 [new_demod,43] proj2tuple(tuple2(A,B,C))=B. % 2.10/2.31 ** KEPT (pick-wt=7): 45 [] proj3tuple(tuple2(A,B,C))=C. % 2.10/2.31 ---> New Demodulator: 46 [new_demod,45] proj3tuple(tuple2(A,B,C))=C. % 2.10/2.31 ** KEPT (pick-wt=6): 47 [] proj1pair(pair22(A,B))=A. % 2.10/2.31 ---> New Demodulator: 48 [new_demod,47] proj1pair(pair22(A,B))=A. % 2.10/2.31 ** KEPT (pick-wt=6): 49 [] proj2pair(pair22(A,B))=B. % 2.10/2.31 ---> New Demodulator: 50 [new_demod,49] proj2pair(pair22(A,B))=B. % 2.10/2.31 ** KEPT (pick-wt=6): 51 [] proj1pair2(pair23(A,B))=A. % 2.10/2.31 ---> New Demodulator: 52 [new_demod,51] proj1pair2(pair23(A,B))=A. % 2.10/2.31 ** KEPT (pick-wt=6): 53 [] proj2pair2(pair23(A,B))=B. % 2.10/2.31 ---> New Demodulator: 54 [new_demod,53] proj2pair2(pair23(A,B))=B. % 2.10/2.31 ** KEPT (pick-wt=6): 55 [] proj1pair3(pair24(A,B))=A. % 2.10/2.31 ---> New Demodulator: 56 [new_demod,55] proj1pair3(pair24(A,B))=A. % 2.10/2.31 ** KEPT (pick-wt=6): 57 [] proj2pair3(pair24(A,B))=B. % 2.10/2.31 ---> New Demodulator: 58 [new_demod,57] proj2pair3(pair24(A,B))=B. % 2.10/2.31 ** KEPT (pick-wt=6): 59 [] proj1pair4(pair25(A,B))=A. % 2.10/2.31 ---> New Demodulator: 60 [new_demod,59] proj1pair4(pair25(A,B))=A. % 2.10/2.31 ** KEPT (pick-wt=6): 61 [] proj2pair4(pair25(A,B))=B. % 2.10/2.31 ---> New Demodulator: 62 [new_demod,61] proj2pair4(pair25(A,B))=B. % 2.10/2.31 ** KEPT (pick-wt=6): 63 [] head(cons(A,B))=A. % 2.10/2.31 ---> New Demodulator: 64 [new_demod,63] head(cons(A,B))=A. % 2.43/2.62 ** KEPT (pick-wt=6): 65 [] tail(cons(A,B))=B. % 2.43/2.62 ---> New Demodulator: 66 [new_demod,65] tail(cons(A,B))=B. % 2.43/2.62 ** KEPT (pick-wt=6): 67 [] head2(cons2(A,B))=A. % 2.43/2.62 ---> New Demodulator: 68 [new_demod,67] head2(cons2(A,B))=A. % 2.43/2.62 ** KEPT (pick-wt=6): 69 [] tail2(cons2(A,B))=B. % 2.43/2.62 ---> New Demodulator: 70 [new_demod,69] tail2(cons2(A,B))=B. % 2.43/2.62 ** KEPT (pick-wt=5): 71 [] proj1Succ(succ(A))=A. % 2.43/2.62 ---> New Demodulator: 72 [new_demod,71] proj1Succ(succ(A))=A. % 2.43/2.62 ** KEPT (pick-wt=5): 73 [] proj1Left(left(A))=A. % 2.43/2.62 ---> New Demodulator: 74 [new_demod,73] proj1Left(left(A))=A. % 2.43/2.62 ** KEPT (pick-wt=5): 75 [] proj1Right(right(A))=A. % 2.43/2.62 ---> New Demodulator: 76 [new_demod,75] proj1Right(right(A))=A. % 2.43/2.62 ** KEPT (pick-wt=5): 77 [] proj1Lft(lft(A))=A. % 2.43/2.62 ---> New Demodulator: 78 [new_demod,77] proj1Lft(lft(A))=A. % 2.43/2.62 ** KEPT (pick-wt=5): 79 [] proj1Rgt(rgt(A))=A. % 2.43/2.62 ---> New Demodulator: 80 [new_demod,79] proj1Rgt(rgt(A))=A. % 2.43/2.62 ** KEPT (pick-wt=6): 81 [] split(nil2)=pair24(o,nil2). % 2.43/2.62 ---> New Demodulator: 82 [new_demod,81] split(nil2)=pair24(o,nil2). % 2.43/2.62 ** KEPT (pick-wt=8): 83 [] split(cons2(A,B))=pair24(A,B). % 2.43/2.62 ---> New Demodulator: 84 [new_demod,83] split(cons2(A,B))=pair24(A,B). % 2.43/2.62 ** KEPT (pick-wt=5): 85 [] rev(nil2,A)=A. % 2.43/2.62 ---> New Demodulator: 86 [new_demod,85] rev(nil2,A)=A. % 2.43/2.62 ** KEPT (pick-wt=14): 87 [] A=o|rev(cons2(A,B),C)=rev(B,cons2(A,C)). % 2.43/2.62 ** KEPT (pick-wt=7): 88 [] rev(cons2(o,A),B)=B. % 2.43/2.62 ---> New Demodulator: 89 [new_demod,88] rev(cons2(o,A),B)=B. % 2.43/2.62 ** KEPT (pick-wt=4): 91 [copy,90,flip.1] succ(zero)=one. % 2.43/2.62 ---> New Demodulator: 92 [new_demod,91] succ(zero)=one. % 2.43/2.62 ** KEPT (pick-wt=4): 94 [copy,93,flip.1] succ(one)=two. % 2.43/2.62 ---> New Demodulator: 95 [new_demod,94] succ(one)=two. % 2.43/2.62 ** KEPT (pick-wt=7): 96 [] apply(nil,A)=pair25(o,stp). % 2.43/2.62 ** KEPT (pick-wt=14): 97 [] A=B|apply(cons(pair22(A,C),D),B)=apply(D,B). % 2.43/2.62 ** KEPT (pick-wt=14): 99 [copy,98,flip.1] right(tuple2(A,cons2(B,C),D))=act(rgt(A),C,B,D). % 2.43/2.62 ---> New Demodulator: 100 [new_demod,99] right(tuple2(A,cons2(B,C),D))=act(rgt(A),C,B,D). % 2.43/2.62 ** KEPT (pick-wt=12): 102 [copy,101,flip.1] left(rev(A,cons2(B,C)))=act(stp,A,B,C). % 2.43/2.62 ---> New Demodulator: 103 [new_demod,102] left(rev(A,cons2(B,C)))=act(stp,A,B,C). % 2.43/2.62 ** KEPT (pick-wt=10): 105 [copy,104,flip.1] steps(A,tuple2(zero,nil2,B))=runt(A,B). % 2.43/2.62 ---> New Demodulator: 106 [new_demod,105] steps(A,tuple2(zero,nil2,B))=runt(A,B). % 2.43/2.62 Following clause subsumed by 40 during input processing: 0 [copy,40,flip.1] A=A. % 2.43/2.62 >>>> Starting back demodulation with 42. % 2.43/2.62 >>>> Starting back demodulation with 44. % 2.43/2.62 >>>> Starting back demodulation with 46. % 2.43/2.62 >>>> Starting back demodulation with 48. % 2.43/2.62 >>>> Starting back demodulation with 50. % 2.43/2.62 >>>> Starting back demodulation with 52. % 2.43/2.62 >>>> Starting back demodulation with 54. % 2.43/2.62 >>>> Starting back demodulation with 56. % 2.43/2.62 >>>> Starting back demodulation with 58. % 2.43/2.62 >>>> Starting back demodulation with 60. % 2.43/2.62 >>>> Starting back demodulation with 62. % 2.43/2.62 >>>> Starting back demodulation with 64. % 2.43/2.62 >>>> Starting back demodulation with 66. % 2.43/2.62 >>>> Starting back demodulation with 68. % 2.43/2.62 >>>> Starting back demodulation with 70. % 2.43/2.62 >>>> Starting back demodulation with 72. % 2.43/2.62 >>>> Starting back demodulation with 74. % 2.43/2.62 >>>> Starting back demodulation with 76. % 2.43/2.62 >>>> Starting back demodulation with 78. % 2.43/2.62 >>>> Starting back demodulation with 80. % 2.43/2.62 >>>> Starting back demodulation with 82. % 2.43/2.62 >>>> Starting back demodulation with 84. % 2.43/2.62 >>>> Starting back demodulation with 86. % 2.43/2.62 >>>> Starting back demodulation with 89. % 2.43/2.62 >>>> Starting back demodulation with 92. % 2.43/2.62 >>>> Starting back demodulation with 95. % 2.43/2.62 ** KEPT (pick-wt=7): 107 [copy,96,flip.1] pair25(o,stp)=apply(nil,A). % 2.43/2.62 >>>> Starting back demodulation with 100. % 2.43/2.62 >>>> Starting back demodulation with 103. % 2.43/2.62 >>>> Starting back demodulation with 106. % 2.43/2.62 Following clause subsumed by 96 during input processing: 0 [copy,107,flip.1] apply(nil,A)=pair25(o,stp). % 2.43/2.62 % 2.43/2.62 ======= end of input processing ======= % 2.43/2.62 % 2.43/2.62 =========== start of search =========== % 2.43/2.62 % 2.43/2.62 % 2.43/2.62 Resetting weight limit to 16. % 2.43/2.62 % 2.43/2.62 % 2.43/2.62 Resetting weight limit to 16. % 2.43/2.62 % 2.43/2.62 sos_size=664 % 2.43/2.62 % 2.43/2.62 % 2.43/2.62 Resetting weight limit to 15. % 2.43/2.62 % 2.43/2.62 % 2.43/2.62 Resetting weight limit to 15. % 2.43/2.62 % 2.43/2.62 sos_size=702 % 2.43/2.62 % 2.43/2.62 % 2.43/2.62 Resetting weight limit to 14. % 2.43/2.62 % 2.43/2.62 % 2.43/2.62 Resetting weight limit to 14. % 2.43/2.62 % 2.43/2.62 sos_size=612 % 2.43/2.62 % 2.43/2.62 % 2.43/2.62 Resetting weight limit to 12. % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 12. % 15.63/15.88 % 15.63/15.88 sos_size=682 % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 11. % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 11. % 15.63/15.88 % 15.63/15.88 sos_size=766 % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 10. % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 10. % 15.63/15.88 % 15.63/15.88 sos_size=909 % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 9. % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 9. % 15.63/15.88 % 15.63/15.88 sos_size=820 % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 8. % 15.63/15.88 % 15.63/15.88 % 15.63/15.88 Resetting weight limit to 8. % 15.63/15.88 % 15.63/15.88 sos_size=822 % 15.63/15.88 % 15.63/15.88 Search stopped in tp_alloc by max_mem option. % 15.63/15.88 % 15.63/15.88 Search stopped in tp_alloc by max_mem option. % 15.63/15.88 % 15.63/15.88 ============ end of search ============ % 15.63/15.88 % 15.63/15.88 -------------- statistics ------------- % 15.63/15.88 clauses given 1213 % 15.63/15.88 clauses generated 888138 % 15.63/15.88 clauses kept 1731 % 15.63/15.88 clauses forward subsumed 11024 % 15.63/15.88 clauses back subsumed 425 % 15.63/15.88 Kbytes malloced 11718 % 15.63/15.88 % 15.63/15.88 ----------- times (seconds) ----------- % 15.63/15.88 user CPU time 13.56 (0 hr, 0 min, 13 sec) % 15.63/15.88 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 15.63/15.88 wall-clock time 16 (0 hr, 0 min, 16 sec) % 15.63/15.88 % 15.63/15.88 Process 25246 finished Tue May 5 12:17:20 2026 % 15.63/15.88 Otter interrupted % 15.63/15.88 PROOF NOT FOUND %------------------------------------------------------------------------------