%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR036+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 13.12s 2.30s
% Output : CNFRefutation 13.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 33
% Syntax : Number of formulae : 131 ( 91 unt; 0 def)
% Number of atoms : 179 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 150 ( 102 ~; 41 |; 3 &)
% ( 0 <=>; 4 =>; 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 : 53 ( 53 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f20,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f176,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f227,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f336,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f460,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f487,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f512,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f587,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f615,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f759,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f783,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f793,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f814,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f853,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f867,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f879,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f940,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1248,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1300,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1366,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1731,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1760,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1818,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1975,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2287,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2436,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2540,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3253,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3764,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7585,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7586,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8006,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8007,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f8031,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f8095,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f8239,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f8309,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f8463,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f8626,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(thm)],[f460]) ).
fof(f8665,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[status(thm)],[f487]) ).
fof(f8700,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[status(thm)],[f512]) ).
fof(f8805,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[status(thm)],[f587]) ).
fof(f8847,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[status(thm)],[f615]) ).
fof(f9054,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[status(thm)],[f759]) ).
fof(f9088,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[status(thm)],[f783]) ).
fof(f9100,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[status(thm)],[f793]) ).
fof(f9132,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[status(thm)],[f814]) ).
fof(f9192,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[status(thm)],[f853]) ).
fof(f9214,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f867]) ).
fof(f9232,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[status(thm)],[f879]) ).
fof(f9323,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[status(thm)],[f940]) ).
fof(f9756,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f1248]) ).
fof(f9830,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[status(thm)],[f1300]) ).
fof(f9922,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[status(thm)],[f1366]) ).
fof(f10438,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[status(thm)],[f1731]) ).
fof(f10480,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[status(thm)],[f1760]) ).
fof(f10555,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[status(thm)],[f1818]) ).
fof(f10775,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[status(thm)],[f1975]) ).
fof(f11214,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[status(thm)],[f2287]) ).
fof(f11416,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[status(thm)],[f2436]) ).
fof(f11561,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[status(thm)],[f2540]) ).
fof(f12553,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(thm)],[f3253]) ).
fof(f13262,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[status(thm)],[f3764]) ).
fof(f20548,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(pre_NNF_transformation,[status(thm)],[f7585]) ).
fof(f20549,plain,
! [ARG1,NEW] :
( disjointwith(ARG1,NEW)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ) ),
inference(miniscoping,[status(thm)],[f20548]) ).
fof(f20550,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20549]) ).
fof(f20551,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f7586]) ).
fof(f20552,plain,
! [ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ) ),
inference(miniscoping,[status(thm)],[f20551]) ).
fof(f20553,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f20552]) ).
fof(f21391,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(pre_NNF_transformation,[status(thm)],[f8007]) ).
fof(f21393,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[status(thm)],[f21391]) ).
fof(f21397,plain,
! [X0] :
( ~ genls(c_tptpcol_16_72795,X0)
| ~ disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[status(thm)],[f20550,f21393]) ).
fof(f21401,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793),
inference(resolution,[status(thm)],[f21397,f8700]) ).
fof(f21406,plain,
! [X0] :
( ~ genls(c_tptpcol_15_22076,X0)
| ~ disjointwith(X0,c_tptpcol_15_72793) ),
inference(resolution,[status(thm)],[f21401,f20553]) ).
fof(f21413,plain,
~ disjointwith(c_tptpcol_14_22072,c_tptpcol_15_72793),
inference(resolution,[status(thm)],[f21406,f9830]) ).
fof(f21417,plain,
! [X0] :
( ~ genls(c_tptpcol_14_22072,X0)
| ~ disjointwith(X0,c_tptpcol_15_72793) ),
inference(resolution,[status(thm)],[f21413,f20553]) ).
fof(f21565,plain,
~ disjointwith(c_tptpcol_13_22071,c_tptpcol_15_72793),
inference(resolution,[status(thm)],[f10775,f21417]) ).
fof(f21576,plain,
! [X0] :
( ~ genls(c_tptpcol_13_22071,X0)
| ~ disjointwith(X0,c_tptpcol_15_72793) ),
inference(resolution,[status(thm)],[f21565,f20553]) ).
fof(f21590,plain,
~ disjointwith(c_tptpcol_12_22055,c_tptpcol_15_72793),
inference(resolution,[status(thm)],[f21576,f9922]) ).
fof(f21592,plain,
! [X0] :
( ~ genls(c_tptpcol_12_22055,X0)
| ~ disjointwith(X0,c_tptpcol_15_72793) ),
inference(resolution,[status(thm)],[f21590,f20553]) ).
fof(f21611,plain,
~ disjointwith(c_tptpcol_11_22023,c_tptpcol_15_72793),
inference(resolution,[status(thm)],[f21592,f9232]) ).
fof(f21612,plain,
! [X0] :
( ~ genls(c_tptpcol_11_22023,X0)
| ~ disjointwith(X0,c_tptpcol_15_72793) ),
inference(resolution,[status(thm)],[f21611,f20553]) ).
fof(f21630,plain,
~ disjointwith(c_tptpcol_10_22022,c_tptpcol_15_72793),
inference(resolution,[status(thm)],[f21612,f8665]) ).
fof(f21631,plain,
! [X0] :
( ~ genls(c_tptpcol_10_22022,X0)
| ~ disjointwith(X0,c_tptpcol_15_72793) ),
inference(resolution,[status(thm)],[f21630,f20553]) ).
fof(f21649,plain,
~ disjointwith(c_tptpcol_9_22021,c_tptpcol_15_72793),
inference(resolution,[status(thm)],[f21631,f8095]) ).
fof(f21651,plain,
! [X0] :
( ~ genls(c_tptpcol_15_72793,X0)
| ~ disjointwith(c_tptpcol_9_22021,X0) ),
inference(resolution,[status(thm)],[f21649,f20550]) ).
fof(f21847,plain,
~ disjointwith(c_tptpcol_9_22021,c_tptpcol_14_72792),
inference(resolution,[status(thm)],[f11561,f21651]) ).
fof(f21935,plain,
! [X0] :
( ~ genls(c_tptpcol_14_72792,X0)
| ~ disjointwith(c_tptpcol_9_22021,X0) ),
inference(resolution,[status(thm)],[f21847,f20550]) ).
fof(f22108,plain,
~ disjointwith(c_tptpcol_9_22021,c_tptpcol_13_72791),
inference(resolution,[status(thm)],[f21935,f10480]) ).
fof(f22110,plain,
! [X0] :
( ~ genls(c_tptpcol_13_72791,X0)
| ~ disjointwith(c_tptpcol_9_22021,X0) ),
inference(resolution,[status(thm)],[f22108,f20550]) ).
fof(f22624,plain,
~ disjointwith(c_tptpcol_9_22021,c_tptpcol_12_72775),
inference(resolution,[status(thm)],[f13262,f22110]) ).
fof(f22747,plain,
! [X0] :
( ~ genls(c_tptpcol_12_72775,X0)
| ~ disjointwith(c_tptpcol_9_22021,X0) ),
inference(resolution,[status(thm)],[f22624,f20550]) ).
fof(f23051,plain,
~ disjointwith(c_tptpcol_9_22021,c_tptpcol_11_72774),
inference(resolution,[status(thm)],[f22747,f9192]) ).
fof(f23053,plain,
! [X0] :
( ~ genls(c_tptpcol_11_72774,X0)
| ~ disjointwith(c_tptpcol_9_22021,X0) ),
inference(resolution,[status(thm)],[f23051,f20550]) ).
fof(f23150,plain,
~ disjointwith(c_tptpcol_9_22021,c_tptpcol_10_72710),
inference(resolution,[status(thm)],[f23053,f9054]) ).
fof(f23151,plain,
! [X0] :
( ~ genls(c_tptpcol_9_22021,X0)
| ~ disjointwith(X0,c_tptpcol_10_72710) ),
inference(resolution,[status(thm)],[f23150,f20553]) ).
fof(f23250,plain,
~ disjointwith(c_tptpcol_8_22020,c_tptpcol_10_72710),
inference(resolution,[status(thm)],[f23151,f10438]) ).
fof(f23255,plain,
! [X0] :
( ~ genls(c_tptpcol_8_22020,X0)
| ~ disjointwith(X0,c_tptpcol_10_72710) ),
inference(resolution,[status(thm)],[f23250,f20553]) ).
fof(f23359,plain,
~ disjointwith(c_tptpcol_7_21508,c_tptpcol_10_72710),
inference(resolution,[status(thm)],[f23255,f8463]) ).
fof(f23360,plain,
! [X0] :
( ~ genls(c_tptpcol_7_21508,X0)
| ~ disjointwith(X0,c_tptpcol_10_72710) ),
inference(resolution,[status(thm)],[f23359,f20553]) ).
fof(f23489,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_10_72710),
inference(resolution,[status(thm)],[f23360,f11416]) ).
fof(f23495,plain,
! [X0] :
( ~ genls(c_tptpcol_10_72710,X0)
| ~ disjointwith(c_tptpcol_6_20484,X0) ),
inference(resolution,[status(thm)],[f23489,f20550]) ).
fof(f23685,plain,
~ disjointwith(c_tptpcol_6_20484,c_tptpcol_9_72709),
inference(resolution,[status(thm)],[f23495,f8309]) ).
fof(f23686,plain,
! [X0] :
( ~ genls(c_tptpcol_6_20484,X0)
| ~ disjointwith(X0,c_tptpcol_9_72709) ),
inference(resolution,[status(thm)],[f23685,f20553]) ).
fof(f23862,plain,
~ disjointwith(c_tptpcol_5_20483,c_tptpcol_9_72709),
inference(resolution,[status(thm)],[f23686,f9100]) ).
fof(f23863,plain,
! [X0] :
( ~ genls(c_tptpcol_5_20483,X0)
| ~ disjointwith(X0,c_tptpcol_9_72709) ),
inference(resolution,[status(thm)],[f23862,f20553]) ).
fof(f24098,plain,
~ disjointwith(c_tptpcol_4_16387,c_tptpcol_9_72709),
inference(resolution,[status(thm)],[f23863,f10555]) ).
fof(f24104,plain,
! [X0] :
( ~ genls(c_tptpcol_9_72709,X0)
| ~ disjointwith(c_tptpcol_4_16387,X0) ),
inference(resolution,[status(thm)],[f24098,f20550]) ).
fof(f24332,plain,
~ disjointwith(c_tptpcol_4_16387,c_tptpcol_8_72708),
inference(resolution,[status(thm)],[f24104,f8847]) ).
fof(f24338,plain,
! [X0] :
( ~ genls(c_tptpcol_4_16387,X0)
| ~ disjointwith(X0,c_tptpcol_8_72708) ),
inference(resolution,[status(thm)],[f24332,f20553]) ).
fof(f24534,plain,
~ disjointwith(c_tptpcol_3_16386,c_tptpcol_8_72708),
inference(resolution,[status(thm)],[f24338,f9088]) ).
fof(f24546,plain,
! [X0] :
( ~ genls(c_tptpcol_8_72708,X0)
| ~ disjointwith(c_tptpcol_3_16386,X0) ),
inference(resolution,[status(thm)],[f24534,f20550]) ).
fof(f24779,plain,
~ disjointwith(c_tptpcol_3_16386,c_tptpcol_7_72707),
inference(resolution,[status(thm)],[f24546,f9323]) ).
fof(f24796,plain,
! [X0] :
( ~ genls(c_tptpcol_3_16386,X0)
| ~ disjointwith(X0,c_tptpcol_7_72707) ),
inference(resolution,[status(thm)],[f24779,f20553]) ).
fof(f25037,plain,
~ disjointwith(c_tptpcol_2_2,c_tptpcol_7_72707),
inference(resolution,[status(thm)],[f24796,f8626]) ).
fof(f25042,plain,
! [X0] :
( ~ genls(c_tptpcol_7_72707,X0)
| ~ disjointwith(c_tptpcol_2_2,X0) ),
inference(resolution,[status(thm)],[f25037,f20550]) ).
fof(f25245,plain,
~ disjointwith(c_tptpcol_2_2,c_tptpcol_6_71683),
inference(resolution,[status(thm)],[f25042,f11214]) ).
fof(f25251,plain,
! [X0] :
( ~ genls(c_tptpcol_6_71683,X0)
| ~ disjointwith(c_tptpcol_2_2,X0) ),
inference(resolution,[status(thm)],[f25245,f20550]) ).
fof(f25485,plain,
~ disjointwith(c_tptpcol_2_2,c_tptpcol_5_69635),
inference(resolution,[status(thm)],[f25251,f8031]) ).
fof(f25489,plain,
! [X0] :
( ~ genls(c_tptpcol_2_2,X0)
| ~ disjointwith(X0,c_tptpcol_5_69635) ),
inference(resolution,[status(thm)],[f25485,f20553]) ).
fof(f25618,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_5_69635),
inference(resolution,[status(thm)],[f25489,f12553]) ).
fof(f25620,plain,
! [X0] :
( ~ genls(c_tptpcol_5_69635,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f25618,f20550]) ).
fof(f25785,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_4_65539),
inference(resolution,[status(thm)],[f25620,f9132]) ).
fof(f25788,plain,
! [X0] :
( ~ genls(c_tptpcol_4_65539,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f25785,f20550]) ).
fof(f25912,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_3_65538),
inference(resolution,[status(thm)],[f25788,f8239]) ).
fof(f25914,plain,
! [X0] :
( ~ genls(c_tptpcol_3_65538,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f25912,f20550]) ).
fof(f26061,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[f25914,f8805]) ).
fof(f26064,plain,
! [X0] :
( ~ genls(c_tptpcol_2_65537,X0)
| ~ disjointwith(c_tptpcol_1_1,X0) ),
inference(resolution,[status(thm)],[f26061,f20550]) ).
fof(f26174,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f26064,f9214]) ).
fof(f26175,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f26174,f9756]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n009.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 14:28:42 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.24/0.55 % Drodi V4.1.1
% 13.12/2.30 % Refutation found
% 13.12/2.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.12/2.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.89/3.58 % Elapsed time: 2.972398 seconds
% 7.89/3.58 % CPU time: 13.949761 seconds
% 7.89/3.58 % Total memory used: 534.986 MB
% 7.89/3.58 % Net memory used: 531.572 MB
%------------------------------------------------------------------------------