%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX224+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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.22s 0.59s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 7
% Syntax : Number of formulae : 33 ( 21 unt; 0 def)
% Number of atoms : 50 ( 14 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 33 ( 16 ~; 12 |; 1 &)
% ( 3 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 94 ( 21 sgn 19 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_020,axiom,
! [X] : proj1Var(var(X)) = X,
file('theBenchmark.p',axiom_020) ).
fof(axiom_025,axiom,
! [Z,Xs] : index(cons(Z,Xs),zero) = just(Z),
file('theBenchmark.p',axiom_025) ).
fof(axiom_026,axiom,
! [Z,Xs,N] : index(cons(Z,Xs),suc(N)) = index(Xs,N),
file('theBenchmark.p',axiom_026) ).
fof(axiom_027,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_027) ).
fof(axiom_029,axiom,
! [X,E,Tx2,T1] :
( tc(X,lam(E),arr(Tx2,T1))
<=> tc(cons(Tx2,X),E,T1) ),
file('theBenchmark.p',axiom_029) ).
fof(axiom_031,axiom,
! [X,Z,X3,Tx3] :
( index(X,X3) = just(Tx3)
=> ( tc(X,var(X3),Z)
<=> Tx3 = Z ) ),
file('theBenchmark.p',axiom_031) ).
fof(goal_032,conjecture,
? [E] : tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))),
file('theBenchmark.p',goal_032) ).
fof(goal_032_neg,negated_conjecture,
~ ? [E] : tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))),
inference(assume_negation,[status(cth)],[goal_032]) ).
cnf(c_52,plain,
proj1Var(var(A)) = A,
inference(clausify,[status(thm)],[axiom_020]) ).
cnf(c_57,plain,
index(cons(A,B),zero) = just(A),
inference(clausify,[status(thm)],[axiom_025]) ).
cnf(c_58,plain,
index(cons(A,B),suc(C)) = index(B,C),
inference(clausify,[status(thm)],[axiom_026]) ).
cnf(c_61,plain,
( ~ tc(A,C,D)
| ~ tc(A,B,arr(D,E))
| tc(A,app(B,C,D),E) ),
inference(clausify,[status(thm)],[axiom_027]) ).
cnf(c_64,plain,
( ~ tc(cons(C,A),B,D)
| tc(A,lam(B),arr(C,D)) ),
inference(clausify,[status(thm)],[axiom_029]) ).
cnf(c_67,plain,
( C != D
| tc(A,var(B),D)
| index(A,B) != just(C) ),
inference(clausify,[status(thm)],[axiom_031]) ).
cnf(c_68,negated_conjecture,
~ tc(nil,A,arr(arr(a,arr(a,b)),arr(a,b))),
inference(clausify,[status(thm)],[goal_032_neg]) ).
cnf(c_457,plain,
( A != C
| tc(cons(A,B),var(zero),C) ),
inference(resolve,[status(thm)],[c_67,c_57]) ).
cnf(c_458,plain,
tc(cons(proj1Var(var(A)),B),var(zero),A),
inference(resolve,[status(thm)],[c_457,c_52]) ).
cnf(c_103,plain,
tc(cons(A,B),var(zero),A),
inference(paramod,[status(thm)],[c_52,c_458]) ).
cnf(c_105,plain,
( C != E
| tc(cons(D,A),var(suc(B)),E)
| index(A,B) != just(C) ),
inference(paramod,[status(thm)],[c_58,c_67]) ).
cnf(c_106,negated_conjecture,
~ tc(cons(arr(a,arr(a,b)),nil),A,arr(a,b)),
inference(resolve,[status(thm)],[c_64,c_68]) ).
cnf(c_125,plain,
tc(A,lam(var(zero)),arr(B,B)),
inference(resolve,[status(thm)],[c_64,c_103]) ).
cnf(c_459,plain,
( B != D
| tc(cons(A,cons(B,C)),var(suc(zero)),D) ),
inference(resolve,[status(thm)],[c_105,c_57]) ).
cnf(c_460,plain,
tc(cons(A,cons(proj1Var(var(B)),C)),var(suc(zero)),B),
inference(resolve,[status(thm)],[c_459,c_52]) ).
cnf(c_197,plain,
tc(cons(A,cons(B,C)),var(suc(zero)),B),
inference(paramod,[status(thm)],[c_52,c_460]) ).
cnf(c_200,plain,
tc(cons(A,B),lam(var(suc(zero))),arr(C,A)),
inference(resolve,[status(thm)],[c_64,c_197]) ).
cnf(c_461,plain,
( ~ tc(cons(A,cons(arr(B,C),D)),E,B)
| tc(cons(A,cons(arr(B,C),D)),app(var(suc(zero)),E,B),C) ),
inference(resolve,[status(thm)],[c_61,c_197]) ).
cnf(c_204,plain,
tc(cons(A,cons(arr(A,B),C)),app(var(suc(zero)),var(zero),A),B),
inference(resolve,[status(thm)],[c_461,c_103]) ).
cnf(c_462,plain,
( ~ tc(cons(A,B),C,D)
| tc(cons(A,B),app(lam(var(suc(zero))),C,D),A) ),
inference(resolve,[status(thm)],[c_61,c_200]) ).
cnf(c_210,plain,
tc(cons(A,B),app(lam(var(suc(zero))),lam(var(zero)),arr(C,C)),A),
inference(resolve,[status(thm)],[c_462,c_125]) ).
cnf(c_463,plain,
( ~ tc(cons(A,cons(arr(A,arr(B,C)),D)),E,B)
| tc(cons(A,cons(arr(A,arr(B,C)),D)),app(app(var(suc(zero)),var(zero),A),E,B),C) ),
inference(resolve,[status(thm)],[c_61,c_204]) ).
cnf(c_406,plain,
tc(cons(A,cons(arr(A,arr(A,B)),C)),app(app(var(suc(zero)),var(zero),A),app(lam(var(suc(zero))),lam(var(zero)),arr(D,D)),A),B),
inference(resolve,[status(thm)],[c_463,c_210]) ).
cnf(c_455,plain,
~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),A,b),
inference(resolve,[status(thm)],[c_64,c_106]) ).
cnf(c_456,plain,
$false,
inference(resolve,[status(thm)],[c_455,c_406]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX224+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n009.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sat Sep 26 16:59:14 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.44 % Process 665766 was started by sandbox2 on n009,
% 0.18/0.44 % Sat Sep 26 16:59:14 2026
% 0.18/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.45
% 0.18/0.45 % From the command line: assign(max_seconds, 300).
% 0.22/0.59
% 0.22/0.59 % SZS status Theorem for theBenchmark
% 0.22/0.59
% 0.22/0.59 % Proof 1 at 0.09 (+ 0.05) seconds.
% 0.22/0.59 % Length of proof is 25.
% 0.22/0.59 % Level of proof is 7.
% 0.22/0.59 % Maximum clause weight is 71.000.
% 0.22/0.59 % Given clauses 103.
% 0.22/0.59
% 0.22/0.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------