%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWC109-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 : n013.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:56:52 AM UTC 2026
% Result : Unsatisfiable 217.97s 29.08s
% Output : CNFRefutation 217.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 25
% Syntax : Number of formulae : 116 ( 18 unt; 0 def)
% Number of atoms : 304 ( 126 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 317 ( 129 ~; 188 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 46 ( 2 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1_23,axiom,
( neq(sk2,nil)
| nil != sk1 ),
file('theBenchmark.p',co1_23) ).
cnf(c_53,plain,
( neq(sk2,nil)
| nil != sk1 ),
inference(clausify,[status(thm)],[co1_23]) ).
cnf(c_54,plain,
( neq(sk2,nil)
| sk1 != nil ),
inference(copy,[status(thm)],[c_53]) ).
fof(co1_22,axiom,
( ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil)
| nil = sk2 ),
file('theBenchmark.p',co1_22) ).
cnf(c_55,plain,
( ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil)
| nil = sk2 ),
inference(clausify,[status(thm)],[co1_22]) ).
cnf(c_56,plain,
( ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil)
| sk2 = nil ),
inference(copy,[status(thm)],[c_55]) ).
fof(co1_18,axiom,
( nil = sk3
| app(app(sk6,sk3),sk7) = sk4 ),
file('theBenchmark.p',co1_18) ).
cnf(c_63,plain,
( nil = sk3
| app(app(sk6,sk3),sk7) = sk4 ),
inference(clausify,[status(thm)],[co1_18]) ).
cnf(c_64,plain,
( sk3 = nil
| app(app(sk6,sk3),sk7) = sk4 ),
inference(copy,[status(thm)],[c_63]) ).
fof(co1_16,axiom,
( nil = sk3
| ssList(sk7) ),
file('theBenchmark.p',co1_16) ).
cnf(c_67,plain,
( nil = sk3
| ssList(sk7) ),
inference(clausify,[status(thm)],[co1_16]) ).
cnf(c_68,plain,
( sk3 = nil
| ssList(sk7) ),
inference(copy,[status(thm)],[c_67]) ).
fof(co1_15,axiom,
( nil = sk3
| ssList(sk6) ),
file('theBenchmark.p',co1_15) ).
cnf(c_69,plain,
( nil = sk3
| ssList(sk6) ),
inference(clausify,[status(thm)],[co1_15]) ).
cnf(c_70,plain,
( sk3 = nil
| ssList(sk6) ),
inference(copy,[status(thm)],[c_69]) ).
fof(co1_12,axiom,
( nil = sk4
| app(app(sk6,sk3),sk7) = sk4 ),
file('theBenchmark.p',co1_12) ).
cnf(c_75,plain,
( nil = sk4
| app(app(sk6,sk3),sk7) = sk4 ),
inference(clausify,[status(thm)],[co1_12]) ).
cnf(c_76,plain,
( sk4 = nil
| app(app(sk6,sk3),sk7) = sk4 ),
inference(copy,[status(thm)],[c_75]) ).
fof(co1_11,axiom,
( nil = sk4
| cons(sk5,nil) = sk3 ),
file('theBenchmark.p',co1_11) ).
cnf(c_77,plain,
( nil = sk4
| cons(sk5,nil) = sk3 ),
inference(clausify,[status(thm)],[co1_11]) ).
cnf(c_78,plain,
( sk4 = nil
| cons(sk5,nil) = sk3 ),
inference(copy,[status(thm)],[c_77]) ).
fof(co1_10,axiom,
( nil = sk4
| ssList(sk7) ),
file('theBenchmark.p',co1_10) ).
cnf(c_79,plain,
( nil = sk4
| ssList(sk7) ),
inference(clausify,[status(thm)],[co1_10]) ).
cnf(c_80,plain,
( sk4 = nil
| ssList(sk7) ),
inference(copy,[status(thm)],[c_79]) ).
fof(co1_9,axiom,
( nil = sk4
| ssList(sk6) ),
file('theBenchmark.p',co1_9) ).
cnf(c_81,plain,
( nil = sk4
| ssList(sk6) ),
inference(clausify,[status(thm)],[co1_9]) ).
cnf(c_82,plain,
( sk4 = nil
| ssList(sk6) ),
inference(copy,[status(thm)],[c_81]) ).
fof(co1_7,axiom,
( nil = sk4
| ssItem(sk5) ),
file('theBenchmark.p',co1_7) ).
cnf(c_85,plain,
( nil = sk4
| ssItem(sk5) ),
inference(clausify,[status(thm)],[co1_7]) ).
cnf(c_86,plain,
( sk4 = nil
| ssItem(sk5) ),
inference(copy,[status(thm)],[c_85]) ).
fof(co1_6,axiom,
sk1 = sk3,
file('theBenchmark.p',co1_6) ).
cnf(c_87,plain,
sk1 = sk3,
inference(clausify,[status(thm)],[co1_6]) ).
fof(co1_5,axiom,
sk2 = sk4,
file('theBenchmark.p',co1_5) ).
cnf(c_88,plain,
sk2 = sk4,
inference(clausify,[status(thm)],[co1_5]) ).
fof(co1_4,axiom,
ssList(sk4),
file('theBenchmark.p',co1_4) ).
cnf(c_89,plain,
ssList(sk4),
inference(clausify,[status(thm)],[co1_4]) ).
fof(co1_3,axiom,
ssList(sk3),
file('theBenchmark.p',co1_3) ).
cnf(c_90,plain,
ssList(sk3),
inference(clausify,[status(thm)],[co1_3]) ).
fof(clause173,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( segmentP(VAR_3,VAR_1)
| ~ ssList(VAR_3)
| ~ ssList(VAR_1)
| ~ ssList(VAR_0)
| ~ ssList(VAR_2)
| app(app(VAR_0,VAR_1),VAR_2) != VAR_3 ),
file('theBenchmark.p',clause173) ).
cnf(c_100,plain,
( segmentP(D,B)
| ~ ssList(D)
| ~ ssList(B)
| ~ ssList(A)
| ~ ssList(C)
| app(app(A,B),C) != D ),
inference(clausify,[status(thm)],[clause173]) ).
fof(clause152,axiom,
! [VAR_0,VAR_1,VAR_2] :
( segmentP(VAR_0,VAR_2)
| ~ ssList(VAR_0)
| ~ ssList(VAR_1)
| ~ ssList(VAR_2)
| ~ segmentP(VAR_1,VAR_2)
| ~ segmentP(VAR_0,VAR_1) ),
file('theBenchmark.p',clause152) ).
cnf(c_118,plain,
( segmentP(A,C)
| ~ ssList(A)
| ~ ssList(B)
| ~ ssList(C)
| ~ segmentP(B,C)
| ~ segmentP(A,B) ),
inference(clausify,[status(thm)],[clause152]) ).
fof(clause116,axiom,
! [VAR_0,VAR_1] :
( singletonP(VAR_1)
| ~ ssList(VAR_1)
| ~ ssItem(VAR_0)
| cons(VAR_0,nil) != VAR_1 ),
file('theBenchmark.p',clause116) ).
cnf(c_152,plain,
( singletonP(B)
| ~ ssList(B)
| ~ ssItem(A)
| cons(A,nil) != B ),
inference(clausify,[status(thm)],[clause116]) ).
fof(clause115,axiom,
! [VAR_0,VAR_1] :
( ~ ssList(VAR_0)
| ~ ssList(VAR_1)
| ~ neq(VAR_0,VAR_1)
| VAR_0 != VAR_1 ),
file('theBenchmark.p',clause115) ).
cnf(c_153,plain,
( ~ ssList(A)
| ~ ssList(B)
| ~ neq(A,B)
| A != B ),
inference(clausify,[status(thm)],[clause115]) ).
fof(clause101,axiom,
! [VAR_0] :
( cons(skaf44(VAR_0),nil) = VAR_0
| ~ ssList(VAR_0)
| ~ singletonP(VAR_0) ),
file('theBenchmark.p',clause101) ).
cnf(c_167,plain,
( cons(skaf44(A),nil) = A
| ~ ssList(A)
| ~ singletonP(A) ),
inference(clausify,[status(thm)],[clause101]) ).
fof(clause100,axiom,
! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| neq(VAR_1,VAR_0)
| ~ ssList(VAR_1)
| ~ ssList(VAR_0) ),
file('theBenchmark.p',clause100) ).
cnf(c_168,plain,
( B = A
| neq(B,A)
| ~ ssList(B)
| ~ ssList(A) ),
inference(clausify,[status(thm)],[clause100]) ).
fof(clause98,axiom,
! [VAR_0,VAR_1] :
( ~ ssList(VAR_1)
| ~ ssItem(VAR_0)
| cons(VAR_0,VAR_1) != nil ),
file('theBenchmark.p',clause98) ).
cnf(c_170,plain,
( ~ ssList(B)
| ~ ssItem(A)
| cons(A,B) != nil ),
inference(clausify,[status(thm)],[clause98]) ).
fof(clause80,axiom,
! [VAR_0] :
( nil = VAR_0
| ~ ssList(VAR_0)
| ~ segmentP(nil,VAR_0) ),
file('theBenchmark.p',clause80) ).
cnf(c_181,plain,
( nil = A
| ~ ssList(A)
| ~ segmentP(nil,A) ),
inference(clausify,[status(thm)],[clause80]) ).
fof(clause79,axiom,
! [VAR_0] :
( segmentP(nil,VAR_0)
| ~ ssList(VAR_0)
| nil != VAR_0 ),
file('theBenchmark.p',clause79) ).
cnf(c_182,plain,
( segmentP(nil,A)
| ~ ssList(A)
| nil != A ),
inference(clausify,[status(thm)],[clause79]) ).
fof(clause47,axiom,
! [VAR_0] : ssItem(skaf44(VAR_0)),
file('theBenchmark.p',clause47) ).
cnf(c_206,plain,
ssItem(skaf44(A)),
inference(clausify,[status(thm)],[clause47]) ).
fof(clause8,axiom,
ssList(nil),
file('theBenchmark.p',clause8) ).
cnf(c_245,plain,
ssList(nil),
inference(clausify,[status(thm)],[clause8]) ).
cnf(c_13263,plain,
( ~ segmentP(sk2,sk1)
| ~ neq(sk1,nil)
| sk4 = nil ),
inference(paramod,[status(thm)],[c_88,c_56]) ).
cnf(c_13264,plain,
( ~ segmentP(sk2,sk1)
| ~ neq(sk3,nil)
| sk4 = nil ),
inference(paramod,[status(thm)],[c_87,c_13263]) ).
cnf(c_13265,plain,
( ~ segmentP(sk4,sk1)
| ~ neq(sk3,nil)
| sk4 = nil ),
inference(paramod,[status(thm)],[c_88,c_13264]) ).
cnf(c_349,plain,
( ~ segmentP(sk4,sk3)
| ~ neq(sk3,nil)
| sk4 = nil ),
inference(paramod,[status(thm)],[c_87,c_13265]) ).
cnf(c_13266,plain,
( neq(sk2,nil)
| sk3 != nil ),
inference(paramod,[status(thm)],[c_87,c_54]) ).
cnf(c_350,plain,
( neq(sk4,nil)
| sk3 != nil ),
inference(paramod,[status(thm)],[c_88,c_13266]) ).
cnf(c_13267,plain,
( ~ ssList(A)
| ~ neq(A,A)
| A != A ),
inference(factor,[status(thm)],[c_153]) ).
cnf(c_417,plain,
( ~ ssList(A)
| ~ neq(A,A) ),
inference(copy,[status(thm)],[c_13267]) ).
cnf(c_13268,plain,
( sk4 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk4)
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_100,c_76]) ).
cnf(c_13269,plain,
( sk4 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk4)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_90,c_13268]) ).
cnf(c_930,plain,
( sk4 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_89,c_13269]) ).
cnf(c_13270,plain,
( sk3 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk4)
| ~ ssList(sk3)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_100,c_64]) ).
cnf(c_13271,plain,
( sk3 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk4)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_90,c_13270]) ).
cnf(c_931,plain,
( sk3 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk6)
| ~ ssList(sk7) ),
inference(resolve,[status(thm)],[c_89,c_13271]) ).
cnf(c_13272,plain,
( sk4 = nil
| singletonP(sk3)
| ~ ssList(sk3)
| ~ ssItem(sk5) ),
inference(resolve,[status(thm)],[c_152,c_78]) ).
cnf(c_1518,plain,
( sk4 = nil
| singletonP(sk3)
| ~ ssItem(sk5) ),
inference(resolve,[status(thm)],[c_90,c_13272]) ).
cnf(c_1623,plain,
( sk3 = A
| neq(sk3,A)
| ~ ssList(A) ),
inference(resolve,[status(thm)],[c_168,c_90]) ).
cnf(c_13273,plain,
( nil = sk3
| ~ segmentP(nil,sk3) ),
inference(resolve,[status(thm)],[c_181,c_90]) ).
cnf(c_1719,plain,
( sk3 = nil
| ~ segmentP(nil,sk3) ),
inference(copy,[status(thm)],[c_13273]) ).
cnf(c_13274,plain,
( segmentP(nil,sk4)
| nil != sk4 ),
inference(resolve,[status(thm)],[c_182,c_89]) ).
cnf(c_1727,plain,
( segmentP(nil,sk4)
| sk4 != nil ),
inference(copy,[status(thm)],[c_13274]) ).
cnf(c_5175,plain,
( ~ ssItem(A)
| cons(A,nil) != nil ),
inference(resolve,[status(thm)],[c_245,c_170]) ).
cnf(c_5934,plain,
~ neq(nil,nil),
inference(resolve,[status(thm)],[c_417,c_245]) ).
cnf(c_13275,plain,
( sk4 = nil
| sk4 = nil
| singletonP(sk3) ),
inference(resolve,[status(thm)],[c_1518,c_86]) ).
cnf(c_7130,plain,
( sk4 = nil
| singletonP(sk3) ),
inference(copy,[status(thm)],[c_13275]) ).
cnf(c_13276,plain,
( cons(skaf44(sk3),nil) = sk3
| ~ ssList(sk3)
| sk4 = nil ),
inference(resolve,[status(thm)],[c_7130,c_167]) ).
cnf(c_7145,plain,
( cons(skaf44(sk3),nil) = sk3
| sk4 = nil ),
inference(resolve,[status(thm)],[c_90,c_13276]) ).
cnf(c_7228,plain,
( sk3 = nil
| neq(sk3,nil) ),
inference(resolve,[status(thm)],[c_1623,c_245]) ).
cnf(c_7260,plain,
( ~ segmentP(sk4,sk3)
| sk4 = nil
| sk3 = nil ),
inference(resolve,[status(thm)],[c_7228,c_349]) ).
cnf(c_8710,plain,
cons(skaf44(A),nil) != nil,
inference(resolve,[status(thm)],[c_5175,c_206]) ).
cnf(c_13277,plain,
( sk4 = nil
| sk4 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk6) ),
inference(resolve,[status(thm)],[c_930,c_80]) ).
cnf(c_9372,plain,
( sk4 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk6) ),
inference(copy,[status(thm)],[c_13277]) ).
cnf(c_13278,plain,
( sk4 = nil
| sk4 = nil
| segmentP(sk4,sk3) ),
inference(resolve,[status(thm)],[c_9372,c_82]) ).
cnf(c_9374,plain,
( sk4 = nil
| segmentP(sk4,sk3) ),
inference(copy,[status(thm)],[c_13278]) ).
cnf(c_13279,plain,
( sk4 = nil
| sk3 = nil
| sk4 = nil ),
inference(resolve,[status(thm)],[c_9374,c_7260]) ).
cnf(c_9375,plain,
( sk3 = nil
| sk4 = nil ),
inference(copy,[status(thm)],[c_13279]) ).
cnf(c_9391,plain,
( segmentP(nil,sk4)
| sk3 = nil ),
inference(resolve,[status(thm)],[c_9375,c_1727]) ).
cnf(c_13280,plain,
( sk3 = nil
| sk3 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk6) ),
inference(resolve,[status(thm)],[c_931,c_68]) ).
cnf(c_9413,plain,
( sk3 = nil
| segmentP(sk4,sk3)
| ~ ssList(sk6) ),
inference(copy,[status(thm)],[c_13280]) ).
cnf(c_13281,plain,
( segmentP(nil,A)
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ ssList(A)
| ~ segmentP(sk4,A)
| sk3 = nil ),
inference(resolve,[status(thm)],[c_9391,c_118]) ).
cnf(c_13282,plain,
( segmentP(nil,A)
| ~ ssList(nil)
| ~ ssList(A)
| ~ segmentP(sk4,A)
| sk3 = nil ),
inference(resolve,[status(thm)],[c_89,c_13281]) ).
cnf(c_9423,plain,
( segmentP(nil,A)
| ~ ssList(A)
| ~ segmentP(sk4,A)
| sk3 = nil ),
inference(resolve,[status(thm)],[c_245,c_13282]) ).
cnf(c_13283,plain,
( sk3 = nil
| sk3 = nil
| segmentP(sk4,sk3) ),
inference(resolve,[status(thm)],[c_9413,c_70]) ).
cnf(c_9479,plain,
( sk3 = nil
| segmentP(sk4,sk3) ),
inference(copy,[status(thm)],[c_13283]) ).
cnf(c_13284,plain,
( sk3 = nil
| segmentP(nil,sk3)
| ~ ssList(sk3)
| sk3 = nil ),
inference(resolve,[status(thm)],[c_9423,c_9479]) ).
cnf(c_13285,plain,
( segmentP(nil,sk3)
| ~ ssList(sk3)
| sk3 = nil ),
inference(copy,[status(thm)],[c_13284]) ).
cnf(c_13103,plain,
( segmentP(nil,sk3)
| sk3 = nil ),
inference(resolve,[status(thm)],[c_90,c_13285]) ).
cnf(c_13286,plain,
( sk3 = nil
| sk3 = nil ),
inference(resolve,[status(thm)],[c_13103,c_1719]) ).
cnf(c_13144,plain,
sk3 = nil,
inference(copy,[status(thm)],[c_13286]) ).
cnf(c_13287,plain,
( cons(skaf44(nil),nil) = sk3
| sk4 = nil ),
inference(paramod,[status(thm)],[c_13144,c_7145]) ).
cnf(c_13288,plain,
( cons(skaf44(nil),nil) = nil
| sk4 = nil ),
inference(paramod,[status(thm)],[c_13144,c_13287]) ).
cnf(c_13194,plain,
sk4 = nil,
inference(resolve,[status(thm)],[c_8710,c_13288]) ).
cnf(c_13289,plain,
( neq(sk4,nil)
| nil != nil ),
inference(paramod,[status(thm)],[c_13144,c_350]) ).
cnf(c_13290,plain,
( neq(nil,nil)
| nil != nil ),
inference(paramod,[status(thm)],[c_13194,c_13289]) ).
cnf(c_13291,plain,
neq(nil,nil),
inference(copy,[status(thm)],[c_13290]) ).
cnf(c_13262,plain,
$false,
inference(resolve,[status(thm)],[c_5934,c_13291]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC109-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n013.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sat Sep 26 12:15:50 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.46 % Process 2706529 was started by sandbox2 on n013,
% 0.19/0.46 % Sat Sep 26 12:15:50 2026
% 0.19/0.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.19/0.47
% 0.19/0.47 % From the command line: assign(max_seconds, 300).
% 217.97/29.08
% 217.97/29.08 % given #500 (I,wt=52): 572 app(app(A,cons(B,A)),cons(C,D)) != D | -ssList(D) | -ssList(A) | -ssItem(C) | -ssItem(B) | lt(B,C) | lt(C,B) | -lt(skaf60(D),skaf59(D)). [factor(315,c,d)].
% 217.97/29.08
% 217.97/29.08 % given #1000 (F,wt=15): 4213 -lt(skaf74(A),skaf74(A)). [resolve(232,a,190,b)].
% 217.97/29.08
% 217.97/29.08 % given #1500 (T,wt=11): 9385 sk4 = nil | -neq(sk3,nil). [resolve(9374,a,349,c),merge(b)].
% 217.97/29.08
% 217.97/29.08 % given #2000 (F,wt=18): 6924 skaf67(A) != nil | -neq(nil,skaf67(A)). [resolve(5178,c,225,a),flip(a)].
% 217.97/29.08
% 217.97/29.08 % SZS status Unsatisfiable for theBenchmark
% 217.97/29.08
% 217.97/29.08 % Proof 1 at 3.19 (+ 1.14) seconds.
% 217.97/29.08 % Length of proof is 62.
% 217.97/29.08 % Level of proof is 11.
% 217.97/29.08 % Maximum clause weight is 35.000.
% 217.97/29.08 % Given clauses 2091.
% 217.97/29.08
% 217.97/29.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------