%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR047+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:28 PM UTC 2026
% Result : Theorem 240.60s 35.31s
% Output : Proof 240.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 77
% Syntax : Number of formulae : 321 ( 141 unt; 0 def)
% Number of atoms : 509 ( 10 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 628 ( 440 ~; 138 |; 46 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 49 ( 47 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-4 aty)
% Number of variables : 426 ( 0 sgn 318 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1350,axiom,
( mtvisible(c_tptpgeo_member4_mt)
=> borderson(c_georegion_l4_x36_y50,c_georegion_l4_x37_y50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1351) ).
fof(f1350_nnf,plain,
( borderson(c_georegion_l4_x36_y50,c_georegion_l4_x37_y50)
| ~ mtvisible(c_tptpgeo_member4_mt) ),
inference(nnf_transformation,[status(thm)],[f1350]) ).
fof(f1350_sk,plain,
( borderson(c_georegion_l4_x36_y50,c_georegion_l4_x37_y50)
| ~ mtvisible(c_tptpgeo_member4_mt) ),
inference(skolemisation,[status(esa)],[f1350_nnf]) ).
cnf(c1350,plain,
( borderson(c_georegion_l4_x36_y50,c_georegion_l4_x37_y50)
| ~ mtvisible(c_tptpgeo_member4_mt) ),
inference(cnf_transformation,[status(esa)],[f1350_sk]) ).
cnf(hi1345,axiom,
ifeq(mtvisible(c_tptpgeo_member4_mt),true,borderson(c_georegion_l4_x36_y50,c_georegion_l4_x37_y50),true) = true,
inference(equality_encoding,[status(esa)],[c1350]) ).
fof(f8005,conjecture,
( mtvisible(c_tptpgeo_member4_mt)
=> borderson(c_georegion_l4_x37_y50,c_georegion_l4_x36_y50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query147) ).
fof(f8005_neg,negated_conjecture,
~ ( mtvisible(c_tptpgeo_member4_mt)
=> borderson(c_georegion_l4_x37_y50,c_georegion_l4_x36_y50) ),
inference(negated_conjecture,[status(cth)],[f8005]) ).
fof(f8005_nnf,plain,
( ~ borderson(c_georegion_l4_x37_y50,c_georegion_l4_x36_y50)
& mtvisible(c_tptpgeo_member4_mt) ),
inference(nnf_transformation,[status(thm)],[f8005_neg]) ).
fof(f8005_sk,plain,
( ~ borderson(c_georegion_l4_x37_y50,c_georegion_l4_x36_y50)
& mtvisible(c_tptpgeo_member4_mt) ),
inference(skolemisation,[status(esa)],[f8005_nnf]) ).
cnf(c8005,plain,
mtvisible(c_tptpgeo_member4_mt),
inference(cnf_transformation,[status(esa)],[f8005_sk]) ).
cnf(hi7931,negated_conjecture,
mtvisible(c_tptpgeo_member4_mt) = true,
inference(equality_encoding,[status(esa)],[c8005]) ).
cnf(h0,plain,
borderson(c_georegion_l4_x36_y50,c_georegion_l4_x37_y50) = true,
inference(hyper_resolution,[status(thm)],[hi1345,hi7931]) ).
fof(f7641,axiom,
! [X,Y] :
( borderson(X,Y)
=> borderson(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_7642) ).
fof(f7641_nnf,plain,
! [X,Y] :
( borderson(Y,X)
| ~ borderson(X,Y) ),
inference(nnf_transformation,[status(thm)],[f7641]) ).
fof(f7641_sk,plain,
! [X,Y] :
( borderson(Y,X)
| ~ borderson(X,Y) ),
inference(skolemisation,[status(esa)],[f7641_nnf]) ).
cnf(c7641,plain,
( borderson(X1,X0)
| ~ borderson(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7641_sk]) ).
cnf(hi7570,axiom,
ifeq(borderson(X0,X1),true,borderson(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c7641]) ).
cnf(h57,plain,
borderson(c_georegion_l4_x37_y50,c_georegion_l4_x36_y50) = true,
inference(hyper_resolution,[status(thm)],[hi7570,h0]) ).
cnf(c8006,plain,
~ borderson(c_georegion_l4_x37_y50,c_georegion_l4_x36_y50),
inference(cnf_transformation,[status(esa)],[f8005_sk]) ).
cnf(hi8006,negated_conjecture,
ifeq(borderson(c_georegion_l4_x37_y50,c_georegion_l4_x36_y50),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c8006]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi8006,h57]) ).
cnf(t195,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f219,axiom,
! [OBJ] :
~ ( setorcollection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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,t195]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR047+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 08:33:07 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 240.60/35.31 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 240.60/35.31 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------