%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : SWX222+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n026.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:27 PM UTC 2026
% Result : Theorem 1.95s 2.19s
% Output : Refutation 1.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 7
% Syntax : Number of clauses : 13 ( 9 unt; 0 nHn; 5 RR)
% Number of literals : 18 ( 4 equ; 6 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 23 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(27,axiom,
( nf(lam(A))
| ~ nf(A) ),
file('SWX222+1.p',unknown),
[] ).
cnf(34,axiom,
( tc(A,lam(B),arr(C,D))
| ~ tc(cons(C,A),B,D) ),
file('SWX222+1.p',unknown),
[] ).
cnf(37,axiom,
( index(A,B) != just(C)
| tc(A,var(B),D)
| C != D ),
file('SWX222+1.p',unknown),
[] ).
cnf(38,axiom,
( ~ nf(A)
| ~ tc(nil,A,arr(a,arr(b,b))) ),
file('SWX222+1.p',unknown),
[] ).
cnf(66,axiom,
proj1Var(var(A)) = A,
file('SWX222+1.p',unknown),
[] ).
cnf(67,axiom,
nf(var(A)),
file('SWX222+1.p',unknown),
[] ).
cnf(70,axiom,
index(cons(A,B),zero) = just(A),
file('SWX222+1.p',unknown),
[] ).
cnf(75,plain,
nf(lam(var(A))),
inference(hyper,[status(thm)],[67,27]),
[iquote('hyper,67,27')] ).
cnf(78,plain,
nf(lam(lam(var(A)))),
inference(hyper,[status(thm)],[75,27]),
[iquote('hyper,75,27')] ).
cnf(131,plain,
tc(cons(A,B),var(zero),A),
inference(demod,[status(thm),theory(equality)],[inference(hyper,[status(thm)],[70,37,66]),66]),
[iquote('hyper,70,37,65,demod,66')] ).
cnf(140,plain,
tc(A,lam(var(zero)),arr(B,B)),
inference(hyper,[status(thm)],[131,34]),
[iquote('hyper,131,34')] ).
cnf(194,plain,
tc(A,lam(lam(var(zero))),arr(B,arr(C,C))),
inference(hyper,[status(thm)],[140,34]),
[iquote('hyper,140,34')] ).
cnf(486,plain,
$false,
inference(hyper,[status(thm)],[194,38,78]),
[iquote('hyper,194,38,78')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX222+1 : TPTP v9.3.0. Released v9.3.0.
% 0.13/0.13 % Command : otter-tptp-script %s
% 0.16/0.34 % Computer : n026.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 12:33:53 EDT 2026
% 0.16/0.35 % CPUTime :
% 1.95/2.16 ----- Otter 3.3f, August 2004 -----
% 1.95/2.16 The process was started by sandbox2 on n026.cluster.edu,
% 1.95/2.16 Tue May 5 12:33:53 2026
% 1.95/2.16 The command was "./otter". The process ID is 31683.
% 1.95/2.16
% 1.95/2.16 set(prolog_style_variables).
% 1.95/2.16 set(auto).
% 1.95/2.16 dependent: set(auto1).
% 1.95/2.16 dependent: set(process_input).
% 1.95/2.16 dependent: clear(print_kept).
% 1.95/2.16 dependent: clear(print_new_demod).
% 1.95/2.16 dependent: clear(print_back_demod).
% 1.95/2.16 dependent: clear(print_back_sub).
% 1.95/2.16 dependent: set(control_memory).
% 1.95/2.16 dependent: assign(max_mem, 12000).
% 1.95/2.16 dependent: assign(pick_given_ratio, 4).
% 1.95/2.16 dependent: assign(stats_level, 1).
% 1.95/2.16 dependent: assign(max_seconds, 10800).
% 1.95/2.16 clear(print_given).
% 1.95/2.16
% 1.95/2.16 formula_list(usable).
% 1.95/2.16 all A (A=A).
% 1.95/2.16 all X X2 (head(cons(X,X2))=X).
% 1.95/2.16 all X X2 (tail(cons(X,X2))=X2).
% 1.95/2.16 all X X2 (nil!=cons(X,X2)).
% 1.95/2.16 all X X2 (proj1Arr(arr(X,X2))=X).
% 1.95/2.16 all X X2 (proj2Arr(arr(X,X2))=X2).
% 1.95/2.16 all X X2 (arr(X,X2)!=a).
% 1.95/2.16 all X X2 (arr(X,X2)!=b).
% 1.95/2.16 all X X2 (arr(X,X2)!=c).
% 1.95/2.16 a!=b.
% 1.95/2.16 a!=c.
% 1.95/2.16 b!=c.
% 1.95/2.16 all X (proj1Suc(suc(X))=X).
% 1.95/2.16 all X (zero!=suc(X)).
% 1.95/2.16 all X (proj1Just(just(X))=X).
% 1.95/2.16 all X (nothing!=just(X)).
% 1.95/2.16 all X X2 X3 (proj1App(app(X,X2,X3))=X).
% 1.95/2.16 all X X2 X3 (proj2App(app(X,X2,X3))=X2).
% 1.95/2.16 all X X2 X3 (proj3App(app(X,X2,X3))=X3).
% 1.95/2.16 all X (proj1Lam(lam(X))=X).
% 1.95/2.16 all X (proj1Var(var(X))=X).
% 1.95/2.16 all X X2 X3 X4 (app(X,X2,X3)!=lam(X4)).
% 1.95/2.16 all X X2 X3 X4 (app(X,X2,X3)!=var(X4)).
% 1.95/2.16 all X X2 (lam(X)!=var(X2)).
% 1.95/2.16 all Y Z X2 (Y!=lam(proj1Lam(Y))-> (nf(app(Y,Z,X2))<->nf(Y)&nf(Z))).
% 1.95/2.16 all Z X2 X3 (-nf(app(lam(X3),Z,X2))).
% 1.95/2.16 all E (nf(lam(E))<->nf(E)).
% 1.95/2.16 all X4 nf(var(X4)).
% 1.95/2.16 all Y (index(nil,Y)=nothing).
% 1.95/2.16 all Z Xs (index(cons(Z,Xs),zero)=just(Z)).
% 1.95/2.16 all Z Xs N (index(cons(Z,Xs),suc(N))=index(Xs,N)).
% 1.95/2.16 all X Z F X2 Tx (tc(X,app(F,X2,Tx),Z)<->tc(X,F,arr(Tx,Z))&tc(X,X2,Tx)).
% 1.95/2.16 all X Z E (Z!=arr(proj1Arr(Z),proj2Arr(Z))-> -tc(X,lam(E),Z)).
% 1.95/2.16 all X E Tx2 T1 (tc(X,lam(E),arr(Tx2,T1))<->tc(cons(Tx2,X),E,T1)).
% 1.95/2.16 all X Z X3 (index(X,X3)=nothing-> -tc(X,var(X3),Z)).
% 1.95/2.16 all X Z X3 Tx3 (index(X,X3)=just(Tx3)-> (tc(X,var(X3),Z)<->Tx3=Z)).
% 1.95/2.16 -(exists E (nf(E)&tc(nil,E,arr(a,arr(b,b))))).
% 1.95/2.16 end_of_list.
% 1.95/2.16
% 1.95/2.16 -------> usable clausifies to:
% 1.95/2.16
% 1.95/2.16 list(usable).
% 1.95/2.16 0 [] A=A.
% 1.95/2.16 0 [] head(cons(X,X2))=X.
% 1.95/2.16 0 [] tail(cons(X,X2))=X2.
% 1.95/2.16 0 [] nil!=cons(X,X2).
% 1.95/2.16 0 [] proj1Arr(arr(X,X2))=X.
% 1.95/2.16 0 [] proj2Arr(arr(X,X2))=X2.
% 1.95/2.16 0 [] arr(X,X2)!=a.
% 1.95/2.16 0 [] arr(X,X2)!=b.
% 1.95/2.16 0 [] arr(X,X2)!=c.
% 1.95/2.16 0 [] a!=b.
% 1.95/2.16 0 [] a!=c.
% 1.95/2.16 0 [] b!=c.
% 1.95/2.16 0 [] proj1Suc(suc(X))=X.
% 1.95/2.16 0 [] zero!=suc(X).
% 1.95/2.16 0 [] proj1Just(just(X))=X.
% 1.95/2.16 0 [] nothing!=just(X).
% 1.95/2.16 0 [] proj1App(app(X,X2,X3))=X.
% 1.95/2.16 0 [] proj2App(app(X,X2,X3))=X2.
% 1.95/2.16 0 [] proj3App(app(X,X2,X3))=X3.
% 1.95/2.16 0 [] proj1Lam(lam(X))=X.
% 1.95/2.16 0 [] proj1Var(var(X))=X.
% 1.95/2.16 0 [] app(X,X2,X3)!=lam(X4).
% 1.95/2.16 0 [] app(X,X2,X3)!=var(X4).
% 1.95/2.16 0 [] lam(X)!=var(X2).
% 1.95/2.16 0 [] Y=lam(proj1Lam(Y))| -nf(app(Y,Z,X2))|nf(Y).
% 1.95/2.16 0 [] Y=lam(proj1Lam(Y))| -nf(app(Y,Z,X2))|nf(Z).
% 1.95/2.16 0 [] Y=lam(proj1Lam(Y))|nf(app(Y,Z,X2))| -nf(Y)| -nf(Z).
% 1.95/2.16 0 [] -nf(app(lam(X3),Z,X2)).
% 1.95/2.16 0 [] -nf(lam(E))|nf(E).
% 1.95/2.16 0 [] nf(lam(E))| -nf(E).
% 1.95/2.16 0 [] nf(var(X4)).
% 1.95/2.16 0 [] index(nil,Y)=nothing.
% 1.95/2.16 0 [] index(cons(Z,Xs),zero)=just(Z).
% 1.95/2.16 0 [] index(cons(Z,Xs),suc(N))=index(Xs,N).
% 1.95/2.16 0 [] -tc(X,app(F,X2,Tx),Z)|tc(X,F,arr(Tx,Z)).
% 1.95/2.16 0 [] -tc(X,app(F,X2,Tx),Z)|tc(X,X2,Tx).
% 1.95/2.16 0 [] tc(X,app(F,X2,Tx),Z)| -tc(X,F,arr(Tx,Z))| -tc(X,X2,Tx).
% 1.95/2.16 0 [] Z=arr(proj1Arr(Z),proj2Arr(Z))| -tc(X,lam(E),Z).
% 1.95/2.16 0 [] -tc(X,lam(E),arr(Tx2,T1))|tc(cons(Tx2,X),E,T1).
% 1.95/2.16 0 [] tc(X,lam(E),arr(Tx2,T1))| -tc(cons(Tx2,X),E,T1).
% 1.95/2.16 0 [] index(X,X3)!=nothing| -tc(X,var(X3),Z).
% 1.95/2.16 0 [] index(X,X3)!=just(Tx3)| -tc(X,var(X3),Z)|Tx3=Z.
% 1.95/2.16 0 [] index(X,X3)!=just(Tx3)|tc(X,var(X3),Z)|Tx3!=Z.
% 1.95/2.16 0 [] -nf(E)| -tc(nil,E,arr(a,arr(b,b))).
% 1.95/2.16 end_of_list.
% 1.95/2.16
% 1.95/2.16 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4.
% 1.95/2.16
% 1.95/2.16 This ia a non-Horn set with equality. The strategy will be
% 1.95/2.16 Knuth-Bendix, ordered hyper_res, factoring, and unit
% 1.95/2.16 deletion, with positive clauses in sos and nonpositive
% 1.95/2.16 clauses in usable.
% 1.95/2.16
% 1.95/2.16 dependent: set(knuth_bendix).
% 1.95/2.16 dependent: set(anl_eq).
% 1.95/2.16 dependent: set(para_from).
% 1.95/2.16 dependent: set(para_into).
% 1.95/2.16 dependent: clear(para_from_right).
% 1.95/2.16 dependent: clear(para_into_right).
% 1.95/2.16 dependent: set(para_from_vars).
% 1.95/2.16 dependent: set(eq_units_both_ways).
% 1.95/2.16 dependent: set(dynamic_demod_all).
% 1.95/2.16 dependent: set(dynamic_demod).
% 1.95/2.16 dependent: set(order_eq).
% 1.95/2.16 dependent: set(back_demod).
% 1.95/2.16 dependent: set(lrpo).
% 1.95/2.16 dependent: set(hyper_res).
% 1.95/2.16 dependent: set(unit_deletion).
% 1.95/2.16 dependent: set(factor).
% 1.95/2.16
% 1.95/2.16 ------------> process usable:
% 1.95/2.16 ** KEPT (pick-wt=5): 2 [copy,1,flip.1] cons(A,B)!=nil.
% 1.95/2.16 ** KEPT (pick-wt=5): 3 [] arr(A,B)!=a.
% 1.95/2.16 ** KEPT (pick-wt=5): 4 [] arr(A,B)!=b.
% 1.95/2.16 ** KEPT (pick-wt=5): 5 [] arr(A,B)!=c.
% 1.95/2.16 ** KEPT (pick-wt=3): 7 [copy,6,flip.1] b!=a.
% 1.95/2.16 ** KEPT (pick-wt=3): 9 [copy,8,flip.1] c!=a.
% 1.95/2.16 ** KEPT (pick-wt=3): 11 [copy,10,flip.1] c!=b.
% 1.95/2.16 ** KEPT (pick-wt=4): 13 [copy,12,flip.1] suc(A)!=zero.
% 1.95/2.16 ** KEPT (pick-wt=4): 15 [copy,14,flip.1] just(A)!=nothing.
% 1.95/2.16 ** KEPT (pick-wt=7): 16 [] app(A,B,C)!=lam(D).
% 1.95/2.16 ** KEPT (pick-wt=7): 17 [] app(A,B,C)!=var(D).
% 1.95/2.16 ** KEPT (pick-wt=5): 18 [] lam(A)!=var(B).
% 1.95/2.16 ** KEPT (pick-wt=12): 20 [copy,19,flip.1] lam(proj1Lam(A))=A| -nf(app(A,B,C))|nf(A).
% 1.95/2.16 ** KEPT (pick-wt=12): 22 [copy,21,flip.1] lam(proj1Lam(A))=A| -nf(app(A,B,C))|nf(B).
% 1.95/2.16 ** KEPT (pick-wt=14): 24 [copy,23,flip.1] lam(proj1Lam(A))=A|nf(app(A,B,C))| -nf(A)| -nf(B).
% 1.95/2.16 ** KEPT (pick-wt=6): 25 [] -nf(app(lam(A),B,C)).
% 1.95/2.16 ** KEPT (pick-wt=5): 26 [] -nf(lam(A))|nf(A).
% 1.95/2.16 ** KEPT (pick-wt=5): 27 [] nf(lam(A))| -nf(A).
% 1.95/2.16 ** KEPT (pick-wt=13): 28 [] -tc(A,app(B,C,D),E)|tc(A,B,arr(D,E)).
% 1.95/2.16 ** KEPT (pick-wt=11): 29 [] -tc(A,app(B,C,D),E)|tc(A,C,D).
% 1.95/2.16 ** KEPT (pick-wt=17): 30 [] tc(A,app(B,C,D),E)| -tc(A,B,arr(D,E))| -tc(A,C,D).
% 1.95/2.16 ** KEPT (pick-wt=12): 32 [copy,31,flip.1] arr(proj1Arr(A),proj2Arr(A))=A| -tc(B,lam(C),A).
% 1.95/2.16 ** KEPT (pick-wt=13): 33 [] -tc(A,lam(B),arr(C,D))|tc(cons(C,A),B,D).
% 1.95/2.16 ** KEPT (pick-wt=13): 34 [] tc(A,lam(B),arr(C,D))| -tc(cons(C,A),B,D).
% 1.95/2.16 ** KEPT (pick-wt=10): 35 [] index(A,B)!=nothing| -tc(A,var(B),C).
% 1.95/2.16 ** KEPT (pick-wt=14): 36 [] index(A,B)!=just(C)| -tc(A,var(B),D)|C=D.
% 1.95/2.16 ** KEPT (pick-wt=14): 37 [] index(A,B)!=just(C)|tc(A,var(B),D)|C!=D.
% 1.95/2.16 ** KEPT (pick-wt=10): 38 [] -nf(A)| -tc(nil,A,arr(a,arr(b,b))).
% 1.95/2.16 ** KEPT (pick-wt=7): 39 [copy,16,flip.1] lam(A)!=app(B,C,D).
% 1.95/2.16 ** KEPT (pick-wt=7): 40 [copy,17,flip.1] var(A)!=app(B,C,D).
% 1.95/2.16 ** KEPT (pick-wt=5): 41 [copy,18,flip.1] var(A)!=lam(B).
% 1.95/2.16 Following clause subsumed by 16 during input processing: 0 [copy,39,flip.1] app(A,B,C)!=lam(D).
% 1.95/2.16 Following clause subsumed by 17 during input processing: 0 [copy,40,flip.1] app(A,B,C)!=var(D).
% 1.95/2.16 Following clause subsumed by 18 during input processing: 0 [copy,41,flip.1] lam(A)!=var(B).
% 1.95/2.16
% 1.95/2.16 ------------> process sos:
% 1.95/2.16 ** KEPT (pick-wt=3): 44 [] A=A.
% 1.95/2.16 ** KEPT (pick-wt=6): 45 [] head(cons(A,B))=A.
% 1.95/2.16 ---> New Demodulator: 46 [new_demod,45] head(cons(A,B))=A.
% 1.95/2.16 ** KEPT (pick-wt=6): 47 [] tail(cons(A,B))=B.
% 1.95/2.16 ---> New Demodulator: 48 [new_demod,47] tail(cons(A,B))=B.
% 1.95/2.16 ** KEPT (pick-wt=6): 49 [] proj1Arr(arr(A,B))=A.
% 1.95/2.16 ---> New Demodulator: 50 [new_demod,49] proj1Arr(arr(A,B))=A.
% 1.95/2.16 ** KEPT (pick-wt=6): 51 [] proj2Arr(arr(A,B))=B.
% 1.95/2.16 ---> New Demodulator: 52 [new_demod,51] proj2Arr(arr(A,B))=B.
% 1.95/2.16 ** KEPT (pick-wt=5): 53 [] proj1Suc(suc(A))=A.
% 1.95/2.16 ---> New Demodulator: 54 [new_demod,53] proj1Suc(suc(A))=A.
% 1.95/2.16 ** KEPT (pick-wt=5): 55 [] proj1Just(just(A))=A.
% 1.95/2.16 ---> New Demodulator: 56 [new_demod,55] proj1Just(just(A))=A.
% 1.95/2.16 ** KEPT (pick-wt=7): 57 [] proj1App(app(A,B,C))=A.
% 1.95/2.16 ---> New Demodulator: 58 [new_demod,57] proj1App(app(A,B,C))=A.
% 1.95/2.16 ** KEPT (pick-wt=7): 59 [] proj2App(app(A,B,C))=B.
% 1.95/2.16 ---> New Demodulator: 60 [new_demod,59] proj2App(app(A,B,C))=B.
% 1.95/2.16 ** KEPT (pick-wt=7): 61 [] proj3App(app(A,B,C))=C.
% 1.95/2.16 ---> New Demodulator: 62 [new_demod,61] proj3App(app(A,B,C))=C.
% 1.95/2.16 ** KEPT (pick-wt=5): 63 [] proj1Lam(lam(A))=A.
% 1.95/2.16 ---> New Demodulator: 64 [new_demod,63] proj1Lam(lam(A))=A.
% 1.95/2.16 ** KEPT (pick-wt=5): 65 [] proj1Var(var(A))=A.
% 1.95/2.16 ---> New Demodulator: 66 [new_demod,65] proj1Var(var(A))=A.
% 1.95/2.16 ** KEPT (pick-wt=3): 67 [] nf(var(A)).
% 1.95/2.16 ** KEPT (pick-wt=5): 68 [] index(nil,A)=nothing.
% 1.95/2.16 ---> New Demodulator: 69 [new_demod,68] index(nil,A)=nothing.
% 1.95/2.16 ** KEPT (pick-wt=8): 70 [] index(cons(A,B),zero)=just(A).
% 1.95/2.16 ** KEPT (pick-wt=10): 71 [] index(cons(A,B),suc(C))=index(B,C).
% 1.95/2.16 ---> New Demodulator: 72 [new_demod,71] index(cons(A,B),suc(C))=index(B,C).
% 1.95/2.16 Following clause subsumed by 44 during input processing: 0 [copy,44,flip.1] A=A.
% 1.95/2.16 >>>> Starting back demodulation with 46.
% 1.95/2.16 >>>> Starting back demodulation with 48.
% 1.95/2.16 >>>> Starting back demodulation with 50.
% 1.95/2.19 >>>> Starting back demodulation with 52.
% 1.95/2.19 >>>> Starting back demodulation with 54.
% 1.95/2.19 >>>> Starting back demodulation with 56.
% 1.95/2.19 >>>> Starting back demodulation with 58.
% 1.95/2.19 >>>> Starting back demodulation with 60.
% 1.95/2.19 >>>> Starting back demodulation with 62.
% 1.95/2.19 >>>> Starting back demodulation with 64.
% 1.95/2.19 >>>> Starting back demodulation with 66.
% 1.95/2.19 >>>> Starting back demodulation with 69.
% 1.95/2.19 ** KEPT (pick-wt=8): 73 [copy,70,flip.1] just(A)=index(cons(A,B),zero).
% 1.95/2.19 >>>> Starting back demodulation with 72.
% 1.95/2.19 Following clause subsumed by 70 during input processing: 0 [copy,73,flip.1] index(cons(A,B),zero)=just(A).
% 1.95/2.19
% 1.95/2.19 ======= end of input processing =======
% 1.95/2.19
% 1.95/2.19 =========== start of search ===========
% 1.95/2.19
% 1.95/2.19 -------- PROOF --------
% 1.95/2.19
% 1.95/2.19 -----> EMPTY CLAUSE at 0.03 sec ----> 486 [hyper,194,38,78] $F.
% 1.95/2.19
% 1.95/2.19 Length of proof is 5. Level of proof is 3.
% 1.95/2.19
% 1.95/2.19 ---------------- PROOF ----------------
% 1.95/2.19 % SZS status Theorem
% 1.95/2.19 % SZS output start Refutation
% See solution above
% 1.95/2.19 ------------ end of proof -------------
% 1.95/2.19
% 1.95/2.19
% 1.95/2.19 Search stopped by max_proofs option.
% 1.95/2.19
% 1.95/2.19
% 1.95/2.19 Search stopped by max_proofs option.
% 1.95/2.19
% 1.95/2.19 ============ end of search ============
% 1.95/2.19
% 1.95/2.19 -------------- statistics -------------
% 1.95/2.19 clauses given 49
% 1.95/2.19 clauses generated 860
% 1.95/2.19 clauses kept 461
% 1.95/2.19 clauses forward subsumed 450
% 1.95/2.19 clauses back subsumed 10
% 1.95/2.19 Kbytes malloced 3906
% 1.95/2.19
% 1.95/2.19 ----------- times (seconds) -----------
% 1.95/2.19 user CPU time 0.03 (0 hr, 0 min, 0 sec)
% 1.95/2.19 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.95/2.19 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 1.95/2.19
% 1.95/2.19 That finishes the proof of the theorem.
% 1.95/2.19
% 1.95/2.19 Process 31683 finished Tue May 5 12:33:55 2026
% 1.95/2.19 Otter interrupted
% 1.95/2.19 PROOF FOUND
%------------------------------------------------------------------------------