%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC279-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:42:03 PM UTC 2026
% Result : Unsatisfiable 0.21s 5.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC279-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.45 % Computer : n016.cluster.edu
% 0.16/5.45 % Model : x86_64 x86_64
% 0.16/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.45 % Memory : 8046.5625MB
% 0.16/5.45 % OS : Linux 6.8.0-71-generic
% 0.16/5.45 % CPULimit : 300
% 0.16/5.45 % WCLimit : 300
% 0.16/5.45 % DateTime : Mon Sep 21 08:16:28 UTC 2026
% 0.16/5.45 % CPUTime :
% 0.16/5.48 % Drodi V4.1.1
% 0.21/5.70 % Refutation found
% 0.21/5.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.21/5.70 % SZS output start CNFRefutation for theBenchmark
% 0.21/5.70 fof(f8,axiom,(
% 0.21/5.70 ssList(nil) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f9,axiom,(
% 0.21/5.70 ssItem(skac3) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f10,axiom,(
% 0.21/5.70 ssItem(skac2) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f62,axiom,(
% 0.21/5.70 (![U]: (( ~ ssItem(U)| leq(U,U) ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f73,axiom,(
% 0.21/5.70 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f79,axiom,(
% 0.21/5.70 (![U]: (( nil != U| ~ ssList(U)| segmentP(nil,U) ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f81,axiom,(
% 0.21/5.70 (![U]: (( nil != U| ~ ssList(U)| rearsegP(nil,U) ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f83,axiom,(
% 0.21/5.70 (![U]: (( nil != U| ~ ssList(U)| frontsegP(nil,U) ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f86,axiom,(
% 0.21/5.70 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f118,axiom,(
% 0.21/5.70 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = U ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f130,axiom,(
% 0.21/5.70 (![U,V]: (( ~ leq(U,V)| ~ leq(V,U)| ~ ssItem(U)| ~ ssItem(V)| V = U ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f150,axiom,(
% 0.21/5.70 (![U,V,W]: (( app(U,V) != app(U,W)| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| V = W ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f156,axiom,(
% 0.21/5.70 (![U,V,W]: (( ~ leq(U,V)| ~ leq(V,W)| ~ ssItem(W)| ~ ssItem(V)| ~ ssItem(U)| leq(U,W) ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f188,negated_conjecture,(
% 0.21/5.70 ssList(sk3) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f189,negated_conjecture,(
% 0.21/5.70 ssList(sk4) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f191,negated_conjecture,(
% 0.21/5.70 sk1 = sk3 ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f192,negated_conjecture,(
% 0.21/5.70 (![A,B,C,D]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk3| ~ ssItem(D)| leq(A,D)| ~ memberP(C,D) ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f193,negated_conjecture,(
% 0.21/5.70 (![A,B,C,D]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk3| ~ ssItem(D)| leq(D,A)| ~ memberP(B,D) ) ))),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f194,negated_conjecture,(
% 0.21/5.70 ssItem(sk5) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f195,negated_conjecture,(
% 0.21/5.70 ssList(sk6) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f196,negated_conjecture,(
% 0.21/5.70 ssList(sk7) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f197,negated_conjecture,(
% 0.21/5.70 app(app(sk6,cons(sk5,nil)),sk7) = sk1 ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f198,negated_conjecture,(
% 0.21/5.70 ssItem(sk8) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f199,negated_conjecture,(
% 0.21/5.70 ( memberP(sk6,sk8)| memberP(sk7,sk8) ) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f200,negated_conjecture,(
% 0.21/5.70 ( memberP(sk6,sk8)| ~ leq(sk5,sk8) ) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f201,negated_conjecture,(
% 0.21/5.70 ( ~ leq(sk8,sk5)| memberP(sk7,sk8) ) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f202,negated_conjecture,(
% 0.21/5.70 ( ~ leq(sk8,sk5)| ~ leq(sk5,sk8) ) ),
% 0.21/5.70 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.21/5.70 fof(f210,plain,(
% 0.21/5.70 ssList(nil)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f8])).
% 0.21/5.70 fof(f211,plain,(
% 0.21/5.70 ssItem(skac3)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f9])).
% 0.21/5.70 fof(f212,plain,(
% 0.21/5.70 ssItem(skac2)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f10])).
% 0.21/5.70 fof(f264,plain,(
% 0.21/5.70 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f62])).
% 0.21/5.70 fof(f276,plain,(
% 0.21/5.70 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f73])).
% 0.21/5.70 fof(f282,plain,(
% 0.21/5.70 ![X0]: (~nil=X0|~ssList(X0)|segmentP(nil,X0))),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f79])).
% 0.21/5.70 fof(f284,plain,(
% 0.21/5.70 ![X0]: (~nil=X0|~ssList(X0)|rearsegP(nil,X0))),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f81])).
% 0.21/5.70 fof(f286,plain,(
% 0.21/5.70 ![X0]: (~nil=X0|~ssList(X0)|frontsegP(nil,X0))),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f83])).
% 0.21/5.70 fof(f289,plain,(
% 0.21/5.70 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f86])).
% 0.21/5.70 fof(f329,plain,(
% 0.21/5.70 ![U]: (((![V]: (~app(U,V)=nil|~ssList(V)))|~ssList(U))|nil=U)),
% 0.21/5.70 inference(miniscoping,[status(thm)],[f118])).
% 0.21/5.70 fof(f330,plain,(
% 0.21/5.70 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X0)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f329])).
% 0.21/5.70 fof(f345,plain,(
% 0.21/5.70 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|~ssItem(X0)|~ssItem(X1)|X1=X0)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f130])).
% 0.21/5.70 fof(f372,plain,(
% 0.21/5.70 ![V,W]: (((![U]: ((~app(U,V)=app(U,W)|~ssList(V))|~ssList(U)))|~ssList(W))|V=W)),
% 0.21/5.70 inference(miniscoping,[status(thm)],[f150])).
% 0.21/5.70 fof(f373,plain,(
% 0.21/5.70 ![X0,X1,X2]: (~app(X0,X1)=app(X0,X2)|~ssList(X1)|~ssList(X0)|~ssList(X2)|X1=X2)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f372])).
% 0.21/5.70 fof(f384,plain,(
% 0.21/5.70 ![U,W]: (((![V]: (((~leq(U,V)|~leq(V,W))|~ssItem(W))|~ssItem(V)))|~ssItem(U))|leq(U,W))),
% 0.21/5.70 inference(miniscoping,[status(thm)],[f156])).
% 0.21/5.70 fof(f385,plain,(
% 0.21/5.70 ![X0,X1,X2]: (~leq(X0,X1)|~leq(X1,X2)|~ssItem(X2)|~ssItem(X1)|~ssItem(X0)|leq(X0,X2))),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f384])).
% 0.21/5.70 fof(f435,plain,(
% 0.21/5.70 ssList(sk3)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f188])).
% 0.21/5.70 fof(f436,plain,(
% 0.21/5.70 ssList(sk4)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f189])).
% 0.21/5.70 fof(f438,plain,(
% 0.21/5.70 sk1=sk3),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f191])).
% 0.21/5.70 fof(f439,plain,(
% 0.21/5.70 ![C,D]: ((![A]: (((![B]: (((~ssItem(A)|~ssList(B))|~ssList(C))|~app(app(B,cons(A,nil)),C)=sk3))|~ssItem(D))|leq(A,D)))|~memberP(C,D))),
% 0.21/5.70 inference(miniscoping,[status(thm)],[f192])).
% 0.21/5.70 fof(f440,plain,(
% 0.21/5.70 ![X0,X1,X2,X3]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk3|~ssItem(X3)|leq(X0,X3)|~memberP(X2,X3))),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f439])).
% 0.21/5.70 fof(f441,plain,(
% 0.21/5.70 ![B,D]: ((![A]: (((![C]: (((~ssItem(A)|~ssList(B))|~ssList(C))|~app(app(B,cons(A,nil)),C)=sk3))|~ssItem(D))|leq(D,A)))|~memberP(B,D))),
% 0.21/5.70 inference(miniscoping,[status(thm)],[f193])).
% 0.21/5.70 fof(f442,plain,(
% 0.21/5.70 ![X0,X1,X2,X3]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk3|~ssItem(X3)|leq(X3,X0)|~memberP(X1,X3))),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f441])).
% 0.21/5.70 fof(f443,plain,(
% 0.21/5.70 ssItem(sk5)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f194])).
% 0.21/5.70 fof(f444,plain,(
% 0.21/5.70 ssList(sk6)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f195])).
% 0.21/5.70 fof(f445,plain,(
% 0.21/5.70 ssList(sk7)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f196])).
% 0.21/5.70 fof(f446,plain,(
% 0.21/5.70 app(app(sk6,cons(sk5,nil)),sk7)=sk1),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f197])).
% 0.21/5.70 fof(f447,plain,(
% 0.21/5.70 ssItem(sk8)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f198])).
% 0.21/5.70 fof(f448,plain,(
% 0.21/5.70 memberP(sk6,sk8)|memberP(sk7,sk8)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f199])).
% 0.21/5.70 fof(f449,plain,(
% 0.21/5.70 memberP(sk6,sk8)|~leq(sk5,sk8)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f200])).
% 0.21/5.70 fof(f450,plain,(
% 0.21/5.70 ~leq(sk8,sk5)|memberP(sk7,sk8)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f201])).
% 0.21/5.70 fof(f451,plain,(
% 0.21/5.70 ~leq(sk8,sk5)|~leq(sk5,sk8)),
% 0.21/5.70 inference(cnf_transformation,[status(thm)],[f202])).
% 0.21/5.70 fof(f459,definition,(
% 0.21/5.70 sQ2_spl <=> (memberP(sk6,sk8))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f460,plain,(
% 0.21/5.70 memberP(sk6,sk8)|~sQ2_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f459])).
% 0.21/5.70 fof(f462,definition,(
% 0.21/5.70 sQ3_spl <=> (memberP(sk7,sk8))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f463,plain,(
% 0.21/5.70 memberP(sk7,sk8)|~sQ3_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f462])).
% 0.21/5.70 fof(f465,plain,(
% 0.21/5.70 sQ2_spl|sQ3_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f448,f459,f462])).
% 0.21/5.70 fof(f466,definition,(
% 0.21/5.70 sQ4_spl <=> (leq(sk5,sk8))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f469,plain,(
% 0.21/5.70 sQ2_spl|~sQ4_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f449,f459,f466])).
% 0.21/5.70 fof(f470,definition,(
% 0.21/5.70 sQ5_spl <=> (leq(sk8,sk5))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f473,plain,(
% 0.21/5.70 ~sQ5_spl|sQ3_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f450,f470,f462])).
% 0.21/5.70 fof(f474,plain,(
% 0.21/5.70 ~sQ5_spl|~sQ4_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f451,f470,f466])).
% 0.21/5.70 fof(f475,plain,(
% 0.21/5.70 ~ssList(nil)|segmentP(nil,nil)),
% 0.21/5.70 inference(destructive_equality_resolution,[status(thm)],[f282])).
% 0.21/5.70 fof(f476,plain,(
% 0.21/5.70 ~ssList(nil)|rearsegP(nil,nil)),
% 0.21/5.70 inference(destructive_equality_resolution,[status(thm)],[f284])).
% 0.21/5.70 fof(f477,plain,(
% 0.21/5.70 ~ssList(nil)|frontsegP(nil,nil)),
% 0.21/5.70 inference(destructive_equality_resolution,[status(thm)],[f286])).
% 0.21/5.70 fof(f506,plain,(
% 0.21/5.70 leq(sk8,sk8)),
% 0.21/5.70 inference(resolution,[status(thm)],[f264,f447])).
% 0.21/5.70 fof(f507,plain,(
% 0.21/5.70 leq(sk5,sk5)),
% 0.21/5.70 inference(resolution,[status(thm)],[f264,f443])).
% 0.21/5.70 fof(f510,plain,(
% 0.21/5.70 app(nil,nil)=nil),
% 0.21/5.70 inference(resolution,[status(thm)],[f276,f210])).
% 0.21/5.70 fof(f513,plain,(
% 0.21/5.70 leq(skac3,skac3)),
% 0.21/5.70 inference(resolution,[status(thm)],[f211,f264])).
% 0.21/5.70 fof(f514,plain,(
% 0.21/5.70 leq(skac2,skac2)),
% 0.21/5.70 inference(resolution,[status(thm)],[f212,f264])).
% 0.21/5.70 fof(f522,plain,(
% 0.21/5.70 app(app(sk6,cons(sk5,nil)),sk7)=sk3),
% 0.21/5.70 inference(forward_demodulation,[status(thm)],[f438,f446])).
% 0.21/5.70 fof(f523,plain,(
% 0.21/5.70 ![X0]: (~ssItem(sk5)|~ssList(sk6)|~ssList(sk7)|~ssItem(X0)|leq(sk5,X0)|~memberP(sk7,X0))),
% 0.21/5.70 inference(resolution,[status(thm)],[f440,f522])).
% 0.21/5.70 fof(f525,definition,(
% 0.21/5.70 sQ6_spl <=> (ssItem(sk5))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f527,plain,(
% 0.21/5.70 ~ssItem(sk5)|sQ6_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f525])).
% 0.21/5.70 fof(f528,definition,(
% 0.21/5.70 sQ7_spl <=> (ssList(sk6))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f530,plain,(
% 0.21/5.70 ~ssList(sk6)|sQ7_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f528])).
% 0.21/5.70 fof(f531,definition,(
% 0.21/5.70 sQ8_spl <=> (ssList(sk7))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f533,plain,(
% 0.21/5.70 ~ssList(sk7)|sQ8_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f531])).
% 0.21/5.70 fof(f534,definition,(
% 0.21/5.70 ![X0]: (sQ9_spl <=> (~ssItem(X0)|leq(sk5,X0)|~memberP(sk7,X0)))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f535,plain,(
% 0.21/5.70 ![X0]: (~ssItem(X0)|leq(sk5,X0)|~memberP(sk7,X0)|~sQ9_spl)),
% 0.21/5.70 inference(component_clause,[status(thm)],[f534])).
% 0.21/5.70 fof(f537,plain,(
% 0.21/5.70 ~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ9_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f523,f525,f528,f531,f534])).
% 0.21/5.70 fof(f565,plain,(
% 0.21/5.70 ![X0]: (~ssList(X0)|ssList(cons(sk8,X0)))),
% 0.21/5.70 inference(resolution,[status(thm)],[f289,f447])).
% 0.21/5.70 fof(f639,plain,(
% 0.21/5.70 ![X0]: (~ssItem(sk5)|~ssList(sk6)|~ssList(sk7)|~ssItem(X0)|leq(X0,sk5)|~memberP(sk6,X0))),
% 0.21/5.70 inference(resolution,[status(thm)],[f442,f522])).
% 0.21/5.70 fof(f641,definition,(
% 0.21/5.70 ![X0]: (sQ11_spl <=> (~ssItem(X0)|leq(X0,sk5)|~memberP(sk6,X0)))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f642,plain,(
% 0.21/5.70 ![X0]: (~ssItem(X0)|leq(X0,sk5)|~memberP(sk6,X0)|~sQ11_spl)),
% 0.21/5.70 inference(component_clause,[status(thm)],[f641])).
% 0.21/5.70 fof(f644,plain,(
% 0.21/5.70 ~sQ6_spl|~sQ7_spl|~sQ8_spl|sQ11_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f639,f525,f528,f531,f641])).
% 0.21/5.70 fof(f646,plain,(
% 0.21/5.70 $false|sQ8_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f533,f445])).
% 0.21/5.70 fof(f647,plain,(
% 0.21/5.70 sQ8_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f646])).
% 0.21/5.70 fof(f648,plain,(
% 0.21/5.70 $false|sQ7_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f530,f444])).
% 0.21/5.70 fof(f649,plain,(
% 0.21/5.70 sQ7_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f648])).
% 0.21/5.70 fof(f650,plain,(
% 0.21/5.70 $false|sQ6_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f527,f443])).
% 0.21/5.70 fof(f651,plain,(
% 0.21/5.70 sQ6_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f650])).
% 0.21/5.70 fof(f818,plain,(
% 0.21/5.70 ~ssList(nil)|~ssList(nil)|nil=nil),
% 0.21/5.70 inference(resolution,[status(thm)],[f330,f510])).
% 0.21/5.70 fof(f829,definition,(
% 0.21/5.70 sQ12_spl <=> (ssList(nil))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f831,plain,(
% 0.21/5.70 ~ssList(nil)|sQ12_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f829])).
% 0.21/5.70 fof(f832,definition,(
% 0.21/5.70 sQ13_spl <=> (nil=nil)),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f835,plain,(
% 0.21/5.70 ~sQ12_spl|sQ13_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f818,f829,f832])).
% 0.21/5.70 fof(f839,definition,(
% 0.21/5.70 sQ15_spl <=> (ssList(sk3))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f841,plain,(
% 0.21/5.70 ~ssList(sk3)|sQ15_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f839])).
% 0.21/5.70 fof(f846,definition,(
% 0.21/5.70 sQ17_spl <=> (ssList(sk4))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f848,plain,(
% 0.21/5.70 ~ssList(sk4)|sQ17_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f846])).
% 0.21/5.70 fof(f870,plain,(
% 0.21/5.70 $false|sQ12_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f831,f210])).
% 0.21/5.70 fof(f871,plain,(
% 0.21/5.70 sQ12_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f870])).
% 0.21/5.70 fof(f1174,plain,(
% 0.21/5.70 ~leq(skac2,skac2)|~ssItem(skac2)|~ssItem(skac2)|skac2=skac2),
% 0.21/5.70 inference(resolution,[status(thm)],[f345,f514])).
% 0.21/5.70 fof(f1175,plain,(
% 0.21/5.70 ~leq(skac3,skac3)|~ssItem(skac3)|~ssItem(skac3)|skac3=skac3),
% 0.21/5.70 inference(resolution,[status(thm)],[f345,f513])).
% 0.21/5.70 fof(f1176,plain,(
% 0.21/5.70 ~leq(sk5,sk5)|~ssItem(sk5)|~ssItem(sk5)|sk5=sk5),
% 0.21/5.70 inference(resolution,[status(thm)],[f345,f507])).
% 0.21/5.70 fof(f1177,plain,(
% 0.21/5.70 ~leq(sk8,sk8)|~ssItem(sk8)|~ssItem(sk8)|sk8=sk8),
% 0.21/5.70 inference(resolution,[status(thm)],[f345,f506])).
% 0.21/5.70 fof(f1178,definition,(
% 0.21/5.70 sQ22_spl <=> (leq(skac2,skac2))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1180,plain,(
% 0.21/5.70 ~leq(skac2,skac2)|sQ22_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f1178])).
% 0.21/5.70 fof(f1181,definition,(
% 0.21/5.70 sQ23_spl <=> (ssItem(skac2))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1183,plain,(
% 0.21/5.70 ~ssItem(skac2)|sQ23_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f1181])).
% 0.21/5.70 fof(f1184,definition,(
% 0.21/5.70 sQ24_spl <=> (skac2=skac2)),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1187,plain,(
% 0.21/5.70 ~sQ22_spl|~sQ23_spl|sQ24_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f1174,f1178,f1181,f1184])).
% 0.21/5.70 fof(f1188,definition,(
% 0.21/5.70 sQ25_spl <=> (leq(skac3,skac3))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1190,plain,(
% 0.21/5.70 ~leq(skac3,skac3)|sQ25_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f1188])).
% 0.21/5.70 fof(f1191,definition,(
% 0.21/5.70 sQ26_spl <=> (ssItem(skac3))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1193,plain,(
% 0.21/5.70 ~ssItem(skac3)|sQ26_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f1191])).
% 0.21/5.70 fof(f1194,definition,(
% 0.21/5.70 sQ27_spl <=> (skac3=skac3)),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1197,plain,(
% 0.21/5.70 ~sQ25_spl|~sQ26_spl|sQ27_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f1175,f1188,f1191,f1194])).
% 0.21/5.70 fof(f1198,definition,(
% 0.21/5.70 sQ28_spl <=> (leq(sk5,sk5))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1200,plain,(
% 0.21/5.70 ~leq(sk5,sk5)|sQ28_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f1198])).
% 0.21/5.70 fof(f1201,definition,(
% 0.21/5.70 sQ29_spl <=> (sk5=sk5)),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1204,plain,(
% 0.21/5.70 ~sQ28_spl|~sQ6_spl|sQ29_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f1176,f1198,f525,f1201])).
% 0.21/5.70 fof(f1205,definition,(
% 0.21/5.70 sQ30_spl <=> (leq(sk8,sk8))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1207,plain,(
% 0.21/5.70 ~leq(sk8,sk8)|sQ30_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f1205])).
% 0.21/5.70 fof(f1208,definition,(
% 0.21/5.70 sQ31_spl <=> (ssItem(sk8))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1210,plain,(
% 0.21/5.70 ~ssItem(sk8)|sQ31_spl),
% 0.21/5.70 inference(component_clause,[status(thm)],[f1208])).
% 0.21/5.70 fof(f1211,definition,(
% 0.21/5.70 sQ32_spl <=> (sk8=sk8)),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f1214,plain,(
% 0.21/5.70 ~sQ30_spl|~sQ31_spl|sQ32_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f1177,f1205,f1208,f1211])).
% 0.21/5.70 fof(f1215,plain,(
% 0.21/5.70 $false|sQ28_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f1200,f507])).
% 0.21/5.70 fof(f1216,plain,(
% 0.21/5.70 sQ28_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f1215])).
% 0.21/5.70 fof(f1217,plain,(
% 0.21/5.70 $false|sQ31_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f1210,f447])).
% 0.21/5.70 fof(f1218,plain,(
% 0.21/5.70 sQ31_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f1217])).
% 0.21/5.70 fof(f1219,plain,(
% 0.21/5.70 $false|sQ30_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f1207,f506])).
% 0.21/5.70 fof(f1220,plain,(
% 0.21/5.70 sQ30_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f1219])).
% 0.21/5.70 fof(f1221,plain,(
% 0.21/5.70 $false|sQ26_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f1193,f211])).
% 0.21/5.70 fof(f1222,plain,(
% 0.21/5.70 sQ26_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f1221])).
% 0.21/5.70 fof(f1223,plain,(
% 0.21/5.70 $false|sQ25_spl),
% 0.21/5.70 inference(forward_subsumption_resolution,[status(thm)],[f1190,f513])).
% 0.21/5.70 fof(f1224,plain,(
% 0.21/5.70 sQ25_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f1223])).
% 0.21/5.70 fof(f1552,plain,(
% 0.21/5.70 ssList(cons(sk8,sk7))),
% 0.21/5.70 inference(resolution,[status(thm)],[f565,f445])).
% 0.21/5.70 fof(f2828,plain,(
% 0.21/5.70 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(X0)|X0=X0)),
% 0.21/5.70 inference(equality_resolution,[status(thm)],[f373])).
% 0.21/5.70 fof(f2829,definition,(
% 0.21/5.70 ![X0]: (sQ137_spl <=> (~ssList(X0)|~ssList(X0)|X0=X0))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f2832,definition,(
% 0.21/5.70 ![X1]: (sQ138_spl <=> (~ssList(X1)))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f2833,plain,(
% 0.21/5.70 ![X0]: (~ssList(X0)|~sQ138_spl)),
% 0.21/5.70 inference(component_clause,[status(thm)],[f2832])).
% 0.21/5.70 fof(f2835,plain,(
% 0.21/5.70 sQ137_spl|sQ138_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f2828,f2829,f2832])).
% 0.21/5.70 fof(f2838,plain,(
% 0.21/5.70 $false|~sQ138_spl),
% 0.21/5.70 inference(backward_subsumption_resolution,[status(thm)],[f1552,f2833])).
% 0.21/5.70 fof(f2872,plain,(
% 0.21/5.70 ~sQ138_spl),
% 0.21/5.70 inference(contradiction_clause,[status(thm)],[f2838])).
% 0.21/5.70 fof(f2960,plain,(
% 0.21/5.70 ![X0]: (~leq(X0,skac2)|~ssItem(skac2)|~ssItem(skac2)|~ssItem(X0)|leq(X0,skac2))),
% 0.21/5.70 inference(resolution,[status(thm)],[f385,f514])).
% 0.21/5.70 fof(f2961,plain,(
% 0.21/5.70 ![X0]: (~leq(X0,skac3)|~ssItem(skac3)|~ssItem(skac3)|~ssItem(X0)|leq(X0,skac3))),
% 0.21/5.70 inference(resolution,[status(thm)],[f385,f513])).
% 0.21/5.70 fof(f2962,plain,(
% 0.21/5.70 ![X0]: (~leq(X0,sk5)|~ssItem(sk5)|~ssItem(sk5)|~ssItem(X0)|leq(X0,sk5))),
% 0.21/5.70 inference(resolution,[status(thm)],[f385,f507])).
% 0.21/5.70 fof(f2963,plain,(
% 0.21/5.70 ![X0]: (~leq(X0,sk8)|~ssItem(sk8)|~ssItem(sk8)|~ssItem(X0)|leq(X0,sk8))),
% 0.21/5.70 inference(resolution,[status(thm)],[f385,f506])).
% 0.21/5.70 fof(f2969,definition,(
% 0.21/5.70 ![X0]: (sQ140_spl <=> (~leq(X0,skac2)|~ssItem(X0)|leq(X0,skac2)))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f2972,plain,(
% 0.21/5.70 sQ140_spl|~sQ23_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f2960,f2969,f1181])).
% 0.21/5.70 fof(f2973,definition,(
% 0.21/5.70 ![X0]: (sQ141_spl <=> (~leq(X0,skac3)|~ssItem(X0)|leq(X0,skac3)))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f2976,plain,(
% 0.21/5.70 sQ141_spl|~sQ26_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f2961,f2973,f1191])).
% 0.21/5.70 fof(f2977,definition,(
% 0.21/5.70 ![X0]: (sQ142_spl <=> (~leq(X0,sk5)|~ssItem(X0)|leq(X0,sk5)))),
% 0.21/5.70 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 0.21/5.70 fof(f2980,plain,(
% 0.21/5.70 sQ142_spl|~sQ6_spl),
% 0.21/5.70 inference(split_clause,[status(thm)],[f2962,f2977,f525])).
% 0.21/5.70 fof(f2981,definition,(
% 0.21/5.70 ![X0]: (sQ143_spl <=> (~leq(X0,sk8)|~ssItem(X0)|leq(X0,sk8)))),
% 0.21/5.74 introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition])).
% 0.21/5.74 fof(f2984,plain,(
% 0.21/5.74 sQ143_spl|~sQ31_spl),
% 0.21/5.74 inference(split_clause,[status(thm)],[f2963,f2981,f1208])).
% 0.21/5.74 fof(f2996,plain,(
% 0.21/5.74 $false|sQ23_spl),
% 0.21/5.74 inference(forward_subsumption_resolution,[status(thm)],[f1183,f212])).
% 0.21/5.74 fof(f2997,plain,(
% 0.21/5.74 sQ23_spl),
% 0.21/5.74 inference(contradiction_clause,[status(thm)],[f2996])).
% 0.21/5.74 fof(f2998,plain,(
% 0.21/5.74 $false|sQ22_spl),
% 0.21/5.74 inference(forward_subsumption_resolution,[status(thm)],[f1180,f514])).
% 0.21/5.74 fof(f2999,plain,(
% 0.21/5.74 sQ22_spl),
% 0.21/5.74 inference(contradiction_clause,[status(thm)],[f2998])).
% 0.21/5.74 fof(f3116,definition,(
% 0.21/5.74 sQ146_spl <=> (segmentP(nil,nil))),
% 0.21/5.74 introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition])).
% 0.21/5.74 fof(f3119,plain,(
% 0.21/5.74 ~sQ12_spl|sQ146_spl),
% 0.21/5.74 inference(split_clause,[status(thm)],[f475,f829,f3116])).
% 0.21/5.74 fof(f3128,definition,(
% 0.21/5.74 sQ148_spl <=> (rearsegP(nil,nil))),
% 0.21/5.74 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 0.21/5.74 fof(f3131,plain,(
% 0.21/5.74 ~sQ12_spl|sQ148_spl),
% 0.21/5.74 inference(split_clause,[status(thm)],[f476,f829,f3128])).
% 0.21/5.74 fof(f3210,definition,(
% 0.21/5.74 sQ149_spl <=> (frontsegP(nil,nil))),
% 0.21/5.74 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 0.21/5.74 fof(f3213,plain,(
% 0.21/5.74 ~sQ12_spl|sQ149_spl),
% 0.21/5.74 inference(split_clause,[status(thm)],[f477,f829,f3210])).
% 0.21/5.74 fof(f3409,plain,(
% 0.21/5.74 $false|sQ15_spl),
% 0.21/5.74 inference(forward_subsumption_resolution,[status(thm)],[f841,f435])).
% 0.21/5.74 fof(f3410,plain,(
% 0.21/5.74 sQ15_spl),
% 0.21/5.74 inference(contradiction_clause,[status(thm)],[f3409])).
% 0.21/5.74 fof(f3714,plain,(
% 0.21/5.74 ~ssItem(sk8)|leq(sk5,sk8)|~sQ9_spl|~sQ3_spl),
% 0.21/5.74 inference(resolution,[status(thm)],[f535,f463])).
% 0.21/5.74 fof(f3715,plain,(
% 0.21/5.74 ~sQ31_spl|sQ4_spl|~sQ9_spl|~sQ3_spl),
% 0.21/5.74 inference(split_clause,[status(thm)],[f3714,f1208,f466,f534,f462])).
% 0.21/5.74 fof(f3775,plain,(
% 0.21/5.74 $false|sQ17_spl),
% 0.21/5.74 inference(forward_subsumption_resolution,[status(thm)],[f848,f436])).
% 0.21/5.74 fof(f3776,plain,(
% 0.21/5.74 sQ17_spl),
% 0.21/5.74 inference(contradiction_clause,[status(thm)],[f3775])).
% 0.21/5.74 fof(f4184,plain,(
% 0.21/5.74 ~ssItem(sk8)|leq(sk8,sk5)|~sQ11_spl|~sQ2_spl),
% 0.21/5.74 inference(resolution,[status(thm)],[f642,f460])).
% 0.21/5.74 fof(f4185,plain,(
% 0.21/5.74 ~sQ31_spl|sQ5_spl|~sQ11_spl|~sQ2_spl),
% 0.21/5.74 inference(split_clause,[status(thm)],[f4184,f1208,f470,f641,f459])).
% 0.21/5.74 fof(f4186,plain,(
% 0.21/5.74 $false),
% 0.21/5.74 inference(sat_refutation,[status(thm)],[f465,f469,f473,f474,f537,f644,f647,f649,f651,f835,f871,f1187,f1197,f1204,f1214,f1216,f1218,f1220,f1222,f1224,f2835,f2872,f2972,f2976,f2980,f2984,f2997,f2999,f3119,f3131,f3213,f3410,f3715,f3776,f4185])).
% 0.21/5.74 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/5.76 % Elapsed time: 0.292010 seconds
% 0.21/5.76 % CPU time: 1.811270 seconds
% 0.21/5.76 % Total memory used: 135.561 MB
% 0.21/5.76 % Net memory used: 134.457 MB
%------------------------------------------------------------------------------