%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX222+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 0.09s 0.60s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of formulae : 24 ( 14 unt; 0 def)
% Number of atoms : 36 ( 9 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 21 ( 9 ~; 6 |; 2 &)
% ( 3 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 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 : 44 ( 11 sgn 13 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_020,axiom,
! [X] : proj1Var(var(X)) = X,
file('theBenchmark.p',axiom_020) ).
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_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(a,arr(b,b)))
& nf(E) ),
file('theBenchmark.p',goal_036) ).
fof(goal_036_neg,negated_conjecture,
~ ? [E] :
( tc(nil,E,arr(a,arr(b,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_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_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(a,arr(b,b)))
| ~ nf(A) ),
inference(clausify,[status(thm)],[goal_036_neg]) ).
cnf(c_86,plain,
nf(lam(var(A))),
inference(resolve,[status(thm)],[c_66,c_65]) ).
cnf(c_121,plain,
( A != C
| tc(cons(A,B),var(zero),C) ),
inference(resolve,[status(thm)],[c_78,c_68]) ).
cnf(c_148,plain,
nf(lam(lam(var(A)))),
inference(resolve,[status(thm)],[c_86,c_65]) ).
cnf(c_223,plain,
tc(cons(proj1Var(var(A)),B),var(zero),A),
inference(resolve,[status(thm)],[c_121,c_56]) ).
cnf(c_185,plain,
tc(cons(A,B),var(zero),A),
inference(paramod,[status(thm)],[c_56,c_223]) ).
cnf(c_187,plain,
tc(A,lam(var(zero)),arr(B,B)),
inference(resolve,[status(thm)],[c_185,c_75]) ).
cnf(c_215,plain,
tc(A,lam(lam(var(zero))),arr(B,arr(C,C))),
inference(resolve,[status(thm)],[c_187,c_75]) ).
cnf(c_221,plain,
~ tc(nil,lam(lam(var(A))),arr(a,arr(b,b))),
inference(resolve,[status(thm)],[c_148,c_79]) ).
cnf(c_222,plain,
$false,
inference(resolve,[status(thm)],[c_221,c_215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX222+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.57 % Computer : n018.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Sat Sep 26 17:01:08 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.57 % Process 935439 was started by sandbox on n018,
% 0.09/0.57 % Sat Sep 26 17:01:08 2026
% 0.09/0.57 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.58
% 0.09/0.58 % From the command line: assign(max_seconds, 300).
% 0.09/0.60
% 0.09/0.60 % SZS status Theorem for theBenchmark
% 0.09/0.60
% 0.09/0.60 % Proof 1 at 0.01 (+ 0.01) seconds.
% 0.09/0.60 % Length of proof is 22.
% 0.09/0.60 % Level of proof is 6.
% 0.09/0.60 % Maximum clause weight is 23.000.
% 0.09/0.60 % Given clauses 76.
% 0.09/0.60
% 0.09/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------