%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC153-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 : n011.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:44 PM UTC 2026
% Result : Unsatisfiable 9.43s 22.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC153-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/20.77 % CPULimit : 300
% 0.10/20.77 % WCLimit : 300
% 0.10/20.77 % DateTime : Mon Sep 21 08:01:05 UTC 2026
% 0.10/20.78 % CPUTime :
% 0.51/20.80 % Drodi V4.1.1
% 9.43/22.27 % Refutation found
% 9.43/22.27 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.43/22.27 % SZS output start CNFRefutation for theBenchmark
% 9.43/22.27 fof(f8,axiom,(
% 9.43/22.27 ssList(nil) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f9,axiom,(
% 9.43/22.27 ssItem(skac3) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f10,axiom,(
% 9.43/22.27 ssItem(skac2) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f57,axiom,(
% 9.43/22.27 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f59,axiom,(
% 9.43/22.27 (![U]: (( ~ ssList(U)| rearsegP(U,U) ) ))),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f61,axiom,(
% 9.43/22.27 (![U]: (( ~ ssList(U)| frontsegP(U,U) ) ))),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f62,axiom,(
% 9.43/22.27 (![U]: (( ~ ssItem(U)| leq(U,U) ) ))),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f130,axiom,(
% 9.43/22.27 (![U,V]: (( ~ leq(U,V)| ~ leq(V,U)| ~ ssItem(U)| ~ ssItem(V)| V = U ) ))),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f191,negated_conjecture,(
% 9.43/22.27 sk3 = sk1 ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f192,negated_conjecture,(
% 9.43/22.27 (![A,B,C,D,E]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| ~ ssList(D)| ~ ssList(E)| app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E) != sk3| ~ leq(B,A)| leq(A,B) ) ))),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f193,negated_conjecture,(
% 9.43/22.27 (![A,B,C,D,E,F]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| ~ ssList(D)| ~ ssList(E)| app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E) != sk3| ~ leq(B,A)| ~ ssItem(F)| ~ memberP(D,F)| leq(A,F) ) ))),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f194,negated_conjecture,(
% 9.43/22.27 (![A,B,C,D,E,F]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| ~ ssList(D)| ~ ssList(E)| app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E) != sk3| ~ leq(B,A)| ~ ssItem(F)| ~ memberP(D,F)| leq(F,B) ) ))),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f195,negated_conjecture,(
% 9.43/22.27 ssItem(sk5) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f196,negated_conjecture,(
% 9.43/22.27 ssItem(sk6) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f197,negated_conjecture,(
% 9.43/22.27 ssList(sk7) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f198,negated_conjecture,(
% 9.43/22.27 ssList(sk8) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f199,negated_conjecture,(
% 9.43/22.27 ssList(sk9) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f200,negated_conjecture,(
% 9.43/22.27 app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1 ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f201,negated_conjecture,(
% 9.43/22.27 leq(sk6,sk5) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f202,negated_conjecture,(
% 9.43/22.27 ( ssItem(sk10)| ~ leq(sk5,sk6) ) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f203,negated_conjecture,(
% 9.43/22.27 ( memberP(sk8,sk10)| ~ leq(sk5,sk6) ) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f204,negated_conjecture,(
% 9.43/22.27 ( ~ leq(sk10,sk6)| ~ leq(sk5,sk10)| ~ leq(sk5,sk6) ) ),
% 9.43/22.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.43/22.27 fof(f212,plain,(
% 9.43/22.27 ssList(nil)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f8])).
% 9.43/22.27 fof(f213,plain,(
% 9.43/22.27 ssItem(skac3)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f9])).
% 9.43/22.27 fof(f214,plain,(
% 9.43/22.27 ssItem(skac2)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f10])).
% 9.43/22.27 fof(f261,plain,(
% 9.43/22.27 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f57])).
% 9.43/22.27 fof(f263,plain,(
% 9.43/22.27 ![X0]: (~ssList(X0)|rearsegP(X0,X0))),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f59])).
% 9.43/22.27 fof(f265,plain,(
% 9.43/22.27 ![X0]: (~ssList(X0)|frontsegP(X0,X0))),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f61])).
% 9.43/22.27 fof(f266,plain,(
% 9.43/22.27 ![X0]: (~ssItem(X0)|leq(X0,X0))),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f62])).
% 9.43/22.27 fof(f347,plain,(
% 9.43/22.27 ![X0,X1]: (~leq(X0,X1)|~leq(X1,X0)|~ssItem(X0)|~ssItem(X1)|X1=X0)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f130])).
% 9.43/22.27 fof(f440,plain,(
% 9.43/22.27 sk3=sk1),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f191])).
% 9.43/22.27 fof(f441,plain,(
% 9.43/22.27 ![A,B]: (((![C,D,E]: (((((~ssItem(A)|~ssItem(B))|~ssList(C))|~ssList(D))|~ssList(E))|~app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)=sk3))|~leq(B,A))|leq(A,B))),
% 9.43/22.27 inference(miniscoping,[status(thm)],[f192])).
% 9.43/22.27 fof(f442,plain,(
% 9.43/22.27 ![X0,X1,X2,X3,X4]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sk3|~leq(X1,X0)|leq(X0,X1))),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f441])).
% 9.43/22.27 fof(f443,plain,(
% 9.43/22.27 ![A,F]: ((![D]: (((![B]: ((![C,E]: (((((~ssItem(A)|~ssItem(B))|~ssList(C))|~ssList(D))|~ssList(E))|~app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)=sk3))|~leq(B,A)))|~ssItem(F))|~memberP(D,F)))|leq(A,F))),
% 9.43/22.27 inference(miniscoping,[status(thm)],[f193])).
% 9.43/22.27 fof(f444,plain,(
% 9.43/22.27 ![X0,X1,X2,X3,X4,X5]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sk3|~leq(X1,X0)|~ssItem(X5)|~memberP(X3,X5)|leq(X0,X5))),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f443])).
% 9.43/22.27 fof(f445,plain,(
% 9.43/22.27 ![B,F]: ((![D]: (((![A]: ((![C,E]: (((((~ssItem(A)|~ssItem(B))|~ssList(C))|~ssList(D))|~ssList(E))|~app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)=sk3))|~leq(B,A)))|~ssItem(F))|~memberP(D,F)))|leq(F,B))),
% 9.43/22.27 inference(miniscoping,[status(thm)],[f194])).
% 9.43/22.27 fof(f446,plain,(
% 9.43/22.27 ![X0,X1,X2,X3,X4,X5]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~ssList(X3)|~ssList(X4)|~app(app(app(app(X2,cons(X0,nil)),X3),cons(X1,nil)),X4)=sk3|~leq(X1,X0)|~ssItem(X5)|~memberP(X3,X5)|leq(X5,X1))),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f445])).
% 9.43/22.27 fof(f447,plain,(
% 9.43/22.27 ssItem(sk5)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f195])).
% 9.43/22.27 fof(f448,plain,(
% 9.43/22.27 ssItem(sk6)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f196])).
% 9.43/22.27 fof(f449,plain,(
% 9.43/22.27 ssList(sk7)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f197])).
% 9.43/22.27 fof(f450,plain,(
% 9.43/22.27 ssList(sk8)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f198])).
% 9.43/22.27 fof(f451,plain,(
% 9.43/22.27 ssList(sk9)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f199])).
% 9.43/22.27 fof(f452,plain,(
% 9.43/22.27 app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9)=sk1),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f200])).
% 9.43/22.27 fof(f453,plain,(
% 9.43/22.27 leq(sk6,sk5)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f201])).
% 9.43/22.27 fof(f454,plain,(
% 9.43/22.27 ssItem(sk10)|~leq(sk5,sk6)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f202])).
% 9.43/22.27 fof(f455,plain,(
% 9.43/22.27 memberP(sk8,sk10)|~leq(sk5,sk6)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f203])).
% 9.43/22.27 fof(f456,plain,(
% 9.43/22.27 ~leq(sk10,sk6)|~leq(sk5,sk10)|~leq(sk5,sk6)),
% 9.43/22.27 inference(cnf_transformation,[status(thm)],[f204])).
% 9.43/22.27 fof(f464,definition,(
% 9.43/22.27 sQ2_spl <=> (ssItem(sk10))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f467,definition,(
% 9.43/22.27 sQ3_spl <=> (leq(sk5,sk6))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f470,plain,(
% 9.43/22.27 sQ2_spl|~sQ3_spl),
% 9.43/22.27 inference(split_clause,[status(thm)],[f454,f464,f467])).
% 9.43/22.27 fof(f471,definition,(
% 9.43/22.27 sQ4_spl <=> (memberP(sk8,sk10))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f472,plain,(
% 9.43/22.27 memberP(sk8,sk10)|~sQ4_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f471])).
% 9.43/22.27 fof(f474,plain,(
% 9.43/22.27 sQ4_spl|~sQ3_spl),
% 9.43/22.27 inference(split_clause,[status(thm)],[f455,f471,f467])).
% 9.43/22.27 fof(f475,definition,(
% 9.43/22.27 sQ5_spl <=> (leq(sk10,sk6))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f477,plain,(
% 9.43/22.27 ~leq(sk10,sk6)|sQ5_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f475])).
% 9.43/22.27 fof(f478,definition,(
% 9.43/22.27 sQ6_spl <=> (leq(sk5,sk10))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f481,plain,(
% 9.43/22.27 ~sQ5_spl|~sQ6_spl|~sQ3_spl),
% 9.43/22.27 inference(split_clause,[status(thm)],[f456,f475,f478,f467])).
% 9.43/22.27 fof(f494,plain,(
% 9.43/22.27 leq(sk6,sk6)),
% 9.43/22.27 inference(resolution,[status(thm)],[f266,f448])).
% 9.43/22.27 fof(f495,plain,(
% 9.43/22.27 leq(sk5,sk5)),
% 9.43/22.27 inference(resolution,[status(thm)],[f266,f447])).
% 9.43/22.27 fof(f508,plain,(
% 9.43/22.27 leq(skac3,skac3)),
% 9.43/22.27 inference(resolution,[status(thm)],[f213,f266])).
% 9.43/22.27 fof(f509,plain,(
% 9.43/22.27 leq(skac2,skac2)),
% 9.43/22.27 inference(resolution,[status(thm)],[f214,f266])).
% 9.43/22.27 fof(f841,plain,(
% 9.43/22.27 segmentP(sk8,sk8)),
% 9.43/22.27 inference(resolution,[status(thm)],[f261,f450])).
% 9.43/22.27 fof(f846,plain,(
% 9.43/22.27 app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9)=sk3),
% 9.43/22.27 inference(forward_demodulation,[status(thm)],[f440,f452])).
% 9.43/22.27 fof(f847,plain,(
% 9.43/22.27 ![X0]: (~ssItem(sk5)|~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|~ssList(sk9)|~leq(sk6,sk5)|~ssItem(X0)|~memberP(sk8,X0)|leq(X0,sk6))),
% 9.43/22.27 inference(resolution,[status(thm)],[f846,f446])).
% 9.43/22.27 fof(f848,plain,(
% 9.43/22.27 ![X0]: (~ssItem(sk5)|~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|~ssList(sk9)|~leq(sk6,sk5)|~ssItem(X0)|~memberP(sk8,X0)|leq(sk5,X0))),
% 9.43/22.27 inference(resolution,[status(thm)],[f846,f444])).
% 9.43/22.27 fof(f849,plain,(
% 9.43/22.27 ~ssItem(sk5)|~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|~ssList(sk9)|~leq(sk6,sk5)|leq(sk5,sk6)),
% 9.43/22.27 inference(resolution,[status(thm)],[f846,f442])).
% 9.43/22.27 fof(f856,definition,(
% 9.43/22.27 sQ7_spl <=> (ssItem(sk5))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f858,plain,(
% 9.43/22.27 ~ssItem(sk5)|sQ7_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f856])).
% 9.43/22.27 fof(f859,definition,(
% 9.43/22.27 sQ8_spl <=> (ssItem(sk6))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f861,plain,(
% 9.43/22.27 ~ssItem(sk6)|sQ8_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f859])).
% 9.43/22.27 fof(f862,definition,(
% 9.43/22.27 sQ9_spl <=> (ssList(sk7))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f864,plain,(
% 9.43/22.27 ~ssList(sk7)|sQ9_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f862])).
% 9.43/22.27 fof(f865,definition,(
% 9.43/22.27 sQ10_spl <=> (ssList(sk8))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f867,plain,(
% 9.43/22.27 ~ssList(sk8)|sQ10_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f865])).
% 9.43/22.27 fof(f868,definition,(
% 9.43/22.27 sQ11_spl <=> (ssList(sk9))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f870,plain,(
% 9.43/22.27 ~ssList(sk9)|sQ11_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f868])).
% 9.43/22.27 fof(f871,definition,(
% 9.43/22.27 sQ12_spl <=> (leq(sk6,sk5))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f873,plain,(
% 9.43/22.27 ~leq(sk6,sk5)|sQ12_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f871])).
% 9.43/22.27 fof(f874,definition,(
% 9.43/22.27 ![X0]: (sQ13_spl <=> (~ssItem(X0)|~memberP(sk8,X0)|leq(X0,sk6)))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f875,plain,(
% 9.43/22.27 ![X0]: (~ssItem(X0)|~memberP(sk8,X0)|leq(X0,sk6)|~sQ13_spl)),
% 9.43/22.27 inference(component_clause,[status(thm)],[f874])).
% 9.43/22.27 fof(f877,plain,(
% 9.43/22.27 ~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ13_spl),
% 9.43/22.27 inference(split_clause,[status(thm)],[f847,f856,f859,f862,f865,f868,f871,f874])).
% 9.43/22.27 fof(f878,definition,(
% 9.43/22.27 ![X0]: (sQ14_spl <=> (~ssItem(X0)|~memberP(sk8,X0)|leq(sk5,X0)))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f879,plain,(
% 9.43/22.27 ![X0]: (~ssItem(X0)|~memberP(sk8,X0)|leq(sk5,X0)|~sQ14_spl)),
% 9.43/22.27 inference(component_clause,[status(thm)],[f878])).
% 9.43/22.27 fof(f881,plain,(
% 9.43/22.27 ~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ14_spl),
% 9.43/22.27 inference(split_clause,[status(thm)],[f848,f856,f859,f862,f865,f868,f871,f878])).
% 9.43/22.27 fof(f882,plain,(
% 9.43/22.27 ~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|sQ3_spl),
% 9.43/22.27 inference(split_clause,[status(thm)],[f849,f856,f859,f862,f865,f868,f871,f467])).
% 9.43/22.27 fof(f907,plain,(
% 9.43/22.27 $false|sQ11_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f870,f451])).
% 9.43/22.27 fof(f908,plain,(
% 9.43/22.27 sQ11_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f907])).
% 9.43/22.27 fof(f909,plain,(
% 9.43/22.27 $false|sQ8_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f861,f448])).
% 9.43/22.27 fof(f910,plain,(
% 9.43/22.27 sQ8_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f909])).
% 9.43/22.27 fof(f911,plain,(
% 9.43/22.27 $false|sQ12_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f873,f453])).
% 9.43/22.27 fof(f912,plain,(
% 9.43/22.27 sQ12_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f911])).
% 9.43/22.27 fof(f913,plain,(
% 9.43/22.27 $false|sQ10_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f867,f450])).
% 9.43/22.27 fof(f914,plain,(
% 9.43/22.27 sQ10_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f913])).
% 9.43/22.27 fof(f915,plain,(
% 9.43/22.27 $false|sQ7_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f858,f447])).
% 9.43/22.27 fof(f916,plain,(
% 9.43/22.27 sQ7_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f915])).
% 9.43/22.27 fof(f917,plain,(
% 9.43/22.27 $false|sQ9_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f864,f449])).
% 9.43/22.27 fof(f918,plain,(
% 9.43/22.27 sQ9_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f917])).
% 9.43/22.27 fof(f935,definition,(
% 9.43/22.27 sQ21_spl <=> (ssList(nil))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f937,plain,(
% 9.43/22.27 ~ssList(nil)|sQ21_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f935])).
% 9.43/22.27 fof(f981,plain,(
% 9.43/22.27 $false|sQ21_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f937,f212])).
% 9.43/22.27 fof(f982,plain,(
% 9.43/22.27 sQ21_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f981])).
% 9.43/22.27 fof(f1088,plain,(
% 9.43/22.27 rearsegP(sk8,sk8)),
% 9.43/22.27 inference(resolution,[status(thm)],[f263,f450])).
% 9.43/22.27 fof(f1216,plain,(
% 9.43/22.27 ~leq(sk5,sk6)|~ssItem(sk5)|~ssItem(sk6)|sk6=sk5),
% 9.43/22.27 inference(resolution,[status(thm)],[f347,f453])).
% 9.43/22.27 fof(f1224,definition,(
% 9.43/22.27 sQ34_spl <=> (leq(skac2,skac2))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f1226,plain,(
% 9.43/22.27 ~leq(skac2,skac2)|sQ34_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f1224])).
% 9.43/22.27 fof(f1227,definition,(
% 9.43/22.27 sQ35_spl <=> (ssItem(skac2))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f1229,plain,(
% 9.43/22.27 ~ssItem(skac2)|sQ35_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f1227])).
% 9.43/22.27 fof(f1234,definition,(
% 9.43/22.27 sQ37_spl <=> (leq(skac3,skac3))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f1236,plain,(
% 9.43/22.27 ~leq(skac3,skac3)|sQ37_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f1234])).
% 9.43/22.27 fof(f1237,definition,(
% 9.43/22.27 sQ38_spl <=> (ssItem(skac3))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f1239,plain,(
% 9.43/22.27 ~ssItem(skac3)|sQ38_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f1237])).
% 9.43/22.27 fof(f1244,definition,(
% 9.43/22.27 sQ40_spl <=> (sk5=sk6)),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f1245,plain,(
% 9.43/22.27 sk5=sk6|~sQ40_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f1244])).
% 9.43/22.27 fof(f1248,definition,(
% 9.43/22.27 sQ41_spl <=> (leq(sk5,sk5))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f1250,plain,(
% 9.43/22.27 ~leq(sk5,sk5)|sQ41_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f1248])).
% 9.43/22.27 fof(f1255,definition,(
% 9.43/22.27 sQ43_spl <=> (leq(sk6,sk6))),
% 9.43/22.27 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 9.43/22.27 fof(f1257,plain,(
% 9.43/22.27 ~leq(sk6,sk6)|sQ43_spl),
% 9.43/22.27 inference(component_clause,[status(thm)],[f1255])).
% 9.43/22.27 fof(f1262,plain,(
% 9.43/22.27 ~sQ3_spl|~sQ7_spl|~sQ8_spl|sQ40_spl),
% 9.43/22.27 inference(split_clause,[status(thm)],[f1216,f467,f856,f859,f1244])).
% 9.43/22.27 fof(f1265,plain,(
% 9.43/22.27 $false|sQ43_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f1257,f494])).
% 9.43/22.27 fof(f1266,plain,(
% 9.43/22.27 sQ43_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f1265])).
% 9.43/22.27 fof(f1267,plain,(
% 9.43/22.27 $false|sQ41_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f1250,f495])).
% 9.43/22.27 fof(f1268,plain,(
% 9.43/22.27 sQ41_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f1267])).
% 9.43/22.27 fof(f1269,plain,(
% 9.43/22.27 $false|sQ38_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f1239,f213])).
% 9.43/22.27 fof(f1270,plain,(
% 9.43/22.27 sQ38_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f1269])).
% 9.43/22.27 fof(f1271,plain,(
% 9.43/22.27 $false|sQ37_spl),
% 9.43/22.27 inference(forward_subsumption_resolution,[status(thm)],[f1236,f508])).
% 9.43/22.27 fof(f1272,plain,(
% 9.43/22.27 sQ37_spl),
% 9.43/22.27 inference(contradiction_clause,[status(thm)],[f1271])).
% 9.43/22.27 fof(f1274,plain,(
% 9.43/22.27 ~leq(sk10,sk5)|~sQ40_spl|sQ5_spl),
% 9.43/22.27 inference(backward_demodulation,[status(thm)],[f1245,f477])).
% 9.43/22.27 fof(f1319,plain,(
% 9.43/22.27 frontsegP(sk8,sk8)),
% 9.43/22.27 inference(resolution,[status(thm)],[f265,f450])).
% 10.12/22.30 fof(f2539,definition,(
% 10.12/22.30 ![X1]: (sQ119_spl <=> (~ssList(X1)))),
% 10.12/22.30 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 10.12/22.30 fof(f2540,plain,(
% 10.12/22.30 ![X0]: (~ssList(X0)|~sQ119_spl)),
% 10.12/22.30 inference(component_clause,[status(thm)],[f2539])).
% 10.12/22.30 fof(f2552,plain,(
% 10.12/22.30 $false|~sQ119_spl),
% 10.12/22.30 inference(backward_subsumption_resolution,[status(thm)],[f450,f2540])).
% 10.12/22.30 fof(f2583,plain,(
% 10.12/22.30 ~sQ119_spl),
% 10.12/22.30 inference(contradiction_clause,[status(thm)],[f2552])).
% 10.12/22.30 fof(f2746,plain,(
% 10.12/22.30 $false|sQ35_spl),
% 10.12/22.30 inference(forward_subsumption_resolution,[status(thm)],[f1229,f214])).
% 10.12/22.30 fof(f2747,plain,(
% 10.12/22.30 sQ35_spl),
% 10.12/22.30 inference(contradiction_clause,[status(thm)],[f2746])).
% 10.12/22.30 fof(f2748,plain,(
% 10.12/22.30 $false|sQ34_spl),
% 10.12/22.30 inference(forward_subsumption_resolution,[status(thm)],[f1226,f509])).
% 10.12/22.30 fof(f2749,plain,(
% 10.12/22.30 sQ34_spl),
% 10.12/22.30 inference(contradiction_clause,[status(thm)],[f2748])).
% 10.12/22.30 fof(f5349,definition,(
% 10.12/22.30 sQ209_spl <=> (segmentP(sk8,sk8))),
% 10.12/22.30 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 10.12/22.30 fof(f5351,plain,(
% 10.12/22.30 ~segmentP(sk8,sk8)|sQ209_spl),
% 10.12/22.30 inference(component_clause,[status(thm)],[f5349])).
% 10.12/22.30 fof(f5468,plain,(
% 10.12/22.30 $false|sQ209_spl),
% 10.12/22.30 inference(forward_subsumption_resolution,[status(thm)],[f5351,f841])).
% 10.12/22.30 fof(f5469,plain,(
% 10.12/22.30 sQ209_spl),
% 10.12/22.30 inference(contradiction_clause,[status(thm)],[f5468])).
% 10.12/22.30 fof(f5813,definition,(
% 10.12/22.30 sQ249_spl <=> (rearsegP(sk8,sk8))),
% 10.12/22.30 introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 10.12/22.30 fof(f5815,plain,(
% 10.12/22.30 ~rearsegP(sk8,sk8)|sQ249_spl),
% 10.12/22.30 inference(component_clause,[status(thm)],[f5813])).
% 10.12/22.30 fof(f5893,plain,(
% 10.12/22.30 $false|sQ249_spl),
% 10.12/22.30 inference(forward_subsumption_resolution,[status(thm)],[f5815,f1088])).
% 10.12/22.30 fof(f5894,plain,(
% 10.12/22.30 sQ249_spl),
% 10.12/22.30 inference(contradiction_clause,[status(thm)],[f5893])).
% 10.12/22.30 fof(f6055,definition,(
% 10.12/22.30 sQ289_spl <=> (frontsegP(sk8,sk8))),
% 10.12/22.30 introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition])).
% 10.12/22.30 fof(f6057,plain,(
% 10.12/22.30 ~frontsegP(sk8,sk8)|sQ289_spl),
% 10.12/22.30 inference(component_clause,[status(thm)],[f6055])).
% 10.12/22.30 fof(f6087,plain,(
% 10.12/22.30 $false|sQ289_spl),
% 10.12/22.30 inference(forward_subsumption_resolution,[status(thm)],[f6057,f1319])).
% 10.12/22.30 fof(f6088,plain,(
% 10.12/22.30 sQ289_spl),
% 10.12/22.30 inference(contradiction_clause,[status(thm)],[f6087])).
% 10.12/22.30 fof(f8900,plain,(
% 10.12/22.30 ![X0]: (~ssItem(X0)|~memberP(sk8,X0)|leq(X0,sk5)|~sQ40_spl|~sQ13_spl)),
% 10.12/22.30 inference(forward_demodulation,[status(thm)],[f1245,f875])).
% 10.12/22.30 fof(f8901,plain,(
% 10.12/22.30 ~ssItem(sk10)|leq(sk10,sk5)|~sQ40_spl|~sQ13_spl|~sQ4_spl),
% 10.12/22.30 inference(resolution,[status(thm)],[f8900,f472])).
% 10.12/22.30 fof(f8902,definition,(
% 10.12/22.30 sQ525_spl <=> (leq(sk10,sk5))),
% 10.12/22.30 introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition])).
% 10.12/22.30 fof(f8903,plain,(
% 10.12/22.30 leq(sk10,sk5)|~sQ525_spl),
% 10.12/22.30 inference(component_clause,[status(thm)],[f8902])).
% 10.12/22.30 fof(f8905,plain,(
% 10.12/22.30 ~sQ2_spl|sQ525_spl|~sQ40_spl|~sQ13_spl|~sQ4_spl),
% 10.12/22.30 inference(split_clause,[status(thm)],[f8901,f464,f8902,f1244,f874,f471])).
% 10.12/22.30 fof(f8906,plain,(
% 10.12/22.30 $false|~sQ40_spl|sQ5_spl|~sQ525_spl),
% 10.12/22.30 inference(forward_subsumption_resolution,[status(thm)],[f8903,f1274])).
% 10.12/22.30 fof(f8907,plain,(
% 10.12/22.30 ~sQ40_spl|sQ5_spl|~sQ525_spl),
% 10.12/22.30 inference(contradiction_clause,[status(thm)],[f8906])).
% 10.12/22.30 fof(f9775,plain,(
% 10.12/22.30 ~ssItem(sk10)|leq(sk5,sk10)|~sQ14_spl|~sQ4_spl),
% 10.12/22.30 inference(resolution,[status(thm)],[f879,f472])).
% 10.12/22.30 fof(f9776,plain,(
% 10.12/22.30 ~sQ2_spl|sQ6_spl|~sQ14_spl|~sQ4_spl),
% 10.12/22.30 inference(split_clause,[status(thm)],[f9775,f464,f478,f878,f471])).
% 10.12/22.30 fof(f9777,plain,(
% 10.12/22.30 $false),
% 10.12/22.30 inference(sat_refutation,[status(thm)],[f470,f474,f481,f877,f881,f882,f908,f910,f912,f914,f916,f918,f982,f1262,f1266,f1268,f1270,f1272,f2583,f2747,f2749,f5469,f5894,f6088,f8905,f8907,f9776])).
% 10.12/22.30 % SZS output end CNFRefutation for theBenchmark.p
% 10.12/22.31 % Elapsed time: 1.512573 seconds
% 10.12/22.31 % CPU time: 11.284710 seconds
% 10.12/22.31 % Total memory used: 206.093 MB
% 10.12/22.31 % Net memory used: 201.533 MB
%------------------------------------------------------------------------------