%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC090-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:41:33 PM UTC 2026
% Result : Unsatisfiable 9.28s 1.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC090-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.16/0.42 % Computer : n003.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 07:56:30 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 9.28/1.67 % Refutation found
% 9.28/1.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.28/1.67 % SZS output start CNFRefutation for theBenchmark
% 9.28/1.67 fof(f8,axiom,(
% 9.28/1.67 ssList(nil) ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f57,axiom,(
% 9.28/1.67 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f73,axiom,(
% 9.28/1.67 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f74,axiom,(
% 9.28/1.67 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f100,axiom,(
% 9.28/1.67 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f151,axiom,(
% 9.28/1.67 (![U,V,W]: (( app(U,V) != app(W,V)| ~ ssList(U)| ~ ssList(V)| ~ ssList(W)| U = W ) ))),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f172,axiom,(
% 9.28/1.67 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f186,negated_conjecture,(
% 9.28/1.67 ssList(sk1) ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f187,negated_conjecture,(
% 9.28/1.67 ssList(sk2) ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f190,negated_conjecture,(
% 9.28/1.67 sk2 = sk4 ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f191,negated_conjecture,(
% 9.28/1.67 sk1 = sk3 ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f192,negated_conjecture,(
% 9.28/1.67 neq(sk2,nil) ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f193,negated_conjecture,(
% 9.28/1.67 (![A]: (( ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f194,negated_conjecture,(
% 9.28/1.67 ssList(sk5) ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f195,negated_conjecture,(
% 9.28/1.67 ssList(sk6) ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f196,negated_conjecture,(
% 9.28/1.67 app(sk5,sk6) = sk4 ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f197,negated_conjecture,(
% 9.28/1.67 app(sk6,sk5) = sk3 ),
% 9.28/1.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.28/1.67 fof(f205,plain,(
% 9.28/1.67 ssList(nil)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f8])).
% 9.28/1.67 fof(f254,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f57])).
% 9.28/1.67 fof(f271,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f73])).
% 9.28/1.67 fof(f272,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f74])).
% 9.28/1.67 fof(f300,plain,(
% 9.28/1.67 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f100])).
% 9.28/1.67 fof(f369,plain,(
% 9.28/1.67 ![U,W]: (((![V]: ((~app(U,V)=app(W,V)|~ssList(U))|~ssList(V)))|~ssList(W))|U=W)),
% 9.28/1.67 inference(miniscoping,[status(thm)],[f151])).
% 9.28/1.67 fof(f370,plain,(
% 9.28/1.67 ![X0,X1,X2]: (~app(X0,X1)=app(X2,X1)|~ssList(X0)|~ssList(X1)|~ssList(X2)|X0=X2)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f369])).
% 9.28/1.67 fof(f402,plain,(
% 9.28/1.67 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f172])).
% 9.28/1.67 fof(f428,plain,(
% 9.28/1.67 ssList(sk1)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f186])).
% 9.28/1.67 fof(f429,plain,(
% 9.28/1.67 ssList(sk2)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f187])).
% 9.28/1.67 fof(f432,plain,(
% 9.28/1.67 sk2=sk4),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f190])).
% 9.28/1.67 fof(f433,plain,(
% 9.28/1.67 sk1=sk3),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f191])).
% 9.28/1.67 fof(f434,plain,(
% 9.28/1.67 neq(sk2,nil)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f192])).
% 9.28/1.67 fof(f435,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f193])).
% 9.28/1.67 fof(f436,plain,(
% 9.28/1.67 ssList(sk5)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f194])).
% 9.28/1.67 fof(f437,plain,(
% 9.28/1.67 ssList(sk6)),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f195])).
% 9.28/1.67 fof(f438,plain,(
% 9.28/1.67 app(sk5,sk6)=sk4),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f196])).
% 9.28/1.67 fof(f439,plain,(
% 9.28/1.67 app(sk6,sk5)=sk3),
% 9.28/1.67 inference(cnf_transformation,[status(thm)],[f197])).
% 9.28/1.67 fof(f473,plain,(
% 9.28/1.67 app(sk5,sk6)=sk2),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f432,f438])).
% 9.28/1.67 fof(f474,plain,(
% 9.28/1.67 app(sk6,sk5)=sk1),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f433,f439])).
% 9.28/1.67 fof(f475,plain,(
% 9.28/1.67 app(sk2,nil)=sk2),
% 9.28/1.67 inference(resolution,[status(thm)],[f271,f429])).
% 9.28/1.67 fof(f477,plain,(
% 9.28/1.67 app(sk1,nil)=sk1),
% 9.28/1.67 inference(resolution,[status(thm)],[f271,f428])).
% 9.28/1.67 fof(f494,plain,(
% 9.28/1.67 ~ssList(sk2)|~segmentP(sk2,sk2)|~segmentP(sk1,sk2)),
% 9.28/1.67 inference(resolution,[status(thm)],[f435,f434])).
% 9.28/1.67 fof(f495,plain,(
% 9.28/1.67 ~segmentP(sk2,sk2)|~segmentP(sk1,sk2)),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f494,f429])).
% 9.28/1.67 fof(f499,plain,(
% 9.28/1.67 app(nil,sk5)=sk5),
% 9.28/1.67 inference(resolution,[status(thm)],[f436,f272])).
% 9.28/1.67 fof(f500,plain,(
% 9.28/1.67 app(sk5,nil)=sk5),
% 9.28/1.67 inference(resolution,[status(thm)],[f436,f271])).
% 9.28/1.67 fof(f514,plain,(
% 9.28/1.67 ![X0]: (~ssList(nil)|~ssList(X0)|X0=nil|~ssList(X0)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 9.28/1.67 inference(resolution,[status(thm)],[f300,f435])).
% 9.28/1.67 fof(f516,plain,(
% 9.28/1.67 ![X0]: (~ssList(nil)|~ssList(X0)|X0=nil|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 9.28/1.67 inference(duplicate_literals_removal,[status(thm)],[f514])).
% 9.28/1.67 fof(f517,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|X0=nil|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f516,f205])).
% 9.28/1.67 fof(f545,plain,(
% 9.28/1.67 ~ssList(sk2)|sk2=nil|~segmentP(sk1,sk2)|~ssList(sk2)),
% 9.28/1.67 inference(resolution,[status(thm)],[f517,f254])).
% 9.28/1.67 fof(f546,plain,(
% 9.28/1.67 ~ssList(sk2)|sk2=nil|~segmentP(sk1,sk2)),
% 9.28/1.67 inference(duplicate_literals_removal,[status(thm)],[f545])).
% 9.28/1.67 fof(f547,plain,(
% 9.28/1.67 sk2=nil|~segmentP(sk1,sk2)),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f546,f429])).
% 9.28/1.67 fof(f554,plain,(
% 9.28/1.67 app(nil,sk6)=sk6),
% 9.28/1.67 inference(resolution,[status(thm)],[f437,f272])).
% 9.28/1.67 fof(f555,plain,(
% 9.28/1.67 app(sk6,nil)=sk6),
% 9.28/1.67 inference(resolution,[status(thm)],[f437,f271])).
% 9.28/1.67 fof(f804,plain,(
% 9.28/1.67 ![X0,X1]: (~app(X0,X1)=app(sk5,X1)|~ssList(X0)|~ssList(X1)|X0=sk5)),
% 9.28/1.67 inference(resolution,[status(thm)],[f370,f436])).
% 9.28/1.67 fof(f1039,plain,(
% 9.28/1.67 ![X0]: (~app(X0,sk6)=app(sk5,sk6)|~ssList(X0)|X0=sk5)),
% 9.28/1.67 inference(resolution,[status(thm)],[f804,f437])).
% 9.28/1.67 fof(f1044,plain,(
% 9.28/1.67 ![X0]: (~app(X0,sk6)=sk2|~ssList(X0)|X0=sk5)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f473,f1039])).
% 9.28/1.67 fof(f1053,plain,(
% 9.28/1.67 ~app(sk2,sk6)=sk2|sk2=sk5),
% 9.28/1.67 inference(resolution,[status(thm)],[f1044,f429])).
% 9.28/1.67 fof(f1255,plain,(
% 9.28/1.67 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X2)|segmentP(app(app(X1,X2),X0),X2)|~ssList(X2))),
% 9.28/1.67 inference(resolution,[status(thm)],[f402,f254])).
% 9.28/1.67 fof(f1258,plain,(
% 9.28/1.67 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|segmentP(app(app(X1,X2),X0),X2))),
% 9.28/1.67 inference(duplicate_literals_removal,[status(thm)],[f1255])).
% 9.28/1.67 fof(f1335,plain,(
% 9.28/1.67 ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(sk6,X1),X0),X1))),
% 9.28/1.67 inference(resolution,[status(thm)],[f1258,f437])).
% 9.28/1.67 fof(f1337,plain,(
% 9.28/1.67 ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(sk5,X1),X0),X1))),
% 9.28/1.67 inference(resolution,[status(thm)],[f1258,f436])).
% 9.28/1.67 fof(f1341,plain,(
% 9.28/1.67 ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(nil,X1),X0),X1))),
% 9.28/1.67 inference(resolution,[status(thm)],[f1258,f205])).
% 9.28/1.67 fof(f1505,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|~ssList(nil)|segmentP(app(sk6,X0),nil))),
% 9.28/1.67 inference(paramodulation,[status(thm)],[f555,f1335])).
% 9.28/1.67 fof(f1506,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|~ssList(sk5)|segmentP(app(sk1,X0),sk5))),
% 9.28/1.67 inference(paramodulation,[status(thm)],[f474,f1335])).
% 9.28/1.67 fof(f1510,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|segmentP(app(sk6,X0),nil))),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1505,f205])).
% 9.28/1.67 fof(f1511,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk5))),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1506,f436])).
% 9.28/1.67 fof(f1515,plain,(
% 9.28/1.67 ~ssList(nil)|segmentP(sk6,nil)),
% 9.28/1.67 inference(paramodulation,[status(thm)],[f555,f1510])).
% 9.28/1.67 fof(f1517,plain,(
% 9.28/1.67 segmentP(sk6,nil)),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1515,f205])).
% 9.28/1.67 fof(f1544,plain,(
% 9.28/1.67 ~ssList(nil)|segmentP(sk1,sk5)),
% 9.28/1.67 inference(paramodulation,[status(thm)],[f477,f1511])).
% 9.28/1.67 fof(f1548,plain,(
% 9.28/1.67 segmentP(sk1,sk5)),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1544,f205])).
% 9.28/1.67 fof(f1583,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|~ssList(sk6)|segmentP(app(sk2,X0),sk6))),
% 9.28/1.67 inference(paramodulation,[status(thm)],[f473,f1337])).
% 9.28/1.67 fof(f1588,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|segmentP(app(sk2,X0),sk6))),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1583,f437])).
% 9.28/1.67 fof(f1606,plain,(
% 9.28/1.67 ~ssList(nil)|segmentP(sk2,sk6)),
% 9.28/1.67 inference(paramodulation,[status(thm)],[f475,f1588])).
% 9.28/1.67 fof(f1610,plain,(
% 9.28/1.67 segmentP(sk2,sk6)),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1606,f205])).
% 9.28/1.67 fof(f1751,plain,(
% 9.28/1.67 ~ssList(sk6)|sk6=nil|~segmentP(sk1,sk6)),
% 9.28/1.67 inference(resolution,[status(thm)],[f1610,f517])).
% 9.28/1.67 fof(f1755,plain,(
% 9.28/1.67 sk6=nil|~segmentP(sk1,sk6)),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1751,f437])).
% 9.28/1.67 fof(f1792,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|~ssList(sk6)|segmentP(app(sk6,X0),sk6))),
% 9.28/1.67 inference(paramodulation,[status(thm)],[f554,f1341])).
% 9.28/1.67 fof(f1800,plain,(
% 9.28/1.67 ![X0]: (~ssList(X0)|segmentP(app(sk6,X0),sk6))),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1792,f437])).
% 9.28/1.67 fof(f1808,plain,(
% 9.28/1.67 ~ssList(sk5)|segmentP(sk1,sk6)),
% 9.28/1.67 inference(paramodulation,[status(thm)],[f474,f1800])).
% 9.28/1.67 fof(f1813,plain,(
% 9.28/1.67 sk6=nil),
% 9.28/1.67 inference(backward_subsumption_resolution,[status(thm)],[f1755,f1814])).
% 9.28/1.67 fof(f1814,plain,(
% 9.28/1.67 segmentP(sk1,sk6)),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f1808,f436])).
% 9.28/1.67 fof(f1818,plain,(
% 9.28/1.67 segmentP(nil,nil)),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f1813,f1517])).
% 9.28/1.67 fof(f1837,plain,(
% 9.28/1.67 app(nil,sk5)=sk1),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f1813,f474])).
% 9.28/1.67 fof(f1838,plain,(
% 9.28/1.67 app(sk5,nil)=sk2),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f1813,f473])).
% 9.28/1.67 fof(f1951,plain,(
% 9.28/1.67 ~app(sk2,nil)=sk2|sk2=sk5),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f1813,f1053])).
% 9.28/1.67 fof(f2039,plain,(
% 9.28/1.67 sk1=sk5),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f1837,f499])).
% 9.28/1.67 fof(f2040,plain,(
% 9.28/1.67 sk2=sk5),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f1838,f500])).
% 9.28/1.67 fof(f2226,plain,(
% 9.28/1.67 ~sk2=sk2|sk2=sk5),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f475,f1951])).
% 9.28/1.67 fof(f2231,plain,(
% 9.28/1.67 segmentP(sk1,sk2)),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f2396,f1548])).
% 9.28/1.67 fof(f2396,plain,(
% 9.28/1.67 sk2=sk5),
% 9.28/1.67 inference(trivial_equality_resolution,[status(thm)],[f2226])).
% 9.28/1.67 fof(f2485,plain,(
% 9.28/1.67 sk2=nil|~segmentP(sk1,sk1)),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f2605,f547])).
% 9.28/1.67 fof(f2488,plain,(
% 9.28/1.67 ~segmentP(sk2,sk2)|~segmentP(sk1,sk1)),
% 9.28/1.67 inference(backward_demodulation,[status(thm)],[f2605,f495])).
% 9.28/1.67 fof(f2605,plain,(
% 9.28/1.67 sk2=sk1),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f2039,f2040])).
% 9.28/1.67 fof(f2616,plain,(
% 9.28/1.67 segmentP(sk1,sk1)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f2605,f2231])).
% 9.28/1.67 fof(f2951,plain,(
% 9.28/1.67 sk1=nil|~segmentP(sk1,sk1)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f2605,f2485])).
% 9.28/1.67 fof(f3078,plain,(
% 9.28/1.67 sk1=nil),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f2951,f2616])).
% 9.28/1.67 fof(f3085,plain,(
% 9.28/1.67 ~segmentP(sk1,sk2)|~segmentP(sk1,sk1)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f2605,f2488])).
% 9.28/1.67 fof(f3086,plain,(
% 9.28/1.67 ~segmentP(nil,sk2)|~segmentP(sk1,sk1)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f3078,f3085])).
% 9.28/1.67 fof(f3087,plain,(
% 9.28/1.67 ~segmentP(nil,sk1)|~segmentP(sk1,sk1)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f2605,f3086])).
% 9.28/1.67 fof(f3088,plain,(
% 9.28/1.67 ~segmentP(nil,nil)|~segmentP(sk1,sk1)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f3078,f3087])).
% 9.28/1.67 fof(f3089,plain,(
% 9.28/1.67 ~segmentP(nil,nil)|~segmentP(nil,sk1)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f3078,f3088])).
% 9.28/1.67 fof(f3090,plain,(
% 9.28/1.67 ~segmentP(nil,nil)|~segmentP(nil,nil)),
% 9.28/1.67 inference(forward_demodulation,[status(thm)],[f3078,f3089])).
% 9.28/1.67 fof(f3091,plain,(
% 9.28/1.67 ~segmentP(nil,nil)),
% 9.28/1.67 inference(duplicate_literals_removal,[status(thm)],[f3090])).
% 9.28/1.67 fof(f3092,plain,(
% 9.28/1.67 $false),
% 9.28/1.67 inference(forward_subsumption_resolution,[status(thm)],[f3091,f1818])).
% 9.28/1.67 % SZS output end CNFRefutation for theBenchmark.p
% 9.28/1.72 % Elapsed time: 1.286781 seconds
% 9.28/1.72 % CPU time: 9.755735 seconds
% 9.28/1.72 % Total memory used: 210.815 MB
% 9.28/1.72 % Net memory used: 205.764 MB
%------------------------------------------------------------------------------