%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR061+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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:18 PM UTC 2026
% Result : Theorem 0.12s 0.40s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 21
% Syntax : Number of formulae : 83 ( 52 unt; 0 def)
% Number of atoms : 126 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 80 ( 37 ~; 34 |; 4 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 52 ( 52 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [X,Y,Z] :
( ( genls(Y,Z)
& genls(X,Y) )
=> genls(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,conjecture,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,negated_conjecture,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(negated_conjecture,[status(cth)],[f119]) ).
fof(f125,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f128,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f131,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f134,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f137,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f140,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f143,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f146,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f149,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f152,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f155,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f158,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f161,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f164,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f167,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f170,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f173,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f221,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f222,plain,
! [ARG1,NEW] :
( disjointwith(ARG1,NEW)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ) ),
inference(miniscoping,[status(thm)],[f221]) ).
fof(f223,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f224,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f225,plain,
! [ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ) ),
inference(miniscoping,[status(thm)],[f224]) ).
fof(f226,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f225]) ).
fof(f311,plain,
! [X,Y,Z] :
( genls(X,Z)
| ~ genls(Y,Z)
| ~ genls(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f312,plain,
! [X,Z] :
( genls(X,Z)
| ! [Y] :
( ~ genls(Y,Z)
| ~ genls(X,Y) ) ),
inference(miniscoping,[status(thm)],[f311]) ).
fof(f313,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f367,plain,
( ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)
& mtvisible(c_timehasnoendmt) ),
inference(pre_NNF_transformation,[status(thm)],[f120]) ).
fof(f369,plain,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(cnf_transformation,[status(thm)],[f367]) ).
fof(f371,plain,
! [X0] :
( disjointwith(c_tptpcol_3_98305,X0)
| ~ genls(X0,c_tptpcol_3_114688) ),
inference(resolution,[status(thm)],[f173,f223]) ).
fof(f384,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_4_114689),
inference(resolution,[status(thm)],[f371,f140]) ).
fof(f387,plain,
! [X0] :
( disjointwith(c_tptpcol_3_98305,X0)
| ~ genls(X0,c_tptpcol_4_114689) ),
inference(resolution,[status(thm)],[f384,f223]) ).
fof(f408,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_5_114690),
inference(resolution,[status(thm)],[f387,f143]) ).
fof(f409,plain,
! [X0] :
( disjointwith(X0,c_tptpcol_5_114690)
| ~ genls(X0,c_tptpcol_3_98305) ),
inference(resolution,[status(thm)],[f408,f226]) ).
fof(f559,plain,
! [X0] :
( genls(X0,c_tptpcol_12_118116)
| ~ genls(X0,c_tptpcol_13_118117) ),
inference(resolution,[status(thm)],[f313,f167]) ).
fof(f560,plain,
! [X0] :
( genls(X0,c_tptpcol_11_118084)
| ~ genls(X0,c_tptpcol_12_118116) ),
inference(resolution,[status(thm)],[f313,f164]) ).
fof(f561,plain,
! [X0] :
( genls(X0,c_tptpcol_10_118020)
| ~ genls(X0,c_tptpcol_11_118084) ),
inference(resolution,[status(thm)],[f313,f161]) ).
fof(f562,plain,
! [X0] :
( genls(X0,c_tptpcol_9_118019)
| ~ genls(X0,c_tptpcol_10_118020) ),
inference(resolution,[status(thm)],[f313,f158]) ).
fof(f563,plain,
! [X0] :
( genls(X0,c_tptpcol_8_117763)
| ~ genls(X0,c_tptpcol_9_118019) ),
inference(resolution,[status(thm)],[f313,f155]) ).
fof(f565,plain,
! [X0] :
( genls(X0,c_tptpcol_6_116738)
| ~ genls(X0,c_tptpcol_7_117762) ),
inference(resolution,[status(thm)],[f313,f149]) ).
fof(f566,plain,
! [X0] :
( genls(X0,c_tptpcol_5_114690)
| ~ genls(X0,c_tptpcol_6_116738) ),
inference(resolution,[status(thm)],[f313,f146]) ).
fof(f569,plain,
! [X0] :
( genls(X0,c_tptpcol_6_112641)
| ~ genls(X0,c_tptpcol_7_113665) ),
inference(resolution,[status(thm)],[f313,f134]) ).
fof(f570,plain,
! [X0] :
( genls(X0,c_tptpcol_5_110593)
| ~ genls(X0,c_tptpcol_6_112641) ),
inference(resolution,[status(thm)],[f313,f131]) ).
fof(f571,plain,
! [X0] :
( genls(X0,c_tptpcol_4_106497)
| ~ genls(X0,c_tptpcol_5_110593) ),
inference(resolution,[status(thm)],[f313,f128]) ).
fof(f572,plain,
! [X0] :
( genls(X0,c_tptpcol_3_98305)
| ~ genls(X0,c_tptpcol_4_106497) ),
inference(resolution,[status(thm)],[f313,f125]) ).
fof(f800,plain,
genls(c_tptpcol_14_118118,c_tptpcol_12_118116),
inference(resolution,[status(thm)],[f559,f170]) ).
fof(f824,plain,
genls(c_tptpcol_14_118118,c_tptpcol_11_118084),
inference(resolution,[status(thm)],[f560,f800]) ).
fof(f856,plain,
genls(c_tptpcol_8_117763,c_tptpcol_6_116738),
inference(resolution,[status(thm)],[f565,f152]) ).
fof(f858,plain,
genls(c_tptpcol_14_118118,c_tptpcol_10_118020),
inference(resolution,[status(thm)],[f824,f561]) ).
fof(f885,plain,
genls(c_tptpcol_14_118118,c_tptpcol_9_118019),
inference(resolution,[status(thm)],[f858,f562]) ).
fof(f890,plain,
genls(c_tptpcol_8_114177,c_tptpcol_6_112641),
inference(resolution,[status(thm)],[f569,f137]) ).
fof(f895,plain,
genls(c_tptpcol_8_114177,c_tptpcol_5_110593),
inference(resolution,[status(thm)],[f890,f570]) ).
fof(f904,plain,
genls(c_tptpcol_8_114177,c_tptpcol_4_106497),
inference(resolution,[status(thm)],[f895,f571]) ).
fof(f919,plain,
genls(c_tptpcol_8_114177,c_tptpcol_3_98305),
inference(resolution,[status(thm)],[f904,f572]) ).
fof(f936,plain,
genls(c_tptpcol_14_118118,c_tptpcol_8_117763),
inference(resolution,[status(thm)],[f885,f563]) ).
fof(f958,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_5_114690),
inference(resolution,[status(thm)],[f919,f409]) ).
fof(f980,plain,
! [X0] :
( genls(X0,c_tptpcol_6_116738)
| ~ genls(X0,c_tptpcol_8_117763) ),
inference(resolution,[status(thm)],[f856,f313]) ).
fof(f1037,plain,
! [X0] :
( disjointwith(c_tptpcol_8_114177,X0)
| ~ genls(X0,c_tptpcol_5_114690) ),
inference(resolution,[status(thm)],[f958,f223]) ).
fof(f1157,plain,
genls(c_tptpcol_14_118118,c_tptpcol_6_116738),
inference(resolution,[status(thm)],[f980,f936]) ).
fof(f1176,plain,
genls(c_tptpcol_14_118118,c_tptpcol_5_114690),
inference(resolution,[status(thm)],[f1157,f566]) ).
fof(f1326,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(resolution,[status(thm)],[f1176,f1037]) ).
fof(f1338,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1326,f369]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR061+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 14:40:11 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.40 % Refutation found
% 0.12/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.43 % Elapsed time: 0.065351 seconds
% 0.12/0.43 % CPU time: 0.236550 seconds
% 0.12/0.43 % Total memory used: 61.661 MB
% 0.12/0.43 % Net memory used: 61.555 MB
%------------------------------------------------------------------------------