%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC079-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:31 PM UTC 2026
% Result : Unsatisfiable 196.49s 25.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC079-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n014.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 07:53:49 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.39 % Drodi V4.1.1
% 196.49/25.27 % Refutation found
% 196.49/25.27 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 196.49/25.27 % SZS output start CNFRefutation for theBenchmark
% 196.49/25.27 fof(f8,axiom,(
% 196.49/25.27 ssList(nil) ),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f11,axiom,(
% 196.49/25.27 ~ singletonP(nil) ),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f20,axiom,(
% 196.49/25.27 (![U]: (ssList(skaf75(U)) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f56,axiom,(
% 196.49/25.27 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f73,axiom,(
% 196.49/25.27 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f74,axiom,(
% 196.49/25.27 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f75,axiom,(
% 196.49/25.27 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f76,axiom,(
% 196.49/25.27 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f85,axiom,(
% 196.49/25.27 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f86,axiom,(
% 196.49/25.27 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f97,axiom,(
% 196.49/25.27 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| hd(cons(U,V)) = U ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f100,axiom,(
% 196.49/25.27 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f104,axiom,(
% 196.49/25.27 (![U]: (( ~ ssList(U)| cons(hd(U),tl(U)) = U| nil = U ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f116,axiom,(
% 196.49/25.27 (![U,V]: (( cons(U,nil) != V| ~ ssItem(U)| ~ ssList(V)| singletonP(V) ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f120,axiom,(
% 196.49/25.27 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| app(cons(U,nil),V) = cons(U,V) ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f173,axiom,(
% 196.49/25.27 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f186,negated_conjecture,(
% 196.49/25.27 ssList(sk1) ),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f187,negated_conjecture,(
% 196.49/25.27 ssList(sk2) ),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f190,negated_conjecture,(
% 196.49/25.27 sk2 = sk4 ),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f191,negated_conjecture,(
% 196.49/25.27 sk1 = sk3 ),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f192,negated_conjecture,(
% 196.49/25.27 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f196,negated_conjecture,(
% 196.49/25.27 (![A]: (( ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A)| ~ neq(sk4,nil) ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f197,negated_conjecture,(
% 196.49/25.27 (![A,B]: (( ~ ssList(A)| sk3 = A| ~ ssItem(B)| cons(B,nil) != A| hd(sk4) != B| ~ neq(nil,sk4)| ~ neq(sk4,nil) ) ))),
% 196.49/25.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 196.49/25.27 fof(f205,plain,(
% 196.49/25.27 ssList(nil)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f8])).
% 196.49/25.27 fof(f208,plain,(
% 196.49/25.27 ~singletonP(nil)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f11])).
% 196.49/25.27 fof(f217,plain,(
% 196.49/25.27 ![X0]: (ssList(skaf75(X0)))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f20])).
% 196.49/25.27 fof(f253,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f56])).
% 196.49/25.27 fof(f271,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f73])).
% 196.49/25.27 fof(f272,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f74])).
% 196.49/25.27 fof(f273,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f75])).
% 196.49/25.27 fof(f274,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f76])).
% 196.49/25.27 fof(f283,plain,(
% 196.49/25.27 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f85])).
% 196.49/25.27 fof(f284,plain,(
% 196.49/25.27 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f86])).
% 196.49/25.27 fof(f295,plain,(
% 196.49/25.27 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|hd(cons(X0,X1))=X0)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f97])).
% 196.49/25.27 fof(f300,plain,(
% 196.49/25.27 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f100])).
% 196.49/25.27 fof(f304,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|nil=X0)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f104])).
% 196.49/25.27 fof(f320,plain,(
% 196.49/25.27 ![V]: (((![U]: (~cons(U,nil)=V|~ssItem(U)))|~ssList(V))|singletonP(V))),
% 196.49/25.27 inference(miniscoping,[status(thm)],[f116])).
% 196.49/25.27 fof(f321,plain,(
% 196.49/25.27 ![X0,X1]: (~cons(X0,nil)=X1|~ssItem(X0)|~ssList(X1)|singletonP(X1))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f320])).
% 196.49/25.27 fof(f328,plain,(
% 196.49/25.27 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=cons(X0,X1))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f120])).
% 196.49/25.27 fof(f403,plain,(
% 196.49/25.27 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 196.49/25.27 inference(miniscoping,[status(thm)],[f173])).
% 196.49/25.27 fof(f404,plain,(
% 196.49/25.27 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f403])).
% 196.49/25.27 fof(f428,plain,(
% 196.49/25.27 ssList(sk1)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f186])).
% 196.49/25.27 fof(f429,plain,(
% 196.49/25.27 ssList(sk2)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f187])).
% 196.49/25.27 fof(f432,plain,(
% 196.49/25.27 sk2=sk4),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f190])).
% 196.49/25.27 fof(f433,plain,(
% 196.49/25.27 sk1=sk3),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f191])).
% 196.49/25.27 fof(f434,plain,(
% 196.49/25.27 neq(sk2,nil)|neq(sk2,nil)),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f192])).
% 196.49/25.27 fof(f440,plain,(
% 196.49/25.27 (![A]: (((~ssList(A)|~neq(A,nil))|~segmentP(sk2,A))|~segmentP(sk1,A)))|~neq(sk4,nil)),
% 196.49/25.27 inference(miniscoping,[status(thm)],[f196])).
% 196.49/25.27 fof(f441,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~neq(sk4,nil))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f440])).
% 196.49/25.27 fof(f442,plain,(
% 196.49/25.27 ((![B]: ((![A]: (((~ssList(A)|sk3=A)|~ssItem(B))|~cons(B,nil)=A))|~hd(sk4)=B))|~neq(nil,sk4))|~neq(sk4,nil)),
% 196.49/25.27 inference(miniscoping,[status(thm)],[f197])).
% 196.49/25.27 fof(f443,plain,(
% 196.49/25.27 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~neq(nil,sk4)|~neq(sk4,nil))),
% 196.49/25.27 inference(cnf_transformation,[status(thm)],[f442])).
% 196.49/25.27 fof(f451,definition,(
% 196.49/25.27 sQ2_spl <=> (neq(sk2,nil))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f452,plain,(
% 196.49/25.27 neq(sk2,nil)|~sQ2_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f451])).
% 196.49/25.27 fof(f454,plain,(
% 196.49/25.27 sQ2_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f434,f451])).
% 196.49/25.27 fof(f455,definition,(
% 196.49/25.27 sQ3_spl <=> (neq(sk4,nil))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f457,plain,(
% 196.49/25.27 ~neq(sk4,nil)|sQ3_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f455])).
% 196.49/25.27 fof(f459,definition,(
% 196.49/25.27 ![X0]: (sQ4_spl <=> (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f460,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~sQ4_spl)),
% 196.49/25.27 inference(component_clause,[status(thm)],[f459])).
% 196.49/25.27 fof(f463,definition,(
% 196.49/25.27 ![X0,X1]: (sQ5_spl <=> (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f464,plain,(
% 196.49/25.27 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~sQ5_spl)),
% 196.49/25.27 inference(component_clause,[status(thm)],[f463])).
% 196.49/25.27 fof(f466,definition,(
% 196.49/25.27 sQ6_spl <=> (neq(nil,sk4))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f468,plain,(
% 196.49/25.27 ~neq(nil,sk4)|sQ6_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f466])).
% 196.49/25.27 fof(f470,plain,(
% 196.49/25.27 sQ4_spl|~sQ3_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f441,f459,f455])).
% 196.49/25.27 fof(f471,plain,(
% 196.49/25.27 sQ5_spl|~sQ6_spl|~sQ3_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f443,f463,f466,f455])).
% 196.49/25.27 fof(f481,plain,(
% 196.49/25.27 ![X0]: (~ssItem(X0)|~ssList(cons(X0,nil))|singletonP(cons(X0,nil)))),
% 196.49/25.27 inference(destructive_equality_resolution,[status(thm)],[f321])).
% 196.49/25.27 fof(f490,plain,(
% 196.49/25.27 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 196.49/25.27 inference(destructive_equality_resolution,[status(thm)],[f404])).
% 196.49/25.27 fof(f501,plain,(
% 196.49/25.27 ~neq(sk2,nil)|sQ3_spl),
% 196.49/25.27 inference(backward_demodulation,[status(thm)],[f432,f457])).
% 196.49/25.27 fof(f503,plain,(
% 196.49/25.27 $false|~sQ2_spl|sQ3_spl),
% 196.49/25.27 inference(forward_subsumption_resolution,[status(thm)],[f501,f452])).
% 196.49/25.27 fof(f504,plain,(
% 196.49/25.27 ~sQ2_spl|sQ3_spl),
% 196.49/25.27 inference(contradiction_clause,[status(thm)],[f503])).
% 196.49/25.27 fof(f505,plain,(
% 196.49/25.27 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk2)=X1|~sQ5_spl)),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f432,f464])).
% 196.49/25.27 fof(f506,plain,(
% 196.49/25.27 ~ssList(cons(hd(sk2),nil))|sk3=cons(hd(sk2),nil)|~ssItem(hd(sk2))|~sQ5_spl),
% 196.49/25.27 inference(destructive_equality_resolution,[status(thm)],[f505])).
% 196.49/25.27 fof(f509,plain,(
% 196.49/25.27 ~ssList(sk2)|~segmentP(sk2,sk2)|~segmentP(sk1,sk2)|~sQ4_spl|~sQ2_spl),
% 196.49/25.27 inference(resolution,[status(thm)],[f460,f452])).
% 196.49/25.27 fof(f510,definition,(
% 196.49/25.27 sQ7_spl <=> (ssList(sk2))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f512,plain,(
% 196.49/25.27 ~ssList(sk2)|sQ7_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f510])).
% 196.49/25.27 fof(f513,definition,(
% 196.49/25.27 sQ8_spl <=> (segmentP(sk2,sk2))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f516,definition,(
% 196.49/25.27 sQ9_spl <=> (segmentP(sk1,sk2))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f518,plain,(
% 196.49/25.27 ~segmentP(sk1,sk2)|sQ9_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f516])).
% 196.49/25.27 fof(f519,plain,(
% 196.49/25.27 ~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f509,f510,f513,f516,f459,f451])).
% 196.49/25.27 fof(f520,plain,(
% 196.49/25.27 ~neq(nil,sk2)|sQ6_spl),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f432,f468])).
% 196.49/25.27 fof(f531,plain,(
% 196.49/25.27 ~ssList(cons(hd(sk2),nil))|sk1=cons(hd(sk2),nil)|~ssItem(hd(sk2))|~sQ5_spl),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f433,f506])).
% 196.49/25.27 fof(f538,definition,(
% 196.49/25.27 sQ10_spl <=> (ssList(nil))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f540,plain,(
% 196.49/25.27 ~ssList(nil)|sQ10_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f538])).
% 196.49/25.27 fof(f546,plain,(
% 196.49/25.27 $false|sQ10_spl),
% 196.49/25.27 inference(forward_subsumption_resolution,[status(thm)],[f540,f205])).
% 196.49/25.27 fof(f547,plain,(
% 196.49/25.27 sQ10_spl),
% 196.49/25.27 inference(contradiction_clause,[status(thm)],[f546])).
% 196.49/25.27 fof(f555,plain,(
% 196.49/25.27 app(sk2,nil)=sk2),
% 196.49/25.27 inference(resolution,[status(thm)],[f271,f429])).
% 196.49/25.27 fof(f556,plain,(
% 196.49/25.27 app(sk1,nil)=sk1),
% 196.49/25.27 inference(resolution,[status(thm)],[f271,f428])).
% 196.49/25.27 fof(f564,plain,(
% 196.49/25.27 app(nil,sk2)=sk2),
% 196.49/25.27 inference(resolution,[status(thm)],[f272,f429])).
% 196.49/25.27 fof(f565,plain,(
% 196.49/25.27 app(nil,sk1)=sk1),
% 196.49/25.27 inference(resolution,[status(thm)],[f272,f428])).
% 196.49/25.27 fof(f576,plain,(
% 196.49/25.27 ~ssList(sk2)|~ssList(nil)|nil=sk2|sQ6_spl),
% 196.49/25.27 inference(resolution,[status(thm)],[f300,f520])).
% 196.49/25.27 fof(f577,plain,(
% 196.49/25.27 ![X0]: (~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~sQ4_spl)),
% 196.49/25.27 inference(resolution,[status(thm)],[f300,f460])).
% 196.49/25.27 fof(f579,definition,(
% 196.49/25.27 sQ12_spl <=> (nil=sk2)),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f580,plain,(
% 196.49/25.27 nil=sk2|~sQ12_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f579])).
% 196.49/25.27 fof(f582,plain,(
% 196.49/25.27 ~sQ7_spl|~sQ10_spl|sQ12_spl|sQ6_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f576,f510,f538,f579,f466])).
% 196.49/25.27 fof(f583,definition,(
% 196.49/25.27 ![X0]: (sQ13_spl <=> (~ssList(X0)|X0=nil|~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f584,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|X0=nil|~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~sQ13_spl)),
% 196.49/25.27 inference(component_clause,[status(thm)],[f583])).
% 196.49/25.27 fof(f586,plain,(
% 196.49/25.27 ~sQ10_spl|sQ13_spl|~sQ4_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f577,f538,f583,f459])).
% 196.49/25.27 fof(f587,plain,(
% 196.49/25.27 $false|sQ7_spl),
% 196.49/25.27 inference(forward_subsumption_resolution,[status(thm)],[f512,f429])).
% 196.49/25.27 fof(f588,plain,(
% 196.49/25.27 sQ7_spl),
% 196.49/25.27 inference(contradiction_clause,[status(thm)],[f587])).
% 196.49/25.27 fof(f589,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|X0=nil|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~sQ13_spl)),
% 196.49/25.27 inference(duplicate_literals_removal,[status(thm)],[f584])).
% 196.49/25.27 fof(f630,definition,(
% 196.49/25.27 sQ19_spl <=> (nil=sk1)),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f631,plain,(
% 196.49/25.27 nil=sk1|~sQ19_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f630])).
% 196.49/25.27 fof(f665,plain,(
% 196.49/25.27 ~segmentP(sk1,nil)|~sQ12_spl|sQ9_spl),
% 196.49/25.27 inference(backward_demodulation,[status(thm)],[f580,f518])).
% 196.49/25.27 fof(f677,definition,(
% 196.49/25.27 sQ20_spl <=> (ssList(cons(hd(sk2),nil)))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f680,definition,(
% 196.49/25.27 sQ21_spl <=> (sk1=cons(hd(sk2),nil))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f681,plain,(
% 196.49/25.27 sk1=cons(hd(sk2),nil)|~sQ21_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f680])).
% 196.49/25.27 fof(f683,definition,(
% 196.49/25.27 sQ22_spl <=> (ssItem(hd(nil)))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f685,plain,(
% 196.49/25.27 ~ssItem(hd(nil))|sQ22_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f683])).
% 196.49/25.27 fof(f700,plain,(
% 196.49/25.27 ~ssList(sk1)|~sQ12_spl|sQ9_spl),
% 196.49/25.27 inference(resolution,[status(thm)],[f665,f253])).
% 196.49/25.27 fof(f701,plain,(
% 196.49/25.27 $false|~sQ12_spl|sQ9_spl),
% 196.49/25.27 inference(forward_subsumption_resolution,[status(thm)],[f700,f428])).
% 196.49/25.27 fof(f702,plain,(
% 196.49/25.27 ~sQ12_spl|sQ9_spl),
% 196.49/25.27 inference(contradiction_clause,[status(thm)],[f701])).
% 196.49/25.27 fof(f703,definition,(
% 196.49/25.27 sQ25_spl <=> (ssItem(hd(sk2)))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f704,plain,(
% 196.49/25.27 ssItem(hd(sk2))|~sQ25_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f703])).
% 196.49/25.27 fof(f706,plain,(
% 196.49/25.27 ~sQ20_spl|sQ21_spl|~sQ25_spl|~sQ5_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f531,f677,f680,f703,f463])).
% 196.49/25.27 fof(f739,definition,(
% 196.49/25.27 sQ30_spl <=> (ssList(sk1))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f843,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|ssList(app(sk2,X0)))),
% 196.49/25.27 inference(resolution,[status(thm)],[f283,f429])).
% 196.49/25.27 fof(f852,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 196.49/25.27 inference(resolution,[status(thm)],[f283,f428])).
% 196.49/25.27 fof(f894,plain,(
% 196.49/25.27 ~ssList(nil)|ssList(sk1)),
% 196.49/25.27 inference(paramodulation,[status(thm)],[f556,f852])).
% 196.49/25.27 fof(f895,plain,(
% 196.49/25.27 ~sQ10_spl|sQ30_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f894,f538,f739])).
% 196.49/25.27 fof(f1017,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk2)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2))),
% 196.49/25.27 inference(paramodulation,[status(thm)],[f564,f490])).
% 196.49/25.27 fof(f1018,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 196.49/25.27 inference(paramodulation,[status(thm)],[f565,f490])).
% 196.49/25.27 fof(f1028,definition,(
% 196.49/25.27 ![X0]: (sQ42_spl <=> (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2)))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f1029,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(app(nil,sk2),X0),sk2)|~sQ42_spl)),
% 196.49/25.27 inference(component_clause,[status(thm)],[f1028])).
% 196.49/25.27 fof(f1031,plain,(
% 196.49/25.27 sQ42_spl|~sQ10_spl|~sQ7_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f1017,f1028,f538,f510])).
% 196.49/25.27 fof(f1032,definition,(
% 196.49/25.27 ![X0]: (sQ43_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f1033,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)|~sQ43_spl)),
% 196.49/25.27 inference(component_clause,[status(thm)],[f1032])).
% 196.49/25.27 fof(f1035,plain,(
% 196.49/25.27 sQ43_spl|~sQ10_spl|~sQ30_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f1018,f1032,f538,f739])).
% 196.49/25.27 fof(f1041,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(sk1,X0),sk1)|~sQ43_spl)),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f565,f1033])).
% 196.49/25.27 fof(f1042,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ43_spl)),
% 196.49/25.27 inference(forward_subsumption_resolution,[status(thm)],[f1041,f852])).
% 196.49/25.27 fof(f1044,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|~ssList(app(sk2,X0))|segmentP(app(sk2,X0),sk2)|~sQ42_spl)),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f564,f1029])).
% 196.49/25.27 fof(f1045,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),sk2)|~sQ42_spl)),
% 196.49/25.27 inference(forward_subsumption_resolution,[status(thm)],[f1044,f843])).
% 196.49/25.27 fof(f1168,plain,(
% 196.49/25.27 ~ssList(nil)|segmentP(sk1,sk1)|~sQ43_spl),
% 196.49/25.27 inference(paramodulation,[status(thm)],[f556,f1042])).
% 196.49/25.27 fof(f1177,definition,(
% 196.49/25.27 sQ47_spl <=> (segmentP(sk1,sk1))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f1180,plain,(
% 196.49/25.27 ~sQ10_spl|sQ47_spl|~sQ43_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f1168,f538,f1177,f1032])).
% 196.49/25.27 fof(f1197,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|hd(cons(hd(sk2),X0))=hd(sk2)|~sQ25_spl)),
% 196.49/25.27 inference(resolution,[status(thm)],[f704,f295])).
% 196.49/25.27 fof(f1199,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|ssList(cons(hd(sk2),X0))|~sQ25_spl)),
% 196.49/25.27 inference(resolution,[status(thm)],[f704,f284])).
% 196.49/25.27 fof(f1391,plain,(
% 196.49/25.27 ~ssList(nil)|segmentP(sk2,sk2)|~sQ42_spl),
% 196.49/25.27 inference(paramodulation,[status(thm)],[f555,f1045])).
% 196.49/25.27 fof(f1400,plain,(
% 196.49/25.27 ~sQ10_spl|sQ8_spl|~sQ42_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f1391,f538,f513,f1028])).
% 196.49/25.27 fof(f1826,plain,(
% 196.49/25.27 hd(cons(hd(sk2),nil))=hd(sk2)|~sQ25_spl),
% 196.49/25.27 inference(resolution,[status(thm)],[f1197,f205])).
% 196.49/25.27 fof(f1828,plain,(
% 196.49/25.27 hd(sk1)=hd(sk2)|~sQ21_spl|~sQ25_spl),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f681,f1826])).
% 196.49/25.27 fof(f1831,plain,(
% 196.49/25.27 sk1=cons(hd(sk1),nil)|~sQ25_spl|~sQ21_spl),
% 196.49/25.27 inference(backward_demodulation,[status(thm)],[f1828,f681])).
% 196.49/25.27 fof(f1846,plain,(
% 196.49/25.27 ssItem(hd(sk1))|~sQ21_spl|~sQ25_spl),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f1828,f704])).
% 196.49/25.27 fof(f6594,plain,(
% 196.49/25.27 cons(hd(sk2),tl(sk2))=sk2|nil=sk2),
% 196.49/25.27 inference(resolution,[status(thm)],[f304,f429])).
% 196.49/25.27 fof(f6604,definition,(
% 196.49/25.27 sQ124_spl <=> (cons(hd(sk2),tl(sk2))=sk2)),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f6605,plain,(
% 196.49/25.27 cons(hd(sk2),tl(sk2))=sk2|~sQ124_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f6604])).
% 196.49/25.27 fof(f6607,plain,(
% 196.49/25.27 sQ124_spl|sQ12_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f6594,f6604,f579])).
% 196.49/25.27 fof(f6616,plain,(
% 196.49/25.27 cons(hd(sk1),tl(sk2))=sk2|~sQ21_spl|~sQ25_spl|~sQ124_spl),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f1828,f6605])).
% 196.49/25.27 fof(f6696,definition,(
% 196.49/25.27 sQ130_spl <=> (ssList(tl(sk2)))),
% 196.49/25.27 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 196.49/25.27 fof(f6697,plain,(
% 196.49/25.27 ssList(tl(sk2))|~sQ130_spl),
% 196.49/25.27 inference(component_clause,[status(thm)],[f6696])).
% 196.49/25.27 fof(f7235,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|app(cons(hd(sk1),nil),X0)=cons(hd(sk1),X0)|~sQ21_spl|~sQ25_spl)),
% 196.49/25.27 inference(resolution,[status(thm)],[f328,f1846])).
% 196.49/25.27 fof(f7237,plain,(
% 196.49/25.27 ![X0]: (~ssList(X0)|app(sk1,X0)=cons(hd(sk1),X0)|~sQ21_spl|~sQ25_spl)),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f1831,f7235])).
% 196.49/25.27 fof(f14090,plain,(
% 196.49/25.27 ssItem(hd(sk2))|nil=sk2),
% 196.49/25.27 inference(resolution,[status(thm)],[f274,f429])).
% 196.49/25.27 fof(f14101,plain,(
% 196.49/25.27 sQ25_spl|sQ12_spl),
% 196.49/25.27 inference(split_clause,[status(thm)],[f14090,f703,f579])).
% 196.49/25.27 fof(f14248,plain,(
% 196.49/25.27 sk1=cons(hd(nil),nil)|~sQ19_spl|~sQ25_spl|~sQ21_spl),
% 196.49/25.27 inference(backward_demodulation,[status(thm)],[f631,f1831])).
% 196.49/25.27 fof(f14250,plain,(
% 196.49/25.27 ssItem(hd(nil))|~sQ19_spl|~sQ21_spl|~sQ25_spl),
% 196.49/25.27 inference(backward_demodulation,[status(thm)],[f631,f1846])).
% 196.49/25.27 fof(f14300,plain,(
% 196.49/25.27 nil=cons(hd(nil),nil)|~sQ19_spl|~sQ25_spl|~sQ21_spl),
% 196.49/25.27 inference(forward_demodulation,[status(thm)],[f631,f14248])).
% 196.49/25.27 fof(f14698,plain,(
% 196.49/25.27 $false|~sQ19_spl|~sQ21_spl|~sQ25_spl|sQ22_spl),
% 196.49/25.27 inference(forward_subsumption_resolution,[status(thm)],[f685,f14250])).
% 196.49/25.27 fof(f14699,plain,(
% 196.49/25.27 ~sQ19_spl|~sQ21_spl|~sQ25_spl|sQ22_spl),
% 177.30/25.35 inference(contradiction_clause,[status(thm)],[f14698])).
% 177.30/25.35 fof(f15294,plain,(
% 177.30/25.35 ~ssItem(hd(nil))|~ssList(cons(hd(nil),nil))|singletonP(nil)|~sQ19_spl|~sQ25_spl|~sQ21_spl),
% 177.30/25.35 inference(paramodulation,[status(thm)],[f14300,f481])).
% 177.30/25.35 fof(f15295,definition,(
% 177.30/25.35 sQ463_spl <=> (ssList(cons(hd(nil),nil)))),
% 177.30/25.35 introduced(definition,[new_symbols(definition,[sQ463_spl])],[split_symbol_definition])).
% 177.30/25.35 fof(f15297,plain,(
% 177.30/25.35 ~ssList(cons(hd(nil),nil))|sQ463_spl),
% 177.30/25.35 inference(component_clause,[status(thm)],[f15295])).
% 177.30/25.35 fof(f15298,definition,(
% 177.30/25.35 sQ464_spl <=> (singletonP(nil))),
% 177.30/25.35 introduced(definition,[new_symbols(definition,[sQ464_spl])],[split_symbol_definition])).
% 177.30/25.35 fof(f15299,plain,(
% 177.30/25.35 singletonP(nil)|~sQ464_spl),
% 177.30/25.35 inference(component_clause,[status(thm)],[f15298])).
% 177.30/25.35 fof(f15301,plain,(
% 177.30/25.35 ~sQ22_spl|~sQ463_spl|sQ464_spl|~sQ19_spl|~sQ25_spl|~sQ21_spl),
% 177.30/25.35 inference(split_clause,[status(thm)],[f15294,f683,f15295,f15298,f630,f703,f680])).
% 177.30/25.35 fof(f15302,plain,(
% 177.30/25.35 ~ssList(nil)|~sQ19_spl|~sQ25_spl|~sQ21_spl|sQ463_spl),
% 177.30/25.35 inference(forward_demodulation,[status(thm)],[f14300,f15297])).
% 177.30/25.35 fof(f15303,plain,(
% 177.30/25.35 $false|~sQ19_spl|~sQ25_spl|~sQ21_spl|sQ463_spl),
% 177.30/25.35 inference(forward_subsumption_resolution,[status(thm)],[f15302,f205])).
% 177.30/25.35 fof(f15304,plain,(
% 177.30/25.35 ~sQ19_spl|~sQ25_spl|~sQ21_spl|sQ463_spl),
% 177.30/25.35 inference(contradiction_clause,[status(thm)],[f15303])).
% 177.30/25.35 fof(f15305,plain,(
% 177.30/25.35 $false|~sQ464_spl),
% 177.30/25.35 inference(forward_subsumption_resolution,[status(thm)],[f15299,f208])).
% 177.30/25.35 fof(f15306,plain,(
% 177.30/25.35 ~sQ464_spl),
% 177.30/25.35 inference(contradiction_clause,[status(thm)],[f15305])).
% 177.30/25.35 fof(f24549,plain,(
% 177.30/25.35 ssList(tl(sk2))|nil=sk2),
% 177.30/25.35 inference(resolution,[status(thm)],[f273,f429])).
% 177.30/25.35 fof(f24595,plain,(
% 177.30/25.35 sQ130_spl|sQ12_spl),
% 177.30/25.35 inference(split_clause,[status(thm)],[f24549,f6696,f579])).
% 177.30/25.35 fof(f30184,plain,(
% 177.30/25.35 ssList(cons(hd(sk2),nil))|~sQ25_spl),
% 177.30/25.35 inference(resolution,[status(thm)],[f1199,f205])).
% 177.30/25.35 fof(f30187,plain,(
% 177.30/25.35 sQ20_spl|~sQ25_spl),
% 177.30/25.35 inference(split_clause,[status(thm)],[f30184,f677,f703])).
% 177.30/25.35 fof(f30806,definition,(
% 177.30/25.35 ![X0]: (sQ861_spl <=> (~ssList(X0)|~ssList(X0)))),
% 177.30/25.35 introduced(definition,[new_symbols(definition,[sQ861_spl])],[split_symbol_definition])).
% 177.30/25.35 fof(f30807,plain,(
% 177.30/25.35 ![X0]: (~ssList(X0)|~ssList(X0)|~sQ861_spl)),
% 177.30/25.35 inference(component_clause,[status(thm)],[f30806])).
% 177.30/25.35 fof(f30813,plain,(
% 177.30/25.35 ![X0]: (~ssList(X0)|~sQ861_spl)),
% 177.30/25.35 inference(duplicate_literals_removal,[status(thm)],[f30807])).
% 177.30/25.35 fof(f30814,plain,(
% 177.30/25.35 $false|~sQ861_spl),
% 177.30/25.35 inference(backward_subsumption_resolution,[status(thm)],[f217,f30813])).
% 177.30/25.35 fof(f30883,plain,(
% 177.30/25.35 ~sQ861_spl),
% 177.30/25.35 inference(contradiction_clause,[status(thm)],[f30814])).
% 177.30/25.35 fof(f42587,plain,(
% 177.30/25.35 app(sk1,tl(sk2))=cons(hd(sk1),tl(sk2))|~sQ21_spl|~sQ25_spl|~sQ130_spl),
% 177.30/25.35 inference(resolution,[status(thm)],[f7237,f6697])).
% 177.30/25.35 fof(f42661,plain,(
% 177.30/25.35 app(sk1,tl(sk2))=sk2|~sQ124_spl|~sQ21_spl|~sQ25_spl|~sQ130_spl),
% 177.30/25.35 inference(forward_demodulation,[status(thm)],[f6616,f42587])).
% 177.30/25.35 fof(f42690,plain,(
% 177.30/25.35 ~ssList(tl(sk2))|segmentP(sk2,sk1)|~sQ43_spl|~sQ124_spl|~sQ21_spl|~sQ25_spl|~sQ130_spl),
% 177.30/25.35 inference(paramodulation,[status(thm)],[f42661,f1042])).
% 177.30/25.35 fof(f42757,definition,(
% 177.30/25.35 sQ1394_spl <=> (segmentP(sk2,sk1))),
% 177.30/25.35 introduced(definition,[new_symbols(definition,[sQ1394_spl])],[split_symbol_definition])).
% 177.30/25.35 fof(f42758,plain,(
% 177.30/25.35 segmentP(sk2,sk1)|~sQ1394_spl),
% 177.30/25.35 inference(component_clause,[status(thm)],[f42757])).
% 177.30/25.35 fof(f42760,plain,(
% 177.30/25.35 ~sQ130_spl|sQ1394_spl|~sQ43_spl|~sQ124_spl|~sQ21_spl|~sQ25_spl),
% 177.30/25.35 inference(split_clause,[status(thm)],[f42690,f6696,f42757,f1032,f6604,f680,f703])).
% 177.30/25.35 fof(f42773,plain,(
% 177.30/25.35 ~ssList(sk1)|sk1=nil|~segmentP(sk1,sk1)|~sQ1394_spl|~sQ13_spl),
% 177.30/25.35 inference(resolution,[status(thm)],[f42758,f589])).
% 177.30/25.35 fof(f42775,plain,(
% 177.30/25.35 ~sQ30_spl|sQ19_spl|~sQ47_spl|~sQ1394_spl|~sQ13_spl),
% 177.30/25.35 inference(split_clause,[status(thm)],[f42773,f739,f630,f1177,f42757,f583])).
% 177.30/25.35 fof(f42777,plain,(
% 177.30/25.35 $false),
% 177.30/25.35 inference(sat_refutation,[status(thm)],[f454,f470,f471,f504,f519,f547,f582,f586,f588,f702,f706,f895,f1031,f1035,f1180,f1400,f6607,f14101,f14699,f15301,f15304,f15306,f24595,f30187,f30883,f42760,f42775])).
% 177.30/25.35 % SZS output end CNFRefutation for theBenchmark.p
% 11.83/25.44 % Elapsed time: 25.045402 seconds
% 11.83/25.44 % CPU time: 197.963028 seconds
% 11.83/25.44 % Total memory used: 1.259 GB
% 11.83/25.44 % Net memory used: 1.191 GB
%------------------------------------------------------------------------------