%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : CSR040+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n007.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 : Wed Apr 9 05:53:34 PM UTC 2025
% Result : Theorem 5.12s 2.22s
% Output : CNFRefutation 5.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 21
% Syntax : Number of formulae : 62 ( 13 unt; 0 typ; 0 def)
% Number of atoms : 111 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 83 ( 34 ~; 29 |; 1 &)
% ( 0 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 38 ( 37 usr; 1 prp; 0-3 aty)
% Number of functors : 40 ( 40 usr; 37 con; 0-2 aty)
% Number of variables : 48 ( 48 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ natargument > natfunction > isa > genls > genlpreds > genlmt > genlinverse > disjointwith > uniformresourcelocator > transitivebinarypredicate > tptpcol_9_109060 > tptpcol_8_109059 > tptpcol_7_108547 > tptpcol_6_108546 > tptpcol_5_106498 > tptpcol_4_106497 > tptpcol_3_98305 > tptpcol_2_98304 > tptpcol_1_65536 > tptpcol_16_62187 > tptpcol_15_109185 > tptpcol_14_109181 > tptpcol_13_109173 > tptpcol_12_109157 > tptpcol_11_109125 > tptpcol_10_109061 > tptpcol_0_0 > thing > predicate > mtvisible > microtheory > individual > fixedordercollection > firstordercollection > computerdataartifact > collection > binarypredicate > f_contentmtofcdafromeventfn > #nlpp > f_urlreferentfn > f_urlfn > s_http_wwwthedailybulletincompostcardsmar9chtm > n_2 > n_1 > c_urlreferentfn > c_urlfn > c_universalvocabularymt > c_translation_14 > c_transitivebinarypredicate > c_tptpcol_9_109060 > c_tptpcol_8_109059 > c_tptpcol_7_108547 > c_tptpcol_6_108546 > c_tptpcol_5_106498 > c_tptpcol_4_106497 > c_tptpcol_3_98305 > c_tptpcol_2_98304 > c_tptpcol_1_65536 > c_tptpcol_16_62187 > c_tptpcol_15_109185 > c_tptpcol_14_109181 > c_tptpcol_13_109173 > c_tptpcol_12_109157 > c_tptpcol_11_109125 > c_tptpcol_10_109061 > c_tptpcol_0_0 > c_machinelearningspindleheadmt > c_logicaltruthmt > c_individual > c_genlmt > c_fixedordercollection > c_firstordercollection > c_cycorpproductsmt > c_cycnounlearnermt > c_corecyclmt > c_contentmtofcdafromeventfn > c_collection > c_basekb
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(c_corecyclmt,type,
c_corecyclmt: $i ).
tff(tptpcol_2_98304,type,
tptpcol_2_98304: $i > $o ).
tff(f_urlreferentfn,type,
f_urlreferentfn: $i > $i ).
tff(mtvisible,type,
mtvisible: $i > $o ).
tff(c_tptpcol_13_109173,type,
c_tptpcol_13_109173: $i ).
tff(tptpcol_0_0,type,
tptpcol_0_0: $i > $o ).
tff(c_tptpcol_10_109061,type,
c_tptpcol_10_109061: $i ).
tff(microtheory,type,
microtheory: $i > $o ).
tff(genls,type,
genls: ( $i * $i ) > $o ).
tff(tptpcol_16_62187,type,
tptpcol_16_62187: $i > $o ).
tff(firstordercollection,type,
firstordercollection: $i > $o ).
tff(genlpreds,type,
genlpreds: ( $i * $i ) > $o ).
tff(collection,type,
collection: $i > $o ).
tff(c_urlfn,type,
c_urlfn: $i ).
tff(tptpcol_11_109125,type,
tptpcol_11_109125: $i > $o ).
tff(fixedordercollection,type,
fixedordercollection: $i > $o ).
tff(c_tptpcol_15_109185,type,
c_tptpcol_15_109185: $i ).
tff(tptpcol_8_109059,type,
tptpcol_8_109059: $i > $o ).
tff(c_tptpcol_12_109157,type,
c_tptpcol_12_109157: $i ).
tff(c_tptpcol_4_106497,type,
c_tptpcol_4_106497: $i ).
tff(tptpcol_6_108546,type,
tptpcol_6_108546: $i > $o ).
tff(c_logicaltruthmt,type,
c_logicaltruthmt: $i ).
tff(binarypredicate,type,
binarypredicate: $i > $o ).
tff(genlmt,type,
genlmt: ( $i * $i ) > $o ).
tff(c_fixedordercollection,type,
c_fixedordercollection: $i ).
tff(tptpcol_5_106498,type,
tptpcol_5_106498: $i > $o ).
tff(f_urlfn,type,
f_urlfn: $i > $i ).
tff(c_genlmt,type,
c_genlmt: $i ).
tff(individual,type,
individual: $i > $o ).
tff(tptpcol_10_109061,type,
tptpcol_10_109061: $i > $o ).
tff(isa,type,
isa: ( $i * $i ) > $o ).
tff(tptpcol_3_98305,type,
tptpcol_3_98305: $i > $o ).
tff(tptpcol_4_106497,type,
tptpcol_4_106497: $i > $o ).
tff(c_tptpcol_8_109059,type,
c_tptpcol_8_109059: $i ).
tff(c_transitivebinarypredicate,type,
c_transitivebinarypredicate: $i ).
tff(tptpcol_7_108547,type,
tptpcol_7_108547: $i > $o ).
tff(c_contentmtofcdafromeventfn,type,
c_contentmtofcdafromeventfn: $i ).
tff(predicate,type,
predicate: $i > $o ).
tff(n_2,type,
n_2: $i ).
tff(tptpcol_12_109157,type,
tptpcol_12_109157: $i > $o ).
tff(c_tptpcol_11_109125,type,
c_tptpcol_11_109125: $i ).
tff(c_translation_14,type,
c_translation_14: $i ).
tff(c_tptpcol_0_0,type,
c_tptpcol_0_0: $i ).
tff(disjointwith,type,
disjointwith: ( $i * $i ) > $o ).
tff(c_tptpcol_5_106498,type,
c_tptpcol_5_106498: $i ).
tff(uniformresourcelocator,type,
uniformresourcelocator: $i > $o ).
tff(tptpcol_15_109185,type,
tptpcol_15_109185: $i > $o ).
tff(c_collection,type,
c_collection: $i ).
tff(thing,type,
thing: $i > $o ).
tff(c_individual,type,
c_individual: $i ).
tff(natfunction,type,
natfunction: ( $i * $i ) > $o ).
tff(c_tptpcol_14_109181,type,
c_tptpcol_14_109181: $i ).
tff(tptpcol_1_65536,type,
tptpcol_1_65536: $i > $o ).
tff(computerdataartifact,type,
computerdataartifact: $i > $o ).
tff(c_machinelearningspindleheadmt,type,
c_machinelearningspindleheadmt: $i ).
tff(c_basekb,type,
c_basekb: $i ).
tff(n_1,type,
n_1: $i ).
tff(natargument,type,
natargument: ( $i * $i * $i ) > $o ).
tff(c_tptpcol_2_98304,type,
c_tptpcol_2_98304: $i ).
tff(c_universalvocabularymt,type,
c_universalvocabularymt: $i ).
tff(c_tptpcol_16_62187,type,
c_tptpcol_16_62187: $i ).
tff(transitivebinarypredicate,type,
transitivebinarypredicate: $i > $o ).
tff(c_cycnounlearnermt,type,
c_cycnounlearnermt: $i ).
tff(s_http_wwwthedailybulletincompostcardsmar9chtm,type,
s_http_wwwthedailybulletincompostcardsmar9chtm: $i ).
tff(c_urlreferentfn,type,
c_urlreferentfn: $i ).
tff(tptpcol_9_109060,type,
tptpcol_9_109060: $i > $o ).
tff(c_cycorpproductsmt,type,
c_cycorpproductsmt: $i ).
tff(c_firstordercollection,type,
c_firstordercollection: $i ).
tff(tptpcol_14_109181,type,
tptpcol_14_109181: $i > $o ).
tff(c_tptpcol_9_109060,type,
c_tptpcol_9_109060: $i ).
tff(c_tptpcol_7_108547,type,
c_tptpcol_7_108547: $i ).
tff(c_tptpcol_6_108546,type,
c_tptpcol_6_108546: $i ).
tff(tptpcol_13_109173,type,
tptpcol_13_109173: $i > $o ).
tff(genlinverse,type,
genlinverse: ( $i * $i ) > $o ).
tff(f_contentmtofcdafromeventfn,type,
f_contentmtofcdafromeventfn: ( $i * $i ) > $i ).
tff(c_tptpcol_1_65536,type,
c_tptpcol_1_65536: $i ).
tff(c_tptpcol_3_98305,type,
c_tptpcol_3_98305: $i ).
tff(f_76,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just17) ).
tff(f_43,axiom,
! [OBJ] :
( firstordercollection(OBJ)
=> fixedordercollection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just4) ).
tff(f_68,axiom,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just14) ).
tff(f_595,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query40) ).
tff(f_166,axiom,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just47) ).
tff(f_160,axiom,
! [OBJ] :
( tptpcol_14_109181(OBJ)
=> tptpcol_13_109173(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just45) ).
tff(f_154,axiom,
! [OBJ] :
( tptpcol_13_109173(OBJ)
=> tptpcol_12_109157(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just43) ).
tff(f_148,axiom,
! [OBJ] :
( tptpcol_12_109157(OBJ)
=> tptpcol_11_109125(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just41) ).
tff(f_142,axiom,
! [OBJ] :
( tptpcol_11_109125(OBJ)
=> tptpcol_10_109061(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just39) ).
tff(f_136,axiom,
! [OBJ] :
( tptpcol_10_109061(OBJ)
=> tptpcol_9_109060(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just37) ).
tff(f_130,axiom,
! [OBJ] :
( tptpcol_9_109060(OBJ)
=> tptpcol_8_109059(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just35) ).
tff(f_124,axiom,
! [OBJ] :
( tptpcol_8_109059(OBJ)
=> tptpcol_7_108547(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just33) ).
tff(f_118,axiom,
! [OBJ] :
( tptpcol_7_108547(OBJ)
=> tptpcol_6_108546(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just31) ).
tff(f_112,axiom,
! [OBJ] :
( tptpcol_6_108546(OBJ)
=> tptpcol_5_106498(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just29) ).
tff(f_106,axiom,
! [OBJ] :
( tptpcol_5_106498(OBJ)
=> tptpcol_4_106497(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just27) ).
tff(f_100,axiom,
! [OBJ] :
( tptpcol_4_106497(OBJ)
=> tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just25) ).
tff(f_94,axiom,
! [OBJ] :
( tptpcol_3_98305(OBJ)
=> tptpcol_2_98304(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just23) ).
tff(f_88,axiom,
! [OBJ] :
( tptpcol_2_98304(OBJ)
=> tptpcol_1_65536(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just21) ).
tff(f_82,axiom,
! [OBJ] :
( tptpcol_1_65536(OBJ)
=> tptpcol_0_0(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just19) ).
tff(f_74,axiom,
! [OBJ] :
( tptpcol_0_0(OBJ)
=> individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just16) ).
tff(f_57,axiom,
! [OBJ] :
~ ( collection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just9) ).
tff(c_34,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_8,plain,
! [OBJ_1] :
( fixedordercollection(OBJ_1)
| ~ firstordercollection(OBJ_1) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_319,plain,
! [OBJ_181] :
( collection(OBJ_181)
| ~ fixedordercollection(OBJ_181) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_352,plain,
! [OBJ_190] :
( collection(OBJ_190)
| ~ firstordercollection(OBJ_190) ),
inference(resolution,[status(thm)],[c_8,c_319]) ).
tff(c_356,plain,
collection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_34,c_352]) ).
tff(c_292,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnfTransformation,[status(thm)],[f_595]) ).
tff(c_305,plain,
! [OBJ_175] :
( tptpcol_14_109181(OBJ_175)
| ~ tptpcol_15_109185(OBJ_175) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_309,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_292,c_305]) ).
tff(c_313,plain,
! [OBJ_179] :
( tptpcol_13_109173(OBJ_179)
| ~ tptpcol_14_109181(OBJ_179) ),
inference(cnfTransformation,[status(thm)],[f_160]) ).
tff(c_317,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_309,c_313]) ).
tff(c_326,plain,
! [OBJ_184] :
( tptpcol_12_109157(OBJ_184)
| ~ tptpcol_13_109173(OBJ_184) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_330,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_317,c_326]) ).
tff(c_337,plain,
! [OBJ_187] :
( tptpcol_11_109125(OBJ_187)
| ~ tptpcol_12_109157(OBJ_187) ),
inference(cnfTransformation,[status(thm)],[f_148]) ).
tff(c_341,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_330,c_337]) ).
tff(c_342,plain,
! [OBJ_188] :
( tptpcol_10_109061(OBJ_188)
| ~ tptpcol_11_109125(OBJ_188) ),
inference(cnfTransformation,[status(thm)],[f_142]) ).
tff(c_346,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_341,c_342]) ).
tff(c_332,plain,
! [OBJ_186] :
( tptpcol_9_109060(OBJ_186)
| ~ tptpcol_10_109061(OBJ_186) ),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_70,plain,
! [OBJ_13] :
( tptpcol_8_109059(OBJ_13)
| ~ tptpcol_9_109060(OBJ_13) ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_347,plain,
! [OBJ_189] :
( tptpcol_8_109059(OBJ_189)
| ~ tptpcol_10_109061(OBJ_189) ),
inference(resolution,[status(thm)],[c_332,c_70]) ).
tff(c_66,plain,
! [OBJ_12] :
( tptpcol_7_108547(OBJ_12)
| ~ tptpcol_8_109059(OBJ_12) ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_358,plain,
! [OBJ_192] :
( tptpcol_7_108547(OBJ_192)
| ~ tptpcol_10_109061(OBJ_192) ),
inference(resolution,[status(thm)],[c_347,c_66]) ).
tff(c_62,plain,
! [OBJ_11] :
( tptpcol_6_108546(OBJ_11)
| ~ tptpcol_7_108547(OBJ_11) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_363,plain,
! [OBJ_193] :
( tptpcol_6_108546(OBJ_193)
| ~ tptpcol_10_109061(OBJ_193) ),
inference(resolution,[status(thm)],[c_358,c_62]) ).
tff(c_58,plain,
! [OBJ_10] :
( tptpcol_5_106498(OBJ_10)
| ~ tptpcol_6_108546(OBJ_10) ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_368,plain,
! [OBJ_194] :
( tptpcol_5_106498(OBJ_194)
| ~ tptpcol_10_109061(OBJ_194) ),
inference(resolution,[status(thm)],[c_363,c_58]) ).
tff(c_54,plain,
! [OBJ_9] :
( tptpcol_4_106497(OBJ_9)
| ~ tptpcol_5_106498(OBJ_9) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_374,plain,
! [OBJ_196] :
( tptpcol_4_106497(OBJ_196)
| ~ tptpcol_10_109061(OBJ_196) ),
inference(resolution,[status(thm)],[c_368,c_54]) ).
tff(c_50,plain,
! [OBJ_8] :
( tptpcol_3_98305(OBJ_8)
| ~ tptpcol_4_106497(OBJ_8) ),
inference(cnfTransformation,[status(thm)],[f_100]) ).
tff(c_379,plain,
! [OBJ_197] :
( tptpcol_3_98305(OBJ_197)
| ~ tptpcol_10_109061(OBJ_197) ),
inference(resolution,[status(thm)],[c_374,c_50]) ).
tff(c_46,plain,
! [OBJ_7] :
( tptpcol_2_98304(OBJ_7)
| ~ tptpcol_3_98305(OBJ_7) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_384,plain,
! [OBJ_198] :
( tptpcol_2_98304(OBJ_198)
| ~ tptpcol_10_109061(OBJ_198) ),
inference(resolution,[status(thm)],[c_379,c_46]) ).
tff(c_42,plain,
! [OBJ_6] :
( tptpcol_1_65536(OBJ_6)
| ~ tptpcol_2_98304(OBJ_6) ),
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_389,plain,
! [OBJ_199] :
( tptpcol_1_65536(OBJ_199)
| ~ tptpcol_10_109061(OBJ_199) ),
inference(resolution,[status(thm)],[c_384,c_42]) ).
tff(c_38,plain,
! [OBJ_5] :
( tptpcol_0_0(OBJ_5)
| ~ tptpcol_1_65536(OBJ_5) ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_394,plain,
! [OBJ_200] :
( tptpcol_0_0(OBJ_200)
| ~ tptpcol_10_109061(OBJ_200) ),
inference(resolution,[status(thm)],[c_389,c_38]) ).
tff(c_398,plain,
tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_346,c_394]) ).
tff(c_32,plain,
! [OBJ_4] :
( individual(OBJ_4)
| ~ tptpcol_0_0(OBJ_4) ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_403,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_398,c_32]) ).
tff(c_18,plain,
! [OBJ_2] :
( ~ individual(OBJ_2)
| ~ collection(OBJ_2) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_406,plain,
~ collection(c_tptpcol_16_62187),
inference(resolution,[status(thm)],[c_403,c_18]) ).
tff(c_410,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_356,c_406]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : CSR040+1 : TPTP v9.0.0. Released v3.4.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n007.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 16:47:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 5.12/2.22 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.12/2.22
% 5.12/2.22 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------