%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR049+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.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:29 PM UTC 2026
% Result : Theorem 162.60s 21.77s
% Output : Proof 162.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 109
% Syntax : Number of formulae : 476 ( 292 unt; 0 def)
% Number of atoms : 680 ( 69 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 656 ( 452 ~; 150 |; 49 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 1 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 36 con; 0-4 aty)
% Number of variables : 461 ( 0 sgn 339 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7994,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& genls(ARG1,OLD) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7995) ).
fof(f7994_nnf,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f7994]) ).
fof(f7994_sk,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f7994_nnf]) ).
cnf(c7994,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7994_sk]) ).
cnf(hi7920,axiom,
ifeq(genls(X0,X1),true,ifeq(genls(X1,X2),true,genls(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c7994]) ).
fof(f1179,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1180) ).
fof(f1179_nnf,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(nnf_transformation,[status(thm)],[f1179]) ).
cnf(c1179,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(cnf_transformation,[status(esa)],[f1179_nnf]) ).
cnf(hi1176,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268) = true,
inference(equality_encoding,[status(esa)],[c1179]) ).
fof(f1714,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1715) ).
fof(f1714_nnf,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(nnf_transformation,[status(thm)],[f1714]) ).
cnf(c1714,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(cnf_transformation,[status(esa)],[f1714_nnf]) ).
cnf(hi1708,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264) = true,
inference(equality_encoding,[status(esa)],[c1714]) ).
cnf(h20,plain,
genls(c_tptpcol_16_92269,c_tptpcol_14_92264) = true,
inference(hyper_resolution,[status(thm)],[hi7920,hi1176,hi1708]) ).
fof(f741,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_742) ).
fof(f741_nnf,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(nnf_transformation,[status(thm)],[f741]) ).
cnf(c741,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(cnf_transformation,[status(esa)],[f741_nnf]) ).
cnf(hi739,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263) = true,
inference(equality_encoding,[status(esa)],[c741]) ).
cnf(h597,plain,
genls(c_tptpcol_16_92269,c_tptpcol_13_92263) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h20,hi739]) ).
fof(f2007,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2008) ).
fof(f2007_nnf,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(nnf_transformation,[status(thm)],[f2007]) ).
cnf(c2007,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(cnf_transformation,[status(esa)],[f2007_nnf]) ).
cnf(hi1999,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262) = true,
inference(equality_encoding,[status(esa)],[c2007]) ).
cnf(h1677,plain,
genls(c_tptpcol_16_92269,c_tptpcol_12_92262) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h597,hi1999]) ).
fof(f3435,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3436) ).
fof(f3435_nnf,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(nnf_transformation,[status(thm)],[f3435]) ).
cnf(c3435,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(cnf_transformation,[status(esa)],[f3435_nnf]) ).
cnf(hi3421,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230) = true,
inference(equality_encoding,[status(esa)],[c3435]) ).
cnf(h3259,plain,
genls(c_tptpcol_16_92269,c_tptpcol_11_92230) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1677,hi3421]) ).
fof(f415,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_416) ).
fof(f415_nnf,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(nnf_transformation,[status(thm)],[f415]) ).
cnf(c415,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(cnf_transformation,[status(esa)],[f415_nnf]) ).
cnf(hi414,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166) = true,
inference(equality_encoding,[status(esa)],[c415]) ).
cnf(h3264,plain,
genls(c_tptpcol_16_92269,c_tptpcol_10_92166) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3259,hi414]) ).
fof(f2999,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3000) ).
fof(f2999_nnf,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(nnf_transformation,[status(thm)],[f2999]) ).
cnf(c2999,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(cnf_transformation,[status(esa)],[f2999_nnf]) ).
cnf(hi2987,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165) = true,
inference(equality_encoding,[status(esa)],[c2999]) ).
cnf(h3267,plain,
genls(c_tptpcol_16_92269,c_tptpcol_9_92165) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3264,hi2987]) ).
fof(f3409,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3410) ).
fof(f3409_nnf,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(nnf_transformation,[status(thm)],[f3409]) ).
cnf(c3409,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(cnf_transformation,[status(esa)],[f3409_nnf]) ).
cnf(hi3395,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164) = true,
inference(equality_encoding,[status(esa)],[c3409]) ).
cnf(h3270,plain,
genls(c_tptpcol_16_92269,c_tptpcol_8_92164) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3267,hi3395]) ).
fof(f2875,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2876) ).
fof(f2875_nnf,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(nnf_transformation,[status(thm)],[f2875]) ).
cnf(c2875,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(cnf_transformation,[status(esa)],[f2875_nnf]) ).
cnf(hi2863,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163) = true,
inference(equality_encoding,[status(esa)],[c2875]) ).
cnf(h3273,plain,
genls(c_tptpcol_16_92269,c_tptpcol_7_92163) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3270,hi2863]) ).
fof(f1558,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1559) ).
fof(f1558_nnf,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(nnf_transformation,[status(thm)],[f1558]) ).
cnf(c1558,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(cnf_transformation,[status(esa)],[f1558_nnf]) ).
cnf(hi1553,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162) = true,
inference(equality_encoding,[status(esa)],[c1558]) ).
cnf(h3276,plain,
genls(c_tptpcol_16_92269,c_tptpcol_6_92162) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3273,hi1553]) ).
fof(f2947,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2948) ).
fof(f2947_nnf,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(nnf_transformation,[status(thm)],[f2947]) ).
cnf(c2947,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[status(esa)],[f2947_nnf]) ).
cnf(hi2935,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114) = true,
inference(equality_encoding,[status(esa)],[c2947]) ).
cnf(h3279,plain,
genls(c_tptpcol_16_92269,c_tptpcol_5_90114) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3276,hi2935]) ).
fof(f2885,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2886) ).
fof(f2885_nnf,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(nnf_transformation,[status(thm)],[f2885]) ).
cnf(c2885,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[status(esa)],[f2885_nnf]) ).
cnf(hi2873,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113) = true,
inference(equality_encoding,[status(esa)],[c2885]) ).
cnf(h3282,plain,
genls(c_tptpcol_16_92269,c_tptpcol_4_90113) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3279,hi2873]) ).
fof(f3628,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3629) ).
fof(f3628_nnf,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(nnf_transformation,[status(thm)],[f3628]) ).
cnf(c3628,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[status(esa)],[f3628_nnf]) ).
cnf(hi3614,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921) = true,
inference(equality_encoding,[status(esa)],[c3628]) ).
cnf(h3990,plain,
genls(c_tptpcol_16_92269,c_tptpcol_3_81921) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3282,hi3614]) ).
fof(f1199,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1200) ).
fof(f1199_nnf,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(nnf_transformation,[status(thm)],[f1199]) ).
cnf(c1199,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(cnf_transformation,[status(esa)],[f1199_nnf]) ).
cnf(hi1196,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925) = true,
inference(equality_encoding,[status(esa)],[c1199]) ).
fof(f243,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_244) ).
fof(f243_nnf,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(nnf_transformation,[status(thm)],[f243]) ).
cnf(c243,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(cnf_transformation,[status(esa)],[f243_nnf]) ).
cnf(hi242,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921) = true,
inference(equality_encoding,[status(esa)],[c243]) ).
cnf(h12,plain,
genls(c_tptpcol_16_26926,c_tptpcol_14_26921) = true,
inference(hyper_resolution,[status(thm)],[hi7920,hi1196,hi242]) ).
fof(f1916,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1917) ).
fof(f1916_nnf,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(nnf_transformation,[status(thm)],[f1916]) ).
cnf(c1916,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(cnf_transformation,[status(esa)],[f1916_nnf]) ).
cnf(hi1908,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920) = true,
inference(equality_encoding,[status(esa)],[c1916]) ).
cnf(h1625,plain,
genls(c_tptpcol_16_26926,c_tptpcol_13_26920) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h12,hi1908]) ).
fof(f695,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_696) ).
fof(f695_nnf,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(nnf_transformation,[status(thm)],[f695]) ).
cnf(c695,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(cnf_transformation,[status(esa)],[f695_nnf]) ).
cnf(hi693,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919) = true,
inference(equality_encoding,[status(esa)],[c695]) ).
cnf(h1629,plain,
genls(c_tptpcol_16_26926,c_tptpcol_12_26919) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1625,hi693]) ).
fof(f550,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_551) ).
fof(f550_nnf,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(nnf_transformation,[status(thm)],[f550]) ).
cnf(c550,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(cnf_transformation,[status(esa)],[f550_nnf]) ).
cnf(hi548,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887) = true,
inference(equality_encoding,[status(esa)],[c550]) ).
cnf(h1632,plain,
genls(c_tptpcol_16_26926,c_tptpcol_11_26887) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1629,hi548]) ).
fof(f1156,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1157) ).
fof(f1156_nnf,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(nnf_transformation,[status(thm)],[f1156]) ).
cnf(c1156,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(cnf_transformation,[status(esa)],[f1156_nnf]) ).
cnf(hi1153,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886) = true,
inference(equality_encoding,[status(esa)],[c1156]) ).
cnf(h1635,plain,
genls(c_tptpcol_16_26926,c_tptpcol_10_26886) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1632,hi1153]) ).
fof(f884,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_885) ).
fof(f884_nnf,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(nnf_transformation,[status(thm)],[f884]) ).
cnf(c884,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(cnf_transformation,[status(esa)],[f884_nnf]) ).
cnf(hi881,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885) = true,
inference(equality_encoding,[status(esa)],[c884]) ).
cnf(h1638,plain,
genls(c_tptpcol_16_26926,c_tptpcol_9_26885) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1635,hi881]) ).
fof(f3512,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3513) ).
fof(f3512_nnf,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(nnf_transformation,[status(thm)],[f3512]) ).
cnf(c3512,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(cnf_transformation,[status(esa)],[f3512_nnf]) ).
cnf(hi3498,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629) = true,
inference(equality_encoding,[status(esa)],[c3512]) ).
cnf(h3313,plain,
genls(c_tptpcol_16_26926,c_tptpcol_8_26629) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1638,hi3498]) ).
fof(f1165,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1166) ).
fof(f1165_nnf,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(nnf_transformation,[status(thm)],[f1165]) ).
cnf(c1165,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(cnf_transformation,[status(esa)],[f1165_nnf]) ).
cnf(hi1162,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628) = true,
inference(equality_encoding,[status(esa)],[c1165]) ).
cnf(h3325,plain,
genls(c_tptpcol_16_26926,c_tptpcol_7_26628) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3313,hi1162]) ).
fof(f3255,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3256) ).
fof(f3255_nnf,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(nnf_transformation,[status(thm)],[f3255]) ).
cnf(c3255,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(cnf_transformation,[status(esa)],[f3255_nnf]) ).
cnf(hi3241,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627) = true,
inference(equality_encoding,[status(esa)],[c3255]) ).
cnf(h3346,plain,
genls(c_tptpcol_16_26926,c_tptpcol_6_26627) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3325,hi3241]) ).
fof(f3012,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3013) ).
fof(f3012_nnf,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(nnf_transformation,[status(thm)],[f3012]) ).
cnf(c3012,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(cnf_transformation,[status(esa)],[f3012_nnf]) ).
cnf(hi3000,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579) = true,
inference(equality_encoding,[status(esa)],[c3012]) ).
cnf(h3402,plain,
genls(c_tptpcol_16_26926,c_tptpcol_5_24579) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3346,hi3000]) ).
fof(f1243,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1244) ).
fof(f1243_nnf,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(nnf_transformation,[status(thm)],[f1243]) ).
cnf(c1243,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(cnf_transformation,[status(esa)],[f1243_nnf]) ).
cnf(hi1240,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578) = true,
inference(equality_encoding,[status(esa)],[c1243]) ).
cnf(h3481,plain,
genls(c_tptpcol_16_26926,c_tptpcol_4_24578) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3402,hi1240]) ).
fof(f3213,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3214) ).
fof(f3213_nnf,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(nnf_transformation,[status(thm)],[f3213]) ).
cnf(c3213,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(cnf_transformation,[status(esa)],[f3213_nnf]) ).
cnf(hi3200,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386) = true,
inference(equality_encoding,[status(esa)],[c3213]) ).
cnf(h3505,plain,
genls(c_tptpcol_16_26926,c_tptpcol_3_16386) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3481,hi3200]) ).
fof(f459,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_460) ).
fof(f459_nnf,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(nnf_transformation,[status(thm)],[f459]) ).
cnf(c459,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(esa)],[f459_nnf]) ).
cnf(hi458,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2) = true,
inference(equality_encoding,[status(esa)],[c459]) ).
cnf(h3521,plain,
genls(c_tptpcol_16_26926,c_tptpcol_2_2) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3505,hi458]) ).
fof(f3252,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3253) ).
fof(f3252_nnf,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(nnf_transformation,[status(thm)],[f3252]) ).
cnf(c3252,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(esa)],[f3252_nnf]) ).
cnf(hi3238,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1) = true,
inference(equality_encoding,[status(esa)],[c3252]) ).
cnf(h3535,plain,
genls(c_tptpcol_16_26926,c_tptpcol_1_1) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h3521,hi3238]) ).
fof(f7585,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7586) ).
fof(f7585_nnf,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(nnf_transformation,[status(thm)],[f7585]) ).
fof(f7585_sk,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(skolemisation,[status(esa)],[f7585_nnf]) ).
cnf(c7585,plain,
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7585_sk]) ).
cnf(hi7514,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X0),true,disjointwith(X2,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c7585]) ).
fof(f1801,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1802) ).
fof(f1801_nnf,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(nnf_transformation,[status(thm)],[f1801]) ).
cnf(c1801,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(esa)],[f1801_nnf]) ).
cnf(hi1794,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) = true,
inference(equality_encoding,[status(esa)],[c1801]) ).
cnf(h3543,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi7514,hi1794,h3535]) ).
fof(f7584,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7585) ).
fof(f7584_nnf,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f7584]) ).
fof(f7584_sk,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f7584_nnf]) ).
cnf(c7584,plain,
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7584_sk]) ).
cnf(hi7513,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X1),true,disjointwith(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c7584]) ).
fof(f917,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_918) ).
fof(f917_nnf,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(nnf_transformation,[status(thm)],[f917]) ).
cnf(c917,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(esa)],[f917_nnf]) ).
cnf(hi914,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536) = true,
inference(equality_encoding,[status(esa)],[c917]) ).
cnf(h3549,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_2_65537) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h3543,hi914]) ).
fof(f3462,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3463) ).
fof(f3462_nnf,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(nnf_transformation,[status(thm)],[f3462]) ).
cnf(c3462,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[status(esa)],[f3462_nnf]) ).
cnf(hi3448,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537) = true,
inference(equality_encoding,[status(esa)],[c3462]) ).
cnf(h3562,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_3_81921) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h3549,hi3448]) ).
cnf(h4010,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h3562,h3990]) ).
fof(f8005,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query149) ).
fof(f8005_neg,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(negated_conjecture,[status(cth)],[f8005]) ).
fof(f8005_nnf,plain,
( ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)
& mtvisible(c_unitedstatesgeographypeoplemt) ),
inference(nnf_transformation,[status(thm)],[f8005_neg]) ).
fof(f8005_sk,plain,
( ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)
& mtvisible(c_unitedstatesgeographypeoplemt) ),
inference(skolemisation,[status(esa)],[f8005_nnf]) ).
cnf(c8006,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(cnf_transformation,[status(esa)],[f8005_sk]) ).
cnf(hi8006,negated_conjecture,
ifeq(disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c8006]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi8006,h4010]) ).
cnf(t347,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f219,axiom,
! [OBJ] :
~ ( setorcollection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_220) ).
fof(f219_nnf,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(nnf_transformation,[status(thm)],[f219]) ).
fof(f219_sk,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(skolemisation,[status(esa)],[f219_nnf]) ).
cnf(c219,plain,
( ~ setorcollection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
fof(f493,axiom,
! [OBJ] :
~ ( setorcollection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_494) ).
fof(f493_nnf,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(nnf_transformation,[status(thm)],[f493]) ).
fof(f493_sk,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(skolemisation,[status(esa)],[f493_nnf]) ).
cnf(c493,plain,
( ~ setorcollection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[status(esa)],[f493_sk]) ).
fof(f847,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_848) ).
fof(f847_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f847]) ).
fof(f847_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f847_nnf]) ).
cnf(c847,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f847_sk]) ).
fof(f1248,axiom,
! [OBJ] :
~ ( tptpcol_1_65536(OBJ)
& tptpcol_1_1(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1249) ).
fof(f1248_nnf,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(nnf_transformation,[status(thm)],[f1248]) ).
fof(f1248_sk,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(skolemisation,[status(esa)],[f1248_nnf]) ).
cnf(c1248,plain,
( ~ tptpcol_1_65536(X0)
| ~ tptpcol_1_1(X0) ),
inference(cnf_transformation,[status(esa)],[f1248_sk]) ).
fof(f1270,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& intangible(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1271) ).
fof(f1270_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(nnf_transformation,[status(thm)],[f1270]) ).
fof(f1270_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(skolemisation,[status(esa)],[f1270_nnf]) ).
cnf(c1270,plain,
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[status(esa)],[f1270_sk]) ).
fof(f1603,axiom,
~ spatiallydisjointobjecttype(c_vulnerabletoactivitymonitoring),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1604) ).
fof(f1603_nnf,plain,
~ spatiallydisjointobjecttype(c_vulnerabletoactivitymonitoring),
inference(nnf_transformation,[status(thm)],[f1603]) ).
fof(f1603_sk,plain,
~ spatiallydisjointobjecttype(c_vulnerabletoactivitymonitoring),
inference(skolemisation,[status(esa)],[f1603_nnf]) ).
cnf(c1603,plain,
~ spatiallydisjointobjecttype(c_vulnerabletoactivitymonitoring),
inference(cnf_transformation,[status(esa)],[f1603_sk]) ).
fof(f1744,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& intangible(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1745) ).
fof(f1744_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(nnf_transformation,[status(thm)],[f1744]) ).
fof(f1744_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(skolemisation,[status(esa)],[f1744_nnf]) ).
cnf(c1744,plain,
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[status(esa)],[f1744_sk]) ).
fof(f1802,axiom,
! [OBJ] :
~ ( tptpcol_1_65536(OBJ)
& tptpcol_1_1(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1803) ).
fof(f1802_nnf,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(nnf_transformation,[status(thm)],[f1802]) ).
fof(f1802_sk,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(skolemisation,[status(esa)],[f1802_nnf]) ).
cnf(c1802,plain,
( ~ tptpcol_1_65536(X0)
| ~ tptpcol_1_1(X0) ),
inference(cnf_transformation,[status(esa)],[f1802_sk]) ).
fof(f2128,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2129) ).
fof(f2128_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f2128]) ).
fof(f2128_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f2128_nnf]) ).
cnf(c2128,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2128_sk]) ).
fof(f2345,axiom,
! [OBJ] :
~ ( tptpcol_3_114688(OBJ)
& tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2346) ).
fof(f2345_nnf,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(nnf_transformation,[status(thm)],[f2345]) ).
fof(f2345_sk,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(skolemisation,[status(esa)],[f2345_nnf]) ).
cnf(c2345,plain,
( ~ tptpcol_3_114688(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(esa)],[f2345_sk]) ).
fof(f2497,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& waitinglist(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2498) ).
fof(f2497_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ waitinglist(OBJ) ),
inference(nnf_transformation,[status(thm)],[f2497]) ).
fof(f2497_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ waitinglist(OBJ) ),
inference(skolemisation,[status(esa)],[f2497_nnf]) ).
cnf(c2497,plain,
( ~ partiallytangible(X0)
| ~ waitinglist(X0) ),
inference(cnf_transformation,[status(esa)],[f2497_sk]) ).
fof(f2791,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& thermalenergy(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2792) ).
fof(f2791_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ thermalenergy(OBJ) ),
inference(nnf_transformation,[status(thm)],[f2791]) ).
fof(f2791_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ thermalenergy(OBJ) ),
inference(skolemisation,[status(esa)],[f2791_nnf]) ).
cnf(c2791,plain,
( ~ partiallytangible(X0)
| ~ thermalenergy(X0) ),
inference(cnf_transformation,[status(esa)],[f2791_sk]) ).
fof(f3088,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3089) ).
fof(f3088_nnf,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f3088]) ).
fof(f3088_sk,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(skolemisation,[status(esa)],[f3088_nnf]) ).
cnf(c3088,plain,
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f3088_sk]) ).
fof(f3225,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3226) ).
fof(f3225_nnf,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f3225]) ).
fof(f3225_sk,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(skolemisation,[status(esa)],[f3225_nnf]) ).
cnf(c3225,plain,
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f3225_sk]) ).
fof(f3853,axiom,
! [OBJ] :
~ ( tptpcol_3_114688(OBJ)
& tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3854) ).
fof(f3853_nnf,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(nnf_transformation,[status(thm)],[f3853]) ).
fof(f3853_sk,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(skolemisation,[status(esa)],[f3853_nnf]) ).
cnf(c3853,plain,
( ~ tptpcol_3_114688(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(esa)],[f3853_sk]) ).
fof(f4278,axiom,
! [OBJ] :
~ ( set_mathematical(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4279) ).
fof(f4278_nnf,plain,
! [OBJ] :
( ~ set_mathematical(OBJ)
| ~ collection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f4278]) ).
fof(f4278_sk,plain,
! [OBJ] :
( ~ set_mathematical(OBJ)
| ~ collection(OBJ) ),
inference(skolemisation,[status(esa)],[f4278_nnf]) ).
cnf(c4278,plain,
( ~ set_mathematical(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f4278_sk]) ).
fof(f4518,axiom,
! [X,Y] :
~ ( temporaryparts(Y,X)
& temporaryparts(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4519) ).
fof(f4518_nnf,plain,
! [X,Y] :
( ~ temporaryparts(Y,X)
| ~ temporaryparts(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4518]) ).
fof(f4518_sk,plain,
! [X,Y] :
( ~ temporaryparts(Y,X)
| ~ temporaryparts(X,Y) ),
inference(skolemisation,[status(esa)],[f4518_nnf]) ).
cnf(c4518,plain,
( ~ temporaryparts(X1,X0)
| ~ temporaryparts(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4518_sk]) ).
fof(f4519,axiom,
! [X] : ~ temporaryparts(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4520) ).
fof(f4519_nnf,plain,
! [X] : ~ temporaryparts(X,X),
inference(nnf_transformation,[status(thm)],[f4519]) ).
fof(f4519_sk,plain,
! [X] : ~ temporaryparts(X,X),
inference(skolemisation,[status(esa)],[f4519_nnf]) ).
cnf(c4519,plain,
~ temporaryparts(X0,X0),
inference(cnf_transformation,[status(esa)],[f4519_sk]) ).
fof(f4584,axiom,
! [X,Y] :
~ ( along_underspecifiedpath(Y,X)
& along_underspecifiedpath(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4585) ).
fof(f4584_nnf,plain,
! [X,Y] :
( ~ along_underspecifiedpath(Y,X)
| ~ along_underspecifiedpath(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4584]) ).
fof(f4584_sk,plain,
! [X,Y] :
( ~ along_underspecifiedpath(Y,X)
| ~ along_underspecifiedpath(X,Y) ),
inference(skolemisation,[status(esa)],[f4584_nnf]) ).
cnf(c4584,plain,
( ~ along_underspecifiedpath(X1,X0)
| ~ along_underspecifiedpath(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4584_sk]) ).
fof(f4585,axiom,
! [X] : ~ along_underspecifiedpath(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4586) ).
fof(f4585_nnf,plain,
! [X] : ~ along_underspecifiedpath(X,X),
inference(nnf_transformation,[status(thm)],[f4585]) ).
fof(f4585_sk,plain,
! [X] : ~ along_underspecifiedpath(X,X),
inference(skolemisation,[status(esa)],[f4585_nnf]) ).
cnf(c4585,plain,
~ along_underspecifiedpath(X0,X0),
inference(cnf_transformation,[status(esa)],[f4585_sk]) ).
fof(f4597,axiom,
! [X,Y] :
~ ( typicallycomparestowrtslotfnlessthanbasicprice(Y,X)
& typicallycomparestowrtslotfnlessthanbasicprice(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4598) ).
fof(f4597_nnf,plain,
! [X,Y] :
( ~ typicallycomparestowrtslotfnlessthanbasicprice(Y,X)
| ~ typicallycomparestowrtslotfnlessthanbasicprice(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4597]) ).
fof(f4597_sk,plain,
! [X,Y] :
( ~ typicallycomparestowrtslotfnlessthanbasicprice(Y,X)
| ~ typicallycomparestowrtslotfnlessthanbasicprice(X,Y) ),
inference(skolemisation,[status(esa)],[f4597_nnf]) ).
cnf(c4597,plain,
( ~ typicallycomparestowrtslotfnlessthanbasicprice(X1,X0)
| ~ typicallycomparestowrtslotfnlessthanbasicprice(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4597_sk]) ).
fof(f4598,axiom,
! [X] : ~ typicallycomparestowrtslotfnlessthanbasicprice(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4599) ).
fof(f4598_nnf,plain,
! [X] : ~ typicallycomparestowrtslotfnlessthanbasicprice(X,X),
inference(nnf_transformation,[status(thm)],[f4598]) ).
fof(f4598_sk,plain,
! [X] : ~ typicallycomparestowrtslotfnlessthanbasicprice(X,X),
inference(skolemisation,[status(esa)],[f4598_nnf]) ).
cnf(c4598,plain,
~ typicallycomparestowrtslotfnlessthanbasicprice(X0,X0),
inference(cnf_transformation,[status(esa)],[f4598_sk]) ).
fof(f4626,axiom,
! [X,Y] :
~ ( properphysicalparts(Y,X)
& properphysicalparts(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4627) ).
fof(f4626_nnf,plain,
! [X,Y] :
( ~ properphysicalparts(Y,X)
| ~ properphysicalparts(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4626]) ).
fof(f4626_sk,plain,
! [X,Y] :
( ~ properphysicalparts(Y,X)
| ~ properphysicalparts(X,Y) ),
inference(skolemisation,[status(esa)],[f4626_nnf]) ).
cnf(c4626,plain,
( ~ properphysicalparts(X1,X0)
| ~ properphysicalparts(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4626_sk]) ).
fof(f4627,axiom,
! [X] : ~ properphysicalparts(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4628) ).
fof(f4627_nnf,plain,
! [X] : ~ properphysicalparts(X,X),
inference(nnf_transformation,[status(thm)],[f4627]) ).
fof(f4627_sk,plain,
! [X] : ~ properphysicalparts(X,X),
inference(skolemisation,[status(esa)],[f4627_nnf]) ).
cnf(c4627,plain,
~ properphysicalparts(X0,X0),
inference(cnf_transformation,[status(esa)],[f4627_sk]) ).
fof(f4677,axiom,
! [X,Y] :
~ ( northof(Y,X)
& northof(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4678) ).
fof(f4677_nnf,plain,
! [X,Y] :
( ~ northof(Y,X)
| ~ northof(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4677]) ).
fof(f4677_sk,plain,
! [X,Y] :
( ~ northof(Y,X)
| ~ northof(X,Y) ),
inference(skolemisation,[status(esa)],[f4677_nnf]) ).
cnf(c4677,plain,
( ~ northof(X1,X0)
| ~ northof(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4677_sk]) ).
fof(f4678,axiom,
! [X] : ~ northof(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4679) ).
fof(f4678_nnf,plain,
! [X] : ~ northof(X,X),
inference(nnf_transformation,[status(thm)],[f4678]) ).
fof(f4678_sk,plain,
! [X] : ~ northof(X,X),
inference(skolemisation,[status(esa)],[f4678_nnf]) ).
cnf(c4678,plain,
~ northof(X0,X0),
inference(cnf_transformation,[status(esa)],[f4678_sk]) ).
fof(f4837,axiom,
! [X,Y] :
~ ( temporallyfinishedby(Y,X)
& temporallyfinishedby(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4838) ).
fof(f4837_nnf,plain,
! [X,Y] :
( ~ temporallyfinishedby(Y,X)
| ~ temporallyfinishedby(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4837]) ).
fof(f4837_sk,plain,
! [X,Y] :
( ~ temporallyfinishedby(Y,X)
| ~ temporallyfinishedby(X,Y) ),
inference(skolemisation,[status(esa)],[f4837_nnf]) ).
cnf(c4837,plain,
( ~ temporallyfinishedby(X1,X0)
| ~ temporallyfinishedby(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4837_sk]) ).
fof(f4838,axiom,
! [X] : ~ temporallyfinishedby(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4839) ).
fof(f4838_nnf,plain,
! [X] : ~ temporallyfinishedby(X,X),
inference(nnf_transformation,[status(thm)],[f4838]) ).
fof(f4838_sk,plain,
! [X] : ~ temporallyfinishedby(X,X),
inference(skolemisation,[status(esa)],[f4838_nnf]) ).
cnf(c4838,plain,
~ temporallyfinishedby(X0,X0),
inference(cnf_transformation,[status(esa)],[f4838_sk]) ).
fof(f4928,axiom,
! [X,Y] :
~ ( for_underspecifiedlocation(Y,X)
& for_underspecifiedlocation(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4929) ).
fof(f4928_nnf,plain,
! [X,Y] :
( ~ for_underspecifiedlocation(Y,X)
| ~ for_underspecifiedlocation(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4928]) ).
fof(f4928_sk,plain,
! [X,Y] :
( ~ for_underspecifiedlocation(Y,X)
| ~ for_underspecifiedlocation(X,Y) ),
inference(skolemisation,[status(esa)],[f4928_nnf]) ).
cnf(c4928,plain,
( ~ for_underspecifiedlocation(X1,X0)
| ~ for_underspecifiedlocation(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4928_sk]) ).
fof(f4929,axiom,
! [X] : ~ for_underspecifiedlocation(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4930) ).
fof(f4929_nnf,plain,
! [X] : ~ for_underspecifiedlocation(X,X),
inference(nnf_transformation,[status(thm)],[f4929]) ).
fof(f4929_sk,plain,
! [X] : ~ for_underspecifiedlocation(X,X),
inference(skolemisation,[status(esa)],[f4929_nnf]) ).
cnf(c4929,plain,
~ for_underspecifiedlocation(X0,X0),
inference(cnf_transformation,[status(esa)],[f4929_sk]) ).
fof(f4989,axiom,
! [X,Y] :
~ ( spatiallycontains(Y,X)
& spatiallycontains(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4990) ).
fof(f4989_nnf,plain,
! [X,Y] :
( ~ spatiallycontains(Y,X)
| ~ spatiallycontains(X,Y) ),
inference(nnf_transformation,[status(thm)],[f4989]) ).
fof(f4989_sk,plain,
! [X,Y] :
( ~ spatiallycontains(Y,X)
| ~ spatiallycontains(X,Y) ),
inference(skolemisation,[status(esa)],[f4989_nnf]) ).
cnf(c4989,plain,
( ~ spatiallycontains(X1,X0)
| ~ spatiallycontains(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4989_sk]) ).
fof(f4990,axiom,
! [X] : ~ spatiallycontains(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4991) ).
fof(f4990_nnf,plain,
! [X] : ~ spatiallycontains(X,X),
inference(nnf_transformation,[status(thm)],[f4990]) ).
fof(f4990_sk,plain,
! [X] : ~ spatiallycontains(X,X),
inference(skolemisation,[status(esa)],[f4990_nnf]) ).
cnf(c4990,plain,
~ spatiallycontains(X0,X0),
inference(cnf_transformation,[status(esa)],[f4990_sk]) ).
fof(f5004,axiom,
! [X,Y] :
~ ( permanentlynorthwestof(Y,X)
& permanentlynorthwestof(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5005) ).
fof(f5004_nnf,plain,
! [X,Y] :
( ~ permanentlynorthwestof(Y,X)
| ~ permanentlynorthwestof(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5004]) ).
fof(f5004_sk,plain,
! [X,Y] :
( ~ permanentlynorthwestof(Y,X)
| ~ permanentlynorthwestof(X,Y) ),
inference(skolemisation,[status(esa)],[f5004_nnf]) ).
cnf(c5004,plain,
( ~ permanentlynorthwestof(X1,X0)
| ~ permanentlynorthwestof(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5004_sk]) ).
fof(f5005,axiom,
! [X] : ~ permanentlynorthwestof(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5006) ).
fof(f5005_nnf,plain,
! [X] : ~ permanentlynorthwestof(X,X),
inference(nnf_transformation,[status(thm)],[f5005]) ).
fof(f5005_sk,plain,
! [X] : ~ permanentlynorthwestof(X,X),
inference(skolemisation,[status(esa)],[f5005_nnf]) ).
cnf(c5005,plain,
~ permanentlynorthwestof(X0,X0),
inference(cnf_transformation,[status(esa)],[f5005_sk]) ).
fof(f5122,axiom,
! [X,Y] :
~ ( suborgs_materialsupport(Y,X)
& suborgs_materialsupport(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5123) ).
fof(f5122_nnf,plain,
! [X,Y] :
( ~ suborgs_materialsupport(Y,X)
| ~ suborgs_materialsupport(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5122]) ).
fof(f5122_sk,plain,
! [X,Y] :
( ~ suborgs_materialsupport(Y,X)
| ~ suborgs_materialsupport(X,Y) ),
inference(skolemisation,[status(esa)],[f5122_nnf]) ).
cnf(c5122,plain,
( ~ suborgs_materialsupport(X1,X0)
| ~ suborgs_materialsupport(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5122_sk]) ).
fof(f5123,axiom,
! [X] : ~ suborgs_materialsupport(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5124) ).
fof(f5123_nnf,plain,
! [X] : ~ suborgs_materialsupport(X,X),
inference(nnf_transformation,[status(thm)],[f5123]) ).
fof(f5123_sk,plain,
! [X] : ~ suborgs_materialsupport(X,X),
inference(skolemisation,[status(esa)],[f5123_nnf]) ).
cnf(c5123,plain,
~ suborgs_materialsupport(X0,X0),
inference(cnf_transformation,[status(esa)],[f5123_sk]) ).
fof(f5282,axiom,
! [X,Y] :
~ ( contiguousafter_tempstage(Y,X)
& contiguousafter_tempstage(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5283) ).
fof(f5282_nnf,plain,
! [X,Y] :
( ~ contiguousafter_tempstage(Y,X)
| ~ contiguousafter_tempstage(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5282]) ).
fof(f5282_sk,plain,
! [X,Y] :
( ~ contiguousafter_tempstage(Y,X)
| ~ contiguousafter_tempstage(X,Y) ),
inference(skolemisation,[status(esa)],[f5282_nnf]) ).
cnf(c5282,plain,
( ~ contiguousafter_tempstage(X1,X0)
| ~ contiguousafter_tempstage(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5282_sk]) ).
fof(f5283,axiom,
! [X] : ~ contiguousafter_tempstage(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5284) ).
fof(f5283_nnf,plain,
! [X] : ~ contiguousafter_tempstage(X,X),
inference(nnf_transformation,[status(thm)],[f5283]) ).
fof(f5283_sk,plain,
! [X] : ~ contiguousafter_tempstage(X,X),
inference(skolemisation,[status(esa)],[f5283_nnf]) ).
cnf(c5283,plain,
~ contiguousafter_tempstage(X0,X0),
inference(cnf_transformation,[status(esa)],[f5283_sk]) ).
fof(f5336,axiom,
! [X,Y] :
~ ( negligiblewrt(Y,X)
& negligiblewrt(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5337) ).
fof(f5336_nnf,plain,
! [X,Y] :
( ~ negligiblewrt(Y,X)
| ~ negligiblewrt(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5336]) ).
fof(f5336_sk,plain,
! [X,Y] :
( ~ negligiblewrt(Y,X)
| ~ negligiblewrt(X,Y) ),
inference(skolemisation,[status(esa)],[f5336_nnf]) ).
cnf(c5336,plain,
( ~ negligiblewrt(X1,X0)
| ~ negligiblewrt(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5336_sk]) ).
fof(f5337,axiom,
! [X] : ~ negligiblewrt(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5338) ).
fof(f5337_nnf,plain,
! [X] : ~ negligiblewrt(X,X),
inference(nnf_transformation,[status(thm)],[f5337]) ).
fof(f5337_sk,plain,
! [X] : ~ negligiblewrt(X,X),
inference(skolemisation,[status(esa)],[f5337_nnf]) ).
cnf(c5337,plain,
~ negligiblewrt(X0,X0),
inference(cnf_transformation,[status(esa)],[f5337_sk]) ).
fof(f5369,axiom,
! [X,Y] :
~ ( under_underspecifiedlocation(Y,X)
& under_underspecifiedlocation(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5370) ).
fof(f5369_nnf,plain,
! [X,Y] :
( ~ under_underspecifiedlocation(Y,X)
| ~ under_underspecifiedlocation(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5369]) ).
fof(f5369_sk,plain,
! [X,Y] :
( ~ under_underspecifiedlocation(Y,X)
| ~ under_underspecifiedlocation(X,Y) ),
inference(skolemisation,[status(esa)],[f5369_nnf]) ).
cnf(c5369,plain,
( ~ under_underspecifiedlocation(X1,X0)
| ~ under_underspecifiedlocation(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5369_sk]) ).
fof(f5370,axiom,
! [X] : ~ under_underspecifiedlocation(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5371) ).
fof(f5370_nnf,plain,
! [X] : ~ under_underspecifiedlocation(X,X),
inference(nnf_transformation,[status(thm)],[f5370]) ).
fof(f5370_sk,plain,
! [X] : ~ under_underspecifiedlocation(X,X),
inference(skolemisation,[status(esa)],[f5370_nnf]) ).
cnf(c5370,plain,
~ under_underspecifiedlocation(X0,X0),
inference(cnf_transformation,[status(esa)],[f5370_sk]) ).
fof(f5422,axiom,
! [X,Y] :
~ ( lessthan(Y,X)
& lessthan(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5423) ).
fof(f5422_nnf,plain,
! [X,Y] :
( ~ lessthan(Y,X)
| ~ lessthan(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5422]) ).
fof(f5422_sk,plain,
! [X,Y] :
( ~ lessthan(Y,X)
| ~ lessthan(X,Y) ),
inference(skolemisation,[status(esa)],[f5422_nnf]) ).
cnf(c5422,plain,
( ~ lessthan(X1,X0)
| ~ lessthan(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5422_sk]) ).
fof(f5423,axiom,
! [X] : ~ lessthan(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5424) ).
fof(f5423_nnf,plain,
! [X] : ~ lessthan(X,X),
inference(nnf_transformation,[status(thm)],[f5423]) ).
fof(f5423_sk,plain,
! [X] : ~ lessthan(X,X),
inference(skolemisation,[status(esa)],[f5423_nnf]) ).
cnf(c5423,plain,
~ lessthan(X0,X0),
inference(cnf_transformation,[status(esa)],[f5423_sk]) ).
fof(f5429,axiom,
! [X,Y] :
~ ( typicallycomparestowrtslotfnlessthanwidthofobject(Y,X)
& typicallycomparestowrtslotfnlessthanwidthofobject(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5430) ).
fof(f5429_nnf,plain,
! [X,Y] :
( ~ typicallycomparestowrtslotfnlessthanwidthofobject(Y,X)
| ~ typicallycomparestowrtslotfnlessthanwidthofobject(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5429]) ).
fof(f5429_sk,plain,
! [X,Y] :
( ~ typicallycomparestowrtslotfnlessthanwidthofobject(Y,X)
| ~ typicallycomparestowrtslotfnlessthanwidthofobject(X,Y) ),
inference(skolemisation,[status(esa)],[f5429_nnf]) ).
cnf(c5429,plain,
( ~ typicallycomparestowrtslotfnlessthanwidthofobject(X1,X0)
| ~ typicallycomparestowrtslotfnlessthanwidthofobject(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5429_sk]) ).
fof(f5430,axiom,
! [X] : ~ typicallycomparestowrtslotfnlessthanwidthofobject(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5431) ).
fof(f5430_nnf,plain,
! [X] : ~ typicallycomparestowrtslotfnlessthanwidthofobject(X,X),
inference(nnf_transformation,[status(thm)],[f5430]) ).
fof(f5430_sk,plain,
! [X] : ~ typicallycomparestowrtslotfnlessthanwidthofobject(X,X),
inference(skolemisation,[status(esa)],[f5430_nnf]) ).
cnf(c5430,plain,
~ typicallycomparestowrtslotfnlessthanwidthofobject(X0,X0),
inference(cnf_transformation,[status(esa)],[f5430_sk]) ).
fof(f5491,axiom,
! [X,Y] :
~ ( owns(Y,X)
& owns(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5492) ).
fof(f5491_nnf,plain,
! [X,Y] :
( ~ owns(Y,X)
| ~ owns(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5491]) ).
fof(f5491_sk,plain,
! [X,Y] :
( ~ owns(Y,X)
| ~ owns(X,Y) ),
inference(skolemisation,[status(esa)],[f5491_nnf]) ).
cnf(c5491,plain,
( ~ owns(X1,X0)
| ~ owns(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5491_sk]) ).
fof(f5492,axiom,
! [X] : ~ owns(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5493) ).
fof(f5492_nnf,plain,
! [X] : ~ owns(X,X),
inference(nnf_transformation,[status(thm)],[f5492]) ).
fof(f5492_sk,plain,
! [X] : ~ owns(X,X),
inference(skolemisation,[status(esa)],[f5492_nnf]) ).
cnf(c5492,plain,
~ owns(X0,X0),
inference(cnf_transformation,[status(esa)],[f5492_sk]) ).
fof(f5699,axiom,
! [X,Y] :
~ ( formofcondition(Y,X)
& formofcondition(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5700) ).
fof(f5699_nnf,plain,
! [X,Y] :
( ~ formofcondition(Y,X)
| ~ formofcondition(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5699]) ).
fof(f5699_sk,plain,
! [X,Y] :
( ~ formofcondition(Y,X)
| ~ formofcondition(X,Y) ),
inference(skolemisation,[status(esa)],[f5699_nnf]) ).
cnf(c5699,plain,
( ~ formofcondition(X1,X0)
| ~ formofcondition(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5699_sk]) ).
fof(f5700,axiom,
! [X] : ~ formofcondition(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5701) ).
fof(f5700_nnf,plain,
! [X] : ~ formofcondition(X,X),
inference(nnf_transformation,[status(thm)],[f5700]) ).
fof(f5700_sk,plain,
! [X] : ~ formofcondition(X,X),
inference(skolemisation,[status(esa)],[f5700_nnf]) ).
cnf(c5700,plain,
~ formofcondition(X0,X0),
inference(cnf_transformation,[status(esa)],[f5700_sk]) ).
fof(f5740,axiom,
! [X,Y] :
~ ( uniquepropersubsituationtypes(Y,X)
& uniquepropersubsituationtypes(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5741) ).
fof(f5740_nnf,plain,
! [X,Y] :
( ~ uniquepropersubsituationtypes(Y,X)
| ~ uniquepropersubsituationtypes(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5740]) ).
fof(f5740_sk,plain,
! [X,Y] :
( ~ uniquepropersubsituationtypes(Y,X)
| ~ uniquepropersubsituationtypes(X,Y) ),
inference(skolemisation,[status(esa)],[f5740_nnf]) ).
cnf(c5740,plain,
( ~ uniquepropersubsituationtypes(X1,X0)
| ~ uniquepropersubsituationtypes(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5740_sk]) ).
fof(f5741,axiom,
! [X] : ~ uniquepropersubsituationtypes(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5742) ).
fof(f5741_nnf,plain,
! [X] : ~ uniquepropersubsituationtypes(X,X),
inference(nnf_transformation,[status(thm)],[f5741]) ).
fof(f5741_sk,plain,
! [X] : ~ uniquepropersubsituationtypes(X,X),
inference(skolemisation,[status(esa)],[f5741_nnf]) ).
cnf(c5741,plain,
~ uniquepropersubsituationtypes(X0,X0),
inference(cnf_transformation,[status(esa)],[f5741_sk]) ).
fof(f5830,axiom,
! [X,Y] :
~ ( after(Y,X)
& after(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5831) ).
fof(f5830_nnf,plain,
! [X,Y] :
( ~ after(Y,X)
| ~ after(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5830]) ).
fof(f5830_sk,plain,
! [X,Y] :
( ~ after(Y,X)
| ~ after(X,Y) ),
inference(skolemisation,[status(esa)],[f5830_nnf]) ).
cnf(c5830,plain,
( ~ after(X1,X0)
| ~ after(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5830_sk]) ).
fof(f5831,axiom,
! [X] : ~ after(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5832) ).
fof(f5831_nnf,plain,
! [X] : ~ after(X,X),
inference(nnf_transformation,[status(thm)],[f5831]) ).
fof(f5831_sk,plain,
! [X] : ~ after(X,X),
inference(skolemisation,[status(esa)],[f5831_nnf]) ).
cnf(c5831,plain,
~ after(X0,X0),
inference(cnf_transformation,[status(esa)],[f5831_sk]) ).
fof(f5904,axiom,
! [X,Y] :
~ ( properpartofspaceregion_inverse(Y,X)
& properpartofspaceregion_inverse(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5905) ).
fof(f5904_nnf,plain,
! [X,Y] :
( ~ properpartofspaceregion_inverse(Y,X)
| ~ properpartofspaceregion_inverse(X,Y) ),
inference(nnf_transformation,[status(thm)],[f5904]) ).
fof(f5904_sk,plain,
! [X,Y] :
( ~ properpartofspaceregion_inverse(Y,X)
| ~ properpartofspaceregion_inverse(X,Y) ),
inference(skolemisation,[status(esa)],[f5904_nnf]) ).
cnf(c5904,plain,
( ~ properpartofspaceregion_inverse(X1,X0)
| ~ properpartofspaceregion_inverse(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5904_sk]) ).
fof(f5905,axiom,
! [X] : ~ properpartofspaceregion_inverse(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_5906) ).
fof(f5905_nnf,plain,
! [X] : ~ properpartofspaceregion_inverse(X,X),
inference(nnf_transformation,[status(thm)],[f5905]) ).
fof(f5905_sk,plain,
! [X] : ~ properpartofspaceregion_inverse(X,X),
inference(skolemisation,[status(esa)],[f5905_nnf]) ).
cnf(c5905,plain,
~ properpartofspaceregion_inverse(X0,X0),
inference(cnf_transformation,[status(esa)],[f5905_sk]) ).
fof(f6011,axiom,
! [X,Y] :
~ ( westof(Y,X)
& westof(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6012) ).
fof(f6011_nnf,plain,
! [X,Y] :
( ~ westof(Y,X)
| ~ westof(X,Y) ),
inference(nnf_transformation,[status(thm)],[f6011]) ).
fof(f6011_sk,plain,
! [X,Y] :
( ~ westof(Y,X)
| ~ westof(X,Y) ),
inference(skolemisation,[status(esa)],[f6011_nnf]) ).
cnf(c6011,plain,
( ~ westof(X1,X0)
| ~ westof(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6011_sk]) ).
fof(f6012,axiom,
! [X] : ~ westof(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6013) ).
fof(f6012_nnf,plain,
! [X] : ~ westof(X,X),
inference(nnf_transformation,[status(thm)],[f6012]) ).
fof(f6012_sk,plain,
! [X] : ~ westof(X,X),
inference(skolemisation,[status(esa)],[f6012_nnf]) ).
cnf(c6012,plain,
~ westof(X0,X0),
inference(cnf_transformation,[status(esa)],[f6012_sk]) ).
fof(f6285,axiom,
! [X,Y] :
~ ( physicallycontains(Y,X)
& physicallycontains(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6286) ).
fof(f6285_nnf,plain,
! [X,Y] :
( ~ physicallycontains(Y,X)
| ~ physicallycontains(X,Y) ),
inference(nnf_transformation,[status(thm)],[f6285]) ).
fof(f6285_sk,plain,
! [X,Y] :
( ~ physicallycontains(Y,X)
| ~ physicallycontains(X,Y) ),
inference(skolemisation,[status(esa)],[f6285_nnf]) ).
cnf(c6285,plain,
( ~ physicallycontains(X1,X0)
| ~ physicallycontains(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6285_sk]) ).
fof(f6286,axiom,
! [X] : ~ physicallycontains(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6287) ).
fof(f6286_nnf,plain,
! [X] : ~ physicallycontains(X,X),
inference(nnf_transformation,[status(thm)],[f6286]) ).
fof(f6286_sk,plain,
! [X] : ~ physicallycontains(X,X),
inference(skolemisation,[status(esa)],[f6286_nnf]) ).
cnf(c6286,plain,
~ physicallycontains(X0,X0),
inference(cnf_transformation,[status(esa)],[f6286_sk]) ).
fof(f6438,axiom,
! [X] : ~ sisters(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6439) ).
fof(f6438_nnf,plain,
! [X] : ~ sisters(X,X),
inference(nnf_transformation,[status(thm)],[f6438]) ).
fof(f6438_sk,plain,
! [X] : ~ sisters(X,X),
inference(skolemisation,[status(esa)],[f6438_nnf]) ).
cnf(c6438,plain,
~ sisters(X0,X0),
inference(cnf_transformation,[status(esa)],[f6438_sk]) ).
fof(f6547,axiom,
! [X,Y] :
~ ( outof_underspecifiedcontainer(Y,X)
& outof_underspecifiedcontainer(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6548) ).
fof(f6547_nnf,plain,
! [X,Y] :
( ~ outof_underspecifiedcontainer(Y,X)
| ~ outof_underspecifiedcontainer(X,Y) ),
inference(nnf_transformation,[status(thm)],[f6547]) ).
fof(f6547_sk,plain,
! [X,Y] :
( ~ outof_underspecifiedcontainer(Y,X)
| ~ outof_underspecifiedcontainer(X,Y) ),
inference(skolemisation,[status(esa)],[f6547_nnf]) ).
cnf(c6547,plain,
( ~ outof_underspecifiedcontainer(X1,X0)
| ~ outof_underspecifiedcontainer(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6547_sk]) ).
fof(f6548,axiom,
! [X] : ~ outof_underspecifiedcontainer(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6549) ).
fof(f6548_nnf,plain,
! [X] : ~ outof_underspecifiedcontainer(X,X),
inference(nnf_transformation,[status(thm)],[f6548]) ).
fof(f6548_sk,plain,
! [X] : ~ outof_underspecifiedcontainer(X,X),
inference(skolemisation,[status(esa)],[f6548_nnf]) ).
cnf(c6548,plain,
~ outof_underspecifiedcontainer(X0,X0),
inference(cnf_transformation,[status(esa)],[f6548_sk]) ).
fof(f6627,axiom,
! [X,Y] :
~ ( allnegligiblewrt(Y,X)
& allnegligiblewrt(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6628) ).
fof(f6627_nnf,plain,
! [X,Y] :
( ~ allnegligiblewrt(Y,X)
| ~ allnegligiblewrt(X,Y) ),
inference(nnf_transformation,[status(thm)],[f6627]) ).
fof(f6627_sk,plain,
! [X,Y] :
( ~ allnegligiblewrt(Y,X)
| ~ allnegligiblewrt(X,Y) ),
inference(skolemisation,[status(esa)],[f6627_nnf]) ).
cnf(c6627,plain,
( ~ allnegligiblewrt(X1,X0)
| ~ allnegligiblewrt(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6627_sk]) ).
fof(f6628,axiom,
! [X] : ~ allnegligiblewrt(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6629) ).
fof(f6628_nnf,plain,
! [X] : ~ allnegligiblewrt(X,X),
inference(nnf_transformation,[status(thm)],[f6628]) ).
fof(f6628_sk,plain,
! [X] : ~ allnegligiblewrt(X,X),
inference(skolemisation,[status(esa)],[f6628_nnf]) ).
cnf(c6628,plain,
~ allnegligiblewrt(X0,X0),
inference(cnf_transformation,[status(esa)],[f6628_sk]) ).
fof(f6642,axiom,
! [X,Y] :
~ ( properparts(Y,X)
& properparts(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6643) ).
fof(f6642_nnf,plain,
! [X,Y] :
( ~ properparts(Y,X)
| ~ properparts(X,Y) ),
inference(nnf_transformation,[status(thm)],[f6642]) ).
fof(f6642_sk,plain,
! [X,Y] :
( ~ properparts(Y,X)
| ~ properparts(X,Y) ),
inference(skolemisation,[status(esa)],[f6642_nnf]) ).
cnf(c6642,plain,
( ~ properparts(X1,X0)
| ~ properparts(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6642_sk]) ).
fof(f6643,axiom,
! [X] : ~ properparts(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_6644) ).
fof(f6643_nnf,plain,
! [X] : ~ properparts(X,X),
inference(nnf_transformation,[status(thm)],[f6643]) ).
fof(f6643_sk,plain,
! [X] : ~ properparts(X,X),
inference(skolemisation,[status(esa)],[f6643_nnf]) ).
cnf(c6643,plain,
~ properparts(X0,X0),
inference(cnf_transformation,[status(esa)],[f6643_sk]) ).
fof(f7178,axiom,
! [X] : ~ affiliatedwith(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7179) ).
fof(f7178_nnf,plain,
! [X] : ~ affiliatedwith(X,X),
inference(nnf_transformation,[status(thm)],[f7178]) ).
fof(f7178_sk,plain,
! [X] : ~ affiliatedwith(X,X),
inference(skolemisation,[status(esa)],[f7178_nnf]) ).
cnf(c7178,plain,
~ affiliatedwith(X0,X0),
inference(cnf_transformation,[status(esa)],[f7178_sk]) ).
fof(f7322,axiom,
! [X,Y] :
~ ( requisitefor(Y,X)
& requisitefor(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7323) ).
fof(f7322_nnf,plain,
! [X,Y] :
( ~ requisitefor(Y,X)
| ~ requisitefor(X,Y) ),
inference(nnf_transformation,[status(thm)],[f7322]) ).
fof(f7322_sk,plain,
! [X,Y] :
( ~ requisitefor(Y,X)
| ~ requisitefor(X,Y) ),
inference(skolemisation,[status(esa)],[f7322_nnf]) ).
cnf(c7322,plain,
( ~ requisitefor(X1,X0)
| ~ requisitefor(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7322_sk]) ).
fof(f7323,axiom,
! [X] : ~ requisitefor(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7324) ).
fof(f7323_nnf,plain,
! [X] : ~ requisitefor(X,X),
inference(nnf_transformation,[status(thm)],[f7323]) ).
fof(f7323_sk,plain,
! [X] : ~ requisitefor(X,X),
inference(skolemisation,[status(esa)],[f7323_nnf]) ).
cnf(c7323,plain,
~ requisitefor(X0,X0),
inference(cnf_transformation,[status(esa)],[f7323_sk]) ).
fof(f7358,axiom,
! [X] : ~ objectfoundinlocation(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7359) ).
fof(f7358_nnf,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(nnf_transformation,[status(thm)],[f7358]) ).
fof(f7358_sk,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(skolemisation,[status(esa)],[f7358_nnf]) ).
cnf(c7358,plain,
~ objectfoundinlocation(X0,X0),
inference(cnf_transformation,[status(esa)],[f7358_sk]) ).
fof(f7642,axiom,
! [X] : ~ borderson(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7643) ).
fof(f7642_nnf,plain,
! [X] : ~ borderson(X,X),
inference(nnf_transformation,[status(thm)],[f7642]) ).
fof(f7642_sk,plain,
! [X] : ~ borderson(X,X),
inference(skolemisation,[status(esa)],[f7642_nnf]) ).
cnf(c7642,plain,
~ borderson(X0,X0),
inference(cnf_transformation,[status(esa)],[f7642_sk]) ).
fof(f7949,axiom,
! [X,Y] :
~ ( superabstractype(Y,X)
& superabstractype(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7950) ).
fof(f7949_nnf,plain,
! [X,Y] :
( ~ superabstractype(Y,X)
| ~ superabstractype(X,Y) ),
inference(nnf_transformation,[status(thm)],[f7949]) ).
fof(f7949_sk,plain,
! [X,Y] :
( ~ superabstractype(Y,X)
| ~ superabstractype(X,Y) ),
inference(skolemisation,[status(esa)],[f7949_nnf]) ).
cnf(c7949,plain,
( ~ superabstractype(X1,X0)
| ~ superabstractype(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7949_sk]) ).
fof(f7950,axiom,
! [X] : ~ superabstractype(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_7951) ).
fof(f7950_nnf,plain,
! [X] : ~ superabstractype(X,X),
inference(nnf_transformation,[status(thm)],[f7950]) ).
fof(f7950_sk,plain,
! [X] : ~ superabstractype(X,X),
inference(skolemisation,[status(esa)],[f7950_nnf]) ).
cnf(c7950,plain,
~ superabstractype(X0,X0),
inference(cnf_transformation,[status(esa)],[f7950_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c219,c493,c847,c1248,c1270,c1603,c1744,c1802,c2128,c2345,c2497,c2791,c3088,c3225,c3853,c4278,c4518,c4519,c4584,c4585,c4597,c4598,c4626,c4627,c4677,c4678,c4837,c4838,c4928,c4929,c4989,c4990,c5004,c5005,c5122,c5123,c5282,c5283,c5336,c5337,c5369,c5370,c5422,c5423,c5429,c5430,c5491,c5492,c5699,c5700,c5740,c5741,c5830,c5831,c5904,c5905,c6011,c6012,c6285,c6286,c6438,c6547,c6548,c6627,c6628,c6642,c6643,c7178,c7322,c7323,c7358,c7642,c7949,c7950,c8006]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t347]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR049+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.36 % Computer : n020.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Fri Sep 25 08:34:49 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 162.60/21.77 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 162.60/21.77 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------