%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC220-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Thu Sep 24 02:41:54 PM UTC 2026
% Result : Unsatisfiable 4.01s 1.08s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC220-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n019.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.46 % DateTime : Mon Sep 21 08:05:35 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.49 % Drodi V4.1.1
% 4.01/1.08 % Refutation found
% 4.01/1.08 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.01/1.08 % SZS output start CNFRefutation for theBenchmark
% 4.01/1.08 fof(f8,axiom,(
% 4.01/1.08 ssList(nil) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f9,axiom,(
% 4.01/1.08 ssItem(skac3) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f10,axiom,(
% 4.01/1.08 ssItem(skac2) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f48,axiom,(
% 4.01/1.08 (![U,V]: (ssList(skaf48(U,V)) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f57,axiom,(
% 4.01/1.08 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f62,axiom,(
% 4.01/1.08 (![U]: (( ~ ssItem(U)| leq(U,U) ) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f186,negated_conjecture,(
% 4.01/1.08 ssList(sk1) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f187,negated_conjecture,(
% 4.01/1.08 ssList(sk2) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f191,negated_conjecture,(
% 4.01/1.08 sk1 = sk3 ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f192,negated_conjecture,(
% 4.01/1.08 nil != sk1 ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f193,negated_conjecture,(
% 4.01/1.08 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk1| ssItem(sk5(C,B,A)) ) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f194,negated_conjecture,(
% 4.01/1.08 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk1| memberP(B,sk5(C,B,A)) ) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f195,negated_conjecture,(
% 4.01/1.08 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk1| memberP(C,sk5(C,B,A)) ) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f196,negated_conjecture,(
% 4.01/1.08 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk1| leq(A,sk5(C,B,A)) ) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f197,negated_conjecture,(
% 4.01/1.08 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk1| ~ leq(sk5(C,B,A),A) ) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f198,negated_conjecture,(
% 4.01/1.08 ( nil = sk3| ssItem(sk6) ) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f199,negated_conjecture,(
% 4.01/1.08 ( nil = sk3| ssList(sk7) ) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f200,negated_conjecture,(
% 4.01/1.08 ( nil = sk3| ssList(sk8) ) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f201,negated_conjecture,(
% 4.01/1.08 ( nil = sk3| app(app(sk7,cons(sk6,nil)),sk8) = sk3 ) ),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f202,negated_conjecture,(
% 4.01/1.08 (![A]: (( nil = sk3| ~ ssItem(A)| leq(A,sk6)| ~ memberP(sk7,A)| ~ memberP(sk8,A)| ~ leq(sk6,A) ) ))),
% 4.01/1.08 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.01/1.08 fof(f210,plain,(
% 4.01/1.08 ssList(nil)),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f8])).
% 4.01/1.08 fof(f211,plain,(
% 4.01/1.08 ssItem(skac3)),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f9])).
% 4.01/1.08 fof(f212,plain,(
% 4.01/1.08 ssItem(skac2)),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f10])).
% 4.01/1.08 fof(f250,plain,(
% 4.01/1.08 ![X0,X1]: (ssList(skaf48(X0,X1)))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f48])).
% 4.01/1.08 fof(f259,plain,(
% 4.01/1.08 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f57])).
% 4.01/1.08 fof(f264,plain,(
% 4.01/1.08 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f62])).
% 4.01/1.08 fof(f433,plain,(
% 4.01/1.08 ssList(sk1)),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f186])).
% 4.01/1.08 fof(f434,plain,(
% 4.01/1.08 ssList(sk2)),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f187])).
% 4.01/1.08 fof(f438,plain,(
% 4.01/1.08 sk1=sk3),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f191])).
% 4.01/1.08 fof(f439,plain,(
% 4.01/1.08 ~nil=sk1),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f192])).
% 4.01/1.08 fof(f440,plain,(
% 4.01/1.08 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk1|ssItem(sk5(X2,X1,X0)))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f193])).
% 4.01/1.08 fof(f441,plain,(
% 4.01/1.08 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk1|memberP(X1,sk5(X2,X1,X0)))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f194])).
% 4.01/1.08 fof(f442,plain,(
% 4.01/1.08 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk1|memberP(X2,sk5(X2,X1,X0)))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f195])).
% 4.01/1.08 fof(f443,plain,(
% 4.01/1.08 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk1|leq(X0,sk5(X2,X1,X0)))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f196])).
% 4.01/1.08 fof(f444,plain,(
% 4.01/1.08 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk1|~leq(sk5(X2,X1,X0),X0))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f197])).
% 4.01/1.08 fof(f445,plain,(
% 4.01/1.08 nil=sk3|ssItem(sk6)),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f198])).
% 4.01/1.08 fof(f446,plain,(
% 4.01/1.08 nil=sk3|ssList(sk7)),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f199])).
% 4.01/1.08 fof(f447,plain,(
% 4.01/1.08 nil=sk3|ssList(sk8)),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f200])).
% 4.01/1.08 fof(f448,plain,(
% 4.01/1.08 nil=sk3|app(app(sk7,cons(sk6,nil)),sk8)=sk3),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f201])).
% 4.01/1.08 fof(f449,plain,(
% 4.01/1.08 ![X0]: (nil=sk3|~ssItem(X0)|leq(X0,sk6)|~memberP(sk7,X0)|~memberP(sk8,X0)|~leq(sk6,X0))),
% 4.01/1.08 inference(cnf_transformation,[status(thm)],[f202])).
% 4.01/1.08 fof(f457,definition,(
% 4.01/1.08 sQ2_spl <=> (nil=sk3)),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f458,plain,(
% 4.01/1.08 nil=sk3|~sQ2_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f457])).
% 4.01/1.08 fof(f460,definition,(
% 4.01/1.08 sQ3_spl <=> (ssItem(sk6))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f463,plain,(
% 4.01/1.08 sQ2_spl|sQ3_spl),
% 4.01/1.08 inference(split_clause,[status(thm)],[f445,f457,f460])).
% 4.01/1.08 fof(f464,definition,(
% 4.01/1.08 sQ4_spl <=> (ssList(sk7))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f467,plain,(
% 4.01/1.08 sQ2_spl|sQ4_spl),
% 4.01/1.08 inference(split_clause,[status(thm)],[f446,f457,f464])).
% 4.01/1.08 fof(f468,definition,(
% 4.01/1.08 sQ5_spl <=> (ssList(sk8))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f471,plain,(
% 4.01/1.08 sQ2_spl|sQ5_spl),
% 4.01/1.08 inference(split_clause,[status(thm)],[f447,f457,f468])).
% 4.01/1.08 fof(f472,definition,(
% 4.01/1.08 sQ6_spl <=> (app(app(sk7,cons(sk6,nil)),sk8)=sk3)),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f473,plain,(
% 4.01/1.08 app(app(sk7,cons(sk6,nil)),sk8)=sk3|~sQ6_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f472])).
% 4.01/1.08 fof(f475,plain,(
% 4.01/1.08 sQ2_spl|sQ6_spl),
% 4.01/1.08 inference(split_clause,[status(thm)],[f448,f457,f472])).
% 4.01/1.08 fof(f476,definition,(
% 4.01/1.08 ![X0]: (sQ7_spl <=> (~ssItem(X0)|leq(X0,sk6)|~memberP(sk7,X0)|~memberP(sk8,X0)|~leq(sk6,X0)))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f477,plain,(
% 4.01/1.08 ![X0]: (~ssItem(X0)|leq(X0,sk6)|~memberP(sk7,X0)|~memberP(sk8,X0)|~leq(sk6,X0)|~sQ7_spl)),
% 4.01/1.08 inference(component_clause,[status(thm)],[f476])).
% 4.01/1.08 fof(f479,plain,(
% 4.01/1.08 sQ2_spl|sQ7_spl),
% 4.01/1.08 inference(split_clause,[status(thm)],[f449,f457,f476])).
% 4.01/1.08 fof(f492,plain,(
% 4.01/1.08 sk1=nil|~sQ2_spl),
% 4.01/1.08 inference(backward_demodulation,[status(thm)],[f458,f438])).
% 4.01/1.08 fof(f493,plain,(
% 4.01/1.08 $false|~sQ2_spl),
% 4.01/1.08 inference(forward_subsumption_resolution,[status(thm)],[f492,f439])).
% 4.01/1.08 fof(f494,plain,(
% 4.01/1.08 ~sQ2_spl),
% 4.01/1.08 inference(contradiction_clause,[status(thm)],[f493])).
% 4.01/1.08 fof(f512,plain,(
% 4.01/1.08 leq(skac3,skac3)),
% 4.01/1.08 inference(resolution,[status(thm)],[f211,f264])).
% 4.01/1.08 fof(f513,plain,(
% 4.01/1.08 leq(skac2,skac2)),
% 4.01/1.08 inference(resolution,[status(thm)],[f212,f264])).
% 4.01/1.08 fof(f681,definition,(
% 4.01/1.08 sQ8_spl <=> (ssList(nil))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f683,plain,(
% 4.01/1.08 ~ssList(nil)|sQ8_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f681])).
% 4.01/1.08 fof(f688,definition,(
% 4.01/1.08 sQ10_spl <=> (sk1=nil)),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f689,plain,(
% 4.01/1.08 sk1=nil|~sQ10_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f688])).
% 4.01/1.08 fof(f691,definition,(
% 4.01/1.08 sQ11_spl <=> (ssList(sk1))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f693,plain,(
% 4.01/1.08 ~ssList(sk1)|sQ11_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f691])).
% 4.01/1.08 fof(f699,definition,(
% 4.01/1.08 sQ13_spl <=> (ssList(sk2))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f701,plain,(
% 4.01/1.08 ~ssList(sk2)|sQ13_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f699])).
% 4.01/1.08 fof(f715,plain,(
% 4.01/1.08 $false|sQ8_spl),
% 4.01/1.08 inference(forward_subsumption_resolution,[status(thm)],[f683,f210])).
% 4.01/1.08 fof(f716,plain,(
% 4.01/1.08 sQ8_spl),
% 4.01/1.08 inference(contradiction_clause,[status(thm)],[f715])).
% 4.01/1.08 fof(f904,plain,(
% 4.01/1.08 segmentP(sk1,sk1)),
% 4.01/1.08 inference(resolution,[status(thm)],[f259,f433])).
% 4.01/1.08 fof(f1123,definition,(
% 4.01/1.08 sQ16_spl <=> (leq(skac2,skac2))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f1125,plain,(
% 4.01/1.08 ~leq(skac2,skac2)|sQ16_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f1123])).
% 4.01/1.08 fof(f1126,definition,(
% 4.01/1.08 sQ17_spl <=> (ssItem(skac2))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f1128,plain,(
% 4.01/1.08 ~ssItem(skac2)|sQ17_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f1126])).
% 4.01/1.08 fof(f1133,definition,(
% 4.01/1.08 sQ19_spl <=> (leq(skac3,skac3))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f1135,plain,(
% 4.01/1.08 ~leq(skac3,skac3)|sQ19_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f1133])).
% 4.01/1.08 fof(f1136,definition,(
% 4.01/1.08 sQ20_spl <=> (ssItem(skac3))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f1138,plain,(
% 4.01/1.08 ~ssItem(skac3)|sQ20_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f1136])).
% 4.01/1.08 fof(f1152,plain,(
% 4.01/1.08 $false|sQ20_spl),
% 4.01/1.08 inference(forward_subsumption_resolution,[status(thm)],[f1138,f211])).
% 4.01/1.08 fof(f1153,plain,(
% 4.01/1.08 sQ20_spl),
% 4.01/1.08 inference(contradiction_clause,[status(thm)],[f1152])).
% 4.01/1.08 fof(f1154,plain,(
% 4.01/1.08 $false|sQ19_spl),
% 4.01/1.08 inference(forward_subsumption_resolution,[status(thm)],[f1135,f512])).
% 4.01/1.08 fof(f1155,plain,(
% 4.01/1.08 sQ19_spl),
% 4.01/1.08 inference(contradiction_clause,[status(thm)],[f1154])).
% 4.01/1.08 fof(f1478,plain,(
% 4.01/1.08 app(app(sk7,cons(sk6,nil)),sk8)=sk1|~sQ6_spl),
% 4.01/1.08 inference(forward_demodulation,[status(thm)],[f438,f473])).
% 4.01/1.08 fof(f1479,plain,(
% 4.01/1.08 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|~leq(sk5(sk8,sk7,sk6),sk6)|~sQ6_spl),
% 4.01/1.08 inference(resolution,[status(thm)],[f1478,f444])).
% 4.01/1.08 fof(f1480,plain,(
% 4.01/1.08 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|leq(sk6,sk5(sk8,sk7,sk6))|~sQ6_spl),
% 4.01/1.08 inference(resolution,[status(thm)],[f1478,f443])).
% 4.01/1.08 fof(f1481,plain,(
% 4.01/1.08 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|memberP(sk8,sk5(sk8,sk7,sk6))|~sQ6_spl),
% 4.01/1.08 inference(resolution,[status(thm)],[f1478,f442])).
% 4.01/1.08 fof(f1482,plain,(
% 4.01/1.08 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|memberP(sk7,sk5(sk8,sk7,sk6))|~sQ6_spl),
% 4.01/1.08 inference(resolution,[status(thm)],[f1478,f441])).
% 4.01/1.08 fof(f1483,plain,(
% 4.01/1.08 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|ssItem(sk5(sk8,sk7,sk6))|~sQ6_spl),
% 4.01/1.08 inference(resolution,[status(thm)],[f1478,f440])).
% 4.01/1.08 fof(f1491,definition,(
% 4.01/1.08 sQ24_spl <=> (leq(sk5(sk8,sk7,sk6),sk6))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f1494,plain,(
% 4.01/1.08 ~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ24_spl|~sQ6_spl),
% 4.01/1.08 inference(split_clause,[status(thm)],[f1479,f460,f464,f468,f1491,f472])).
% 4.01/1.08 fof(f1495,definition,(
% 4.01/1.08 sQ25_spl <=> (leq(sk6,sk5(sk8,sk7,sk6)))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f1496,plain,(
% 4.01/1.08 leq(sk6,sk5(sk8,sk7,sk6))|~sQ25_spl),
% 4.01/1.08 inference(component_clause,[status(thm)],[f1495])).
% 4.01/1.08 fof(f1498,plain,(
% 4.01/1.08 ~sQ3_spl|~sQ4_spl|~sQ5_spl|sQ25_spl|~sQ6_spl),
% 4.01/1.08 inference(split_clause,[status(thm)],[f1480,f460,f464,f468,f1495,f472])).
% 4.01/1.08 fof(f1499,definition,(
% 4.01/1.08 sQ26_spl <=> (memberP(sk8,sk5(sk8,sk7,sk6)))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 4.01/1.08 fof(f1502,plain,(
% 4.01/1.08 ~sQ3_spl|~sQ4_spl|~sQ5_spl|sQ26_spl|~sQ6_spl),
% 4.01/1.08 inference(split_clause,[status(thm)],[f1481,f460,f464,f468,f1499,f472])).
% 4.01/1.08 fof(f1503,definition,(
% 4.01/1.08 sQ27_spl <=> (memberP(sk7,sk5(sk8,sk7,sk6)))),
% 4.01/1.08 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 4.01/1.09 fof(f1506,plain,(
% 4.01/1.09 ~sQ3_spl|~sQ4_spl|~sQ5_spl|sQ27_spl|~sQ6_spl),
% 4.01/1.09 inference(split_clause,[status(thm)],[f1482,f460,f464,f468,f1503,f472])).
% 4.01/1.09 fof(f1507,definition,(
% 4.01/1.09 sQ28_spl <=> (ssItem(sk5(sk8,sk7,sk6)))),
% 4.01/1.09 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 4.01/1.09 fof(f1510,plain,(
% 4.01/1.09 ~sQ3_spl|~sQ4_spl|~sQ5_spl|sQ28_spl|~sQ6_spl),
% 4.01/1.09 inference(split_clause,[status(thm)],[f1483,f460,f464,f468,f1507,f472])).
% 4.01/1.09 fof(f1743,plain,(
% 4.01/1.09 $false|~sQ10_spl),
% 4.01/1.09 inference(forward_subsumption_resolution,[status(thm)],[f689,f439])).
% 4.01/1.09 fof(f1744,plain,(
% 4.01/1.09 ~sQ10_spl),
% 4.01/1.09 inference(contradiction_clause,[status(thm)],[f1743])).
% 4.01/1.09 fof(f2313,plain,(
% 4.01/1.09 $false|sQ11_spl),
% 4.01/1.09 inference(forward_subsumption_resolution,[status(thm)],[f693,f433])).
% 4.01/1.09 fof(f2314,plain,(
% 4.01/1.09 sQ11_spl),
% 4.01/1.09 inference(contradiction_clause,[status(thm)],[f2313])).
% 4.01/1.09 fof(f2315,plain,(
% 4.01/1.09 $false|sQ13_spl),
% 4.01/1.09 inference(forward_subsumption_resolution,[status(thm)],[f701,f434])).
% 4.01/1.09 fof(f2316,plain,(
% 4.01/1.09 sQ13_spl),
% 4.01/1.09 inference(contradiction_clause,[status(thm)],[f2315])).
% 4.01/1.09 fof(f2667,plain,(
% 4.01/1.09 $false|sQ17_spl),
% 4.01/1.09 inference(forward_subsumption_resolution,[status(thm)],[f1128,f212])).
% 4.01/1.09 fof(f2668,plain,(
% 4.01/1.09 sQ17_spl),
% 4.01/1.09 inference(contradiction_clause,[status(thm)],[f2667])).
% 4.01/1.09 fof(f2670,plain,(
% 4.01/1.09 $false|sQ16_spl),
% 4.01/1.09 inference(forward_subsumption_resolution,[status(thm)],[f1125,f513])).
% 4.01/1.09 fof(f2671,plain,(
% 4.01/1.09 sQ16_spl),
% 4.01/1.09 inference(contradiction_clause,[status(thm)],[f2670])).
% 4.01/1.09 fof(f3180,definition,(
% 4.01/1.09 ![X1]: (sQ172_spl <=> (~ssList(X1)|~ssList(X1)))),
% 4.01/1.09 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 4.01/1.09 fof(f3181,plain,(
% 4.01/1.09 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ172_spl)),
% 4.01/1.09 inference(component_clause,[status(thm)],[f3180])).
% 4.01/1.09 fof(f3184,plain,(
% 4.01/1.09 ![X0]: (~ssList(X0)|~sQ172_spl)),
% 4.01/1.09 inference(duplicate_literals_removal,[status(thm)],[f3181])).
% 4.01/1.09 fof(f3185,plain,(
% 4.01/1.09 $false|~sQ172_spl),
% 4.01/1.09 inference(backward_subsumption_resolution,[status(thm)],[f250,f3184])).
% 4.01/1.09 fof(f3216,plain,(
% 4.01/1.09 ~sQ172_spl),
% 4.01/1.09 inference(contradiction_clause,[status(thm)],[f3185])).
% 4.01/1.09 fof(f5764,definition,(
% 4.01/1.09 sQ299_spl <=> (segmentP(sk1,sk1))),
% 4.01/1.09 introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition])).
% 4.01/1.09 fof(f5766,plain,(
% 4.01/1.09 ~segmentP(sk1,sk1)|sQ299_spl),
% 4.01/1.09 inference(component_clause,[status(thm)],[f5764])).
% 4.01/1.09 fof(f5808,plain,(
% 4.01/1.09 $false|sQ299_spl),
% 4.01/1.09 inference(forward_subsumption_resolution,[status(thm)],[f5766,f904])).
% 4.01/1.09 fof(f5809,plain,(
% 4.01/1.09 sQ299_spl),
% 4.01/1.09 inference(contradiction_clause,[status(thm)],[f5808])).
% 4.01/1.09 fof(f14721,plain,(
% 4.01/1.09 ~ssItem(sk5(sk8,sk7,sk6))|leq(sk5(sk8,sk7,sk6),sk6)|~memberP(sk7,sk5(sk8,sk7,sk6))|~memberP(sk8,sk5(sk8,sk7,sk6))|~sQ25_spl|~sQ7_spl),
% 4.01/1.09 inference(resolution,[status(thm)],[f1496,f477])).
% 4.01/1.09 fof(f14726,plain,(
% 4.01/1.09 ~sQ28_spl|sQ24_spl|~sQ27_spl|~sQ26_spl|~sQ25_spl|~sQ7_spl),
% 4.01/1.09 inference(split_clause,[status(thm)],[f14721,f1507,f1491,f1503,f1499,f1495,f476])).
% 4.01/1.09 fof(f14743,plain,(
% 4.01/1.09 $false),
% 4.01/1.09 inference(sat_refutation,[status(thm)],[f463,f467,f471,f475,f479,f494,f716,f1153,f1155,f1494,f1498,f1502,f1506,f1510,f1744,f2314,f2316,f2668,f2671,f3216,f5809,f14726])).
% 4.01/1.09 % SZS output end CNFRefutation for theBenchmark.p
% 2.26/1.13 % Elapsed time: 0.646927 seconds
% 2.26/1.13 % CPU time: 4.579908 seconds
% 2.26/1.13 % Total memory used: 163.949 MB
% 2.26/1.13 % Net memory used: 161.416 MB
%------------------------------------------------------------------------------