%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC100-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:35 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC100-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.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 07:57:16 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 0.14/0.44 % Refutation found
% 0.14/0.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.44 fof(f8,axiom,(
% 0.14/0.44 ssList(nil) ),
% 0.14/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f85,axiom,(
% 0.14/0.44 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f100,axiom,(
% 0.14/0.44 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.14/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f118,axiom,(
% 0.14/0.44 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = U ) ))),
% 0.14/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f144,axiom,(
% 0.14/0.44 (![U,V,W]: (( app(U,V) != W| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| frontsegP(W,U) ) ))),
% 0.14/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f186,negated_conjecture,(
% 0.14/0.44 ssList(sk1) ),
% 0.14/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.44 fof(f190,negated_conjecture,(
% 0.14/0.44 sk2 = sk4 ),
% 0.14/0.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f191,negated_conjecture,(
% 0.14/0.45 sk1 = sk3 ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f192,negated_conjecture,(
% 0.14/0.45 ssList(sk5) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f193,negated_conjecture,(
% 0.14/0.45 app(sk3,sk5) = sk4 ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f196,negated_conjecture,(
% 0.14/0.45 ( nil = sk4| nil != sk3 ) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f198,negated_conjecture,(
% 0.14/0.45 ( nil = sk2| ~ neq(sk1,nil)| ~ frontsegP(sk2,sk1) ) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f199,negated_conjecture,(
% 0.14/0.45 ( nil != sk1| neq(sk2,nil) ) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f200,negated_conjecture,(
% 0.14/0.45 ( nil != sk1| ~ neq(sk1,nil)| ~ frontsegP(sk2,sk1) ) ),
% 0.14/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.45 fof(f208,plain,(
% 0.14/0.45 ssList(nil)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.45 fof(f286,plain,(
% 0.14/0.45 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f85])).
% 0.14/0.45 fof(f303,plain,(
% 0.14/0.45 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f100])).
% 0.14/0.45 fof(f327,plain,(
% 0.14/0.45 ![U]: (((![V]: (~app(U,V)=nil|~ssList(V)))|~ssList(U))|nil=U)),
% 0.14/0.45 inference(miniscoping,[status(thm)],[f118])).
% 0.14/0.45 fof(f328,plain,(
% 0.14/0.45 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X0)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f327])).
% 0.14/0.45 fof(f360,plain,(
% 0.14/0.45 ![U,W]: ((((![V]: (~app(U,V)=W|~ssList(V)))|~ssList(U))|~ssList(W))|frontsegP(W,U))),
% 0.14/0.45 inference(miniscoping,[status(thm)],[f144])).
% 0.14/0.45 fof(f361,plain,(
% 0.14/0.45 ![X0,X1,X2]: (~app(X0,X1)=X2|~ssList(X1)|~ssList(X0)|~ssList(X2)|frontsegP(X2,X0))),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f360])).
% 0.14/0.45 fof(f431,plain,(
% 0.14/0.45 ssList(sk1)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f186])).
% 0.14/0.45 fof(f435,plain,(
% 0.14/0.45 sk2=sk4),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f190])).
% 0.14/0.45 fof(f436,plain,(
% 0.14/0.45 sk1=sk3),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f191])).
% 0.14/0.45 fof(f437,plain,(
% 0.14/0.45 ssList(sk5)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f192])).
% 0.14/0.45 fof(f438,plain,(
% 0.14/0.45 app(sk3,sk5)=sk4),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f193])).
% 0.14/0.45 fof(f442,plain,(
% 0.14/0.45 nil=sk4|~nil=sk3),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f196])).
% 0.14/0.45 fof(f444,plain,(
% 0.14/0.45 nil=sk2|~neq(sk1,nil)|~frontsegP(sk2,sk1)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f198])).
% 0.14/0.45 fof(f445,plain,(
% 0.14/0.45 ~nil=sk1|neq(sk2,nil)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f199])).
% 0.14/0.45 fof(f446,plain,(
% 0.14/0.45 ~nil=sk1|~neq(sk1,nil)|~frontsegP(sk2,sk1)),
% 0.14/0.45 inference(cnf_transformation,[status(thm)],[f200])).
% 0.14/0.45 fof(f462,plain,(
% 0.14/0.45 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(app(X1,X0))|frontsegP(app(X1,X0),X1))),
% 0.14/0.45 inference(destructive_equality_resolution,[status(thm)],[f361])).
% 0.14/0.45 fof(f504,plain,(
% 0.14/0.45 app(sk1,sk5)=sk4),
% 0.14/0.45 inference(forward_demodulation,[status(thm)],[f436,f438])).
% 0.14/0.45 fof(f505,plain,(
% 0.14/0.45 app(sk1,sk5)=sk2),
% 0.14/0.45 inference(forward_demodulation,[status(thm)],[f435,f504])).
% 0.14/0.45 fof(f507,plain,(
% 0.14/0.45 nil=sk2|~nil=sk3),
% 0.14/0.45 inference(forward_demodulation,[status(thm)],[f435,f442])).
% 0.14/0.45 fof(f508,plain,(
% 0.14/0.45 nil=sk2|~nil=sk1),
% 0.14/0.45 inference(forward_demodulation,[status(thm)],[f436,f507])).
% 0.14/0.45 fof(f546,plain,(
% 0.14/0.45 ~ssList(nil)|~ssList(sk1)|sk1=nil|nil=sk2|~frontsegP(sk2,sk1)),
% 0.14/0.45 inference(resolution,[status(thm)],[f303,f444])).
% 0.14/0.45 fof(f548,plain,(
% 0.14/0.45 ~ssList(sk1)|sk1=nil|nil=sk2|~frontsegP(sk2,sk1)),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f546,f208])).
% 0.14/0.45 fof(f596,plain,(
% 0.14/0.45 ![X0]: (~app(X0,sk5)=nil|~ssList(X0)|nil=X0)),
% 0.14/0.45 inference(resolution,[status(thm)],[f328,f437])).
% 0.14/0.45 fof(f708,plain,(
% 0.14/0.45 ~sk2=nil|~ssList(sk1)|nil=sk1),
% 0.14/0.45 inference(paramodulation,[status(thm)],[f505,f596])).
% 0.14/0.45 fof(f709,plain,(
% 0.14/0.45 ~sk2=nil|nil=sk1),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f708,f431])).
% 0.14/0.45 fof(f710,plain,(
% 0.14/0.45 sk1=nil|nil=sk2|~frontsegP(sk2,sk1)),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f548,f431])).
% 0.14/0.45 fof(f717,plain,(
% 0.14/0.45 ![X0,X1]: (~ssList(X0)|~ssList(X1)|frontsegP(app(X1,X0),X1))),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f462,f286])).
% 0.14/0.45 fof(f727,plain,(
% 0.14/0.45 ~ssList(sk5)|~ssList(sk1)|frontsegP(sk2,sk1)),
% 0.14/0.45 inference(paramodulation,[status(thm)],[f505,f717])).
% 0.14/0.45 fof(f733,plain,(
% 0.14/0.45 ~ssList(sk1)|frontsegP(sk2,sk1)),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f727,f437])).
% 0.14/0.45 fof(f735,plain,(
% 0.14/0.45 sk1=nil|~frontsegP(sk2,sk1)),
% 0.14/0.45 inference(backward_subsumption_resolution,[status(thm)],[f710,f709])).
% 0.14/0.45 fof(f1065,plain,(
% 0.14/0.45 ~nil=sk1|~neq(sk1,nil)),
% 0.14/0.45 inference(backward_subsumption_resolution,[status(thm)],[f446,f1066])).
% 0.14/0.45 fof(f1066,plain,(
% 0.14/0.45 frontsegP(sk2,sk1)),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f733,f431])).
% 0.14/0.45 fof(f1111,plain,(
% 0.14/0.45 ~nil=sk1|~neq(nil,nil)),
% 0.14/0.45 inference(backward_demodulation,[status(thm)],[f1125,f1065])).
% 0.14/0.45 fof(f1118,plain,(
% 0.14/0.45 ~nil=nil|neq(sk2,nil)),
% 0.14/0.45 inference(backward_demodulation,[status(thm)],[f1125,f445])).
% 0.14/0.45 fof(f1119,plain,(
% 0.14/0.45 nil=sk2|~nil=nil),
% 0.14/0.45 inference(backward_demodulation,[status(thm)],[f1125,f508])).
% 0.14/0.45 fof(f1125,plain,(
% 0.14/0.45 sk1=nil),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f735,f1066])).
% 0.14/0.45 fof(f1126,plain,(
% 0.14/0.45 ~nil=nil|~neq(nil,nil)),
% 0.14/0.45 inference(forward_demodulation,[status(thm)],[f1125,f1111])).
% 0.14/0.45 fof(f1127,plain,(
% 0.14/0.45 ~neq(nil,nil)),
% 0.14/0.45 inference(trivial_equality_resolution,[status(thm)],[f1126])).
% 0.14/0.45 fof(f1130,plain,(
% 0.14/0.45 neq(sk2,nil)),
% 0.14/0.45 inference(trivial_equality_resolution,[status(thm)],[f1118])).
% 0.14/0.45 fof(f1131,plain,(
% 0.14/0.45 nil=sk2),
% 0.14/0.45 inference(trivial_equality_resolution,[status(thm)],[f1119])).
% 0.14/0.45 fof(f1194,plain,(
% 0.14/0.45 neq(nil,nil)),
% 0.14/0.45 inference(forward_demodulation,[status(thm)],[f1131,f1130])).
% 0.14/0.45 fof(f1195,plain,(
% 0.14/0.45 $false),
% 0.14/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1194,f1127])).
% 0.14/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.47 % Elapsed time: 0.093722 seconds
% 0.14/0.47 % CPU time: 0.374522 seconds
% 0.14/0.47 % Total memory used: 114.438 MB
% 0.14/0.47 % Net memory used: 114.036 MB
%------------------------------------------------------------------------------