%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR104+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 : n020.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:43 PM UTC 2026
% Result : Theorem 200.80s 26.14s
% Output : CNFRefutation 200.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 21
% Syntax : Number of formulae : 81 ( 23 unt; 9 def)
% Number of atoms : 202 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 217 ( 96 ~; 97 |; 8 &)
% ( 9 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 10 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 49 ( 49 !; 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(f74,axiom,
! [V__ROW1,V__ROW2] :
( ( s__instance(V__ROW1,s__TimeInterval)
& s__instance(V__ROW2,s__TimeInterval) )
=> ( s__during(V__ROW1,V__ROW2)
=> s__temporalPart(V__ROW1,V__ROW2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f905,axiom,
s__subclass(s__TimeInterval,s__TimePosition),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f909,axiom,
s__subclass(s__TimePoint,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__TimePoint35_1,s__TimePoint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7219,axiom,
s__instance(s__TimeInterval35_1,s__TimeInterval),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7220,axiom,
s__instance(s__TimeInterval35_2,s__TimeInterval),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7221,axiom,
s__temporalPart(s__TimePoint35_1,s__TimeInterval35_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7222,axiom,
s__during(s__TimeInterval35_1,s__TimeInterval35_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7223,conjecture,
s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7224,negated_conjecture,
~ s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2),
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__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
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(f7355,plain,
! [V__ROW1,V__ROW2] :
( s__temporalPart(V__ROW1,V__ROW2)
| ~ s__during(V__ROW1,V__ROW2)
| ~ s__instance(V__ROW1,s__TimeInterval)
| ~ s__instance(V__ROW2,s__TimeInterval) ),
inference(pre_NNF_transformation,[status(thm)],[f74]) ).
fof(f7356,plain,
! [X0,X1] :
( ~ s__during(X0,X1)
| ~ s__instance(X0,s__TimeInterval)
| ~ s__instance(X1,s__TimeInterval)
| s__temporalPart(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7355]) ).
fof(f8880,plain,
s__subclass(s__TimeInterval,s__TimePosition),
inference(cnf_transformation,[status(thm)],[f905]) ).
fof(f8884,plain,
s__subclass(s__TimePoint,s__TimePosition),
inference(cnf_transformation,[status(thm)],[f909]) ).
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__instance(X0,s__TimePosition)
| ~ s__instance(X2,s__TimePosition)
| ~ s__temporalPart(X0,X2)
| ~ s__temporalPart(X2,X1)
| ~ s__instance(X1,s__TimePosition)
| s__temporalPart(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f9596]) ).
fof(f19224,plain,
s__instance(s__TimePoint35_1,s__TimePoint),
inference(cnf_transformation,[status(thm)],[f7218]) ).
fof(f19225,plain,
s__instance(s__TimeInterval35_1,s__TimeInterval),
inference(cnf_transformation,[status(thm)],[f7219]) ).
fof(f19226,plain,
s__instance(s__TimeInterval35_2,s__TimeInterval),
inference(cnf_transformation,[status(thm)],[f7220]) ).
fof(f19227,plain,
s__temporalPart(s__TimePoint35_1,s__TimeInterval35_1),
inference(cnf_transformation,[status(thm)],[f7221]) ).
fof(f19228,plain,
s__during(s__TimeInterval35_1,s__TimeInterval35_2),
inference(cnf_transformation,[status(thm)],[f7222]) ).
fof(f19229,plain,
~ s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2),
inference(cnf_transformation,[status(thm)],[f7224]) ).
fof(f19895,definition,
( sQ67_spl
<=> s__instance(s__TimeInterval35_2,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f19897,plain,
( sQ67_spl
| ~ s__instance(s__TimeInterval35_2,s__TimeInterval) ),
inference(component_clause,[status(thm)],[f19895]) ).
fof(f19905,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f19897,f19226]) ).
fof(f19906,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f19905]) ).
fof(f19928,plain,
! [X0,X1,X2] :
( ~ s__instance(X2,X0)
| s__instance(X2,X1)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f7269,f7266]) ).
fof(f20255,definition,
( sQ76_spl
<=> s__instance(s__TimeInterval35_1,s__TimeInterval) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f20257,plain,
( sQ76_spl
| ~ s__instance(s__TimeInterval35_1,s__TimeInterval) ),
inference(component_clause,[status(thm)],[f20255]) ).
fof(f20270,plain,
( sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20257,f19225]) ).
fof(f20271,plain,
sQ76_spl,
inference(contradiction_clause,[status(thm)],[f20270]) ).
fof(f20421,definition,
( sQ96_spl
<=> s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f20422,plain,
( ~ sQ96_spl
| s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2) ),
inference(component_clause,[status(thm)],[f20421]) ).
fof(f21359,definition,
( sQ136_spl
<=> s__temporalPart(s__TimeInterval35_1,s__TimeInterval35_2) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f21360,plain,
( ~ sQ136_spl
| s__temporalPart(s__TimeInterval35_1,s__TimeInterval35_2) ),
inference(component_clause,[status(thm)],[f21359]) ).
fof(f21361,plain,
( sQ136_spl
| ~ s__temporalPart(s__TimeInterval35_1,s__TimeInterval35_2) ),
inference(component_clause,[status(thm)],[f21359]) ).
fof(f21363,plain,
( sQ136_spl
| ~ s__during(s__TimeInterval35_1,s__TimeInterval35_2)
| ~ s__instance(s__TimeInterval35_1,s__TimeInterval)
| ~ s__instance(s__TimeInterval35_2,s__TimeInterval) ),
inference(resolution,[status(thm)],[f21361,f7356]) ).
fof(f21364,definition,
( sQ137_spl
<=> s__during(s__TimeInterval35_1,s__TimeInterval35_2) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f21366,plain,
( sQ137_spl
| ~ s__during(s__TimeInterval35_1,s__TimeInterval35_2) ),
inference(component_clause,[status(thm)],[f21364]) ).
fof(f21367,plain,
( sQ136_spl
| ~ sQ137_spl
| ~ sQ76_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f21363,f19895,f20255,f21364,f21359]) ).
fof(f21368,plain,
( sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f21366,f19228]) ).
fof(f21369,plain,
sQ137_spl,
inference(contradiction_clause,[status(thm)],[f21368]) ).
fof(f21461,plain,
( ~ sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f20422,f19229]) ).
fof(f21462,plain,
~ sQ96_spl,
inference(contradiction_clause,[status(thm)],[f21461]) ).
fof(f23982,definition,
( sQ433_spl
<=> s__instance(s__TimeInterval35_2,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[sQ433_spl])],[split_symbol_definition]) ).
fof(f23984,plain,
( sQ433_spl
| ~ s__instance(s__TimeInterval35_2,s__TimePosition) ),
inference(component_clause,[status(thm)],[f23982]) ).
fof(f23993,plain,
! [X0] :
( sQ433_spl
| ~ s__instance(s__TimeInterval35_2,X0)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,s__TimePosition) ),
inference(resolution,[status(thm)],[f23984,f19928]) ).
fof(f23994,plain,
! [X0] :
( sQ433_spl
| ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__TimeInterval35_2,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f23993,f7265]) ).
fof(f23995,plain,
( sQ433_spl
| ~ s__instance(s__TimeInterval35_2,s__TimeInterval) ),
inference(resolution,[status(thm)],[f23994,f8880]) ).
fof(f23997,plain,
( sQ433_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f23995,f19895,f23982]) ).
fof(f24034,definition,
( sQ437_spl
<=> s__instance(s__TimeInterval35_1,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition]) ).
fof(f24035,plain,
( ~ sQ437_spl
| s__instance(s__TimeInterval35_1,s__TimePosition) ),
inference(component_clause,[status(thm)],[f24034]) ).
fof(f24036,plain,
( sQ437_spl
| ~ s__instance(s__TimeInterval35_1,s__TimePosition) ),
inference(component_clause,[status(thm)],[f24034]) ).
fof(f24039,plain,
! [X0] :
( sQ437_spl
| ~ s__instance(s__TimeInterval35_1,X0)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,s__TimePosition) ),
inference(resolution,[status(thm)],[f24036,f19928]) ).
fof(f24040,plain,
! [X0] :
( sQ437_spl
| ~ s__subclass(X0,s__TimePosition)
| ~ s__instance(s__TimeInterval35_1,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f24039,f7265]) ).
fof(f24041,plain,
( sQ437_spl
| ~ s__instance(s__TimeInterval35_1,s__TimeInterval) ),
inference(resolution,[status(thm)],[f24040,f8880]) ).
fof(f24043,plain,
( sQ437_spl
| ~ sQ76_spl ),
inference(split_clause,[status(thm)],[f24041,f20255,f24034]) ).
fof(f24053,plain,
! [X0,X1] :
( ~ sQ437_spl
| ~ s__instance(X0,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| s__temporalPart(X1,X0)
| ~ s__temporalPart(X1,s__TimeInterval35_1)
| ~ s__temporalPart(s__TimeInterval35_1,X0) ),
inference(resolution,[status(thm)],[f24035,f9597]) ).
fof(f24066,definition,
( sQ439_spl
<=> s__instance(s__TimePoint35_1,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition]) ).
fof(f24068,plain,
( sQ439_spl
| ~ s__instance(s__TimePoint35_1,s__TimePosition) ),
inference(component_clause,[status(thm)],[f24066]) ).
fof(f24070,plain,
! [X0] :
( sQ439_spl
| ~ s__instance(s__TimePoint35_1,X0)
| ~ s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,s__TimePosition) ),
inference(resolution,[status(thm)],[f24068,f19928]) ).
fof(f24071,plain,
! [X0] :
( sQ439_spl
| ~ s__instance(s__TimePoint35_1,X0)
| ~ s__subclass(X0,s__TimePosition) ),
inference(forward_subsumption_resolution,[status(thm)],[f24070,f7265]) ).
fof(f24073,plain,
( sQ439_spl
| ~ s__instance(s__TimePoint35_1,s__TimePoint) ),
inference(resolution,[status(thm)],[f24071,f8884]) ).
fof(f24074,plain,
( sQ439_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f24073,f19224]) ).
fof(f24075,plain,
sQ439_spl,
inference(contradiction_clause,[status(thm)],[f24074]) ).
fof(f24244,plain,
! [X0] :
( ~ sQ437_spl
| ~ s__instance(X0,s__TimePosition)
| ~ s__instance(s__TimePoint35_1,s__TimePosition)
| s__temporalPart(s__TimePoint35_1,X0)
| ~ s__temporalPart(s__TimeInterval35_1,X0) ),
inference(resolution,[status(thm)],[f24053,f19227]) ).
fof(f24252,definition,
! [X0] :
( sQ452_spl
<=> ( ~ s__instance(X0,s__TimePosition)
| s__temporalPart(s__TimePoint35_1,X0)
| ~ s__temporalPart(s__TimeInterval35_1,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition]) ).
fof(f24253,plain,
! [X0] :
( ~ sQ452_spl
| ~ s__temporalPart(s__TimeInterval35_1,X0)
| s__temporalPart(s__TimePoint35_1,X0)
| ~ s__instance(X0,s__TimePosition) ),
inference(component_clause,[status(thm)],[f24252]) ).
fof(f24255,plain,
( ~ sQ437_spl
| ~ sQ439_spl
| sQ452_spl ),
inference(split_clause,[status(thm)],[f24244,f24252,f24066,f24034]) ).
fof(f24260,plain,
( ~ sQ136_spl
| ~ sQ452_spl
| s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2)
| ~ s__instance(s__TimeInterval35_2,s__TimePosition) ),
inference(resolution,[status(thm)],[f24253,f21360]) ).
fof(f24274,plain,
( ~ sQ136_spl
| ~ sQ452_spl
| sQ96_spl
| ~ sQ433_spl ),
inference(split_clause,[status(thm)],[f24260,f23982,f20421,f24252,f21359]) ).
fof(f24275,plain,
$false,
inference(sat_refutation,[status(thm)],[f19906,f20271,f21367,f21369,f21462,f23997,f24043,f24075,f24255,f24274]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR104+4 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.52 % Computer : n020.cluster.edu
% 0.09/0.52 % Model : x86_64 x86_64
% 0.09/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.52 % Memory : 8046.5625MB
% 0.09/0.52 % OS : Linux 6.8.0-71-generic
% 0.09/0.52 % CPULimit : 300
% 0.09/0.52 % WCLimit : 300
% 0.09/0.52 % DateTime : Mon Sep 21 15:00:34 UTC 2026
% 0.09/0.53 % CPUTime :
% 0.14/0.81 % Drodi V4.1.1
% 200.80/26.14 % Refutation found
% 200.80/26.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 200.80/26.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.06/26.44 % Elapsed time: 25.896673 seconds
% 12.06/26.44 % CPU time: 201.889613 seconds
% 12.06/26.44 % Total memory used: 1.030 GB
% 12.06/26.44 % Net memory used: 999.157 MB
%------------------------------------------------------------------------------