%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC416-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 : n002.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:25 PM UTC 2026
% Result : Unsatisfiable 1.34s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC416-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 : n002.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:25:19 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.15/0.38 % Drodi V4.1.1
% 1.34/0.66 % Refutation found
% 1.34/0.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.34/0.66 % SZS output start CNFRefutation for theBenchmark
% 1.34/0.66 fof(f8,axiom,(
% 1.34/0.66 ssList(nil) ),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f86,axiom,(
% 1.34/0.66 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f97,axiom,(
% 1.34/0.66 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| hd(cons(U,V)) = U ) ))),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f98,axiom,(
% 1.34/0.66 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f100,axiom,(
% 1.34/0.66 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f120,axiom,(
% 1.34/0.66 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| app(cons(U,nil),V) = cons(U,V) ) ))),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f186,negated_conjecture,(
% 1.34/0.66 ssList(sk1) ),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f189,negated_conjecture,(
% 1.34/0.66 ssList(sk4) ),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f190,negated_conjecture,(
% 1.34/0.66 sk2 = sk4 ),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f191,negated_conjecture,(
% 1.34/0.66 sk1 = sk3 ),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f192,negated_conjecture,(
% 1.34/0.66 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f197,negated_conjecture,(
% 1.34/0.66 (![A,B,C]: (( ~ ssList(A)| sk2 != A| ~ ssList(B)| app(B,sk1) != A| ~ ssItem(C)| cons(C,nil) != B| hd(sk2) != C| ~ neq(nil,sk2)| ~ neq(sk4,nil) ) ))),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f198,negated_conjecture,(
% 1.34/0.66 ( ssItem(sk5)| ~ neq(sk4,nil) ) ),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f199,negated_conjecture,(
% 1.34/0.66 ( app(cons(sk5,nil),sk3) = sk4| ~ neq(sk4,nil) ) ),
% 1.34/0.66 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.66 fof(f207,plain,(
% 1.34/0.66 ssList(nil)),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f8])).
% 1.34/0.66 fof(f286,plain,(
% 1.34/0.66 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f86])).
% 1.34/0.66 fof(f297,plain,(
% 1.34/0.66 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|hd(cons(X0,X1))=X0)),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f97])).
% 1.34/0.66 fof(f298,plain,(
% 1.34/0.66 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 1.34/0.66 inference(miniscoping,[status(thm)],[f98])).
% 1.34/0.66 fof(f299,plain,(
% 1.34/0.66 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f298])).
% 1.34/0.66 fof(f302,plain,(
% 1.34/0.66 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f100])).
% 1.34/0.66 fof(f330,plain,(
% 1.34/0.66 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=cons(X0,X1))),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f120])).
% 1.34/0.66 fof(f430,plain,(
% 1.34/0.66 ssList(sk1)),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f186])).
% 1.34/0.66 fof(f433,plain,(
% 1.34/0.66 ssList(sk4)),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f189])).
% 1.34/0.66 fof(f434,plain,(
% 1.34/0.66 sk2=sk4),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f190])).
% 1.34/0.66 fof(f435,plain,(
% 1.34/0.66 sk1=sk3),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f191])).
% 1.34/0.66 fof(f436,plain,(
% 1.34/0.66 neq(sk2,nil)|neq(sk2,nil)),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f192])).
% 1.34/0.66 fof(f442,plain,(
% 1.34/0.66 ((![C]: ((![B]: (((![A]: (((~ssList(A)|~sk2=A)|~ssList(B))|~app(B,sk1)=A))|~ssItem(C))|~cons(C,nil)=B))|~hd(sk2)=C))|~neq(nil,sk2))|~neq(sk4,nil)),
% 1.34/0.66 inference(miniscoping,[status(thm)],[f197])).
% 1.34/0.66 fof(f443,plain,(
% 1.34/0.66 ![X0,X1,X2]: (~ssList(X0)|~sk2=X0|~ssList(X1)|~app(X1,sk1)=X0|~ssItem(X2)|~cons(X2,nil)=X1|~hd(sk2)=X2|~neq(nil,sk2)|~neq(sk4,nil))),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f442])).
% 1.34/0.66 fof(f444,plain,(
% 1.34/0.66 ssItem(sk5)|~neq(sk4,nil)),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f198])).
% 1.34/0.66 fof(f445,plain,(
% 1.34/0.66 app(cons(sk5,nil),sk3)=sk4|~neq(sk4,nil)),
% 1.34/0.66 inference(cnf_transformation,[status(thm)],[f199])).
% 1.34/0.66 fof(f479,plain,(
% 1.34/0.66 neq(sk4,nil)|neq(sk2,nil)),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f434,f436])).
% 1.34/0.66 fof(f480,plain,(
% 1.34/0.66 neq(sk4,nil)|neq(sk4,nil)),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f434,f479])).
% 1.34/0.66 fof(f481,plain,(
% 1.34/0.66 neq(sk4,nil)),
% 1.34/0.66 inference(duplicate_literals_removal,[status(thm)],[f480])).
% 1.34/0.66 fof(f490,plain,(
% 1.34/0.66 ![X0,X1,X2]: (~ssList(X0)|~sk4=X0|~ssList(X1)|~app(X1,sk1)=X0|~ssItem(X2)|~cons(X2,nil)=X1|~hd(sk2)=X2|~neq(nil,sk2)|~neq(sk4,nil))),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f434,f443])).
% 1.34/0.66 fof(f491,plain,(
% 1.34/0.66 ![X0,X1,X2]: (~ssList(X0)|~sk4=X0|~ssList(X1)|~app(X1,sk1)=X0|~ssItem(X2)|~cons(X2,nil)=X1|~hd(sk4)=X2|~neq(nil,sk2)|~neq(sk4,nil))),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f434,f490])).
% 1.34/0.66 fof(f492,plain,(
% 1.34/0.66 ![X0,X1,X2]: (~ssList(X0)|~sk4=X0|~ssList(X1)|~app(X1,sk1)=X0|~ssItem(X2)|~cons(X2,nil)=X1|~hd(sk4)=X2|~neq(nil,sk4)|~neq(sk4,nil))),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f434,f491])).
% 1.34/0.66 fof(f493,plain,(
% 1.34/0.66 ~ssList(sk4)|~ssList(cons(hd(sk4),nil))|~app(cons(hd(sk4),nil),sk1)=sk4|~ssItem(hd(sk4))|~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(destructive_equality_resolution,[status(thm)],[f492])).
% 1.34/0.66 fof(f494,plain,(
% 1.34/0.66 ~ssList(cons(hd(sk4),nil))|~app(cons(hd(sk4),nil),sk1)=sk4|~ssItem(hd(sk4))|~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(forward_subsumption_resolution,[status(thm)],[f493,f433])).
% 1.34/0.66 fof(f495,plain,(
% 1.34/0.66 ssItem(sk5)),
% 1.34/0.66 inference(forward_subsumption_resolution,[status(thm)],[f444,f481])).
% 1.34/0.66 fof(f496,plain,(
% 1.34/0.66 app(cons(sk5,nil),sk1)=sk4|~neq(sk4,nil)),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f435,f445])).
% 1.34/0.66 fof(f497,plain,(
% 1.34/0.66 app(cons(sk5,nil),sk1)=sk4),
% 1.34/0.66 inference(forward_subsumption_resolution,[status(thm)],[f496,f481])).
% 1.34/0.66 fof(f558,plain,(
% 1.34/0.66 ![X0]: (~ssList(X0)|hd(cons(sk5,X0))=sk5)),
% 1.34/0.66 inference(resolution,[status(thm)],[f495,f297])).
% 1.34/0.66 fof(f560,plain,(
% 1.34/0.66 ![X0]: (~cons(sk5,X0)=nil|~ssList(X0))),
% 1.34/0.66 inference(resolution,[status(thm)],[f495,f299])).
% 1.34/0.66 fof(f561,plain,(
% 1.34/0.66 ![X0]: (~ssList(X0)|ssList(cons(sk5,X0)))),
% 1.34/0.66 inference(resolution,[status(thm)],[f495,f286])).
% 1.34/0.66 fof(f566,plain,(
% 1.34/0.66 hd(cons(sk5,sk1))=sk5),
% 1.34/0.66 inference(resolution,[status(thm)],[f558,f430])).
% 1.34/0.66 fof(f573,plain,(
% 1.34/0.66 ~cons(sk5,sk1)=nil),
% 1.34/0.66 inference(resolution,[status(thm)],[f560,f430])).
% 1.34/0.66 fof(f575,plain,(
% 1.34/0.66 ssList(cons(sk5,nil))),
% 1.34/0.66 inference(resolution,[status(thm)],[f561,f207])).
% 1.34/0.66 fof(f587,plain,(
% 1.34/0.66 ![X0]: (~ssList(X0)|app(cons(sk5,nil),X0)=cons(sk5,X0))),
% 1.34/0.66 inference(resolution,[status(thm)],[f330,f495])).
% 1.34/0.66 fof(f634,plain,(
% 1.34/0.66 app(cons(sk5,nil),sk1)=cons(sk5,sk1)),
% 1.34/0.66 inference(resolution,[status(thm)],[f587,f430])).
% 1.34/0.66 fof(f636,plain,(
% 1.34/0.66 ~sk4=nil),
% 1.34/0.66 inference(backward_demodulation,[status(thm)],[f639,f573])).
% 1.34/0.66 fof(f638,plain,(
% 1.34/0.66 hd(sk4)=sk5),
% 1.34/0.66 inference(backward_demodulation,[status(thm)],[f639,f566])).
% 1.34/0.66 fof(f639,plain,(
% 1.34/0.66 sk4=cons(sk5,sk1)),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f497,f634])).
% 1.34/0.66 fof(f645,plain,(
% 1.34/0.66 ~ssList(cons(hd(sk4),nil))|~app(cons(hd(sk4),nil),sk1)=sk4|~ssItem(sk5)|~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(backward_demodulation,[status(thm)],[f638,f494])).
% 1.34/0.66 fof(f647,plain,(
% 1.34/0.66 ~ssList(cons(sk5,nil))|~app(cons(hd(sk4),nil),sk1)=sk4|~ssItem(sk5)|~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f638,f645])).
% 1.34/0.66 fof(f648,plain,(
% 1.34/0.66 ~ssList(cons(sk5,nil))|~app(cons(sk5,nil),sk1)=sk4|~ssItem(sk5)|~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f638,f647])).
% 1.34/0.66 fof(f649,plain,(
% 1.34/0.66 ~ssList(cons(sk5,nil))|~sk4=sk4|~ssItem(sk5)|~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(forward_demodulation,[status(thm)],[f497,f648])).
% 1.34/0.66 fof(f650,plain,(
% 1.34/0.66 ~ssList(cons(sk5,nil))|~ssItem(sk5)|~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(trivial_equality_resolution,[status(thm)],[f649])).
% 1.34/0.66 fof(f651,plain,(
% 1.34/0.66 ~ssItem(sk5)|~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(forward_subsumption_resolution,[status(thm)],[f650,f575])).
% 1.34/0.66 fof(f782,plain,(
% 1.34/0.66 ~neq(nil,sk4)|~neq(sk4,nil)),
% 1.34/0.66 inference(resolution,[status(thm)],[f651,f495])).
% 1.34/0.66 fof(f783,plain,(
% 1.34/0.66 ~neq(nil,sk4)),
% 1.34/0.66 inference(forward_subsumption_resolution,[status(thm)],[f782,f481])).
% 1.34/0.66 fof(f784,plain,(
% 1.34/0.66 ~ssList(sk4)|~ssList(nil)|nil=sk4),
% 1.34/0.66 inference(resolution,[status(thm)],[f783,f302])).
% 1.34/0.66 fof(f785,plain,(
% 1.34/0.66 ~ssList(nil)|nil=sk4),
% 1.34/0.66 inference(forward_subsumption_resolution,[status(thm)],[f784,f433])).
% 1.34/0.66 fof(f786,plain,(
% 1.34/0.66 nil=sk4),
% 1.34/0.66 inference(resolution,[status(thm)],[f785,f207])).
% 1.34/0.66 fof(f787,plain,(
% 1.34/0.66 $false),
% 1.34/0.66 inference(forward_subsumption_resolution,[status(thm)],[f786,f636])).
% 1.34/0.66 % SZS output end CNFRefutation for theBenchmark.p
% 1.34/0.68 % Elapsed time: 0.296177 seconds
% 1.34/0.68 % CPU time: 2.128866 seconds
% 1.34/0.68 % Total memory used: 153.692 MB
% 1.34/0.68 % Net memory used: 151.427 MB
%------------------------------------------------------------------------------