%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC382-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:42:19 PM UTC 2026
% Result : Unsatisfiable 82.51s 15.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC382-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.10/5.36 % Computer : n019.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Mon Sep 21 08:20:27 UTC 2026
% 0.10/5.36 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 82.51/15.86 % Refutation found
% 82.51/15.86 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 82.51/15.86 % SZS output start CNFRefutation for theBenchmark
% 82.51/15.86 fof(f8,axiom,(
% 82.51/15.86 ssList(nil) ),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f12,axiom,(
% 82.51/15.86 (![U]: (ssItem(skaf83(U)) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f13,axiom,(
% 82.51/15.86 (![U]: (ssList(skaf82(U)) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f25,axiom,(
% 82.51/15.86 (![U]: (ssItem(skaf70(U)) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f26,axiom,(
% 82.51/15.86 (![U]: (ssItem(skaf69(U)) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f44,axiom,(
% 82.51/15.86 (![U]: (ssList(skaf51(U)) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f49,axiom,(
% 82.51/15.86 (![U,V]: (ssList(skaf47(U,V)) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f50,axiom,(
% 82.51/15.86 (![U,V]: (ssList(skaf46(U,V)) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f51,axiom,(
% 82.51/15.86 (![U,V]: (ssList(skaf45(U,V)) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f74,axiom,(
% 82.51/15.86 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f75,axiom,(
% 82.51/15.86 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f76,axiom,(
% 82.51/15.86 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f85,axiom,(
% 82.51/15.86 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f86,axiom,(
% 82.51/15.86 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f97,axiom,(
% 82.51/15.86 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| hd(cons(U,V)) = U ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f98,axiom,(
% 82.51/15.86 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f100,axiom,(
% 82.51/15.86 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f104,axiom,(
% 82.51/15.86 (![U]: (( ~ ssList(U)| cons(hd(U),tl(U)) = U| nil = U ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f109,axiom,(
% 82.51/15.86 (![U]: (( ~ ssList(U)| cons(skaf83(U),skaf82(U)) = U| nil = U ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f115,axiom,(
% 82.51/15.86 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f116,axiom,(
% 82.51/15.86 (![U,V]: (( cons(U,nil) != V| ~ ssItem(U)| ~ ssList(V)| singletonP(V) ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f120,axiom,(
% 82.51/15.86 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| app(cons(U,nil),V) = cons(U,V) ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f173,axiom,(
% 82.51/15.86 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f186,negated_conjecture,(
% 82.51/15.86 ssList(sk1) ),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f187,negated_conjecture,(
% 82.51/15.86 ssList(sk2) ),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f190,negated_conjecture,(
% 82.51/15.86 sk2 = sk4 ),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f191,negated_conjecture,(
% 82.51/15.86 sk1 = sk3 ),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f192,negated_conjecture,(
% 82.51/15.86 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f196,negated_conjecture,(
% 82.51/15.86 (![A,B]: (( ~ ssList(A)| sk3 = A| ~ ssItem(B)| cons(B,nil) != A| hd(sk4) != B| ~ neq(nil,sk4)| ~ neq(sk4,nil) ) ))),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f197,negated_conjecture,(
% 82.51/15.86 ( ~ singletonP(sk1)| ~ segmentP(sk2,sk1)| ~ neq(sk4,nil) ) ),
% 82.51/15.86 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 82.51/15.86 fof(f205,plain,(
% 82.51/15.86 ssList(nil)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f8])).
% 82.51/15.86 fof(f209,plain,(
% 82.51/15.86 ![X0]: (ssItem(skaf83(X0)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f12])).
% 82.51/15.86 fof(f210,plain,(
% 82.51/15.86 ![X0]: (ssList(skaf82(X0)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f13])).
% 82.51/15.86 fof(f222,plain,(
% 82.51/15.86 ![X0]: (ssItem(skaf70(X0)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f25])).
% 82.51/15.86 fof(f223,plain,(
% 82.51/15.86 ![X0]: (ssItem(skaf69(X0)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f26])).
% 82.51/15.86 fof(f241,plain,(
% 82.51/15.86 ![X0]: (ssList(skaf51(X0)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f44])).
% 82.51/15.86 fof(f246,plain,(
% 82.51/15.86 ![X0,X1]: (ssList(skaf47(X0,X1)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f49])).
% 82.51/15.86 fof(f247,plain,(
% 82.51/15.86 ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f50])).
% 82.51/15.86 fof(f248,plain,(
% 82.51/15.86 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f51])).
% 82.51/15.86 fof(f272,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f74])).
% 82.51/15.86 fof(f273,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f75])).
% 82.51/15.86 fof(f274,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f76])).
% 82.51/15.86 fof(f283,plain,(
% 82.51/15.86 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f85])).
% 82.51/15.86 fof(f284,plain,(
% 82.51/15.86 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f86])).
% 82.51/15.86 fof(f295,plain,(
% 82.51/15.86 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|hd(cons(X0,X1))=X0)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f97])).
% 82.51/15.86 fof(f296,plain,(
% 82.51/15.86 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 82.51/15.86 inference(miniscoping,[status(thm)],[f98])).
% 82.51/15.86 fof(f297,plain,(
% 82.51/15.86 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f296])).
% 82.51/15.86 fof(f300,plain,(
% 82.51/15.86 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f100])).
% 82.51/15.86 fof(f304,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|nil=X0)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f104])).
% 82.51/15.86 fof(f309,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|cons(skaf83(X0),skaf82(X0))=X0|nil=X0)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f109])).
% 82.51/15.86 fof(f318,plain,(
% 82.51/15.86 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 82.51/15.86 inference(miniscoping,[status(thm)],[f115])).
% 82.51/15.86 fof(f319,plain,(
% 82.51/15.86 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f318])).
% 82.51/15.86 fof(f320,plain,(
% 82.51/15.86 ![V]: (((![U]: (~cons(U,nil)=V|~ssItem(U)))|~ssList(V))|singletonP(V))),
% 82.51/15.86 inference(miniscoping,[status(thm)],[f116])).
% 82.51/15.86 fof(f321,plain,(
% 82.51/15.86 ![X0,X1]: (~cons(X0,nil)=X1|~ssItem(X0)|~ssList(X1)|singletonP(X1))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f320])).
% 82.51/15.86 fof(f328,plain,(
% 82.51/15.86 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=cons(X0,X1))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f120])).
% 82.51/15.86 fof(f403,plain,(
% 82.51/15.86 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 82.51/15.86 inference(miniscoping,[status(thm)],[f173])).
% 82.51/15.86 fof(f404,plain,(
% 82.51/15.86 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f403])).
% 82.51/15.86 fof(f428,plain,(
% 82.51/15.86 ssList(sk1)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f186])).
% 82.51/15.86 fof(f429,plain,(
% 82.51/15.86 ssList(sk2)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f187])).
% 82.51/15.86 fof(f432,plain,(
% 82.51/15.86 sk2=sk4),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f190])).
% 82.51/15.86 fof(f433,plain,(
% 82.51/15.86 sk1=sk3),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f191])).
% 82.51/15.86 fof(f434,plain,(
% 82.51/15.86 neq(sk2,nil)|neq(sk2,nil)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f192])).
% 82.51/15.86 fof(f439,plain,(
% 82.51/15.86 ((![B]: ((![A]: (((~ssList(A)|sk3=A)|~ssItem(B))|~cons(B,nil)=A))|~hd(sk4)=B))|~neq(nil,sk4))|~neq(sk4,nil)),
% 82.51/15.86 inference(miniscoping,[status(thm)],[f196])).
% 82.51/15.86 fof(f440,plain,(
% 82.51/15.86 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~neq(nil,sk4)|~neq(sk4,nil))),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f439])).
% 82.51/15.86 fof(f441,plain,(
% 82.51/15.86 ~singletonP(sk1)|~segmentP(sk2,sk1)|~neq(sk4,nil)),
% 82.51/15.86 inference(cnf_transformation,[status(thm)],[f197])).
% 82.51/15.86 fof(f449,definition,(
% 82.51/15.86 sQ2_spl <=> (neq(sk2,nil))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f450,plain,(
% 82.51/15.86 neq(sk2,nil)|~sQ2_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f449])).
% 82.51/15.86 fof(f452,plain,(
% 82.51/15.86 sQ2_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f434,f449])).
% 82.51/15.86 fof(f453,definition,(
% 82.51/15.86 sQ3_spl <=> (neq(sk4,nil))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f455,plain,(
% 82.51/15.86 ~neq(sk4,nil)|sQ3_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f453])).
% 82.51/15.86 fof(f457,definition,(
% 82.51/15.86 ![X0,X1]: (sQ4_spl <=> (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f458,plain,(
% 82.51/15.86 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~sQ4_spl)),
% 82.51/15.86 inference(component_clause,[status(thm)],[f457])).
% 82.51/15.86 fof(f460,definition,(
% 82.51/15.86 sQ5_spl <=> (neq(nil,sk4))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f462,plain,(
% 82.51/15.86 ~neq(nil,sk4)|sQ5_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f460])).
% 82.51/15.86 fof(f464,definition,(
% 82.51/15.86 sQ6_spl <=> (singletonP(sk1))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f467,definition,(
% 82.51/15.86 sQ7_spl <=> (segmentP(sk2,sk1))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f471,plain,(
% 82.51/15.86 sQ4_spl|~sQ5_spl|~sQ3_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f440,f457,f460,f453])).
% 82.51/15.86 fof(f472,plain,(
% 82.51/15.86 ~sQ6_spl|~sQ7_spl|~sQ3_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f441,f464,f467,f453])).
% 82.51/15.86 fof(f480,plain,(
% 82.51/15.86 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 82.51/15.86 inference(destructive_equality_resolution,[status(thm)],[f319])).
% 82.51/15.86 fof(f481,plain,(
% 82.51/15.86 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 82.51/15.86 inference(duplicate_literals_removal,[status(thm)],[f480])).
% 82.51/15.86 fof(f482,plain,(
% 82.51/15.86 ![X0]: (~ssItem(X0)|~ssList(cons(X0,nil))|singletonP(cons(X0,nil)))),
% 82.51/15.86 inference(destructive_equality_resolution,[status(thm)],[f321])).
% 82.51/15.86 fof(f491,plain,(
% 82.51/15.86 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 82.51/15.86 inference(destructive_equality_resolution,[status(thm)],[f404])).
% 82.51/15.86 fof(f502,plain,(
% 82.51/15.86 ~neq(sk2,nil)|sQ3_spl),
% 82.51/15.86 inference(backward_demodulation,[status(thm)],[f432,f455])).
% 82.51/15.86 fof(f504,plain,(
% 82.51/15.86 $false|~sQ2_spl|sQ3_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f502,f450])).
% 82.51/15.86 fof(f505,plain,(
% 82.51/15.86 ~sQ2_spl|sQ3_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f504])).
% 82.51/15.86 fof(f506,plain,(
% 82.51/15.86 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk2)=X1|~sQ4_spl)),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f432,f458])).
% 82.51/15.86 fof(f507,plain,(
% 82.51/15.86 ~ssList(cons(hd(sk2),nil))|sk3=cons(hd(sk2),nil)|~ssItem(hd(sk2))|~sQ4_spl),
% 82.51/15.86 inference(destructive_equality_resolution,[status(thm)],[f506])).
% 82.51/15.86 fof(f510,plain,(
% 82.51/15.86 ~ssList(cons(hd(sk2),nil))|sk1=cons(hd(sk2),nil)|~ssItem(hd(sk2))|~sQ4_spl),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f433,f507])).
% 82.51/15.86 fof(f511,plain,(
% 82.51/15.86 ~ssList(sk2)|nil=sk2|~ssList(cons(hd(sk2),nil))|sk1=cons(hd(sk2),nil)|~sQ4_spl),
% 82.51/15.86 inference(resolution,[status(thm)],[f274,f510])).
% 82.51/15.86 fof(f514,definition,(
% 82.51/15.86 sQ8_spl <=> (ssList(sk2))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f516,plain,(
% 82.51/15.86 ~ssList(sk2)|sQ8_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f514])).
% 82.51/15.86 fof(f517,definition,(
% 82.51/15.86 sQ9_spl <=> (nil=sk2)),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f518,plain,(
% 82.51/15.86 nil=sk2|~sQ9_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f517])).
% 82.51/15.86 fof(f520,definition,(
% 82.51/15.86 sQ10_spl <=> (ssList(cons(hd(sk2),nil)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f522,plain,(
% 82.51/15.86 ~ssList(cons(hd(sk2),nil))|sQ10_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f520])).
% 82.51/15.86 fof(f523,definition,(
% 82.51/15.86 sQ11_spl <=> (sk1=cons(hd(sk2),nil))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f524,plain,(
% 82.51/15.86 sk1=cons(hd(sk2),nil)|~sQ11_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f523])).
% 82.51/15.86 fof(f526,plain,(
% 82.51/15.86 ~sQ8_spl|sQ9_spl|~sQ10_spl|sQ11_spl|~sQ4_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f511,f514,f517,f520,f523,f457])).
% 82.51/15.86 fof(f527,plain,(
% 82.51/15.86 ~neq(nil,sk2)|sQ5_spl),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f432,f462])).
% 82.51/15.86 fof(f537,plain,(
% 82.51/15.86 ![X0,X1]: (~ssList(X0)|ssList(cons(hd(X1),X0))|~ssList(X1)|nil=X1)),
% 82.51/15.86 inference(resolution,[status(thm)],[f284,f274])).
% 82.51/15.86 fof(f542,definition,(
% 82.51/15.86 sQ12_spl <=> (ssList(nil))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f544,plain,(
% 82.51/15.86 ~ssList(nil)|sQ12_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f542])).
% 82.51/15.86 fof(f550,plain,(
% 82.51/15.86 $false|sQ12_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f544,f205])).
% 82.51/15.86 fof(f551,plain,(
% 82.51/15.86 sQ12_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f550])).
% 82.51/15.86 fof(f572,plain,(
% 82.51/15.86 ~ssList(sk2)|~ssList(nil)|nil=sk2|sQ5_spl),
% 82.51/15.86 inference(resolution,[status(thm)],[f300,f527])).
% 82.51/15.86 fof(f574,plain,(
% 82.51/15.86 ~sQ8_spl|~sQ12_spl|sQ9_spl|sQ5_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f572,f514,f542,f517,f460])).
% 82.51/15.86 fof(f575,definition,(
% 82.51/15.86 sQ14_spl <=> (ssItem(hd(sk2)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f576,plain,(
% 82.51/15.86 ssItem(hd(sk2))|~sQ14_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f575])).
% 82.51/15.86 fof(f577,plain,(
% 82.51/15.86 ~ssItem(hd(sk2))|sQ14_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f575])).
% 82.51/15.86 fof(f579,plain,(
% 82.51/15.86 $false|sQ8_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f516,f429])).
% 82.51/15.86 fof(f580,plain,(
% 82.51/15.86 sQ8_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f579])).
% 82.51/15.86 fof(f604,plain,(
% 82.51/15.86 ~ssItem(hd(sk2))|~ssList(cons(hd(sk2),nil))|singletonP(sk1)|~sQ11_spl),
% 82.51/15.86 inference(paramodulation,[status(thm)],[f524,f482])).
% 82.51/15.86 fof(f605,plain,(
% 82.51/15.86 ~sQ14_spl|~sQ10_spl|sQ6_spl|~sQ11_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f604,f575,f520,f464,f523])).
% 82.51/15.86 fof(f613,plain,(
% 82.51/15.86 app(nil,sk2)=sk2),
% 82.51/15.86 inference(resolution,[status(thm)],[f272,f429])).
% 82.51/15.86 fof(f614,plain,(
% 82.51/15.86 app(nil,sk1)=sk1),
% 82.51/15.86 inference(resolution,[status(thm)],[f272,f428])).
% 82.51/15.86 fof(f618,plain,(
% 82.51/15.86 ![X0,X1]: (~ssList(X0)|ssList(cons(skaf83(X1),X0)))),
% 82.51/15.86 inference(resolution,[status(thm)],[f209,f284])).
% 82.51/15.86 fof(f637,plain,(
% 82.51/15.86 neq(nil,nil)|~sQ9_spl|~sQ2_spl),
% 82.51/15.86 inference(backward_demodulation,[status(thm)],[f518,f450])).
% 82.51/15.86 fof(f672,definition,(
% 82.51/15.86 sQ18_spl <=> (nil=sk1)),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f786,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 82.51/15.86 inference(resolution,[status(thm)],[f283,f428])).
% 82.51/15.86 fof(f896,definition,(
% 82.51/15.86 sQ25_spl <=> (ssList(sk1))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f1209,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 82.51/15.86 inference(paramodulation,[status(thm)],[f614,f491])).
% 82.51/15.86 fof(f1231,definition,(
% 82.51/15.86 ![X0]: (sQ35_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f1232,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)|~sQ35_spl)),
% 82.51/15.86 inference(component_clause,[status(thm)],[f1231])).
% 82.51/15.86 fof(f1234,plain,(
% 82.51/15.86 sQ35_spl|~sQ12_spl|~sQ25_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f1209,f1231,f542,f896])).
% 82.51/15.86 fof(f1241,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(sk1,X0),sk1)|~sQ35_spl)),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f614,f1232])).
% 82.51/15.86 fof(f1242,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ35_spl)),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f1241,f786])).
% 82.51/15.86 fof(f1248,plain,(
% 82.51/15.86 ~ssList(nil)|~ssList(sk2)|nil=sk2|sQ10_spl),
% 82.51/15.86 inference(resolution,[status(thm)],[f537,f522])).
% 82.51/15.86 fof(f1264,plain,(
% 82.51/15.86 ~sQ12_spl|~sQ8_spl|sQ9_spl|sQ10_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f1248,f542,f514,f517,f520])).
% 82.51/15.86 fof(f1442,plain,(
% 82.51/15.86 ~ssList(sk2)|nil=sk2|sQ14_spl),
% 82.51/15.86 inference(resolution,[status(thm)],[f577,f274])).
% 82.51/15.86 fof(f1443,plain,(
% 82.51/15.86 ~sQ8_spl|sQ9_spl|sQ14_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f1442,f514,f517,f575])).
% 82.51/15.86 fof(f1447,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|hd(cons(hd(sk2),X0))=hd(sk2)|~sQ14_spl)),
% 82.51/15.86 inference(resolution,[status(thm)],[f576,f295])).
% 82.51/15.86 fof(f1448,plain,(
% 82.51/15.86 ![X0]: (~cons(hd(sk2),X0)=nil|~ssList(X0)|~sQ14_spl)),
% 82.51/15.86 inference(resolution,[status(thm)],[f576,f297])).
% 82.51/15.86 fof(f2737,plain,(
% 82.51/15.86 ~ssList(nil)|~sQ9_spl|~sQ2_spl),
% 82.51/15.86 inference(resolution,[status(thm)],[f637,f481])).
% 82.51/15.86 fof(f2738,plain,(
% 82.51/15.86 ~sQ12_spl|~sQ9_spl|~sQ2_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f2737,f542,f517,f449])).
% 82.51/15.86 fof(f3305,plain,(
% 82.51/15.86 hd(cons(hd(sk2),nil))=hd(sk2)|~sQ14_spl),
% 82.51/15.86 inference(resolution,[status(thm)],[f1447,f205])).
% 82.51/15.86 fof(f3307,plain,(
% 82.51/15.86 hd(sk1)=hd(sk2)|~sQ11_spl|~sQ14_spl),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f524,f3305])).
% 82.51/15.86 fof(f3313,plain,(
% 82.51/15.86 sk1=cons(hd(sk1),nil)|~sQ14_spl|~sQ11_spl),
% 82.51/15.86 inference(backward_demodulation,[status(thm)],[f3307,f524])).
% 82.51/15.86 fof(f3314,plain,(
% 82.51/15.86 ssItem(hd(sk1))|~sQ11_spl|~sQ14_spl),
% 82.51/15.86 inference(backward_demodulation,[status(thm)],[f3307,f576])).
% 82.51/15.86 fof(f3653,plain,(
% 82.51/15.86 ![X0]: (~cons(hd(sk1),X0)=nil|~ssList(X0)|~sQ11_spl|~sQ14_spl)),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f3307,f1448])).
% 82.51/15.86 fof(f3654,plain,(
% 82.51/15.86 ~sk1=nil|~ssList(nil)|~sQ14_spl|~sQ11_spl),
% 82.51/15.86 inference(paramodulation,[status(thm)],[f3313,f3653])).
% 82.51/15.86 fof(f3655,plain,(
% 82.51/15.86 ~sQ18_spl|~sQ12_spl|~sQ14_spl|~sQ11_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f3654,f672,f542,f575,f523])).
% 82.51/15.86 fof(f5408,plain,(
% 82.51/15.86 cons(hd(sk2),tl(sk2))=sk2|nil=sk2),
% 82.51/15.86 inference(resolution,[status(thm)],[f304,f429])).
% 82.51/15.86 fof(f5430,definition,(
% 82.51/15.86 sQ144_spl <=> (cons(hd(sk2),tl(sk2))=sk2)),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f5431,plain,(
% 82.51/15.86 cons(hd(sk2),tl(sk2))=sk2|~sQ144_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f5430])).
% 82.51/15.86 fof(f5433,plain,(
% 82.51/15.86 sQ144_spl|sQ9_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f5408,f5430,f517])).
% 82.51/15.86 fof(f5442,plain,(
% 82.51/15.86 cons(hd(sk1),tl(sk2))=sk2|~sQ11_spl|~sQ14_spl|~sQ144_spl),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f3307,f5431])).
% 82.51/15.86 fof(f5464,definition,(
% 82.51/15.86 sQ148_spl <=> (ssList(tl(sk2)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f5465,plain,(
% 82.51/15.86 ssList(tl(sk2))|~sQ148_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f5464])).
% 82.51/15.86 fof(f5843,plain,(
% 82.51/15.86 cons(skaf83(sk1),skaf82(sk1))=sk1|nil=sk1),
% 82.51/15.86 inference(resolution,[status(thm)],[f309,f428])).
% 82.51/15.86 fof(f5863,definition,(
% 82.51/15.86 sQ158_spl <=> (cons(skaf83(sk1),skaf82(sk1))=sk1)),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f5864,plain,(
% 82.51/15.86 cons(skaf83(sk1),skaf82(sk1))=sk1|~sQ158_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f5863])).
% 82.51/15.86 fof(f5866,plain,(
% 82.51/15.86 sQ158_spl|sQ18_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f5843,f5863,f672])).
% 82.51/15.86 fof(f5872,plain,(
% 82.51/15.86 ~ssList(skaf82(sk1))|ssList(sk1)|~sQ158_spl),
% 82.51/15.86 inference(paramodulation,[status(thm)],[f5864,f618])).
% 82.51/15.86 fof(f5874,definition,(
% 82.51/15.86 sQ159_spl <=> (ssList(skaf82(sk1)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f5876,plain,(
% 82.51/15.86 ~ssList(skaf82(sk1))|sQ159_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f5874])).
% 82.51/15.86 fof(f5878,plain,(
% 82.51/15.86 ~sQ159_spl|sQ25_spl|~sQ158_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f5872,f5874,f896,f5863])).
% 82.51/15.86 fof(f5883,definition,(
% 82.51/15.86 sQ160_spl <=> (ssList(skaf82(sk2)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f5885,plain,(
% 82.51/15.86 ~ssList(skaf82(sk2))|sQ160_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f5883])).
% 82.51/15.86 fof(f6504,plain,(
% 82.51/15.86 $false|sQ159_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f5876,f210])).
% 82.51/15.86 fof(f6505,plain,(
% 82.51/15.86 sQ159_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f6504])).
% 82.51/15.86 fof(f6506,plain,(
% 82.51/15.86 $false|sQ160_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f5885,f210])).
% 82.51/15.86 fof(f6507,plain,(
% 82.51/15.86 sQ160_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f6506])).
% 82.51/15.86 fof(f7933,definition,(
% 82.51/15.86 sQ185_spl <=> (ssList(skaf46(sk2,sk2)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f7935,plain,(
% 82.51/15.86 ~ssList(skaf46(sk2,sk2))|sQ185_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f7933])).
% 82.51/15.86 fof(f7946,definition,(
% 82.51/15.86 sQ187_spl <=> (ssList(skaf46(nil,nil)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f7948,plain,(
% 82.51/15.86 ~ssList(skaf46(nil,nil))|sQ187_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f7946])).
% 82.51/15.86 fof(f8029,definition,(
% 82.51/15.86 sQ189_spl <=> (ssList(skaf46(sk1,sk1)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f8031,plain,(
% 82.51/15.86 ~ssList(skaf46(sk1,sk1))|sQ189_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f8029])).
% 82.51/15.86 fof(f8038,definition,(
% 82.51/15.86 sQ190_spl <=> (ssList(skaf45(sk2,sk2)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f8040,plain,(
% 82.51/15.86 ~ssList(skaf45(sk2,sk2))|sQ190_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f8038])).
% 82.51/15.86 fof(f8046,plain,(
% 82.51/15.86 $false|sQ190_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f8040,f248])).
% 82.51/15.86 fof(f8047,plain,(
% 82.51/15.86 sQ190_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8046])).
% 82.51/15.86 fof(f8054,definition,(
% 82.51/15.86 sQ192_spl <=> (ssList(skaf45(nil,nil)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f8056,plain,(
% 82.51/15.86 ~ssList(skaf45(nil,nil))|sQ192_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f8054])).
% 82.51/15.86 fof(f8064,plain,(
% 82.51/15.86 $false|sQ192_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f8056,f248])).
% 82.51/15.86 fof(f8065,plain,(
% 82.51/15.86 sQ192_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8064])).
% 82.51/15.86 fof(f8073,definition,(
% 82.51/15.86 sQ194_spl <=> (ssList(skaf45(sk1,sk1)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f8075,plain,(
% 82.51/15.86 ~ssList(skaf45(sk1,sk1))|sQ194_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f8073])).
% 82.51/15.86 fof(f8084,plain,(
% 82.51/15.86 $false|sQ194_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f8075,f248])).
% 82.51/15.86 fof(f8085,plain,(
% 82.51/15.86 sQ194_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8084])).
% 82.51/15.86 fof(f8242,plain,(
% 82.51/15.86 $false|sQ189_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f8031,f247])).
% 82.51/15.86 fof(f8243,plain,(
% 82.51/15.86 sQ189_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8242])).
% 82.51/15.86 fof(f8244,plain,(
% 82.51/15.86 $false|sQ187_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f7948,f247])).
% 82.51/15.86 fof(f8245,plain,(
% 82.51/15.86 sQ187_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8244])).
% 82.51/15.86 fof(f8246,plain,(
% 82.51/15.86 $false|sQ185_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f7935,f247])).
% 82.51/15.86 fof(f8247,plain,(
% 82.51/15.86 sQ185_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8246])).
% 82.51/15.86 fof(f8728,definition,(
% 82.51/15.86 sQ221_spl <=> (ssList(skaf46(sk2,nil)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f8730,plain,(
% 82.51/15.86 ~ssList(skaf46(sk2,nil))|sQ221_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f8728])).
% 82.51/15.86 fof(f8740,plain,(
% 82.51/15.86 $false|sQ221_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f8730,f247])).
% 82.51/15.86 fof(f8741,plain,(
% 82.51/15.86 sQ221_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8740])).
% 82.51/15.86 fof(f8750,definition,(
% 82.51/15.86 sQ224_spl <=> (ssList(skaf46(sk1,nil)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f8752,plain,(
% 82.51/15.86 ~ssList(skaf46(sk1,nil))|sQ224_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f8750])).
% 82.51/15.86 fof(f8762,plain,(
% 82.51/15.86 $false|sQ224_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f8752,f247])).
% 82.51/15.86 fof(f8763,plain,(
% 82.51/15.86 sQ224_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8762])).
% 82.51/15.86 fof(f8837,definition,(
% 82.51/15.86 sQ227_spl <=> (ssList(skaf45(sk2,nil)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f8839,plain,(
% 82.51/15.86 ~ssList(skaf45(sk2,nil))|sQ227_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f8837])).
% 82.51/15.86 fof(f8852,plain,(
% 82.51/15.86 $false|sQ227_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f8839,f248])).
% 82.51/15.86 fof(f8853,plain,(
% 82.51/15.86 sQ227_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8852])).
% 82.51/15.86 fof(f8866,definition,(
% 82.51/15.86 sQ230_spl <=> (ssList(skaf45(sk1,nil)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f8868,plain,(
% 82.51/15.86 ~ssList(skaf45(sk1,nil))|sQ230_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f8866])).
% 82.51/15.86 fof(f8881,plain,(
% 82.51/15.86 $false|sQ230_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f8868,f248])).
% 82.51/15.86 fof(f8882,plain,(
% 82.51/15.86 sQ230_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f8881])).
% 82.51/15.86 fof(f19375,definition,(
% 82.51/15.86 ![X0]: (sQ863_spl <=> (~app(X0,sk2)=app(X0,sk2)|~ssList(X0)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ863_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f19376,plain,(
% 82.51/15.86 ![X0]: (~app(X0,sk2)=app(X0,sk2)|~ssList(X0)|~sQ863_spl)),
% 82.51/15.86 inference(component_clause,[status(thm)],[f19375])).
% 82.51/15.86 fof(f19390,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|~sQ863_spl)),
% 82.51/15.86 inference(trivial_equality_resolution,[status(thm)],[f19376])).
% 82.51/15.86 fof(f19391,plain,(
% 82.51/15.86 $false|~sQ863_spl),
% 82.51/15.86 inference(backward_subsumption_resolution,[status(thm)],[f241,f19390])).
% 82.51/15.86 fof(f19429,plain,(
% 82.51/15.86 ~sQ863_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f19391])).
% 82.51/15.86 fof(f19464,definition,(
% 82.51/15.86 ![X0]: (sQ867_spl <=> (~app(X0,sk1)=app(X0,sk1)|~ssList(X0)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ867_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f19465,plain,(
% 82.51/15.86 ![X0]: (~app(X0,sk1)=app(X0,sk1)|~ssList(X0)|~sQ867_spl)),
% 82.51/15.86 inference(component_clause,[status(thm)],[f19464])).
% 82.51/15.86 fof(f19473,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|~sQ867_spl)),
% 82.51/15.86 inference(trivial_equality_resolution,[status(thm)],[f19465])).
% 82.51/15.86 fof(f19474,plain,(
% 82.51/15.86 $false|~sQ867_spl),
% 82.51/15.86 inference(backward_subsumption_resolution,[status(thm)],[f246,f19473])).
% 82.51/15.86 fof(f19482,plain,(
% 82.51/15.86 ~sQ867_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f19474])).
% 82.51/15.86 fof(f19524,definition,(
% 82.51/15.86 sQ869_spl <=> (app(nil,sk2)=sk2)),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ869_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f19526,plain,(
% 82.51/15.86 ~app(nil,sk2)=sk2|sQ869_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f19524])).
% 82.51/15.86 fof(f19532,plain,(
% 82.51/15.86 ~sk2=sk2|sQ869_spl),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f613,f19526])).
% 82.51/15.86 fof(f19533,plain,(
% 82.51/15.86 $false|sQ869_spl),
% 82.51/15.86 inference(trivial_equality_resolution,[status(thm)],[f19532])).
% 82.51/15.86 fof(f19534,plain,(
% 82.51/15.86 sQ869_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f19533])).
% 82.51/15.86 fof(f19587,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|app(cons(hd(sk1),nil),X0)=cons(hd(sk1),X0)|~sQ11_spl|~sQ14_spl)),
% 82.51/15.86 inference(resolution,[status(thm)],[f328,f3314])).
% 82.51/15.86 fof(f19588,plain,(
% 82.51/15.86 ![X0]: (~ssList(X0)|app(sk1,X0)=cons(hd(sk1),X0)|~sQ11_spl|~sQ14_spl)),
% 82.51/15.86 inference(forward_demodulation,[status(thm)],[f3313,f19587])).
% 82.51/15.86 fof(f24153,definition,(
% 82.51/15.86 sQ1073_spl <=> (ssItem(skaf70(sk2)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ1073_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f24155,plain,(
% 82.51/15.86 ~ssItem(skaf70(sk2))|sQ1073_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f24153])).
% 82.51/15.86 fof(f24156,definition,(
% 82.51/15.86 sQ1074_spl <=> (ssItem(skaf69(sk2)))),
% 82.51/15.86 introduced(definition,[new_symbols(definition,[sQ1074_spl])],[split_symbol_definition])).
% 82.51/15.86 fof(f24158,plain,(
% 82.51/15.86 ~ssItem(skaf69(sk2))|sQ1074_spl),
% 82.51/15.86 inference(component_clause,[status(thm)],[f24156])).
% 82.51/15.86 fof(f24231,plain,(
% 82.51/15.86 $false|sQ1073_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f24155,f222])).
% 82.51/15.86 fof(f24232,plain,(
% 82.51/15.86 sQ1073_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f24231])).
% 82.51/15.86 fof(f24233,plain,(
% 82.51/15.86 $false|sQ1074_spl),
% 82.51/15.86 inference(forward_subsumption_resolution,[status(thm)],[f24158,f223])).
% 82.51/15.86 fof(f24234,plain,(
% 82.51/15.86 sQ1074_spl),
% 82.51/15.86 inference(contradiction_clause,[status(thm)],[f24233])).
% 82.51/15.86 fof(f30358,plain,(
% 82.51/15.86 ssList(tl(sk2))|nil=sk2),
% 82.51/15.86 inference(resolution,[status(thm)],[f273,f429])).
% 82.51/15.86 fof(f30380,plain,(
% 82.51/15.86 sQ148_spl|sQ9_spl),
% 82.51/15.86 inference(split_clause,[status(thm)],[f30358,f5464,f517])).
% 82.51/15.93 fof(f30630,plain,(
% 82.51/15.93 app(sk1,tl(sk2))=cons(hd(sk1),tl(sk2))|~sQ148_spl|~sQ11_spl|~sQ14_spl),
% 82.51/15.93 inference(resolution,[status(thm)],[f5465,f19588])).
% 82.51/15.93 fof(f30689,plain,(
% 82.51/15.93 app(sk1,tl(sk2))=sk2|~sQ144_spl|~sQ148_spl|~sQ11_spl|~sQ14_spl),
% 82.51/15.93 inference(forward_demodulation,[status(thm)],[f5442,f30630])).
% 82.51/15.93 fof(f30877,plain,(
% 82.51/15.93 ~ssList(tl(sk2))|segmentP(sk2,sk1)|~sQ35_spl|~sQ144_spl|~sQ148_spl|~sQ11_spl|~sQ14_spl),
% 82.51/15.93 inference(paramodulation,[status(thm)],[f30689,f1242])).
% 82.51/15.93 fof(f30895,plain,(
% 82.51/15.93 ~sQ148_spl|sQ7_spl|~sQ35_spl|~sQ144_spl|~sQ11_spl|~sQ14_spl),
% 82.51/15.93 inference(split_clause,[status(thm)],[f30877,f5464,f467,f1231,f5430,f523,f575])).
% 82.51/15.93 fof(f30914,plain,(
% 82.51/15.93 $false),
% 82.51/15.93 inference(sat_refutation,[status(thm)],[f452,f471,f472,f505,f526,f551,f574,f580,f605,f1234,f1264,f1443,f2738,f3655,f5433,f5866,f5878,f6505,f6507,f8047,f8065,f8085,f8243,f8245,f8247,f8741,f8763,f8853,f8882,f19429,f19482,f19534,f24232,f24234,f30380,f30895])).
% 82.51/15.93 % SZS output end CNFRefutation for theBenchmark.p
% 18.63/15.98 % Elapsed time: 10.595267 seconds
% 18.63/15.98 % CPU time: 83.675160 seconds
% 18.63/15.98 % Total memory used: 948.645 MB
% 18.63/15.98 % Net memory used: 895.295 MB
%------------------------------------------------------------------------------