%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR096+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:13:38 PM UTC 2026
% Result : Theorem 243.11s 31.52s
% Output : CNFRefutation 223.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 60 ( 18 unt; 0 def)
% Number of atoms : 169 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 207 ( 98 ~; 95 |; 5 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 47 ( 47 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [V__X,V__Y] :
( s__subclass(V__X,V__Y)
=> ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [V__X,V__Y,V__Z] :
( ( s__instance(V__X,s__SetOrClass)
& s__instance(V__Y,s__SetOrClass) )
=> ( ( s__instance(V__Z,V__X)
& s__subclass(V__X,V__Y) )
=> s__instance(V__Z,V__Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f613,axiom,
s__subclass(s__Object,s__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6942,axiom,
s__subclass(s__AstronomicalBody,s__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16750,axiom,
s__subclass(s__Planet26_1,s__AstronomicalBody),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16751,axiom,
! [V_P] :
( s__instance(V_P,s__Object)
=> ( s__instance(V_P,s__Planet26_1)
=> ( s__attribute(V_P,s__Gaseous)
| s__attribute(V_P,s__Solid) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16752,axiom,
! [V_P] :
( s__instance(V_P,s__Object)
=> ( s__instance(V_P,s__Planet26_1)
=> ( s__attribute(V_P,s__HostileToEarthLife)
| s__attribute(V_P,s__Earthlike) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16753,axiom,
! [V_X] :
( s__instance(V_X,s__Object)
=> ( ( s__attribute(V_X,s__Gaseous)
& s__instance(V_X,s__Planet26_1) )
=> ~ s__attribute(V_X,s__Earthlike) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16754,axiom,
s__instance(s__Object26_1,s__Planet26_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16755,axiom,
~ s__attribute(s__Object26_1,s__Solid),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16756,conjecture,
s__attribute(s__Object26_1,s__HostileToEarthLife),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16757,negated_conjecture,
~ s__attribute(s__Object26_1,s__HostileToEarthLife),
inference(negated_conjecture,[status(cth)],[f16756]) ).
fof(f16797,plain,
! [V__X,V__Y] :
( ( s__instance(V__Y,s__SetOrClass)
& s__instance(V__X,s__SetOrClass) )
| ~ s__subclass(V__X,V__Y) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f16798,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f16797]) ).
fof(f16799,plain,
! [X0,X1] :
( ~ s__subclass(X1,X0)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f16797]) ).
fof(f16800,plain,
! [V__X,V__Y,V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y)
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f16801,plain,
! [V__X,V__Y] :
( ! [V__Z] :
( s__instance(V__Z,V__Y)
| ~ s__instance(V__Z,V__X)
| ~ s__subclass(V__X,V__Y) )
| ~ s__instance(V__X,s__SetOrClass)
| ~ s__instance(V__Y,s__SetOrClass) ),
inference(miniscoping,[status(thm)],[f16800]) ).
fof(f16802,plain,
! [X0,X1,X2] :
( ~ s__instance(X1,s__SetOrClass)
| s__instance(X2,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16801]) ).
fof(f18085,plain,
s__subclass(s__Object,s__Physical),
inference(cnf_transformation,[status(thm)],[f613]) ).
fof(f29173,plain,
s__subclass(s__AstronomicalBody,s__Object),
inference(cnf_transformation,[status(thm)],[f6942]) ).
fof(f44211,plain,
s__subclass(s__Planet26_1,s__AstronomicalBody),
inference(cnf_transformation,[status(thm)],[f16750]) ).
fof(f44212,plain,
! [V_P] :
( s__attribute(V_P,s__Gaseous)
| s__attribute(V_P,s__Solid)
| ~ s__instance(V_P,s__Planet26_1)
| ~ s__instance(V_P,s__Object) ),
inference(pre_NNF_transformation,[status(thm)],[f16751]) ).
fof(f44213,plain,
! [X0] :
( s__attribute(X0,s__Solid)
| ~ s__instance(X0,s__Object)
| s__attribute(X0,s__Gaseous)
| ~ s__instance(X0,s__Planet26_1) ),
inference(cnf_transformation,[status(thm)],[f44212]) ).
fof(f44214,plain,
! [V_P] :
( s__attribute(V_P,s__HostileToEarthLife)
| s__attribute(V_P,s__Earthlike)
| ~ s__instance(V_P,s__Planet26_1)
| ~ s__instance(V_P,s__Object) ),
inference(pre_NNF_transformation,[status(thm)],[f16752]) ).
fof(f44215,plain,
! [X0] :
( ~ s__instance(X0,s__Planet26_1)
| s__attribute(X0,s__Earthlike)
| ~ s__instance(X0,s__Object)
| s__attribute(X0,s__HostileToEarthLife) ),
inference(cnf_transformation,[status(thm)],[f44214]) ).
fof(f44216,plain,
! [V_X] :
( ~ s__attribute(V_X,s__Earthlike)
| ~ s__attribute(V_X,s__Gaseous)
| ~ s__instance(V_X,s__Planet26_1)
| ~ s__instance(V_X,s__Object) ),
inference(pre_NNF_transformation,[status(thm)],[f16753]) ).
fof(f44217,plain,
! [X0] :
( ~ s__instance(X0,s__Planet26_1)
| ~ s__instance(X0,s__Object)
| ~ s__attribute(X0,s__Gaseous)
| ~ s__attribute(X0,s__Earthlike) ),
inference(cnf_transformation,[status(thm)],[f44216]) ).
fof(f44218,plain,
s__instance(s__Object26_1,s__Planet26_1),
inference(cnf_transformation,[status(thm)],[f16754]) ).
fof(f44219,plain,
~ s__attribute(s__Object26_1,s__Solid),
inference(cnf_transformation,[status(thm)],[f16755]) ).
fof(f44220,plain,
~ s__attribute(s__Object26_1,s__HostileToEarthLife),
inference(cnf_transformation,[status(thm)],[f16757]) ).
fof(f44464,plain,
( s__attribute(s__Object26_1,s__Earthlike)
| ~ s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__HostileToEarthLife) ),
inference(resolution,[status(thm)],[f44215,f44218]) ).
fof(f44465,plain,
( ~ s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Earthlike) ),
inference(forward_subsumption_resolution,[status(thm)],[f44464,f44220]) ).
fof(f44541,plain,
! [X0] :
( ~ s__instance(s__Planet26_1,s__SetOrClass)
| ~ s__subclass(s__Planet26_1,X0)
| ~ s__instance(X0,s__SetOrClass)
| s__instance(s__Object26_1,X0) ),
inference(resolution,[status(thm)],[f16802,f44218]) ).
fof(f44548,plain,
! [X0] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(s__Object,s__SetOrClass)
| ~ s__instance(s__Object26_1,X0)
| ~ s__subclass(X0,s__Object)
| s__attribute(s__Object26_1,s__Earthlike) ),
inference(resolution,[status(thm)],[f16802,f44465]) ).
fof(f44603,plain,
! [X0,X1] :
( ~ s__instance(X1,s__SetOrClass)
| s__instance(s__Object26_1,X1)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1)
| ~ s__instance(s__Planet26_1,s__SetOrClass)
| ~ s__subclass(s__Planet26_1,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[status(thm)],[f44541,f16802]) ).
fof(f44605,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| s__instance(s__Object26_1,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(s__Planet26_1,X0)
| ~ s__instance(s__Planet26_1,s__SetOrClass) ),
inference(duplicate_literals_removal,[status(thm)],[f44603]) ).
fof(f44630,plain,
( s__attribute(s__Object26_1,s__Earthlike)
| ~ s__instance(s__Object26_1,s__AstronomicalBody)
| ~ s__instance(s__AstronomicalBody,s__SetOrClass)
| ~ s__instance(s__Object,s__SetOrClass) ),
inference(resolution,[status(thm)],[f44548,f29173]) ).
fof(f45923,plain,
( s__attribute(s__Object26_1,s__Solid)
| ~ s__instance(s__Object26_1,s__Object)
| s__attribute(s__Object26_1,s__Gaseous) ),
inference(resolution,[status(thm)],[f44213,f44218]) ).
fof(f45929,plain,
( s__attribute(s__Object26_1,s__Gaseous)
| ~ s__instance(s__Object26_1,s__Object) ),
inference(forward_subsumption_resolution,[status(thm)],[f45923,f44219]) ).
fof(f46128,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| s__instance(s__Object26_1,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(s__Planet26_1,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f44605,f16798]) ).
fof(f46129,plain,
! [X0] :
( s__instance(s__Object26_1,X0)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(s__Planet26_1,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f44541,f16798]) ).
fof(f46233,plain,
! [X0,X1] :
( ~ s__instance(X1,s__SetOrClass)
| s__instance(s__Object26_1,X1)
| ~ s__subclass(s__Planet26_1,X0)
| ~ s__subclass(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f46128,f16798]) ).
fof(f46316,plain,
( s__attribute(s__Object26_1,s__Earthlike)
| ~ s__instance(s__AstronomicalBody,s__SetOrClass)
| ~ s__instance(s__Object,s__SetOrClass)
| ~ s__instance(s__AstronomicalBody,s__SetOrClass)
| ~ s__subclass(s__Planet26_1,s__AstronomicalBody) ),
inference(resolution,[status(thm)],[f46129,f44630]) ).
fof(f46423,plain,
( s__attribute(s__Object26_1,s__Earthlike)
| ~ s__instance(s__Object,s__SetOrClass)
| ~ s__instance(s__AstronomicalBody,s__SetOrClass)
| ~ s__subclass(s__Planet26_1,s__AstronomicalBody) ),
inference(duplicate_literals_removal,[status(thm)],[f46316]) ).
fof(f46424,plain,
( ~ s__instance(s__Object,s__SetOrClass)
| s__attribute(s__Object26_1,s__Earthlike)
| ~ s__instance(s__AstronomicalBody,s__SetOrClass) ),
inference(forward_subsumption_resolution,[status(thm)],[f46423,f44211]) ).
fof(f46654,plain,
! [X0] :
( ~ s__subclass(s__AstronomicalBody,X0)
| s__attribute(s__Object26_1,s__Earthlike)
| ~ s__instance(s__Object,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46424,f16798]) ).
fof(f46657,plain,
! [X0,X1] :
( ~ s__subclass(s__Object,X1)
| s__attribute(s__Object26_1,s__Earthlike)
| ~ s__subclass(s__AstronomicalBody,X0) ),
inference(resolution,[status(thm)],[f46654,f16798]) ).
fof(f46658,plain,
! [X0] :
( s__attribute(s__Object26_1,s__Earthlike)
| ~ s__subclass(s__Object,X0) ),
inference(resolution,[status(thm)],[f46657,f29173]) ).
fof(f46659,plain,
s__attribute(s__Object26_1,s__Earthlike),
inference(resolution,[status(thm)],[f46658,f18085]) ).
fof(f46835,plain,
! [X0] :
( ~ s__subclass(s__AstronomicalBody,X0)
| ~ s__instance(X0,s__SetOrClass)
| s__instance(s__Object26_1,X0) ),
inference(resolution,[status(thm)],[f46233,f44211]) ).
fof(f46955,plain,
( s__attribute(s__Object26_1,s__Gaseous)
| ~ s__subclass(s__AstronomicalBody,s__Object)
| ~ s__instance(s__Object,s__SetOrClass) ),
inference(resolution,[status(thm)],[f46835,f45929]) ).
fof(f47022,plain,
( s__attribute(s__Object26_1,s__Gaseous)
| ~ s__instance(s__Object,s__SetOrClass) ),
inference(forward_subsumption_resolution,[status(thm)],[f46955,f29173]) ).
fof(f47029,plain,
! [X0] :
( ~ s__subclass(s__Object,X0)
| s__attribute(s__Object26_1,s__Gaseous) ),
inference(resolution,[status(thm)],[f47022,f16798]) ).
fof(f47030,plain,
s__attribute(s__Object26_1,s__Gaseous),
inference(resolution,[status(thm)],[f47029,f18085]) ).
fof(f50014,plain,
! [X0] :
( s__instance(s__Object26_1,X0)
| ~ s__subclass(s__AstronomicalBody,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f46835,f16799]) ).
fof(f57066,plain,
( ~ s__instance(s__Object26_1,s__Object)
| ~ s__attribute(s__Object26_1,s__Gaseous)
| ~ s__attribute(s__Object26_1,s__Earthlike) ),
inference(resolution,[status(thm)],[f44217,f44218]) ).
fof(f57076,plain,
( ~ s__instance(s__Object26_1,s__Object)
| ~ s__attribute(s__Object26_1,s__Gaseous) ),
inference(forward_subsumption_resolution,[status(thm)],[f57066,f46659]) ).
fof(f57077,plain,
~ s__instance(s__Object26_1,s__Object),
inference(forward_subsumption_resolution,[status(thm)],[f57076,f47030]) ).
fof(f57079,plain,
~ s__subclass(s__AstronomicalBody,s__Object),
inference(resolution,[status(thm)],[f57077,f50014]) ).
fof(f57083,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f57079,f29173]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR096+5 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 14:58:31 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.66/0.93 % Drodi V4.1.1
% 243.11/31.52 % Refutation found
% 243.11/31.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 243.11/31.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 62.85/31.76 % Elapsed time: 31.390191 seconds
% 62.85/31.76 % CPU time: 244.066274 seconds
% 62.85/31.76 % Total memory used: 1.459 GB
% 62.85/31.76 % Net memory used: 1.411 GB
%------------------------------------------------------------------------------