%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC182-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 : n019.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:48 PM UTC 2026
% Result : Unsatisfiable 17.12s 3.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC182-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n019.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 08:02:50 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.52 % Drodi V4.1.1
% 17.12/3.23 % Refutation found
% 17.12/3.23 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 17.12/3.23 % SZS output start CNFRefutation for theBenchmark
% 17.12/3.23 fof(f8,axiom,(
% 17.12/3.23 ssList(nil) ),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f85,axiom,(
% 17.12/3.23 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f86,axiom,(
% 17.12/3.23 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f98,axiom,(
% 17.12/3.23 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f118,axiom,(
% 17.12/3.23 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = U ) ))),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f119,axiom,(
% 17.12/3.23 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = V ) ))),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f190,negated_conjecture,(
% 17.12/3.23 nil = sk3 ),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f192,negated_conjecture,(
% 17.12/3.23 sk1 = sk3 ),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f193,negated_conjecture,(
% 17.12/3.23 ssItem(sk5) ),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f194,negated_conjecture,(
% 17.12/3.23 ssList(sk6) ),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f195,negated_conjecture,(
% 17.12/3.23 ssList(sk7) ),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f196,negated_conjecture,(
% 17.12/3.23 app(app(sk6,cons(sk5,nil)),sk7) = sk1 ),
% 17.12/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.12/3.23 fof(f205,plain,(
% 17.12/3.23 ssList(nil)),
% 17.12/3.23 inference(cnf_transformation,[status(thm)],[f8])).
% 17.12/3.23 fof(f283,plain,(
% 17.12/3.23 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 17.12/3.23 inference(cnf_transformation,[status(thm)],[f85])).
% 17.12/3.23 fof(f284,plain,(
% 17.12/3.23 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 17.12/3.23 inference(cnf_transformation,[status(thm)],[f86])).
% 17.12/3.23 fof(f296,plain,(
% 17.12/3.23 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 17.12/3.24 inference(miniscoping,[status(thm)],[f98])).
% 17.12/3.24 fof(f297,plain,(
% 17.12/3.24 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f296])).
% 17.12/3.24 fof(f324,plain,(
% 17.12/3.24 ![U]: (((![V]: (~app(U,V)=nil|~ssList(V)))|~ssList(U))|nil=U)),
% 17.12/3.24 inference(miniscoping,[status(thm)],[f118])).
% 17.12/3.24 fof(f325,plain,(
% 17.12/3.24 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X0)),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f324])).
% 17.12/3.24 fof(f326,plain,(
% 17.12/3.24 ![V]: ((![U]: ((~app(U,V)=nil|~ssList(V))|~ssList(U)))|nil=V)),
% 17.12/3.24 inference(miniscoping,[status(thm)],[f119])).
% 17.12/3.24 fof(f327,plain,(
% 17.12/3.24 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X1)),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f326])).
% 17.12/3.24 fof(f432,plain,(
% 17.12/3.24 nil=sk3),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f190])).
% 17.12/3.24 fof(f434,plain,(
% 17.12/3.24 sk1=sk3),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f192])).
% 17.12/3.24 fof(f435,plain,(
% 17.12/3.24 ssItem(sk5)),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f193])).
% 17.12/3.24 fof(f436,plain,(
% 17.12/3.24 ssList(sk6)),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f194])).
% 17.12/3.24 fof(f437,plain,(
% 17.12/3.24 ssList(sk7)),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f195])).
% 17.12/3.24 fof(f438,plain,(
% 17.12/3.24 app(app(sk6,cons(sk5,nil)),sk7)=sk1),
% 17.12/3.24 inference(cnf_transformation,[status(thm)],[f196])).
% 17.12/3.24 fof(f498,plain,(
% 17.12/3.24 ![X0]: (~ssList(X0)|ssList(app(sk6,X0)))),
% 17.12/3.24 inference(resolution,[status(thm)],[f283,f436])).
% 17.12/3.24 fof(f537,definition,(
% 17.12/3.24 sQ4_spl <=> (ssList(nil))),
% 17.12/3.24 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 17.12/3.24 fof(f539,plain,(
% 17.12/3.24 ~ssList(nil)|sQ4_spl),
% 17.12/3.24 inference(component_clause,[status(thm)],[f537])).
% 17.12/3.24 fof(f544,plain,(
% 17.12/3.24 $false|sQ4_spl),
% 17.12/3.24 inference(forward_subsumption_resolution,[status(thm)],[f539,f205])).
% 17.12/3.24 fof(f545,plain,(
% 17.12/3.24 sQ4_spl),
% 17.12/3.24 inference(contradiction_clause,[status(thm)],[f544])).
% 17.12/3.24 fof(f624,plain,(
% 17.12/3.24 ![X0]: (~ssList(X0)|ssList(cons(sk5,X0)))),
% 17.12/3.24 inference(resolution,[status(thm)],[f284,f435])).
% 17.12/3.24 fof(f629,plain,(
% 17.12/3.24 ![X0]: (~cons(sk5,X0)=nil|~ssList(X0))),
% 17.12/3.24 inference(resolution,[status(thm)],[f297,f435])).
% 17.12/3.24 fof(f647,plain,(
% 17.12/3.24 ![X0]: (~app(X0,sk7)=nil|~ssList(X0)|nil=X0)),
% 17.12/3.24 inference(resolution,[status(thm)],[f325,f437])).
% 17.12/3.24 fof(f776,definition,(
% 17.12/3.24 sQ23_spl <=> (ssList(cons(sk5,nil)))),
% 17.12/3.24 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 17.12/3.24 fof(f777,plain,(
% 17.12/3.24 ssList(cons(sk5,nil))|~sQ23_spl),
% 17.12/3.24 inference(component_clause,[status(thm)],[f776])).
% 17.12/3.24 fof(f778,plain,(
% 17.12/3.24 ~ssList(cons(sk5,nil))|sQ23_spl),
% 17.12/3.24 inference(component_clause,[status(thm)],[f776])).
% 17.12/3.24 fof(f808,plain,(
% 17.12/3.24 app(app(sk6,cons(sk5,nil)),sk7)=nil),
% 17.12/3.24 inference(backward_demodulation,[status(thm)],[f813,f438])).
% 17.12/3.24 fof(f813,plain,(
% 17.12/3.24 sk1=nil),
% 17.12/3.24 inference(forward_demodulation,[status(thm)],[f432,f434])).
% 17.12/3.24 fof(f1121,plain,(
% 17.12/3.24 ![X0]: (~cons(sk5,cons(sk5,X0))=nil|~ssList(X0))),
% 17.12/3.24 inference(resolution,[status(thm)],[f629,f624])).
% 17.12/3.24 fof(f1338,definition,(
% 17.12/3.24 sQ37_spl <=> (ssList(app(sk6,cons(sk5,nil))))),
% 17.12/3.24 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 17.12/3.24 fof(f1339,plain,(
% 17.12/3.24 ssList(app(sk6,cons(sk5,nil)))|~sQ37_spl),
% 17.12/3.24 inference(component_clause,[status(thm)],[f1338])).
% 17.12/3.24 fof(f1340,plain,(
% 17.12/3.24 ~ssList(app(sk6,cons(sk5,nil)))|sQ37_spl),
% 17.12/3.24 inference(component_clause,[status(thm)],[f1338])).
% 17.12/3.24 fof(f1488,plain,(
% 17.12/3.24 ~ssList(cons(sk5,nil))|sQ37_spl),
% 17.12/3.24 inference(resolution,[status(thm)],[f1340,f498])).
% 17.12/3.24 fof(f1518,definition,(
% 17.12/3.24 sQ41_spl <=> (nil=app(sk6,cons(sk5,nil)))),
% 17.12/3.24 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 17.12/3.24 fof(f1630,plain,(
% 17.12/3.24 ~ssList(nil)|sQ23_spl),
% 17.12/3.24 inference(resolution,[status(thm)],[f624,f778])).
% 17.12/3.24 fof(f1647,plain,(
% 17.12/3.24 ~sQ4_spl|sQ23_spl),
% 17.12/3.24 inference(split_clause,[status(thm)],[f1630,f537,f776])).
% 17.12/3.24 fof(f1659,plain,(
% 17.12/3.24 ![X0]: (~app(X0,cons(sk5,nil))=nil|~ssList(X0)|nil=cons(sk5,nil)|~sQ23_spl)),
% 17.12/3.24 inference(resolution,[status(thm)],[f777,f327])).
% 17.12/3.24 fof(f1664,definition,(
% 17.12/3.24 ![X0]: (sQ43_spl <=> (~app(X0,cons(sk5,nil))=nil|~ssList(X0)))),
% 17.12/3.24 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 17.12/3.24 fof(f1665,plain,(
% 17.12/3.24 ![X0]: (~app(X0,cons(sk5,nil))=nil|~ssList(X0)|~sQ43_spl)),
% 17.12/3.24 inference(component_clause,[status(thm)],[f1664])).
% 17.12/3.24 fof(f1667,definition,(
% 17.12/3.24 sQ44_spl <=> (nil=cons(sk5,nil))),
% 17.12/3.24 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 17.12/3.24 fof(f1668,plain,(
% 17.12/3.24 nil=cons(sk5,nil)|~sQ44_spl),
% 17.12/3.24 inference(component_clause,[status(thm)],[f1667])).
% 17.12/3.24 fof(f1670,plain,(
% 17.12/3.24 sQ43_spl|sQ44_spl|~sQ23_spl),
% 17.12/3.24 inference(split_clause,[status(thm)],[f1659,f1664,f1667,f776])).
% 17.12/3.24 fof(f1840,plain,(
% 17.12/3.24 ~cons(sk5,cons(sk5,nil))=nil),
% 17.12/3.24 inference(resolution,[status(thm)],[f1121,f205])).
% 17.12/3.24 fof(f2079,plain,(
% 17.12/3.24 ~app(sk6,cons(sk5,nil))=nil|~sQ43_spl),
% 17.12/3.24 inference(resolution,[status(thm)],[f1665,f436])).
% 17.12/3.24 fof(f2575,plain,(
% 17.12/3.24 ~sQ41_spl|~sQ43_spl),
% 17.12/3.24 inference(split_clause,[status(thm)],[f2079,f1518,f1664])).
% 17.12/3.24 fof(f2854,plain,(
% 17.12/3.24 ~cons(sk5,nil)=nil|~sQ44_spl),
% 17.12/3.24 inference(backward_demodulation,[status(thm)],[f1668,f1840])).
% 17.12/3.24 fof(f2860,plain,(
% 17.12/3.24 ~sQ44_spl),
% 17.12/3.24 inference(split_clause,[status(thm)],[f2854,f1667])).
% 17.12/3.24 fof(f2960,plain,(
% 17.12/3.24 ~app(app(sk6,cons(sk5,nil)),sk7)=nil|nil=app(sk6,cons(sk5,nil))|~sQ37_spl),
% 17.12/3.24 inference(resolution,[status(thm)],[f1339,f647])).
% 17.12/3.24 fof(f2987,definition,(
% 17.12/3.24 sQ63_spl <=> (app(app(sk6,cons(sk5,nil)),sk7)=nil)),
% 17.12/3.24 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 17.12/3.24 fof(f2989,plain,(
% 17.12/3.24 ~app(app(sk6,cons(sk5,nil)),sk7)=nil|sQ63_spl),
% 17.12/3.24 inference(component_clause,[status(thm)],[f2987])).
% 17.12/3.24 fof(f2990,plain,(
% 17.12/3.24 ~sQ63_spl|sQ41_spl|~sQ37_spl),
% 17.12/3.24 inference(split_clause,[status(thm)],[f2960,f2987,f1518,f1338])).
% 17.12/3.24 fof(f2992,plain,(
% 17.12/3.24 ~sQ23_spl|sQ37_spl),
% 17.12/3.24 inference(split_clause,[status(thm)],[f1488,f776,f1338])).
% 17.12/3.24 fof(f3824,plain,(
% 17.12/3.24 ~nil=nil|sQ63_spl),
% 17.12/3.24 inference(forward_demodulation,[status(thm)],[f808,f2989])).
% 17.12/3.24 fof(f3825,plain,(
% 17.12/3.24 $false|sQ63_spl),
% 17.12/3.24 inference(trivial_equality_resolution,[status(thm)],[f3824])).
% 17.12/3.24 fof(f3826,plain,(
% 17.12/3.24 sQ63_spl),
% 17.12/3.24 inference(contradiction_clause,[status(thm)],[f3825])).
% 17.12/3.24 fof(f3827,plain,(
% 17.12/3.24 $false),
% 17.12/3.24 inference(sat_refutation,[status(thm)],[f545,f1647,f1670,f2575,f2860,f2990,f2992,f3826])).
% 17.12/3.26 % SZS output end CNFRefutation for theBenchmark.p
% 17.35/3.30 % Elapsed time: 2.818405 seconds
% 17.35/3.30 % CPU time: 21.267964 seconds
% 17.35/3.30 % Total memory used: 304.238 MB
% 17.35/3.30 % Net memory used: 292.091 MB
%------------------------------------------------------------------------------