%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR048+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:08 PM UTC 2026
% Result : Theorem 1.23s 2.14s
% Output : CNFRefutation 1.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 6
% Syntax : Number of formulae : 27 ( 7 unt; 2 def)
% Number of atoms : 52 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 45 ( 20 ~; 16 |; 3 &)
% ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 14 ( 12 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4063,axiom,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6736,axiom,
( mtvisible(c_tptpgeo_member1_mt)
=> borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44208,axiom,
! [SPECMT,GENLMT] :
( ( genlmt(SPECMT,GENLMT)
& mtvisible(SPECMT) )
=> mtvisible(GENLMT) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44217,conjecture,
? [ARG2] :
( mtvisible(c_tptpgeo_spindlecollectormt)
=> borderson(c_georegion_l4_x45_y9,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44218,negated_conjecture,
~ ? [ARG2] :
( mtvisible(c_tptpgeo_spindlecollectormt)
=> borderson(c_georegion_l4_x45_y9,ARG2) ),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f49309,plain,
genlmt(c_tptpgeo_spindlecollectormt,c_tptpgeo_member1_mt),
inference(cnf_transformation,[status(thm)],[f4063]) ).
fof(f52674,plain,
( borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10)
| ~ mtvisible(c_tptpgeo_member1_mt) ),
inference(pre_NNF_transformation,[status(thm)],[f6736]) ).
fof(f52675,plain,
( borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10)
| ~ mtvisible(c_tptpgeo_member1_mt) ),
inference(cnf_transformation,[status(thm)],[f52674]) ).
fof(f110715,plain,
! [SPECMT,GENLMT] :
( mtvisible(GENLMT)
| ~ genlmt(SPECMT,GENLMT)
| ~ mtvisible(SPECMT) ),
inference(pre_NNF_transformation,[status(thm)],[f44208]) ).
fof(f110716,plain,
! [GENLMT] :
( mtvisible(GENLMT)
| ! [SPECMT] :
( ~ genlmt(SPECMT,GENLMT)
| ~ mtvisible(SPECMT) ) ),
inference(miniscoping,[status(thm)],[f110715]) ).
fof(f110717,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ genlmt(X0,X1)
| ~ mtvisible(X0) ),
inference(cnf_transformation,[status(thm)],[f110716]) ).
fof(f110738,plain,
! [ARG2] :
( ~ borderson(c_georegion_l4_x45_y9,ARG2)
& mtvisible(c_tptpgeo_spindlecollectormt) ),
inference(pre_NNF_transformation,[status(thm)],[f44218]) ).
fof(f110739,plain,
( ! [ARG2] : ~ borderson(c_georegion_l4_x45_y9,ARG2)
& mtvisible(c_tptpgeo_spindlecollectormt) ),
inference(miniscoping,[status(thm)],[f110738]) ).
fof(f110740,plain,
mtvisible(c_tptpgeo_spindlecollectormt),
inference(cnf_transformation,[status(thm)],[f110739]) ).
fof(f110741,plain,
! [X0] : ~ borderson(c_georegion_l4_x45_y9,X0),
inference(cnf_transformation,[status(thm)],[f110739]) ).
fof(f110876,definition,
( sQ37_spl
<=> mtvisible(c_tptpgeo_member1_mt) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f110878,plain,
( sQ37_spl
| ~ mtvisible(c_tptpgeo_member1_mt) ),
inference(component_clause,[status(thm)],[f110876]) ).
fof(f112614,definition,
( sQ492_spl
<=> borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10) ),
introduced(definition,[new_symbols(definition,[sQ492_spl])],[split_symbol_definition]) ).
fof(f112615,plain,
( ~ sQ492_spl
| borderson(c_georegion_l4_x45_y9,c_georegion_l4_x45_y10) ),
inference(component_clause,[status(thm)],[f112614]) ).
fof(f112617,plain,
( sQ492_spl
| ~ sQ37_spl ),
inference(split_clause,[status(thm)],[f52675,f110876,f112614]) ).
fof(f118237,plain,
! [X0] :
( sQ37_spl
| ~ genlmt(X0,c_tptpgeo_member1_mt)
| ~ mtvisible(X0) ),
inference(resolution,[status(thm)],[f110878,f110717]) ).
fof(f118252,plain,
( sQ37_spl
| ~ mtvisible(c_tptpgeo_spindlecollectormt) ),
inference(resolution,[status(thm)],[f118237,f49309]) ).
fof(f118253,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f118252,f110740]) ).
fof(f118254,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f118253]) ).
fof(f118255,plain,
( ~ sQ492_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f112615,f110741]) ).
fof(f118256,plain,
~ sQ492_spl,
inference(contradiction_clause,[status(thm)],[f118255]) ).
fof(f118257,plain,
$false,
inference(sat_refutation,[status(thm)],[f112617,f118254,f118256]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR048+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n010.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 14:34:58 UTC 2026
% 0.09/0.36 % CPUTime :
% 1.05/1.31 % Drodi V4.1.1
% 1.23/2.14 % Refutation found
% 1.23/2.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.23/2.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.02/2.48 % Elapsed time: 2.064723 seconds
% 5.02/2.48 % CPU time: 7.679574 seconds
% 5.02/2.48 % Total memory used: 1.877 GB
% 5.02/2.48 % Net memory used: 1.871 GB
%------------------------------------------------------------------------------