%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU275+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:22:12 PM UTC 2026
% Result : Theorem 46.04s 6.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU275+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n026.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 06:09:24 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.48 % Drodi V4.1.1
% 46.04/6.36 % Refutation found
% 46.04/6.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 46.04/6.36 % SZS output start CNFRefutation for theBenchmark
% 46.04/6.36 fof(f56,axiom,(
% 46.04/6.36 (! [A] :( relation(A)=> ( well_ordering(A)<=> ( reflexive(A)& transitive(A)& antisymmetric(A)& connected(A)& well_founded_relation(A) ) ) ) )),
% 46.04/6.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.04/6.36 fof(f86,axiom,(
% 46.04/6.36 (! [A] : relation(inclusion_relation(A)) )),
% 46.04/6.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.04/6.36 fof(f262,lemma,(
% 46.04/6.36 (! [A] : reflexive(inclusion_relation(A)) )),
% 46.04/6.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.04/6.36 fof(f285,lemma,(
% 46.04/6.36 (! [A] : transitive(inclusion_relation(A)) )),
% 46.04/6.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.04/6.36 fof(f305,lemma,(
% 46.04/6.36 (! [A] :( ordinal(A)=> connected(inclusion_relation(A)) ) )),
% 46.04/6.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.04/6.36 fof(f317,lemma,(
% 46.04/6.36 (! [A] : antisymmetric(inclusion_relation(A)) )),
% 46.04/6.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.04/6.36 fof(f328,lemma,(
% 46.04/6.36 (! [A] :( ordinal(A)=> well_founded_relation(inclusion_relation(A)) ) )),
% 46.04/6.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.04/6.36 fof(f337,conjecture,(
% 46.04/6.36 (! [A] :( ordinal(A)=> well_ordering(inclusion_relation(A)) ) )),
% 46.04/6.36 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.04/6.36 fof(f338,negated_conjecture,(
% 46.04/6.36 ~((! [A] :( ordinal(A)=> well_ordering(inclusion_relation(A)) ) ))),
% 46.04/6.36 inference(negated_conjecture,[status(cth)],[f337])).
% 46.04/6.36 fof(f704,plain,(
% 46.04/6.36 ![A]: (~relation(A)|(well_ordering(A)<=>((((reflexive(A)&transitive(A))&antisymmetric(A))&connected(A))&well_founded_relation(A))))),
% 46.04/6.36 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 46.04/6.36 fof(f705,plain,(
% 46.04/6.36 ![A]: (~relation(A)|((~well_ordering(A)|((((reflexive(A)&transitive(A))&antisymmetric(A))&connected(A))&well_founded_relation(A)))&(well_ordering(A)|((((~reflexive(A)|~transitive(A))|~antisymmetric(A))|~connected(A))|~well_founded_relation(A)))))),
% 46.04/6.36 inference(NNF_transformation,[status(thm)],[f704])).
% 46.04/6.36 fof(f711,plain,(
% 46.04/6.36 ![X0]: (~relation(X0)|well_ordering(X0)|~reflexive(X0)|~transitive(X0)|~antisymmetric(X0)|~connected(X0)|~well_founded_relation(X0))),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f705])).
% 46.04/6.36 fof(f842,plain,(
% 46.04/6.36 ![X0]: (relation(inclusion_relation(X0)))),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f86])).
% 46.04/6.36 fof(f1351,plain,(
% 46.04/6.36 ![X0]: (reflexive(inclusion_relation(X0)))),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f262])).
% 46.04/6.36 fof(f1427,plain,(
% 46.04/6.36 ![X0]: (transitive(inclusion_relation(X0)))),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f285])).
% 46.04/6.36 fof(f1478,plain,(
% 46.04/6.36 ![A]: (~ordinal(A)|connected(inclusion_relation(A)))),
% 46.04/6.36 inference(pre_NNF_transformation,[status(thm)],[f305])).
% 46.04/6.36 fof(f1479,plain,(
% 46.04/6.36 ![X0]: (~ordinal(X0)|connected(inclusion_relation(X0)))),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f1478])).
% 46.04/6.36 fof(f1528,plain,(
% 46.04/6.36 ![X0]: (antisymmetric(inclusion_relation(X0)))),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f317])).
% 46.04/6.36 fof(f1560,plain,(
% 46.04/6.36 ![A]: (~ordinal(A)|well_founded_relation(inclusion_relation(A)))),
% 46.04/6.36 inference(pre_NNF_transformation,[status(thm)],[f328])).
% 46.04/6.36 fof(f1561,plain,(
% 46.04/6.36 ![X0]: (~ordinal(X0)|well_founded_relation(inclusion_relation(X0)))),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f1560])).
% 46.04/6.36 fof(f1590,plain,(
% 46.04/6.36 (?[A]: (ordinal(A)&~well_ordering(inclusion_relation(A))))),
% 46.04/6.36 inference(pre_NNF_transformation,[status(thm)],[f338])).
% 46.04/6.36 fof(f1591,plain,(
% 46.04/6.36 (ordinal(sK143_skl)&~well_ordering(inclusion_relation(sK143_skl)))),
% 46.04/6.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK143_skl]),skolemize(A,sK143_skl)],[f1590])).
% 46.04/6.36 fof(f1592,plain,(
% 46.04/6.36 ordinal(sK143_skl)),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f1591])).
% 46.04/6.36 fof(f1593,plain,(
% 46.04/6.36 ~well_ordering(inclusion_relation(sK143_skl))),
% 46.04/6.36 inference(cnf_transformation,[status(thm)],[f1591])).
% 46.04/6.36 fof(f1717,plain,(
% 46.04/6.36 well_founded_relation(inclusion_relation(sK143_skl))),
% 46.04/6.36 inference(resolution,[status(thm)],[f1561,f1592])).
% 46.04/6.36 fof(f2418,plain,(
% 46.04/6.36 connected(inclusion_relation(sK143_skl))),
% 46.04/6.36 inference(resolution,[status(thm)],[f1592,f1479])).
% 46.04/6.36 fof(f7945,plain,(
% 46.04/6.36 ![X0]: (~relation(inclusion_relation(X0))|well_ordering(inclusion_relation(X0))|~transitive(inclusion_relation(X0))|~antisymmetric(inclusion_relation(X0))|~connected(inclusion_relation(X0))|~well_founded_relation(inclusion_relation(X0)))),
% 22.42/6.40 inference(resolution,[status(thm)],[f711,f1351])).
% 22.42/6.40 fof(f7946,plain,(
% 22.42/6.40 ![X0]: (well_ordering(inclusion_relation(X0))|~transitive(inclusion_relation(X0))|~antisymmetric(inclusion_relation(X0))|~connected(inclusion_relation(X0))|~well_founded_relation(inclusion_relation(X0)))),
% 22.42/6.40 inference(forward_subsumption_resolution,[status(thm)],[f7945,f842])).
% 22.42/6.40 fof(f13073,plain,(
% 22.42/6.40 ![X0]: (well_ordering(inclusion_relation(X0))|~antisymmetric(inclusion_relation(X0))|~connected(inclusion_relation(X0))|~well_founded_relation(inclusion_relation(X0)))),
% 22.42/6.40 inference(forward_subsumption_resolution,[status(thm)],[f7946,f1427])).
% 22.42/6.40 fof(f13074,plain,(
% 22.42/6.40 well_ordering(inclusion_relation(sK143_skl))|~antisymmetric(inclusion_relation(sK143_skl))|~connected(inclusion_relation(sK143_skl))),
% 22.42/6.40 inference(resolution,[status(thm)],[f13073,f1717])).
% 22.42/6.40 fof(f13078,definition,(
% 22.42/6.40 sQ827_spl <=> (well_ordering(inclusion_relation(sK143_skl)))),
% 22.42/6.40 introduced(definition,[new_symbols(definition,[sQ827_spl])],[split_symbol_definition])).
% 22.42/6.40 fof(f13079,plain,(
% 22.42/6.40 well_ordering(inclusion_relation(sK143_skl))|~sQ827_spl),
% 22.42/6.40 inference(component_clause,[status(thm)],[f13078])).
% 22.42/6.40 fof(f13081,definition,(
% 22.42/6.40 sQ828_spl <=> (antisymmetric(inclusion_relation(sK143_skl)))),
% 22.42/6.40 introduced(definition,[new_symbols(definition,[sQ828_spl])],[split_symbol_definition])).
% 22.42/6.40 fof(f13083,plain,(
% 22.42/6.40 ~antisymmetric(inclusion_relation(sK143_skl))|sQ828_spl),
% 22.42/6.40 inference(component_clause,[status(thm)],[f13081])).
% 22.42/6.40 fof(f13084,definition,(
% 22.42/6.40 sQ829_spl <=> (connected(inclusion_relation(sK143_skl)))),
% 22.42/6.40 introduced(definition,[new_symbols(definition,[sQ829_spl])],[split_symbol_definition])).
% 22.42/6.40 fof(f13086,plain,(
% 22.42/6.40 ~connected(inclusion_relation(sK143_skl))|sQ829_spl),
% 22.42/6.40 inference(component_clause,[status(thm)],[f13084])).
% 22.42/6.40 fof(f13087,plain,(
% 22.42/6.40 sQ827_spl|~sQ828_spl|~sQ829_spl),
% 22.42/6.40 inference(split_clause,[status(thm)],[f13074,f13078,f13081,f13084])).
% 22.42/6.40 fof(f13127,plain,(
% 22.42/6.40 $false|sQ829_spl),
% 22.42/6.40 inference(forward_subsumption_resolution,[status(thm)],[f13086,f2418])).
% 22.42/6.40 fof(f13128,plain,(
% 22.42/6.40 sQ829_spl),
% 22.42/6.40 inference(contradiction_clause,[status(thm)],[f13127])).
% 22.42/6.40 fof(f13129,plain,(
% 22.42/6.40 $false|sQ828_spl),
% 22.42/6.40 inference(forward_subsumption_resolution,[status(thm)],[f13083,f1528])).
% 22.42/6.40 fof(f13130,plain,(
% 22.42/6.40 sQ828_spl),
% 22.42/6.40 inference(contradiction_clause,[status(thm)],[f13129])).
% 22.42/6.40 fof(f13131,plain,(
% 22.42/6.40 $false|~sQ827_spl),
% 22.42/6.40 inference(forward_subsumption_resolution,[status(thm)],[f13079,f1593])).
% 22.42/6.40 fof(f13132,plain,(
% 22.42/6.40 ~sQ827_spl),
% 22.42/6.40 inference(contradiction_clause,[status(thm)],[f13131])).
% 22.42/6.40 fof(f13133,plain,(
% 22.42/6.40 $false),
% 22.42/6.40 inference(sat_refutation,[status(thm)],[f13087,f13128,f13130,f13132])).
% 22.42/6.40 % SZS output end CNFRefutation for theBenchmark.p
% 22.42/6.43 % Elapsed time: 5.981672 seconds
% 22.42/6.43 % CPU time: 46.594787 seconds
% 22.42/6.43 % Total memory used: 344.381 MB
% 22.42/6.43 % Net memory used: 315.001 MB
%------------------------------------------------------------------------------