%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC022-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:21 PM UTC 2026
% Result : Unsatisfiable 58.93s 7.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC022-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 07:49:56 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 58.93/7.87 % Refutation found
% 58.93/7.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 58.93/7.87 % SZS output start CNFRefutation for theBenchmark
% 58.93/7.87 fof(f8,axiom,(
% 58.93/7.87 ssList(nil) ),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f50,axiom,(
% 58.93/7.87 (![U,V]: (ssList(skaf46(U,V)) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f51,axiom,(
% 58.93/7.87 (![U,V]: (ssList(skaf45(U,V)) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f60,axiom,(
% 58.93/7.87 (![U]: (( ~ ssList(U)| frontsegP(U,nil) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f73,axiom,(
% 58.93/7.87 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f74,axiom,(
% 58.93/7.87 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f75,axiom,(
% 58.93/7.87 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f76,axiom,(
% 58.93/7.87 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f85,axiom,(
% 58.93/7.87 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f86,axiom,(
% 58.93/7.87 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f97,axiom,(
% 58.93/7.87 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| hd(cons(U,V)) = U ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f99,axiom,(
% 58.93/7.87 (![U,V]: (( cons(U,V) != V| ~ ssItem(U)| ~ ssList(V) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f100,axiom,(
% 58.93/7.87 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f104,axiom,(
% 58.93/7.87 (![U]: (( ~ ssList(U)| cons(hd(U),tl(U)) = U| nil = U ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f137,axiom,(
% 58.93/7.87 (![U,V,W]: (( ~ frontsegP(U,V)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| frontsegP(app(U,W),V) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f144,axiom,(
% 58.93/7.87 (![U,V,W]: (( app(U,V) != W| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| frontsegP(W,U) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f178,axiom,(
% 58.93/7.87 (![U,V,W,X]: (( ~ frontsegP(U,V)| W != X| ~ ssList(V)| ~ ssList(U)| ~ ssItem(X)| ~ ssItem(W)| frontsegP(cons(W,U),cons(X,V)) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f186,negated_conjecture,(
% 58.93/7.87 ssList(sk1) ),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f187,negated_conjecture,(
% 58.93/7.87 ssList(sk2) ),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f190,negated_conjecture,(
% 58.93/7.87 sk2 = sk4 ),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f191,negated_conjecture,(
% 58.93/7.87 sk1 = sk3 ),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f192,negated_conjecture,(
% 58.93/7.87 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f196,negated_conjecture,(
% 58.93/7.87 (![A]: (( ~ ssList(A)| ~ neq(A,nil)| ~ frontsegP(sk2,A)| ~ frontsegP(sk1,A)| ~ neq(sk4,nil) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f197,negated_conjecture,(
% 58.93/7.87 (![A,B]: (( ~ ssList(A)| sk3 = A| ~ ssItem(B)| cons(B,nil) != A| hd(sk4) != B| ~ neq(nil,sk4)| ~ neq(sk4,nil) ) ))),
% 58.93/7.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 58.93/7.87 fof(f205,plain,(
% 58.93/7.87 ssList(nil)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f8])).
% 58.93/7.87 fof(f247,plain,(
% 58.93/7.87 ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f50])).
% 58.93/7.87 fof(f248,plain,(
% 58.93/7.87 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f51])).
% 58.93/7.87 fof(f257,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|frontsegP(X0,nil))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f60])).
% 58.93/7.87 fof(f271,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f73])).
% 58.93/7.87 fof(f272,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f74])).
% 58.93/7.87 fof(f273,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f75])).
% 58.93/7.87 fof(f274,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f76])).
% 58.93/7.87 fof(f283,plain,(
% 58.93/7.87 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f85])).
% 58.93/7.87 fof(f284,plain,(
% 58.93/7.87 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f86])).
% 58.93/7.87 fof(f295,plain,(
% 58.93/7.87 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|hd(cons(X0,X1))=X0)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f97])).
% 58.93/7.87 fof(f298,plain,(
% 58.93/7.87 ![V]: ((![U]: (~cons(U,V)=V|~ssItem(U)))|~ssList(V))),
% 58.93/7.87 inference(miniscoping,[status(thm)],[f99])).
% 58.93/7.87 fof(f299,plain,(
% 58.93/7.87 ![X0,X1]: (~cons(X0,X1)=X1|~ssItem(X0)|~ssList(X1))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f298])).
% 58.93/7.87 fof(f300,plain,(
% 58.93/7.87 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f100])).
% 58.93/7.87 fof(f304,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|nil=X0)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f104])).
% 58.93/7.87 fof(f349,plain,(
% 58.93/7.87 ![X0,X1,X2]: (~frontsegP(X0,X1)|~ssList(X2)|~ssList(X1)|~ssList(X0)|frontsegP(app(X0,X2),X1))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f137])).
% 58.93/7.87 fof(f357,plain,(
% 58.93/7.87 ![U,W]: ((((![V]: (~app(U,V)=W|~ssList(V)))|~ssList(U))|~ssList(W))|frontsegP(W,U))),
% 58.93/7.87 inference(miniscoping,[status(thm)],[f144])).
% 58.93/7.87 fof(f358,plain,(
% 58.93/7.87 ![X0,X1,X2]: (~app(X0,X1)=X2|~ssList(X1)|~ssList(X0)|~ssList(X2)|frontsegP(X2,X0))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f357])).
% 58.93/7.87 fof(f413,plain,(
% 58.93/7.87 ![X0,X1,X2,X3]: (~frontsegP(X0,X1)|~X2=X3|~ssList(X1)|~ssList(X0)|~ssItem(X3)|~ssItem(X2)|frontsegP(cons(X2,X0),cons(X3,X1)))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f178])).
% 58.93/7.87 fof(f428,plain,(
% 58.93/7.87 ssList(sk1)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f186])).
% 58.93/7.87 fof(f429,plain,(
% 58.93/7.87 ssList(sk2)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f187])).
% 58.93/7.87 fof(f432,plain,(
% 58.93/7.87 sk2=sk4),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f190])).
% 58.93/7.87 fof(f433,plain,(
% 58.93/7.87 sk1=sk3),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f191])).
% 58.93/7.87 fof(f434,plain,(
% 58.93/7.87 neq(sk2,nil)|neq(sk2,nil)),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f192])).
% 58.93/7.87 fof(f440,plain,(
% 58.93/7.87 (![A]: (((~ssList(A)|~neq(A,nil))|~frontsegP(sk2,A))|~frontsegP(sk1,A)))|~neq(sk4,nil)),
% 58.93/7.87 inference(miniscoping,[status(thm)],[f196])).
% 58.93/7.87 fof(f441,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|~neq(X0,nil)|~frontsegP(sk2,X0)|~frontsegP(sk1,X0)|~neq(sk4,nil))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f440])).
% 58.93/7.87 fof(f442,plain,(
% 58.93/7.87 ((![B]: ((![A]: (((~ssList(A)|sk3=A)|~ssItem(B))|~cons(B,nil)=A))|~hd(sk4)=B))|~neq(nil,sk4))|~neq(sk4,nil)),
% 58.93/7.87 inference(miniscoping,[status(thm)],[f197])).
% 58.93/7.87 fof(f443,plain,(
% 58.93/7.87 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~neq(nil,sk4)|~neq(sk4,nil))),
% 58.93/7.87 inference(cnf_transformation,[status(thm)],[f442])).
% 58.93/7.87 fof(f451,definition,(
% 58.93/7.87 sQ2_spl <=> (neq(sk2,nil))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f452,plain,(
% 58.93/7.87 neq(sk2,nil)|~sQ2_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f451])).
% 58.93/7.87 fof(f454,plain,(
% 58.93/7.87 sQ2_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f434,f451])).
% 58.93/7.87 fof(f455,definition,(
% 58.93/7.87 sQ3_spl <=> (neq(sk4,nil))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f457,plain,(
% 58.93/7.87 ~neq(sk4,nil)|sQ3_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f455])).
% 58.93/7.87 fof(f459,definition,(
% 58.93/7.87 ![X0]: (sQ4_spl <=> (~ssList(X0)|~neq(X0,nil)|~frontsegP(sk2,X0)|~frontsegP(sk1,X0)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f460,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|~neq(X0,nil)|~frontsegP(sk2,X0)|~frontsegP(sk1,X0)|~sQ4_spl)),
% 58.93/7.87 inference(component_clause,[status(thm)],[f459])).
% 58.93/7.87 fof(f463,definition,(
% 58.93/7.87 ![X0,X1]: (sQ5_spl <=> (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f464,plain,(
% 58.93/7.87 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~sQ5_spl)),
% 58.93/7.87 inference(component_clause,[status(thm)],[f463])).
% 58.93/7.87 fof(f466,definition,(
% 58.93/7.87 sQ6_spl <=> (neq(nil,sk4))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f468,plain,(
% 58.93/7.87 ~neq(nil,sk4)|sQ6_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f466])).
% 58.93/7.87 fof(f470,plain,(
% 58.93/7.87 sQ4_spl|~sQ3_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f441,f459,f455])).
% 58.93/7.87 fof(f471,plain,(
% 58.93/7.87 sQ5_spl|~sQ6_spl|~sQ3_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f443,f463,f466,f455])).
% 58.93/7.87 fof(f487,plain,(
% 58.93/7.87 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(app(X1,X0))|frontsegP(app(X1,X0),X1))),
% 58.93/7.87 inference(destructive_equality_resolution,[status(thm)],[f358])).
% 58.93/7.87 fof(f492,plain,(
% 58.93/7.87 ![X0,X1,X3]: (~frontsegP(X0,X1)|~ssList(X1)|~ssList(X0)|~ssItem(X3)|~ssItem(X3)|frontsegP(cons(X3,X0),cons(X3,X1)))),
% 58.93/7.87 inference(destructive_equality_resolution,[status(thm)],[f413])).
% 58.93/7.87 fof(f493,plain,(
% 58.93/7.87 ![X0,X1,X2]: (~frontsegP(X0,X1)|~ssList(X1)|~ssList(X0)|~ssItem(X2)|frontsegP(cons(X2,X0),cons(X2,X1)))),
% 58.93/7.87 inference(duplicate_literals_removal,[status(thm)],[f492])).
% 58.93/7.87 fof(f501,plain,(
% 58.93/7.87 ~neq(sk2,nil)|sQ3_spl),
% 58.93/7.87 inference(backward_demodulation,[status(thm)],[f432,f457])).
% 58.93/7.87 fof(f503,plain,(
% 58.93/7.87 $false|~sQ2_spl|sQ3_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f501,f452])).
% 58.93/7.87 fof(f504,plain,(
% 58.93/7.87 ~sQ2_spl|sQ3_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f503])).
% 58.93/7.87 fof(f505,plain,(
% 58.93/7.87 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk2)=X1|~sQ5_spl)),
% 58.93/7.87 inference(forward_demodulation,[status(thm)],[f432,f464])).
% 58.93/7.87 fof(f506,plain,(
% 58.93/7.87 ~ssList(cons(hd(sk2),nil))|sk3=cons(hd(sk2),nil)|~ssItem(hd(sk2))|~sQ5_spl),
% 58.93/7.87 inference(destructive_equality_resolution,[status(thm)],[f505])).
% 58.93/7.87 fof(f531,plain,(
% 58.93/7.87 app(sk2,nil)=sk2),
% 58.93/7.87 inference(resolution,[status(thm)],[f271,f429])).
% 58.93/7.87 fof(f537,definition,(
% 58.93/7.87 sQ8_spl <=> (ssList(nil))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f539,plain,(
% 58.93/7.87 ~ssList(nil)|sQ8_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f537])).
% 58.93/7.87 fof(f545,definition,(
% 58.93/7.87 sQ10_spl <=> (ssList(sk2))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f547,plain,(
% 58.93/7.87 ~ssList(sk2)|sQ10_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f545])).
% 58.93/7.87 fof(f549,plain,(
% 58.93/7.87 $false|sQ8_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f539,f205])).
% 58.93/7.87 fof(f550,plain,(
% 58.93/7.87 sQ8_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f549])).
% 58.93/7.87 fof(f555,definition,(
% 58.93/7.87 sQ12_spl <=> (ssList(sk1))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f557,plain,(
% 58.93/7.87 ~ssList(sk1)|sQ12_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f555])).
% 58.93/7.87 fof(f568,plain,(
% 58.93/7.87 app(nil,sk1)=sk1),
% 58.93/7.87 inference(resolution,[status(thm)],[f272,f428])).
% 58.93/7.87 fof(f574,plain,(
% 58.93/7.87 $false|sQ10_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f547,f429])).
% 58.93/7.87 fof(f575,plain,(
% 58.93/7.87 sQ10_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f574])).
% 58.93/7.87 fof(f576,plain,(
% 58.93/7.87 ![X0]: (~frontsegP(nil,X0)|~ssList(sk1)|~ssList(X0)|~ssList(nil)|frontsegP(sk1,X0))),
% 58.93/7.87 inference(paramodulation,[status(thm)],[f568,f349])).
% 58.93/7.87 fof(f577,definition,(
% 58.93/7.87 ![X0]: (sQ14_spl <=> (~frontsegP(nil,X0)|~ssList(X0)|frontsegP(sk1,X0)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f578,plain,(
% 58.93/7.87 ![X0]: (~frontsegP(nil,X0)|~ssList(X0)|frontsegP(sk1,X0)|~sQ14_spl)),
% 58.93/7.87 inference(component_clause,[status(thm)],[f577])).
% 58.93/7.87 fof(f580,plain,(
% 58.93/7.87 sQ14_spl|~sQ12_spl|~sQ8_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f576,f577,f555,f537])).
% 58.93/7.87 fof(f581,plain,(
% 58.93/7.87 $false|sQ12_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f557,f428])).
% 58.93/7.87 fof(f582,plain,(
% 58.93/7.87 sQ12_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f581])).
% 58.93/7.87 fof(f583,plain,(
% 58.93/7.87 ~ssList(sk2)|~frontsegP(sk2,sk2)|~frontsegP(sk1,sk2)|~sQ4_spl|~sQ2_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f460,f452])).
% 58.93/7.87 fof(f584,definition,(
% 58.93/7.87 sQ15_spl <=> (frontsegP(sk2,sk2))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f587,definition,(
% 58.93/7.87 sQ16_spl <=> (frontsegP(sk1,sk2))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f589,plain,(
% 58.93/7.87 ~frontsegP(sk1,sk2)|sQ16_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f587])).
% 58.93/7.87 fof(f590,plain,(
% 58.93/7.87 ~sQ10_spl|~sQ15_spl|~sQ16_spl|~sQ4_spl|~sQ2_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f583,f545,f584,f587,f459,f451])).
% 58.93/7.87 fof(f594,definition,(
% 58.93/7.87 sQ17_spl <=> (frontsegP(nil,sk2))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f596,plain,(
% 58.93/7.87 ~frontsegP(nil,sk2)|sQ17_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f594])).
% 58.93/7.87 fof(f603,plain,(
% 58.93/7.87 ~frontsegP(nil,sk2)|~ssList(sk2)|sQ16_spl|~sQ14_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f589,f578])).
% 58.93/7.87 fof(f605,plain,(
% 58.93/7.87 ~sQ17_spl|~sQ10_spl|sQ16_spl|~sQ14_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f603,f594,f545,f587,f577])).
% 58.93/7.87 fof(f697,definition,(
% 58.93/7.87 sQ26_spl <=> (nil=sk2)),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f698,plain,(
% 58.93/7.87 nil=sk2|~sQ26_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f697])).
% 58.93/7.87 fof(f704,definition,(
% 58.93/7.87 sQ28_spl <=> (nil=sk1)),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f705,plain,(
% 58.93/7.87 nil=sk1|~sQ28_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f704])).
% 58.93/7.87 fof(f719,plain,(
% 58.93/7.87 nil=sk3|~sQ28_spl),
% 58.93/7.87 inference(backward_demodulation,[status(thm)],[f705,f433])).
% 58.93/7.87 fof(f724,plain,(
% 58.93/7.87 ~ssList(cons(hd(sk2),nil))|sk3=cons(hd(sk2),nil)|~ssList(sk2)|nil=sk2|~sQ5_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f506,f274])).
% 58.93/7.87 fof(f725,definition,(
% 58.93/7.87 sQ30_spl <=> (ssList(cons(hd(sk2),nil)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f727,plain,(
% 58.93/7.87 ~ssList(cons(hd(sk2),nil))|sQ30_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f725])).
% 58.93/7.87 fof(f728,definition,(
% 58.93/7.87 sQ31_spl <=> (sk3=cons(hd(sk2),nil))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f729,plain,(
% 58.93/7.87 sk3=cons(hd(sk2),nil)|~sQ31_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f728])).
% 58.93/7.87 fof(f731,plain,(
% 58.93/7.87 ~sQ30_spl|sQ31_spl|~sQ10_spl|sQ26_spl|~sQ5_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f724,f725,f728,f545,f697,f463])).
% 58.93/7.87 fof(f732,plain,(
% 58.93/7.87 ~neq(nil,sk2)|sQ6_spl),
% 58.93/7.87 inference(forward_demodulation,[status(thm)],[f432,f468])).
% 58.93/7.87 fof(f737,plain,(
% 58.93/7.87 ~frontsegP(nil,nil)|~sQ26_spl|sQ17_spl),
% 58.93/7.87 inference(backward_demodulation,[status(thm)],[f698,f596])).
% 58.93/7.87 fof(f752,plain,(
% 58.93/7.87 ~ssList(nil)|~sQ26_spl|sQ17_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f737,f257])).
% 58.93/7.87 fof(f755,plain,(
% 58.93/7.87 ~sQ8_spl|~sQ26_spl|sQ17_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f752,f537,f697,f594])).
% 58.93/7.87 fof(f776,plain,(
% 58.93/7.87 ~ssList(sk2)|~ssList(nil)|nil=sk2|sQ6_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f300,f732])).
% 58.93/7.87 fof(f779,plain,(
% 58.93/7.87 ~sQ10_spl|~sQ8_spl|sQ26_spl|sQ6_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f776,f545,f537,f697,f466])).
% 58.93/7.87 fof(f780,definition,(
% 58.93/7.87 sQ33_spl <=> (ssItem(hd(sk2)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f781,plain,(
% 58.93/7.87 ssItem(hd(sk2))|~sQ33_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f780])).
% 58.93/7.87 fof(f782,plain,(
% 58.93/7.87 ~ssItem(hd(sk2))|sQ33_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f780])).
% 58.93/7.87 fof(f804,definition,(
% 58.93/7.87 sQ34_spl <=> (ssList(skaf46(sk2,sk2)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f806,plain,(
% 58.93/7.87 ~ssList(skaf46(sk2,sk2))|sQ34_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f804])).
% 58.93/7.87 fof(f814,definition,(
% 58.93/7.87 sQ36_spl <=> (ssList(skaf46(nil,nil)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f816,plain,(
% 58.93/7.87 ~ssList(skaf46(nil,nil))|sQ36_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f814])).
% 58.93/7.87 fof(f852,definition,(
% 58.93/7.87 sQ40_spl <=> (ssList(skaf45(sk2,sk2)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f854,plain,(
% 58.93/7.87 ~ssList(skaf45(sk2,sk2))|sQ40_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f852])).
% 58.93/7.87 fof(f859,definition,(
% 58.93/7.87 sQ41_spl <=> (ssList(skaf45(nil,nil)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f861,plain,(
% 58.93/7.87 ~ssList(skaf45(nil,nil))|sQ41_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f859])).
% 58.93/7.87 fof(f906,definition,(
% 58.93/7.87 sQ42_spl <=> (ssList(skaf45(sk2,nil)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f908,plain,(
% 58.93/7.87 ~ssList(skaf45(sk2,nil))|sQ42_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f906])).
% 58.93/7.87 fof(f1328,plain,(
% 58.93/7.87 ~ssItem(hd(sk2))|~ssList(nil)|sQ30_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f727,f284])).
% 58.93/7.87 fof(f1329,plain,(
% 58.93/7.87 ~sQ33_spl|~sQ8_spl|sQ30_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f1328,f780,f537,f725])).
% 58.93/7.87 fof(f1330,plain,(
% 58.93/7.87 nil=cons(hd(sk2),nil)|~sQ28_spl|~sQ31_spl),
% 58.93/7.87 inference(forward_demodulation,[status(thm)],[f719,f729])).
% 58.93/7.87 fof(f1499,plain,(
% 58.93/7.87 ![X0,X1]: (~ssList(X0)|~ssList(X1)|frontsegP(app(X1,X0),X1))),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f487,f283])).
% 58.93/7.87 fof(f1505,plain,(
% 58.93/7.87 ~ssList(nil)|~ssList(sk2)|frontsegP(sk2,sk2)),
% 58.93/7.87 inference(paramodulation,[status(thm)],[f531,f1499])).
% 58.93/7.87 fof(f1523,plain,(
% 58.93/7.87 ~sQ8_spl|~sQ10_spl|sQ15_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f1505,f537,f545,f584])).
% 58.93/7.87 fof(f1534,plain,(
% 58.93/7.87 $false|sQ36_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f816,f247])).
% 58.93/7.87 fof(f1535,plain,(
% 58.93/7.87 sQ36_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f1534])).
% 58.93/7.87 fof(f1536,plain,(
% 58.93/7.87 $false|sQ34_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f806,f247])).
% 58.93/7.87 fof(f1537,plain,(
% 58.93/7.87 sQ34_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f1536])).
% 58.93/7.87 fof(f1849,plain,(
% 58.93/7.87 ~ssList(sk2)|nil=sk2|sQ33_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f782,f274])).
% 58.93/7.87 fof(f1850,plain,(
% 58.93/7.87 ~sQ10_spl|sQ26_spl|sQ33_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f1849,f545,f697,f780])).
% 58.93/7.87 fof(f1926,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|hd(cons(hd(sk2),X0))=hd(sk2)|~sQ33_spl)),
% 58.93/7.87 inference(resolution,[status(thm)],[f781,f295])).
% 58.93/7.87 fof(f1928,plain,(
% 58.93/7.87 ![X0]: (~cons(hd(sk2),X0)=X0|~ssList(X0)|~sQ33_spl)),
% 58.93/7.87 inference(resolution,[status(thm)],[f781,f299])).
% 58.93/7.87 fof(f1938,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|~frontsegP(sk2,X0)|~frontsegP(sk1,X0)|~ssList(nil)|~ssList(X0)|X0=nil|~sQ4_spl)),
% 58.93/7.87 inference(resolution,[status(thm)],[f460,f300])).
% 58.93/7.87 fof(f1940,definition,(
% 58.93/7.87 ![X0]: (sQ82_spl <=> (~ssList(X0)|~frontsegP(sk2,X0)|~frontsegP(sk1,X0)|~ssList(X0)|X0=nil))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f1941,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|~frontsegP(sk2,X0)|~frontsegP(sk1,X0)|~ssList(X0)|X0=nil|~sQ82_spl)),
% 58.93/7.87 inference(component_clause,[status(thm)],[f1940])).
% 58.93/7.87 fof(f1943,plain,(
% 58.93/7.87 sQ82_spl|~sQ8_spl|~sQ4_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f1938,f1940,f537,f459])).
% 58.93/7.87 fof(f1944,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|~frontsegP(sk2,X0)|~frontsegP(sk1,X0)|X0=nil|~sQ82_spl)),
% 58.93/7.87 inference(duplicate_literals_removal,[status(thm)],[f1941])).
% 58.93/7.87 fof(f1980,definition,(
% 58.93/7.87 sQ88_spl <=> (frontsegP(sk1,sk1))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f2160,plain,(
% 58.93/7.87 ![X0]: (~frontsegP(X0,nil)|~ssList(nil)|~ssList(X0)|~ssItem(hd(sk2))|frontsegP(cons(hd(sk2),X0),sk3)|~sQ31_spl)),
% 58.93/7.87 inference(paramodulation,[status(thm)],[f729,f493])).
% 58.93/7.87 fof(f2174,definition,(
% 58.93/7.87 ![X0]: (sQ113_spl <=> (~frontsegP(X0,nil)|~ssList(X0)|frontsegP(cons(hd(sk2),X0),sk3)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f2175,plain,(
% 58.93/7.87 ![X0]: (~frontsegP(X0,nil)|~ssList(X0)|frontsegP(cons(hd(sk2),X0),sk3)|~sQ113_spl)),
% 58.93/7.87 inference(component_clause,[status(thm)],[f2174])).
% 58.93/7.87 fof(f2177,plain,(
% 58.93/7.87 sQ113_spl|~sQ8_spl|~sQ33_spl|~sQ31_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f2160,f2174,f537,f780,f728])).
% 58.93/7.87 fof(f2178,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|frontsegP(cons(hd(sk2),X0),sk3)|~sQ113_spl)),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f2175,f257])).
% 58.93/7.87 fof(f2181,plain,(
% 58.93/7.87 sk1=cons(hd(sk2),nil)|~sQ31_spl),
% 58.93/7.87 inference(backward_demodulation,[status(thm)],[f433,f729])).
% 58.93/7.87 fof(f2333,plain,(
% 58.93/7.87 ~cons(hd(sk2),nil)=nil|~sQ33_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f1928,f205])).
% 58.93/7.87 fof(f2334,plain,(
% 58.93/7.87 ~nil=nil|~sQ28_spl|~sQ31_spl|~sQ33_spl),
% 58.93/7.87 inference(forward_demodulation,[status(thm)],[f1330,f2333])).
% 58.93/7.87 fof(f2335,plain,(
% 58.93/7.87 $false|~sQ28_spl|~sQ31_spl|~sQ33_spl),
% 58.93/7.87 inference(trivial_equality_resolution,[status(thm)],[f2334])).
% 58.93/7.87 fof(f2336,plain,(
% 58.93/7.87 ~sQ28_spl|~sQ31_spl|~sQ33_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f2335])).
% 58.93/7.87 fof(f2629,definition,(
% 58.93/7.87 sQ132_spl <=> (ssList(skaf45(sk1,nil)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f2631,plain,(
% 58.93/7.87 ~ssList(skaf45(sk1,nil))|sQ132_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f2629])).
% 58.93/7.87 fof(f2643,definition,(
% 58.93/7.87 sQ134_spl <=> (ssList(skaf45(sk1,sk1)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f2645,plain,(
% 58.93/7.87 ~ssList(skaf45(sk1,sk1))|sQ134_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f2643])).
% 58.93/7.87 fof(f2670,definition,(
% 58.93/7.87 sQ135_spl <=> (ssList(skaf46(sk1,sk1)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f2672,plain,(
% 58.93/7.87 ~ssList(skaf46(sk1,sk1))|sQ135_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f2670])).
% 58.93/7.87 fof(f2689,plain,(
% 58.93/7.87 $false|sQ135_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f2672,f247])).
% 58.93/7.87 fof(f2690,plain,(
% 58.93/7.87 sQ135_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f2689])).
% 58.93/7.87 fof(f2711,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|frontsegP(cons(hd(sk2),X0),sk1)|~sQ113_spl)),
% 58.93/7.87 inference(forward_demodulation,[status(thm)],[f433,f2178])).
% 58.93/7.87 fof(f2714,plain,(
% 58.93/7.87 ~ssList(nil)|frontsegP(sk1,sk1)|~sQ113_spl|~sQ31_spl),
% 58.93/7.87 inference(paramodulation,[status(thm)],[f2181,f2711])).
% 58.93/7.87 fof(f2723,plain,(
% 58.93/7.87 ~sQ8_spl|sQ88_spl|~sQ113_spl|~sQ31_spl),
% 58.93/7.87 inference(split_clause,[status(thm)],[f2714,f537,f1980,f2174,f728])).
% 58.93/7.87 fof(f2784,plain,(
% 58.93/7.87 $false|sQ132_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f2631,f248])).
% 58.93/7.87 fof(f2785,plain,(
% 58.93/7.87 sQ132_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f2784])).
% 58.93/7.87 fof(f2786,plain,(
% 58.93/7.87 $false|sQ42_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f908,f248])).
% 58.93/7.87 fof(f2787,plain,(
% 58.93/7.87 sQ42_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f2786])).
% 58.93/7.87 fof(f2788,plain,(
% 58.93/7.87 $false|sQ134_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f2645,f248])).
% 58.93/7.87 fof(f2789,plain,(
% 58.93/7.87 sQ134_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f2788])).
% 58.93/7.87 fof(f2805,plain,(
% 58.93/7.87 hd(cons(hd(sk2),nil))=hd(sk2)|~sQ33_spl),
% 58.93/7.87 inference(resolution,[status(thm)],[f1926,f205])).
% 58.93/7.87 fof(f2806,plain,(
% 58.93/7.87 hd(sk1)=hd(sk2)|~sQ31_spl|~sQ33_spl),
% 58.93/7.87 inference(forward_demodulation,[status(thm)],[f2181,f2805])).
% 58.93/7.87 fof(f2809,plain,(
% 58.93/7.87 ![X0]: (~ssList(X0)|frontsegP(cons(hd(sk1),X0),sk1)|~sQ31_spl|~sQ33_spl|~sQ113_spl)),
% 58.93/7.87 inference(backward_demodulation,[status(thm)],[f2806,f2711])).
% 58.93/7.87 fof(f11252,plain,(
% 58.93/7.87 $false|sQ40_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f854,f248])).
% 58.93/7.87 fof(f11253,plain,(
% 58.93/7.87 sQ40_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f11252])).
% 58.93/7.87 fof(f11254,plain,(
% 58.93/7.87 $false|sQ41_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f861,f248])).
% 58.93/7.87 fof(f11255,plain,(
% 58.93/7.87 sQ41_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f11254])).
% 58.93/7.87 fof(f16643,definition,(
% 58.93/7.87 sQ392_spl <=> (ssList(skaf46(sk1,nil)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f16645,plain,(
% 58.93/7.87 ~ssList(skaf46(sk1,nil))|sQ392_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f16643])).
% 58.93/7.87 fof(f16683,plain,(
% 58.93/7.87 $false|sQ392_spl),
% 58.93/7.87 inference(forward_subsumption_resolution,[status(thm)],[f16645,f247])).
% 58.93/7.87 fof(f16684,plain,(
% 58.93/7.87 sQ392_spl),
% 58.93/7.87 inference(contradiction_clause,[status(thm)],[f16683])).
% 58.93/7.87 fof(f16719,definition,(
% 58.93/7.87 sQ406_spl <=> (ssList(skaf46(sk2,nil)))),
% 58.93/7.87 introduced(definition,[new_symbols(definition,[sQ406_spl])],[split_symbol_definition])).
% 58.93/7.87 fof(f16721,plain,(
% 58.93/7.87 ~ssList(skaf46(sk2,nil))|sQ406_spl),
% 58.93/7.87 inference(component_clause,[status(thm)],[f16719])).
% 42.80/7.91 fof(f16759,plain,(
% 42.80/7.91 $false|sQ406_spl),
% 42.80/7.91 inference(forward_subsumption_resolution,[status(thm)],[f16721,f247])).
% 42.80/7.91 fof(f16760,plain,(
% 42.80/7.91 sQ406_spl),
% 42.80/7.91 inference(contradiction_clause,[status(thm)],[f16759])).
% 42.80/7.91 fof(f16895,plain,(
% 42.80/7.91 ssList(tl(sk2))|nil=sk2),
% 42.80/7.91 inference(resolution,[status(thm)],[f273,f429])).
% 42.80/7.91 fof(f16916,definition,(
% 42.80/7.91 sQ420_spl <=> (ssList(tl(sk2)))),
% 42.80/7.91 introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition])).
% 42.80/7.91 fof(f16919,plain,(
% 42.80/7.91 sQ420_spl|sQ26_spl),
% 42.80/7.91 inference(split_clause,[status(thm)],[f16895,f16916,f697])).
% 42.80/7.91 fof(f29179,plain,(
% 42.80/7.91 cons(hd(sk2),tl(sk2))=sk2|nil=sk2),
% 42.80/7.91 inference(resolution,[status(thm)],[f304,f429])).
% 42.80/7.91 fof(f29259,definition,(
% 42.80/7.91 sQ713_spl <=> (cons(hd(sk2),tl(sk2))=sk2)),
% 42.80/7.91 introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition])).
% 42.80/7.91 fof(f29260,plain,(
% 42.80/7.91 cons(hd(sk2),tl(sk2))=sk2|~sQ713_spl),
% 42.80/7.91 inference(component_clause,[status(thm)],[f29259])).
% 42.80/7.91 fof(f29262,plain,(
% 42.80/7.91 sQ713_spl|sQ26_spl),
% 42.80/7.91 inference(split_clause,[status(thm)],[f29179,f29259,f697])).
% 42.80/7.91 fof(f29277,plain,(
% 42.80/7.91 cons(hd(sk1),tl(sk2))=sk2|~sQ31_spl|~sQ33_spl|~sQ713_spl),
% 42.80/7.91 inference(forward_demodulation,[status(thm)],[f2806,f29260])).
% 42.80/7.91 fof(f29286,plain,(
% 42.80/7.91 ~ssList(tl(sk2))|frontsegP(sk2,sk1)|~sQ113_spl|~sQ31_spl|~sQ33_spl|~sQ713_spl),
% 42.80/7.91 inference(paramodulation,[status(thm)],[f29277,f2809])).
% 42.80/7.91 fof(f29287,definition,(
% 42.80/7.91 sQ717_spl <=> (frontsegP(sk2,sk1))),
% 42.80/7.91 introduced(definition,[new_symbols(definition,[sQ717_spl])],[split_symbol_definition])).
% 42.80/7.91 fof(f29288,plain,(
% 42.80/7.91 frontsegP(sk2,sk1)|~sQ717_spl),
% 42.80/7.91 inference(component_clause,[status(thm)],[f29287])).
% 42.80/7.91 fof(f29290,plain,(
% 42.80/7.91 ~sQ420_spl|sQ717_spl|~sQ113_spl|~sQ31_spl|~sQ33_spl|~sQ713_spl),
% 42.80/7.91 inference(split_clause,[status(thm)],[f29286,f16916,f29287,f2174,f728,f780,f29259])).
% 42.80/7.91 fof(f29291,plain,(
% 42.80/7.91 ~ssList(sk1)|~frontsegP(sk1,sk1)|sk1=nil|~sQ717_spl|~sQ82_spl),
% 42.80/7.91 inference(resolution,[status(thm)],[f29288,f1944])).
% 42.80/7.91 fof(f29296,plain,(
% 42.80/7.91 ~sQ12_spl|~sQ88_spl|sQ28_spl|~sQ717_spl|~sQ82_spl),
% 42.80/7.91 inference(split_clause,[status(thm)],[f29291,f555,f1980,f704,f29287,f1940])).
% 42.80/7.91 fof(f29313,plain,(
% 42.80/7.91 $false),
% 42.80/7.91 inference(sat_refutation,[status(thm)],[f454,f470,f471,f504,f550,f575,f580,f582,f590,f605,f731,f755,f779,f1329,f1523,f1535,f1537,f1850,f1943,f2177,f2336,f2690,f2723,f2785,f2787,f2789,f11253,f11255,f16684,f16760,f16919,f29262,f29290,f29296])).
% 42.80/7.91 % SZS output end CNFRefutation for theBenchmark.p
% 42.80/7.96 % Elapsed time: 7.587403 seconds
% 42.80/7.96 % CPU time: 59.697818 seconds
% 42.80/7.96 % Total memory used: 738.500 MB
% 42.80/7.96 % Net memory used: 704.367 MB
%------------------------------------------------------------------------------