%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC181-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 28.39s 9.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC181-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/5.58 % Computer : n017.cluster.edu
% 0.08/5.58 % Model : x86_64 x86_64
% 0.08/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.58 % Memory : 8046.5625MB
% 0.08/5.58 % OS : Linux 6.8.0-71-generic
% 0.08/5.58 % CPULimit : 300
% 0.08/5.58 % WCLimit : 300
% 0.08/5.58 % DateTime : Mon Sep 21 07:57:51 UTC 2026
% 0.08/5.58 % CPUTime :
% 0.15/5.60 % Drodi V4.1.1
% 28.39/9.45 % Refutation found
% 28.39/9.45 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 28.39/9.45 % SZS output start CNFRefutation for theBenchmark
% 28.39/9.45 fof(f18,axiom,(
% 28.39/9.45 (![U]: (ssList(skaf77(U)) ))),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f19,axiom,(
% 28.39/9.45 (![U]: (ssList(skaf76(U)) ))),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f20,axiom,(
% 28.39/9.45 (![U]: (ssList(skaf75(U)) ))),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f63,axiom,(
% 28.39/9.45 (![U]: (( ~ lt(U,U)| ~ ssItem(U) ) ))),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f72,axiom,(
% 28.39/9.45 (![U,V]: (( ~ ssList(U)| duplicatefreeP(U)| ssItem(V) ) ))),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f162,axiom,(
% 28.39/9.45 (![U]: (( ~ ssList(U)| duplicatefreeP(U)| app(app(skaf75(U),cons(skaf74(U),skaf76(U))),cons(skaf74(U),skaf77(U))) = U ) ))),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f181,axiom,(
% 28.39/9.45 (![U,V,W,X,Y,Z]: (( app(app(U,cons(V,W)),cons(X,Y)) != Z| ~ ssList(Y)| ~ ssList(W)| ~ ssList(U)| ~ ssItem(X)| ~ ssItem(V)| ~ strictorderedP(Z)| ~ ssList(Z)| lt(V,X) ) ))),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f186,negated_conjecture,(
% 28.39/9.45 ssList(sk1) ),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f191,negated_conjecture,(
% 28.39/9.45 sk1 = sk3 ),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f195,negated_conjecture,(
% 28.39/9.45 strictorderedP(sk3) ),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f198,negated_conjecture,(
% 28.39/9.45 ~ duplicatefreeP(sk1) ),
% 28.39/9.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.39/9.45 fof(f217,plain,(
% 28.39/9.45 ![X0]: (ssList(skaf77(X0)))),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f18])).
% 28.39/9.45 fof(f218,plain,(
% 28.39/9.45 ![X0]: (ssList(skaf76(X0)))),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f19])).
% 28.39/9.45 fof(f219,plain,(
% 28.39/9.45 ![X0]: (ssList(skaf75(X0)))),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f20])).
% 28.39/9.45 fof(f262,plain,(
% 28.39/9.45 ![X0]: (~lt(X0,X0)|~ssItem(X0))),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f63])).
% 28.39/9.45 fof(f271,plain,(
% 28.39/9.45 (![U]: (~ssList(U)|duplicatefreeP(U)))|(![V]: ssItem(V))),
% 28.39/9.45 inference(miniscoping,[status(thm)],[f72])).
% 28.39/9.45 fof(f272,plain,(
% 28.39/9.45 ![X0,X1]: (~ssList(X0)|duplicatefreeP(X0)|ssItem(X1))),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f271])).
% 28.39/9.45 fof(f392,plain,(
% 28.39/9.45 ![X0]: (~ssList(X0)|duplicatefreeP(X0)|app(app(skaf75(X0),cons(skaf74(X0),skaf76(X0))),cons(skaf74(X0),skaf77(X0)))=X0)),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f162])).
% 28.39/9.45 fof(f420,plain,(
% 28.39/9.45 ![V,X]: ((![Z]: (((((![U]: ((![W]: ((![Y]: (~app(app(U,cons(V,W)),cons(X,Y))=Z|~ssList(Y)))|~ssList(W)))|~ssList(U)))|~ssItem(X))|~ssItem(V))|~strictorderedP(Z))|~ssList(Z)))|lt(V,X))),
% 28.39/9.45 inference(miniscoping,[status(thm)],[f181])).
% 28.39/9.45 fof(f421,plain,(
% 28.39/9.45 ![X0,X1,X2,X3,X4,X5]: (~app(app(X0,cons(X1,X2)),cons(X3,X4))=X5|~ssList(X4)|~ssList(X2)|~ssList(X0)|~ssItem(X3)|~ssItem(X1)|~strictorderedP(X5)|~ssList(X5)|lt(X1,X3))),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f420])).
% 28.39/9.45 fof(f430,plain,(
% 28.39/9.45 ssList(sk1)),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f186])).
% 28.39/9.45 fof(f435,plain,(
% 28.39/9.45 sk1=sk3),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f191])).
% 28.39/9.45 fof(f439,plain,(
% 28.39/9.45 strictorderedP(sk3)),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f195])).
% 28.39/9.45 fof(f444,plain,(
% 28.39/9.45 ~duplicatefreeP(sk1)),
% 28.39/9.45 inference(cnf_transformation,[status(thm)],[f198])).
% 28.39/9.45 fof(f446,definition,(
% 28.39/9.45 ![X0]: (sQ0_spl <=> (~ssList(X0)|duplicatefreeP(X0)))),
% 28.39/9.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 28.39/9.45 fof(f447,plain,(
% 28.39/9.45 ![X0]: (~ssList(X0)|duplicatefreeP(X0)|~sQ0_spl)),
% 28.39/9.45 inference(component_clause,[status(thm)],[f446])).
% 28.39/9.45 fof(f449,definition,(
% 28.39/9.45 ![X1]: (sQ1_spl <=> (ssItem(X1)))),
% 28.39/9.45 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 28.39/9.45 fof(f450,plain,(
% 28.39/9.45 ![X0]: (ssItem(X0)|~sQ1_spl)),
% 28.39/9.45 inference(component_clause,[status(thm)],[f449])).
% 28.39/9.45 fof(f452,plain,(
% 28.39/9.45 sQ0_spl|sQ1_spl),
% 28.39/9.45 inference(split_clause,[status(thm)],[f272,f446,f449])).
% 28.39/9.45 fof(f484,plain,(
% 28.39/9.45 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X4)|~strictorderedP(app(app(X2,cons(X4,X1)),cons(X3,X0)))|~ssList(app(app(X2,cons(X4,X1)),cons(X3,X0)))|lt(X4,X3))),
% 28.39/9.45 inference(destructive_equality_resolution,[status(thm)],[f421])).
% 28.39/9.45 fof(f494,plain,(
% 28.39/9.45 strictorderedP(sk1)),
% 28.39/9.45 inference(forward_demodulation,[status(thm)],[f435,f439])).
% 28.39/9.45 fof(f539,plain,(
% 28.39/9.45 duplicatefreeP(sk1)|~sQ0_spl),
% 28.39/9.45 inference(resolution,[status(thm)],[f447,f430])).
% 28.39/9.45 fof(f540,plain,(
% 28.39/9.45 $false|~sQ0_spl),
% 28.39/9.45 inference(forward_subsumption_resolution,[status(thm)],[f539,f444])).
% 28.39/9.45 fof(f541,plain,(
% 28.39/9.45 ~sQ0_spl),
% 28.39/9.45 inference(contradiction_clause,[status(thm)],[f540])).
% 28.39/9.45 fof(f544,plain,(
% 28.39/9.45 ![X0]: (~lt(X0,X0)|~sQ1_spl)),
% 28.39/9.45 inference(backward_subsumption_resolution,[status(thm)],[f262,f450])).
% 28.39/9.45 fof(f1784,plain,(
% 28.39/9.45 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssItem(X3)|~strictorderedP(app(app(X2,cons(X3,X1)),cons(X4,X0)))|~ssList(app(app(X2,cons(X3,X1)),cons(X4,X0)))|lt(X3,X4)|~sQ1_spl)),
% 28.39/9.45 inference(forward_subsumption_resolution,[status(thm)],[f484,f450])).
% 28.39/9.45 fof(f3446,plain,(
% 28.39/9.46 duplicatefreeP(sk1)|app(app(skaf75(sk1),cons(skaf74(sk1),skaf76(sk1))),cons(skaf74(sk1),skaf77(sk1)))=sk1),
% 28.39/9.46 inference(resolution,[status(thm)],[f392,f430])).
% 28.39/9.46 fof(f3468,definition,(
% 28.39/9.46 sQ173_spl <=> (duplicatefreeP(sk1))),
% 28.39/9.46 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 28.39/9.46 fof(f3469,plain,(
% 28.39/9.46 duplicatefreeP(sk1)|~sQ173_spl),
% 28.39/9.46 inference(component_clause,[status(thm)],[f3468])).
% 28.39/9.46 fof(f3471,definition,(
% 28.39/9.46 sQ174_spl <=> (app(app(skaf75(sk1),cons(skaf74(sk1),skaf76(sk1))),cons(skaf74(sk1),skaf77(sk1)))=sk1)),
% 28.39/9.46 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 28.39/9.46 fof(f3472,plain,(
% 28.39/9.46 app(app(skaf75(sk1),cons(skaf74(sk1),skaf76(sk1))),cons(skaf74(sk1),skaf77(sk1)))=sk1|~sQ174_spl),
% 28.39/9.46 inference(component_clause,[status(thm)],[f3471])).
% 28.39/9.46 fof(f3474,plain,(
% 28.39/9.46 sQ173_spl|sQ174_spl),
% 28.39/9.46 inference(split_clause,[status(thm)],[f3446,f3468,f3471])).
% 28.39/9.46 fof(f3475,plain,(
% 28.39/9.46 $false|~sQ173_spl),
% 28.39/9.46 inference(forward_subsumption_resolution,[status(thm)],[f3469,f444])).
% 28.39/9.46 fof(f3476,plain,(
% 28.39/9.46 ~sQ173_spl),
% 28.39/9.46 inference(contradiction_clause,[status(thm)],[f3475])).
% 28.39/9.46 fof(f3833,definition,(
% 28.39/9.46 sQ221_spl <=> (strictorderedP(sk1))),
% 28.39/9.46 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 28.39/9.46 fof(f3835,plain,(
% 28.39/9.46 ~strictorderedP(sk1)|sQ221_spl),
% 28.39/9.46 inference(component_clause,[status(thm)],[f3833])).
% 28.39/9.46 fof(f23909,plain,(
% 28.39/9.46 ~ssList(skaf77(sk1))|~ssList(skaf76(sk1))|~ssList(skaf75(sk1))|~ssItem(skaf74(sk1))|~strictorderedP(sk1)|~ssList(app(app(skaf75(sk1),cons(skaf74(sk1),skaf76(sk1))),cons(skaf74(sk1),skaf77(sk1))))|lt(skaf74(sk1),skaf74(sk1))|~sQ1_spl|~sQ174_spl),
% 28.39/9.46 inference(paramodulation,[status(thm)],[f3472,f1784])).
% 28.39/9.46 fof(f23933,definition,(
% 28.39/9.46 sQ1151_spl <=> (ssList(skaf77(sk1)))),
% 28.39/9.46 introduced(definition,[new_symbols(definition,[sQ1151_spl])],[split_symbol_definition])).
% 28.39/9.46 fof(f23935,plain,(
% 28.39/9.46 ~ssList(skaf77(sk1))|sQ1151_spl),
% 28.39/9.46 inference(component_clause,[status(thm)],[f23933])).
% 28.39/9.46 fof(f23936,definition,(
% 28.39/9.46 sQ1152_spl <=> (ssList(skaf76(sk1)))),
% 28.39/9.46 introduced(definition,[new_symbols(definition,[sQ1152_spl])],[split_symbol_definition])).
% 28.39/9.46 fof(f23938,plain,(
% 28.39/9.46 ~ssList(skaf76(sk1))|sQ1152_spl),
% 28.39/9.46 inference(component_clause,[status(thm)],[f23936])).
% 28.39/9.46 fof(f23939,definition,(
% 28.39/9.46 sQ1153_spl <=> (ssList(skaf75(sk1)))),
% 28.39/9.46 introduced(definition,[new_symbols(definition,[sQ1153_spl])],[split_symbol_definition])).
% 28.39/9.46 fof(f23941,plain,(
% 28.39/9.46 ~ssList(skaf75(sk1))|sQ1153_spl),
% 28.39/9.46 inference(component_clause,[status(thm)],[f23939])).
% 28.39/9.46 fof(f23942,definition,(
% 28.39/9.46 sQ1154_spl <=> (ssItem(skaf74(sk1)))),
% 28.39/9.46 introduced(definition,[new_symbols(definition,[sQ1154_spl])],[split_symbol_definition])).
% 28.39/9.46 fof(f23944,plain,(
% 28.39/9.46 ~ssItem(skaf74(sk1))|sQ1154_spl),
% 28.39/9.46 inference(component_clause,[status(thm)],[f23942])).
% 28.39/9.46 fof(f23945,definition,(
% 28.39/9.46 sQ1155_spl <=> (ssList(app(app(skaf75(sk1),cons(skaf74(sk1),skaf76(sk1))),cons(skaf74(sk1),skaf77(sk1)))))),
% 28.39/9.46 introduced(definition,[new_symbols(definition,[sQ1155_spl])],[split_symbol_definition])).
% 28.39/9.46 fof(f23947,plain,(
% 28.39/9.46 ~ssList(app(app(skaf75(sk1),cons(skaf74(sk1),skaf76(sk1))),cons(skaf74(sk1),skaf77(sk1))))|sQ1155_spl),
% 30.30/9.50 inference(component_clause,[status(thm)],[f23945])).
% 30.30/9.50 fof(f23950,definition,(
% 30.30/9.50 sQ1156_spl <=> (lt(skaf74(sk1),skaf74(sk1)))),
% 30.30/9.50 introduced(definition,[new_symbols(definition,[sQ1156_spl])],[split_symbol_definition])).
% 30.30/9.50 fof(f23951,plain,(
% 30.30/9.50 lt(skaf74(sk1),skaf74(sk1))|~sQ1156_spl),
% 30.30/9.50 inference(component_clause,[status(thm)],[f23950])).
% 30.30/9.50 fof(f23955,plain,(
% 30.30/9.50 ~sQ1151_spl|~sQ1152_spl|~sQ1153_spl|~sQ1154_spl|~sQ221_spl|~sQ1155_spl|sQ1156_spl|~sQ1_spl|~sQ174_spl),
% 30.30/9.50 inference(split_clause,[status(thm)],[f23909,f23933,f23936,f23939,f23942,f3833,f23945,f23950,f449,f3471])).
% 30.30/9.50 fof(f24033,plain,(
% 30.30/9.50 $false|sQ1151_spl),
% 30.30/9.50 inference(forward_subsumption_resolution,[status(thm)],[f23935,f217])).
% 30.30/9.50 fof(f24034,plain,(
% 30.30/9.50 sQ1151_spl),
% 30.30/9.50 inference(contradiction_clause,[status(thm)],[f24033])).
% 30.30/9.50 fof(f24035,plain,(
% 30.30/9.50 $false|~sQ1_spl|sQ1154_spl),
% 30.30/9.50 inference(forward_subsumption_resolution,[status(thm)],[f23944,f450])).
% 30.30/9.50 fof(f24036,plain,(
% 30.30/9.50 ~sQ1_spl|sQ1154_spl),
% 30.30/9.50 inference(contradiction_clause,[status(thm)],[f24035])).
% 30.30/9.50 fof(f24037,plain,(
% 30.30/9.50 $false|sQ1153_spl),
% 30.30/9.50 inference(forward_subsumption_resolution,[status(thm)],[f23941,f219])).
% 30.30/9.50 fof(f24038,plain,(
% 30.30/9.50 sQ1153_spl),
% 30.30/9.50 inference(contradiction_clause,[status(thm)],[f24037])).
% 30.30/9.50 fof(f24039,plain,(
% 30.30/9.50 ~ssList(sk1)|~sQ174_spl|sQ1155_spl),
% 30.30/9.50 inference(forward_demodulation,[status(thm)],[f3472,f23947])).
% 30.30/9.50 fof(f24040,plain,(
% 30.30/9.50 $false|~sQ174_spl|sQ1155_spl),
% 30.30/9.50 inference(forward_subsumption_resolution,[status(thm)],[f24039,f430])).
% 30.30/9.50 fof(f24041,plain,(
% 30.30/9.50 ~sQ174_spl|sQ1155_spl),
% 30.30/9.50 inference(contradiction_clause,[status(thm)],[f24040])).
% 30.30/9.50 fof(f24042,plain,(
% 30.30/9.50 $false|sQ1152_spl),
% 30.30/9.50 inference(forward_subsumption_resolution,[status(thm)],[f23938,f218])).
% 30.30/9.50 fof(f24043,plain,(
% 30.30/9.50 sQ1152_spl),
% 30.30/9.50 inference(contradiction_clause,[status(thm)],[f24042])).
% 30.30/9.50 fof(f24045,plain,(
% 30.30/9.50 $false|~sQ1_spl|~sQ1156_spl),
% 30.30/9.50 inference(forward_subsumption_resolution,[status(thm)],[f23951,f544])).
% 30.30/9.50 fof(f24046,plain,(
% 30.30/9.50 ~sQ1_spl|~sQ1156_spl),
% 30.30/9.50 inference(contradiction_clause,[status(thm)],[f24045])).
% 30.30/9.50 fof(f24049,plain,(
% 30.30/9.50 $false|sQ221_spl),
% 30.30/9.50 inference(forward_subsumption_resolution,[status(thm)],[f3835,f494])).
% 30.30/9.50 fof(f24050,plain,(
% 30.30/9.50 sQ221_spl),
% 30.30/9.50 inference(contradiction_clause,[status(thm)],[f24049])).
% 30.30/9.50 fof(f24051,plain,(
% 30.30/9.50 $false),
% 30.30/9.50 inference(sat_refutation,[status(thm)],[f452,f541,f3474,f3476,f23955,f24034,f24036,f24038,f24041,f24043,f24046,f24050])).
% 30.30/9.50 % SZS output end CNFRefutation for theBenchmark.p
% 30.30/9.53 % Elapsed time: 3.926031 seconds
% 30.30/9.53 % CPU time: 30.826596 seconds
% 30.30/9.53 % Total memory used: 495.241 MB
% 30.30/9.53 % Net memory used: 466.922 MB
%------------------------------------------------------------------------------