%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC092-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 : n005.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:33 PM UTC 2026
% Result : Unsatisfiable 10.32s 1.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC092-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.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 07:55:02 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 10.32/1.80 % Refutation found
% 10.32/1.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.32/1.80 % SZS output start CNFRefutation for theBenchmark
% 10.32/1.80 fof(f8,axiom,(
% 10.32/1.80 ssList(nil) ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f56,axiom,(
% 10.32/1.80 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f57,axiom,(
% 10.32/1.80 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f73,axiom,(
% 10.32/1.80 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f74,axiom,(
% 10.32/1.80 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f85,axiom,(
% 10.32/1.80 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f100,axiom,(
% 10.32/1.80 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f173,axiom,(
% 10.32/1.80 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f186,negated_conjecture,(
% 10.32/1.80 ssList(sk1) ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f187,negated_conjecture,(
% 10.32/1.80 ssList(sk2) ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f190,negated_conjecture,(
% 10.32/1.80 sk2 = sk4 ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f191,negated_conjecture,(
% 10.32/1.80 sk1 = sk3 ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f192,negated_conjecture,(
% 10.32/1.80 neq(sk2,nil) ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f193,negated_conjecture,(
% 10.32/1.80 (![A]: (( ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f194,negated_conjecture,(
% 10.32/1.80 ssList(sk5) ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f195,negated_conjecture,(
% 10.32/1.80 app(sk3,sk5) = sk4 ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f198,negated_conjecture,(
% 10.32/1.80 ( nil = sk4| nil != sk3 ) ),
% 10.32/1.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.32/1.80 fof(f206,plain,(
% 10.32/1.80 ssList(nil)),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f8])).
% 10.32/1.80 fof(f254,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f56])).
% 10.32/1.80 fof(f255,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f57])).
% 10.32/1.80 fof(f272,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f73])).
% 10.32/1.80 fof(f273,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f74])).
% 10.32/1.80 fof(f284,plain,(
% 10.32/1.80 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f85])).
% 10.32/1.80 fof(f301,plain,(
% 10.32/1.80 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f100])).
% 10.32/1.80 fof(f404,plain,(
% 10.32/1.80 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 10.32/1.80 inference(miniscoping,[status(thm)],[f173])).
% 10.32/1.80 fof(f405,plain,(
% 10.32/1.80 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f404])).
% 10.32/1.80 fof(f429,plain,(
% 10.32/1.80 ssList(sk1)),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f186])).
% 10.32/1.80 fof(f430,plain,(
% 10.32/1.80 ssList(sk2)),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f187])).
% 10.32/1.80 fof(f433,plain,(
% 10.32/1.80 sk2=sk4),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f190])).
% 10.32/1.80 fof(f434,plain,(
% 10.32/1.80 sk1=sk3),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f191])).
% 10.32/1.80 fof(f435,plain,(
% 10.32/1.80 neq(sk2,nil)),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f192])).
% 10.32/1.80 fof(f436,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f193])).
% 10.32/1.80 fof(f437,plain,(
% 10.32/1.80 ssList(sk5)),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f194])).
% 10.32/1.80 fof(f438,plain,(
% 10.32/1.80 app(sk3,sk5)=sk4),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f195])).
% 10.32/1.80 fof(f442,plain,(
% 10.32/1.80 nil=sk4|~nil=sk3),
% 10.32/1.80 inference(cnf_transformation,[status(thm)],[f198])).
% 10.32/1.80 fof(f450,definition,(
% 10.32/1.80 sQ2_spl <=> (nil=sk4)),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f451,plain,(
% 10.32/1.80 nil=sk4|~sQ2_spl),
% 10.32/1.80 inference(component_clause,[status(thm)],[f450])).
% 10.32/1.80 fof(f453,definition,(
% 10.32/1.80 sQ3_spl <=> (nil=sk3)),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f455,plain,(
% 10.32/1.80 ~nil=sk3|sQ3_spl),
% 10.32/1.80 inference(component_clause,[status(thm)],[f453])).
% 10.32/1.80 fof(f456,plain,(
% 10.32/1.80 sQ2_spl|~sQ3_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f442,f450,f453])).
% 10.32/1.80 fof(f475,plain,(
% 10.32/1.80 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 10.32/1.80 inference(destructive_equality_resolution,[status(thm)],[f405])).
% 10.32/1.80 fof(f486,plain,(
% 10.32/1.80 app(sk3,sk5)=sk2),
% 10.32/1.80 inference(backward_demodulation,[status(thm)],[f433,f438])).
% 10.32/1.80 fof(f493,plain,(
% 10.32/1.80 app(sk5,nil)=sk5),
% 10.32/1.80 inference(resolution,[status(thm)],[f272,f437])).
% 10.32/1.80 fof(f497,plain,(
% 10.32/1.80 app(sk1,nil)=sk1),
% 10.32/1.80 inference(resolution,[status(thm)],[f272,f429])).
% 10.32/1.80 fof(f511,plain,(
% 10.32/1.80 app(sk1,sk5)=sk2),
% 10.32/1.80 inference(backward_demodulation,[status(thm)],[f434,f486])).
% 10.32/1.80 fof(f524,plain,(
% 10.32/1.80 app(nil,sk1)=sk1),
% 10.32/1.80 inference(resolution,[status(thm)],[f273,f429])).
% 10.32/1.80 fof(f531,plain,(
% 10.32/1.80 sk2=nil|~sQ2_spl),
% 10.32/1.80 inference(backward_demodulation,[status(thm)],[f451,f433])).
% 10.32/1.80 fof(f532,plain,(
% 10.32/1.80 ~ssList(sk2)|~segmentP(sk2,sk2)|~segmentP(sk1,sk2)),
% 10.32/1.80 inference(resolution,[status(thm)],[f436,f435])).
% 10.32/1.80 fof(f533,definition,(
% 10.32/1.80 sQ4_spl <=> (ssList(sk2))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f536,definition,(
% 10.32/1.80 sQ5_spl <=> (segmentP(sk2,sk2))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f538,plain,(
% 10.32/1.80 ~segmentP(sk2,sk2)|sQ5_spl),
% 10.32/1.80 inference(component_clause,[status(thm)],[f536])).
% 10.32/1.80 fof(f539,definition,(
% 10.32/1.80 sQ6_spl <=> (segmentP(sk1,sk2))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f541,plain,(
% 10.32/1.80 ~segmentP(sk1,sk2)|sQ6_spl),
% 10.32/1.80 inference(component_clause,[status(thm)],[f539])).
% 10.32/1.80 fof(f542,plain,(
% 10.32/1.80 ~sQ4_spl|~sQ5_spl|~sQ6_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f532,f533,f536,f539])).
% 10.32/1.80 fof(f567,definition,(
% 10.32/1.80 sQ7_spl <=> (ssList(nil))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f569,plain,(
% 10.32/1.80 ~ssList(nil)|sQ7_spl),
% 10.32/1.80 inference(component_clause,[status(thm)],[f567])).
% 10.32/1.80 fof(f575,plain,(
% 10.32/1.80 $false|sQ7_spl),
% 10.32/1.80 inference(forward_subsumption_resolution,[status(thm)],[f569,f206])).
% 10.32/1.80 fof(f576,plain,(
% 10.32/1.80 sQ7_spl),
% 10.32/1.80 inference(contradiction_clause,[status(thm)],[f575])).
% 10.32/1.80 fof(f583,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|ssList(app(sk5,X0)))),
% 10.32/1.80 inference(resolution,[status(thm)],[f284,f437])).
% 10.32/1.80 fof(f586,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 10.32/1.80 inference(resolution,[status(thm)],[f284,f429])).
% 10.32/1.80 fof(f593,plain,(
% 10.32/1.80 ~ssList(nil)|ssList(sk5)),
% 10.32/1.80 inference(paramodulation,[status(thm)],[f493,f583])).
% 10.32/1.80 fof(f594,definition,(
% 10.32/1.80 sQ9_spl <=> (ssList(sk5))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f597,plain,(
% 10.32/1.80 ~sQ7_spl|sQ9_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f593,f567,f594])).
% 10.32/1.80 fof(f622,plain,(
% 10.32/1.80 ~ssList(sk2)|sQ5_spl),
% 10.32/1.80 inference(resolution,[status(thm)],[f538,f255])).
% 10.32/1.80 fof(f623,plain,(
% 10.32/1.80 $false|sQ5_spl),
% 10.32/1.80 inference(forward_subsumption_resolution,[status(thm)],[f622,f430])).
% 10.32/1.80 fof(f624,plain,(
% 10.32/1.80 sQ5_spl),
% 10.32/1.80 inference(contradiction_clause,[status(thm)],[f623])).
% 10.32/1.80 fof(f636,definition,(
% 10.32/1.80 sQ10_spl <=> (ssList(sk1))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f649,plain,(
% 10.32/1.80 ~ssList(sk5)|ssList(sk2)),
% 10.32/1.80 inference(paramodulation,[status(thm)],[f511,f586])).
% 10.32/1.80 fof(f650,plain,(
% 10.32/1.80 ~ssList(nil)|ssList(sk1)),
% 10.32/1.80 inference(paramodulation,[status(thm)],[f497,f586])).
% 10.32/1.80 fof(f651,plain,(
% 10.32/1.80 ~sQ9_spl|sQ4_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f649,f594,f533])).
% 10.32/1.80 fof(f652,plain,(
% 10.32/1.80 ~sQ7_spl|sQ10_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f650,f567,f636])).
% 10.32/1.80 fof(f706,plain,(
% 10.32/1.80 ~segmentP(sk1,nil)|~sQ2_spl|sQ6_spl),
% 10.32/1.80 inference(backward_demodulation,[status(thm)],[f531,f541])).
% 10.32/1.80 fof(f719,plain,(
% 10.32/1.80 ~nil=sk1|sQ3_spl),
% 10.32/1.80 inference(forward_demodulation,[status(thm)],[f434,f455])).
% 10.32/1.80 fof(f920,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~ssList(nil)|~ssList(X0)|X0=nil)),
% 10.32/1.80 inference(resolution,[status(thm)],[f436,f301])).
% 10.32/1.80 fof(f922,definition,(
% 10.32/1.80 ![X0]: (sQ16_spl <=> (~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~ssList(X0)|X0=nil))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f923,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|~ssList(X0)|X0=nil|~sQ16_spl)),
% 10.32/1.80 inference(component_clause,[status(thm)],[f922])).
% 10.32/1.80 fof(f925,plain,(
% 10.32/1.80 sQ16_spl|~sQ7_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f920,f922,f567])).
% 10.32/1.80 fof(f926,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0)|X0=nil|~sQ16_spl)),
% 10.32/1.80 inference(duplicate_literals_removal,[status(thm)],[f923])).
% 10.32/1.80 fof(f974,definition,(
% 10.32/1.80 sQ23_spl <=> (nil=sk1)),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f975,plain,(
% 10.32/1.80 nil=sk1|~sQ23_spl),
% 10.32/1.80 inference(component_clause,[status(thm)],[f974])).
% 10.32/1.80 fof(f2201,plain,(
% 10.32/1.80 $false|sQ3_spl|~sQ23_spl),
% 10.32/1.80 inference(forward_subsumption_resolution,[status(thm)],[f975,f719])).
% 10.32/1.80 fof(f2202,plain,(
% 10.32/1.80 sQ3_spl|~sQ23_spl),
% 10.32/1.80 inference(contradiction_clause,[status(thm)],[f2201])).
% 10.32/1.80 fof(f2453,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|~ssList(nil)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1))),
% 10.32/1.80 inference(paramodulation,[status(thm)],[f524,f475])).
% 10.32/1.80 fof(f2533,definition,(
% 10.32/1.80 ![X0]: (sQ71_spl <=> (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f2534,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(app(nil,sk1),X0),sk1)|~sQ71_spl)),
% 10.32/1.80 inference(component_clause,[status(thm)],[f2533])).
% 10.32/1.80 fof(f2536,plain,(
% 10.32/1.80 sQ71_spl|~sQ7_spl|~sQ10_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f2453,f2533,f567,f636])).
% 10.32/1.80 fof(f2561,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|~ssList(app(sk1,X0))|segmentP(app(sk1,X0),sk1)|~sQ71_spl)),
% 10.32/1.80 inference(forward_demodulation,[status(thm)],[f524,f2534])).
% 10.32/1.80 fof(f2562,plain,(
% 10.32/1.80 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ71_spl)),
% 10.32/1.80 inference(forward_subsumption_resolution,[status(thm)],[f2561,f586])).
% 10.32/1.80 fof(f2697,plain,(
% 10.32/1.80 ~ssList(sk5)|segmentP(sk2,sk1)|~sQ71_spl),
% 10.32/1.80 inference(paramodulation,[status(thm)],[f511,f2562])).
% 10.32/1.80 fof(f2711,definition,(
% 10.32/1.80 sQ97_spl <=> (segmentP(sk2,sk1))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f2714,plain,(
% 10.32/1.80 ~sQ9_spl|sQ97_spl|~sQ71_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f2697,f594,f2711,f2533])).
% 10.32/1.80 fof(f3097,definition,(
% 10.32/1.80 sQ120_spl <=> (ssList(app(sk5,sk2)))),
% 10.32/1.80 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 10.32/1.80 fof(f3099,plain,(
% 10.32/1.80 ~ssList(app(sk5,sk2))|sQ120_spl),
% 10.32/1.80 inference(component_clause,[status(thm)],[f3097])).
% 10.32/1.80 fof(f3179,plain,(
% 10.32/1.80 ~ssList(sk2)|sQ120_spl),
% 10.32/1.80 inference(resolution,[status(thm)],[f3099,f583])).
% 10.32/1.80 fof(f3180,plain,(
% 10.32/1.80 $false|sQ120_spl),
% 10.32/1.80 inference(forward_subsumption_resolution,[status(thm)],[f3179,f430])).
% 10.32/1.80 fof(f3181,plain,(
% 10.32/1.80 sQ120_spl),
% 10.32/1.80 inference(contradiction_clause,[status(thm)],[f3180])).
% 10.32/1.80 fof(f3383,plain,(
% 10.32/1.80 ~ssList(sk1)|~segmentP(sk2,sk1)|sk1=nil|~ssList(sk1)|~sQ16_spl),
% 10.32/1.80 inference(resolution,[status(thm)],[f926,f255])).
% 10.32/1.80 fof(f3393,plain,(
% 10.32/1.80 ~sQ10_spl|~sQ97_spl|sQ23_spl|~sQ16_spl),
% 10.32/1.80 inference(split_clause,[status(thm)],[f3383,f636,f2711,f974,f922])).
% 10.32/1.80 fof(f3395,plain,(
% 10.32/1.80 ~ssList(sk1)|~sQ2_spl|sQ6_spl),
% 10.32/1.80 inference(resolution,[status(thm)],[f706,f254])).
% 10.32/1.80 fof(f3397,plain,(
% 10.32/1.80 $false|~sQ2_spl|sQ6_spl),
% 10.32/1.80 inference(forward_subsumption_resolution,[status(thm)],[f3395,f429])).
% 10.32/1.80 fof(f3398,plain,(
% 10.32/1.80 ~sQ2_spl|sQ6_spl),
% 10.32/1.80 inference(contradiction_clause,[status(thm)],[f3397])).
% 10.32/1.80 fof(f3399,plain,(
% 5.05/1.82 $false),
% 5.05/1.82 inference(sat_refutation,[status(thm)],[f456,f542,f576,f597,f624,f651,f652,f925,f2202,f2536,f2714,f3181,f3393,f3398])).
% 5.05/1.82 % SZS output end CNFRefutation for theBenchmark.p
% 5.05/1.84 % Elapsed time: 1.472918 seconds
% 5.05/1.84 % CPU time: 11.234288 seconds
% 5.05/1.84 % Total memory used: 221.135 MB
% 5.05/1.84 % Net memory used: 215.745 MB
%------------------------------------------------------------------------------