%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR036+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:00 PM UTC 2026
% Result : Theorem 10.64s 1.91s
% Output : CNFRefutation 10.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 34
% Syntax : Number of formulae : 135 ( 91 unt; 0 def)
% Number of atoms : 191 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 138 ( 82 ~; 47 |; 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 : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 65 ( 65 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f189,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f193,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f199,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f224,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f230,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f280,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f285,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f305,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f311,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f335,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f348,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f385,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f395,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f397,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f403,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f405,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f436,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f442,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f449,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f456,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f491,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1109,axiom,
! [X,Y,Z] :
( ( genls(Y,Z)
& genls(X,Y) )
=> genls(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1121,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1122,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1132,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1133,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(negated_conjecture,[status(cth)],[f1132]) ).
fof(f1141,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f1164,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f1172,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f1175,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f1178,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f1240,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f1343,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f1353,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f1379,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f1410,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f1416,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f1424,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[status(thm)],[f199]) ).
fof(f1461,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f1470,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f1540,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[status(thm)],[f280]) ).
fof(f1548,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f1581,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f1590,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[status(thm)],[f311]) ).
fof(f1622,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f1640,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f1694,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f1709,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[status(thm)],[f395]) ).
fof(f1712,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[status(thm)],[f397]) ).
fof(f1721,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[status(thm)],[f403]) ).
fof(f1724,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[status(thm)],[f405]) ).
fof(f1769,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f1779,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f1788,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[status(thm)],[f449]) ).
fof(f1798,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[status(thm)],[f456]) ).
fof(f1852,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[status(thm)],[f491]) ).
fof(f3146,plain,
! [X,Y,Z] :
( genls(X,Z)
| ~ genls(Y,Z)
| ~ genls(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f1109]) ).
fof(f3147,plain,
! [X,Z] :
( genls(X,Z)
| ! [Y] :
( ~ genls(Y,Z)
| ~ genls(X,Y) ) ),
inference(miniscoping,[status(thm)],[f3146]) ).
fof(f3148,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3147]) ).
fof(f3175,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(pre_NNF_transformation,[status(thm)],[f1121]) ).
fof(f3176,plain,
! [ARG1,NEW] :
( disjointwith(ARG1,NEW)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ) ),
inference(miniscoping,[status(thm)],[f3175]) ).
fof(f3177,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3176]) ).
fof(f3178,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f1122]) ).
fof(f3179,plain,
! [ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ) ),
inference(miniscoping,[status(thm)],[f3178]) ).
fof(f3180,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f3179]) ).
fof(f3204,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(pre_NNF_transformation,[status(thm)],[f1133]) ).
fof(f3206,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[status(thm)],[f3204]) ).
fof(f3208,plain,
! [X0] :
( ~ genls(c_tptpcol_16_72795,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f3177,f3206]) ).
fof(f3213,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793),
inference(resolution,[status(thm)],[f3208,f1721]) ).
fof(f3215,plain,
! [X0] :
( ~ genls(c_tptpcol_15_72793,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f3213,f3177]) ).
fof(f3364,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_14_72792),
inference(resolution,[status(thm)],[f1540,f3215]) ).
fof(f3369,plain,
! [X0] :
( ~ genls(c_tptpcol_14_72792,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f3364,f3177]) ).
fof(f3384,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_13_72791),
inference(resolution,[status(thm)],[f3369,f1172]) ).
fof(f3433,plain,
! [X0] :
( ~ genls(c_tptpcol_13_72791,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f3384,f3177]) ).
fof(f3729,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_12_72775),
inference(resolution,[status(thm)],[f1852,f3433]) ).
fof(f3734,plain,
! [X0] :
( ~ genls(c_tptpcol_12_72775,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f3729,f3177]) ).
fof(f3750,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_11_72774),
inference(resolution,[status(thm)],[f3734,f1709]) ).
fof(f3774,plain,
! [X0] :
( ~ genls(c_tptpcol_11_72774,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f3750,f3177]) ).
fof(f3808,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_10_72710),
inference(resolution,[status(thm)],[f3774,f1788]) ).
fof(f3836,plain,
! [X0] :
( ~ genls(c_tptpcol_10_72710,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f3808,f3177]) ).
fof(f3875,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_9_72709),
inference(resolution,[status(thm)],[f3836,f1141]) ).
fof(f3885,plain,
! [X0] :
( ~ genls(c_tptpcol_9_72709,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f3875,f3177]) ).
fof(f4000,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_8_72708),
inference(resolution,[status(thm)],[f3885,f1424]) ).
fof(f4010,plain,
! [X0] :
( ~ genls(c_tptpcol_8_72708,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f4000,f3177]) ).
fof(f4078,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_7_72707),
inference(resolution,[status(thm)],[f4010,f1240]) ).
fof(f4094,plain,
! [X0] :
( ~ genls(c_tptpcol_7_72707,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f4078,f3177]) ).
fof(f4221,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_6_71683),
inference(resolution,[status(thm)],[f4094,f1712]) ).
fof(f4226,plain,
! [X0] :
( ~ genls(c_tptpcol_6_71683,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f4221,f3177]) ).
fof(f4367,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_5_69635),
inference(resolution,[status(thm)],[f4226,f1724]) ).
fof(f4372,plain,
! [X0] :
( ~ genls(c_tptpcol_5_69635,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f4367,f3177]) ).
fof(f4526,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_4_65539),
inference(resolution,[status(thm)],[f4372,f1461]) ).
fof(f4528,plain,
! [X0] :
( ~ genls(c_tptpcol_4_65539,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f4526,f3177]) ).
fof(f4810,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_3_65538),
inference(resolution,[status(thm)],[f4528,f1769]) ).
fof(f4812,plain,
! [X0] :
( ~ genls(c_tptpcol_3_65538,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f4810,f3177]) ).
fof(f5262,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[f4812,f1590]) ).
fof(f5290,plain,
! [X0] :
( ~ genls(c_tptpcol_2_65537,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f5262,f3177]) ).
fof(f5861,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f5290,f1640]) ).
fof(f5865,plain,
! [X0] :
( ~ genls(c_tptpcol_15_22076,X0)
| ~ disjointwith(X0,c_tptpcol_1_65536) ),
inference(resolution,[status(thm)],[f5861,f3180]) ).
fof(f7014,plain,
! [X0] :
( genls(X0,c_tptpcol_6_20484)
| ~ genls(X0,c_tptpcol_7_21508) ),
inference(resolution,[status(thm)],[f3148,f1798]) ).
fof(f7035,plain,
! [X0] :
( genls(X0,c_tptpcol_2_2)
| ~ genls(X0,c_tptpcol_3_16386) ),
inference(resolution,[status(thm)],[f3148,f1694]) ).
fof(f7052,plain,
! [X0] :
( genls(X0,c_tptpcol_5_20483)
| ~ genls(X0,c_tptpcol_6_20484) ),
inference(resolution,[status(thm)],[f3148,f1622]) ).
fof(f7060,plain,
! [X0] :
( genls(X0,c_tptpcol_7_21508)
| ~ genls(X0,c_tptpcol_8_22020) ),
inference(resolution,[status(thm)],[f3148,f1581]) ).
fof(f7063,plain,
! [X0] :
( genls(X0,c_tptpcol_3_16386)
| ~ genls(X0,c_tptpcol_4_16387) ),
inference(resolution,[status(thm)],[f3148,f1548]) ).
fof(f7080,plain,
! [X0] :
( genls(X0,c_tptpcol_12_22055)
| ~ genls(X0,c_tptpcol_13_22071) ),
inference(resolution,[status(thm)],[f3148,f1470]) ).
fof(f7090,plain,
! [X0] :
( genls(X0,c_tptpcol_9_22021)
| ~ genls(X0,c_tptpcol_10_22022) ),
inference(resolution,[status(thm)],[f3148,f1416]) ).
fof(f7092,plain,
! [X0] :
( genls(X0,c_tptpcol_13_22071)
| ~ genls(X0,c_tptpcol_14_22072) ),
inference(resolution,[status(thm)],[f3148,f1410]) ).
fof(f7099,plain,
! [X0] :
( genls(X0,c_tptpcol_11_22023)
| ~ genls(X0,c_tptpcol_12_22055) ),
inference(resolution,[status(thm)],[f3148,f1379]) ).
fof(f7104,plain,
! [X0] :
( genls(X0,c_tptpcol_1_1)
| ~ genls(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f3148,f1343]) ).
fof(f7137,plain,
! [X0] :
( genls(X0,c_tptpcol_10_22022)
| ~ genls(X0,c_tptpcol_11_22023) ),
inference(resolution,[status(thm)],[f3148,f1178]) ).
fof(f7138,plain,
! [X0] :
( genls(X0,c_tptpcol_4_16387)
| ~ genls(X0,c_tptpcol_5_20483) ),
inference(resolution,[status(thm)],[f3148,f1175]) ).
fof(f7141,plain,
! [X0] :
( genls(X0,c_tptpcol_8_22020)
| ~ genls(X0,c_tptpcol_9_22021) ),
inference(resolution,[status(thm)],[f3148,f1164]) ).
fof(f12135,plain,
genls(c_tptpcol_15_22076,c_tptpcol_13_22071),
inference(resolution,[status(thm)],[f7092,f1779]) ).
fof(f12188,plain,
genls(c_tptpcol_15_22076,c_tptpcol_12_22055),
inference(resolution,[status(thm)],[f12135,f7080]) ).
fof(f12382,plain,
genls(c_tptpcol_15_22076,c_tptpcol_11_22023),
inference(resolution,[status(thm)],[f7099,f12188]) ).
fof(f13113,plain,
genls(c_tptpcol_15_22076,c_tptpcol_10_22022),
inference(resolution,[status(thm)],[f7137,f12382]) ).
fof(f13162,plain,
genls(c_tptpcol_15_22076,c_tptpcol_9_22021),
inference(resolution,[status(thm)],[f13113,f7090]) ).
fof(f13325,plain,
genls(c_tptpcol_15_22076,c_tptpcol_8_22020),
inference(resolution,[status(thm)],[f7141,f13162]) ).
fof(f13546,plain,
genls(c_tptpcol_15_22076,c_tptpcol_7_21508),
inference(resolution,[status(thm)],[f13325,f7060]) ).
fof(f13794,plain,
genls(c_tptpcol_15_22076,c_tptpcol_6_20484),
inference(resolution,[status(thm)],[f13546,f7014]) ).
fof(f14122,plain,
genls(c_tptpcol_15_22076,c_tptpcol_5_20483),
inference(resolution,[status(thm)],[f13794,f7052]) ).
fof(f14393,plain,
genls(c_tptpcol_15_22076,c_tptpcol_4_16387),
inference(resolution,[status(thm)],[f14122,f7138]) ).
fof(f14640,plain,
genls(c_tptpcol_15_22076,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[f14393,f7063]) ).
fof(f14899,plain,
genls(c_tptpcol_15_22076,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f14640,f7035]) ).
fof(f15208,plain,
genls(c_tptpcol_15_22076,c_tptpcol_1_1),
inference(resolution,[status(thm)],[f14899,f7104]) ).
fof(f15732,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f15208,f5865]) ).
fof(f15766,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f15732,f1353]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 14:30:36 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.43 % Drodi V4.1.1
% 10.64/1.91 % Refutation found
% 10.64/1.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.64/1.91 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.68/3.16 % Elapsed time: 2.554385 seconds
% 10.68/3.16 % CPU time: 11.610692 seconds
% 10.68/3.16 % Total memory used: 205.933 MB
% 10.68/3.16 % Net memory used: 201.541 MB
%------------------------------------------------------------------------------