%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:12:59 PM UTC 2026
% Result : Theorem 0.14s 0.41s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% 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 : 106 ( 50 ~; 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_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,axiom,
! [X,Y,Z] :
( ( genls(Y,Z)
& genls(X,Y) )
=> genls(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(negated_conjecture,[status(cth)],[f174]) ).
fof(f181,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f184,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f187,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f190,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f193,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f196,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f199,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f202,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f205,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f208,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f211,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f214,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f217,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f220,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f223,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f226,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f229,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f232,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f235,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f238,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f241,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f244,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f247,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f250,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f253,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f256,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f259,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f262,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f265,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f268,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f318,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f319,plain,
! [ARG1,NEW] :
( disjointwith(ARG1,NEW)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ) ),
inference(miniscoping,[status(thm)],[f318]) ).
fof(f320,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f319]) ).
fof(f321,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f322,plain,
! [ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ! [OLD] :
( ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ) ),
inference(miniscoping,[status(thm)],[f321]) ).
fof(f323,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f322]) ).
fof(f460,plain,
! [X,Y,Z] :
( genls(X,Z)
| ~ genls(Y,Z)
| ~ genls(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f152]) ).
fof(f461,plain,
! [X,Z] :
( genls(X,Z)
| ! [Y] :
( ~ genls(Y,Z)
| ~ genls(X,Y) ) ),
inference(miniscoping,[status(thm)],[f460]) ).
fof(f462,plain,
! [X0,X1,X2] :
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f461]) ).
fof(f516,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(pre_NNF_transformation,[status(thm)],[f175]) ).
fof(f518,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f519,plain,
! [X0] :
( disjointwith(X0,c_tptpcol_1_65536)
| ~ genls(X0,c_tptpcol_1_1) ),
inference(resolution,[status(thm)],[f268,f323]) ).
fof(f522,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(resolution,[status(thm)],[f519,f181]) ).
fof(f527,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_1_65536) ),
inference(resolution,[status(thm)],[f522,f320]) ).
fof(f543,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_2_65537),
inference(resolution,[status(thm)],[f527,f223]) ).
fof(f548,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_2_65537) ),
inference(resolution,[status(thm)],[f543,f320]) ).
fof(f571,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_3_65538),
inference(resolution,[status(thm)],[f548,f226]) ).
fof(f580,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_3_65538) ),
inference(resolution,[status(thm)],[f571,f320]) ).
fof(f615,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_4_65539),
inference(resolution,[status(thm)],[f580,f229]) ).
fof(f626,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_4_65539) ),
inference(resolution,[status(thm)],[f615,f320]) ).
fof(f676,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_5_69635),
inference(resolution,[status(thm)],[f626,f232]) ).
fof(f684,plain,
! [X0] :
( disjointwith(c_tptpcol_2_2,X0)
| ~ genls(X0,c_tptpcol_5_69635) ),
inference(resolution,[status(thm)],[f676,f320]) ).
fof(f755,plain,
! [X0] :
( genls(X0,c_tptpcol_14_72792)
| ~ genls(X0,c_tptpcol_15_72793) ),
inference(resolution,[status(thm)],[f462,f262]) ).
fof(f756,plain,
! [X0] :
( genls(X0,c_tptpcol_13_72791)
| ~ genls(X0,c_tptpcol_14_72792) ),
inference(resolution,[status(thm)],[f462,f259]) ).
fof(f757,plain,
! [X0] :
( genls(X0,c_tptpcol_12_72775)
| ~ genls(X0,c_tptpcol_13_72791) ),
inference(resolution,[status(thm)],[f462,f256]) ).
fof(f758,plain,
! [X0] :
( genls(X0,c_tptpcol_11_72774)
| ~ genls(X0,c_tptpcol_12_72775) ),
inference(resolution,[status(thm)],[f462,f253]) ).
fof(f759,plain,
! [X0] :
( genls(X0,c_tptpcol_10_72710)
| ~ genls(X0,c_tptpcol_11_72774) ),
inference(resolution,[status(thm)],[f462,f250]) ).
fof(f760,plain,
! [X0] :
( genls(X0,c_tptpcol_9_72709)
| ~ genls(X0,c_tptpcol_10_72710) ),
inference(resolution,[status(thm)],[f462,f247]) ).
fof(f761,plain,
! [X0] :
( genls(X0,c_tptpcol_8_72708)
| ~ genls(X0,c_tptpcol_9_72709) ),
inference(resolution,[status(thm)],[f462,f244]) ).
fof(f762,plain,
! [X0] :
( genls(X0,c_tptpcol_7_72707)
| ~ genls(X0,c_tptpcol_8_72708) ),
inference(resolution,[status(thm)],[f462,f241]) ).
fof(f763,plain,
! [X0] :
( genls(X0,c_tptpcol_6_71683)
| ~ genls(X0,c_tptpcol_7_72707) ),
inference(resolution,[status(thm)],[f462,f238]) ).
fof(f764,plain,
! [X0] :
( genls(X0,c_tptpcol_5_69635)
| ~ genls(X0,c_tptpcol_6_71683) ),
inference(resolution,[status(thm)],[f462,f235]) ).
fof(f769,plain,
! [X0] :
( genls(X0,c_tptpcol_13_22071)
| ~ genls(X0,c_tptpcol_14_22072) ),
inference(resolution,[status(thm)],[f462,f217]) ).
fof(f770,plain,
! [X0] :
( genls(X0,c_tptpcol_12_22055)
| ~ genls(X0,c_tptpcol_13_22071) ),
inference(resolution,[status(thm)],[f462,f214]) ).
fof(f771,plain,
! [X0] :
( genls(X0,c_tptpcol_11_22023)
| ~ genls(X0,c_tptpcol_12_22055) ),
inference(resolution,[status(thm)],[f462,f211]) ).
fof(f772,plain,
! [X0] :
( genls(X0,c_tptpcol_10_22022)
| ~ genls(X0,c_tptpcol_11_22023) ),
inference(resolution,[status(thm)],[f462,f208]) ).
fof(f773,plain,
! [X0] :
( genls(X0,c_tptpcol_9_22021)
| ~ genls(X0,c_tptpcol_10_22022) ),
inference(resolution,[status(thm)],[f462,f205]) ).
fof(f774,plain,
! [X0] :
( genls(X0,c_tptpcol_8_22020)
| ~ genls(X0,c_tptpcol_9_22021) ),
inference(resolution,[status(thm)],[f462,f202]) ).
fof(f775,plain,
! [X0] :
( genls(X0,c_tptpcol_7_21508)
| ~ genls(X0,c_tptpcol_8_22020) ),
inference(resolution,[status(thm)],[f462,f199]) ).
fof(f776,plain,
! [X0] :
( genls(X0,c_tptpcol_6_20484)
| ~ genls(X0,c_tptpcol_7_21508) ),
inference(resolution,[status(thm)],[f462,f196]) ).
fof(f777,plain,
! [X0] :
( genls(X0,c_tptpcol_5_20483)
| ~ genls(X0,c_tptpcol_6_20484) ),
inference(resolution,[status(thm)],[f462,f193]) ).
fof(f778,plain,
! [X0] :
( genls(X0,c_tptpcol_4_16387)
| ~ genls(X0,c_tptpcol_5_20483) ),
inference(resolution,[status(thm)],[f462,f190]) ).
fof(f779,plain,
! [X0] :
( genls(X0,c_tptpcol_3_16386)
| ~ genls(X0,c_tptpcol_4_16387) ),
inference(resolution,[status(thm)],[f462,f187]) ).
fof(f780,plain,
! [X0] :
( genls(X0,c_tptpcol_2_2)
| ~ genls(X0,c_tptpcol_3_16386) ),
inference(resolution,[status(thm)],[f462,f184]) ).
fof(f992,plain,
genls(c_tptpcol_16_72795,c_tptpcol_14_72792),
inference(resolution,[status(thm)],[f755,f265]) ).
fof(f1025,plain,
genls(c_tptpcol_16_72795,c_tptpcol_13_72791),
inference(resolution,[status(thm)],[f756,f992]) ).
fof(f1036,plain,
genls(c_tptpcol_16_72795,c_tptpcol_12_72775),
inference(resolution,[status(thm)],[f1025,f757]) ).
fof(f1040,plain,
genls(c_tptpcol_16_72795,c_tptpcol_11_72774),
inference(resolution,[status(thm)],[f1036,f758]) ).
fof(f1055,plain,
genls(c_tptpcol_16_72795,c_tptpcol_10_72710),
inference(resolution,[status(thm)],[f1040,f759]) ).
fof(f1060,plain,
genls(c_tptpcol_16_72795,c_tptpcol_9_72709),
inference(resolution,[status(thm)],[f1055,f760]) ).
fof(f1088,plain,
genls(c_tptpcol_16_72795,c_tptpcol_8_72708),
inference(resolution,[status(thm)],[f1060,f761]) ).
fof(f1092,plain,
genls(c_tptpcol_16_72795,c_tptpcol_7_72707),
inference(resolution,[status(thm)],[f1088,f762]) ).
fof(f1096,plain,
genls(c_tptpcol_16_72795,c_tptpcol_6_71683),
inference(resolution,[status(thm)],[f1092,f763]) ).
fof(f1103,plain,
genls(c_tptpcol_16_72795,c_tptpcol_5_69635),
inference(resolution,[status(thm)],[f1096,f764]) ).
fof(f1122,plain,
genls(c_tptpcol_15_22076,c_tptpcol_13_22071),
inference(resolution,[status(thm)],[f769,f220]) ).
fof(f1129,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[f1103,f684]) ).
fof(f1135,plain,
genls(c_tptpcol_15_22076,c_tptpcol_12_22055),
inference(resolution,[status(thm)],[f1122,f770]) ).
fof(f1139,plain,
genls(c_tptpcol_15_22076,c_tptpcol_11_22023),
inference(resolution,[status(thm)],[f1135,f771]) ).
fof(f1154,plain,
genls(c_tptpcol_15_22076,c_tptpcol_10_22022),
inference(resolution,[status(thm)],[f1139,f772]) ).
fof(f1159,plain,
genls(c_tptpcol_15_22076,c_tptpcol_9_22021),
inference(resolution,[status(thm)],[f1154,f773]) ).
fof(f1198,plain,
genls(c_tptpcol_15_22076,c_tptpcol_8_22020),
inference(resolution,[status(thm)],[f1159,f774]) ).
fof(f1209,plain,
! [X0] :
( disjointwith(X0,c_tptpcol_16_72795)
| ~ genls(X0,c_tptpcol_2_2) ),
inference(resolution,[status(thm)],[f1129,f323]) ).
fof(f1213,plain,
genls(c_tptpcol_15_22076,c_tptpcol_7_21508),
inference(resolution,[status(thm)],[f1198,f775]) ).
fof(f1218,plain,
genls(c_tptpcol_15_22076,c_tptpcol_6_20484),
inference(resolution,[status(thm)],[f1213,f776]) ).
fof(f1288,plain,
genls(c_tptpcol_15_22076,c_tptpcol_5_20483),
inference(resolution,[status(thm)],[f1218,f777]) ).
fof(f1307,plain,
genls(c_tptpcol_15_22076,c_tptpcol_4_16387),
inference(resolution,[status(thm)],[f1288,f778]) ).
fof(f1380,plain,
genls(c_tptpcol_15_22076,c_tptpcol_3_16386),
inference(resolution,[status(thm)],[f1307,f779]) ).
fof(f1412,plain,
genls(c_tptpcol_15_22076,c_tptpcol_2_2),
inference(resolution,[status(thm)],[f1380,f780]) ).
fof(f1778,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(resolution,[status(thm)],[f1412,f1209]) ).
fof(f1794,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1778,f518]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+1 : 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.35 % Computer : n011.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:27:55 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.44 % Elapsed time: 0.081681 seconds
% 0.14/0.44 % CPU time: 0.375399 seconds
% 0.14/0.44 % Total memory used: 67.209 MB
% 0.14/0.44 % Net memory used: 66.982 MB
%------------------------------------------------------------------------------