%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR089+1 : 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 : n014.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:07 PM UTC 2026
% Result : Theorem 182.78s 24.11s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR089+1 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.57 % Computer : n014.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Mon Sep 21 14:53:36 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.13/0.93 % Drodi V4.1.1
% 182.78/24.11 % Refutation found
% 182.78/24.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 182.78/24.11 % SZS output start CNFRefutation for theBenchmark
% 182.78/24.11 fof(f26,axiom,(
% 182.78/24.11 (! [V__X,V__Y] :( s__subclass(V__X,V__Y)=> ( s__instance(V__X,s__SetOrClass)& s__instance(V__Y,s__SetOrClass) ) ) )),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f27,axiom,(
% 182.78/24.11 (! [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) ) ) )),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f55,axiom,(
% 182.78/24.11 (! [V__ROW1,V__ROW2] :( ( s__instance(V__ROW2,s__EngineeringComponent)& s__instance(V__ROW1,s__EngineeringComponent) )=> ( s__connectedEngineeringComponents(V__ROW1,V__ROW2)=> s__connected(V__ROW1,V__ROW2) ) ) )),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f1291,axiom,(
% 182.78/24.11 (! [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) ) ) )),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f4643,axiom,(
% 182.78/24.11 (! [V__OBJ1,V__OBJ2] :( ( s__instance(V__OBJ2,s__Object)& s__instance(V__OBJ1,s__Object) )=> ( s__connected(V__OBJ1,V__OBJ2)=> ( s__meetsSpatially(V__OBJ1,V__OBJ2)| s__overlapsSpatially(V__OBJ1,V__OBJ2) ) ) ) )),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f6310,axiom,(
% 182.78/24.11 s__subclass(s__Artifact,s__Object) ),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f6441,axiom,(
% 182.78/24.11 (! [V__COMP2,V__COMP1] :( ( s__instance(V__COMP1,s__EngineeringComponent)& s__instance(V__COMP2,s__EngineeringComponent) )=> ( s__connectedEngineeringComponents(V__COMP1,V__COMP2)<=> (? [V__CONNECTION] :( s__instance(V__CONNECTION,s__EngineeringConnection)& s__connectsEngineeringComponents(V__CONNECTION,V__COMP1,V__COMP2) ) )) ) )),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f12482,axiom,(
% 182.78/24.11 s__subclass(s__EngineeringComponent,s__Artifact) ),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f14788,axiom,(
% 182.78/24.11 s__instance(s__Object16_1,s__EngineeringConnection) ),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f14789,axiom,(
% 182.78/24.11 s__instance(s__Object16_2,s__EngineeringComponent) ),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f14790,axiom,(
% 182.78/24.11 s__instance(s__Object16_3,s__EngineeringComponent) ),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f14791,axiom,(
% 182.78/24.11 s__connectsEngineeringComponents(s__Object16_1,s__Object16_2,s__Object16_3) ),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f14792,axiom,(
% 182.78/24.11 ~ s__overlapsSpatially(s__Object16_2,s__Object16_3) ),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f14793,conjecture,(
% 182.78/24.11 s__meetsSpatially(s__Object16_2,s__Object16_3) ),
% 182.78/24.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 182.78/24.11 fof(f14794,negated_conjecture,(
% 182.78/24.11 ~(s__meetsSpatially(s__Object16_2,s__Object16_3) )),
% 182.78/24.11 inference(negated_conjecture,[status(cth)],[f14793])).
% 182.78/24.11 fof(f14834,plain,(
% 182.78/24.11 ![V__X,V__Y]: (~s__subclass(V__X,V__Y)|(s__instance(V__X,s__SetOrClass)&s__instance(V__Y,s__SetOrClass)))),
% 182.78/24.11 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 182.78/24.11 fof(f14835,plain,(
% 182.78/24.11 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X0,s__SetOrClass))),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14834])).
% 182.78/24.11 fof(f14836,plain,(
% 182.78/24.11 ![X0,X1]: (~s__subclass(X0,X1)|s__instance(X1,s__SetOrClass))),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14834])).
% 182.78/24.11 fof(f14837,plain,(
% 182.78/24.11 ![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)))),
% 182.78/24.11 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 182.78/24.11 fof(f14838,plain,(
% 182.78/24.11 ![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))))),
% 182.78/24.11 inference(miniscoping,[status(thm)],[f14837])).
% 182.78/24.11 fof(f14839,plain,(
% 182.78/24.11 ![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))),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14838])).
% 182.78/24.11 fof(f14886,plain,(
% 182.78/24.11 ![V__ROW1,V__ROW2]: ((~s__instance(V__ROW2,s__EngineeringComponent)|~s__instance(V__ROW1,s__EngineeringComponent))|(~s__connectedEngineeringComponents(V__ROW1,V__ROW2)|s__connected(V__ROW1,V__ROW2)))),
% 182.78/24.11 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 182.78/24.11 fof(f14887,plain,(
% 182.78/24.11 ![X0,X1]: (~s__instance(X0,s__EngineeringComponent)|~s__instance(X1,s__EngineeringComponent)|~s__connectedEngineeringComponents(X1,X0)|s__connected(X1,X0))),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14886])).
% 182.78/24.11 fof(f17231,plain,(
% 182.78/24.11 ![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)))),
% 182.78/24.11 inference(pre_NNF_transformation,[status(thm)],[f1291])).
% 182.78/24.11 fof(f17232,plain,(
% 182.78/24.11 ![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))),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f17231])).
% 182.78/24.11 fof(f22833,plain,(
% 182.78/24.11 ![V__OBJ1,V__OBJ2]: ((~s__instance(V__OBJ2,s__Object)|~s__instance(V__OBJ1,s__Object))|(~s__connected(V__OBJ1,V__OBJ2)|(s__meetsSpatially(V__OBJ1,V__OBJ2)|s__overlapsSpatially(V__OBJ1,V__OBJ2))))),
% 182.78/24.11 inference(pre_NNF_transformation,[status(thm)],[f4643])).
% 182.78/24.11 fof(f22834,plain,(
% 182.78/24.11 ![X0,X1]: (~s__instance(X0,s__Object)|~s__instance(X1,s__Object)|~s__connected(X1,X0)|s__meetsSpatially(X1,X0)|s__overlapsSpatially(X1,X0))),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f22833])).
% 182.78/24.11 fof(f25552,plain,(
% 182.78/24.11 s__subclass(s__Artifact,s__Object)),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f6310])).
% 182.78/24.11 fof(f25759,plain,(
% 182.78/24.11 ![V__COMP2,V__COMP1]: ((~s__instance(V__COMP1,s__EngineeringComponent)|~s__instance(V__COMP2,s__EngineeringComponent))|(s__connectedEngineeringComponents(V__COMP1,V__COMP2)<=>(?[V__CONNECTION]: (s__instance(V__CONNECTION,s__EngineeringConnection)&s__connectsEngineeringComponents(V__CONNECTION,V__COMP1,V__COMP2)))))),
% 182.78/24.11 inference(pre_NNF_transformation,[status(thm)],[f6441])).
% 182.78/24.11 fof(f25760,plain,(
% 182.78/24.11 ![V__COMP2,V__COMP1]: ((~s__instance(V__COMP1,s__EngineeringComponent)|~s__instance(V__COMP2,s__EngineeringComponent))|((~s__connectedEngineeringComponents(V__COMP1,V__COMP2)|(?[V__CONNECTION]: (s__instance(V__CONNECTION,s__EngineeringConnection)&s__connectsEngineeringComponents(V__CONNECTION,V__COMP1,V__COMP2))))&(s__connectedEngineeringComponents(V__COMP1,V__COMP2)|(![V__CONNECTION]: (~s__instance(V__CONNECTION,s__EngineeringConnection)|~s__connectsEngineeringComponents(V__CONNECTION,V__COMP1,V__COMP2))))))),
% 182.78/24.11 inference(NNF_transformation,[status(thm)],[f25759])).
% 182.78/24.11 fof(f25761,plain,(
% 182.78/24.11 ![V__COMP2,V__COMP1]: ((~s__instance(V__COMP1,s__EngineeringComponent)|~s__instance(V__COMP2,s__EngineeringComponent))|((~s__connectedEngineeringComponents(V__COMP1,V__COMP2)|(s__instance(sK471_skl(V__COMP1,V__COMP2),s__EngineeringConnection)&s__connectsEngineeringComponents(sK471_skl(V__COMP1,V__COMP2),V__COMP1,V__COMP2)))&(s__connectedEngineeringComponents(V__COMP1,V__COMP2)|(![V__CONNECTION]: (~s__instance(V__CONNECTION,s__EngineeringConnection)|~s__connectsEngineeringComponents(V__CONNECTION,V__COMP1,V__COMP2))))))),
% 182.78/24.11 inference(skolemize,[status(esa),new_symbols(skolem,[sK471_skl]),skolemize(V__CONNECTION,sK471_skl(V__COMP1,V__COMP2))],[f25760])).
% 182.78/24.11 fof(f25764,plain,(
% 182.78/24.11 ![X0,X1,X2]: (~s__instance(X0,s__EngineeringComponent)|~s__instance(X1,s__EngineeringComponent)|s__connectedEngineeringComponents(X0,X1)|~s__instance(X2,s__EngineeringConnection)|~s__connectsEngineeringComponents(X2,X0,X1))),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f25761])).
% 182.78/24.11 fof(f32058,plain,(
% 182.78/24.11 s__subclass(s__EngineeringComponent,s__Artifact)),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f12482])).
% 182.78/24.11 fof(f34364,plain,(
% 182.78/24.11 s__instance(s__Object16_1,s__EngineeringConnection)),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14788])).
% 182.78/24.11 fof(f34365,plain,(
% 182.78/24.11 s__instance(s__Object16_2,s__EngineeringComponent)),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14789])).
% 182.78/24.11 fof(f34366,plain,(
% 182.78/24.11 s__instance(s__Object16_3,s__EngineeringComponent)),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14790])).
% 182.78/24.11 fof(f34367,plain,(
% 182.78/24.11 s__connectsEngineeringComponents(s__Object16_1,s__Object16_2,s__Object16_3)),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14791])).
% 182.78/24.11 fof(f34368,plain,(
% 182.78/24.11 ~s__overlapsSpatially(s__Object16_2,s__Object16_3)),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14792])).
% 182.78/24.11 fof(f34369,plain,(
% 182.78/24.11 ~s__meetsSpatially(s__Object16_2,s__Object16_3)),
% 182.78/24.11 inference(cnf_transformation,[status(thm)],[f14794])).
% 182.78/24.11 fof(f34793,plain,(
% 182.78/24.11 ![X0,X1,X2]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,X1)|~s__instance(X2,X0)|s__instance(X2,X1))),
% 182.78/24.11 inference(forward_subsumption_resolution,[status(thm)],[f14839,f14836])).
% 182.78/24.11 fof(f36361,plain,(
% 182.78/24.11 ![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))),
% 182.78/24.11 inference(forward_subsumption_resolution,[status(thm)],[f17232,f14836])).
% 182.78/24.11 fof(f36408,plain,(
% 182.78/24.11 ![X0,X1,X2,X3]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__subclass(X1,X2)|~s__subclass(X2,X0)|~s__instance(X1,s__SetOrClass)|~s__instance(X3,X1)|s__instance(X3,X0))),
% 182.78/24.11 inference(resolution,[status(thm)],[f36361,f34793])).
% 182.78/24.11 fof(f36460,plain,(
% 182.78/24.11 ![X0,X1,X2,X3]: (~s__instance(X0,s__SetOrClass)|~s__instance(X1,s__SetOrClass)|~s__subclass(X1,X2)|~s__subclass(X2,X0)|~s__instance(X3,X1)|s__instance(X3,X0))),
% 182.78/24.11 inference(duplicate_literals_removal,[status(thm)],[f36408])).
% 182.78/24.11 fof(f36461,plain,(
% 182.78/24.11 ![X0,X1,X2,X3]: (~s__instance(X0,s__SetOrClass)|~s__subclass(X0,X1)|~s__subclass(X1,X2)|~s__instance(X3,X0)|s__instance(X3,X2))),
% 182.78/24.11 inference(forward_subsumption_resolution,[status(thm)],[f36460,f14836])).
% 182.78/24.11 fof(f74304,plain,(
% 182.78/24.11 ~s__instance(s__Object16_2,s__EngineeringComponent)|~s__instance(s__Object16_3,s__EngineeringComponent)|s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)|~s__instance(s__Object16_1,s__EngineeringConnection)),
% 182.78/24.11 inference(resolution,[status(thm)],[f34367,f25764])).
% 182.78/24.11 fof(f74307,plain,(
% 182.78/24.11 ~s__instance(s__Object16_3,s__EngineeringComponent)|s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)|~s__instance(s__Object16_1,s__EngineeringConnection)),
% 182.78/24.11 inference(forward_subsumption_resolution,[status(thm)],[f74304,f34365])).
% 182.78/24.11 fof(f74310,plain,(
% 182.78/24.11 s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)|~s__instance(s__Object16_1,s__EngineeringConnection)),
% 182.78/24.11 inference(forward_subsumption_resolution,[status(thm)],[f74307,f34366])).
% 182.78/24.11 fof(f74311,plain,(
% 182.78/24.11 s__connectedEngineeringComponents(s__Object16_2,s__Object16_3)),
% 182.78/24.11 inference(resolution,[status(thm)],[f74310,f34364])).
% 182.78/24.11 fof(f93917,plain,(
% 182.78/24.11 ![X0,X1,X2,X3]: (~s__subclass(X0,X1)|~s__subclass(X1,X2)|~s__instance(X3,X0)|s__instance(X3,X2))),
% 182.78/24.11 inference(forward_subsumption_resolution,[status(thm)],[f36461,f14835])).
% 182.78/24.11 fof(f95416,plain,(
% 182.78/24.11 ![X0,X1,X2,X3]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(X2,X0)|~s__instance(X3,s__Object)|~s__connected(X2,X3)|s__meetsSpatially(X2,X3)|s__overlapsSpatially(X2,X3))),
% 182.78/24.11 inference(resolution,[status(thm)],[f93917,f22834])).
% 182.78/24.11 fof(f95472,plain,(
% 182.78/24.11 ![X0,X1,X2,X3]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(X2,X0)|~s__instance(X3,s__Object)|s__meetsSpatially(X2,X3)|s__overlapsSpatially(X2,X3)|~s__instance(X3,s__EngineeringComponent)|~s__instance(X2,s__EngineeringComponent)|~s__connectedEngineeringComponents(X2,X3))),
% 182.78/24.11 inference(resolution,[status(thm)],[f95416,f14887])).
% 182.78/24.11 fof(f95594,plain,(
% 182.78/24.11 ![X0,X1]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0)|~s__instance(s__Object16_3,s__Object)|s__meetsSpatially(s__Object16_2,s__Object16_3)|s__overlapsSpatially(s__Object16_2,s__Object16_3)|~s__instance(s__Object16_3,s__EngineeringComponent)|~s__instance(s__Object16_2,s__EngineeringComponent))),
% 182.78/24.11 inference(resolution,[status(thm)],[f95472,f74311])).
% 183.61/24.21 fof(f95596,plain,(
% 183.61/24.21 ![X0,X1]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0)|~s__instance(s__Object16_3,s__Object)|s__overlapsSpatially(s__Object16_2,s__Object16_3)|~s__instance(s__Object16_3,s__EngineeringComponent)|~s__instance(s__Object16_2,s__EngineeringComponent))),
% 183.61/24.21 inference(forward_subsumption_resolution,[status(thm)],[f95594,f34369])).
% 183.61/24.21 fof(f95616,plain,(
% 183.61/24.21 ![X0,X1]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0)|~s__instance(s__Object16_3,s__Object)|~s__instance(s__Object16_3,s__EngineeringComponent)|~s__instance(s__Object16_2,s__EngineeringComponent))),
% 183.61/24.21 inference(forward_subsumption_resolution,[status(thm)],[f95596,f34368])).
% 183.61/24.21 fof(f95617,plain,(
% 183.61/24.21 ![X0,X1,X2,X3]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0)|~s__instance(s__Object16_3,s__EngineeringComponent)|~s__instance(s__Object16_2,s__EngineeringComponent)|~s__subclass(X2,X3)|~s__subclass(X3,s__Object)|~s__instance(s__Object16_3,X2))),
% 183.61/24.21 inference(resolution,[status(thm)],[f95616,f93917])).
% 183.61/24.21 fof(f95618,plain,(
% 183.61/24.21 ![X0,X1,X2,X3]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0)|~s__instance(s__Object16_2,s__EngineeringComponent)|~s__subclass(X2,X3)|~s__subclass(X3,s__Object)|~s__instance(s__Object16_3,X2))),
% 183.61/24.21 inference(forward_subsumption_resolution,[status(thm)],[f95617,f34366])).
% 183.61/24.21 fof(f95619,plain,(
% 183.61/24.21 ![X0,X1,X2,X3]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0)|~s__subclass(X2,X3)|~s__subclass(X3,s__Object)|~s__instance(s__Object16_3,X2))),
% 183.61/24.21 inference(forward_subsumption_resolution,[status(thm)],[f95618,f34365])).
% 183.61/24.21 fof(f95620,plain,(
% 183.61/24.21 ![X0,X1,X2]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0)|~s__subclass(s__EngineeringComponent,X2)|~s__subclass(X2,s__Object))),
% 183.61/24.21 inference(resolution,[status(thm)],[f95619,f34366])).
% 183.61/24.21 fof(f95670,plain,(
% 183.61/24.21 ![X0,X1]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0)|~s__subclass(s__Artifact,s__Object))),
% 183.61/24.21 inference(resolution,[status(thm)],[f95620,f32058])).
% 183.61/24.21 fof(f95676,plain,(
% 183.61/24.21 ![X0,X1]: (~s__subclass(X0,X1)|~s__subclass(X1,s__Object)|~s__instance(s__Object16_2,X0))),
% 183.61/24.21 inference(forward_subsumption_resolution,[status(thm)],[f95670,f25552])).
% 183.61/24.21 fof(f95682,plain,(
% 183.61/24.21 ![X0]: (~s__subclass(s__EngineeringComponent,X0)|~s__subclass(X0,s__Object))),
% 183.61/24.21 inference(resolution,[status(thm)],[f95676,f34365])).
% 183.61/24.21 fof(f95752,plain,(
% 183.61/24.21 ~s__subclass(s__Artifact,s__Object)),
% 183.61/24.21 inference(resolution,[status(thm)],[f95682,f32058])).
% 183.61/24.21 fof(f95758,plain,(
% 183.61/24.21 $false),
% 183.61/24.21 inference(forward_subsumption_resolution,[status(thm)],[f95752,f25552])).
% 183.61/24.21 % SZS output end CNFRefutation for theBenchmark.p
% 9.94/24.44 % Elapsed time: 23.828591 seconds
% 9.94/24.44 % CPU time: 184.816823 seconds
% 9.94/24.44 % Total memory used: 1.257 GB
% 9.94/24.44 % Net memory used: 1.227 GB
%------------------------------------------------------------------------------