%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : CSR040+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 11:18:41 AM UTC 2025
% Result : Theorem 8.26s 1.47s
% Output : CNFRefutation 8.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 31
% Syntax : Number of formulae : 106 ( 57 unt; 0 def)
% Number of atoms : 184 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 142 ( 64 ~; 58 |; 7 &)
% ( 0 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 22 con; 0-2 aty)
% Number of variables : 48 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query40,plain,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query40) ).
fof(query40_negated,plain,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(negate_conjecture,[status(cth)],[query40]) ).
cnf(146,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf,[status(esa)],[query40_negated]) ).
cnf(l0,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(instantiation,[status(thm)],[146]) ).
fof(just47,plain,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just47) ).
cnf(46,plain,
( ~ tptpcol_15_109185(X0)
| tptpcol_14_109181(X0) ),
inference(cnf,[status(esa)],[just47]) ).
cnf(l1,plain,
( ~ tptpcol_15_109185(c_tptpcol_16_62187)
| tptpcol_14_109181(c_tptpcol_16_62187) ),
inference(instantiation,[status(thm)],[46]) ).
fof(just64,plain,
! [X] :
( tptpcol_14_109181(X)
=> isa(X,c_tptpcol_14_109181) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just64) ).
cnf(63,plain,
( ~ tptpcol_14_109181(X0)
| isa(X0,c_tptpcol_14_109181) ),
inference(cnf,[status(esa)],[just64]) ).
cnf(l47,plain,
( ~ tptpcol_14_109181(c_tptpcol_16_62187)
| isa(c_tptpcol_16_62187,c_tptpcol_14_109181) ),
inference(instantiation,[status(thm)],[63]) ).
fof(just48,plain,
! [OBJ,COL1,COL2] :
~ ( isa(OBJ,COL1)
& isa(OBJ,COL2)
& disjointwith(COL1,COL2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just48) ).
cnf(47,plain,
( ~ disjointwith(X0,X1)
| ~ isa(X2,X0)
| ~ isa(X2,X1) ),
inference(cnf,[status(esa)],[just48]) ).
cnf(l48,plain,
( ~ disjointwith(c_collection,c_tptpcol_14_109181)
| ~ isa(c_tptpcol_16_62187,c_collection)
| ~ isa(c_tptpcol_16_62187,c_tptpcol_14_109181) ),
inference(instantiation,[status(thm)],[47]) ).
fof(just102,plain,
! [ARG1,OLD,NEW] :
( ( disjointwith(ARG1,OLD)
& genls(NEW,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just102) ).
cnf(101,plain,
( ~ genls(X0,X1)
| ~ disjointwith(X2,X1)
| disjointwith(X2,X0) ),
inference(cnf,[status(esa)],[just102]) ).
cnf(l112,plain,
( ~ genls(c_tptpcol_14_109181,c_individual)
| ~ disjointwith(c_collection,c_individual)
| disjointwith(c_collection,c_tptpcol_14_109181) ),
inference(instantiation,[status(thm)],[101]) ).
fof(just10,plain,
disjointwith(c_collection,c_individual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just10) ).
cnf(9,plain,
disjointwith(c_collection,c_individual),
inference(cnf,[status(esa)],[just10]) ).
cnf(l113,plain,
disjointwith(c_collection,c_individual),
inference(instantiation,[status(thm)],[9]) ).
fof(just121,plain,
! [X,Y,Z] :
( ( genls(X,Y)
& genls(Y,Z) )
=> genls(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just121) ).
cnf(120,plain,
( ~ genls(X0,X1)
| ~ genls(X1,X2)
| genls(X0,X2) ),
inference(cnf,[status(esa)],[just121]) ).
cnf(l114,plain,
( ~ genls(c_tptpcol_14_109181,c_tptpcol_6_108546)
| ~ genls(c_tptpcol_6_108546,c_individual)
| genls(c_tptpcol_14_109181,c_individual) ),
inference(instantiation,[status(thm)],[120]) ).
fof(just125,plain,
! [ARG1,OLD,NEW] :
( ( genls(ARG1,OLD)
& genls(OLD,NEW) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just125) ).
cnf(124,plain,
( ~ genls(X0,X1)
| ~ genls(X1,X2)
| genls(X0,X2) ),
inference(cnf,[status(esa)],[just125]) ).
cnf(l115,plain,
( ~ genls(c_tptpcol_6_108546,c_tptpcol_2_98304)
| ~ genls(c_tptpcol_2_98304,c_individual)
| genls(c_tptpcol_6_108546,c_individual) ),
inference(instantiation,[status(thm)],[124]) ).
fof(just124,plain,
! [OLD,ARG2,NEW] :
( ( genls(OLD,ARG2)
& genls(NEW,OLD) )
=> genls(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just124) ).
cnf(123,plain,
( ~ genls(X0,X1)
| ~ genls(X2,X0)
| genls(X2,X1) ),
inference(cnf,[status(esa)],[just124]) ).
cnf(l116,plain,
( ~ genls(c_tptpcol_0_0,c_individual)
| ~ genls(c_tptpcol_2_98304,c_tptpcol_0_0)
| genls(c_tptpcol_2_98304,c_individual) ),
inference(instantiation,[status(thm)],[123]) ).
cnf(l117,plain,
( ~ genls(c_tptpcol_10_109061,c_tptpcol_6_108546)
| ~ genls(c_tptpcol_14_109181,c_tptpcol_10_109061)
| genls(c_tptpcol_14_109181,c_tptpcol_6_108546) ),
inference(instantiation,[status(thm)],[123]) ).
fof(just15,plain,
genls(c_tptpcol_0_0,c_individual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just15) ).
cnf(14,plain,
genls(c_tptpcol_0_0,c_individual),
inference(cnf,[status(esa)],[just15]) ).
cnf(l118,plain,
genls(c_tptpcol_0_0,c_individual),
inference(instantiation,[status(thm)],[14]) ).
fof(just98,plain,
! [X] :
( collection(X)
=> isa(X,c_collection) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just98) ).
cnf(97,plain,
( ~ collection(X0)
| isa(X0,c_collection) ),
inference(cnf,[status(esa)],[just98]) ).
cnf(l49,plain,
( ~ collection(c_tptpcol_16_62187)
| isa(c_tptpcol_16_62187,c_collection) ),
inference(instantiation,[status(thm)],[97]) ).
cnf(l128,plain,
( ~ genls(c_tptpcol_1_65536,c_tptpcol_0_0)
| ~ genls(c_tptpcol_2_98304,c_tptpcol_1_65536)
| genls(c_tptpcol_2_98304,c_tptpcol_0_0) ),
inference(instantiation,[status(thm)],[123]) ).
cnf(l120,plain,
( ~ genls(c_tptpcol_6_108546,c_tptpcol_4_106497)
| ~ genls(c_tptpcol_4_106497,c_tptpcol_2_98304)
| genls(c_tptpcol_6_108546,c_tptpcol_2_98304) ),
inference(instantiation,[status(thm)],[120]) ).
fof(just18,plain,
genls(c_tptpcol_1_65536,c_tptpcol_0_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just18) ).
cnf(17,plain,
genls(c_tptpcol_1_65536,c_tptpcol_0_0),
inference(cnf,[status(esa)],[just18]) ).
cnf(l135,plain,
genls(c_tptpcol_1_65536,c_tptpcol_0_0),
inference(instantiation,[status(thm)],[17]) ).
fof(just20,plain,
genls(c_tptpcol_2_98304,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just20) ).
cnf(19,plain,
genls(c_tptpcol_2_98304,c_tptpcol_1_65536),
inference(cnf,[status(esa)],[just20]) ).
cnf(l136,plain,
genls(c_tptpcol_2_98304,c_tptpcol_1_65536),
inference(instantiation,[status(thm)],[19]) ).
cnf(l119,plain,
( ~ genls(c_tptpcol_10_109061,c_tptpcol_8_109059)
| ~ genls(c_tptpcol_8_109059,c_tptpcol_6_108546)
| genls(c_tptpcol_10_109061,c_tptpcol_6_108546) ),
inference(instantiation,[status(thm)],[120]) ).
cnf(l121,plain,
( ~ genls(c_tptpcol_3_98305,c_tptpcol_2_98304)
| ~ genls(c_tptpcol_4_106497,c_tptpcol_3_98305)
| genls(c_tptpcol_4_106497,c_tptpcol_2_98304) ),
inference(instantiation,[status(thm)],[123]) ).
fof(just22,plain,
genls(c_tptpcol_3_98305,c_tptpcol_2_98304),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just22) ).
cnf(21,plain,
genls(c_tptpcol_3_98305,c_tptpcol_2_98304),
inference(cnf,[status(esa)],[just22]) ).
cnf(l130,plain,
genls(c_tptpcol_3_98305,c_tptpcol_2_98304),
inference(instantiation,[status(thm)],[21]) ).
fof(just14,plain,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just14) ).
cnf(13,plain,
( ~ fixedordercollection(X0)
| collection(X0) ),
inference(cnf,[status(esa)],[just14]) ).
cnf(l50,plain,
( ~ fixedordercollection(c_tptpcol_16_62187)
| collection(c_tptpcol_16_62187) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l122,plain,
( ~ genls(c_tptpcol_12_109157,c_tptpcol_10_109061)
| ~ genls(c_tptpcol_14_109181,c_tptpcol_12_109157)
| genls(c_tptpcol_14_109181,c_tptpcol_10_109061) ),
inference(instantiation,[status(thm)],[123]) ).
fof(just24,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just24) ).
cnf(23,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf,[status(esa)],[just24]) ).
cnf(l129,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(instantiation,[status(thm)],[23]) ).
fof(just113,plain,
! [X] :
( isa(X,c_fixedordercollection)
=> fixedordercollection(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just113) ).
cnf(112,plain,
( ~ isa(X0,c_fixedordercollection)
| fixedordercollection(X0) ),
inference(cnf,[status(esa)],[just113]) ).
cnf(l51,plain,
( ~ isa(c_tptpcol_16_62187,c_fixedordercollection)
| fixedordercollection(c_tptpcol_16_62187) ),
inference(instantiation,[status(thm)],[112]) ).
cnf(l124,plain,
( ~ genls(c_tptpcol_6_108546,c_tptpcol_5_106498)
| ~ genls(c_tptpcol_5_106498,c_tptpcol_4_106497)
| genls(c_tptpcol_6_108546,c_tptpcol_4_106497) ),
inference(instantiation,[status(thm)],[124]) ).
cnf(l138,plain,
( ~ genls(c_tptpcol_7_108547,c_tptpcol_6_108546)
| ~ genls(c_tptpcol_8_109059,c_tptpcol_7_108547)
| genls(c_tptpcol_8_109059,c_tptpcol_6_108546) ),
inference(instantiation,[status(thm)],[123]) ).
fof(just28,plain,
genls(c_tptpcol_6_108546,c_tptpcol_5_106498),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just28) ).
cnf(27,plain,
genls(c_tptpcol_6_108546,c_tptpcol_5_106498),
inference(cnf,[status(esa)],[just28]) ).
cnf(l131,plain,
genls(c_tptpcol_6_108546,c_tptpcol_5_106498),
inference(instantiation,[status(thm)],[27]) ).
fof(just30,plain,
genls(c_tptpcol_7_108547,c_tptpcol_6_108546),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just30) ).
cnf(29,plain,
genls(c_tptpcol_7_108547,c_tptpcol_6_108546),
inference(cnf,[status(esa)],[just30]) ).
cnf(l140,plain,
genls(c_tptpcol_7_108547,c_tptpcol_6_108546),
inference(instantiation,[status(thm)],[29]) ).
fof(just111,plain,
! [ARG1,OLD,NEW] :
( ( isa(ARG1,OLD)
& genls(OLD,NEW) )
=> isa(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just111) ).
cnf(110,plain,
( ~ genls(X0,X1)
| ~ isa(X2,X0)
| isa(X2,X1) ),
inference(cnf,[status(esa)],[just111]) ).
cnf(l62,plain,
( ~ genls(c_firstordercollection,c_fixedordercollection)
| ~ isa(c_tptpcol_16_62187,c_firstordercollection)
| isa(c_tptpcol_16_62187,c_fixedordercollection) ),
inference(instantiation,[status(thm)],[110]) ).
fof(just32,plain,
genls(c_tptpcol_8_109059,c_tptpcol_7_108547),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just32) ).
cnf(31,plain,
genls(c_tptpcol_8_109059,c_tptpcol_7_108547),
inference(cnf,[status(esa)],[just32]) ).
cnf(l139,plain,
genls(c_tptpcol_8_109059,c_tptpcol_7_108547),
inference(instantiation,[status(thm)],[31]) ).
fof(just26,plain,
genls(c_tptpcol_5_106498,c_tptpcol_4_106497),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just26) ).
cnf(25,plain,
genls(c_tptpcol_5_106498,c_tptpcol_4_106497),
inference(cnf,[status(esa)],[just26]) ).
cnf(l133,plain,
genls(c_tptpcol_5_106498,c_tptpcol_4_106497),
inference(instantiation,[status(thm)],[25]) ).
fof(just3,plain,
genls(c_firstordercollection,c_fixedordercollection),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just3) ).
cnf(2,plain,
genls(c_firstordercollection,c_fixedordercollection),
inference(cnf,[status(esa)],[just3]) ).
cnf(l66,plain,
genls(c_firstordercollection,c_fixedordercollection),
inference(instantiation,[status(thm)],[2]) ).
fof(just116,plain,
! [X] :
( firstordercollection(X)
=> isa(X,c_firstordercollection) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just116) ).
cnf(115,plain,
( ~ firstordercollection(X0)
| isa(X0,c_firstordercollection) ),
inference(cnf,[status(esa)],[just116]) ).
cnf(l63,plain,
( ~ firstordercollection(c_tptpcol_16_62187)
| isa(c_tptpcol_16_62187,c_firstordercollection) ),
inference(instantiation,[status(thm)],[115]) ).
cnf(l137,plain,
( ~ genls(c_tptpcol_10_109061,c_tptpcol_9_109060)
| ~ genls(c_tptpcol_9_109060,c_tptpcol_8_109059)
| genls(c_tptpcol_10_109061,c_tptpcol_8_109059) ),
inference(instantiation,[status(thm)],[120]) ).
cnf(l126,plain,
( ~ genls(c_tptpcol_14_109181,c_tptpcol_13_109173)
| ~ genls(c_tptpcol_13_109173,c_tptpcol_12_109157)
| genls(c_tptpcol_14_109181,c_tptpcol_12_109157) ),
inference(instantiation,[status(thm)],[124]) ).
fof(just34,plain,
genls(c_tptpcol_9_109060,c_tptpcol_8_109059),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just34) ).
cnf(33,plain,
genls(c_tptpcol_9_109060,c_tptpcol_8_109059),
inference(cnf,[status(esa)],[just34]) ).
cnf(l141,plain,
genls(c_tptpcol_9_109060,c_tptpcol_8_109059),
inference(instantiation,[status(thm)],[33]) ).
fof(just44,plain,
genls(c_tptpcol_14_109181,c_tptpcol_13_109173),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just44) ).
cnf(43,plain,
genls(c_tptpcol_14_109181,c_tptpcol_13_109173),
inference(cnf,[status(esa)],[just44]) ).
cnf(l127,plain,
genls(c_tptpcol_14_109181,c_tptpcol_13_109173),
inference(instantiation,[status(thm)],[43]) ).
fof(just17,plain,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just17) ).
cnf(16,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf,[status(esa)],[just17]) ).
cnf(l76,plain,
firstordercollection(c_tptpcol_16_62187),
inference(instantiation,[status(thm)],[16]) ).
fof(just42,plain,
genls(c_tptpcol_13_109173,c_tptpcol_12_109157),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just42) ).
cnf(41,plain,
genls(c_tptpcol_13_109173,c_tptpcol_12_109157),
inference(cnf,[status(esa)],[just42]) ).
cnf(l132,plain,
genls(c_tptpcol_13_109173,c_tptpcol_12_109157),
inference(instantiation,[status(thm)],[41]) ).
fof(just36,plain,
genls(c_tptpcol_10_109061,c_tptpcol_9_109060),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just36) ).
cnf(35,plain,
genls(c_tptpcol_10_109061,c_tptpcol_9_109060),
inference(cnf,[status(esa)],[just36]) ).
cnf(l142,plain,
genls(c_tptpcol_10_109061,c_tptpcol_9_109060),
inference(instantiation,[status(thm)],[35]) ).
cnf(l123,plain,
( ~ genls(c_tptpcol_12_109157,c_tptpcol_11_109125)
| ~ genls(c_tptpcol_11_109125,c_tptpcol_10_109061)
| genls(c_tptpcol_12_109157,c_tptpcol_10_109061) ),
inference(instantiation,[status(thm)],[120]) ).
fof(just40,plain,
genls(c_tptpcol_12_109157,c_tptpcol_11_109125),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just40) ).
cnf(39,plain,
genls(c_tptpcol_12_109157,c_tptpcol_11_109125),
inference(cnf,[status(esa)],[just40]) ).
cnf(l134,plain,
genls(c_tptpcol_12_109157,c_tptpcol_11_109125),
inference(instantiation,[status(thm)],[39]) ).
fof(just38,plain,
genls(c_tptpcol_11_109125,c_tptpcol_10_109061),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',just38) ).
cnf(37,plain,
genls(c_tptpcol_11_109125,c_tptpcol_10_109061),
inference(cnf,[status(esa)],[just38]) ).
cnf(l125,plain,
genls(c_tptpcol_11_109125,c_tptpcol_10_109061),
inference(instantiation,[status(thm)],[37]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l47,l48,l112,l113,l114,l115,l116,l117,l118,l49,l128,l120,l135,l136,l119,l121,l130,l50,l122,l129,l51,l124,l138,l131,l140,l62,l139,l133,l66,l63,l137,l126,l141,l127,l76,l132,l142,l123,l134,l125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.10 % Problem : CSR040+1 : TPTP v9.0.0. Released v3.4.0.
% 0.11/0.11 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.32 % Computer : n029.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Sun Jul 20 06:46:49 EDT 2025
% 0.12/0.32 % CPUTime :
% 0.12/0.33 % launching worker at depth: 1
% 0.12/0.33 % launching worker at depth: 3
% 0.12/0.33 % launching worker at depth: 6
% 0.12/0.33 % launching worker at depth: 4
% 0.12/0.33 % launching worker at depth: 2
% 0.12/0.33 % launching worker at depth: 5
% 0.12/0.33 % launching worker at depth: 7
% 0.12/0.33 % launching worker at depth: 8
% 0.12/0.33 % launching worker at depth: 9
% 0.12/0.33 % launching worker at depth: 10
% 0.12/0.33 % launching worker at depth: 11
% 0.12/0.34 % launching worker at depth: 12
% 0.18/0.52 % launching worker at depth: 13
% 8.26/1.47 % SZS status Theorem for theBenchmark
% 8.26/1.47 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------