%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX219+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 : n005.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:22 AM UTC 2026
% Result : Theorem 156.90s 21.31s
% Output : CNFRefutation 156.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 7
% Syntax : Number of formulae : 34 ( 21 unt; 0 def)
% Number of atoms : 53 ( 17 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 37 ( 18 ~; 14 |; 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 : 14 ( 14 usr; 5 con; 0-3 aty)
% Number of variables : 106 ( 29 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(b,c),arr(arr(a,b),arr(a,c)))),
file('theBenchmark.p',goal_032) ).
fof(goal_032_neg,negated_conjecture,
~ ? [E] : tc(nil,E,arr(arr(b,c),arr(arr(a,b),arr(a,c)))),
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(b,c),arr(arr(a,b),arr(a,c)))),
inference(clausify,[status(thm)],[goal_032_neg]) ).
cnf(c_13160,plain,
( A != C
| tc(cons(A,B),var(zero),C) ),
inference(resolve,[status(thm)],[c_67,c_57]) ).
cnf(c_13161,plain,
tc(cons(proj1Var(var(A)),B),var(zero),A),
inference(resolve,[status(thm)],[c_13160,c_52]) ).
cnf(c_103,plain,
tc(cons(A,B),var(zero),A),
inference(paramod,[status(thm)],[c_52,c_13161]) ).
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(b,c),nil),A,arr(arr(a,b),arr(a,c))),
inference(resolve,[status(thm)],[c_64,c_68]) ).
cnf(c_13162,plain,
( B != D
| tc(cons(A,cons(B,C)),var(suc(zero)),D) ),
inference(resolve,[status(thm)],[c_105,c_57]) ).
cnf(c_13163,plain,
tc(cons(A,cons(proj1Var(var(B)),C)),var(suc(zero)),B),
inference(resolve,[status(thm)],[c_13162,c_52]) ).
cnf(c_196,plain,
tc(cons(A,cons(B,C)),var(suc(zero)),B),
inference(paramod,[status(thm)],[c_52,c_13163]) ).
cnf(c_198,plain,
( C != F
| tc(cons(D,cons(E,A)),var(suc(suc(B))),F)
| index(A,B) != just(C) ),
inference(paramod,[status(thm)],[c_58,c_105]) ).
cnf(c_13164,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_196]) ).
cnf(c_205,plain,
tc(cons(A,cons(arr(A,B),C)),app(var(suc(zero)),var(zero),A),B),
inference(resolve,[status(thm)],[c_13164,c_103]) ).
cnf(c_13165,plain,
( C != E
| tc(cons(A,cons(B,cons(C,D))),var(suc(suc(zero))),E) ),
inference(resolve,[status(thm)],[c_198,c_57]) ).
cnf(c_13166,plain,
tc(cons(A,cons(B,cons(proj1Var(var(C)),D))),var(suc(suc(zero))),C),
inference(resolve,[status(thm)],[c_13165,c_52]) ).
cnf(c_578,plain,
tc(cons(A,cons(B,cons(C,D))),var(suc(suc(zero))),C),
inference(paramod,[status(thm)],[c_52,c_13166]) ).
cnf(c_13167,plain,
( ~ tc(cons(A,cons(B,cons(arr(C,D),E))),F,C)
| tc(cons(A,cons(B,cons(arr(C,D),E))),app(var(suc(suc(zero))),F,C),D) ),
inference(resolve,[status(thm)],[c_61,c_578]) ).
cnf(c_619,plain,
tc(cons(A,cons(arr(A,B),cons(arr(B,C),D))),app(var(suc(suc(zero))),app(var(suc(zero)),var(zero),A),B),C),
inference(resolve,[status(thm)],[c_13167,c_205]) ).
cnf(c_1187,plain,
~ tc(cons(arr(a,b),cons(arr(b,c),nil)),A,arr(a,c)),
inference(resolve,[status(thm)],[c_64,c_106]) ).
cnf(c_13158,plain,
tc(cons(arr(A,B),cons(arr(B,C),D)),lam(app(var(suc(suc(zero))),app(var(suc(zero)),var(zero),A),B)),arr(A,C)),
inference(resolve,[status(thm)],[c_64,c_619]) ).
cnf(c_13159,plain,
$false,
inference(resolve,[status(thm)],[c_13158,c_1187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX219+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.08 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n005.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sat Sep 26 16:57:47 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.20/0.46 % Process 2599425 was started by sandbox2 on n005,
% 0.20/0.46 % Sat Sep 26 16:57:47 2026
% 0.20/0.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.20/0.47
% 0.20/0.47 % From the command line: assign(max_seconds, 300).
% 156.90/21.31
% 156.90/21.31 % SZS status Theorem for theBenchmark
% 156.90/21.31
% 156.90/21.31 % Proof 1 at 4.11 (+ 0.57) seconds.
% 156.90/21.31 % Length of proof is 25.
% 156.90/21.31 % Level of proof is 7.
% 156.90/21.31 % Maximum clause weight is 57.000.
% 156.90/21.31 % Given clauses 460.
% 156.90/21.31
% 156.90/21.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------