%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR094+5 : TPTP v9.3.1. Bugfixed v7.3.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 12:15:10 PM UTC 2026
% Result : Theorem 209.02s 27.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR094+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.49 % Computer : n017.cluster.edu
% 0.18/0.49 % Model : x86_64 x86_64
% 0.18/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.49 % Memory : 8046.5625MB
% 0.18/0.49 % OS : Linux 6.8.0-71-generic
% 0.18/0.49 % CPULimit : 300
% 0.18/0.49 % WCLimit : 300
% 0.18/0.49 % DateTime : Mon Sep 21 14:51:27 UTC 2026
% 0.18/0.49 % CPUTime :
% 0.67/1.06 % Drodi V4.1.1
% 209.02/27.48 % Refutation found
% 209.02/27.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 209.02/27.48 % SZS output start CNFRefutation for theBenchmark
% 209.02/27.48 fof(f26,axiom,(
% 209.02/27.48 (! [V__X,V__Y] :( s__subclass(V__X,V__Y)=> ( s__instance(V__X,s__SetOrClass)& s__instance(V__Y,s__SetOrClass) ) ) )),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f27,axiom,(
% 209.02/27.48 (! [V__X,V__Y,V__Z] :( ( s__instance(V__Y,s__SetOrClass)& s__instance(V__X,s__SetOrClass) )=> ( ( s__subclass(V__X,V__Y)& s__instance(V__Z,V__X) )=> s__instance(V__Z,V__Y) ) ) )),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f7048,axiom,(
% 209.02/27.48 s__subclass(s__OrganicObject,s__CorpuscularObject) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f7055,axiom,(
% 209.02/27.48 s__subclass(s__Organism,s__OrganicObject) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f7100,axiom,(
% 209.02/27.48 s__subclass(s__Animal,s__Organism) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f7117,axiom,(
% 209.02/27.48 s__subclass(s__Vertebrate,s__Animal) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f7150,axiom,(
% 209.02/27.48 s__subclass(s__WarmBloodedVertebrate,s__Vertebrate) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f7166,axiom,(
% 209.02/27.48 s__subclass(s__Mammal,s__WarmBloodedVertebrate) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f7179,axiom,(
% 209.02/27.48 s__subclass(s__Carnivore,s__Mammal) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f7182,axiom,(
% 209.02/27.48 s__subclass(s__Canine,s__Carnivore) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f16749,axiom,(
% 209.02/27.48 s__instance(s__Rover24_1,s__Canine) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f16750,conjecture,(
% 209.02/27.48 s__instance(s__Rover24_1,s__CorpuscularObject) ),
% 209.02/27.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 209.02/27.48 fof(f16751,negated_conjecture,(
% 209.02/27.48 ~(s__instance(s__Rover24_1,s__CorpuscularObject) )),
% 209.02/27.48 inference(negated_conjecture,[status(cth)],[f16750])).
% 209.02/27.48 fof(f16791,plain,(
% 209.02/27.48 ![V__X,V__Y]: (~s__subclass(V__X,V__Y)|(s__instance(V__X,s__SetOrClass)&s__instance(V__Y,s__SetOrClass)))),
% 209.02/27.48 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 209.02/27.48 fof(f16792,plain,(
% 209.02/27.48 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X0,s__SetOrClass))),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f16791])).
% 209.02/27.48 fof(f16793,plain,(
% 209.02/27.48 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X1,s__SetOrClass))),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f16791])).
% 209.02/27.48 fof(f16794,plain,(
% 209.02/27.48 ![V__X,V__Y,V__Z]: ((~s__instance(V__Y,s__SetOrClass)|~s__instance(V__X,s__SetOrClass))|((~s__subclass(V__X,V__Y)|~s__instance(V__Z,V__X))|s__instance(V__Z,V__Y)))),
% 209.02/27.48 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 209.02/27.48 fof(f16795,plain,(
% 209.02/27.48 ![V__X,V__Y]: ((~s__instance(V__Y,s__SetOrClass)|~s__instance(V__X,s__SetOrClass))|(![V__Z]: ((~s__subclass(V__X,V__Y)|~s__instance(V__Z,V__X))|s__instance(V__Z,V__Y))))),
% 209.02/27.48 inference(miniscoping,[status(thm)],[f16794])).
% 209.02/27.48 fof(f16796,plain,(
% 209.02/27.48 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__subclass(X1,X0)|~s__instance(X2,X1)|s__instance(X2,X0))),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f16795])).
% 209.02/27.48 fof(f29313,plain,(
% 209.02/27.48 s__subclass(s__OrganicObject,s__CorpuscularObject)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f7048])).
% 209.02/27.48 fof(f29320,plain,(
% 209.02/27.48 s__subclass(s__Organism,s__OrganicObject)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f7055])).
% 209.02/27.48 fof(f29374,plain,(
% 209.02/27.48 s__subclass(s__Animal,s__Organism)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f7100])).
% 209.02/27.48 fof(f29402,plain,(
% 209.02/27.48 s__subclass(s__Vertebrate,s__Animal)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f7117])).
% 209.02/27.48 fof(f29435,plain,(
% 209.02/27.48 s__subclass(s__WarmBloodedVertebrate,s__Vertebrate)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f7150])).
% 209.02/27.48 fof(f29455,plain,(
% 209.02/27.48 s__subclass(s__Mammal,s__WarmBloodedVertebrate)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f7166])).
% 209.02/27.48 fof(f29468,plain,(
% 209.02/27.48 s__subclass(s__Carnivore,s__Mammal)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f7179])).
% 209.02/27.48 fof(f29473,plain,(
% 209.02/27.48 s__subclass(s__Canine,s__Carnivore)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f7182])).
% 209.02/27.48 fof(f44204,plain,(
% 209.02/27.48 s__instance(s__Rover24_1,s__Canine)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f16749])).
% 209.02/27.48 fof(f44205,plain,(
% 209.02/27.48 ~s__instance(s__Rover24_1,s__CorpuscularObject)),
% 209.02/27.48 inference(cnf_transformation,[status(thm)],[f16751])).
% 209.02/27.48 fof(f44548,plain,(
% 209.02/27.48 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,X1)|~s__instance(X2,X0)|s__instance(X2,X1))),
% 209.02/27.48 inference(forward_subsumption_resolution,[status(thm)],[f16796,f16793])).
% 209.02/27.48 fof(f44625,plain,(
% 209.02/27.48 ![X0]: (~s__instance(s__Canine,s__SetOrClass)|~s__subclass(s__Canine,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(resolution,[status(thm)],[f44548,f44204])).
% 209.02/27.48 fof(f44691,plain,(
% 209.02/27.48 ![X0]: (~s__subclass(s__Canine,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(forward_subsumption_resolution,[status(thm)],[f44625,f16792])).
% 209.02/27.48 fof(f131310,plain,(
% 209.02/27.48 s__instance(s__Rover24_1,s__Carnivore)),
% 209.02/27.48 inference(resolution,[status(thm)],[f29473,f44691])).
% 209.02/27.48 fof(f131686,plain,(
% 209.02/27.48 ![X0]: (~s__instance(s__Carnivore,s__SetOrClass)|~s__subclass(s__Carnivore,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(resolution,[status(thm)],[f131310,f44548])).
% 209.02/27.48 fof(f131689,plain,(
% 209.02/27.48 ![X0]: (~s__subclass(s__Carnivore,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(forward_subsumption_resolution,[status(thm)],[f131686,f16792])).
% 209.02/27.48 fof(f131690,plain,(
% 209.02/27.48 s__instance(s__Rover24_1,s__Mammal)),
% 209.02/27.48 inference(resolution,[status(thm)],[f131689,f29468])).
% 209.02/27.48 fof(f131733,plain,(
% 209.02/27.48 ![X0]: (~s__instance(s__Mammal,s__SetOrClass)|~s__subclass(s__Mammal,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(resolution,[status(thm)],[f131690,f44548])).
% 209.02/27.48 fof(f131736,plain,(
% 209.02/27.48 ![X0]: (~s__subclass(s__Mammal,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(forward_subsumption_resolution,[status(thm)],[f131733,f16792])).
% 209.02/27.48 fof(f131737,plain,(
% 209.02/27.48 s__instance(s__Rover24_1,s__WarmBloodedVertebrate)),
% 209.02/27.48 inference(resolution,[status(thm)],[f131736,f29455])).
% 209.02/27.48 fof(f131780,plain,(
% 209.02/27.48 ![X0]: (~s__instance(s__WarmBloodedVertebrate,s__SetOrClass)|~s__subclass(s__WarmBloodedVertebrate,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(resolution,[status(thm)],[f131737,f44548])).
% 209.02/27.48 fof(f131783,plain,(
% 209.02/27.48 ![X0]: (~s__subclass(s__WarmBloodedVertebrate,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(forward_subsumption_resolution,[status(thm)],[f131780,f16792])).
% 209.02/27.48 fof(f131784,plain,(
% 209.02/27.48 s__instance(s__Rover24_1,s__Vertebrate)),
% 209.02/27.48 inference(resolution,[status(thm)],[f131783,f29435])).
% 209.02/27.48 fof(f131827,plain,(
% 209.02/27.48 ![X0]: (~s__instance(s__Vertebrate,s__SetOrClass)|~s__subclass(s__Vertebrate,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(resolution,[status(thm)],[f131784,f44548])).
% 209.02/27.48 fof(f131830,plain,(
% 209.02/27.48 ![X0]: (~s__subclass(s__Vertebrate,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(forward_subsumption_resolution,[status(thm)],[f131827,f16792])).
% 209.02/27.48 fof(f131831,plain,(
% 209.02/27.48 s__instance(s__Rover24_1,s__Animal)),
% 209.02/27.48 inference(resolution,[status(thm)],[f131830,f29402])).
% 209.02/27.48 fof(f131876,plain,(
% 209.02/27.48 ![X0]: (~s__instance(s__Animal,s__SetOrClass)|~s__subclass(s__Animal,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(resolution,[status(thm)],[f131831,f44548])).
% 209.02/27.48 fof(f131879,plain,(
% 209.02/27.48 ![X0]: (~s__subclass(s__Animal,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(forward_subsumption_resolution,[status(thm)],[f131876,f16792])).
% 209.02/27.48 fof(f131880,plain,(
% 209.02/27.48 s__instance(s__Rover24_1,s__Organism)),
% 209.02/27.48 inference(resolution,[status(thm)],[f131879,f29374])).
% 209.02/27.48 fof(f131959,plain,(
% 209.02/27.48 ![X0]: (~s__instance(s__Organism,s__SetOrClass)|~s__subclass(s__Organism,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(resolution,[status(thm)],[f131880,f44548])).
% 209.02/27.48 fof(f131962,plain,(
% 209.02/27.48 ![X0]: (~s__subclass(s__Organism,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(forward_subsumption_resolution,[status(thm)],[f131959,f16792])).
% 209.02/27.48 fof(f131964,plain,(
% 209.02/27.48 s__instance(s__Rover24_1,s__OrganicObject)),
% 209.02/27.48 inference(resolution,[status(thm)],[f131962,f29320])).
% 209.02/27.48 fof(f132643,plain,(
% 209.02/27.48 ![X0]: (~s__instance(s__OrganicObject,s__SetOrClass)|~s__subclass(s__OrganicObject,X0)|s__instance(s__Rover24_1,X0))),
% 209.02/27.48 inference(resolution,[status(thm)],[f131964,f44548])).
% 209.02/27.48 fof(f132646,plain,(
% 174.55/27.67 ![X0]: (~s__subclass(s__OrganicObject,X0)|s__instance(s__Rover24_1,X0))),
% 174.55/27.67 inference(forward_subsumption_resolution,[status(thm)],[f132643,f16792])).
% 174.55/27.67 fof(f132806,plain,(
% 174.55/27.67 s__instance(s__Rover24_1,s__CorpuscularObject)),
% 174.55/27.67 inference(resolution,[status(thm)],[f132646,f29313])).
% 174.55/27.67 fof(f132807,plain,(
% 174.55/27.67 $false),
% 174.55/27.67 inference(forward_subsumption_resolution,[status(thm)],[f132806,f44205])).
% 174.55/27.67 % SZS output end CNFRefutation for theBenchmark.p
% 8.42/27.86 % Elapsed time: 27.334854 seconds
% 8.42/27.86 % CPU time: 210.296578 seconds
% 8.42/27.86 % Total memory used: 1.462 GB
% 8.42/27.86 % Net memory used: 1.433 GB
%------------------------------------------------------------------------------