%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWC153-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 08:57:01 AM UTC 2026
% Result : Unsatisfiable 224.11s 29.98s
% Output : CNFRefutation 224.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 15
% Syntax : Number of formulae : 68 ( 26 unt; 0 def)
% Number of atoms : 237 ( 18 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 343 ( 174 ~; 169 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 53 ( 0 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clause130,axiom,
! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| ~ ssItem(VAR_1)
| ~ ssItem(VAR_0)
| ~ leq(VAR_1,VAR_0)
| ~ leq(VAR_0,VAR_1) ),
file('theBenchmark.p',clause130) ).
cnf(c_151,plain,
( B = A
| ~ ssItem(B)
| ~ ssItem(A)
| ~ leq(B,A)
| ~ leq(A,B) ),
inference(clausify,[status(thm)],[clause130]) ).
fof(co1_6,axiom,
sk3 = sk1,
file('theBenchmark.p',co1_6) ).
cnf(c_203,plain,
sk3 = sk1,
inference(clausify,[status(thm)],[co1_6]) ).
cnf(c_204,plain,
sk1 = sk3,
inference(copy,[status(thm)],[c_203]) ).
fof(co1_7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( leq(VAR_0,VAR_1)
| ~ leq(VAR_1,VAR_0)
| app(app(app(app(VAR_2,cons(VAR_0,nil)),VAR_3),cons(VAR_1,nil)),VAR_4) != sk3
| ~ ssList(VAR_4)
| ~ ssList(VAR_3)
| ~ ssList(VAR_2)
| ~ ssItem(VAR_1)
| ~ ssItem(VAR_0) ),
file('theBenchmark.p',co1_7) ).
cnf(c_205,plain,
( leq(A,B)
| ~ leq(B,A)
| app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E) != sk3
| ~ ssList(E)
| ~ ssList(D)
| ~ ssList(C)
| ~ ssItem(B)
| ~ ssItem(A) ),
inference(clausify,[status(thm)],[co1_7]) ).
fof(co1_8,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( leq(VAR_0,VAR_5)
| ~ memberP(VAR_3,VAR_5)
| ~ ssItem(VAR_5)
| ~ leq(VAR_1,VAR_0)
| app(app(app(app(VAR_2,cons(VAR_0,nil)),VAR_3),cons(VAR_1,nil)),VAR_4) != sk3
| ~ ssList(VAR_4)
| ~ ssList(VAR_3)
| ~ ssList(VAR_2)
| ~ ssItem(VAR_1)
| ~ ssItem(VAR_0) ),
file('theBenchmark.p',co1_8) ).
cnf(c_206,plain,
( leq(A,F)
| ~ memberP(D,F)
| ~ ssItem(F)
| ~ leq(B,A)
| app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E) != sk3
| ~ ssList(E)
| ~ ssList(D)
| ~ ssList(C)
| ~ ssItem(B)
| ~ ssItem(A) ),
inference(clausify,[status(thm)],[co1_8]) ).
fof(co1_9,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( leq(VAR_5,VAR_1)
| ~ memberP(VAR_3,VAR_5)
| ~ ssItem(VAR_5)
| ~ leq(VAR_1,VAR_0)
| app(app(app(app(VAR_2,cons(VAR_0,nil)),VAR_3),cons(VAR_1,nil)),VAR_4) != sk3
| ~ ssList(VAR_4)
| ~ ssList(VAR_3)
| ~ ssList(VAR_2)
| ~ ssItem(VAR_1)
| ~ ssItem(VAR_0) ),
file('theBenchmark.p',co1_9) ).
cnf(c_207,plain,
( leq(F,B)
| ~ memberP(D,F)
| ~ ssItem(F)
| ~ leq(B,A)
| app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E) != sk3
| ~ ssList(E)
| ~ ssList(D)
| ~ ssList(C)
| ~ ssItem(B)
| ~ ssItem(A) ),
inference(clausify,[status(thm)],[co1_9]) ).
fof(co1_10,axiom,
ssItem(sk5),
file('theBenchmark.p',co1_10) ).
cnf(c_208,plain,
ssItem(sk5),
inference(clausify,[status(thm)],[co1_10]) ).
fof(co1_11,axiom,
ssItem(sk6),
file('theBenchmark.p',co1_11) ).
cnf(c_209,plain,
ssItem(sk6),
inference(clausify,[status(thm)],[co1_11]) ).
fof(co1_12,axiom,
ssList(sk7),
file('theBenchmark.p',co1_12) ).
cnf(c_210,plain,
ssList(sk7),
inference(clausify,[status(thm)],[co1_12]) ).
fof(co1_13,axiom,
ssList(sk8),
file('theBenchmark.p',co1_13) ).
cnf(c_211,plain,
ssList(sk8),
inference(clausify,[status(thm)],[co1_13]) ).
fof(co1_14,axiom,
ssList(sk9),
file('theBenchmark.p',co1_14) ).
cnf(c_212,plain,
ssList(sk9),
inference(clausify,[status(thm)],[co1_14]) ).
fof(co1_15,axiom,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('theBenchmark.p',co1_15) ).
cnf(c_213,plain,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
inference(clausify,[status(thm)],[co1_15]) ).
cnf(c_214,plain,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk3,
inference(paramod,[status(thm)],[c_204,c_213]) ).
fof(co1_16,axiom,
leq(sk6,sk5),
file('theBenchmark.p',co1_16) ).
cnf(c_215,plain,
leq(sk6,sk5),
inference(clausify,[status(thm)],[co1_16]) ).
fof(co1_17,axiom,
( ~ leq(sk5,sk6)
| ssItem(sk10) ),
file('theBenchmark.p',co1_17) ).
cnf(c_216,plain,
( ~ leq(sk5,sk6)
| ssItem(sk10) ),
inference(clausify,[status(thm)],[co1_17]) ).
fof(co1_18,axiom,
( ~ leq(sk5,sk6)
| memberP(sk8,sk10) ),
file('theBenchmark.p',co1_18) ).
cnf(c_217,plain,
( ~ leq(sk5,sk6)
| memberP(sk8,sk10) ),
inference(clausify,[status(thm)],[co1_18]) ).
fof(co1_19,axiom,
( ~ leq(sk5,sk6)
| ~ leq(sk5,sk10)
| ~ leq(sk10,sk6) ),
file('theBenchmark.p',co1_19) ).
cnf(c_218,plain,
( ~ leq(sk5,sk6)
| ~ leq(sk5,sk10)
| ~ leq(sk10,sk6) ),
inference(clausify,[status(thm)],[co1_19]) ).
cnf(c_6923,plain,
( leq(A,sk6)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7)
| ~ ssItem(sk6)
| ~ ssItem(sk5) ),
inference(resolve,[status(thm)],[c_214,c_207]) ).
cnf(c_6924,plain,
( leq(A,sk6)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7)
| ~ ssItem(sk6) ),
inference(resolve,[status(thm)],[c_208,c_6923]) ).
cnf(c_6925,plain,
( leq(A,sk6)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_209,c_6924]) ).
cnf(c_6926,plain,
( leq(A,sk6)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8) ),
inference(resolve,[status(thm)],[c_210,c_6925]) ).
cnf(c_6927,plain,
( leq(A,sk6)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9) ),
inference(resolve,[status(thm)],[c_211,c_6926]) ).
cnf(c_6928,plain,
( leq(A,sk6)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5) ),
inference(resolve,[status(thm)],[c_212,c_6927]) ).
cnf(c_4806,plain,
( leq(A,sk6)
| ~ memberP(sk8,A)
| ~ ssItem(A) ),
inference(resolve,[status(thm)],[c_215,c_6928]) ).
cnf(c_6929,plain,
( leq(sk5,A)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7)
| ~ ssItem(sk6)
| ~ ssItem(sk5) ),
inference(resolve,[status(thm)],[c_214,c_206]) ).
cnf(c_6930,plain,
( leq(sk5,A)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7)
| ~ ssItem(sk6) ),
inference(resolve,[status(thm)],[c_208,c_6929]) ).
cnf(c_6931,plain,
( leq(sk5,A)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_209,c_6930]) ).
cnf(c_6932,plain,
( leq(sk5,A)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8) ),
inference(resolve,[status(thm)],[c_210,c_6931]) ).
cnf(c_6933,plain,
( leq(sk5,A)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5)
| ~ ssList(sk9) ),
inference(resolve,[status(thm)],[c_211,c_6932]) ).
cnf(c_6934,plain,
( leq(sk5,A)
| ~ memberP(sk8,A)
| ~ ssItem(A)
| ~ leq(sk6,sk5) ),
inference(resolve,[status(thm)],[c_212,c_6933]) ).
cnf(c_4807,plain,
( leq(sk5,A)
| ~ memberP(sk8,A)
| ~ ssItem(A) ),
inference(resolve,[status(thm)],[c_215,c_6934]) ).
cnf(c_6935,plain,
( leq(sk5,sk6)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7)
| ~ ssItem(sk6)
| ~ ssItem(sk5) ),
inference(resolve,[status(thm)],[c_214,c_205]) ).
cnf(c_6936,plain,
( leq(sk5,sk6)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7)
| ~ ssItem(sk6) ),
inference(resolve,[status(thm)],[c_208,c_6935]) ).
cnf(c_6937,plain,
( leq(sk5,sk6)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_209,c_6936]) ).
cnf(c_6938,plain,
( leq(sk5,sk6)
| ~ leq(sk6,sk5)
| ~ ssList(sk9)
| ~ ssList(sk8) ),
inference(resolve,[status(thm)],[c_210,c_6937]) ).
cnf(c_6939,plain,
( leq(sk5,sk6)
| ~ leq(sk6,sk5)
| ~ ssList(sk9) ),
inference(resolve,[status(thm)],[c_211,c_6938]) ).
cnf(c_6940,plain,
( leq(sk5,sk6)
| ~ leq(sk6,sk5) ),
inference(resolve,[status(thm)],[c_212,c_6939]) ).
cnf(c_4808,plain,
leq(sk5,sk6),
inference(resolve,[status(thm)],[c_215,c_6940]) ).
cnf(c_4809,plain,
( ~ leq(sk5,sk10)
| ~ leq(sk10,sk6) ),
inference(resolve,[status(thm)],[c_4808,c_218]) ).
cnf(c_4810,plain,
memberP(sk8,sk10),
inference(resolve,[status(thm)],[c_4808,c_217]) ).
cnf(c_4811,plain,
ssItem(sk10),
inference(resolve,[status(thm)],[c_4808,c_216]) ).
cnf(c_6941,plain,
( sk6 = sk5
| ~ ssItem(sk6)
| ~ ssItem(sk5)
| ~ leq(sk5,sk6) ),
inference(resolve,[status(thm)],[c_215,c_151]) ).
cnf(c_6942,plain,
( sk6 = sk5
| ~ ssItem(sk6)
| ~ ssItem(sk5) ),
inference(resolve,[status(thm)],[c_4808,c_6941]) ).
cnf(c_6943,plain,
( sk6 = sk5
| ~ ssItem(sk6) ),
inference(resolve,[status(thm)],[c_208,c_6942]) ).
cnf(c_4815,plain,
sk6 = sk5,
inference(resolve,[status(thm)],[c_209,c_6943]) ).
cnf(c_4816,plain,
( ~ leq(sk5,sk10)
| ~ leq(sk10,sk5) ),
inference(paramod,[status(thm)],[c_4815,c_4809]) ).
cnf(c_4817,plain,
( leq(A,sk5)
| ~ memberP(sk8,A)
| ~ ssItem(A) ),
inference(paramod,[status(thm)],[c_4815,c_4806]) ).
cnf(c_6944,plain,
( leq(sk5,sk10)
| ~ memberP(sk8,sk10) ),
inference(resolve,[status(thm)],[c_4807,c_4811]) ).
cnf(c_6882,plain,
leq(sk5,sk10),
inference(resolve,[status(thm)],[c_4810,c_6944]) ).
cnf(c_6902,plain,
~ leq(sk10,sk5),
inference(resolve,[status(thm)],[c_6882,c_4816]) ).
cnf(c_6945,plain,
( leq(sk10,sk5)
| ~ memberP(sk8,sk10) ),
inference(resolve,[status(thm)],[c_4817,c_4811]) ).
cnf(c_6946,plain,
leq(sk10,sk5),
inference(resolve,[status(thm)],[c_4810,c_6945]) ).
cnf(c_6922,plain,
$false,
inference(resolve,[status(thm)],[c_6902,c_6946]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC153-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 12:21:02 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 3127667 was started by sandbox2 on n014,
% 0.10/0.36 % Sat Sep 26 12:21:02 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 224.11/29.98
% 224.11/29.98 % given #500 (I,wt=46): 559 app(app(A,cons(B,C)),cons(B,D)) != A | -ssList(D) | -ssList(C) | -ssList(A) | -ssItem(B) | -strictorderedP(A) | lt(B,B). [factor(360,e,f)].
% 224.11/29.98
% 224.11/29.98 % given #1000 (W,wt=11): 6509 -lt(sk5,skac3) | gt(skac3,sk5). [resolve(1808,b,208,a)].
% 224.11/29.98
% 224.11/29.98 % SZS status Unsatisfiable for theBenchmark
% 224.11/29.98
% 224.11/29.98 % Proof 1 at 3.80 (+ 1.47) seconds.
% 224.11/29.98 % Length of proof is 29.
% 224.11/29.98 % Level of proof is 7.
% 224.11/29.98 % Maximum clause weight is 72.000.
% 224.11/29.98 % Given clauses 1106.
% 224.11/29.98
% 224.11/29.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------