%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC294-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 : 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:42:05 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC294-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/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:13:04 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.49 % Refutation found
% 0.10/0.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.49 fof(f3,axiom,(
% 0.10/0.49 strictorderedP(nil) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f8,axiom,(
% 0.10/0.49 ssList(nil) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f47,axiom,(
% 0.10/0.49 (![U]: (ssItem(skaf44(U)) ))),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f56,axiom,(
% 0.10/0.49 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f66,axiom,(
% 0.10/0.49 (![U]: (( ~ ssItem(U)| strictorderedP(cons(U,nil)) ) ))),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f73,axiom,(
% 0.10/0.49 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f100,axiom,(
% 0.10/0.49 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f101,axiom,(
% 0.10/0.49 (![U]: (( ~ singletonP(U)| ~ ssList(U)| cons(skaf44(U),nil) = U ) ))),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f127,axiom,(
% 0.10/0.49 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f172,axiom,(
% 0.10/0.49 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f186,negated_conjecture,(
% 0.10/0.49 ssList(sk1) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f187,negated_conjecture,(
% 0.10/0.49 ssList(sk2) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f190,negated_conjecture,(
% 0.10/0.49 sk2 = sk4 ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f191,negated_conjecture,(
% 0.10/0.49 sk1 = sk3 ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f192,negated_conjecture,(
% 0.10/0.49 segmentP(sk4,sk3) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f193,negated_conjecture,(
% 0.10/0.49 ~ strictorderedP(sk1) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f194,negated_conjecture,(
% 0.10/0.49 ( singletonP(sk3)| ~ neq(sk4,nil) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f197,plain,(
% 0.10/0.49 strictorderedP(nil)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.49 fof(f202,plain,(
% 0.10/0.49 ssList(nil)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.49 fof(f241,plain,(
% 0.10/0.49 ![X0]: (ssItem(skaf44(X0)))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f47])).
% 0.10/0.49 fof(f250,plain,(
% 0.10/0.49 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f56])).
% 0.10/0.49 fof(f260,plain,(
% 0.10/0.49 ![X0]: (~ssItem(X0)|strictorderedP(cons(X0,nil)))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f66])).
% 0.10/0.49 fof(f268,plain,(
% 0.10/0.49 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f73])).
% 0.10/0.49 fof(f297,plain,(
% 0.10/0.49 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f100])).
% 0.10/0.49 fof(f298,plain,(
% 0.10/0.49 ![X0]: (~singletonP(X0)|~ssList(X0)|cons(skaf44(X0),nil)=X0)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f101])).
% 0.10/0.49 fof(f334,plain,(
% 0.10/0.49 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f127])).
% 0.10/0.49 fof(f399,plain,(
% 0.10/0.49 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f172])).
% 0.10/0.49 fof(f425,plain,(
% 0.10/0.49 ssList(sk1)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f186])).
% 0.10/0.49 fof(f426,plain,(
% 0.10/0.49 ssList(sk2)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f187])).
% 0.10/0.49 fof(f429,plain,(
% 0.10/0.49 sk2=sk4),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f190])).
% 0.10/0.49 fof(f430,plain,(
% 0.10/0.49 sk1=sk3),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f191])).
% 0.10/0.49 fof(f431,plain,(
% 0.10/0.49 segmentP(sk4,sk3)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f192])).
% 0.10/0.49 fof(f432,plain,(
% 0.10/0.49 ~strictorderedP(sk1)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f193])).
% 0.10/0.49 fof(f433,plain,(
% 0.10/0.49 singletonP(sk3)|~neq(sk4,nil)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f194])).
% 0.10/0.49 fof(f441,definition,(
% 0.10/0.49 sQ2_spl <=> (singletonP(sk3))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f442,plain,(
% 0.10/0.49 singletonP(sk3)|~sQ2_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f441])).
% 0.10/0.49 fof(f444,definition,(
% 0.10/0.49 sQ3_spl <=> (neq(sk4,nil))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f446,plain,(
% 0.10/0.49 ~neq(sk4,nil)|sQ3_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f444])).
% 0.10/0.49 fof(f447,plain,(
% 0.10/0.49 sQ2_spl|~sQ3_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f433,f441,f444])).
% 0.10/0.49 fof(f479,plain,(
% 0.10/0.49 singletonP(sk1)|~sQ2_spl),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f430,f442])).
% 0.10/0.49 fof(f480,plain,(
% 0.10/0.49 segmentP(sk2,sk3)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f429,f431])).
% 0.10/0.49 fof(f481,plain,(
% 0.10/0.49 segmentP(sk2,sk1)),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f430,f480])).
% 0.10/0.49 fof(f484,definition,(
% 0.10/0.49 sQ4_spl <=> (ssList(nil))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f486,plain,(
% 0.10/0.49 ~ssList(nil)|sQ4_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f484])).
% 0.10/0.49 fof(f492,plain,(
% 0.10/0.49 $false|sQ4_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f486,f202])).
% 0.10/0.49 fof(f493,plain,(
% 0.10/0.49 sQ4_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f492])).
% 0.10/0.49 fof(f544,definition,(
% 0.10/0.49 sQ9_spl <=> (ssList(sk1))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f546,plain,(
% 0.10/0.49 ~ssList(sk1)|sQ9_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f544])).
% 0.10/0.49 fof(f547,definition,(
% 0.10/0.49 sQ10_spl <=> (ssList(sk2))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f549,plain,(
% 0.10/0.49 ~ssList(sk2)|sQ10_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f547])).
% 0.10/0.49 fof(f573,plain,(
% 0.10/0.49 $false|sQ10_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f549,f426])).
% 0.10/0.49 fof(f574,plain,(
% 0.10/0.49 sQ10_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f573])).
% 0.10/0.49 fof(f595,plain,(
% 0.10/0.49 $false|sQ9_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f546,f425])).
% 0.10/0.49 fof(f596,plain,(
% 0.10/0.49 sQ9_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f595])).
% 0.10/0.49 fof(f719,definition,(
% 0.10/0.49 sQ27_spl <=> (nil=sk2)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f720,plain,(
% 0.10/0.49 nil=sk2|~sQ27_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f719])).
% 0.10/0.49 fof(f749,definition,(
% 0.10/0.49 sQ30_spl <=> (nil=sk1)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f750,plain,(
% 0.10/0.49 nil=sk1|~sQ30_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f749])).
% 0.10/0.49 fof(f823,plain,(
% 0.10/0.49 app(sk1,nil)=sk1),
% 0.10/0.49 inference(resolution,[status(thm)],[f268,f425])).
% 0.10/0.49 fof(f854,plain,(
% 0.10/0.49 ![X0,X1]: (~segmentP(nil,X0)|~ssList(X1)|~ssList(sk1)|~ssList(X0)|~ssList(nil)|segmentP(app(sk1,X1),X0))),
% 0.10/0.49 inference(paramodulation,[status(thm)],[f823,f399])).
% 0.10/0.49 fof(f859,definition,(
% 0.10/0.49 ![X0,X1]: (sQ34_spl <=> (~segmentP(nil,X0)|~ssList(X1)|~ssList(X0)|segmentP(app(sk1,X1),X0)))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f860,plain,(
% 0.10/0.49 ![X0,X1]: (~segmentP(nil,X0)|~ssList(X1)|~ssList(X0)|segmentP(app(sk1,X1),X0)|~sQ34_spl)),
% 0.10/0.49 inference(component_clause,[status(thm)],[f859])).
% 0.10/0.49 fof(f862,plain,(
% 0.10/0.49 sQ34_spl|~sQ9_spl|~sQ4_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f854,f859,f544,f484])).
% 0.10/0.49 fof(f1171,plain,(
% 0.10/0.49 ![X0]: (~ssList(X0)|~ssList(nil)|segmentP(app(sk1,X0),nil)|~ssList(nil)|~sQ34_spl)),
% 0.10/0.49 inference(resolution,[status(thm)],[f860,f250])).
% 0.10/0.49 fof(f1178,definition,(
% 0.10/0.49 ![X0]: (sQ51_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),nil)))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f1179,plain,(
% 0.10/0.49 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),nil)|~sQ51_spl)),
% 0.10/0.49 inference(component_clause,[status(thm)],[f1178])).
% 0.10/0.49 fof(f1181,plain,(
% 0.10/0.49 sQ51_spl|~sQ4_spl|~sQ34_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f1171,f1178,f484,f859])).
% 0.10/0.49 fof(f1190,plain,(
% 0.10/0.49 ~ssList(nil)|segmentP(sk1,nil)|~sQ51_spl),
% 0.10/0.49 inference(paramodulation,[status(thm)],[f823,f1179])).
% 0.10/0.49 fof(f1199,definition,(
% 0.10/0.49 sQ55_spl <=> (segmentP(sk1,nil))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f1200,plain,(
% 0.10/0.49 segmentP(sk1,nil)|~sQ55_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f1199])).
% 0.10/0.49 fof(f1202,plain,(
% 0.10/0.49 ~sQ4_spl|sQ55_spl|~sQ51_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f1190,f484,f1199,f1178])).
% 0.10/0.49 fof(f1205,plain,(
% 0.10/0.49 ~segmentP(nil,sk1)|~ssList(nil)|~ssList(sk1)|sk1=nil|~sQ55_spl),
% 0.10/0.49 inference(resolution,[status(thm)],[f1200,f334])).
% 0.10/0.49 fof(f1211,definition,(
% 0.10/0.49 sQ57_spl <=> (segmentP(nil,sk1))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f1213,plain,(
% 0.10/0.49 ~segmentP(nil,sk1)|sQ57_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f1211])).
% 0.10/0.49 fof(f1214,plain,(
% 0.10/0.49 ~sQ57_spl|~sQ4_spl|~sQ9_spl|sQ30_spl|~sQ55_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f1205,f1211,f484,f544,f749,f1199])).
% 0.10/0.49 fof(f1328,plain,(
% 0.10/0.49 strictorderedP(sk1)|~sQ30_spl),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f750,f197])).
% 0.10/0.49 fof(f1344,plain,(
% 0.10/0.49 ~neq(sk2,nil)|sQ3_spl),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f429,f446])).
% 0.10/0.49 fof(f1347,plain,(
% 0.10/0.49 ~ssList(nil)|~ssList(sk2)|sk2=nil|sQ3_spl),
% 0.10/0.49 inference(resolution,[status(thm)],[f1344,f297])).
% 0.10/0.49 fof(f1355,plain,(
% 0.10/0.49 ~sQ4_spl|~sQ10_spl|sQ27_spl|sQ3_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f1347,f484,f547,f719,f444])).
% 0.10/0.49 fof(f1373,plain,(
% 0.10/0.49 ~segmentP(sk2,sk1)|~sQ27_spl|sQ57_spl),
% 0.10/0.49 inference(forward_demodulation,[status(thm)],[f720,f1213])).
% 0.10/0.49 fof(f1374,plain,(
% 0.10/0.49 $false|~sQ27_spl|sQ57_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f1373,f481])).
% 0.10/0.49 fof(f1375,plain,(
% 0.10/0.49 ~sQ27_spl|sQ57_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f1374])).
% 0.10/0.49 fof(f1376,plain,(
% 0.10/0.49 $false|~sQ30_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f1328,f432])).
% 0.10/0.49 fof(f1377,plain,(
% 0.10/0.49 ~sQ30_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f1376])).
% 0.10/0.49 fof(f1687,plain,(
% 0.10/0.49 ~ssList(sk1)|cons(skaf44(sk1),nil)=sk1|~sQ2_spl),
% 0.10/0.49 inference(resolution,[status(thm)],[f298,f479])).
% 0.10/0.49 fof(f1688,definition,(
% 0.10/0.49 sQ75_spl <=> (cons(skaf44(sk1),nil)=sk1)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f1689,plain,(
% 0.10/0.49 cons(skaf44(sk1),nil)=sk1|~sQ75_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f1688])).
% 0.10/0.49 fof(f1691,plain,(
% 0.10/0.49 ~sQ9_spl|sQ75_spl|~sQ2_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f1687,f544,f1688,f441])).
% 0.10/0.49 fof(f1737,plain,(
% 0.10/0.49 ~ssItem(skaf44(sk1))|strictorderedP(sk1)|~sQ75_spl),
% 0.10/0.49 inference(paramodulation,[status(thm)],[f1689,f260])).
% 0.10/0.49 fof(f1744,definition,(
% 0.10/0.49 sQ79_spl <=> (ssItem(skaf44(sk1)))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f1746,plain,(
% 0.10/0.49 ~ssItem(skaf44(sk1))|sQ79_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f1744])).
% 0.10/0.49 fof(f1747,definition,(
% 0.10/0.49 sQ80_spl <=> (strictorderedP(sk1))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f1748,plain,(
% 0.10/0.49 strictorderedP(sk1)|~sQ80_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f1747])).
% 0.10/0.49 fof(f1750,plain,(
% 0.10/0.49 ~sQ79_spl|sQ80_spl|~sQ75_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f1737,f1744,f1747,f1688])).
% 0.10/0.49 fof(f1769,plain,(
% 0.10/0.49 $false|sQ79_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f1746,f241])).
% 0.10/0.49 fof(f1770,plain,(
% 0.10/0.49 sQ79_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f1769])).
% 0.10/0.49 fof(f1774,plain,(
% 0.10/0.49 $false|~sQ80_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f1748,f432])).
% 0.10/0.49 fof(f1775,plain,(
% 0.10/0.49 ~sQ80_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f1774])).
% 0.10/0.49 fof(f1776,plain,(
% 0.10/0.49 $false),
% 0.10/0.49 inference(sat_refutation,[status(thm)],[f447,f493,f574,f596,f862,f1181,f1202,f1214,f1355,f1375,f1377,f1691,f1750,f1770,f1775])).
% 0.10/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.51 % Elapsed time: 0.129951 seconds
% 0.10/0.51 % CPU time: 0.757016 seconds
% 0.10/0.51 % Total memory used: 124.036 MB
% 0.10/0.51 % Net memory used: 123.348 MB
%------------------------------------------------------------------------------