%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR039+1 : 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 : n008.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 1.30s 0.61s
% Output : CNFRefutation 1.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 30
% Syntax : Number of formulae : 119 ( 87 unt; 0 def)
% Number of atoms : 153 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 77 ( 43 ~; 29 |; 1 &)
% ( 0 <=>; 4 =>; 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 : 36 ( 0 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(just76,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('theBenchmark.p',just76) ).
fof(just77,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('theBenchmark.p',just77) ).
fof(query39,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',query39) ).
fof(query39_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)],[query39]) ).
fof(just7,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('theBenchmark.p',just7) ).
cnf(c_165,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(clausify,[status(thm)],[just7]) ).
fof(just9,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('theBenchmark.p',just9) ).
cnf(c_167,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(clausify,[status(thm)],[just9]) ).
fof(just11,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('theBenchmark.p',just11) ).
cnf(c_169,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(clausify,[status(thm)],[just11]) ).
fof(just13,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
file('theBenchmark.p',just13) ).
cnf(c_171,plain,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(clausify,[status(thm)],[just13]) ).
fof(just15,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
file('theBenchmark.p',just15) ).
cnf(c_173,plain,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(clausify,[status(thm)],[just15]) ).
fof(just17,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
file('theBenchmark.p',just17) ).
cnf(c_175,plain,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(clausify,[status(thm)],[just17]) ).
fof(just19,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
file('theBenchmark.p',just19) ).
cnf(c_177,plain,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(clausify,[status(thm)],[just19]) ).
fof(just21,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
file('theBenchmark.p',just21) ).
cnf(c_179,plain,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(clausify,[status(thm)],[just21]) ).
fof(just23,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
file('theBenchmark.p',just23) ).
cnf(c_181,plain,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(clausify,[status(thm)],[just23]) ).
fof(just25,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
file('theBenchmark.p',just25) ).
cnf(c_183,plain,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(clausify,[status(thm)],[just25]) ).
fof(just27,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
file('theBenchmark.p',just27) ).
cnf(c_185,plain,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(clausify,[status(thm)],[just27]) ).
fof(just29,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
file('theBenchmark.p',just29) ).
cnf(c_187,plain,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(clausify,[status(thm)],[just29]) ).
fof(just31,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('theBenchmark.p',just31) ).
cnf(c_189,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[just31]) ).
fof(just33,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('theBenchmark.p',just33) ).
cnf(c_191,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(clausify,[status(thm)],[just33]) ).
fof(just35,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('theBenchmark.p',just35) ).
cnf(c_193,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(clausify,[status(thm)],[just35]) ).
fof(just37,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('theBenchmark.p',just37) ).
cnf(c_195,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(clausify,[status(thm)],[just37]) ).
fof(just39,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('theBenchmark.p',just39) ).
cnf(c_197,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(clausify,[status(thm)],[just39]) ).
fof(just41,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
file('theBenchmark.p',just41) ).
cnf(c_199,plain,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(clausify,[status(thm)],[just41]) ).
fof(just43,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
file('theBenchmark.p',just43) ).
cnf(c_201,plain,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(clausify,[status(thm)],[just43]) ).
fof(just45,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
file('theBenchmark.p',just45) ).
cnf(c_203,plain,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(clausify,[status(thm)],[just45]) ).
fof(just47,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
file('theBenchmark.p',just47) ).
cnf(c_205,plain,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(clausify,[status(thm)],[just47]) ).
fof(just49,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
file('theBenchmark.p',just49) ).
cnf(c_207,plain,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(clausify,[status(thm)],[just49]) ).
fof(just51,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
file('theBenchmark.p',just51) ).
cnf(c_209,plain,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(clausify,[status(thm)],[just51]) ).
fof(just53,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
file('theBenchmark.p',just53) ).
cnf(c_211,plain,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(clausify,[status(thm)],[just53]) ).
fof(just55,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
file('theBenchmark.p',just55) ).
cnf(c_213,plain,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(clausify,[status(thm)],[just55]) ).
fof(just57,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
file('theBenchmark.p',just57) ).
cnf(c_215,plain,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(clausify,[status(thm)],[just57]) ).
fof(just59,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('theBenchmark.p',just59) ).
cnf(c_217,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(clausify,[status(thm)],[just59]) ).
cnf(c_222,plain,
( disjointwith(B,A)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[just76]) ).
cnf(c_223,plain,
( disjointwith(A,C)
| ~ genls(C,B)
| ~ disjointwith(A,B) ),
inference(clausify,[status(thm)],[just77]) ).
cnf(c_299,negated_conjecture,
~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(clausify,[status(thm)],[query39_neg]) ).
cnf(c_323,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_15_93775),
inference(resolve,[status(thm)],[c_222,c_299]) ).
cnf(c_324,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(resolve,[status(thm)],[c_222,c_217]) ).
cnf(c_1465,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_1_1) ),
inference(resolve,[status(thm)],[c_223,c_324]) ).
cnf(c_342,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference(resolve,[status(thm)],[c_1465,c_165]) ).
cnf(c_1466,plain,
( disjointwith(A,c_tptpcol_15_93775)
| ~ disjointwith(A,c_tptpcol_14_93774) ),
inference(resolve,[status(thm)],[c_223,c_215]) ).
cnf(c_343,plain,
~ disjointwith(c_tptpcol_13_18664,c_tptpcol_14_93774),
inference(resolve,[status(thm)],[c_1466,c_323]) ).
cnf(c_1467,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_2_2) ),
inference(resolve,[status(thm)],[c_223,c_342]) ).
cnf(c_346,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386),
inference(resolve,[status(thm)],[c_1467,c_167]) ).
cnf(c_1468,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_3_16386) ),
inference(resolve,[status(thm)],[c_223,c_346]) ).
cnf(c_350,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_4_16387),
inference(resolve,[status(thm)],[c_1468,c_169]) ).
cnf(c_354,plain,
~ disjointwith(c_tptpcol_14_93774,c_tptpcol_13_18664),
inference(resolve,[status(thm)],[c_343,c_222]) ).
cnf(c_1469,plain,
( disjointwith(A,c_tptpcol_13_18664)
| ~ disjointwith(A,c_tptpcol_12_18663) ),
inference(resolve,[status(thm)],[c_223,c_187]) ).
cnf(c_358,plain,
~ disjointwith(c_tptpcol_14_93774,c_tptpcol_12_18663),
inference(resolve,[status(thm)],[c_1469,c_354]) ).
cnf(c_361,plain,
( ~ genls(c_tptpcol_12_18663,A)
| ~ disjointwith(c_tptpcol_14_93774,A) ),
inference(resolve,[status(thm)],[c_358,c_223]) ).
cnf(c_1470,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_4_16387) ),
inference(resolve,[status(thm)],[c_223,c_350]) ).
cnf(c_363,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_5_16388),
inference(resolve,[status(thm)],[c_1470,c_171]) ).
cnf(c_1471,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_5_16388) ),
inference(resolve,[status(thm)],[c_223,c_363]) ).
cnf(c_368,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_6_18436),
inference(resolve,[status(thm)],[c_1471,c_173]) ).
cnf(c_1472,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_6_18436) ),
inference(resolve,[status(thm)],[c_223,c_368]) ).
cnf(c_378,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_7_18437),
inference(resolve,[status(thm)],[c_1472,c_175]) ).
cnf(c_1473,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_7_18437) ),
inference(resolve,[status(thm)],[c_223,c_378]) ).
cnf(c_382,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_8_18438),
inference(resolve,[status(thm)],[c_1473,c_177]) ).
cnf(c_1474,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_8_18438) ),
inference(resolve,[status(thm)],[c_223,c_382]) ).
cnf(c_392,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_9_18439),
inference(resolve,[status(thm)],[c_1474,c_179]) ).
cnf(c_1475,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_9_18439) ),
inference(resolve,[status(thm)],[c_223,c_392]) ).
cnf(c_398,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_10_18567),
inference(resolve,[status(thm)],[c_1475,c_181]) ).
cnf(c_1476,plain,
( disjointwith(c_tptpcol_1_65536,A)
| ~ genls(A,c_tptpcol_10_18567) ),
inference(resolve,[status(thm)],[c_223,c_398]) ).
cnf(c_406,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_11_18631),
inference(resolve,[status(thm)],[c_1476,c_183]) ).
cnf(c_410,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_1_65536),
inference(resolve,[status(thm)],[c_222,c_406]) ).
cnf(c_412,plain,
~ disjointwith(c_tptpcol_14_93774,c_tptpcol_11_18631),
inference(resolve,[status(thm)],[c_185,c_361]) ).
cnf(c_416,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_14_93774),
inference(resolve,[status(thm)],[c_412,c_222]) ).
cnf(c_1477,plain,
( disjointwith(c_tptpcol_11_18631,A)
| ~ genls(A,c_tptpcol_1_65536) ),
inference(resolve,[status(thm)],[c_223,c_410]) ).
cnf(c_432,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_2_65537),
inference(resolve,[status(thm)],[c_1477,c_189]) ).
cnf(c_1478,plain,
( disjointwith(c_tptpcol_11_18631,A)
| ~ genls(A,c_tptpcol_2_65537) ),
inference(resolve,[status(thm)],[c_223,c_432]) ).
cnf(c_459,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_3_81921),
inference(resolve,[status(thm)],[c_1478,c_191]) ).
cnf(c_1479,plain,
( disjointwith(c_tptpcol_11_18631,A)
| ~ genls(A,c_tptpcol_3_81921) ),
inference(resolve,[status(thm)],[c_223,c_459]) ).
cnf(c_515,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_4_90113),
inference(resolve,[status(thm)],[c_1479,c_193]) ).
cnf(c_1480,plain,
( disjointwith(c_tptpcol_11_18631,A)
| ~ genls(A,c_tptpcol_4_90113) ),
inference(resolve,[status(thm)],[c_223,c_515]) ).
cnf(c_585,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_5_90114),
inference(resolve,[status(thm)],[c_1480,c_195]) ).
cnf(c_1481,plain,
( disjointwith(A,c_tptpcol_14_93774)
| ~ disjointwith(A,c_tptpcol_13_93766) ),
inference(resolve,[status(thm)],[c_223,c_213]) ).
cnf(c_602,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_13_93766),
inference(resolve,[status(thm)],[c_1481,c_416]) ).
cnf(c_1482,plain,
( disjointwith(A,c_tptpcol_13_93766)
| ~ disjointwith(A,c_tptpcol_12_93765) ),
inference(resolve,[status(thm)],[c_223,c_211]) ).
cnf(c_766,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_12_93765),
inference(resolve,[status(thm)],[c_1482,c_602]) ).
cnf(c_1483,plain,
( disjointwith(c_tptpcol_11_18631,A)
| ~ genls(A,c_tptpcol_5_90114) ),
inference(resolve,[status(thm)],[c_223,c_585]) ).
cnf(c_774,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_6_92162),
inference(resolve,[status(thm)],[c_1483,c_197]) ).
cnf(c_1484,plain,
( disjointwith(A,c_tptpcol_12_93765)
| ~ disjointwith(A,c_tptpcol_11_93764) ),
inference(resolve,[status(thm)],[c_223,c_209]) ).
cnf(c_959,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_11_93764),
inference(resolve,[status(thm)],[c_1484,c_766]) ).
cnf(c_1485,plain,
( disjointwith(c_tptpcol_11_18631,A)
| ~ genls(A,c_tptpcol_6_92162) ),
inference(resolve,[status(thm)],[c_223,c_774]) ).
cnf(c_967,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_7_93186),
inference(resolve,[status(thm)],[c_1485,c_199]) ).
cnf(c_1486,plain,
( disjointwith(A,c_tptpcol_11_93764)
| ~ disjointwith(A,c_tptpcol_10_93700) ),
inference(resolve,[status(thm)],[c_223,c_207]) ).
cnf(c_1166,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_10_93700),
inference(resolve,[status(thm)],[c_1486,c_959]) ).
cnf(c_1487,plain,
( disjointwith(c_tptpcol_11_18631,A)
| ~ genls(A,c_tptpcol_7_93186) ),
inference(resolve,[status(thm)],[c_223,c_967]) ).
cnf(c_1175,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_8_93698),
inference(resolve,[status(thm)],[c_1487,c_201]) ).
cnf(c_1488,plain,
( disjointwith(A,c_tptpcol_10_93700)
| ~ disjointwith(A,c_tptpcol_9_93699) ),
inference(resolve,[status(thm)],[c_223,c_205]) ).
cnf(c_1452,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_9_93699),
inference(resolve,[status(thm)],[c_1488,c_1166]) ).
cnf(c_1489,plain,
( disjointwith(c_tptpcol_11_18631,A)
| ~ genls(A,c_tptpcol_8_93698) ),
inference(resolve,[status(thm)],[c_223,c_1175]) ).
cnf(c_1490,plain,
disjointwith(c_tptpcol_11_18631,c_tptpcol_9_93699),
inference(resolve,[status(thm)],[c_1489,c_203]) ).
cnf(c_1464,plain,
$false,
inference(resolve,[status(thm)],[c_1452,c_1490]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR039+1 : 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.37 % Computer : n008.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 00:09:09 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.37 % Process 665474 was started by sandbox2 on n008,
% 0.11/0.37 % Sun Sep 27 00:09:09 2026
% 0.11/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.40
% 0.11/0.40 % From the command line: assign(max_seconds, 300).
% 0.11/0.40
% 0.11/0.40 % SInE: 147 to sos, 23 to usable, of 170 axioms (tolerance 2.00, depth 0 fixpoint).
% 1.30/0.61
% 1.30/0.61 % given #500 (F,wt=8): 1119 -genls(c_tptpcol_11_93764,c_tptpcol_6_92162). [ur(223,a,900,a,c,917,a)].
% 1.30/0.61
% 1.30/0.61 % SZS status Theorem for theBenchmark
% 1.30/0.61
% 1.30/0.61 % Proof 1 at 0.15 (+ 0.05) seconds.
% 1.30/0.61 % Length of proof is 65.
% 1.30/0.61 % Level of proof is 21.
% 1.30/0.61 % Maximum clause weight is 708.000.
% 1.30/0.61 % Given clauses 533.
% 1.30/0.61
% 1.30/0.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------