%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC277-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 : n008.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:02 PM UTC 2026
% Result : Unsatisfiable 0.14s 5.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC277-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.76 % Computer : n008.cluster.edu
% 0.10/5.76 % Model : x86_64 x86_64
% 0.10/5.76 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.76 % Memory : 8046.5625MB
% 0.10/5.76 % OS : Linux 6.8.0-71-generic
% 0.10/5.76 % CPULimit : 300
% 0.10/5.76 % WCLimit : 300
% 0.10/5.76 % DateTime : Mon Sep 21 08:12:02 UTC 2026
% 0.10/5.76 % CPUTime :
% 0.10/5.78 % Drodi V4.1.1
% 0.14/5.87 % Refutation found
% 0.14/5.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/5.87 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.87 fof(f4,axiom,(
% 0.14/5.87 totalorderedP(nil) ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f8,axiom,(
% 0.14/5.87 ssList(nil) ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f47,axiom,(
% 0.14/5.87 (![U]: (ssItem(skaf44(U)) ))),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f56,axiom,(
% 0.14/5.87 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f67,axiom,(
% 0.14/5.87 (![U]: (( ~ ssItem(U)| totalorderedP(cons(U,nil)) ) ))),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f73,axiom,(
% 0.14/5.87 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f100,axiom,(
% 0.14/5.87 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f101,axiom,(
% 0.14/5.87 (![U]: (( ~ singletonP(U)| ~ ssList(U)| cons(skaf44(U),nil) = U ) ))),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f127,axiom,(
% 0.14/5.87 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f172,axiom,(
% 0.14/5.87 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f186,negated_conjecture,(
% 0.14/5.87 ssList(sk1) ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f187,negated_conjecture,(
% 0.14/5.87 ssList(sk2) ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f190,negated_conjecture,(
% 0.14/5.87 sk2 = sk4 ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f191,negated_conjecture,(
% 0.14/5.87 sk1 = sk3 ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f192,negated_conjecture,(
% 0.14/5.87 segmentP(sk4,sk3) ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f193,negated_conjecture,(
% 0.14/5.87 ~ totalorderedP(sk1) ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f194,negated_conjecture,(
% 0.14/5.87 ( singletonP(sk3)| ~ neq(sk4,nil) ) ),
% 0.14/5.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.87 fof(f198,plain,(
% 0.14/5.87 totalorderedP(nil)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/5.87 fof(f202,plain,(
% 0.14/5.87 ssList(nil)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/5.87 fof(f241,plain,(
% 0.14/5.87 ![X0]: (ssItem(skaf44(X0)))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f47])).
% 0.14/5.87 fof(f250,plain,(
% 0.14/5.87 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f56])).
% 0.14/5.87 fof(f261,plain,(
% 0.14/5.87 ![X0]: (~ssItem(X0)|totalorderedP(cons(X0,nil)))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f67])).
% 0.14/5.87 fof(f268,plain,(
% 0.14/5.87 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/5.87 fof(f297,plain,(
% 0.14/5.87 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f100])).
% 0.14/5.87 fof(f298,plain,(
% 0.14/5.87 ![X0]: (~singletonP(X0)|~ssList(X0)|cons(skaf44(X0),nil)=X0)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f101])).
% 0.14/5.87 fof(f334,plain,(
% 0.14/5.87 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f127])).
% 0.14/5.87 fof(f399,plain,(
% 0.14/5.87 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f172])).
% 0.14/5.87 fof(f425,plain,(
% 0.14/5.87 ssList(sk1)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f186])).
% 0.14/5.87 fof(f426,plain,(
% 0.14/5.87 ssList(sk2)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f187])).
% 0.14/5.87 fof(f429,plain,(
% 0.14/5.87 sk2=sk4),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f190])).
% 0.14/5.87 fof(f430,plain,(
% 0.14/5.87 sk1=sk3),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f191])).
% 0.14/5.87 fof(f431,plain,(
% 0.14/5.87 segmentP(sk4,sk3)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f192])).
% 0.14/5.87 fof(f432,plain,(
% 0.14/5.87 ~totalorderedP(sk1)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f193])).
% 0.14/5.87 fof(f433,plain,(
% 0.14/5.87 singletonP(sk3)|~neq(sk4,nil)),
% 0.14/5.87 inference(cnf_transformation,[status(thm)],[f194])).
% 0.14/5.87 fof(f441,definition,(
% 0.14/5.87 sQ2_spl <=> (singletonP(sk3))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f442,plain,(
% 0.14/5.87 singletonP(sk3)|~sQ2_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f441])).
% 0.14/5.87 fof(f444,definition,(
% 0.14/5.87 sQ3_spl <=> (neq(sk4,nil))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f446,plain,(
% 0.14/5.87 ~neq(sk4,nil)|sQ3_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f444])).
% 0.14/5.87 fof(f447,plain,(
% 0.14/5.87 sQ2_spl|~sQ3_spl),
% 0.14/5.87 inference(split_clause,[status(thm)],[f433,f441,f444])).
% 0.14/5.87 fof(f479,plain,(
% 0.14/5.87 singletonP(sk1)|~sQ2_spl),
% 0.14/5.87 inference(forward_demodulation,[status(thm)],[f430,f442])).
% 0.14/5.87 fof(f480,plain,(
% 0.14/5.87 segmentP(sk2,sk3)),
% 0.14/5.87 inference(forward_demodulation,[status(thm)],[f429,f431])).
% 0.14/5.87 fof(f481,plain,(
% 0.14/5.87 segmentP(sk2,sk1)),
% 0.14/5.87 inference(forward_demodulation,[status(thm)],[f430,f480])).
% 0.14/5.87 fof(f484,definition,(
% 0.14/5.87 sQ4_spl <=> (ssList(nil))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f486,plain,(
% 0.14/5.87 ~ssList(nil)|sQ4_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f484])).
% 0.14/5.87 fof(f492,plain,(
% 0.14/5.87 $false|sQ4_spl),
% 0.14/5.87 inference(forward_subsumption_resolution,[status(thm)],[f486,f202])).
% 0.14/5.87 fof(f493,plain,(
% 0.14/5.87 sQ4_spl),
% 0.14/5.87 inference(contradiction_clause,[status(thm)],[f492])).
% 0.14/5.87 fof(f544,definition,(
% 0.14/5.87 sQ9_spl <=> (ssList(sk1))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f546,plain,(
% 0.14/5.87 ~ssList(sk1)|sQ9_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f544])).
% 0.14/5.87 fof(f547,definition,(
% 0.14/5.87 sQ10_spl <=> (ssList(sk2))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f549,plain,(
% 0.14/5.87 ~ssList(sk2)|sQ10_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f547])).
% 0.14/5.87 fof(f573,plain,(
% 0.14/5.87 $false|sQ10_spl),
% 0.14/5.87 inference(forward_subsumption_resolution,[status(thm)],[f549,f426])).
% 0.14/5.87 fof(f574,plain,(
% 0.14/5.87 sQ10_spl),
% 0.14/5.87 inference(contradiction_clause,[status(thm)],[f573])).
% 0.14/5.87 fof(f595,plain,(
% 0.14/5.87 $false|sQ9_spl),
% 0.14/5.87 inference(forward_subsumption_resolution,[status(thm)],[f546,f425])).
% 0.14/5.87 fof(f596,plain,(
% 0.14/5.87 sQ9_spl),
% 0.14/5.87 inference(contradiction_clause,[status(thm)],[f595])).
% 0.14/5.87 fof(f719,definition,(
% 0.14/5.87 sQ27_spl <=> (nil=sk2)),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f720,plain,(
% 0.14/5.87 nil=sk2|~sQ27_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f719])).
% 0.14/5.87 fof(f749,definition,(
% 0.14/5.87 sQ30_spl <=> (nil=sk1)),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f750,plain,(
% 0.14/5.87 nil=sk1|~sQ30_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f749])).
% 0.14/5.87 fof(f823,plain,(
% 0.14/5.87 app(sk1,nil)=sk1),
% 0.14/5.87 inference(resolution,[status(thm)],[f268,f425])).
% 0.14/5.87 fof(f854,plain,(
% 0.14/5.87 ![X0,X1]: (~segmentP(nil,X0)|~ssList(X1)|~ssList(sk1)|~ssList(X0)|~ssList(nil)|segmentP(app(sk1,X1),X0))),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f823,f399])).
% 0.14/5.87 fof(f859,definition,(
% 0.14/5.87 ![X0,X1]: (sQ34_spl <=> (~segmentP(nil,X0)|~ssList(X1)|~ssList(X0)|segmentP(app(sk1,X1),X0)))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f860,plain,(
% 0.14/5.87 ![X0,X1]: (~segmentP(nil,X0)|~ssList(X1)|~ssList(X0)|segmentP(app(sk1,X1),X0)|~sQ34_spl)),
% 0.14/5.87 inference(component_clause,[status(thm)],[f859])).
% 0.14/5.87 fof(f862,plain,(
% 0.14/5.87 sQ34_spl|~sQ9_spl|~sQ4_spl),
% 0.14/5.87 inference(split_clause,[status(thm)],[f854,f859,f544,f484])).
% 0.14/5.87 fof(f1171,plain,(
% 0.14/5.87 ![X0]: (~ssList(X0)|~ssList(nil)|segmentP(app(sk1,X0),nil)|~ssList(nil)|~sQ34_spl)),
% 0.14/5.87 inference(resolution,[status(thm)],[f860,f250])).
% 0.14/5.87 fof(f1178,definition,(
% 0.14/5.87 ![X0]: (sQ51_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),nil)))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f1179,plain,(
% 0.14/5.87 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),nil)|~sQ51_spl)),
% 0.14/5.87 inference(component_clause,[status(thm)],[f1178])).
% 0.14/5.87 fof(f1181,plain,(
% 0.14/5.87 sQ51_spl|~sQ4_spl|~sQ34_spl),
% 0.14/5.87 inference(split_clause,[status(thm)],[f1171,f1178,f484,f859])).
% 0.14/5.87 fof(f1190,plain,(
% 0.14/5.87 ~ssList(nil)|segmentP(sk1,nil)|~sQ51_spl),
% 0.14/5.87 inference(paramodulation,[status(thm)],[f823,f1179])).
% 0.14/5.87 fof(f1199,definition,(
% 0.14/5.87 sQ55_spl <=> (segmentP(sk1,nil))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f1200,plain,(
% 0.14/5.87 segmentP(sk1,nil)|~sQ55_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f1199])).
% 0.14/5.87 fof(f1202,plain,(
% 0.14/5.87 ~sQ4_spl|sQ55_spl|~sQ51_spl),
% 0.14/5.87 inference(split_clause,[status(thm)],[f1190,f484,f1199,f1178])).
% 0.14/5.87 fof(f1205,plain,(
% 0.14/5.87 ~segmentP(nil,sk1)|~ssList(nil)|~ssList(sk1)|sk1=nil|~sQ55_spl),
% 0.14/5.87 inference(resolution,[status(thm)],[f1200,f334])).
% 0.14/5.87 fof(f1211,definition,(
% 0.14/5.87 sQ57_spl <=> (segmentP(nil,sk1))),
% 0.14/5.87 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/5.87 fof(f1213,plain,(
% 0.14/5.87 ~segmentP(nil,sk1)|sQ57_spl),
% 0.14/5.87 inference(component_clause,[status(thm)],[f1211])).
% 0.14/5.87 fof(f1214,plain,(
% 0.14/5.87 ~sQ57_spl|~sQ4_spl|~sQ9_spl|sQ30_spl|~sQ55_spl),
% 0.14/5.87 inference(split_clause,[status(thm)],[f1205,f1211,f484,f544,f749,f1199])).
% 0.14/5.87 fof(f1328,plain,(
% 0.14/5.87 totalorderedP(sk1)|~sQ30_spl),
% 0.14/5.88 inference(backward_demodulation,[status(thm)],[f750,f198])).
% 0.14/5.88 fof(f1344,plain,(
% 0.14/5.88 ~neq(sk2,nil)|sQ3_spl),
% 0.14/5.88 inference(forward_demodulation,[status(thm)],[f429,f446])).
% 0.14/5.88 fof(f1347,plain,(
% 0.14/5.88 ~ssList(nil)|~ssList(sk2)|sk2=nil|sQ3_spl),
% 0.14/5.88 inference(resolution,[status(thm)],[f1344,f297])).
% 0.14/5.88 fof(f1355,plain,(
% 0.14/5.88 ~sQ4_spl|~sQ10_spl|sQ27_spl|sQ3_spl),
% 0.14/5.88 inference(split_clause,[status(thm)],[f1347,f484,f547,f719,f444])).
% 0.14/5.88 fof(f1378,plain,(
% 0.14/5.88 ~segmentP(sk2,sk1)|~sQ27_spl|sQ57_spl),
% 0.14/5.88 inference(forward_demodulation,[status(thm)],[f720,f1213])).
% 0.14/5.88 fof(f1379,plain,(
% 0.14/5.88 $false|~sQ27_spl|sQ57_spl),
% 0.14/5.88 inference(forward_subsumption_resolution,[status(thm)],[f1378,f481])).
% 0.14/5.88 fof(f1380,plain,(
% 0.14/5.88 ~sQ27_spl|sQ57_spl),
% 0.14/5.88 inference(contradiction_clause,[status(thm)],[f1379])).
% 0.14/5.88 fof(f1381,plain,(
% 0.14/5.88 $false|~sQ30_spl),
% 0.14/5.88 inference(forward_subsumption_resolution,[status(thm)],[f1328,f432])).
% 0.14/5.88 fof(f1382,plain,(
% 0.14/5.88 ~sQ30_spl),
% 0.14/5.88 inference(contradiction_clause,[status(thm)],[f1381])).
% 0.14/5.88 fof(f1694,plain,(
% 0.14/5.88 ~ssList(sk1)|cons(skaf44(sk1),nil)=sk1|~sQ2_spl),
% 0.14/5.88 inference(resolution,[status(thm)],[f298,f479])).
% 0.14/5.88 fof(f1695,definition,(
% 0.14/5.88 sQ76_spl <=> (cons(skaf44(sk1),nil)=sk1)),
% 0.14/5.88 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.14/5.88 fof(f1696,plain,(
% 0.14/5.88 cons(skaf44(sk1),nil)=sk1|~sQ76_spl),
% 0.14/5.88 inference(component_clause,[status(thm)],[f1695])).
% 0.14/5.88 fof(f1698,plain,(
% 0.14/5.88 ~sQ9_spl|sQ76_spl|~sQ2_spl),
% 0.14/5.88 inference(split_clause,[status(thm)],[f1694,f544,f1695,f441])).
% 0.14/5.88 fof(f1744,plain,(
% 0.14/5.88 ~ssItem(skaf44(sk1))|totalorderedP(sk1)|~sQ76_spl),
% 0.14/5.88 inference(paramodulation,[status(thm)],[f1696,f261])).
% 0.14/5.88 fof(f1751,definition,(
% 0.14/5.88 sQ80_spl <=> (ssItem(skaf44(sk1)))),
% 0.14/5.88 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.14/5.88 fof(f1753,plain,(
% 0.14/5.88 ~ssItem(skaf44(sk1))|sQ80_spl),
% 0.14/5.88 inference(component_clause,[status(thm)],[f1751])).
% 0.14/5.88 fof(f1754,definition,(
% 0.14/5.88 sQ81_spl <=> (totalorderedP(sk1))),
% 0.14/5.88 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.14/5.88 fof(f1755,plain,(
% 0.14/5.88 totalorderedP(sk1)|~sQ81_spl),
% 0.14/5.88 inference(component_clause,[status(thm)],[f1754])).
% 0.14/5.88 fof(f1757,plain,(
% 0.14/5.88 ~sQ80_spl|sQ81_spl|~sQ76_spl),
% 0.14/5.88 inference(split_clause,[status(thm)],[f1744,f1751,f1754,f1695])).
% 0.14/5.88 fof(f1776,plain,(
% 0.14/5.88 $false|sQ80_spl),
% 0.14/5.88 inference(forward_subsumption_resolution,[status(thm)],[f1753,f241])).
% 0.14/5.88 fof(f1777,plain,(
% 0.14/5.88 sQ80_spl),
% 0.14/5.88 inference(contradiction_clause,[status(thm)],[f1776])).
% 0.14/5.88 fof(f1781,plain,(
% 0.14/5.88 $false|~sQ81_spl),
% 0.14/5.88 inference(forward_subsumption_resolution,[status(thm)],[f1755,f432])).
% 0.14/5.88 fof(f1782,plain,(
% 0.14/5.88 ~sQ81_spl),
% 0.14/5.88 inference(contradiction_clause,[status(thm)],[f1781])).
% 0.14/5.88 fof(f1783,plain,(
% 0.14/5.88 $false),
% 0.14/5.88 inference(sat_refutation,[status(thm)],[f447,f493,f574,f596,f862,f1181,f1202,f1214,f1355,f1380,f1382,f1698,f1757,f1777,f1782])).
% 0.14/5.88 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.89 % Elapsed time: 0.115086 seconds
% 0.14/5.89 % CPU time: 0.660746 seconds
% 0.14/5.89 % Total memory used: 122.149 MB
% 0.14/5.89 % Net memory used: 121.500 MB
%------------------------------------------------------------------------------