%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR036+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 : n011.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:20 PM UTC 2026
% Result : Theorem 231.39s 30.08s
% Output : Proof 231.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 108
% Syntax : Number of formulae : 471 ( 287 unt; 0 def)
% Number of atoms : 675 ( 67 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 : 36 ( 36 usr; 35 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(f1601,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1602) ).
fof(f1601_nnf,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(nnf_transformation,[status(thm)],[f1601]) ).
cnf(c1601,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[status(esa)],[f1601_nnf]) ).
cnf(hi1596,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793) = true,
inference(equality_encoding,[status(esa)],[c1601]) ).
fof(f2539,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2540) ).
fof(f2539_nnf,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(nnf_transformation,[status(thm)],[f2539]) ).
cnf(c2539,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[status(esa)],[f2539_nnf]) ).
cnf(hi2528,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792) = true,
inference(equality_encoding,[status(esa)],[c2539]) ).
cnf(h19,plain,
genls(c_tptpcol_16_72795,c_tptpcol_14_72792) = true,
inference(hyper_resolution,[status(thm)],[hi7920,hi1596,hi2528]) ).
fof(f1759,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1760) ).
fof(f1759_nnf,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(nnf_transformation,[status(thm)],[f1759]) ).
cnf(c1759,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[status(esa)],[f1759_nnf]) ).
cnf(hi1752,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791) = true,
inference(equality_encoding,[status(esa)],[c1759]) ).
cnf(h1292,plain,
genls(c_tptpcol_16_72795,c_tptpcol_13_72791) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h19,hi1752]) ).
fof(f3763,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3764) ).
fof(f3763_nnf,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(nnf_transformation,[status(thm)],[f3763]) ).
cnf(c3763,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[status(esa)],[f3763_nnf]) ).
cnf(hi3749,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775) = true,
inference(equality_encoding,[status(esa)],[c3763]) ).
cnf(h3947,plain,
genls(c_tptpcol_16_72795,c_tptpcol_12_72775) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1292,hi3749]) ).
fof(f1299,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1300) ).
fof(f1299_nnf,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(nnf_transformation,[status(thm)],[f1299]) ).
cnf(c1299,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[status(esa)],[f1299_nnf]) ).
cnf(hi1294,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072) = true,
inference(equality_encoding,[status(esa)],[c1299]) ).
fof(f1974,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1975) ).
fof(f1974_nnf,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(nnf_transformation,[status(thm)],[f1974]) ).
cnf(c1974,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[status(esa)],[f1974_nnf]) ).
cnf(hi1966,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071) = true,
inference(equality_encoding,[status(esa)],[c1974]) ).
cnf(h17,plain,
genls(c_tptpcol_15_22076,c_tptpcol_13_22071) = true,
inference(hyper_resolution,[status(thm)],[hi7920,hi1294,hi1966]) ).
fof(f1365,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1366) ).
fof(f1365_nnf,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(nnf_transformation,[status(thm)],[f1365]) ).
cnf(c1365,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[status(esa)],[f1365_nnf]) ).
cnf(hi1360,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055) = true,
inference(equality_encoding,[status(esa)],[c1365]) ).
cnf(h1101,plain,
genls(c_tptpcol_15_22076,c_tptpcol_12_22055) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h17,hi1360]) ).
fof(f878,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_879) ).
fof(f878_nnf,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(nnf_transformation,[status(thm)],[f878]) ).
cnf(c878,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[status(esa)],[f878_nnf]) ).
cnf(hi875,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023) = true,
inference(equality_encoding,[status(esa)],[c878]) ).
cnf(h1105,plain,
genls(c_tptpcol_15_22076,c_tptpcol_11_22023) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1101,hi875]) ).
fof(f1169,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1170) ).
fof(f1169_nnf,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(nnf_transformation,[status(thm)],[f1169]) ).
cnf(c1169,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[status(esa)],[f1169_nnf]) ).
cnf(hi1166,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022) = true,
inference(equality_encoding,[status(esa)],[c1169]) ).
cnf(h1108,plain,
genls(c_tptpcol_15_22076,c_tptpcol_10_22022) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1105,hi1166]) ).
fof(f69,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_70) ).
fof(f69_nnf,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(nnf_transformation,[status(thm)],[f69]) ).
cnf(c69,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[status(esa)],[f69_nnf]) ).
cnf(hi69,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021) = true,
inference(equality_encoding,[status(esa)],[c69]) ).
cnf(h1111,plain,
genls(c_tptpcol_15_22076,c_tptpcol_9_22021) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1108,hi69]) ).
fof(f1730,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1731) ).
fof(f1730_nnf,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(nnf_transformation,[status(thm)],[f1730]) ).
cnf(c1730,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[status(esa)],[f1730_nnf]) ).
cnf(hi1724,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020) = true,
inference(equality_encoding,[status(esa)],[c1730]) ).
cnf(h1284,plain,
genls(c_tptpcol_15_22076,c_tptpcol_8_22020) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1111,hi1724]) ).
fof(f335,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_336) ).
fof(f335_nnf,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(nnf_transformation,[status(thm)],[f335]) ).
cnf(c335,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[status(esa)],[f335_nnf]) ).
cnf(hi334,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508) = true,
inference(equality_encoding,[status(esa)],[c335]) ).
cnf(h1290,plain,
genls(c_tptpcol_15_22076,c_tptpcol_7_21508) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1284,hi334]) ).
fof(f2435,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2436) ).
fof(f2435_nnf,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(nnf_transformation,[status(thm)],[f2435]) ).
cnf(c2435,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[status(esa)],[f2435_nnf]) ).
cnf(hi2425,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484) = true,
inference(equality_encoding,[status(esa)],[c2435]) ).
cnf(h1750,plain,
genls(c_tptpcol_15_22076,c_tptpcol_6_20484) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1290,hi2425]) ).
fof(f792,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_793) ).
fof(f792_nnf,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(nnf_transformation,[status(thm)],[f792]) ).
cnf(c792,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[status(esa)],[f792_nnf]) ).
cnf(hi790,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483) = true,
inference(equality_encoding,[status(esa)],[c792]) ).
cnf(h1755,plain,
genls(c_tptpcol_15_22076,c_tptpcol_5_20483) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1750,hi790]) ).
fof(f1817,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1818) ).
fof(f1817_nnf,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(nnf_transformation,[status(thm)],[f1817]) ).
cnf(c1817,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[status(esa)],[f1817_nnf]) ).
cnf(hi1809,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387) = true,
inference(equality_encoding,[status(esa)],[c1817]) ).
cnf(h1758,plain,
genls(c_tptpcol_15_22076,c_tptpcol_4_16387) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1755,hi1809]) ).
fof(f782,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_783) ).
fof(f782_nnf,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(nnf_transformation,[status(thm)],[f782]) ).
cnf(c782,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[status(esa)],[f782_nnf]) ).
cnf(hi780,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386) = true,
inference(equality_encoding,[status(esa)],[c782]) ).
cnf(h1761,plain,
genls(c_tptpcol_15_22076,c_tptpcol_3_16386) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1758,hi780]) ).
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(h1764,plain,
genls(c_tptpcol_15_22076,c_tptpcol_2_2) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1761,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(h2434,plain,
genls(c_tptpcol_15_22076,c_tptpcol_1_1) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1764,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(h2446,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi7514,hi1794,h2434]) ).
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(h2470,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_2_65537) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2446,hi914]) ).
fof(f1707,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1708) ).
fof(f1707_nnf,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(nnf_transformation,[status(thm)],[f1707]) ).
cnf(c1707,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[status(esa)],[f1707_nnf]) ).
cnf(hi1701,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537) = true,
inference(equality_encoding,[status(esa)],[c1707]) ).
cnf(h2536,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_3_65538) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2470,hi1701]) ).
fof(f175,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_176) ).
fof(f175_nnf,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(nnf_transformation,[status(thm)],[f175]) ).
cnf(c175,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[status(esa)],[f175_nnf]) ).
cnf(hi175,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538) = true,
inference(equality_encoding,[status(esa)],[c175]) ).
cnf(h2640,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_4_65539) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2536,hi175]) ).
fof(f813,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_814) ).
fof(f813_nnf,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(nnf_transformation,[status(thm)],[f813]) ).
cnf(c813,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[status(esa)],[f813_nnf]) ).
cnf(hi811,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539) = true,
inference(equality_encoding,[status(esa)],[c813]) ).
cnf(h2708,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_5_69635) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2640,hi811]) ).
fof(f19,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_20) ).
fof(f19_nnf,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(hi19,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(h2775,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_6_71683) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2708,hi19]) ).
fof(f2286,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2287) ).
fof(f2286_nnf,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(nnf_transformation,[status(thm)],[f2286]) ).
cnf(c2286,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[status(esa)],[f2286_nnf]) ).
cnf(hi2277,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683) = true,
inference(equality_encoding,[status(esa)],[c2286]) ).
cnf(h2845,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_7_72707) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2775,hi2277]) ).
fof(f2141,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2142) ).
fof(f2141_nnf,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(nnf_transformation,[status(thm)],[f2141]) ).
cnf(c2141,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[status(esa)],[f2141_nnf]) ).
cnf(hi2132,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707) = true,
inference(equality_encoding,[status(esa)],[c2141]) ).
cnf(h2910,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_8_72708) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2845,hi2132]) ).
fof(f2615,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2616) ).
fof(f2615_nnf,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(nnf_transformation,[status(thm)],[f2615]) ).
cnf(c2615,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[status(esa)],[f2615_nnf]) ).
cnf(hi2604,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708) = true,
inference(equality_encoding,[status(esa)],[c2615]) ).
cnf(h2963,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_9_72709) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2910,hi2604]) ).
fof(f1938,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1939) ).
fof(f1938_nnf,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(nnf_transformation,[status(thm)],[f1938]) ).
cnf(c1938,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[status(esa)],[f1938_nnf]) ).
cnf(hi1930,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709) = true,
inference(equality_encoding,[status(esa)],[c1938]) ).
cnf(h3006,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_10_72710) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h2963,hi1930]) ).
fof(f3204,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3205) ).
fof(f3204_nnf,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(nnf_transformation,[status(thm)],[f3204]) ).
cnf(c3204,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[status(esa)],[f3204_nnf]) ).
cnf(hi3191,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710) = true,
inference(equality_encoding,[status(esa)],[c3204]) ).
cnf(h3048,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_11_72774) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h3006,hi3191]) ).
fof(f2145,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2146) ).
fof(f2145_nnf,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(nnf_transformation,[status(thm)],[f2145]) ).
cnf(c2145,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[status(esa)],[f2145_nnf]) ).
cnf(hi2136,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774) = true,
inference(equality_encoding,[status(esa)],[c2145]) ).
cnf(h3090,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_12_72775) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h3048,hi2136]) ).
cnf(h3967,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) = true,
inference(hyper_resolution,[status(thm)],[hi7513,h3090,h3947]) ).
fof(f8005,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query136) ).
fof(f8005_neg,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(negated_conjecture,[status(cth)],[f8005]) ).
fof(f8005_nnf,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(nnf_transformation,[status(thm)],[f8005_neg]) ).
fof(f8005_sk,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(skolemisation,[status(esa)],[f8005_nnf]) ).
cnf(c8006,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[status(esa)],[f8005_sk]) ).
cnf(hi8006,negated_conjecture,
ifeq(disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c8006]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi8006,h3967]) ).
cnf(t275,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,t275]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 08:20:28 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 231.39/30.08 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 231.39/30.08 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------