%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC120-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:38 PM UTC 2026
% Result : Unsatisfiable 72.72s 9.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC120-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.07/0.36 % Computer : n011.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Mon Sep 21 07:57:11 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.38 % Drodi V4.1.1
% 72.72/9.75 % Refutation found
% 72.72/9.75 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 72.72/9.75 % SZS output start CNFRefutation for theBenchmark
% 72.72/9.75 fof(f8,axiom,(
% 72.72/9.75 ssList(nil) ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f9,axiom,(
% 72.72/9.75 ssItem(skac3) ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f10,axiom,(
% 72.72/9.75 ssItem(skac2) ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f12,axiom,(
% 72.72/9.75 (![U]: (ssItem(skaf83(U)) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f13,axiom,(
% 72.72/9.75 (![U]: (ssList(skaf82(U)) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f54,axiom,(
% 72.72/9.75 skac3 != skac2 ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f73,axiom,(
% 72.72/9.75 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f74,axiom,(
% 72.72/9.75 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f75,axiom,(
% 72.72/9.75 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f78,axiom,(
% 72.72/9.75 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f85,axiom,(
% 72.72/9.75 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f98,axiom,(
% 72.72/9.75 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f99,axiom,(
% 72.72/9.75 (![U,V]: (( cons(U,V) != V| ~ ssItem(U)| ~ ssList(V) ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f100,axiom,(
% 72.72/9.75 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f104,axiom,(
% 72.72/9.75 (![U]: (( ~ ssList(U)| cons(hd(U),tl(U)) = U| nil = U ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f115,axiom,(
% 72.72/9.75 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f150,axiom,(
% 72.72/9.75 (![U,V,W]: (( app(U,V) != app(U,W)| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| V = W ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f173,axiom,(
% 72.72/9.75 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f187,negated_conjecture,(
% 72.72/9.75 ssList(sk2) ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f188,negated_conjecture,(
% 72.72/9.75 ssList(sk3) ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f190,negated_conjecture,(
% 72.72/9.75 sk2 = sk4 ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f191,negated_conjecture,(
% 72.72/9.75 sk1 = sk3 ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f192,negated_conjecture,(
% 72.72/9.75 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f196,negated_conjecture,(
% 72.72/9.75 (![A,B]: (( ~ ssList(A)| sk4 = A| ~ ssList(B)| tl(sk4) != B| app(sk3,B) != A| ~ neq(nil,sk4)| ~ neq(sk4,nil) ) ))),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f197,negated_conjecture,(
% 72.72/9.75 ( ~ neq(sk1,nil)| ~ segmentP(sk2,sk1)| ~ neq(sk4,nil) ) ),
% 72.72/9.75 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 72.72/9.75 fof(f205,plain,(
% 72.72/9.75 ssList(nil)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f8])).
% 72.72/9.75 fof(f206,plain,(
% 72.72/9.75 ssItem(skac3)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f9])).
% 72.72/9.75 fof(f207,plain,(
% 72.72/9.75 ssItem(skac2)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f10])).
% 72.72/9.75 fof(f209,plain,(
% 72.72/9.75 ![X0]: (ssItem(skaf83(X0)))),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f12])).
% 72.72/9.75 fof(f210,plain,(
% 72.72/9.75 ![X0]: (ssList(skaf82(X0)))),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f13])).
% 72.72/9.75 fof(f251,plain,(
% 72.72/9.75 ~skac3=skac2),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f54])).
% 72.72/9.75 fof(f271,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f73])).
% 72.72/9.75 fof(f272,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f74])).
% 72.72/9.75 fof(f273,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f75])).
% 72.72/9.75 fof(f276,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f78])).
% 72.72/9.75 fof(f283,plain,(
% 72.72/9.75 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f85])).
% 72.72/9.75 fof(f296,plain,(
% 72.72/9.75 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 72.72/9.75 inference(miniscoping,[status(thm)],[f98])).
% 72.72/9.75 fof(f297,plain,(
% 72.72/9.75 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f296])).
% 72.72/9.75 fof(f298,plain,(
% 72.72/9.75 ![V]: ((![U]: (~cons(U,V)=V|~ssItem(U)))|~ssList(V))),
% 72.72/9.75 inference(miniscoping,[status(thm)],[f99])).
% 72.72/9.75 fof(f299,plain,(
% 72.72/9.75 ![X0,X1]: (~cons(X0,X1)=X1|~ssItem(X0)|~ssList(X1))),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f298])).
% 72.72/9.75 fof(f300,plain,(
% 72.72/9.75 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f100])).
% 72.72/9.75 fof(f304,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|nil=X0)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f104])).
% 72.72/9.75 fof(f318,plain,(
% 72.72/9.75 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 72.72/9.75 inference(miniscoping,[status(thm)],[f115])).
% 72.72/9.75 fof(f319,plain,(
% 72.72/9.75 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f318])).
% 72.72/9.75 fof(f367,plain,(
% 72.72/9.75 ![V,W]: (((![U]: ((~app(U,V)=app(U,W)|~ssList(V))|~ssList(U)))|~ssList(W))|V=W)),
% 72.72/9.75 inference(miniscoping,[status(thm)],[f150])).
% 72.72/9.75 fof(f368,plain,(
% 72.72/9.75 ![X0,X1,X2]: (~app(X0,X1)=app(X0,X2)|~ssList(X1)|~ssList(X0)|~ssList(X2)|X1=X2)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f367])).
% 72.72/9.75 fof(f403,plain,(
% 72.72/9.75 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 72.72/9.75 inference(miniscoping,[status(thm)],[f173])).
% 72.72/9.75 fof(f404,plain,(
% 72.72/9.75 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f403])).
% 72.72/9.75 fof(f429,plain,(
% 72.72/9.75 ssList(sk2)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f187])).
% 72.72/9.75 fof(f430,plain,(
% 72.72/9.75 ssList(sk3)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f188])).
% 72.72/9.75 fof(f432,plain,(
% 72.72/9.75 sk2=sk4),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f190])).
% 72.72/9.75 fof(f433,plain,(
% 72.72/9.75 sk1=sk3),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f191])).
% 72.72/9.75 fof(f434,plain,(
% 72.72/9.75 neq(sk2,nil)|neq(sk2,nil)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f192])).
% 72.72/9.75 fof(f439,plain,(
% 72.72/9.75 ((![A,B]: ((((~ssList(A)|sk4=A)|~ssList(B))|~tl(sk4)=B)|~app(sk3,B)=A))|~neq(nil,sk4))|~neq(sk4,nil)),
% 72.72/9.75 inference(miniscoping,[status(thm)],[f196])).
% 72.72/9.75 fof(f440,plain,(
% 72.72/9.75 ![X0,X1]: (~ssList(X0)|sk4=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk3,X1)=X0|~neq(nil,sk4)|~neq(sk4,nil))),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f439])).
% 72.72/9.75 fof(f441,plain,(
% 72.72/9.75 ~neq(sk1,nil)|~segmentP(sk2,sk1)|~neq(sk4,nil)),
% 72.72/9.75 inference(cnf_transformation,[status(thm)],[f197])).
% 72.72/9.75 fof(f449,definition,(
% 72.72/9.75 sQ2_spl <=> (neq(sk2,nil))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f450,plain,(
% 72.72/9.75 neq(sk2,nil)|~sQ2_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f449])).
% 72.72/9.75 fof(f452,plain,(
% 72.72/9.75 sQ2_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f434,f449])).
% 72.72/9.75 fof(f453,definition,(
% 72.72/9.75 sQ3_spl <=> (neq(sk4,nil))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f455,plain,(
% 72.72/9.75 ~neq(sk4,nil)|sQ3_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f453])).
% 72.72/9.75 fof(f457,definition,(
% 72.72/9.75 ![X0,X1]: (sQ4_spl <=> (~ssList(X0)|sk4=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk3,X1)=X0))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f458,plain,(
% 72.72/9.75 ![X0,X1]: (~ssList(X0)|sk4=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk3,X1)=X0|~sQ4_spl)),
% 72.72/9.75 inference(component_clause,[status(thm)],[f457])).
% 72.72/9.75 fof(f460,definition,(
% 72.72/9.75 sQ5_spl <=> (neq(nil,sk4))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f462,plain,(
% 72.72/9.75 ~neq(nil,sk4)|sQ5_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f460])).
% 72.72/9.75 fof(f464,definition,(
% 72.72/9.75 sQ6_spl <=> (neq(sk1,nil))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f466,plain,(
% 72.72/9.75 ~neq(sk1,nil)|sQ6_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f464])).
% 72.72/9.75 fof(f467,definition,(
% 72.72/9.75 sQ7_spl <=> (segmentP(sk2,sk1))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f469,plain,(
% 72.72/9.75 ~segmentP(sk2,sk1)|sQ7_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f467])).
% 72.72/9.75 fof(f471,plain,(
% 72.72/9.75 sQ4_spl|~sQ5_spl|~sQ3_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f440,f457,f460,f453])).
% 72.72/9.75 fof(f472,plain,(
% 72.72/9.75 ~sQ6_spl|~sQ7_spl|~sQ3_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f441,f464,f467,f453])).
% 72.72/9.75 fof(f480,plain,(
% 72.72/9.75 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 72.72/9.75 inference(destructive_equality_resolution,[status(thm)],[f319])).
% 72.72/9.75 fof(f481,plain,(
% 72.72/9.75 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 72.72/9.75 inference(duplicate_literals_removal,[status(thm)],[f480])).
% 72.72/9.75 fof(f491,plain,(
% 72.72/9.75 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 72.72/9.75 inference(destructive_equality_resolution,[status(thm)],[f404])).
% 72.72/9.75 fof(f504,plain,(
% 72.72/9.75 ~neq(sk2,nil)|sQ3_spl),
% 72.72/9.75 inference(forward_demodulation,[status(thm)],[f432,f455])).
% 72.72/9.75 fof(f505,plain,(
% 72.72/9.75 $false|~sQ2_spl|sQ3_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f504,f450])).
% 72.72/9.75 fof(f506,plain,(
% 72.72/9.75 ~sQ2_spl|sQ3_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f505])).
% 72.72/9.75 fof(f507,plain,(
% 72.72/9.75 ![X0,X1]: (~ssList(X0)|sk2=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk3,X1)=X0|~sQ4_spl)),
% 72.72/9.75 inference(forward_demodulation,[status(thm)],[f432,f458])).
% 72.72/9.75 fof(f508,plain,(
% 72.72/9.75 ![X0,X1]: (~ssList(X0)|sk2=X0|~ssList(X1)|~tl(sk2)=X1|~app(sk3,X1)=X0|~sQ4_spl)),
% 72.72/9.75 inference(forward_demodulation,[status(thm)],[f432,f507])).
% 72.72/9.75 fof(f509,plain,(
% 72.72/9.75 ~ssList(app(sk3,tl(sk2)))|sk2=app(sk3,tl(sk2))|~ssList(tl(sk2))|~sQ4_spl),
% 72.72/9.75 inference(destructive_equality_resolution,[status(thm)],[f508])).
% 72.72/9.75 fof(f510,plain,(
% 72.72/9.75 ~neq(sk3,nil)|sQ6_spl),
% 72.72/9.75 inference(forward_demodulation,[status(thm)],[f433,f466])).
% 72.72/9.75 fof(f514,plain,(
% 72.72/9.75 app(sk3,nil)=sk3),
% 72.72/9.75 inference(resolution,[status(thm)],[f271,f430])).
% 72.72/9.75 fof(f518,plain,(
% 72.72/9.75 app(nil,sk3)=sk3),
% 72.72/9.75 inference(resolution,[status(thm)],[f272,f430])).
% 72.72/9.75 fof(f519,plain,(
% 72.72/9.75 app(nil,sk2)=sk2),
% 72.72/9.75 inference(resolution,[status(thm)],[f272,f429])).
% 72.72/9.75 fof(f540,definition,(
% 72.72/9.75 sQ8_spl <=> (ssList(nil))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f542,plain,(
% 72.72/9.75 ~ssList(nil)|sQ8_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f540])).
% 72.72/9.75 fof(f548,plain,(
% 72.72/9.75 $false|sQ8_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f542,f205])).
% 72.72/9.75 fof(f549,plain,(
% 72.72/9.75 sQ8_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f548])).
% 72.72/9.75 fof(f561,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|ssList(app(sk3,X0)))),
% 72.72/9.75 inference(resolution,[status(thm)],[f283,f430])).
% 72.72/9.75 fof(f593,plain,(
% 72.72/9.75 sk2=app(sk3,tl(sk2))|~ssList(tl(sk2))|~sQ4_spl),
% 72.72/9.75 inference(backward_subsumption_resolution,[status(thm)],[f509,f561])).
% 72.72/9.75 fof(f597,plain,(
% 72.72/9.75 ~ssList(nil)|ssList(sk3)),
% 72.72/9.75 inference(paramodulation,[status(thm)],[f514,f561])).
% 72.72/9.75 fof(f598,definition,(
% 72.72/9.75 sQ10_spl <=> (sk2=app(sk3,tl(sk2)))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f599,plain,(
% 72.72/9.75 sk2=app(sk3,tl(sk2))|~sQ10_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f598])).
% 72.72/9.75 fof(f601,definition,(
% 72.72/9.75 sQ11_spl <=> (ssList(tl(sk2)))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f603,plain,(
% 72.72/9.75 ~ssList(tl(sk2))|sQ11_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f601])).
% 72.72/9.75 fof(f604,plain,(
% 72.72/9.75 sQ10_spl|~sQ11_spl|~sQ4_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f593,f598,f601,f457])).
% 72.72/9.75 fof(f605,definition,(
% 72.72/9.75 sQ12_spl <=> (ssList(sk3))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f608,plain,(
% 72.72/9.75 ~sQ8_spl|sQ12_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f597,f540,f605])).
% 72.72/9.75 fof(f609,plain,(
% 72.72/9.75 ~neq(nil,sk2)|sQ5_spl),
% 72.72/9.75 inference(forward_demodulation,[status(thm)],[f432,f462])).
% 72.72/9.75 fof(f610,plain,(
% 72.72/9.75 ~segmentP(sk2,sk3)|sQ7_spl),
% 72.72/9.75 inference(forward_demodulation,[status(thm)],[f433,f469])).
% 72.72/9.75 fof(f611,plain,(
% 72.72/9.75 ~ssList(sk2)|nil=sk2|sQ11_spl),
% 72.72/9.75 inference(resolution,[status(thm)],[f603,f273])).
% 72.72/9.75 fof(f612,definition,(
% 72.72/9.75 sQ13_spl <=> (ssList(sk2))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f614,plain,(
% 72.72/9.75 ~ssList(sk2)|sQ13_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f612])).
% 72.72/9.75 fof(f615,definition,(
% 72.72/9.75 sQ14_spl <=> (nil=sk2)),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f616,plain,(
% 72.72/9.75 nil=sk2|~sQ14_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f615])).
% 72.72/9.75 fof(f618,plain,(
% 72.72/9.75 ~sQ13_spl|sQ14_spl|sQ11_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f611,f612,f615,f601])).
% 72.72/9.75 fof(f619,plain,(
% 72.72/9.75 $false|sQ13_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f614,f429])).
% 72.72/9.75 fof(f620,plain,(
% 72.72/9.75 sQ13_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f619])).
% 72.72/9.75 fof(f649,plain,(
% 72.72/9.75 neq(sk2,sk2)|~sQ14_spl|~sQ2_spl),
% 72.72/9.75 inference(backward_demodulation,[status(thm)],[f616,f450])).
% 72.72/9.75 fof(f731,definition,(
% 72.72/9.75 sQ21_spl <=> (nil=sk3)),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f732,plain,(
% 72.72/9.75 nil=sk3|~sQ21_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f731])).
% 72.72/9.75 fof(f974,plain,(
% 72.72/9.75 ~ssList(sk2)|~sQ14_spl|~sQ2_spl),
% 72.72/9.75 inference(resolution,[status(thm)],[f649,f481])).
% 72.72/9.75 fof(f975,plain,(
% 72.72/9.75 ~sQ13_spl|~sQ14_spl|~sQ2_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f974,f612,f615,f449])).
% 72.72/9.75 fof(f1153,plain,(
% 72.72/9.75 ![X0]: (~app(sk3,X0)=sk2|~ssList(X0)|~ssList(sk3)|~ssList(tl(sk2))|X0=tl(sk2)|~sQ10_spl)),
% 72.72/9.75 inference(paramodulation,[status(thm)],[f599,f368])).
% 72.72/9.75 fof(f1161,definition,(
% 72.72/9.75 ![X0]: (sQ37_spl <=> (~app(sk3,X0)=sk2|~ssList(X0)|X0=tl(sk2)))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f1162,plain,(
% 72.72/9.75 ![X0]: (~app(sk3,X0)=sk2|~ssList(X0)|X0=tl(sk2)|~sQ37_spl)),
% 72.72/9.75 inference(component_clause,[status(thm)],[f1161])).
% 72.72/9.75 fof(f1164,plain,(
% 72.72/9.75 sQ37_spl|~sQ12_spl|~sQ11_spl|~sQ10_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f1153,f1161,f605,f601,f598])).
% 72.72/9.75 fof(f1173,plain,(
% 72.72/9.75 ~ssList(sk2)|~ssList(nil)|nil=sk2|sQ5_spl),
% 72.72/9.75 inference(resolution,[status(thm)],[f609,f300])).
% 72.72/9.75 fof(f1178,plain,(
% 72.72/9.75 ~sQ13_spl|~sQ8_spl|sQ14_spl|sQ5_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f1173,f612,f540,f615,f460])).
% 72.72/9.75 fof(f1244,plain,(
% 72.72/9.75 ~ssList(nil)|~ssList(sk3)|sk3=nil|sQ6_spl),
% 72.72/9.75 inference(resolution,[status(thm)],[f510,f300])).
% 72.72/9.75 fof(f1246,plain,(
% 72.72/9.75 ~sQ8_spl|~sQ12_spl|sQ21_spl|sQ6_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f1244,f540,f605,f731,f464])).
% 72.72/9.75 fof(f1387,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk3)|~ssList(app(sk3,X0))|segmentP(app(app(nil,sk3),X0),sk3))),
% 72.72/9.75 inference(paramodulation,[status(thm)],[f518,f491])).
% 72.72/9.75 fof(f1392,definition,(
% 72.72/9.75 ![X0]: (sQ50_spl <=> (~ssList(X0)|~ssList(app(sk3,X0))|segmentP(app(app(nil,sk3),X0),sk3)))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f1393,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|~ssList(app(sk3,X0))|segmentP(app(app(nil,sk3),X0),sk3)|~sQ50_spl)),
% 72.72/9.75 inference(component_clause,[status(thm)],[f1392])).
% 72.72/9.75 fof(f1395,plain,(
% 72.72/9.75 sQ50_spl|~sQ8_spl|~sQ12_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f1387,f1392,f540,f605])).
% 72.72/9.75 fof(f1400,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|~ssList(app(sk3,X0))|segmentP(app(sk3,X0),sk3)|~sQ50_spl)),
% 72.72/9.75 inference(forward_demodulation,[status(thm)],[f518,f1393])).
% 72.72/9.75 fof(f1401,plain,(
% 72.72/9.75 ![X0]: (~ssList(X0)|segmentP(app(sk3,X0),sk3)|~sQ50_spl)),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f1400,f561])).
% 72.72/9.75 fof(f1404,plain,(
% 72.72/9.75 cons(hd(sk2),tl(sk2))=sk2|nil=sk2),
% 72.72/9.75 inference(resolution,[status(thm)],[f304,f429])).
% 72.72/9.75 fof(f1442,definition,(
% 72.72/9.75 sQ53_spl <=> (cons(hd(sk2),tl(sk2))=sk2)),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f1443,plain,(
% 72.72/9.75 cons(hd(sk2),tl(sk2))=sk2|~sQ53_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f1442])).
% 72.72/9.75 fof(f1445,plain,(
% 72.72/9.75 sQ53_spl|sQ14_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f1404,f1442,f615])).
% 72.72/9.75 fof(f2027,plain,(
% 72.72/9.75 app(sk3,sk2)=sk2|~sQ21_spl),
% 72.72/9.75 inference(backward_demodulation,[status(thm)],[f732,f519])).
% 72.72/9.75 fof(f6018,definition,(
% 72.72/9.75 sQ346_spl <=> (sk2=tl(sk2))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f6019,plain,(
% 72.72/9.75 sk2=tl(sk2)|~sQ346_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f6018])).
% 72.72/9.75 fof(f7574,plain,(
% 72.72/9.75 ![X0]: (~cons(skac2,X0)=X0|~ssList(X0))),
% 72.72/9.75 inference(resolution,[status(thm)],[f299,f207])).
% 72.72/9.75 fof(f7575,plain,(
% 72.72/9.75 ![X0]: (~cons(skac3,X0)=X0|~ssList(X0))),
% 72.72/9.75 inference(resolution,[status(thm)],[f299,f206])).
% 72.72/9.75 fof(f7785,plain,(
% 72.72/9.75 ~cons(skac2,nil)=nil),
% 72.72/9.75 inference(resolution,[status(thm)],[f7574,f205])).
% 72.72/9.75 fof(f7822,plain,(
% 72.72/9.75 ![X0]: (~cons(skac2,skaf82(X0))=skaf82(X0))),
% 72.72/9.75 inference(resolution,[status(thm)],[f7574,f210])).
% 72.72/9.75 fof(f7825,plain,(
% 72.72/9.75 ~cons(skac3,nil)=nil),
% 72.72/9.75 inference(resolution,[status(thm)],[f7575,f205])).
% 72.72/9.75 fof(f8710,plain,(
% 72.72/9.75 ~app(sk3,sk2)=sk2|sk2=tl(sk2)|~sQ37_spl),
% 72.72/9.75 inference(resolution,[status(thm)],[f1162,f429])).
% 72.72/9.75 fof(f8755,definition,(
% 72.72/9.75 sQ501_spl <=> (app(sk3,sk2)=sk2)),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ501_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f8757,plain,(
% 72.72/9.75 ~app(sk3,sk2)=sk2|sQ501_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f8755])).
% 72.72/9.75 fof(f8758,plain,(
% 72.72/9.75 ~sQ501_spl|sQ346_spl|~sQ37_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f8710,f8755,f6018,f1161])).
% 72.72/9.75 fof(f9160,plain,(
% 72.72/9.75 cons(hd(sk2),sk2)=sk2|~sQ346_spl|~sQ53_spl),
% 72.72/9.75 inference(forward_demodulation,[status(thm)],[f6019,f1443])).
% 72.72/9.75 fof(f9183,definition,(
% 72.72/9.75 sQ523_spl <=> (ssItem(hd(sk2)))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f9184,plain,(
% 72.72/9.75 ssItem(hd(sk2))|~sQ523_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f9183])).
% 72.72/9.75 fof(f9185,plain,(
% 72.72/9.75 ~ssItem(hd(sk2))|sQ523_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f9183])).
% 72.72/9.75 fof(f9253,plain,(
% 72.72/9.75 ~ssList(sk2)|nil=sk2|sQ523_spl),
% 72.72/9.75 inference(resolution,[status(thm)],[f9185,f276])).
% 72.72/9.75 fof(f9254,plain,(
% 72.72/9.75 ~sQ13_spl|sQ14_spl|sQ523_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f9253,f612,f615,f9183])).
% 72.72/9.75 fof(f9272,plain,(
% 72.72/9.75 ![X0]: (~cons(hd(sk2),X0)=X0|~ssList(X0)|~sQ523_spl)),
% 72.72/9.75 inference(resolution,[status(thm)],[f9184,f299])).
% 72.72/9.75 fof(f9944,definition,(
% 72.72/9.75 sQ552_spl <=> (nil=cons(skac2,sk2))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ552_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f9945,plain,(
% 72.72/9.75 nil=cons(skac2,sk2)|~sQ552_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f9944])).
% 72.72/9.75 fof(f11009,plain,(
% 72.72/9.75 ![X0]: (~cons(skac2,X0)=nil|~ssList(X0))),
% 72.72/9.75 inference(resolution,[status(thm)],[f297,f207])).
% 72.72/9.75 fof(f11206,definition,(
% 72.72/9.75 sQ579_spl <=> (ssList(skaf82(sk2)))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ579_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f11208,plain,(
% 72.72/9.75 ~ssList(skaf82(sk2))|sQ579_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f11206])).
% 72.72/9.75 fof(f11209,definition,(
% 72.72/9.75 sQ580_spl <=> (ssItem(skaf83(sk2)))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f11211,plain,(
% 72.72/9.75 ~ssItem(skaf83(sk2))|sQ580_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f11209])).
% 72.72/9.75 fof(f11303,plain,(
% 72.72/9.75 $false|sQ580_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f11211,f209])).
% 72.72/9.75 fof(f11304,plain,(
% 72.72/9.75 sQ580_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f11303])).
% 72.72/9.75 fof(f11305,plain,(
% 72.72/9.75 $false|sQ579_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f11208,f210])).
% 72.72/9.75 fof(f11306,plain,(
% 72.72/9.75 sQ579_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f11305])).
% 72.72/9.75 fof(f15777,definition,(
% 72.72/9.75 sQ684_spl <=> (ssList(skaf82(tl(sk2))))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ684_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f15779,plain,(
% 72.72/9.75 ~ssList(skaf82(tl(sk2)))|sQ684_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f15777])).
% 72.72/9.75 fof(f15788,plain,(
% 72.72/9.75 $false|sQ684_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f15779,f210])).
% 72.72/9.75 fof(f15789,plain,(
% 72.72/9.75 sQ684_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f15788])).
% 72.72/9.75 fof(f18952,definition,(
% 72.72/9.75 sQ844_spl <=> (ssItem(skac3))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ844_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f18954,plain,(
% 72.72/9.75 ~ssItem(skac3)|sQ844_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f18952])).
% 72.72/9.75 fof(f18956,definition,(
% 72.72/9.75 sQ845_spl <=> (ssItem(skac2))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ845_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f18958,plain,(
% 72.72/9.75 ~ssItem(skac2)|sQ845_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f18956])).
% 72.72/9.75 fof(f19973,plain,(
% 72.72/9.75 $false|sQ845_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f18958,f207])).
% 72.72/9.75 fof(f19974,plain,(
% 72.72/9.75 sQ845_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f19973])).
% 72.72/9.75 fof(f20216,definition,(
% 72.72/9.75 sQ855_spl <=> (nil=cons(skac2,nil))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ855_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f20217,plain,(
% 72.72/9.75 nil=cons(skac2,nil)|~sQ855_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f20216])).
% 72.72/9.75 fof(f20278,plain,(
% 72.72/9.75 $false|~sQ855_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f20217,f7785])).
% 72.72/9.75 fof(f20279,plain,(
% 72.72/9.75 ~sQ855_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f20278])).
% 72.72/9.75 fof(f20347,plain,(
% 72.72/9.75 $false|sQ844_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f18954,f206])).
% 72.72/9.75 fof(f20348,plain,(
% 72.72/9.75 sQ844_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f20347])).
% 72.72/9.75 fof(f20586,definition,(
% 72.72/9.75 sQ879_spl <=> (nil=cons(skac3,nil))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ879_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f20587,plain,(
% 72.72/9.75 nil=cons(skac3,nil)|~sQ879_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f20586])).
% 72.72/9.75 fof(f20648,plain,(
% 72.72/9.75 $false|~sQ879_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f20587,f7825])).
% 72.72/9.75 fof(f20649,plain,(
% 72.72/9.75 ~sQ879_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f20648])).
% 72.72/9.75 fof(f20811,plain,(
% 72.72/9.75 ~cons(skac2,sk2)=nil),
% 72.72/9.75 inference(resolution,[status(thm)],[f11009,f429])).
% 72.72/9.75 fof(f22551,plain,(
% 72.72/9.75 ~cons(hd(sk2),sk2)=sk2|~sQ523_spl),
% 72.72/9.75 inference(resolution,[status(thm)],[f9272,f429])).
% 72.72/9.75 fof(f22942,plain,(
% 72.72/9.75 $false|~sQ552_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f9945,f20811])).
% 72.72/9.75 fof(f22943,plain,(
% 72.72/9.75 ~sQ552_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f22942])).
% 72.72/9.75 fof(f25255,definition,(
% 72.72/9.75 ![X0]: (sQ958_spl <=> (skaf83(sk2)=X0))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ958_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f25256,plain,(
% 72.72/9.75 ![X0]: (skaf83(sk2)=X0|~sQ958_spl)),
% 72.72/9.75 inference(component_clause,[status(thm)],[f25255])).
% 72.72/9.75 fof(f29010,definition,(
% 72.72/9.75 ![X0]: (sQ963_spl <=> (hd(sk2)=X0))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ963_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f29011,plain,(
% 72.72/9.75 ![X0]: (hd(sk2)=X0|~sQ963_spl)),
% 72.72/9.75 inference(component_clause,[status(thm)],[f29010])).
% 72.72/9.75 fof(f29389,plain,(
% 72.72/9.75 ~ssList(tl(sk2))|segmentP(sk2,sk3)|~sQ50_spl|~sQ10_spl),
% 72.72/9.75 inference(paramodulation,[status(thm)],[f599,f1401])).
% 72.72/9.75 fof(f29410,definition,(
% 72.72/9.75 sQ975_spl <=> (segmentP(sk2,sk3))),
% 72.72/9.75 introduced(definition,[new_symbols(definition,[sQ975_spl])],[split_symbol_definition])).
% 72.72/9.75 fof(f29411,plain,(
% 72.72/9.75 segmentP(sk2,sk3)|~sQ975_spl),
% 72.72/9.75 inference(component_clause,[status(thm)],[f29410])).
% 72.72/9.75 fof(f29413,plain,(
% 72.72/9.75 ~sQ11_spl|sQ975_spl|~sQ50_spl|~sQ10_spl),
% 72.72/9.75 inference(split_clause,[status(thm)],[f29389,f601,f29410,f1392,f598])).
% 72.72/9.75 fof(f29418,plain,(
% 72.72/9.75 $false|sQ7_spl|~sQ975_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f29411,f610])).
% 72.72/9.75 fof(f29419,plain,(
% 72.72/9.75 sQ7_spl|~sQ975_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f29418])).
% 72.72/9.75 fof(f29506,plain,(
% 72.72/9.75 $false|sQ501_spl|~sQ21_spl),
% 72.72/9.75 inference(forward_subsumption_resolution,[status(thm)],[f2027,f8757])).
% 72.72/9.75 fof(f29507,plain,(
% 72.72/9.75 sQ501_spl|~sQ21_spl),
% 72.72/9.75 inference(contradiction_clause,[status(thm)],[f29506])).
% 72.72/9.75 fof(f29763,plain,(
% 72.72/9.75 ![X0,X1]: (X0=X1|~sQ958_spl)),
% 72.72/9.75 inference(paramodulation,[status(thm)],[f25256,f25256])).
% 72.72/9.75 fof(f29766,plain,(
% 72.72/9.75 $false|~sQ958_spl),
% 72.72/9.75 inference(backward_subsumption_resolution,[status(thm)],[f7822,f29763])).
% 72.72/9.75 fof(f29792,plain,(
% 72.72/9.75 ~sQ958_spl),
% 72.72/9.81 inference(contradiction_clause,[status(thm)],[f29766])).
% 72.72/9.81 fof(f29868,plain,(
% 72.72/9.81 ![X0,X1]: (X0=X1|~sQ963_spl)),
% 72.72/9.81 inference(paramodulation,[status(thm)],[f29011,f29011])).
% 72.72/9.81 fof(f29869,plain,(
% 72.72/9.81 $false|~sQ963_spl),
% 72.72/9.81 inference(backward_subsumption_resolution,[status(thm)],[f251,f29868])).
% 72.72/9.81 fof(f29871,plain,(
% 72.72/9.81 ~sQ963_spl),
% 72.72/9.81 inference(contradiction_clause,[status(thm)],[f29869])).
% 72.72/9.81 fof(f34896,plain,(
% 72.72/9.81 ~sk2=sk2|~sQ346_spl|~sQ53_spl|~sQ523_spl),
% 72.72/9.81 inference(forward_demodulation,[status(thm)],[f9160,f22551])).
% 72.72/9.81 fof(f34897,plain,(
% 72.72/9.81 $false|~sQ346_spl|~sQ53_spl|~sQ523_spl),
% 72.72/9.81 inference(trivial_equality_resolution,[status(thm)],[f34896])).
% 72.72/9.81 fof(f34898,plain,(
% 72.72/9.81 ~sQ346_spl|~sQ53_spl|~sQ523_spl),
% 72.72/9.81 inference(contradiction_clause,[status(thm)],[f34897])).
% 72.72/9.81 fof(f34899,plain,(
% 72.72/9.81 $false),
% 72.72/9.81 inference(sat_refutation,[status(thm)],[f452,f471,f472,f506,f549,f604,f608,f618,f620,f975,f1164,f1178,f1246,f1395,f1445,f8758,f9254,f11304,f11306,f15789,f19974,f20279,f20348,f20649,f22943,f29413,f29419,f29507,f29792,f29871,f34898])).
% 72.72/9.81 % SZS output end CNFRefutation for theBenchmark.p
% 6.94/9.83 % Elapsed time: 9.454602 seconds
% 6.94/9.83 % CPU time: 74.398652 seconds
% 6.94/9.83 % Total memory used: 608.161 MB
% 6.94/9.83 % Net memory used: 573.423 MB
%------------------------------------------------------------------------------