%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWC182+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 : n012.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:05 AM UTC 2026
% Result : Theorem 109.94s 15.13s
% Output : CNFRefutation 109.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 40 ( 19 unt; 0 def)
% Number of atoms : 128 ( 35 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 133 ( 45 ~; 38 |; 27 &)
% ( 3 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 42 ( 0 sgn 20 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax4,axiom,
! [U] :
( ssList(U)
=> ( singletonP(U)
<=> ? [V] :
( cons(V,nil) = U
& ssItem(V) ) ) ),
file('theBenchmark.p',ax4) ).
fof(ax7,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( segmentP(U,V)
<=> ? [W] :
( ? [X] :
( app(app(W,V),X) = U
& ssList(X) )
& ssList(W) ) ) ) ),
file('theBenchmark.p',ax7) ).
fof(ax16,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ssList(cons(V,U)) ) ),
file('theBenchmark.p',ax16) ).
fof(ax58,axiom,
! [U] :
( ssList(U)
=> ( segmentP(nil,U)
<=> nil = U ) ),
file('theBenchmark.p',ax58) ).
fof(co1,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [Y] :
( ssItem(Y)
=> ! [Z] :
( ssList(Z)
=> ! [X1] :
( ssList(X1)
=> ( ( ~ memberP(X1,Y)
& ~ memberP(Z,Y) )
| app(app(Z,cons(Y,nil)),X1) != U ) ) ) )
| U != W
| V != X
| nil != W ) ) ) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ! [Y] :
( ssItem(Y)
=> ! [Z] :
( ssList(Z)
=> ! [X1] :
( ssList(X1)
=> ( ( ~ memberP(X1,Y)
& ~ memberP(Z,Y) )
| app(app(Z,cons(Y,nil)),X1) != U ) ) ) )
| U != W
| V != X
| nil != W ) ) ) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_203,plain,
( cons(B,nil) != A
| ~ ssItem(B)
| singletonP(A)
| ~ ssList(A) ),
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_213,plain,
( app(app(C,B),D) != A
| ~ ssList(D)
| ~ ssList(C)
| segmentP(A,B)
| ~ ssList(B)
| ~ ssList(A) ),
inference(clausify,[status(thm)],[ax7]) ).
cnf(c_230,plain,
( ssList(cons(B,A))
| ~ ssItem(B)
| ~ ssList(A) ),
inference(clausify,[status(thm)],[ax16]) ).
fof(ax17,axiom,
ssList(nil),
file('theBenchmark.p',ax17) ).
cnf(c_231,plain,
ssList(nil),
inference(clausify,[status(thm)],[ax17]) ).
fof(ax39,axiom,
~ singletonP(nil),
file('theBenchmark.p',ax39) ).
cnf(c_262,plain,
~ singletonP(nil),
inference(clausify,[status(thm)],[ax39]) ).
cnf(c_285,plain,
( nil = A
| ~ segmentP(nil,A)
| ~ ssList(A) ),
inference(clausify,[status(thm)],[ax58]) ).
fof(nnf_87,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ? [Y] :
( ? [Z] :
( ? [X1] :
( ( memberP(X1,Y)
| memberP(Z,Y) )
& app(app(Z,cons(Y,nil)),X1) = U
& ssList(X1) )
& ssList(Z) )
& ssItem(Y) )
& W = U
& X = V
& nil = W
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(fof_nnf,[status(thm)],[co1_neg]) ).
fof(sk_co1_neg,plain,
( ( memberP(sK4,sK2)
| memberP(sK3,sK2) )
& app(app(sK3,cons(sK2,nil)),sK4) = sK1
& ssList(sK4)
& ssList(sK3)
& ssItem(sK2)
& sK0 = sK1
& sK9 = sK8
& nil = sK0
& ssList(sK9)
& ssList(sK0)
& ssList(sK8)
& ssList(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK8,sK0,sK9,sK2,sK3,sK4]),skolemize(U,sK1),skolemize(V,sK8),skolemize(W,sK0),skolemize(X,sK9),skolemize(Y,sK2),skolemize(Z,sK3),skolemize(X1,sK4)],[nnf_87]) ).
cnf(c_331,negated_conjecture,
nil = sK0,
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_332,negated_conjecture,
sK0 = nil,
inference(copy,[status(thm)],[c_331]) ).
cnf(c_334,negated_conjecture,
sK0 = sK1,
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_15701,negated_conjecture,
nil = sK1,
inference(paramod,[status(thm)],[c_332,c_334]) ).
cnf(c_335,negated_conjecture,
sK1 = nil,
inference(copy,[status(thm)],[c_15701]) ).
cnf(c_336,negated_conjecture,
ssItem(sK2),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_337,negated_conjecture,
ssList(sK3),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_338,negated_conjecture,
ssList(sK4),
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_339,negated_conjecture,
app(app(sK3,cons(sK2,nil)),sK4) = sK1,
inference(split_conjunct,[status(thm)],[sk_co1_neg]) ).
cnf(c_340,negated_conjecture,
app(app(sK3,cons(sK2,nil)),sK4) = nil,
inference(paramod,[status(thm)],[c_335,c_339]) ).
cnf(c_1675,plain,
( ssList(cons(A,nil))
| ~ ssItem(A) ),
inference(resolve,[status(thm)],[c_231,c_230]) ).
cnf(c_15702,plain,
( cons(A,nil) != nil
| ~ ssItem(A)
| singletonP(nil) ),
inference(resolve,[status(thm)],[c_231,c_203]) ).
cnf(c_1697,plain,
( cons(A,nil) != nil
| ~ ssItem(A) ),
inference(resolve,[status(thm)],[c_262,c_15702]) ).
cnf(c_15703,negated_conjecture,
( ~ ssList(sK4)
| ~ ssList(sK3)
| segmentP(nil,cons(sK2,nil))
| ~ ssList(cons(sK2,nil))
| ~ ssList(nil) ),
inference(resolve,[status(thm)],[c_340,c_213]) ).
cnf(c_15704,negated_conjecture,
( ~ ssList(sK4)
| ~ ssList(sK3)
| segmentP(nil,cons(sK2,nil))
| ~ ssList(cons(sK2,nil)) ),
inference(resolve,[status(thm)],[c_231,c_15703]) ).
cnf(c_15705,negated_conjecture,
( ~ ssList(sK4)
| segmentP(nil,cons(sK2,nil))
| ~ ssList(cons(sK2,nil)) ),
inference(resolve,[status(thm)],[c_337,c_15704]) ).
cnf(c_2658,negated_conjecture,
( segmentP(nil,cons(sK2,nil))
| ~ ssList(cons(sK2,nil)) ),
inference(resolve,[status(thm)],[c_338,c_15705]) ).
cnf(c_4998,plain,
cons(sK2,nil) != nil,
inference(resolve,[status(thm)],[c_1697,c_336]) ).
cnf(c_13267,plain,
ssList(cons(sK2,nil)),
inference(resolve,[status(thm)],[c_1675,c_336]) ).
cnf(c_13273,negated_conjecture,
segmentP(nil,cons(sK2,nil)),
inference(resolve,[status(thm)],[c_13267,c_2658]) ).
cnf(c_15706,plain,
( nil = cons(sK2,nil)
| ~ segmentP(nil,cons(sK2,nil)) ),
inference(resolve,[status(thm)],[c_13267,c_285]) ).
cnf(c_15707,plain,
( cons(sK2,nil) = nil
| ~ segmentP(nil,cons(sK2,nil)) ),
inference(copy,[status(thm)],[c_15706]) ).
cnf(c_15708,plain,
cons(sK2,nil) = nil,
inference(resolve,[status(thm)],[c_13273,c_15707]) ).
cnf(c_15700,plain,
$false,
inference(resolve,[status(thm)],[c_4998,c_15708]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC182+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n012.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 26 12:26:35 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.34 % Process 588594 was started by sandbox2 on n012,
% 0.07/0.34 % Sat Sep 26 12:26:35 2026
% 0.07/0.34 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.37
% 0.11/0.37 % From the command line: assign(max_seconds, 300).
% 109.94/15.13
% 109.94/15.13 % given #500 (I,wt=37): 698 -ssList(A) | ssList(f35(A)) | -ssItem(B) | -ssItem(C) | -ssList(D) | -ssList(E) | app(app(D,cons(B,D)),cons(C,E)) != A | C != B. [factor(366,e,f)].
% 109.94/15.13
% 109.94/15.13 % given #1000 (I,wt=52): 1218 -ssList(A) | app(app(f35(A),cons(f33(A),f36(A))),cons(f34(A),f37(A))) = A | -ssItem(B) | -ssItem(C) | -ssList(D) | app(app(A,cons(B,D)),cons(C,D)) != A | C != B. [factor(715,e,f)].
% 109.94/15.13
% 109.94/15.13 % given #1500 (A,wt=15): 1665 -ssList(app(A,A)) | -ssList(A) | frontsegP(app(A,A),A). [factor(1664,b,d)].
% 109.94/15.13
% 109.94/15.13 % SZS status Theorem for theBenchmark
% 109.94/15.13
% 109.94/15.13 % Proof 1 at 5.11 (+ 1.56) seconds.
% 109.94/15.13 % Length of proof is 27.
% 109.94/15.13 % Level of proof is 7.
% 109.94/15.13 % Maximum clause weight is 26.000.
% 109.94/15.13 % Given clauses 1585.
% 109.94/15.13
% 109.94/15.13 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------