%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR039+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /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 : Sun Sep 27 07:06:44 AM UTC 2026
% Result : Theorem 38.41s 6.14s
% Output : CNFRefutation 38.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 32
% Syntax : Number of formulae : 119 ( 82 unt; 0 def)
% Number of atoms : 163 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 86 ( 42 ~; 35 |; 3 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 30 con; 0-2 aty)
% Number of variables : 49 ( 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(query89,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
file('theBenchmark.p',query89) ).
fof(query89_neg,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
inference(assume_negation,[status(cth)],[query89]) ).
fof(ax1_14,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
file('theBenchmark.p',ax1_14) ).
cnf(c_1265,plain,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(clausify,[status(thm)],[ax1_14]) ).
fof(ax1_23,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
file('theBenchmark.p',ax1_23) ).
cnf(c_1271,plain,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(clausify,[status(thm)],[ax1_23]) ).
fof(ax1_41,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('theBenchmark.p',ax1_41) ).
cnf(c_1285,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(clausify,[status(thm)],[ax1_41]) ).
fof(ax1_43,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
file('theBenchmark.p',ax1_43) ).
cnf(c_1287,plain,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(clausify,[status(thm)],[ax1_43]) ).
fof(ax1_72,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
file('theBenchmark.p',ax1_72) ).
cnf(c_1301,plain,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(clausify,[status(thm)],[ax1_72]) ).
fof(ax1_78,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
file('theBenchmark.p',ax1_78) ).
cnf(c_1305,plain,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(clausify,[status(thm)],[ax1_78]) ).
fof(ax1_109,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
file('theBenchmark.p',ax1_109) ).
cnf(c_1317,plain,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(clausify,[status(thm)],[ax1_109]) ).
fof(ax1_145,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('theBenchmark.p',ax1_145) ).
cnf(c_1338,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_1344,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[ax1_152]) ).
fof(ax1_175,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
file('theBenchmark.p',ax1_175) ).
cnf(c_1358,plain,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(clausify,[status(thm)],[ax1_175]) ).
fof(ax1_182,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
file('theBenchmark.p',ax1_182) ).
cnf(c_1362,plain,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(clausify,[status(thm)],[ax1_182]) ).
fof(ax1_191,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
file('theBenchmark.p',ax1_191) ).
cnf(c_1368,plain,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(clausify,[status(thm)],[ax1_191]) ).
fof(ax1_208,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
file('theBenchmark.p',ax1_208) ).
cnf(c_1379,plain,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(clausify,[status(thm)],[ax1_208]) ).
fof(ax1_255,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
file('theBenchmark.p',ax1_255) ).
cnf(c_1408,plain,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(clausify,[status(thm)],[ax1_255]) ).
fof(ax1_285,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('theBenchmark.p',ax1_285) ).
cnf(c_1424,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(clausify,[status(thm)],[ax1_285]) ).
fof(ax1_345,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
file('theBenchmark.p',ax1_345) ).
cnf(c_1456,plain,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(clausify,[status(thm)],[ax1_345]) ).
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_351,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
file('theBenchmark.p',ax1_351) ).
cnf(c_1461,plain,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(clausify,[status(thm)],[ax1_351]) ).
fof(ax1_353,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
file('theBenchmark.p',ax1_353) ).
cnf(c_1463,plain,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(clausify,[status(thm)],[ax1_353]) ).
fof(ax1_370,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
file('theBenchmark.p',ax1_370) ).
cnf(c_1474,plain,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(clausify,[status(thm)],[ax1_370]) ).
fof(ax1_372,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
file('theBenchmark.p',ax1_372) ).
cnf(c_1476,plain,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(clausify,[status(thm)],[ax1_372]) ).
fof(ax1_376,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('theBenchmark.p',ax1_376) ).
cnf(c_1480,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(clausify,[status(thm)],[ax1_376]) ).
fof(ax1_379,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
file('theBenchmark.p',ax1_379) ).
cnf(c_1482,plain,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(clausify,[status(thm)],[ax1_379]) ).
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_417,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('theBenchmark.p',ax1_417) ).
cnf(c_1510,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(clausify,[status(thm)],[ax1_417]) ).
fof(ax1_476,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('theBenchmark.p',ax1_476) ).
cnf(c_1539,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(clausify,[status(thm)],[ax1_476]) ).
fof(ax1_483,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
file('theBenchmark.p',ax1_483) ).
cnf(c_1544,plain,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(clausify,[status(thm)],[ax1_483]) ).
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_93775,c_tptpcol_13_18664),
inference(clausify,[status(thm)],[query89_neg]) ).
cnf(c_2037,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_15_93775),
inference(resolve,[status(thm)],[c_1954,c_1963]) ).
cnf(c_2045,plain,
( ~ genls(c_tptpcol_15_93775,A)
| ~ disjointwith(c_tptpcol_13_18664,A) ),
inference(resolve,[status(thm)],[c_1955,c_2037]) ).
cnf(c_2573,plain,
( ~ genls(A,B)
| ~ disjointwith(c_tptpcol_13_18664,B)
| ~ genls(c_tptpcol_15_93775,A) ),
inference(resolve,[status(thm)],[c_2045,c_1955]) ).
cnf(c_24906,plain,
( genls(c_tptpcol_13_18664,A)
| ~ genls(c_tptpcol_12_18663,A) ),
inference(resolve,[status(thm)],[c_1947,c_1379]) ).
cnf(c_3334,plain,
genls(c_tptpcol_13_18664,c_tptpcol_11_18631),
inference(resolve,[status(thm)],[c_24906,c_1317]) ).
cnf(c_24907,plain,
( genls(c_tptpcol_15_93775,A)
| ~ genls(c_tptpcol_14_93774,A) ),
inference(resolve,[status(thm)],[c_1947,c_1362]) ).
cnf(c_3336,plain,
genls(c_tptpcol_15_93775,c_tptpcol_13_93766),
inference(resolve,[status(thm)],[c_24907,c_1368]) ).
cnf(c_24908,plain,
( genls(c_tptpcol_13_93766,A)
| ~ genls(c_tptpcol_12_93765,A) ),
inference(resolve,[status(thm)],[c_1947,c_1305]) ).
cnf(c_3340,plain,
genls(c_tptpcol_13_93766,c_tptpcol_11_93764),
inference(resolve,[status(thm)],[c_24908,c_1301]) ).
cnf(c_24909,plain,
( genls(c_tptpcol_15_93775,A)
| ~ genls(c_tptpcol_13_93766,A) ),
inference(resolve,[status(thm)],[c_1947,c_3336]) ).
cnf(c_3371,plain,
genls(c_tptpcol_15_93775,c_tptpcol_11_93764),
inference(resolve,[status(thm)],[c_24909,c_3340]) ).
cnf(c_24910,plain,
( disjointwith(A,c_tptpcol_1_65536)
| ~ genls(A,c_tptpcol_1_1) ),
inference(resolve,[status(thm)],[c_1956,c_1344]) ).
cnf(c_3661,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(resolve,[status(thm)],[c_24910,c_1338]) ).
cnf(c_24911,plain,
( genls(c_tptpcol_13_18664,A)
| ~ genls(c_tptpcol_11_18631,A) ),
inference(resolve,[status(thm)],[c_1947,c_3334]) ).
cnf(c_3952,plain,
genls(c_tptpcol_13_18664,c_tptpcol_10_18567),
inference(resolve,[status(thm)],[c_24911,c_1358]) ).
cnf(c_24912,plain,
( genls(c_tptpcol_13_18664,A)
| ~ genls(c_tptpcol_10_18567,A) ),
inference(resolve,[status(thm)],[c_1947,c_3952]) ).
cnf(c_4183,plain,
genls(c_tptpcol_13_18664,c_tptpcol_9_18439),
inference(resolve,[status(thm)],[c_24912,c_1287]) ).
cnf(c_24913,plain,
( genls(c_tptpcol_13_18664,A)
| ~ genls(c_tptpcol_9_18439,A) ),
inference(resolve,[status(thm)],[c_1947,c_4183]) ).
cnf(c_4561,plain,
genls(c_tptpcol_13_18664,c_tptpcol_8_18438),
inference(resolve,[status(thm)],[c_24913,c_1408]) ).
cnf(c_24914,plain,
( genls(c_tptpcol_5_16388,A)
| ~ genls(c_tptpcol_4_16387,A) ),
inference(resolve,[status(thm)],[c_1947,c_1271]) ).
cnf(c_4743,plain,
genls(c_tptpcol_5_16388,c_tptpcol_3_16386),
inference(resolve,[status(thm)],[c_24914,c_1424]) ).
cnf(c_24915,plain,
( genls(c_tptpcol_8_93698,A)
| ~ genls(c_tptpcol_7_93186,A) ),
inference(resolve,[status(thm)],[c_1947,c_1456]) ).
cnf(c_5308,plain,
genls(c_tptpcol_8_93698,c_tptpcol_6_92162),
inference(resolve,[status(thm)],[c_24915,c_1265]) ).
cnf(c_24916,plain,
( disjointwith(c_tptpcol_2_2,A)
| ~ genls(A,c_tptpcol_1_65536) ),
inference(resolve,[status(thm)],[c_1955,c_3661]) ).
cnf(c_5335,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_24916,c_1459]) ).
cnf(c_24917,plain,
( genls(c_tptpcol_6_18436,A)
| ~ genls(c_tptpcol_5_16388,A) ),
inference(resolve,[status(thm)],[c_1947,c_1461]) ).
cnf(c_5375,plain,
genls(c_tptpcol_6_18436,c_tptpcol_3_16386),
inference(resolve,[status(thm)],[c_24917,c_4743]) ).
cnf(c_24918,plain,
( genls(c_tptpcol_13_18664,A)
| ~ genls(c_tptpcol_8_18438,A) ),
inference(resolve,[status(thm)],[c_1947,c_4561]) ).
cnf(c_5400,plain,
genls(c_tptpcol_13_18664,c_tptpcol_7_18437),
inference(resolve,[status(thm)],[c_24918,c_1463]) ).
cnf(c_24919,plain,
( genls(c_tptpcol_9_93699,A)
| ~ genls(c_tptpcol_8_93698,A) ),
inference(resolve,[status(thm)],[c_1947,c_1474]) ).
cnf(c_5765,plain,
genls(c_tptpcol_9_93699,c_tptpcol_6_92162),
inference(resolve,[status(thm)],[c_24919,c_5308]) ).
cnf(c_24920,plain,
( genls(c_tptpcol_15_93775,A)
| ~ genls(c_tptpcol_11_93764,A) ),
inference(resolve,[status(thm)],[c_1947,c_3371]) ).
cnf(c_5786,plain,
genls(c_tptpcol_15_93775,c_tptpcol_10_93700),
inference(resolve,[status(thm)],[c_24920,c_1476]) ).
cnf(c_24921,plain,
( genls(c_tptpcol_4_90113,A)
| ~ genls(c_tptpcol_3_81921,A) ),
inference(resolve,[status(thm)],[c_1947,c_1480]) ).
cnf(c_5809,plain,
genls(c_tptpcol_4_90113,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_24921,c_1285]) ).
cnf(c_24922,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_2_2) ),
inference(resolve,[status(thm)],[c_1956,c_5335]) ).
cnf(c_5962,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_24922,c_1486]) ).
cnf(c_24923,plain,
( genls(c_tptpcol_13_18664,A)
| ~ genls(c_tptpcol_7_18437,A) ),
inference(resolve,[status(thm)],[c_1947,c_5400]) ).
cnf(c_8777,plain,
genls(c_tptpcol_13_18664,c_tptpcol_6_18436),
inference(resolve,[status(thm)],[c_24923,c_1544]) ).
cnf(c_24924,plain,
( genls(c_tptpcol_9_93699,A)
| ~ genls(c_tptpcol_6_92162,A) ),
inference(resolve,[status(thm)],[c_1947,c_5765]) ).
cnf(c_9167,plain,
genls(c_tptpcol_9_93699,c_tptpcol_5_90114),
inference(resolve,[status(thm)],[c_24924,c_1510]) ).
cnf(c_24925,plain,
( genls(c_tptpcol_15_93775,A)
| ~ genls(c_tptpcol_10_93700,A) ),
inference(resolve,[status(thm)],[c_1947,c_5786]) ).
cnf(c_9173,plain,
genls(c_tptpcol_15_93775,c_tptpcol_9_93699),
inference(resolve,[status(thm)],[c_24925,c_1482]) ).
cnf(c_24926,plain,
( genls(c_tptpcol_5_90114,A)
| ~ genls(c_tptpcol_4_90113,A) ),
inference(resolve,[status(thm)],[c_1947,c_1539]) ).
cnf(c_9278,plain,
genls(c_tptpcol_5_90114,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_24926,c_5809]) ).
cnf(c_24927,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_3_16386) ),
inference(resolve,[status(thm)],[c_1956,c_5962]) ).
cnf(c_9580,plain,
disjointwith(c_tptpcol_6_18436,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_24927,c_5375]) ).
cnf(c_24928,plain,
( genls(c_tptpcol_15_93775,A)
| ~ genls(c_tptpcol_9_93699,A) ),
inference(resolve,[status(thm)],[c_1947,c_9173]) ).
cnf(c_17028,plain,
genls(c_tptpcol_15_93775,c_tptpcol_5_90114),
inference(resolve,[status(thm)],[c_24928,c_9167]) ).
cnf(c_24929,plain,
( disjointwith(A,c_tptpcol_2_65537)
| ~ genls(A,c_tptpcol_6_18436) ),
inference(resolve,[status(thm)],[c_1956,c_9580]) ).
cnf(c_19468,plain,
disjointwith(c_tptpcol_13_18664,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_24929,c_8777]) ).
cnf(c_24930,plain,
( ~ disjointwith(c_tptpcol_13_18664,c_tptpcol_2_65537)
| ~ genls(c_tptpcol_15_93775,c_tptpcol_5_90114) ),
inference(resolve,[status(thm)],[c_2573,c_9278]) ).
cnf(c_24931,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_17028,c_24930]) ).
cnf(c_24905,plain,
$false,
inference(resolve,[status(thm)],[c_19468,c_24931]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR039+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 27 00:09:14 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1453274 was started by sandbox on n009,
% 0.08/0.36 % Sun Sep 27 00:09:14 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.23/0.52
% 0.23/0.52 % From the command line: assign(max_seconds, 300).
% 0.23/0.52
% 0.23/0.52 % SInE: 732 to sos, 399 to usable, of 1131 axioms (tolerance 2.00, depth 0 fixpoint).
% 38.41/6.14
% 38.41/6.14 % given #500 (F,wt=11): 2484 -disjointwith(c_tptpcol_10_40324,c_tptpcol_10_40324) | -isa(A,c_tptpcol_13_40421). [resolve(2443,b,1238,b)].
% 38.41/6.14
% 38.41/6.14 % given #1000 (W,wt=7): 3732 aspatialinformationstore(c_tptp_member2831_mt). [ur(1347,a,2830,a)].
% 38.41/6.14
% 38.41/6.14 % given #1500 (F,wt=8): 4145 -subsetof(c_xskijump_thegame,c_individual). [ur(1696,a,3880,a,c,3925,a)].
% 38.41/6.14
% 38.41/6.14 % given #2000 (T,wt=8): 4936 few(c_tptpcol_5_106498,c_tptpcol_1_1). [ur(1449,a,4666,a)].
% 38.41/6.14
% 38.41/6.14 % given #2500 (F,wt=7): 5466 -intangibleindividual(c_tptpcol_15_40430). [resolve(5180,a,1446,b)].
% 38.41/6.14
% 38.41/6.14 % given #3000 (T,wt=7): 6939 collection(c_tptpcol_15_22076). [ur(1394,a,1523,a)].
% 38.41/6.14
% 38.41/6.14 % given #3500 (F,wt=7): 7156 -collection(c_wamt_evalinitial_p14). [resolve(6297,a,1428,b)].
% 38.41/6.14
% 38.41/6.14 % given #4000 (T,wt=8): 6025 genls(c_individual,c_location_underspecified). [ur(1947,a,1490,a,b,1281,a)].
% 38.41/6.14
% 38.41/6.14 % given #4500 (A,wt=1308): 1679 -objectfoundinlocation(A,A) # tptp_name(ax1_698) # sine_depth(14). [clausify(280)].
% 38.41/6.14
% 38.41/6.14 % given #5000 (T,wt=8): 6657 subsetof(c_tptpcol_11_118084,c_tptpcol_10_118020). [ur(1509,a,1331,a)].
% 38.41/6.14
% 38.41/6.14 % given #5500 (W,wt=7): 11052 -tptpcol_3_65538(c_tptpcol_15_50957). [resolve(10064,a,1440,b)].
% 38.41/6.14
% 38.41/6.14 % given #6000 (F,wt=7): 11540 -tptpcol_3_98305(c_mathematicalorcomputationalthing). [resolve(10322,a,1398,b)].
% 38.41/6.14
% 38.41/6.14 % given #6500 (W,wt=7): 15346 -tptpcol_4_90113(c_trajector_underspecified). [resolve(11097,a,1481,b)].
% 38.41/6.14
% 38.41/6.14 % given #7000 (F,wt=7): 16711 -tptpcol_4_65539(c_tptpcol_5_110593). [resolve(13305,a,1522,b)].
% 38.41/6.14
% 38.41/6.14 % given #7500 (T,wt=7): 21623 mathematicalthing(c_tptpcol_11_93764). [ur(1320,a,20912,a)].
% 38.41/6.14
% 38.41/6.14 % given #8000 (F,wt=7): 20199 -tptpcol_5_69635(c_tptpcol_14_109181). [resolve(16153,a,1390,b)].
% 38.41/6.14
% 38.41/6.14 % given #8500 (T,wt=8): 9783 subsetof(c_tptpcol_5_24579,c_tptpcol_2_2). [ur(1509,a,5977,a)].
% 38.41/6.14
% 38.41/6.14 % given #9000 (F,wt=7): 22212 -tptpcol_6_71683(c_tptpcol_13_93766). [resolve(18274,a,1505,b)].
% 38.41/6.14
% 38.41/6.14 % given #9500 (T,wt=8): 11009 most(c_tptpcol_16_7738,c_tptpcol_16_7738). [ur(1264,a,6520,a)].
% 38.41/6.14
% 38.41/6.14 % SZS status Theorem for theBenchmark
% 38.41/6.14
% 38.41/6.14 % Proof 1 at 3.55 (+ 1.61) seconds.
% 38.41/6.14 % Length of proof is 65.
% 38.41/6.14 % Level of proof is 9.
% 38.41/6.14 % Maximum clause weight is 908.000.
% 38.41/6.14 % Given clauses 9824.
% 38.41/6.14
% 38.41/6.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------