%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR036+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 : Sun Sep 27 07:06:42 AM UTC 2026
% Result : Theorem 52.54s 8.42s
% Output : CNFRefutation 52.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 35
% Syntax : Number of formulae : 132 ( 91 unt; 0 def)
% Number of atoms : 180 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 95 ( 47 ~; 39 |; 3 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 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 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1_1109,axiom,
! [X,Y,Z] :
( ( genls(Y,Z)
& genls(X,Y) )
=> genls(X,Z) ),
file('theBenchmark.p',ax1_1109) ).
fof(ax1_1120,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('theBenchmark.p',ax1_1120) ).
fof(ax1_1121,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('theBenchmark.p',ax1_1121) ).
fof(ax1_1122,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('theBenchmark.p',ax1_1122) ).
fof(query86,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('theBenchmark.p',query86) ).
fof(query86_neg,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(assume_negation,[status(cth)],[query86]) ).
fof(ax1_6,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('theBenchmark.p',ax1_6) ).
cnf(c_1257,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(clausify,[status(thm)],[ax1_6]) ).
fof(ax1_21,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('theBenchmark.p',ax1_21) ).
cnf(c_1268,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(clausify,[status(thm)],[ax1_21]) ).
fof(ax1_26,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('theBenchmark.p',ax1_26) ).
cnf(c_1272,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(clausify,[status(thm)],[ax1_26]) ).
fof(ax1_28,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('theBenchmark.p',ax1_28) ).
cnf(c_1274,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(clausify,[status(thm)],[ax1_28]) ).
fof(ax1_30,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('theBenchmark.p',ax1_30) ).
cnf(c_1276,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(clausify,[status(thm)],[ax1_30]) ).
fof(ax1_74,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('theBenchmark.p',ax1_74) ).
cnf(c_1302,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(clausify,[status(thm)],[ax1_74]) ).
fof(ax1_145,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('theBenchmark.p',ax1_145) ).
cnf(c_1337,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(clausify,[status(thm)],[ax1_145]) ).
fof(ax1_152,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('theBenchmark.p',ax1_152) ).
cnf(c_1343,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[ax1_152]) ).
fof(ax1_168,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('theBenchmark.p',ax1_168) ).
cnf(c_1353,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(clausify,[status(thm)],[ax1_168]) ).
fof(ax1_189,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('theBenchmark.p',ax1_189) ).
cnf(c_1365,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(clausify,[status(thm)],[ax1_189]) ).
fof(ax1_193,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('theBenchmark.p',ax1_193) ).
cnf(c_1369,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(clausify,[status(thm)],[ax1_193]) ).
fof(ax1_199,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('theBenchmark.p',ax1_199) ).
cnf(c_1374,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(clausify,[status(thm)],[ax1_199]) ).
fof(ax1_224,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('theBenchmark.p',ax1_224) ).
cnf(c_1388,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(clausify,[status(thm)],[ax1_224]) ).
fof(ax1_230,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('theBenchmark.p',ax1_230) ).
cnf(c_1394,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(clausify,[status(thm)],[ax1_230]) ).
fof(ax1_280,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('theBenchmark.p',ax1_280) ).
cnf(c_1423,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(clausify,[status(thm)],[ax1_280]) ).
fof(ax1_285,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('theBenchmark.p',ax1_285) ).
cnf(c_1425,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(clausify,[status(thm)],[ax1_285]) ).
fof(ax1_305,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('theBenchmark.p',ax1_305) ).
cnf(c_1435,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(clausify,[status(thm)],[ax1_305]) ).
fof(ax1_311,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('theBenchmark.p',ax1_311) ).
cnf(c_1440,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(clausify,[status(thm)],[ax1_311]) ).
fof(ax1_335,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('theBenchmark.p',ax1_335) ).
cnf(c_1451,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(clausify,[status(thm)],[ax1_335]) ).
fof(ax1_348,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('theBenchmark.p',ax1_348) ).
cnf(c_1459,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[ax1_348]) ).
fof(ax1_385,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('theBenchmark.p',ax1_385) ).
cnf(c_1486,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(clausify,[status(thm)],[ax1_385]) ).
fof(ax1_395,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('theBenchmark.p',ax1_395) ).
cnf(c_1496,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(clausify,[status(thm)],[ax1_395]) ).
fof(ax1_397,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('theBenchmark.p',ax1_397) ).
cnf(c_1498,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(clausify,[status(thm)],[ax1_397]) ).
fof(ax1_403,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('theBenchmark.p',ax1_403) ).
cnf(c_1502,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(clausify,[status(thm)],[ax1_403]) ).
fof(ax1_405,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('theBenchmark.p',ax1_405) ).
cnf(c_1504,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(clausify,[status(thm)],[ax1_405]) ).
fof(ax1_436,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('theBenchmark.p',ax1_436) ).
cnf(c_1521,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(clausify,[status(thm)],[ax1_436]) ).
fof(ax1_442,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('theBenchmark.p',ax1_442) ).
cnf(c_1523,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(clausify,[status(thm)],[ax1_442]) ).
fof(ax1_449,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('theBenchmark.p',ax1_449) ).
cnf(c_1527,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(clausify,[status(thm)],[ax1_449]) ).
fof(ax1_456,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('theBenchmark.p',ax1_456) ).
cnf(c_1529,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(clausify,[status(thm)],[ax1_456]) ).
fof(ax1_491,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('theBenchmark.p',ax1_491) ).
cnf(c_1550,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(clausify,[status(thm)],[ax1_491]) ).
cnf(c_1947,plain,
( genls(A,C)
| ~ genls(B,C)
| ~ genls(A,B) ),
inference(clausify,[status(thm)],[ax1_1109]) ).
cnf(c_1954,plain,
( disjointwith(B,A)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[ax1_1120]) ).
cnf(c_1955,plain,
( disjointwith(A,C)
| ~ genls(C,B)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[ax1_1121]) ).
cnf(c_1956,plain,
( disjointwith(C,B)
| ~ genls(C,A)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[ax1_1122]) ).
cnf(c_1963,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(clausify,[status(thm)],[query86_neg]) ).
cnf(c_28704,plain,
( disjointwith(A,c_tptpcol_16_72795)
| ~ disjointwith(A,c_tptpcol_15_72793) ),
inference(resolve,[status(thm)],[c_1955,c_1502]) ).
cnf(c_2213,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793),
inference(resolve,[status(thm)],[c_28704,c_1963]) ).
cnf(c_2225,plain,
( ~ genls(c_tptpcol_15_72793,A)
| ~ disjointwith(c_tptpcol_15_22076,A) ),
inference(resolve,[status(thm)],[c_2213,c_1955]) ).
cnf(c_2255,plain,
( ~ disjointwith(A,c_tptpcol_15_22076)
| ~ genls(c_tptpcol_15_72793,A) ),
inference(resolve,[status(thm)],[c_2225,c_1954]) ).
cnf(c_2583,plain,
( ~ genls(A,B)
| ~ disjointwith(B,c_tptpcol_15_22076)
| ~ genls(c_tptpcol_15_72793,A) ),
inference(resolve,[status(thm)],[c_2255,c_1956]) ).
cnf(c_28705,plain,
( genls(c_tptpcol_15_22076,A)
| ~ genls(c_tptpcol_14_22072,A) ),
inference(resolve,[status(thm)],[c_1947,c_1523]) ).
cnf(c_3205,plain,
genls(c_tptpcol_15_22076,c_tptpcol_13_22071),
inference(resolve,[status(thm)],[c_28705,c_1365]) ).
cnf(c_28706,plain,
( genls(c_tptpcol_15_72793,A)
| ~ genls(c_tptpcol_14_72792,A) ),
inference(resolve,[status(thm)],[c_1947,c_1423]) ).
cnf(c_3207,plain,
genls(c_tptpcol_15_72793,c_tptpcol_13_72791),
inference(resolve,[status(thm)],[c_28706,c_1272]) ).
cnf(c_28707,plain,
( disjointwith(A,c_tptpcol_1_65536)
| ~ genls(A,c_tptpcol_1_1) ),
inference(resolve,[status(thm)],[c_1956,c_1343]) ).
cnf(c_4142,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(resolve,[status(thm)],[c_28707,c_1337]) ).
cnf(c_28708,plain,
( genls(c_tptpcol_12_22055,A)
| ~ genls(c_tptpcol_11_22023,A) ),
inference(resolve,[status(thm)],[c_1947,c_1353]) ).
cnf(c_4364,plain,
genls(c_tptpcol_12_22055,c_tptpcol_10_22022),
inference(resolve,[status(thm)],[c_28708,c_1276]) ).
cnf(c_28709,plain,
( genls(c_tptpcol_10_22022,A)
| ~ genls(c_tptpcol_9_22021,A) ),
inference(resolve,[status(thm)],[c_1947,c_1369]) ).
cnf(c_4587,plain,
genls(c_tptpcol_10_22022,c_tptpcol_8_22020),
inference(resolve,[status(thm)],[c_28709,c_1268]) ).
cnf(c_28710,plain,
( genls(c_tptpcol_10_72710,A)
| ~ genls(c_tptpcol_9_72709,A) ),
inference(resolve,[status(thm)],[c_1947,c_1257]) ).
cnf(c_4681,plain,
genls(c_tptpcol_10_72710,c_tptpcol_8_72708),
inference(resolve,[status(thm)],[c_28710,c_1374]) ).
cnf(c_4778,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference(resolve,[status(thm)],[c_1954,c_4142]) ).
cnf(c_28711,plain,
( genls(c_tptpcol_15_22076,A)
| ~ genls(c_tptpcol_13_22071,A) ),
inference(resolve,[status(thm)],[c_1947,c_3205]) ).
cnf(c_4907,plain,
genls(c_tptpcol_15_22076,c_tptpcol_12_22055),
inference(resolve,[status(thm)],[c_28711,c_1394]) ).
cnf(c_28712,plain,
( genls(c_tptpcol_5_20483,A)
| ~ genls(c_tptpcol_4_16387,A) ),
inference(resolve,[status(thm)],[c_1947,c_1274]) ).
cnf(c_5305,plain,
genls(c_tptpcol_5_20483,c_tptpcol_3_16386),
inference(resolve,[status(thm)],[c_28712,c_1425]) ).
cnf(c_28713,plain,
( genls(c_tptpcol_10_72710,A)
| ~ genls(c_tptpcol_8_72708,A) ),
inference(resolve,[status(thm)],[c_1947,c_4681]) ).
cnf(c_5544,plain,
genls(c_tptpcol_10_72710,c_tptpcol_7_72707),
inference(resolve,[status(thm)],[c_28713,c_1302]) ).
cnf(c_28714,plain,
( genls(c_tptpcol_10_22022,A)
| ~ genls(c_tptpcol_8_22020,A) ),
inference(resolve,[status(thm)],[c_1947,c_4587]) ).
cnf(c_5591,plain,
genls(c_tptpcol_10_22022,c_tptpcol_7_21508),
inference(resolve,[status(thm)],[c_28714,c_1435]) ).
cnf(c_28715,plain,
( genls(c_tptpcol_15_22076,A)
| ~ genls(c_tptpcol_12_22055,A) ),
inference(resolve,[status(thm)],[c_1947,c_4907]) ).
cnf(c_5780,plain,
genls(c_tptpcol_15_22076,c_tptpcol_10_22022),
inference(resolve,[status(thm)],[c_28715,c_4364]) ).
cnf(c_28716,plain,
( disjointwith(A,c_tptpcol_2_2)
| ~ genls(A,c_tptpcol_1_65536) ),
inference(resolve,[status(thm)],[c_1956,c_4778]) ).
cnf(c_5835,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_2_2),
inference(resolve,[status(thm)],[c_28716,c_1459]) ).
cnf(c_28717,plain,
( genls(c_tptpcol_6_20484,A)
| ~ genls(c_tptpcol_5_20483,A) ),
inference(resolve,[status(thm)],[c_1947,c_1451]) ).
cnf(c_6171,plain,
genls(c_tptpcol_6_20484,c_tptpcol_3_16386),
inference(resolve,[status(thm)],[c_28717,c_5305]) ).
cnf(c_28718,plain,
( genls(c_tptpcol_6_71683,A)
| ~ genls(c_tptpcol_5_69635,A) ),
inference(resolve,[status(thm)],[c_1947,c_1504]) ).
cnf(c_6300,plain,
genls(c_tptpcol_6_71683,c_tptpcol_4_65539),
inference(resolve,[status(thm)],[c_28718,c_1388]) ).
cnf(c_28719,plain,
( genls(c_tptpcol_10_72710,A)
| ~ genls(c_tptpcol_7_72707,A) ),
inference(resolve,[status(thm)],[c_1947,c_5544]) ).
cnf(c_6409,plain,
genls(c_tptpcol_10_72710,c_tptpcol_6_71683),
inference(resolve,[status(thm)],[c_28719,c_1498]) ).
cnf(c_28720,plain,
( genls(c_tptpcol_15_22076,A)
| ~ genls(c_tptpcol_10_22022,A) ),
inference(resolve,[status(thm)],[c_1947,c_5780]) ).
cnf(c_6911,plain,
genls(c_tptpcol_15_22076,c_tptpcol_7_21508),
inference(resolve,[status(thm)],[c_28720,c_5591]) ).
cnf(c_28721,plain,
( disjointwith(c_tptpcol_2_65537,A)
| ~ genls(A,c_tptpcol_2_2) ),
inference(resolve,[status(thm)],[c_1955,c_5835]) ).
cnf(c_6960,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386),
inference(resolve,[status(thm)],[c_28721,c_1486]) ).
cnf(c_28722,plain,
( genls(c_tptpcol_4_65539,A)
| ~ genls(c_tptpcol_3_65538,A) ),
inference(resolve,[status(thm)],[c_1947,c_1521]) ).
cnf(c_7014,plain,
genls(c_tptpcol_4_65539,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_28722,c_1440]) ).
cnf(c_28723,plain,
( genls(c_tptpcol_12_72775,A)
| ~ genls(c_tptpcol_11_72774,A) ),
inference(resolve,[status(thm)],[c_1947,c_1496]) ).
cnf(c_7237,plain,
genls(c_tptpcol_12_72775,c_tptpcol_10_72710),
inference(resolve,[status(thm)],[c_28723,c_1527]) ).
cnf(c_28724,plain,
( genls(c_tptpcol_15_72793,A)
| ~ genls(c_tptpcol_13_72791,A) ),
inference(resolve,[status(thm)],[c_1947,c_3207]) ).
cnf(c_7682,plain,
genls(c_tptpcol_15_72793,c_tptpcol_12_72775),
inference(resolve,[status(thm)],[c_28724,c_1550]) ).
cnf(c_28725,plain,
( genls(c_tptpcol_15_22076,A)
| ~ genls(c_tptpcol_7_21508,A) ),
inference(resolve,[status(thm)],[c_1947,c_6911]) ).
cnf(c_9675,plain,
genls(c_tptpcol_15_22076,c_tptpcol_6_20484),
inference(resolve,[status(thm)],[c_28725,c_1529]) ).
cnf(c_28726,plain,
( disjointwith(c_tptpcol_2_65537,A)
| ~ genls(A,c_tptpcol_3_16386) ),
inference(resolve,[status(thm)],[c_1955,c_6960]) ).
cnf(c_9788,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_6_20484),
inference(resolve,[status(thm)],[c_28726,c_6171]) ).
cnf(c_28727,plain,
( genls(c_tptpcol_6_71683,A)
| ~ genls(c_tptpcol_4_65539,A) ),
inference(resolve,[status(thm)],[c_1947,c_6300]) ).
cnf(c_9997,plain,
genls(c_tptpcol_6_71683,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_28727,c_7014]) ).
cnf(c_28728,plain,
( genls(c_tptpcol_12_72775,A)
| ~ genls(c_tptpcol_10_72710,A) ),
inference(resolve,[status(thm)],[c_1947,c_7237]) ).
cnf(c_10216,plain,
genls(c_tptpcol_12_72775,c_tptpcol_6_71683),
inference(resolve,[status(thm)],[c_28728,c_6409]) ).
cnf(c_28729,plain,
( disjointwith(c_tptpcol_2_65537,A)
| ~ genls(A,c_tptpcol_6_20484) ),
inference(resolve,[status(thm)],[c_1955,c_9788]) ).
cnf(c_27358,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_15_22076),
inference(resolve,[status(thm)],[c_28729,c_9675]) ).
cnf(c_28730,plain,
( genls(c_tptpcol_15_72793,A)
| ~ genls(c_tptpcol_12_72775,A) ),
inference(resolve,[status(thm)],[c_1947,c_7682]) ).
cnf(c_28302,plain,
genls(c_tptpcol_15_72793,c_tptpcol_6_71683),
inference(resolve,[status(thm)],[c_28730,c_10216]) ).
cnf(c_28731,plain,
( ~ disjointwith(c_tptpcol_2_65537,c_tptpcol_15_22076)
| ~ genls(c_tptpcol_15_72793,c_tptpcol_6_71683) ),
inference(resolve,[status(thm)],[c_2583,c_9997]) ).
cnf(c_28732,plain,
~ disjointwith(c_tptpcol_2_65537,c_tptpcol_15_22076),
inference(resolve,[status(thm)],[c_28302,c_28731]) ).
cnf(c_28703,plain,
$false,
inference(resolve,[status(thm)],[c_27358,c_28732]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.39 % Computer : n013.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 00:05:36 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.40 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.40 % Process 3856031 was started by sandbox2 on n013,
% 0.11/0.40 % Sun Sep 27 00:05:36 2026
% 0.11/0.40 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.20/0.56
% 0.20/0.56 % From the command line: assign(max_seconds, 300).
% 0.20/0.56
% 0.20/0.56 % SInE: 733 to sos, 398 to usable, of 1131 axioms (tolerance 2.00, depth 0 fixpoint).
% 52.54/8.42
% 52.54/8.42 % given #500 (F,wt=5): 2750 -artsupplies(c_tptprunningshorts) | -disjointwith(c_runningshorts,c_artsupplies). [resolve(2648,a,1954,b)].
% 52.54/8.42
% 52.54/8.42 % given #1000 (W,wt=3): 3624 genlmt(c_tptpgeo_member8_mt,c_geographymt). [ur(1960,a,857,a,b,3399,a)].
% 52.54/8.42
% 52.54/8.42 % given #1500 (F,wt=3): 4822 -subsetof(c_tptptptpcol_16_8398,c_tptpcol_1_1). [ur(1696,a,4145,a,c,4354,a)].
% 52.54/8.42
% 52.54/8.42 % given #2000 (T,wt=3): 4819 few(c_tptpcol_1_1,c_tptpcol_1_65536). [ur(1450,a,4145,a)].
% 52.54/8.42
% 52.54/8.42 % given #2500 (F,wt=2): 5903 -partiallyintangibleindividual(c_tptpcol_3_65538). [resolve(5649,a,1279,b)].
% 52.54/8.42
% 52.54/8.42 % given #3000 (T,wt=3): 6012 genls(c_tptpcol_13_18664,c_tptpcol_8_18438). [ur(1947,a,5147,a,b,5138,a)].
% 52.54/8.42
% 52.54/8.42 % given #3500 (F,wt=2): 7276 -inanimateobject_nonnatural(c_artifact). [resolve(6245,a,1372,b)].
% 52.54/8.42
% 52.54/8.42 % given #4000 (T,wt=3): 6699 subsetof(c_tptpcol_9_93699,c_tptpcol_8_93698). [ur(1509,a,1474,a)].
% 52.54/8.42
% 52.54/8.42 % given #4500 (A,wt=405): 1683 collection(f_subcollectionofwithrelationtofn(A,B,C)) # tptp_name(ax1_708) # sine_depth(5). [clausify(284)].
% 52.54/8.42
% 52.54/8.42 % given #5000 (T,wt=3): 7456 genls(c_tptpcol_7_26628,c_tptpcol_4_24578). [ur(1947,a,6025,a,b,1324,a)].
% 52.54/8.42
% 52.54/8.42 % given #5500 (W,wt=2): 10155 -tptpcol_3_81921(c_tptpcol_11_93764). [resolve(9012,a,1285,b)].
% 52.54/8.42
% 52.54/8.42 % given #6000 (F,wt=2): 10989 -partiallyintangibleindividual(c_shavingrazor_manual). [resolve(9435,a,1279,b)].
% 52.54/8.42
% 52.54/8.42 % given #6500 (W,wt=2): 12563 -tptpcol_4_106497(c_tptpcol_3_98305). [resolve(10092,a,1297,b)].
% 52.54/8.42
% 52.54/8.42 % given #7000 (F,wt=2): 13791 -tptpcol_4_106497(c_tptpcol_8_114177). [resolve(10869,a,1297,b)].
% 52.54/8.42
% 52.54/8.42 % given #7500 (T,wt=2): 18175 mathematicalorcomputationalthing(c_tptpcol_8_93698). [ur(1360,a,17452,a)].
% 52.54/8.42
% 52.54/8.42 % given #8000 (F,wt=2): 16438 -tptpcol_5_110593(c_tptpcol_5_24579). [resolve(12887,a,1549,b)].
% 52.54/8.42
% 52.54/8.42 % given #8500 (T,wt=2): 22293 intangibleindividual(c_tptpgeo_member7_mt). [ur(1485,a,21211,a)].
% 52.54/8.42
% 52.54/8.42 % given #9000 (F,wt=2): 18859 -tptpcol_6_108546(c_tptpcol_9_22021). [resolve(14283,a,1532,b)].
% 52.54/8.42
% 52.54/8.42 % given #9500 (T,wt=3): 8439 most(c_tptpcol_14_40429,c_tptpcol_11_40388). [ur(1263,a,6578,a)].
% 52.54/8.42
% 52.54/8.42 % given #10000 (A,wt=9): 2344 -genls(c_tptpcol_15_72793,A) | -disjointwith(B,A) | -genls(c_tptpcol_14_22072,B). [resolve(2239,a,1956,c)].
% 52.54/8.42
% 52.54/8.42 % given #10500 (T,wt=3): 9689 genls(c_tptpcol_12_26919,c_tptpcol_8_26629). [ur(1947,a,6916,a,b,6333,a)].
% 52.54/8.42
% 52.54/8.42 % given #11000 (W,wt=2): 24442 -inanimateobject_nonnatural(c_tptpcol_4_114689). [resolve(18595,a,1372,b)].
% 52.54/8.42
% 52.54/8.42 % SZS status Theorem for theBenchmark
% 52.54/8.42
% 52.54/8.42 % Proof 1 at 5.30 (+ 2.20) seconds.
% 52.54/8.42 % Length of proof is 72.
% 52.54/8.42 % Level of proof is 8.
% 52.54/8.42 % Maximum clause weight is 1003.000.
% 52.54/8.42 % Given clauses 11408.
% 52.54/8.42
% 52.54/8.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------