%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR090+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:13:35 PM UTC 2026
% Result : Theorem 234.79s 40.51s
% Output : CNFRefutation 234.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 18
% Syntax : Number of formulae : 70 ( 20 unt; 8 def)
% Number of atoms : 171 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 182 ( 81 ~; 81 |; 7 &)
% ( 8 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 9 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 43 ( 43 !; 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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f905,axiom,
s__subclass(s__TimeInterval,s__TimePosition),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1259,axiom,
! [V__INST1,V__INST2,V__INST3] :
( ( s__instance(V__INST1,s__TimePosition)
& s__instance(V__INST2,s__TimePosition)
& s__instance(V__INST3,s__TimePosition) )
=> ( ( s__temporalPart(V__INST2,V__INST3)
& s__temporalPart(V__INST1,V__INST2) )
=> s__temporalPart(V__INST1,V__INST3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7218,axiom,
s__instance(s__Time17_1,s__TimeInterval),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7219,axiom,
s__instance(s__Time17_2,s__TimeInterval),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7220,axiom,
s__instance(s__Time17_3,s__TimeInterval),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7221,axiom,
s__temporalPart(s__Time17_1,s__Time17_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7222,axiom,
s__temporalPart(s__Time17_2,s__Time17_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7223,conjecture,
s__temporalPart(s__Time17_1,s__Time17_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7224,negated_conjecture,
~ s__temporalPart(s__Time17_1,s__Time17_3),
inference(negated_conjecture,[status(cth)],[f7223]) ).
fof(f7264,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(f7265,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7264]) ).
fof(f7266,plain,
! [X0,X1] :
( ~ s__subclass(X1,X0)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[status(thm)],[f7264]) ).
fof(f7267,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(f7268,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)],[f7267]) ).
fof(f7269,plain,
! [X0,X1,X2] :
( ~ s__instance(X0,s__SetOrClass)
| s__instance(X2,X1)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7268]) ).
fof(f8880,plain,
s__subclass(s__TimeInterval,s__TimePosition),
inference(cnf_transformation,[status(thm)],[f905]) ).
fof(f9596,plain,
! [V__INST1,V__INST2,V__INST3] :
( s__temporalPart(V__INST1,V__INST3)
| ~ s__temporalPart(V__INST2,V__INST3)
| ~ s__temporalPart(V__INST1,V__INST2)
| ~ s__instance(V__INST1,s__TimePosition)
| ~ s__instance(V__INST2,s__TimePosition)
| ~ s__instance(V__INST3,s__TimePosition) ),
inference(pre_NNF_transformation,[status(thm)],[f1259]) ).
fof(f9597,plain,
! [X0,X1,X2] :
( ~ s__temporalPart(X2,X0)
| s__temporalPart(X1,X0)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X2,s__TimePosition)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X0,s__TimePosition) ),
inference(cnf_transformation,[status(thm)],[f9596]) ).
fof(f19224,plain,
s__instance(s__Time17_1,s__TimeInterval),
inference(cnf_transformation,[status(thm)],[f7218]) ).
fof(f19225,plain,
s__instance(s__Time17_2,s__TimeInterval),
inference(cnf_transformation,[status(thm)],[f7219]) ).
fof(f19226,plain,
s__instance(s__Time17_3,s__TimeInterval),
inference(cnf_transformation,[status(thm)],[f7220]) ).
fof(f19227,plain,
s__temporalPart(s__Time17_1,s__Time17_2),
inference(cnf_transformation,[status(thm)],[f7221]) ).
fof(f19228,plain,
s__temporalPart(s__Time17_2,s__Time17_3),
inference(cnf_transformation,[status(thm)],[f7222]) ).
fof(f19229,plain,
~ s__temporalPart(s__Time17_1,s__Time17_3),
inference(cnf_transformation,[status(thm)],[f7224]) ).
fof(f21082,plain,
! [X0,X1,X2] :
( ~ s__subclass(X1,X2)
| ~ s__instance(X1,s__SetOrClass)
| s__instance(X0,X2)
| ~ s__instance(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f7269,f7266]) ).
fof(f21246,definition,
( sQ280_spl
<=> s__instance(s__Time17_2,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition]) ).
fof(f21248,plain,
( sQ280_spl
| ~ s__instance(s__Time17_2,s__TimeInterval) ),
inference(component_clause,[status(thm)],[f21246]) ).
fof(f21252,definition,
( sQ282_spl
<=> s__instance(s__Time17_1,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f21254,plain,
( sQ282_spl
| ~ s__instance(s__Time17_1,s__TimeInterval) ),
inference(component_clause,[status(thm)],[f21252]) ).
fof(f21259,definition,
( sQ284_spl
<=> s__instance(s__Time17_3,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition]) ).
fof(f21261,plain,
( sQ284_spl
| ~ s__instance(s__Time17_3,s__TimeInterval) ),
inference(component_clause,[status(thm)],[f21259]) ).
fof(f21269,plain,
( sQ280_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21248,f19225]) ).
fof(f21270,plain,
sQ280_spl,
inference(contradiction_clause,[status(thm)],[f21269]) ).
fof(f21271,plain,
( sQ282_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21254,f19224]) ).
fof(f21272,plain,
sQ282_spl,
inference(contradiction_clause,[status(thm)],[f21271]) ).
fof(f21273,plain,
( sQ284_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21261,f19226]) ).
fof(f21274,plain,
sQ284_spl,
inference(contradiction_clause,[status(thm)],[f21273]) ).
fof(f21726,definition,
( sQ328_spl
<=> s__instance(s__Time17_1,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition]) ).
fof(f21727,plain,
( ~ sQ328_spl
| s__instance(s__Time17_1,s__TimePosition) ),
inference(component_clause,[status(thm)],[f21726]) ).
fof(f21728,plain,
( sQ328_spl
| ~ s__instance(s__Time17_1,s__TimePosition) ),
inference(component_clause,[status(thm)],[f21726]) ).
fof(f21730,plain,
! [X0] :
( sQ328_spl
| ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(s__Time17_1,X0) ),
inference(resolution,[status(thm)],[f21728,f21082]) ).
fof(f21731,plain,
! [X0] :
( sQ328_spl
| ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__Time17_1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f21730,f7265]) ).
fof(f21732,plain,
( sQ328_spl
| ~ s__instance(s__Time17_1,s__TimeInterval) ),
inference(resolution,[status(thm)],[f21731,f8880]) ).
fof(f21734,plain,
( sQ328_spl
| ~ sQ282_spl ),
inference(split_clause,[status(thm)],[f21732,f21252,f21726]) ).
fof(f21746,plain,
! [X0,X1] :
( ~ sQ328_spl
| ~ s__temporalPart(s__Time17_1,X0)
| ~ s__instance(X1,s__TimePosition)
| s__temporalPart(s__Time17_1,X1)
| ~ s__temporalPart(X0,X1)
| ~ s__instance(X0,s__TimePosition) ),
inference(resolution,[status(thm)],[f21727,f9597]) ).
fof(f21795,definition,
( sQ332_spl
<=> s__instance(s__Time17_2,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition]) ).
fof(f21797,plain,
( sQ332_spl
| ~ s__instance(s__Time17_2,s__TimePosition) ),
inference(component_clause,[status(thm)],[f21795]) ).
fof(f21803,plain,
! [X0] :
( sQ332_spl
| ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(s__Time17_2,X0) ),
inference(resolution,[status(thm)],[f21797,f21082]) ).
fof(f21804,plain,
! [X0] :
( sQ332_spl
| ~ s__instance(s__Time17_2,X0)
| ~ s__subclass(X0,s__TimePosition) ),
inference(forward_subsumption_resolution,[status(thm)],[f21803,f7265]) ).
fof(f21805,plain,
( sQ332_spl
| ~ s__instance(s__Time17_2,s__TimeInterval) ),
inference(resolution,[status(thm)],[f21804,f8880]) ).
fof(f21807,plain,
( sQ332_spl
| ~ sQ280_spl ),
inference(split_clause,[status(thm)],[f21805,f21246,f21795]) ).
fof(f21871,definition,
( sQ340_spl
<=> s__instance(s__Time17_3,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition]) ).
fof(f21873,plain,
( sQ340_spl
| ~ s__instance(s__Time17_3,s__TimePosition) ),
inference(component_clause,[status(thm)],[f21871]) ).
fof(f21875,plain,
! [X0] :
( sQ340_spl
| ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(s__Time17_3,X0) ),
inference(resolution,[status(thm)],[f21873,f21082]) ).
fof(f21876,plain,
! [X0] :
( sQ340_spl
| ~ s__instance(s__Time17_3,X0)
| ~ s__subclass(X0,s__TimePosition) ),
inference(forward_subsumption_resolution,[status(thm)],[f21875,f7265]) ).
fof(f21880,plain,
( sQ340_spl
| ~ s__instance(s__Time17_3,s__TimeInterval) ),
inference(resolution,[status(thm)],[f21876,f8880]) ).
fof(f21882,plain,
( sQ340_spl
| ~ sQ284_spl ),
inference(split_clause,[status(thm)],[f21880,f21259,f21871]) ).
fof(f22217,plain,
! [X0] :
( ~ sQ328_spl
| ~ s__instance(X0,s__TimePosition)
| s__temporalPart(s__Time17_1,X0)
| ~ s__temporalPart(s__Time17_2,X0)
| ~ s__instance(s__Time17_2,s__TimePosition) ),
inference(resolution,[status(thm)],[f21746,f19227]) ).
fof(f22221,definition,
! [X0] :
( sQ370_spl
<=> ( ~ s__instance(X0,s__TimePosition)
| s__temporalPart(s__Time17_1,X0)
| ~ s__temporalPart(s__Time17_2,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition]) ).
fof(f22222,plain,
! [X0] :
( ~ sQ370_spl
| ~ s__instance(X0,s__TimePosition)
| ~ s__temporalPart(s__Time17_2,X0)
| s__temporalPart(s__Time17_1,X0) ),
inference(component_clause,[status(thm)],[f22221]) ).
fof(f22224,plain,
( ~ sQ328_spl
| sQ370_spl
| ~ sQ332_spl ),
inference(split_clause,[status(thm)],[f22217,f21795,f22221,f21726]) ).
fof(f22226,plain,
( ~ sQ370_spl
| ~ s__instance(s__Time17_3,s__TimePosition)
| s__temporalPart(s__Time17_1,s__Time17_3) ),
inference(resolution,[status(thm)],[f22222,f19228]) ).
fof(f22230,definition,
( sQ371_spl
<=> s__temporalPart(s__Time17_1,s__Time17_3) ),
introduced(definition,[new_symbols(definition,[sQ371_spl])],[split_symbol_definition]) ).
fof(f22231,plain,
( ~ sQ371_spl
| s__temporalPart(s__Time17_1,s__Time17_3) ),
inference(component_clause,[status(thm)],[f22230]) ).
fof(f22233,plain,
( ~ sQ370_spl
| ~ sQ340_spl
| sQ371_spl ),
inference(split_clause,[status(thm)],[f22226,f22230,f21871,f22221]) ).
fof(f22234,plain,
( ~ sQ371_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f22231,f19229]) ).
fof(f22235,plain,
~ sQ371_spl,
inference(contradiction_clause,[status(thm)],[f22234]) ).
fof(f22236,plain,
$false,
inference(sat_refutation,[status(thm)],[f21270,f21272,f21274,f21734,f21807,f21882,f22224,f22233,f22235]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR090+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/10.47 % Computer : n014.cluster.edu
% 0.17/10.47 % Model : x86_64 x86_64
% 0.17/10.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/10.47 % Memory : 8046.5625MB
% 0.17/10.47 % OS : Linux 6.8.0-71-generic
% 0.17/10.47 % CPULimit : 300
% 0.17/10.47 % WCLimit : 300
% 0.17/10.47 % DateTime : Mon Sep 21 14:54:44 UTC 2026
% 0.17/10.47 % CPUTime :
% 0.22/10.89 % Drodi V4.1.1
% 234.79/40.51 % Refutation found
% 234.79/40.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 234.79/40.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 104.23/40.66 % Elapsed time: 30.171442 seconds
% 104.23/40.66 % CPU time: 235.421991 seconds
% 104.23/40.66 % Total memory used: 868.401 MB
% 104.23/40.66 % Net memory used: 840.322 MB
%------------------------------------------------------------------------------