%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX223+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:16:23 AM UTC 2026
% Result : Theorem 180.03s 24.25s
% Output : CNFRefutation 180.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 47 ( 25 unt; 0 def)
% Number of atoms : 79 ( 23 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 57 ( 25 ~; 21 |; 4 &)
% ( 5 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-3 aty)
% Number of variables : 136 ( 50 sgn 30 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_020,axiom,
! [X] : proj1Var(var(X)) = X,
file('theBenchmark.p',axiom_020) ).
fof(axiom_021,axiom,
! [X,X2,X3,X4] : app(X,X2,X3) != lam(X4),
file('theBenchmark.p',axiom_021) ).
fof(axiom_023,axiom,
! [X,X2] : lam(X) != var(X2),
file('theBenchmark.p',axiom_023) ).
fof(axiom_024,axiom,
! [Y,Z,X2] :
( Y != lam(proj1Lam(Y))
=> ( nf(app(Y,Z,X2))
<=> ( nf(Z)
& nf(Y) ) ) ),
file('theBenchmark.p',axiom_024) ).
fof(axiom_026,axiom,
! [E] :
( nf(lam(E))
<=> nf(E) ),
file('theBenchmark.p',axiom_026) ).
fof(axiom_027,axiom,
! [X4] : nf(var(X4)),
file('theBenchmark.p',axiom_027) ).
fof(axiom_029,axiom,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
file('theBenchmark.p',axiom_029) ).
fof(axiom_030,axiom,
! [Z,Xs,N] : index(cons(Z,Xs),suc(N)) = index(Xs,N),
file('theBenchmark.p',axiom_030) ).
fof(axiom_031,axiom,
! [X,Z,F,X2,Tx] :
( tc(X,app(F,X2,Tx),Z)
<=> ( tc(X,X2,Tx)
& tc(X,F,arr(Tx,Z)) ) ),
file('theBenchmark.p',axiom_031) ).
fof(axiom_033,axiom,
! [X,E,Tx2,T1] :
( tc(X,lam(E),arr(Tx2,T1))
<=> tc(cons(Tx2,X),E,T1) ),
file('theBenchmark.p',axiom_033) ).
fof(axiom_035,axiom,
! [X,Z,X3,Tx3] :
( index(X,X3) = just(Tx3)
=> ( tc(X,var(X3),Z)
<=> Tx3 = Z ) ),
file('theBenchmark.p',axiom_035) ).
fof(goal_036,conjecture,
? [E] :
( tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b)))
& nf(E) ),
file('theBenchmark.p',goal_036) ).
fof(goal_036_neg,negated_conjecture,
~ ? [E] :
( tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b)))
& nf(E) ),
inference(assume_negation,[status(cth)],[goal_036]) ).
cnf(c_56,plain,
proj1Var(var(A)) = A,
inference(clausify,[status(thm)],[axiom_020]) ).
cnf(c_57,plain,
lam(A) != app(B,C,D),
inference(clausify,[status(thm)],[axiom_021]) ).
cnf(c_59,plain,
var(A) != lam(B),
inference(clausify,[status(thm)],[axiom_023]) ).
cnf(c_62,plain,
( ~ nf(B)
| ~ nf(A)
| nf(app(A,B,C))
| lam(proj1Lam(A)) = A ),
inference(clausify,[status(thm)],[axiom_024]) ).
cnf(c_65,plain,
( ~ nf(A)
| nf(lam(A)) ),
inference(clausify,[status(thm)],[axiom_026]) ).
cnf(c_66,plain,
nf(var(A)),
inference(clausify,[status(thm)],[axiom_027]) ).
cnf(c_68,plain,
index(cons(A,B),zero) = just(A),
inference(clausify,[status(thm)],[axiom_029]) ).
cnf(c_69,plain,
index(cons(A,B),suc(C)) = index(B,C),
inference(clausify,[status(thm)],[axiom_030]) ).
cnf(c_72,plain,
( ~ tc(A,C,D)
| ~ tc(A,B,arr(D,E))
| tc(A,app(B,C,D),E) ),
inference(clausify,[status(thm)],[axiom_031]) ).
cnf(c_75,plain,
( ~ tc(cons(C,A),B,D)
| tc(A,lam(B),arr(C,D)) ),
inference(clausify,[status(thm)],[axiom_033]) ).
cnf(c_78,plain,
( C != D
| tc(A,var(B),D)
| index(A,B) != just(C) ),
inference(clausify,[status(thm)],[axiom_035]) ).
cnf(c_79,negated_conjecture,
( ~ tc(nil,A,arr(arr(a,arr(a,b)),arr(a,b)))
| ~ nf(A) ),
inference(clausify,[status(thm)],[goal_036_neg]) ).
cnf(c_87,plain,
( ~ nf(A)
| nf(app(A,var(B),C))
| lam(proj1Lam(A)) = A ),
inference(resolve,[status(thm)],[c_66,c_62]) ).
cnf(c_15894,plain,
( ~ nf(B)
| nf(app(var(A),B,C))
| lam(proj1Lam(var(A))) = var(A) ),
inference(resolve,[status(thm)],[c_66,c_62]) ).
cnf(c_88,plain,
( ~ nf(B)
| nf(app(var(A),B,C)) ),
inference(resolve,[status(thm)],[c_59,c_15894]) ).
cnf(c_117,plain,
( A != C
| tc(cons(A,B),var(zero),C) ),
inference(resolve,[status(thm)],[c_78,c_68]) ).
cnf(c_15895,plain,
( tc(A,var(B),C)
| index(A,B) != just(proj1Var(var(C))) ),
inference(resolve,[status(thm)],[c_78,c_56]) ).
cnf(c_121,plain,
( tc(A,var(B),C)
| index(A,B) != just(C) ),
inference(paramod,[status(thm)],[c_56,c_15895]) ).
cnf(c_15896,plain,
tc(cons(proj1Var(var(A)),B),var(zero),A),
inference(resolve,[status(thm)],[c_117,c_56]) ).
cnf(c_149,plain,
tc(cons(A,B),var(zero),A),
inference(paramod,[status(thm)],[c_56,c_15896]) ).
cnf(c_152,plain,
( ~ tc(cons(A,B),C,arr(A,D))
| tc(cons(A,B),app(C,var(zero),A),D) ),
inference(resolve,[status(thm)],[c_149,c_72]) ).
cnf(c_187,plain,
( tc(cons(D,A),var(suc(B)),C)
| index(A,B) != just(C) ),
inference(paramod,[status(thm)],[c_69,c_121]) ).
cnf(c_194,plain,
nf(app(var(A),var(B),C)),
inference(resolve,[status(thm)],[c_88,c_66]) ).
cnf(c_15897,plain,
( nf(app(app(var(A),var(B),C),var(D),E))
| lam(proj1Lam(app(var(A),var(B),C))) = app(var(A),var(B),C) ),
inference(resolve,[status(thm)],[c_194,c_87]) ).
cnf(c_208,plain,
nf(app(app(var(A),var(B),C),var(D),E)),
inference(resolve,[status(thm)],[c_57,c_15897]) ).
cnf(c_250,plain,
tc(cons(A,cons(B,C)),var(suc(zero)),B),
inference(resolve,[status(thm)],[c_187,c_68]) ).
cnf(c_303,plain,
nf(lam(app(app(var(A),var(B),C),var(D),E))),
inference(resolve,[status(thm)],[c_208,c_65]) ).
cnf(c_372,plain,
tc(cons(A,cons(arr(A,B),C)),app(var(suc(zero)),var(zero),A),B),
inference(resolve,[status(thm)],[c_152,c_250]) ).
cnf(c_511,plain,
tc(cons(A,cons(arr(A,arr(A,B)),C)),app(app(var(suc(zero)),var(zero),A),var(zero),A),B),
inference(resolve,[status(thm)],[c_372,c_152]) ).
cnf(c_613,plain,
nf(lam(lam(app(app(var(A),var(B),C),var(D),E)))),
inference(resolve,[status(thm)],[c_303,c_65]) ).
cnf(c_1847,negated_conjecture,
~ tc(nil,lam(lam(app(app(var(A),var(B),C),var(D),E))),arr(arr(a,arr(a,b)),arr(a,b))),
inference(resolve,[status(thm)],[c_79,c_613]) ).
cnf(c_4114,plain,
tc(cons(arr(A,arr(A,B)),C),lam(app(app(var(suc(zero)),var(zero),A),var(zero),A)),arr(A,B)),
inference(resolve,[status(thm)],[c_511,c_75]) ).
cnf(c_15892,plain,
tc(A,lam(lam(app(app(var(suc(zero)),var(zero),B),var(zero),B))),arr(arr(B,arr(B,C)),arr(B,C))),
inference(resolve,[status(thm)],[c_4114,c_75]) ).
cnf(c_15893,plain,
$false,
inference(resolve,[status(thm)],[c_15892,c_1847]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX223+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 17:01:21 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 936053 was started by sandbox on n018,
% 0.09/0.35 % Sat Sep 26 17:01:21 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.36
% 0.09/0.36 % From the command line: assign(max_seconds, 300).
% 180.03/24.25
% 180.03/24.25 % given #500 (F,wt=32): 782 -tc(A,lam(var(zero)),arr(just(c),just(arr(B,C)))). [ur(74,b,268,a)].
% 180.03/24.25
% 180.03/24.25 % given #1000 (T,wt=50): 805 nf(app(app(app(var(A),lam(var(B)),C),lam(lam(var(D))),E),lam(lam(var(F))),V6)). [resolve(238,c,663,a),unit_del(a,57)].
% 180.03/24.25
% 180.03/24.25 % given #1500 (F,wt=39): 2194 -tc(A,app(B,lam(app(C,var(zero),c)),arr(a,D)),E). [ur(71,b,531,a)].
% 180.03/24.25
% 180.03/24.25 % given #2000 (T,wt=53): 2630 index(A,B) != just(C) | tc(cons(D,cons(E,cons(F,cons(V6,A)))),var(suc(suc(suc(suc(B))))),C). [para(69(a,1),599(a,1))].
% 180.03/24.25
% 180.03/24.25 % SZS status Theorem for theBenchmark
% 180.03/24.25
% 180.03/24.25 % Proof 1 at 5.34 (+ 2.34) seconds.
% 180.03/24.25 % Length of proof is 42.
% 180.03/24.25 % Level of proof is 9.
% 180.03/24.25 % Maximum clause weight is 59.000.
% 180.03/24.25 % Given clauses 2044.
% 180.03/24.25
% 180.03/24.25 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------