%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC348-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 : n003.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:13 PM UTC 2026
% Result : Unsatisfiable 0.29s 0.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC348-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n003.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 08:19:31 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.50 % Drodi V4.1.1
% 0.29/0.78 % Refutation found
% 0.29/0.78 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.29/0.78 % SZS output start CNFRefutation for theBenchmark
% 0.29/0.78 fof(f3,axiom,(
% 0.29/0.78 strictorderedP(nil) ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f8,axiom,(
% 0.29/0.78 ssList(nil) ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f47,axiom,(
% 0.29/0.78 (![U]: (ssItem(skaf44(U)) ))),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f56,axiom,(
% 0.29/0.78 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f66,axiom,(
% 0.29/0.78 (![U]: (( ~ ssItem(U)| strictorderedP(cons(U,nil)) ) ))),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f73,axiom,(
% 0.29/0.78 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f100,axiom,(
% 0.29/0.78 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f101,axiom,(
% 0.29/0.78 (![U]: (( ~ singletonP(U)| ~ ssList(U)| cons(skaf44(U),nil) = U ) ))),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f127,axiom,(
% 0.29/0.78 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f172,axiom,(
% 0.29/0.78 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f186,negated_conjecture,(
% 0.29/0.78 ssList(sk1) ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f187,negated_conjecture,(
% 0.29/0.78 ssList(sk2) ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f190,negated_conjecture,(
% 0.29/0.78 sk2 = sk4 ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f191,negated_conjecture,(
% 0.29/0.78 sk1 = sk3 ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f192,negated_conjecture,(
% 0.29/0.78 segmentP(sk4,sk3) ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f193,negated_conjecture,(
% 0.29/0.78 ( singletonP(sk3)| ~ neq(sk4,nil) ) ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f194,negated_conjecture,(
% 0.29/0.78 ( ~ segmentP(sk2,sk1)| ~ strictorderedP(sk1) ) ),
% 0.29/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.29/0.78 fof(f197,plain,(
% 0.29/0.78 strictorderedP(nil)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f3])).
% 0.29/0.78 fof(f202,plain,(
% 0.29/0.78 ssList(nil)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f8])).
% 0.29/0.78 fof(f241,plain,(
% 0.29/0.78 ![X0]: (ssItem(skaf44(X0)))),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f47])).
% 0.29/0.78 fof(f250,plain,(
% 0.29/0.78 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f56])).
% 0.29/0.78 fof(f260,plain,(
% 0.29/0.78 ![X0]: (~ssItem(X0)|strictorderedP(cons(X0,nil)))),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f66])).
% 0.29/0.78 fof(f268,plain,(
% 0.29/0.78 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f73])).
% 0.29/0.78 fof(f297,plain,(
% 0.29/0.78 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f100])).
% 0.29/0.78 fof(f298,plain,(
% 0.29/0.78 ![X0]: (~singletonP(X0)|~ssList(X0)|cons(skaf44(X0),nil)=X0)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f101])).
% 0.29/0.78 fof(f334,plain,(
% 0.29/0.78 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f127])).
% 0.29/0.78 fof(f399,plain,(
% 0.29/0.78 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f172])).
% 0.29/0.78 fof(f425,plain,(
% 0.29/0.78 ssList(sk1)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f186])).
% 0.29/0.78 fof(f426,plain,(
% 0.29/0.78 ssList(sk2)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f187])).
% 0.29/0.78 fof(f429,plain,(
% 0.29/0.78 sk2=sk4),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f190])).
% 0.29/0.78 fof(f430,plain,(
% 0.29/0.78 sk1=sk3),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f191])).
% 0.29/0.78 fof(f431,plain,(
% 0.29/0.78 segmentP(sk4,sk3)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f192])).
% 0.29/0.78 fof(f432,plain,(
% 0.29/0.78 singletonP(sk3)|~neq(sk4,nil)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f193])).
% 0.29/0.78 fof(f433,plain,(
% 0.29/0.78 ~segmentP(sk2,sk1)|~strictorderedP(sk1)),
% 0.29/0.78 inference(cnf_transformation,[status(thm)],[f194])).
% 0.29/0.78 fof(f441,definition,(
% 0.29/0.78 sQ2_spl <=> (singletonP(sk3))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f442,plain,(
% 0.29/0.78 singletonP(sk3)|~sQ2_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f441])).
% 0.29/0.78 fof(f444,definition,(
% 0.29/0.78 sQ3_spl <=> (neq(sk4,nil))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f446,plain,(
% 0.29/0.78 ~neq(sk4,nil)|sQ3_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f444])).
% 0.29/0.78 fof(f447,plain,(
% 0.29/0.78 sQ2_spl|~sQ3_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f432,f441,f444])).
% 0.29/0.78 fof(f448,definition,(
% 0.29/0.78 sQ4_spl <=> (segmentP(sk2,sk1))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f450,plain,(
% 0.29/0.78 ~segmentP(sk2,sk1)|sQ4_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f448])).
% 0.29/0.78 fof(f451,definition,(
% 0.29/0.78 sQ5_spl <=> (strictorderedP(sk1))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f453,plain,(
% 0.29/0.78 ~strictorderedP(sk1)|sQ5_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f451])).
% 0.29/0.78 fof(f454,plain,(
% 0.29/0.78 ~sQ4_spl|~sQ5_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f433,f448,f451])).
% 0.29/0.78 fof(f486,plain,(
% 0.29/0.78 singletonP(sk1)|~sQ2_spl),
% 0.29/0.78 inference(forward_demodulation,[status(thm)],[f430,f442])).
% 0.29/0.78 fof(f487,plain,(
% 0.29/0.78 segmentP(sk2,sk3)),
% 0.29/0.78 inference(forward_demodulation,[status(thm)],[f429,f431])).
% 0.29/0.78 fof(f488,plain,(
% 0.29/0.78 segmentP(sk2,sk1)),
% 0.29/0.78 inference(forward_demodulation,[status(thm)],[f430,f487])).
% 0.29/0.78 fof(f489,plain,(
% 0.29/0.78 $false|sQ4_spl),
% 0.29/0.78 inference(forward_subsumption_resolution,[status(thm)],[f450,f488])).
% 0.29/0.78 fof(f490,plain,(
% 0.29/0.78 sQ4_spl),
% 0.29/0.78 inference(contradiction_clause,[status(thm)],[f489])).
% 0.29/0.78 fof(f493,definition,(
% 0.29/0.78 sQ6_spl <=> (ssList(nil))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f495,plain,(
% 0.29/0.78 ~ssList(nil)|sQ6_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f493])).
% 0.29/0.78 fof(f501,plain,(
% 0.29/0.78 $false|sQ6_spl),
% 0.29/0.78 inference(forward_subsumption_resolution,[status(thm)],[f495,f202])).
% 0.29/0.78 fof(f502,plain,(
% 0.29/0.78 sQ6_spl),
% 0.29/0.78 inference(contradiction_clause,[status(thm)],[f501])).
% 0.29/0.78 fof(f553,definition,(
% 0.29/0.78 sQ11_spl <=> (ssList(sk1))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f555,plain,(
% 0.29/0.78 ~ssList(sk1)|sQ11_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f553])).
% 0.29/0.78 fof(f556,definition,(
% 0.29/0.78 sQ12_spl <=> (ssList(sk2))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f558,plain,(
% 0.29/0.78 ~ssList(sk2)|sQ12_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f556])).
% 0.29/0.78 fof(f582,plain,(
% 0.29/0.78 $false|sQ12_spl),
% 0.29/0.78 inference(forward_subsumption_resolution,[status(thm)],[f558,f426])).
% 0.29/0.78 fof(f583,plain,(
% 0.29/0.78 sQ12_spl),
% 0.29/0.78 inference(contradiction_clause,[status(thm)],[f582])).
% 0.29/0.78 fof(f604,plain,(
% 0.29/0.78 $false|sQ11_spl),
% 0.29/0.78 inference(forward_subsumption_resolution,[status(thm)],[f555,f425])).
% 0.29/0.78 fof(f605,plain,(
% 0.29/0.78 sQ11_spl),
% 0.29/0.78 inference(contradiction_clause,[status(thm)],[f604])).
% 0.29/0.78 fof(f725,definition,(
% 0.29/0.78 sQ28_spl <=> (nil=sk2)),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f726,plain,(
% 0.29/0.78 nil=sk2|~sQ28_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f725])).
% 0.29/0.78 fof(f755,definition,(
% 0.29/0.78 sQ31_spl <=> (nil=sk1)),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f756,plain,(
% 0.29/0.78 nil=sk1|~sQ31_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f755])).
% 0.29/0.78 fof(f829,plain,(
% 0.29/0.78 app(sk1,nil)=sk1),
% 0.29/0.78 inference(resolution,[status(thm)],[f268,f425])).
% 0.29/0.78 fof(f860,plain,(
% 0.29/0.78 ![X0,X1]: (~segmentP(nil,X0)|~ssList(X1)|~ssList(sk1)|~ssList(X0)|~ssList(nil)|segmentP(app(sk1,X1),X0))),
% 0.29/0.78 inference(paramodulation,[status(thm)],[f829,f399])).
% 0.29/0.78 fof(f865,definition,(
% 0.29/0.78 ![X0,X1]: (sQ35_spl <=> (~segmentP(nil,X0)|~ssList(X1)|~ssList(X0)|segmentP(app(sk1,X1),X0)))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f866,plain,(
% 0.29/0.78 ![X0,X1]: (~segmentP(nil,X0)|~ssList(X1)|~ssList(X0)|segmentP(app(sk1,X1),X0)|~sQ35_spl)),
% 0.29/0.78 inference(component_clause,[status(thm)],[f865])).
% 0.29/0.78 fof(f868,plain,(
% 0.29/0.78 sQ35_spl|~sQ11_spl|~sQ6_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f860,f865,f553,f493])).
% 0.29/0.78 fof(f1177,plain,(
% 0.29/0.78 ![X0]: (~ssList(X0)|~ssList(nil)|segmentP(app(sk1,X0),nil)|~ssList(nil)|~sQ35_spl)),
% 0.29/0.78 inference(resolution,[status(thm)],[f866,f250])).
% 0.29/0.78 fof(f1184,definition,(
% 0.29/0.78 ![X0]: (sQ52_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),nil)))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f1185,plain,(
% 0.29/0.78 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),nil)|~sQ52_spl)),
% 0.29/0.78 inference(component_clause,[status(thm)],[f1184])).
% 0.29/0.78 fof(f1187,plain,(
% 0.29/0.78 sQ52_spl|~sQ6_spl|~sQ35_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f1177,f1184,f493,f865])).
% 0.29/0.78 fof(f1196,plain,(
% 0.29/0.78 ~ssList(nil)|segmentP(sk1,nil)|~sQ52_spl),
% 0.29/0.78 inference(paramodulation,[status(thm)],[f829,f1185])).
% 0.29/0.78 fof(f1205,definition,(
% 0.29/0.78 sQ56_spl <=> (segmentP(sk1,nil))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f1206,plain,(
% 0.29/0.78 segmentP(sk1,nil)|~sQ56_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f1205])).
% 0.29/0.78 fof(f1208,plain,(
% 0.29/0.78 ~sQ6_spl|sQ56_spl|~sQ52_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f1196,f493,f1205,f1184])).
% 0.29/0.78 fof(f1211,plain,(
% 0.29/0.78 ~segmentP(nil,sk1)|~ssList(nil)|~ssList(sk1)|sk1=nil|~sQ56_spl),
% 0.29/0.78 inference(resolution,[status(thm)],[f1206,f334])).
% 0.29/0.78 fof(f1217,definition,(
% 0.29/0.78 sQ58_spl <=> (segmentP(nil,sk1))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f1219,plain,(
% 0.29/0.78 ~segmentP(nil,sk1)|sQ58_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f1217])).
% 0.29/0.78 fof(f1220,plain,(
% 0.29/0.78 ~sQ58_spl|~sQ6_spl|~sQ11_spl|sQ31_spl|~sQ56_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f1211,f1217,f493,f553,f755,f1205])).
% 0.29/0.78 fof(f1333,plain,(
% 0.29/0.78 strictorderedP(sk1)|~sQ31_spl),
% 0.29/0.78 inference(backward_demodulation,[status(thm)],[f756,f197])).
% 0.29/0.78 fof(f1349,plain,(
% 0.29/0.78 ~neq(sk2,nil)|sQ3_spl),
% 0.29/0.78 inference(forward_demodulation,[status(thm)],[f429,f446])).
% 0.29/0.78 fof(f1352,plain,(
% 0.29/0.78 ~ssList(nil)|~ssList(sk2)|sk2=nil|sQ3_spl),
% 0.29/0.78 inference(resolution,[status(thm)],[f1349,f297])).
% 0.29/0.78 fof(f1360,plain,(
% 0.29/0.78 ~sQ6_spl|~sQ12_spl|sQ28_spl|sQ3_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f1352,f493,f556,f725,f444])).
% 0.29/0.78 fof(f1378,plain,(
% 0.29/0.78 ~segmentP(sk2,sk1)|~sQ28_spl|sQ58_spl),
% 0.29/0.78 inference(forward_demodulation,[status(thm)],[f726,f1219])).
% 0.29/0.78 fof(f1379,plain,(
% 0.29/0.78 $false|~sQ28_spl|sQ58_spl),
% 0.29/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1378,f488])).
% 0.29/0.78 fof(f1380,plain,(
% 0.29/0.78 ~sQ28_spl|sQ58_spl),
% 0.29/0.78 inference(contradiction_clause,[status(thm)],[f1379])).
% 0.29/0.78 fof(f1381,plain,(
% 0.29/0.78 $false|sQ5_spl|~sQ31_spl),
% 0.29/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1333,f453])).
% 0.29/0.78 fof(f1382,plain,(
% 0.29/0.78 sQ5_spl|~sQ31_spl),
% 0.29/0.78 inference(contradiction_clause,[status(thm)],[f1381])).
% 0.29/0.78 fof(f1692,plain,(
% 0.29/0.78 ~ssList(sk1)|cons(skaf44(sk1),nil)=sk1|~sQ2_spl),
% 0.29/0.78 inference(resolution,[status(thm)],[f298,f486])).
% 0.29/0.78 fof(f1693,definition,(
% 0.29/0.78 sQ76_spl <=> (cons(skaf44(sk1),nil)=sk1)),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f1694,plain,(
% 0.29/0.78 cons(skaf44(sk1),nil)=sk1|~sQ76_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f1693])).
% 0.29/0.78 fof(f1696,plain,(
% 0.29/0.78 ~sQ11_spl|sQ76_spl|~sQ2_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f1692,f553,f1693,f441])).
% 0.29/0.78 fof(f1742,plain,(
% 0.29/0.78 ~ssItem(skaf44(sk1))|strictorderedP(sk1)|~sQ76_spl),
% 0.29/0.78 inference(paramodulation,[status(thm)],[f1694,f260])).
% 0.29/0.78 fof(f1749,definition,(
% 0.29/0.78 sQ80_spl <=> (ssItem(skaf44(sk1)))),
% 0.29/0.78 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.29/0.78 fof(f1751,plain,(
% 0.29/0.78 ~ssItem(skaf44(sk1))|sQ80_spl),
% 0.29/0.78 inference(component_clause,[status(thm)],[f1749])).
% 0.29/0.78 fof(f1752,plain,(
% 0.29/0.78 ~sQ80_spl|sQ5_spl|~sQ76_spl),
% 0.29/0.78 inference(split_clause,[status(thm)],[f1742,f1749,f451,f1693])).
% 0.29/0.78 fof(f1771,plain,(
% 0.29/0.78 $false|sQ80_spl),
% 0.29/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1751,f241])).
% 0.29/0.78 fof(f1772,plain,(
% 0.29/0.78 sQ80_spl),
% 0.29/0.78 inference(contradiction_clause,[status(thm)],[f1771])).
% 0.29/0.78 fof(f1773,plain,(
% 0.29/0.80 $false),
% 0.29/0.80 inference(sat_refutation,[status(thm)],[f447,f454,f490,f502,f583,f605,f868,f1187,f1208,f1220,f1360,f1380,f1382,f1696,f1752,f1772])).
% 0.29/0.80 % SZS output end CNFRefutation for theBenchmark.p
% 0.29/0.81 % Elapsed time: 0.331521 seconds
% 0.29/0.81 % CPU time: 2.027415 seconds
% 0.29/0.81 % Total memory used: 139.847 MB
% 0.29/0.81 % Net memory used: 138.678 MB
%------------------------------------------------------------------------------