%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR100+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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:40 PM UTC 2026
% Result : Theorem 234.18s 30.67s
% Output : CNFRefutation 157.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 13
% Syntax : Number of formulae : 67 ( 30 unt; 0 def)
% Number of atoms : 161 ( 12 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 170 ( 76 ~; 74 |; 10 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 8 con; 0-0 aty)
% Number of variables : 53 ( 53 !; 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(f607,axiom,
! [V__CLASS] :
( s__instance(V__CLASS,s__SetOrClass)
=> ( s__instance(V__CLASS,s__Class)
<=> s__subclass(V__CLASS,s__Entity) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1440,axiom,
! [V__INST1,V__INST2] :
( ( s__instance(V__INST1,s__SetOrClass)
& s__instance(V__INST2,s__SetOrClass) )
=> ( ( s__subclass(V__INST2,V__INST1)
& s__subclass(V__INST1,V__INST2) )
=> V__INST1 = V__INST2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1536,axiom,
! [V__INST1,V__INST2,V__INST3] :
( ( s__instance(V__INST1,s__SetOrClass)
& s__instance(V__INST2,s__SetOrClass)
& s__instance(V__INST3,s__SetOrClass) )
=> ( ( s__subclass(V__INST2,V__INST3)
& s__subclass(V__INST1,V__INST2) )
=> s__subclass(V__INST1,V__INST3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37982,axiom,
s__instance(s__Class31_1,s__Class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37983,axiom,
s__instance(s__Class31_2,s__Class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37985,axiom,
s__subclass(s__Class31_1,s__Animal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37988,axiom,
s__subclass(s__Class31_1,s__Class31_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37989,axiom,
s__subclass(s__Class31_2,s__Class31_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37990,axiom,
s__subclass(s__Class31_3,s__Class31_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37991,axiom,
s__instance(s__Animal31,s__Class31_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37992,conjecture,
s__instance(s__Animal31,s__Class31_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37993,negated_conjecture,
~ s__instance(s__Animal31,s__Class31_1),
inference(negated_conjecture,[status(cth)],[f37992]) ).
fof(f38033,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(f38034,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f38033]) ).
fof(f38035,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f38033]) ).
fof(f38036,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(f38037,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)],[f38036]) ).
fof(f38038,plain,
! [X0,X1,X2] :
( ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__subclass(X2,X1)
| ~ s__instance(X0,X2)
| s__instance(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f38037]) ).
fof(f39305,plain,
! [V__CLASS] :
( ( s__instance(V__CLASS,s__Class)
<=> s__subclass(V__CLASS,s__Entity) )
| ~ s__instance(V__CLASS,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f607]) ).
fof(f39306,plain,
! [V__CLASS] :
( ( ( ~ s__subclass(V__CLASS,s__Entity)
| s__instance(V__CLASS,s__Class) )
& ( s__subclass(V__CLASS,s__Entity)
| ~ s__instance(V__CLASS,s__Class) ) )
| ~ s__instance(V__CLASS,s__SetOrClass) ),
inference(NNF_transformation,[status(thm)],[f39305]) ).
fof(f39307,plain,
! [X0] :
( s__subclass(X0,s__Entity)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X0,s__Class) ),
inference(cnf_transformation,[status(thm)],[f39306]) ).
fof(f40771,plain,
! [V__INST1,V__INST2] :
( V__INST1 = V__INST2
| ~ s__subclass(V__INST2,V__INST1)
| ~ s__subclass(V__INST1,V__INST2)
| ~ s__instance(V__INST1,s__SetOrClass)
| ~ s__instance(V__INST2,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f1440]) ).
fof(f40772,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X0)
| ~ s__subclass(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f40771]) ).
fof(f40958,plain,
! [V__INST1,V__INST2,V__INST3] :
( s__subclass(V__INST1,V__INST3)
| ~ s__subclass(V__INST2,V__INST3)
| ~ s__subclass(V__INST1,V__INST2)
| ~ s__instance(V__INST1,s__SetOrClass)
| ~ s__instance(V__INST2,s__SetOrClass)
| ~ s__instance(V__INST3,s__SetOrClass) ),
inference(pre_NNF_transformation,[status(thm)],[f1536]) ).
fof(f40959,plain,
! [X0,X1,X2] :
( ~ s__subclass(X1,X2)
| ~ s__instance(X1,s__SetOrClass)
| s__subclass(X0,X2)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f40958]) ).
fof(f86679,plain,
s__instance(s__Class31_1,s__Class),
inference(cnf_transformation,[status(thm)],[f37982]) ).
fof(f86680,plain,
s__instance(s__Class31_2,s__Class),
inference(cnf_transformation,[status(thm)],[f37983]) ).
fof(f86682,plain,
s__subclass(s__Class31_1,s__Animal),
inference(cnf_transformation,[status(thm)],[f37985]) ).
fof(f86685,plain,
s__subclass(s__Class31_1,s__Class31_2),
inference(cnf_transformation,[status(thm)],[f37988]) ).
fof(f86686,plain,
s__subclass(s__Class31_2,s__Class31_3),
inference(cnf_transformation,[status(thm)],[f37989]) ).
fof(f86687,plain,
s__subclass(s__Class31_3,s__Class31_1),
inference(cnf_transformation,[status(thm)],[f37990]) ).
fof(f86688,plain,
s__instance(s__Animal31,s__Class31_2),
inference(cnf_transformation,[status(thm)],[f37991]) ).
fof(f86689,plain,
~ s__instance(s__Animal31,s__Class31_1),
inference(cnf_transformation,[status(thm)],[f37993]) ).
fof(f86953,plain,
! [X0] :
( ~ s__instance(s__Class31_2,s__SetOrClass)
| s__instance(s__Animal31,X0)
| ~ s__subclass(s__Class31_2,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(resolution,[status(thm)],[f38038,f86688]) ).
fof(f87056,plain,
! [X0] :
( ~ s__subclass(s__Class31_2,X0)
| ~ s__instance(s__Class31_2,s__SetOrClass)
| s__instance(s__Animal31,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f86953,f38035]) ).
fof(f87067,plain,
s__instance(s__Class31_2,s__SetOrClass),
inference(resolution,[status(thm)],[f38035,f86685]) ).
fof(f87079,plain,
! [X0] :
( ~ s__subclass(s__Class31_2,X0)
| s__instance(s__Animal31,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f87056,f87067]) ).
fof(f87080,plain,
s__instance(s__Animal31,s__Class31_3),
inference(resolution,[status(thm)],[f87079,f86686]) ).
fof(f87141,plain,
s__instance(s__Class31_1,s__SetOrClass),
inference(resolution,[status(thm)],[f38034,f86682]) ).
fof(f97084,plain,
( s__subclass(s__Class31_2,s__Entity)
| ~ s__instance(s__Class31_2,s__Class) ),
inference(resolution,[status(thm)],[f39307,f87067]) ).
fof(f97085,plain,
( s__subclass(s__Class31_1,s__Entity)
| ~ s__instance(s__Class31_1,s__Class) ),
inference(resolution,[status(thm)],[f39307,f87141]) ).
fof(f97086,plain,
s__subclass(s__Class31_2,s__Entity),
inference(forward_subsumption_resolution,[status(thm)],[f97084,f86680]) ).
fof(f97087,plain,
s__subclass(s__Class31_1,s__Entity),
inference(forward_subsumption_resolution,[status(thm)],[f97085,f86679]) ).
fof(f97093,plain,
s__instance(s__Entity,s__SetOrClass),
inference(resolution,[status(thm)],[f97086,f38035]) ).
fof(f107914,plain,
! [X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| X1 = X0
| ~ s__subclass(X1,X0)
| ~ s__subclass(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f40772,f38034]) ).
fof(f109722,plain,
( ~ s__instance(s__Class31_1,s__SetOrClass)
| s__Class31_2 = s__Class31_1
| ~ s__subclass(s__Class31_2,s__Class31_1) ),
inference(resolution,[status(thm)],[f107914,f86685]) ).
fof(f109798,plain,
( s__Class31_1 = s__Class31_2
| ~ s__subclass(s__Class31_2,s__Class31_1) ),
inference(forward_subsumption_resolution,[status(thm)],[f109722,f38035]) ).
fof(f113366,plain,
! [X0,X1,X2] :
( ~ s__instance(X2,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X2)
| ~ s__subclass(X2,X1)
| s__subclass(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f40959,f38034]) ).
fof(f115337,plain,
! [X0] :
( ~ s__instance(s__Class31_1,s__SetOrClass)
| ~ s__instance(s__Entity,s__SetOrClass)
| ~ s__subclass(X0,s__Class31_1)
| s__subclass(X0,s__Entity) ),
inference(resolution,[status(thm)],[f113366,f97087]) ).
fof(f115338,plain,
! [X0] :
( ~ s__instance(s__Class31_1,s__SetOrClass)
| ~ s__instance(s__Class31_2,s__SetOrClass)
| ~ s__subclass(X0,s__Class31_1)
| s__subclass(X0,s__Class31_2) ),
inference(resolution,[status(thm)],[f113366,f86685]) ).
fof(f115509,plain,
! [X0] :
( ~ s__instance(s__Entity,s__SetOrClass)
| s__subclass(X0,s__Entity)
| ~ s__subclass(X0,s__Class31_1) ),
inference(forward_subsumption_resolution,[status(thm)],[f115337,f38035]) ).
fof(f115575,plain,
! [X0] :
( ~ s__instance(s__Class31_2,s__SetOrClass)
| s__subclass(X0,s__Class31_2)
| ~ s__subclass(X0,s__Class31_1) ),
inference(forward_subsumption_resolution,[status(thm)],[f115338,f38035]) ).
fof(f117352,plain,
! [X0] :
( ~ s__subclass(X0,s__Class31_1)
| s__subclass(X0,s__Entity) ),
inference(forward_subsumption_resolution,[status(thm)],[f115509,f97093]) ).
fof(f117353,plain,
s__subclass(s__Class31_3,s__Entity),
inference(resolution,[status(thm)],[f117352,f86687]) ).
fof(f117358,plain,
s__instance(s__Class31_3,s__SetOrClass),
inference(resolution,[status(thm)],[f117353,f38034]) ).
fof(f117433,plain,
! [X0] :
( ~ s__subclass(X0,s__Class31_1)
| s__subclass(X0,s__Class31_2) ),
inference(forward_subsumption_resolution,[status(thm)],[f115575,f87067]) ).
fof(f117434,plain,
s__subclass(s__Class31_3,s__Class31_2),
inference(resolution,[status(thm)],[f117433,f86687]) ).
fof(f117444,plain,
( ~ s__instance(s__Class31_3,s__SetOrClass)
| s__Class31_2 = s__Class31_3
| ~ s__subclass(s__Class31_2,s__Class31_3) ),
inference(resolution,[status(thm)],[f117434,f107914]) ).
fof(f117448,plain,
( ~ s__instance(s__Class31_3,s__SetOrClass)
| s__Class31_2 = s__Class31_3 ),
inference(forward_subsumption_resolution,[status(thm)],[f117444,f86686]) ).
fof(f117513,plain,
( s__Class31_1 = s__Class31_3
| ~ s__subclass(s__Class31_2,s__Class31_1) ),
inference(backward_demodulation,[status(thm)],[f117580,f109798]) ).
fof(f117580,plain,
s__Class31_2 = s__Class31_3,
inference(forward_subsumption_resolution,[status(thm)],[f117448,f117358]) ).
fof(f117592,plain,
( s__Class31_1 = s__Class31_3
| ~ s__subclass(s__Class31_3,s__Class31_1) ),
inference(forward_demodulation,[status(thm)],[f117580,f117513]) ).
fof(f117593,plain,
s__Class31_3 = s__Class31_1,
inference(forward_subsumption_resolution,[status(thm)],[f117592,f86687]) ).
fof(f117682,plain,
s__instance(s__Animal31,s__Class31_1),
inference(backward_demodulation,[status(thm)],[f117593,f87080]) ).
fof(f117732,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f117682,f86689]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR100+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 15:03:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.89/1.17 % Drodi V4.1.1
% 234.18/30.67 % Refutation found
% 234.18/30.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 234.18/30.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.04/31.01 % Elapsed time: 30.624895 seconds
% 8.04/31.01 % CPU time: 235.538767 seconds
% 8.04/31.01 % Total memory used: 2.110 GB
% 8.04/31.01 % Net memory used: 2.088 GB
%------------------------------------------------------------------------------