%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX204+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 : n003.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:19 AM UTC 2026
% Result : Theorem 0.16s 0.51s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 36 ( 36 unt; 0 def)
% Number of atoms : 36 ( 35 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 1 con; 0-2 aty)
% Number of variables : 37 ( 2 sgn 8 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X] : proj1S(s(X)) = X,
file('theBenchmark.p',axiom_001) ).
fof(axiom_002,axiom,
! [X] : z != s(X),
file('theBenchmark.p',axiom_002) ).
fof(axiom_003,axiom,
! [Y] : x2(z,Y) = Y,
file('theBenchmark.p',axiom_003) ).
fof(axiom_004,axiom,
! [Y,N] : x2(s(N),Y) = s(x2(N,Y)),
file('theBenchmark.p',axiom_004) ).
fof(axiom_005,axiom,
! [Y] : x22(z,Y) = z,
file('theBenchmark.p',axiom_005) ).
fof(axiom_006,axiom,
! [Y,N] : x22(s(N),Y) = x2(Y,x22(N,Y)),
file('theBenchmark.p',axiom_006) ).
fof(goal_007,conjecture,
? [X] : x22(X,X) != X,
file('theBenchmark.p',goal_007) ).
fof(goal_007_neg,negated_conjecture,
~ ? [X] : x22(X,X) != X,
inference(assume_negation,[status(cth)],[goal_007]) ).
cnf(c_8,plain,
proj1S(s(A)) = A,
inference(clausify,[status(thm)],[axiom_001]) ).
cnf(c_9,plain,
s(A) != z,
inference(clausify,[status(thm)],[axiom_002]) ).
cnf(c_10,plain,
x2(z,A) = A,
inference(clausify,[status(thm)],[axiom_003]) ).
cnf(c_11,plain,
x2(s(A),B) = s(x2(A,B)),
inference(clausify,[status(thm)],[axiom_004]) ).
cnf(c_12,plain,
s(x2(A,B)) = x2(s(A),B),
inference(copy,[status(thm)],[c_11]) ).
cnf(c_13,plain,
x22(z,A) = z,
inference(clausify,[status(thm)],[axiom_005]) ).
cnf(c_14,plain,
x22(s(A),B) = x2(B,x22(A,B)),
inference(clausify,[status(thm)],[axiom_006]) ).
cnf(c_15,plain,
x2(A,x22(B,A)) = x22(s(B),A),
inference(copy,[status(thm)],[c_14]) ).
cnf(c_16,negated_conjecture,
x22(A,A) = A,
inference(clausify,[status(thm)],[goal_007_neg]) ).
cnf(c_17,plain,
proj1S(x2(s(A),B)) = x2(A,B),
inference(paramod,[status(thm)],[c_12,c_8]) ).
cnf(c_111,plain,
s(A) = x2(s(z),A),
inference(paramod,[status(thm)],[c_10,c_12]) ).
cnf(c_19,plain,
x2(s(z),A) = s(A),
inference(copy,[status(thm)],[c_111]) ).
cnf(c_112,plain,
x2(A,z) = x22(s(z),A),
inference(paramod,[status(thm)],[c_13,c_15]) ).
cnf(c_22,plain,
x22(s(z),A) = x2(A,z),
inference(copy,[status(thm)],[c_112]) ).
cnf(c_113,plain,
proj1S(x22(s(A),s(B))) = x2(B,x22(A,s(B))),
inference(paramod,[status(thm)],[c_15,c_17]) ).
cnf(c_25,plain,
x2(A,x22(B,s(A))) = proj1S(x22(s(B),s(A))),
inference(copy,[status(thm)],[c_113]) ).
cnf(c_114,plain,
s(s(A)) = x2(s(s(z)),A),
inference(paramod,[status(thm)],[c_19,c_12]) ).
cnf(c_35,plain,
x2(s(s(z)),A) = s(s(A)),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_115,plain,
x2(A,x22(A,s(A))) = proj1S(s(A)),
inference(paramod,[status(thm)],[c_16,c_25]) ).
cnf(c_89,plain,
x2(A,x22(A,s(A))) = A,
inference(paramod,[status(thm)],[c_8,c_115]) ).
cnf(c_116,plain,
s(z) = s(x22(s(z),s(s(z)))),
inference(paramod,[status(thm)],[c_89,c_19]) ).
cnf(c_117,plain,
s(z) = s(x2(s(s(z)),z)),
inference(paramod,[status(thm)],[c_22,c_116]) ).
cnf(c_118,plain,
s(z) = s(s(s(z))),
inference(paramod,[status(thm)],[c_35,c_117]) ).
cnf(c_109,plain,
s(s(s(z))) = s(z),
inference(copy,[status(thm)],[c_118]) ).
cnf(c_119,plain,
proj1S(s(z)) = s(s(z)),
inference(paramod,[status(thm)],[c_109,c_8]) ).
cnf(c_120,plain,
z = s(s(z)),
inference(paramod,[status(thm)],[c_8,c_119]) ).
cnf(c_121,plain,
s(s(z)) = z,
inference(copy,[status(thm)],[c_120]) ).
cnf(c_110,plain,
$false,
inference(resolve,[status(thm)],[c_9,c_121]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX204+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.44 % Computer : n003.cluster.edu
% 0.11/0.44 % Model : x86_64 x86_64
% 0.11/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.44 % Memory : 8046.5625MB
% 0.11/0.44 % OS : Linux 6.8.0-71-generic
% 0.11/0.44 % CPULimit : 300
% 0.11/0.44 % WCLimit : 300
% 0.11/0.44 % DateTime : Sat Sep 26 16:57:24 UTC 2026
% 0.11/0.45 % CPUTime :
% 0.11/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.45 % Process 3353603 was started by sandbox on n003,
% 0.11/0.45 % Sat Sep 26 16:57:24 2026
% 0.11/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.45
% 0.11/0.45 % From the command line: assign(max_seconds, 300).
% 0.16/0.51
% 0.16/0.51 % SZS status Theorem for theBenchmark
% 0.16/0.51
% 0.16/0.51 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.16/0.51 % Length of proof is 24.
% 0.16/0.51 % Level of proof is 7.
% 0.16/0.51 % Maximum clause weight is 33.000.
% 0.16/0.51 % Given clauses 29.
% 0.16/0.51
% 0.16/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------