%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR040+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n026.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 : Fri Sep 25 01:05:23 PM UTC 2026
% Result : Theorem 93.95s 17.29s
% Output : Proof 93.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 29
% Syntax : Number of formulae : 160 ( 60 unt; 0 def)
% Number of atoms : 264 ( 43 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 220 ( 116 ~; 75 |; 9 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 135 ( 0 sgn 87 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f265,axiom,
! [OBJ] :
( tptpcol_15_109185(OBJ)
=> tptpcol_14_109181(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_266) ).
fof(f265_nnf,plain,
! [OBJ] :
( tptpcol_14_109181(OBJ)
| ~ tptpcol_15_109185(OBJ) ),
inference(nnf_transformation,[status(thm)],[f265]) ).
fof(f265_sk,plain,
! [OBJ] :
( tptpcol_14_109181(OBJ)
| ~ tptpcol_15_109185(OBJ) ),
inference(skolemisation,[status(esa)],[f265_nnf]) ).
cnf(c265,plain,
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
cnf(hi262,axiom,
ifeq(tptpcol_15_109185(X0),true,tptpcol_14_109181(X0),true) = true,
inference(equality_encoding,[status(esa)],[c265]) ).
fof(f1131,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',query90) ).
fof(f1131_neg,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(negated_conjecture,[status(cth)],[f1131]) ).
fof(f1131_nnf,plain,
( tptpcol_15_109185(c_tptpcol_16_62187)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)) ),
inference(nnf_transformation,[status(thm)],[f1131_neg]) ).
fof(f1131_sk,plain,
( tptpcol_15_109185(c_tptpcol_16_62187)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)) ),
inference(skolemisation,[status(esa)],[f1131_nnf]) ).
cnf(c1132,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[status(esa)],[f1131_sk]) ).
cnf(hi1123,negated_conjecture,
tptpcol_15_109185(c_tptpcol_16_62187) = true,
inference(equality_encoding,[status(esa)],[c1132]) ).
cnf(h22,plain,
tptpcol_14_109181(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi262,hi1123]) ).
fof(f250,axiom,
! [OBJ] :
( tptpcol_14_109181(OBJ)
=> tptpcol_13_109173(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_251) ).
fof(f250_nnf,plain,
! [OBJ] :
( tptpcol_13_109173(OBJ)
| ~ tptpcol_14_109181(OBJ) ),
inference(nnf_transformation,[status(thm)],[f250]) ).
fof(f250_sk,plain,
! [OBJ] :
( tptpcol_13_109173(OBJ)
| ~ tptpcol_14_109181(OBJ) ),
inference(skolemisation,[status(esa)],[f250_nnf]) ).
cnf(c250,plain,
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(cnf_transformation,[status(esa)],[f250_sk]) ).
cnf(hi247,axiom,
ifeq(tptpcol_14_109181(X0),true,tptpcol_13_109173(X0),true) = true,
inference(equality_encoding,[status(esa)],[c250]) ).
cnf(h37,plain,
tptpcol_13_109173(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi247,h22]) ).
fof(f113,axiom,
! [OBJ] :
( tptpcol_13_109173(OBJ)
=> tptpcol_12_109157(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_114) ).
fof(f113_nnf,plain,
! [OBJ] :
( tptpcol_12_109157(OBJ)
| ~ tptpcol_13_109173(OBJ) ),
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
! [OBJ] :
( tptpcol_12_109157(OBJ)
| ~ tptpcol_13_109173(OBJ) ),
inference(skolemisation,[status(esa)],[f113_nnf]) ).
cnf(c113,plain,
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(hi112,axiom,
ifeq(tptpcol_13_109173(X0),true,tptpcol_12_109157(X0),true) = true,
inference(equality_encoding,[status(esa)],[c113]) ).
cnf(h51,plain,
tptpcol_12_109157(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi112,h37]) ).
fof(f359,axiom,
! [OBJ] :
( tptpcol_12_109157(OBJ)
=> tptpcol_11_109125(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_360) ).
fof(f359_nnf,plain,
! [OBJ] :
( tptpcol_11_109125(OBJ)
| ~ tptpcol_12_109157(OBJ) ),
inference(nnf_transformation,[status(thm)],[f359]) ).
fof(f359_sk,plain,
! [OBJ] :
( tptpcol_11_109125(OBJ)
| ~ tptpcol_12_109157(OBJ) ),
inference(skolemisation,[status(esa)],[f359_nnf]) ).
cnf(c359,plain,
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(cnf_transformation,[status(esa)],[f359_sk]) ).
cnf(hi355,axiom,
ifeq(tptpcol_12_109157(X0),true,tptpcol_11_109125(X0),true) = true,
inference(equality_encoding,[status(esa)],[c359]) ).
cnf(h59,plain,
tptpcol_11_109125(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi355,h51]) ).
fof(f342,axiom,
! [OBJ] :
( tptpcol_11_109125(OBJ)
=> tptpcol_10_109061(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_343) ).
fof(f342_nnf,plain,
! [OBJ] :
( tptpcol_10_109061(OBJ)
| ~ tptpcol_11_109125(OBJ) ),
inference(nnf_transformation,[status(thm)],[f342]) ).
fof(f342_sk,plain,
! [OBJ] :
( tptpcol_10_109061(OBJ)
| ~ tptpcol_11_109125(OBJ) ),
inference(skolemisation,[status(esa)],[f342_nnf]) ).
cnf(c342,plain,
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(cnf_transformation,[status(esa)],[f342_sk]) ).
cnf(hi338,axiom,
ifeq(tptpcol_11_109125(X0),true,tptpcol_10_109061(X0),true) = true,
inference(equality_encoding,[status(esa)],[c342]) ).
cnf(h63,plain,
tptpcol_10_109061(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi338,h59]) ).
fof(f95,axiom,
! [OBJ] :
( tptpcol_10_109061(OBJ)
=> tptpcol_9_109060(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_96) ).
fof(f95_nnf,plain,
! [OBJ] :
( tptpcol_9_109060(OBJ)
| ~ tptpcol_10_109061(OBJ) ),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
! [OBJ] :
( tptpcol_9_109060(OBJ)
| ~ tptpcol_10_109061(OBJ) ),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c95,plain,
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(hi94,axiom,
ifeq(tptpcol_10_109061(X0),true,tptpcol_9_109060(X0),true) = true,
inference(equality_encoding,[status(esa)],[c95]) ).
cnf(h67,plain,
tptpcol_9_109060(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi94,h63]) ).
fof(f241,axiom,
! [OBJ] :
( tptpcol_9_109060(OBJ)
=> tptpcol_8_109059(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_242) ).
fof(f241_nnf,plain,
! [OBJ] :
( tptpcol_8_109059(OBJ)
| ~ tptpcol_9_109060(OBJ) ),
inference(nnf_transformation,[status(thm)],[f241]) ).
fof(f241_sk,plain,
! [OBJ] :
( tptpcol_8_109059(OBJ)
| ~ tptpcol_9_109060(OBJ) ),
inference(skolemisation,[status(esa)],[f241_nnf]) ).
cnf(c241,plain,
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
cnf(hi238,axiom,
ifeq(tptpcol_9_109060(X0),true,tptpcol_8_109059(X0),true) = true,
inference(equality_encoding,[status(esa)],[c241]) ).
cnf(h71,plain,
tptpcol_8_109059(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi238,h67]) ).
fof(f184,axiom,
! [OBJ] :
( tptpcol_8_109059(OBJ)
=> tptpcol_7_108547(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_185) ).
fof(f184_nnf,plain,
! [OBJ] :
( tptpcol_7_108547(OBJ)
| ~ tptpcol_8_109059(OBJ) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [OBJ] :
( tptpcol_7_108547(OBJ)
| ~ tptpcol_8_109059(OBJ) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c184,plain,
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(hi181,axiom,
ifeq(tptpcol_8_109059(X0),true,tptpcol_7_108547(X0),true) = true,
inference(equality_encoding,[status(esa)],[c184]) ).
cnf(h75,plain,
tptpcol_7_108547(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi181,h71]) ).
fof(f340,axiom,
! [OBJ] :
( tptpcol_7_108547(OBJ)
=> tptpcol_6_108546(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_341) ).
fof(f340_nnf,plain,
! [OBJ] :
( tptpcol_6_108546(OBJ)
| ~ tptpcol_7_108547(OBJ) ),
inference(nnf_transformation,[status(thm)],[f340]) ).
fof(f340_sk,plain,
! [OBJ] :
( tptpcol_6_108546(OBJ)
| ~ tptpcol_7_108547(OBJ) ),
inference(skolemisation,[status(esa)],[f340_nnf]) ).
cnf(c340,plain,
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(cnf_transformation,[status(esa)],[f340_sk]) ).
cnf(hi336,axiom,
ifeq(tptpcol_7_108547(X0),true,tptpcol_6_108546(X0),true) = true,
inference(equality_encoding,[status(esa)],[c340]) ).
cnf(h78,plain,
tptpcol_6_108546(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi336,h75]) ).
fof(f458,axiom,
! [OBJ] :
( tptpcol_6_108546(OBJ)
=> tptpcol_5_106498(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_459) ).
fof(f458_nnf,plain,
! [OBJ] :
( tptpcol_5_106498(OBJ)
| ~ tptpcol_6_108546(OBJ) ),
inference(nnf_transformation,[status(thm)],[f458]) ).
fof(f458_sk,plain,
! [OBJ] :
( tptpcol_5_106498(OBJ)
| ~ tptpcol_6_108546(OBJ) ),
inference(skolemisation,[status(esa)],[f458_nnf]) ).
cnf(c458,plain,
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(cnf_transformation,[status(esa)],[f458_sk]) ).
cnf(hi453,axiom,
ifeq(tptpcol_6_108546(X0),true,tptpcol_5_106498(X0),true) = true,
inference(equality_encoding,[status(esa)],[c458]) ).
cnf(h80,plain,
tptpcol_5_106498(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi453,h78]) ).
fof(f116,axiom,
! [OBJ] :
( tptpcol_5_106498(OBJ)
=> tptpcol_4_106497(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_117) ).
fof(f116_nnf,plain,
! [OBJ] :
( tptpcol_4_106497(OBJ)
| ~ tptpcol_5_106498(OBJ) ),
inference(nnf_transformation,[status(thm)],[f116]) ).
fof(f116_sk,plain,
! [OBJ] :
( tptpcol_4_106497(OBJ)
| ~ tptpcol_5_106498(OBJ) ),
inference(skolemisation,[status(esa)],[f116_nnf]) ).
cnf(c116,plain,
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(cnf_transformation,[status(esa)],[f116_sk]) ).
cnf(hi115,axiom,
ifeq(tptpcol_5_106498(X0),true,tptpcol_4_106497(X0),true) = true,
inference(equality_encoding,[status(esa)],[c116]) ).
cnf(h82,plain,
tptpcol_4_106497(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi115,h80]) ).
fof(f68,axiom,
! [OBJ] :
( tptpcol_4_106497(OBJ)
=> tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_69) ).
fof(f68_nnf,plain,
! [OBJ] :
( tptpcol_3_98305(OBJ)
| ~ tptpcol_4_106497(OBJ) ),
inference(nnf_transformation,[status(thm)],[f68]) ).
fof(f68_sk,plain,
! [OBJ] :
( tptpcol_3_98305(OBJ)
| ~ tptpcol_4_106497(OBJ) ),
inference(skolemisation,[status(esa)],[f68_nnf]) ).
cnf(c68,plain,
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(cnf_transformation,[status(esa)],[f68_sk]) ).
cnf(hi67,axiom,
ifeq(tptpcol_4_106497(X0),true,tptpcol_3_98305(X0),true) = true,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(h84,plain,
tptpcol_3_98305(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi67,h82]) ).
fof(f233,axiom,
! [OBJ] :
( tptpcol_3_98305(OBJ)
=> tptpcol_2_98304(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_234) ).
fof(f233_nnf,plain,
! [OBJ] :
( tptpcol_2_98304(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(nnf_transformation,[status(thm)],[f233]) ).
fof(f233_sk,plain,
! [OBJ] :
( tptpcol_2_98304(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(skolemisation,[status(esa)],[f233_nnf]) ).
cnf(c233,plain,
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(esa)],[f233_sk]) ).
cnf(hi230,axiom,
ifeq(tptpcol_3_98305(X0),true,tptpcol_2_98304(X0),true) = true,
inference(equality_encoding,[status(esa)],[c233]) ).
cnf(h86,plain,
tptpcol_2_98304(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi230,h84]) ).
fof(f49,axiom,
! [OBJ] :
( tptpcol_2_98304(OBJ)
=> tptpcol_1_65536(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_50) ).
fof(f49_nnf,plain,
! [OBJ] :
( tptpcol_1_65536(OBJ)
| ~ tptpcol_2_98304(OBJ) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [OBJ] :
( tptpcol_1_65536(OBJ)
| ~ tptpcol_2_98304(OBJ) ),
inference(skolemisation,[status(esa)],[f49_nnf]) ).
cnf(c49,plain,
( tptpcol_1_65536(X0)
| ~ tptpcol_2_98304(X0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
cnf(hi48,axiom,
ifeq(tptpcol_2_98304(X0),true,tptpcol_1_65536(X0),true) = true,
inference(equality_encoding,[status(esa)],[c49]) ).
cnf(h88,plain,
tptpcol_1_65536(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi48,h86]) ).
fof(f123,axiom,
! [OBJ] :
( tptpcol_1_65536(OBJ)
=> tptpcol_0_0(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_124) ).
fof(f123_nnf,plain,
! [OBJ] :
( tptpcol_0_0(OBJ)
| ~ tptpcol_1_65536(OBJ) ),
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
! [OBJ] :
( tptpcol_0_0(OBJ)
| ~ tptpcol_1_65536(OBJ) ),
inference(skolemisation,[status(esa)],[f123_nnf]) ).
cnf(c123,plain,
( tptpcol_0_0(X0)
| ~ tptpcol_1_65536(X0) ),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
cnf(hi122,axiom,
ifeq(tptpcol_1_65536(X0),true,tptpcol_0_0(X0),true) = true,
inference(equality_encoding,[status(esa)],[c123]) ).
cnf(h90,plain,
tptpcol_0_0(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi122,h88]) ).
fof(f444,axiom,
! [OBJ] :
( tptpcol_0_0(OBJ)
=> individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_445) ).
fof(f444_nnf,plain,
! [OBJ] :
( individual(OBJ)
| ~ tptpcol_0_0(OBJ) ),
inference(nnf_transformation,[status(thm)],[f444]) ).
fof(f444_sk,plain,
! [OBJ] :
( individual(OBJ)
| ~ tptpcol_0_0(OBJ) ),
inference(skolemisation,[status(esa)],[f444_nnf]) ).
cnf(c444,plain,
( individual(X0)
| ~ tptpcol_0_0(X0) ),
inference(cnf_transformation,[status(esa)],[f444_sk]) ).
cnf(hi439,axiom,
ifeq(tptpcol_0_0(X0),true,individual(X0),true) = true,
inference(equality_encoding,[status(esa)],[c444]) ).
cnf(h92,plain,
individual(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi439,h90]) ).
fof(f204,axiom,
! [OBJ] :
( firstordercollection(OBJ)
=> fixedordercollection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_205) ).
fof(f204_nnf,plain,
! [OBJ] :
( fixedordercollection(OBJ)
| ~ firstordercollection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f204]) ).
fof(f204_sk,plain,
! [OBJ] :
( fixedordercollection(OBJ)
| ~ firstordercollection(OBJ) ),
inference(skolemisation,[status(esa)],[f204_nnf]) ).
cnf(c204,plain,
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(cnf_transformation,[status(esa)],[f204_sk]) ).
cnf(hi201,axiom,
ifeq(firstordercollection(X0),true,fixedordercollection(X0),true) = true,
inference(equality_encoding,[status(esa)],[c204]) ).
fof(f474,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_475) ).
fof(f474_nnf,plain,
firstordercollection(c_tptpcol_16_62187),
inference(nnf_transformation,[status(thm)],[f474]) ).
cnf(c474,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[status(esa)],[f474_nnf]) ).
cnf(hi469,axiom,
firstordercollection(c_tptpcol_16_62187) = true,
inference(equality_encoding,[status(esa)],[c474]) ).
cnf(h20,plain,
fixedordercollection(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi201,hi469]) ).
fof(f150,axiom,
! [OBJ] :
( fixedordercollection(OBJ)
=> collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_151) ).
fof(f150_nnf,plain,
! [OBJ] :
( collection(OBJ)
| ~ fixedordercollection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f150]) ).
fof(f150_sk,plain,
! [OBJ] :
( collection(OBJ)
| ~ fixedordercollection(OBJ) ),
inference(skolemisation,[status(esa)],[f150_nnf]) ).
cnf(c150,plain,
( collection(X0)
| ~ fixedordercollection(X0) ),
inference(cnf_transformation,[status(esa)],[f150_sk]) ).
cnf(hi149,axiom,
ifeq(fixedordercollection(X0),true,collection(X0),true) = true,
inference(equality_encoding,[status(esa)],[c150]) ).
cnf(h35,plain,
collection(c_tptpcol_16_62187) = true,
inference(hyper_resolution,[status(thm)],[hi149,h20]) ).
fof(f288,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_289) ).
fof(f288_nnf,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f288]) ).
fof(f288_sk,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(skolemisation,[status(esa)],[f288_nnf]) ).
cnf(c288,plain,
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
cnf(hi1127,axiom,
ifeq(collection(X0),true,ifeq(individual(X0),true,false,true),true) = true,
inference(equality_encoding,[status(esa)],[c288]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi1127,h35,h92]) ).
cnf(t1044,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f2,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& intangible(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_3) ).
fof(f2_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f152,axiom,
! [OBJ] :
~ ( tptpcol_1_65536(OBJ)
& tptpcol_1_1(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_153) ).
fof(f152_nnf,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(nnf_transformation,[status(thm)],[f152]) ).
fof(f152_sk,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(skolemisation,[status(esa)],[f152_nnf]) ).
cnf(c152,plain,
( ~ tptpcol_1_65536(X0)
| ~ tptpcol_1_1(X0) ),
inference(cnf_transformation,[status(esa)],[f152_sk]) ).
fof(f166,axiom,
! [OBJ] :
~ ( setorcollection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_167) ).
fof(f166_nnf,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
( ~ setorcollection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
fof(f362,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_363) ).
fof(f362_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f362]) ).
fof(f362_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f362_nnf]) ).
cnf(c362,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f362_sk]) ).
fof(f487,axiom,
! [OBJ] :
~ ( tptpcol_3_114688(OBJ)
& tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_488) ).
fof(f487_nnf,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(nnf_transformation,[status(thm)],[f487]) ).
fof(f487_sk,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(skolemisation,[status(esa)],[f487_nnf]) ).
cnf(c487,plain,
( ~ tptpcol_3_114688(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(esa)],[f487_sk]) ).
fof(f520,axiom,
! [X] : ~ affiliatedwith(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_521) ).
fof(f520_nnf,plain,
! [X] : ~ affiliatedwith(X,X),
inference(nnf_transformation,[status(thm)],[f520]) ).
fof(f520_sk,plain,
! [X] : ~ affiliatedwith(X,X),
inference(skolemisation,[status(esa)],[f520_nnf]) ).
cnf(c520,plain,
~ affiliatedwith(X0,X0),
inference(cnf_transformation,[status(esa)],[f520_sk]) ).
fof(f697,axiom,
! [X] : ~ objectfoundinlocation(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_698) ).
fof(f697_nnf,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(nnf_transformation,[status(thm)],[f697]) ).
fof(f697_sk,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(skolemisation,[status(esa)],[f697_nnf]) ).
cnf(c697,plain,
~ objectfoundinlocation(X0,X0),
inference(cnf_transformation,[status(esa)],[f697_sk]) ).
fof(f900,axiom,
! [X] : ~ borderson(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_901) ).
fof(f900_nnf,plain,
! [X] : ~ borderson(X,X),
inference(nnf_transformation,[status(thm)],[f900]) ).
fof(f900_sk,plain,
! [X] : ~ borderson(X,X),
inference(skolemisation,[status(esa)],[f900_nnf]) ).
cnf(c900,plain,
~ borderson(X0,X0),
inference(cnf_transformation,[status(esa)],[f900_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c152,c166,c288,c362,c487,c520,c697,c900]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1044]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.37 % Computer : n026.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Fri Sep 25 08:27:30 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 93.95/17.29 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 93.95/17.29 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------