%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR101+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:13 PM UTC 2026
% Result : Theorem 89.99s 12.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR101+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.58 % Computer : n004.cluster.edu
% 0.08/0.58 % Model : x86_64 x86_64
% 0.08/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.58 % Memory : 8046.5625MB
% 0.08/0.58 % OS : Linux 6.8.0-71-generic
% 0.08/0.58 % CPULimit : 300
% 0.08/0.58 % WCLimit : 300
% 0.08/0.58 % DateTime : Mon Sep 21 14:58:35 UTC 2026
% 0.08/0.58 % CPUTime :
% 0.14/0.85 % Drodi V4.1.1
% 89.99/12.41 % Refutation found
% 89.99/12.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 89.99/12.41 % SZS output start CNFRefutation for theBenchmark
% 89.99/12.41 fof(f26,axiom,(
% 89.99/12.41 (! [V__X,V__Y] :( s__subclass(V__X,V__Y)=> ( s__instance(V__X,s__SetOrClass)& s__instance(V__Y,s__SetOrClass) ) ) )),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f27,axiom,(
% 89.99/12.41 (! [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) ) ) )),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f1217,axiom,(
% 89.99/12.41 (! [V__INST1,V__INST2] :( ( s__instance(V__INST2,s__SetOrClass)& s__instance(V__INST1,s__SetOrClass) )=> ( ( s__subclass(V__INST1,V__INST2)& s__subclass(V__INST2,V__INST1) )=> V__INST1 = V__INST2 ) ) )),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f1291,axiom,(
% 89.99/12.41 (! [V__INST1,V__INST2,V__INST3] :( ( s__instance(V__INST3,s__SetOrClass)& s__instance(V__INST2,s__SetOrClass)& s__instance(V__INST1,s__SetOrClass) )=> ( ( s__subclass(V__INST1,V__INST2)& s__subclass(V__INST2,V__INST3) )=> s__subclass(V__INST1,V__INST3) ) ) )),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f7222,axiom,(
% 89.99/12.41 s__subclass(s__Class32_2,s__Animal) ),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f7224,axiom,(
% 89.99/12.41 s__subclass(s__Class32_1,s__Class32_2) ),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f7225,axiom,(
% 89.99/12.41 s__subclass(s__Class32_2,s__Class32_3) ),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f7226,axiom,(
% 89.99/12.41 s__subclass(s__Class32_3,s__Class32_1) ),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f7227,conjecture,(
% 89.99/12.41 (! [V_X] :( s__instance(V_X,s__Class32_2)=> s__instance(V_X,s__Class32_1) ) )),
% 89.99/12.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 89.99/12.41 fof(f7228,negated_conjecture,(
% 89.99/12.41 ~((! [V_X] :( s__instance(V_X,s__Class32_2)=> s__instance(V_X,s__Class32_1) ) ))),
% 89.99/12.41 inference(negated_conjecture,[status(cth)],[f7227])).
% 89.99/12.41 fof(f7268,plain,(
% 89.99/12.41 ![V__X,V__Y]: (~s__subclass(V__X,V__Y)|(s__instance(V__X,s__SetOrClass)&s__instance(V__Y,s__SetOrClass)))),
% 89.99/12.41 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 89.99/12.41 fof(f7269,plain,(
% 89.99/12.41 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X0,s__SetOrClass))),
% 89.99/12.41 inference(cnf_transformation,[status(thm)],[f7268])).
% 89.99/12.41 fof(f7270,plain,(
% 89.99/12.41 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X1,s__SetOrClass))),
% 89.99/12.41 inference(cnf_transformation,[status(thm)],[f7268])).
% 89.99/12.41 fof(f7271,plain,(
% 89.99/12.41 ![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)))),
% 89.99/12.41 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 89.99/12.41 fof(f7272,plain,(
% 89.99/12.41 ![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))))),
% 89.99/12.41 inference(miniscoping,[status(thm)],[f7271])).
% 89.99/12.41 fof(f7273,plain,(
% 89.99/12.41 ![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))),
% 89.99/12.41 inference(cnf_transformation,[status(thm)],[f7272])).
% 89.99/12.41 fof(f9522,plain,(
% 89.99/12.41 ![V__INST1,V__INST2]: ((~s__instance(V__INST2,s__SetOrClass)|~s__instance(V__INST1,s__SetOrClass))|((~s__subclass(V__INST1,V__INST2)|~s__subclass(V__INST2,V__INST1))|V__INST1=V__INST2))),
% 89.99/12.41 inference(pre_NNF_transformation,[status(thm)],[f1217])).
% 89.99/12.41 fof(f9523,plain,(
% 89.99/12.41 ![X0,X1]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__subclass(X1,X0)|~s__subclass(X0,X1)|X1=X0)),
% 89.99/12.41 inference(cnf_transformation,[status(thm)],[f9522])).
% 89.99/12.41 fof(f9665,plain,(
% 89.99/12.41 ![V__INST1,V__INST2,V__INST3]: (((~s__instance(V__INST3,s__SetOrClass)|~s__instance(V__INST2,s__SetOrClass))|~s__instance(V__INST1,s__SetOrClass))|((~s__subclass(V__INST1,V__INST2)|~s__subclass(V__INST2,V__INST3))|s__subclass(V__INST1,V__INST3)))),
% 89.99/12.41 inference(pre_NNF_transformation,[status(thm)],[f1291])).
% 89.99/12.41 fof(f9666,plain,(
% 89.99/12.41 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__instance(X2,s__SetOrClass)|~s__subclass(X2,X1)|~s__subclass(X1,X0)|s__subclass(X2,X0))),
% 91.80/12.51 inference(cnf_transformation,[status(thm)],[f9665])).
% 91.80/12.51 fof(f19232,plain,(
% 91.80/12.51 s__subclass(s__Class32_2,s__Animal)),
% 91.80/12.51 inference(cnf_transformation,[status(thm)],[f7222])).
% 91.80/12.51 fof(f19234,plain,(
% 91.80/12.51 s__subclass(s__Class32_1,s__Class32_2)),
% 91.80/12.51 inference(cnf_transformation,[status(thm)],[f7224])).
% 91.80/12.51 fof(f19235,plain,(
% 91.80/12.51 s__subclass(s__Class32_2,s__Class32_3)),
% 91.80/12.51 inference(cnf_transformation,[status(thm)],[f7225])).
% 91.80/12.51 fof(f19236,plain,(
% 91.80/12.51 s__subclass(s__Class32_3,s__Class32_1)),
% 91.80/12.51 inference(cnf_transformation,[status(thm)],[f7226])).
% 91.80/12.51 fof(f19237,plain,(
% 91.80/12.51 (?[V_X]: (s__instance(V_X,s__Class32_2)&~s__instance(V_X,s__Class32_1)))),
% 91.80/12.51 inference(pre_NNF_transformation,[status(thm)],[f7228])).
% 91.80/12.51 fof(f19238,plain,(
% 91.80/12.51 (s__instance(sK508_skl,s__Class32_2)&~s__instance(sK508_skl,s__Class32_1))),
% 91.80/12.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK508_skl]),skolemize(V_X,sK508_skl)],[f19237])).
% 91.80/12.51 fof(f19239,plain,(
% 91.80/12.51 s__instance(sK508_skl,s__Class32_2)),
% 91.80/12.51 inference(cnf_transformation,[status(thm)],[f19238])).
% 91.80/12.51 fof(f19240,plain,(
% 91.80/12.51 ~s__instance(sK508_skl,s__Class32_1)),
% 91.80/12.51 inference(cnf_transformation,[status(thm)],[f19238])).
% 91.80/12.51 fof(f19432,plain,(
% 91.80/12.51 s__instance(s__Class32_2,s__SetOrClass)),
% 91.80/12.51 inference(resolution,[status(thm)],[f7269,f19232])).
% 91.80/12.51 fof(f19433,plain,(
% 91.80/12.51 s__instance(s__Class32_1,s__SetOrClass)),
% 91.80/12.51 inference(resolution,[status(thm)],[f7269,f19234])).
% 91.80/12.51 fof(f19467,plain,(
% 91.80/12.51 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,X1)|~s__instance(X2,X0)|s__instance(X2,X1))),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f7273,f7270])).
% 91.80/12.51 fof(f28457,plain,(
% 91.80/12.51 ![X0]: (~s__instance(s__Class32_2,s__SetOrClass)|~s__instance(X0,s__Class32_2)|s__instance(X0,s__Class32_3))),
% 91.80/12.51 inference(resolution,[status(thm)],[f19235,f19467])).
% 91.80/12.51 fof(f28460,plain,(
% 91.80/12.51 ![X0]: (~s__instance(X0,s__Class32_2)|s__instance(X0,s__Class32_3))),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f28457,f19432])).
% 91.80/12.51 fof(f28584,plain,(
% 91.80/12.51 s__instance(sK508_skl,s__Class32_3)),
% 91.80/12.51 inference(resolution,[status(thm)],[f28460,f19239])).
% 91.80/12.51 fof(f40467,plain,(
% 91.80/12.51 ![X0,X1]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,X1)|~s__subclass(X1,X0)|X0=X1)),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f9523,f7270])).
% 91.80/12.51 fof(f43982,plain,(
% 91.80/12.51 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__subclass(X1,X2)|~s__subclass(X2,X0)|s__subclass(X1,X0))),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f9666,f7270])).
% 91.80/12.51 fof(f46067,plain,(
% 91.80/12.51 ![X0]: (~s__instance(X0,s__SetOrClass)|~s__instance(s__Class32_1,s__SetOrClass)|~s__subclass(s__Class32_2,X0)|s__subclass(s__Class32_1,X0))),
% 91.80/12.51 inference(resolution,[status(thm)],[f43982,f19234])).
% 91.80/12.51 fof(f46838,plain,(
% 91.80/12.51 ![X0]: (~s__instance(s__Class32_1,s__SetOrClass)|~s__subclass(s__Class32_2,X0)|s__subclass(s__Class32_1,X0))),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f46067,f7270])).
% 91.80/12.51 fof(f46860,plain,(
% 91.80/12.51 ![X0]: (~s__subclass(s__Class32_2,X0)|s__subclass(s__Class32_1,X0))),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f46838,f19433])).
% 91.80/12.51 fof(f46864,plain,(
% 91.80/12.51 s__subclass(s__Class32_1,s__Class32_3)),
% 91.80/12.51 inference(resolution,[status(thm)],[f46860,f19235])).
% 91.80/12.51 fof(f46875,plain,(
% 91.80/12.51 ~s__instance(s__Class32_1,s__SetOrClass)|~s__subclass(s__Class32_3,s__Class32_1)|s__Class32_1=s__Class32_3),
% 91.80/12.51 inference(resolution,[status(thm)],[f46864,f40467])).
% 91.80/12.51 fof(f46880,plain,(
% 91.80/12.51 ~s__subclass(s__Class32_3,s__Class32_1)|s__Class32_1=s__Class32_3),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f46875,f7270])).
% 91.80/12.51 fof(f46891,plain,(
% 91.80/12.51 s__instance(sK508_skl,s__Class32_1)),
% 91.80/12.51 inference(backward_demodulation,[status(thm)],[f46897,f28584])).
% 91.80/12.51 fof(f46897,plain,(
% 91.80/12.51 s__Class32_1=s__Class32_3),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f46880,f19236])).
% 91.80/12.51 fof(f46899,plain,(
% 91.80/12.51 $false),
% 91.80/12.51 inference(forward_subsumption_resolution,[status(thm)],[f46891,f19240])).
% 91.80/12.51 % SZS output end CNFRefutation for theBenchmark.p
% 91.80/12.53 % Elapsed time: 11.942177 seconds
% 91.80/12.53 % CPU time: 92.078864 seconds
% 91.80/12.53 % Total memory used: 812.345 MB
% 91.80/12.53 % Net memory used: 795.299 MB
%------------------------------------------------------------------------------