%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR040+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 : n002.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:45 AM UTC 2026
% Result : Theorem 8.24s 1.69s
% Output : CNFRefutation 8.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 21
% Syntax : Number of formulae : 63 ( 23 unt; 0 def)
% Number of atoms : 103 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 67 ( 27 ~; 19 |; 1 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 38 ( 0 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1_50,axiom,
! [OBJ] :
( tptpcol_2_98304(OBJ)
=> tptpcol_1_65536(OBJ) ),
file('theBenchmark.p',ax1_50) ).
fof(ax1_69,axiom,
! [OBJ] :
( tptpcol_4_106497(OBJ)
=> tptpcol_3_98305(OBJ) ),
file('theBenchmark.p',ax1_69) ).
fof(ax1_96,axiom,
! [OBJ] :
( tptpcol_10_109061(OBJ)
=> tptpcol_9_109060(OBJ) ),
file('theBenchmark.p',ax1_96) ).
fof(ax1_114,axiom,
! [OBJ] :
( tptpcol_13_109173(OBJ)
=> tptpcol_12_109157(OBJ) ),
file('theBenchmark.p',ax1_114) ).
fof(ax1_117,axiom,
! [OBJ] :
( tptpcol_5_106498(OBJ)
=> tptpcol_4_106497(OBJ) ),
file('theBenchmark.p',ax1_117) ).
fof(ax1_124,axiom,
! [OBJ] :
( tptpcol_1_65536(OBJ)
=> tptpcol_0_0(OBJ) ),
file('theBenchmark.p',ax1_124) ).
fof(ax1_151,axiom,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('theBenchmark.p',ax1_151) ).
fof(ax1_185,axiom,
! [OBJ] :
( tptpcol_8_109059(OBJ)
=> tptpcol_7_108547(OBJ) ),
file('theBenchmark.p',ax1_185) ).
fof(ax1_205,axiom,
! [OBJ] :
( firstordercollection(OBJ)
=> fixedordercollection(OBJ) ),
file('theBenchmark.p',ax1_205) ).
fof(ax1_234,axiom,
! [OBJ] :
( tptpcol_3_98305(OBJ)
=> tptpcol_2_98304(OBJ) ),
file('theBenchmark.p',ax1_234) ).
fof(ax1_242,axiom,
! [OBJ] :
( tptpcol_9_109060(OBJ)
=> tptpcol_8_109059(OBJ) ),
file('theBenchmark.p',ax1_242) ).
fof(ax1_251,axiom,
! [OBJ] :
( tptpcol_14_109181(OBJ)
=> tptpcol_13_109173(OBJ) ),
file('theBenchmark.p',ax1_251) ).
fof(ax1_266,axiom,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('theBenchmark.p',ax1_266) ).
fof(ax1_289,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('theBenchmark.p',ax1_289) ).
fof(ax1_341,axiom,
! [OBJ] :
( tptpcol_7_108547(OBJ)
=> tptpcol_6_108546(OBJ) ),
file('theBenchmark.p',ax1_341) ).
fof(ax1_343,axiom,
! [OBJ] :
( tptpcol_11_109125(OBJ)
=> tptpcol_10_109061(OBJ) ),
file('theBenchmark.p',ax1_343) ).
fof(ax1_360,axiom,
! [OBJ] :
( tptpcol_12_109157(OBJ)
=> tptpcol_11_109125(OBJ) ),
file('theBenchmark.p',ax1_360) ).
fof(ax1_445,axiom,
! [OBJ] :
( tptpcol_0_0(OBJ)
=> individual(OBJ) ),
file('theBenchmark.p',ax1_445) ).
fof(ax1_459,axiom,
! [OBJ] :
( tptpcol_6_108546(OBJ)
=> tptpcol_5_106498(OBJ) ),
file('theBenchmark.p',ax1_459) ).
fof(query90,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('theBenchmark.p',query90) ).
fof(query90_neg,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(assume_negation,[status(cth)],[query90]) ).
cnf(c_1291,plain,
( tptpcol_1_65536(A)
| ~ tptpcol_2_98304(A) ),
inference(clausify,[status(thm)],[ax1_50]) ).
cnf(c_1295,plain,
( tptpcol_3_98305(A)
| ~ tptpcol_4_106497(A) ),
inference(clausify,[status(thm)],[ax1_69]) ).
cnf(c_1309,plain,
( tptpcol_9_109060(A)
| ~ tptpcol_10_109061(A) ),
inference(clausify,[status(thm)],[ax1_96]) ).
cnf(c_1319,plain,
( tptpcol_12_109157(A)
| ~ tptpcol_13_109173(A) ),
inference(clausify,[status(thm)],[ax1_114]) ).
cnf(c_1321,plain,
( tptpcol_4_106497(A)
| ~ tptpcol_5_106498(A) ),
inference(clausify,[status(thm)],[ax1_117]) ).
cnf(c_1325,plain,
( tptpcol_0_0(A)
| ~ tptpcol_1_65536(A) ),
inference(clausify,[status(thm)],[ax1_124]) ).
cnf(c_1340,plain,
( collection(A)
| ~ fixedordercollection(A) ),
inference(clausify,[status(thm)],[ax1_151]) ).
cnf(c_1363,plain,
( tptpcol_7_108547(A)
| ~ tptpcol_8_109059(A) ),
inference(clausify,[status(thm)],[ax1_185]) ).
cnf(c_1376,plain,
( fixedordercollection(A)
| ~ firstordercollection(A) ),
inference(clausify,[status(thm)],[ax1_205]) ).
cnf(c_1396,plain,
( tptpcol_2_98304(A)
| ~ tptpcol_3_98305(A) ),
inference(clausify,[status(thm)],[ax1_234]) ).
cnf(c_1402,plain,
( tptpcol_8_109059(A)
| ~ tptpcol_9_109060(A) ),
inference(clausify,[status(thm)],[ax1_242]) ).
cnf(c_1405,plain,
( tptpcol_13_109173(A)
| ~ tptpcol_14_109181(A) ),
inference(clausify,[status(thm)],[ax1_251]) ).
cnf(c_1415,plain,
( tptpcol_14_109181(A)
| ~ tptpcol_15_109185(A) ),
inference(clausify,[status(thm)],[ax1_266]) ).
cnf(c_1426,plain,
( ~ individual(A)
| ~ collection(A) ),
inference(clausify,[status(thm)],[ax1_289]) ).
cnf(c_1451,plain,
( tptpcol_6_108546(A)
| ~ tptpcol_7_108547(A) ),
inference(clausify,[status(thm)],[ax1_341]) ).
cnf(c_1453,plain,
( tptpcol_10_109061(A)
| ~ tptpcol_11_109125(A) ),
inference(clausify,[status(thm)],[ax1_343]) ).
cnf(c_1465,plain,
( tptpcol_11_109125(A)
| ~ tptpcol_12_109157(A) ),
inference(clausify,[status(thm)],[ax1_360]) ).
cnf(c_1523,plain,
( individual(A)
| ~ tptpcol_0_0(A) ),
inference(clausify,[status(thm)],[ax1_445]) ).
cnf(c_1529,plain,
( tptpcol_5_106498(A)
| ~ tptpcol_6_108546(A) ),
inference(clausify,[status(thm)],[ax1_459]) ).
fof(ax1_475,axiom,
firstordercollection(c_tptpcol_16_62187),
file('theBenchmark.p',ax1_475) ).
cnf(c_1536,plain,
firstordercollection(c_tptpcol_16_62187),
inference(clausify,[status(thm)],[ax1_475]) ).
cnf(c_1963,negated_conjecture,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(clausify,[status(thm)],[query90_neg]) ).
cnf(c_2023,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_1415,c_1963]) ).
cnf(c_2255,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_1405,c_2023]) ).
cnf(c_2329,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_1319,c_2255]) ).
cnf(c_2503,plain,
fixedordercollection(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_1376,c_1536]) ).
cnf(c_2511,plain,
collection(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_2503,c_1340]) ).
cnf(c_2833,plain,
~ individual(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_1426,c_2511]) ).
cnf(c_2989,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_1465,c_2329]) ).
cnf(c_2995,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_2989,c_1453]) ).
cnf(c_2996,plain,
tptpcol_9_109060(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_2995,c_1309]) ).
cnf(c_2997,plain,
tptpcol_8_109059(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_2996,c_1402]) ).
cnf(c_3145,plain,
tptpcol_7_108547(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_2997,c_1363]) ).
cnf(c_3147,plain,
tptpcol_6_108546(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_3145,c_1451]) ).
cnf(c_3709,plain,
~ tptpcol_0_0(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_1523,c_2833]) ).
cnf(c_3793,plain,
tptpcol_5_106498(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_1529,c_3147]) ).
cnf(c_4088,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_3793,c_1321]) ).
cnf(c_4361,plain,
~ tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_3709,c_1325]) ).
cnf(c_4690,plain,
tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_4088,c_1295]) ).
cnf(c_5158,plain,
tptpcol_2_98304(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_4690,c_1396]) ).
cnf(c_5968,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolve,[status(thm)],[c_5158,c_1291]) ).
cnf(c_5967,plain,
$false,
inference(resolve,[status(thm)],[c_4361,c_5968]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.39 % Computer : n002.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:12:06 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.39 % Process 2979233 was started by sandbox on n002,
% 0.11/0.39 % Sun Sep 27 00:12:06 2026
% 0.11/0.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.22/0.55
% 0.22/0.55 % From the command line: assign(max_seconds, 300).
% 0.22/0.55
% 0.22/0.55 % SInE: 735 to sos, 396 to usable, of 1131 axioms (tolerance 2.00, depth 0 fixpoint).
% 8.24/1.69
% 8.24/1.69 % given #500 (F,wt=10): 2324 -disjointwith(c_geolevel_4,c_geolevel_4) | -mtvisible(c_tptpgeo_member8_mt). [resolve(2191,b,2113,b)].
% 8.24/1.69
% 8.24/1.69 % given #1000 (W,wt=7): 2916 -individual(c_tptpcol_15_72793). [resolve(2758,a,1426,a)].
% 8.24/1.69
% 8.24/1.69 % given #1500 (F,wt=7): 3687 -tptpcol_0_0(c_tptpcol_13_22071). [resolve(1523,b,2892,a)].
% 8.24/1.69
% 8.24/1.69 % given #2000 (T,wt=7): 4763 binarypredicate(c_tptp_8_968). [resolve(1667,a,951,a)].
% 8.24/1.69
% 8.24/1.69 % SZS status Theorem for theBenchmark
% 8.24/1.69
% 8.24/1.69 % Proof 1 at 0.84 (+ 0.21) seconds.
% 8.24/1.69 % Length of proof is 60.
% 8.24/1.69 % Level of proof is 15.
% 8.24/1.69 % Maximum clause weight is 1209.000.
% 8.24/1.69 % Given clauses 2208.
% 8.24/1.69
% 8.24/1.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------