%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR061+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 : n003.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:37 PM UTC 2026
% Result : Theorem 246.84s 32.89s
% Output : Proof 246.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 95
% Syntax : Number of formulae : 406 ( 222 unt; 0 def)
% Number of atoms : 610 ( 41 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 : 23 ( 23 usr; 22 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(f466,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_467) ).
fof(f466_nnf,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(nnf_transformation,[status(thm)],[f466]) ).
cnf(c466,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(cnf_transformation,[status(esa)],[f466_nnf]) ).
cnf(hi465,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665) = true,
inference(equality_encoding,[status(esa)],[c466]) ).
fof(f3406,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3407) ).
fof(f3406_nnf,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(nnf_transformation,[status(thm)],[f3406]) ).
cnf(c3406,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(cnf_transformation,[status(esa)],[f3406_nnf]) ).
cnf(hi3392,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641) = true,
inference(equality_encoding,[status(esa)],[c3406]) ).
cnf(h17,plain,
genls(c_tptpcol_8_114177,c_tptpcol_6_112641) = true,
inference(hyper_resolution,[status(thm)],[hi7920,hi465,hi3392]) ).
fof(f1416,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1417) ).
fof(f1416_nnf,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(nnf_transformation,[status(thm)],[f1416]) ).
cnf(c1416,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(cnf_transformation,[status(esa)],[f1416_nnf]) ).
cnf(hi1411,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593) = true,
inference(equality_encoding,[status(esa)],[c1416]) ).
cnf(h1394,plain,
genls(c_tptpcol_8_114177,c_tptpcol_5_110593) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h17,hi1411]) ).
fof(f4157,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_4158) ).
fof(f4157_nnf,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(nnf_transformation,[status(thm)],[f4157]) ).
cnf(c4157,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(cnf_transformation,[status(esa)],[f4157_nnf]) ).
cnf(hi4142,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497) = true,
inference(equality_encoding,[status(esa)],[c4157]) ).
cnf(h4577,plain,
genls(c_tptpcol_8_114177,c_tptpcol_4_106497) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1394,hi4142]) ).
fof(f1311,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1312) ).
fof(f1311_nnf,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(nnf_transformation,[status(thm)],[f1311]) ).
cnf(c1311,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(cnf_transformation,[status(esa)],[f1311_nnf]) ).
cnf(hi1306,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117) = true,
inference(equality_encoding,[status(esa)],[c1311]) ).
fof(f3444,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_3445) ).
fof(f3444_nnf,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(nnf_transformation,[status(thm)],[f3444]) ).
cnf(c3444,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(cnf_transformation,[status(esa)],[f3444_nnf]) ).
cnf(hi3430,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116) = true,
inference(equality_encoding,[status(esa)],[c3444]) ).
cnf(h20,plain,
genls(c_tptpcol_14_118118,c_tptpcol_12_118116) = true,
inference(hyper_resolution,[status(thm)],[hi7920,hi1306,hi3430]) ).
fof(f1913,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1914) ).
fof(f1913_nnf,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(nnf_transformation,[status(thm)],[f1913]) ).
cnf(c1913,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(cnf_transformation,[status(esa)],[f1913_nnf]) ).
cnf(hi1905,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084) = true,
inference(equality_encoding,[status(esa)],[c1913]) ).
cnf(h1607,plain,
genls(c_tptpcol_14_118118,c_tptpcol_11_118084) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h20,hi1905]) ).
fof(f2514,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2515) ).
fof(f2514_nnf,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(nnf_transformation,[status(thm)],[f2514]) ).
cnf(c2514,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(cnf_transformation,[status(esa)],[f2514_nnf]) ).
cnf(hi2503,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020) = true,
inference(equality_encoding,[status(esa)],[c2514]) ).
cnf(h2129,plain,
genls(c_tptpcol_14_118118,c_tptpcol_10_118020) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h1607,hi2503]) ).
fof(f1452,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1453) ).
fof(f1452_nnf,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(nnf_transformation,[status(thm)],[f1452]) ).
cnf(c1452,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(cnf_transformation,[status(esa)],[f1452_nnf]) ).
cnf(hi1447,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019) = true,
inference(equality_encoding,[status(esa)],[c1452]) ).
cnf(h2141,plain,
genls(c_tptpcol_14_118118,c_tptpcol_9_118019) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h2129,hi1447]) ).
fof(f975,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_976) ).
fof(f975_nnf,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(nnf_transformation,[status(thm)],[f975]) ).
cnf(c975,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(cnf_transformation,[status(esa)],[f975_nnf]) ).
cnf(hi972,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763) = true,
inference(equality_encoding,[status(esa)],[c975]) ).
cnf(h2159,plain,
genls(c_tptpcol_14_118118,c_tptpcol_8_117763) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h2141,hi972]) ).
fof(f715,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_716) ).
fof(f715_nnf,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(nnf_transformation,[status(thm)],[f715]) ).
cnf(c715,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(cnf_transformation,[status(esa)],[f715_nnf]) ).
cnf(hi713,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762) = true,
inference(equality_encoding,[status(esa)],[c715]) ).
cnf(h2179,plain,
genls(c_tptpcol_14_118118,c_tptpcol_7_117762) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h2159,hi713]) ).
fof(f2291,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2292) ).
fof(f2291_nnf,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(nnf_transformation,[status(thm)],[f2291]) ).
cnf(c2291,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(cnf_transformation,[status(esa)],[f2291_nnf]) ).
cnf(hi2282,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738) = true,
inference(equality_encoding,[status(esa)],[c2291]) ).
cnf(h2187,plain,
genls(c_tptpcol_14_118118,c_tptpcol_6_116738) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h2179,hi2282]) ).
fof(f2340,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2341) ).
fof(f2340_nnf,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(nnf_transformation,[status(thm)],[f2340]) ).
cnf(c2340,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(cnf_transformation,[status(esa)],[f2340_nnf]) ).
cnf(hi2331,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690) = true,
inference(equality_encoding,[status(esa)],[c2340]) ).
cnf(h2190,plain,
genls(c_tptpcol_14_118118,c_tptpcol_5_114690) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h2187,hi2331]) ).
fof(f816,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_817) ).
fof(f816_nnf,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(nnf_transformation,[status(thm)],[f816]) ).
cnf(c816,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(cnf_transformation,[status(esa)],[f816_nnf]) ).
cnf(hi814,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689) = true,
inference(equality_encoding,[status(esa)],[c816]) ).
cnf(h2193,plain,
genls(c_tptpcol_14_118118,c_tptpcol_4_114689) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h2190,hi814]) ).
fof(f1322,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_1323) ).
fof(f1322_nnf,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(nnf_transformation,[status(thm)],[f1322]) ).
cnf(c1322,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(cnf_transformation,[status(esa)],[f1322_nnf]) ).
cnf(hi1317,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688) = true,
inference(equality_encoding,[status(esa)],[c1322]) ).
cnf(h2196,plain,
genls(c_tptpcol_14_118118,c_tptpcol_3_114688) = true,
inference(hyper_resolution,[status(thm)],[hi7920,h2193,hi1317]) ).
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(f2344,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2345) ).
fof(f2344_nnf,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(nnf_transformation,[status(thm)],[f2344]) ).
cnf(c2344,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(cnf_transformation,[status(esa)],[f2344_nnf]) ).
cnf(hi2335,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688) = true,
inference(equality_encoding,[status(esa)],[c2344]) ).
cnf(h2201,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_14_118118) = true,
inference(hyper_resolution,[status(thm)],[hi7513,hi2335,h2196]) ).
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(f2473,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2_2474) ).
fof(f2473_nnf,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(nnf_transformation,[status(thm)],[f2473]) ).
cnf(c2473,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(cnf_transformation,[status(esa)],[f2473_nnf]) ).
cnf(hi2463,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305) = true,
inference(equality_encoding,[status(esa)],[c2473]) ).
cnf(h2209,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_14_118118) = true,
inference(hyper_resolution,[status(thm)],[hi7514,h2201,hi2463]) ).
cnf(h4596,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) = true,
inference(hyper_resolution,[status(thm)],[hi7514,h2209,h4577]) ).
fof(f8005,conjecture,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query161) ).
fof(f8005_neg,negated_conjecture,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(negated_conjecture,[status(cth)],[f8005]) ).
fof(f8005_nnf,plain,
( ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)
& mtvisible(c_timehasnoendmt) ),
inference(nnf_transformation,[status(thm)],[f8005_neg]) ).
fof(f8005_sk,plain,
( ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)
& mtvisible(c_timehasnoendmt) ),
inference(skolemisation,[status(esa)],[f8005_nnf]) ).
cnf(c8006,plain,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(cnf_transformation,[status(esa)],[f8005_sk]) ).
cnf(hi8006,negated_conjecture,
ifeq(disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c8006]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi8006,h4596]) ).
cnf(t276,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,t276]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR061+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n003.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 08:47:53 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 246.84/32.89 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 246.84/32.89 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------