%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO300+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:17:50 PM UTC 2026
% Result : Theorem 61.72s 8.27s
% Output : Proof 61.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 36
% Syntax : Number of formulae : 195 ( 73 unt; 0 def)
% Number of atoms : 1259 ( 550 equ)
% Maximal formula atoms : 23 ( 6 avg)
% Number of connectives : 1919 ( 855 ~; 657 |; 382 &)
% ( 0 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 38 ( 8 avg)
% Maximal term depth : 10 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 44 ( 44 usr; 18 con; 0-6 aty)
% Number of variables : 746 ( 3 sgn 391 !; 104 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,conjecture,
vf(vd1185,vd1201) = vplus(vf(vd1185,vd1187),vf(vd1187,vd1201)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd0) ).
fof(f0_neg,negated_conjecture,
vf(vd1185,vd1201) != vplus(vf(vd1185,vd1187),vf(vd1187,vd1201)),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
vf(vd1185,vd1201) != vplus(vf(vd1185,vd1187),vf(vd1187,vd1201)),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
vf(vd1185,vd1201) != vplus(vf(vd1185,vd1187),vf(vd1187,vd1201)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
vf(vd1185,vd1201) != vplus(vf(vd1185,vd1187),vf(vd1187,vd1201)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t188,plain,
eq(vf(vd1185,vd1201),vplus(vf(vd1185,vd1187),vf(vd1187,vd1201))) = false,
inference(equality_encoding,[status(esa)],[c0]) ).
fof(f67,axiom,
! [Vd761,Vd762] :
( ( ? [Vd764] :
( rpoint(Vd764)
& Vd761 = Vd764 )
& ? [Vd765] :
( rpoint(Vd765)
& Vd762 = Vd765 ) )
=> vf(Vd761,Vd762) = vf(Vd762,Vd761) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd67) ).
fof(f67_nnf,plain,
! [Vd761,Vd762] :
( vf(Vd761,Vd762) = vf(Vd762,Vd761)
| ! [Vd764] :
( ~ rpoint(Vd764)
| Vd761 != Vd764 )
| ! [Vd765] :
( ~ rpoint(Vd765)
| Vd762 != Vd765 ) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [Vd762,Vd765,Vd761,Vd764] :
( vf(Vd761,Vd762) = vf(Vd762,Vd761)
| ~ rpoint(Vd764)
| Vd761 != Vd764
| ~ rpoint(Vd765)
| Vd762 != Vd765 ),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c108,plain,
( vf(X0,X1) = vf(X1,X0)
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2 ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(hi94,axiom,
ifeq(X0,X1,ifeq(rpoint(X1),true,ifeq(X2,X3,ifeq(rpoint(X3),true,vf(X2,X0),vf(X0,X2)),vf(X0,X2)),vf(X0,X2)),vf(X0,X2)) = vf(X0,X2),
inference(equality_encoding,[status(esa)],[c108]) ).
fof(f6,axiom,
? [Vd1205] :
( rpoint(Vd1205)
& vd1201 = Vd1205 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd6) ).
fof(f6_nnf,plain,
? [Vd1205] :
( rpoint(Vd1205)
& vd1201 = Vd1205 ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
( rpoint(sk0)
& vd1201 = sk0 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f6_nnf]) ).
cnf(c6,plain,
vd1201 = sk0,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi3,axiom,
vd1201 = sk0,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(c7,plain,
rpoint(sk0),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi4,axiom,
rpoint(sk0) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
fof(f7,axiom,
( ? [Vd1182] :
( rpoint(Vd1182)
& vd1178 = Vd1182 )
& ? [Vd1183] :
( rpoint(Vd1183)
& vd1179 = Vd1183 )
& ? [Vd1184] :
( rpoint(Vd1184)
& vd1180 = Vd1184 )
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& ? [Vd1189] :
( rpoint(Vd1189)
& vd1185 = Vd1189 )
& ? [Vd1190] :
( rpoint(Vd1190)
& vd1186 = Vd1190 )
& ? [Vd1191] :
( rpoint(Vd1191)
& vd1187 = Vd1191 )
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& ~ ? [Vd1195] :
( rline(Vd1195)
& ron(vd1185,Vd1195)
& ron(vd1186,Vd1195)
& ron(vd1187,Vd1195) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd7) ).
fof(f7_nnf,plain,
( ? [Vd1182] :
( rpoint(Vd1182)
& vd1178 = Vd1182 )
& ? [Vd1183] :
( rpoint(Vd1183)
& vd1179 = Vd1183 )
& ? [Vd1184] :
( rpoint(Vd1184)
& vd1180 = Vd1184 )
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& ? [Vd1189] :
( rpoint(Vd1189)
& vd1185 = Vd1189 )
& ? [Vd1190] :
( rpoint(Vd1190)
& vd1186 = Vd1190 )
& ? [Vd1191] :
( rpoint(Vd1191)
& vd1187 = Vd1191 )
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& ! [Vd1195] :
( ~ rline(Vd1195)
| ~ ron(vd1185,Vd1195)
| ~ ron(vd1186,Vd1195)
| ~ ron(vd1187,Vd1195) ) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [Vd1195] :
( rpoint(sk6)
& vd1178 = sk6
& rpoint(sk5)
& vd1179 = sk5
& rpoint(sk4)
& vd1180 = sk4
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& rpoint(sk3)
& vd1185 = sk3
& rpoint(sk2)
& vd1186 = sk2
& rpoint(sk1)
& vd1187 = sk1
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& ( ~ rline(Vd1195)
| ~ ron(vd1185,Vd1195)
| ~ ron(vd1186,Vd1195)
| ~ ron(vd1187,Vd1195) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3,sk4,sk5,sk6])],[f7_nnf]) ).
cnf(c16,plain,
vd1185 = sk3,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi12,axiom,
vd1185 = sk3,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(c17,plain,
rpoint(sk3),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi13,axiom,
rpoint(sk3) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t176,plain,
vf(vd1201,vd1185) = vf(vd1185,vd1201),
inference(hyper_resolution,[status(thm)],[hi94,hi3,hi4,hi12,hi13]) ).
cnf(t3286,plain,
vf(vd1185,vd1201) = vf(vd1201,vd1185),
inference(orient,[status(thm)],[t176]) ).
cnf(t4496,plain,
eq(vf(vd1201,vd1185),vplus(vf(vd1185,vd1187),vf(vd1187,vd1201))) = false,
inference(step,[status(thm)],[t188,t3286]) ).
cnf(c12,plain,
vd1187 = sk1,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi8,axiom,
vd1187 = sk1,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(c13,plain,
rpoint(sk1),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi9,axiom,
rpoint(sk1) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t168,plain,
vf(vd1187,vd1185) = vf(vd1185,vd1187),
inference(hyper_resolution,[status(thm)],[hi94,hi8,hi9,hi12,hi13]) ).
cnf(t3186,plain,
vf(vd1185,vd1187) = vf(vd1187,vd1185),
inference(orient,[status(thm)],[t168]) ).
cnf(t4497,plain,
eq(vf(vd1201,vd1185),vplus(vf(vd1187,vd1185),vf(vd1187,vd1201))) = false,
inference(step,[status(thm)],[t4496,t3186]) ).
cnf(t180,plain,
vf(vd1201,vd1187) = vf(vd1187,vd1201),
inference(hyper_resolution,[status(thm)],[hi94,hi3,hi4,hi8,hi9]) ).
cnf(t3159,plain,
vf(vd1187,vd1201) = vf(vd1201,vd1187),
inference(orient,[status(thm)],[t180]) ).
cnf(t4498,plain,
eq(vf(vd1201,vd1185),vplus(vf(vd1187,vd1185),vf(vd1201,vd1187))) = false,
inference(step,[status(thm)],[t4497,t3159]) ).
fof(f4,axiom,
! [Vd828,Vd829,Vd830] :
( ( ? [Vd832] :
( rpoint(Vd832)
& Vd828 = Vd832 )
& ? [Vd833] :
( rpoint(Vd833)
& Vd829 = Vd833 )
& ? [Vd834] :
( rpoint(Vd834)
& Vd830 = Vd834 )
& rR(Vd829,Vd828,Vd830) )
=> vplus(vf(Vd828,Vd829),vf(Vd829,Vd830)) = vf(Vd828,Vd830) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd4) ).
fof(f4_nnf,plain,
! [Vd828,Vd829,Vd830] :
( vplus(vf(Vd828,Vd829),vf(Vd829,Vd830)) = vf(Vd828,Vd830)
| ! [Vd832] :
( ~ rpoint(Vd832)
| Vd828 != Vd832 )
| ! [Vd833] :
( ~ rpoint(Vd833)
| Vd829 != Vd833 )
| ! [Vd834] :
( ~ rpoint(Vd834)
| Vd830 != Vd834 )
| ~ rR(Vd829,Vd828,Vd830) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [Vd829,Vd828,Vd830,Vd834,Vd833,Vd832] :
( vplus(vf(Vd828,Vd829),vf(Vd829,Vd830)) = vf(Vd828,Vd830)
| ~ rpoint(Vd832)
| Vd828 != Vd832
| ~ rpoint(Vd833)
| Vd829 != Vd833
| ~ rpoint(Vd834)
| Vd830 != Vd834
| ~ rR(Vd829,Vd828,Vd830) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( vplus(vf(X0,X1),vf(X1,X2)) = vf(X0,X2)
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X1,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi1,axiom,
ifeq(rR(X0,X1,X2),true,ifeq(X2,X3,ifeq(rpoint(X3),true,ifeq(X0,X4,ifeq(rpoint(X4),true,ifeq(X1,X5,ifeq(rpoint(X5),true,vplus(vf(X1,X0),vf(X0,X2)),vf(X1,X2)),vf(X1,X2)),vf(X1,X2)),vf(X1,X2)),vf(X1,X2)),vf(X1,X2)),vf(X1,X2)) = vf(X1,X2),
inference(equality_encoding,[status(esa)],[c4]) ).
fof(f1,axiom,
rR(vd1187,vd1185,vd1201),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd1) ).
fof(f1_nnf,plain,
rR(vd1187,vd1185,vd1201),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
rR(vd1187,vd1185,vd1201),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(hi0,axiom,
rR(vd1187,vd1185,vd1201) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t187,plain,
vplus(vf(vd1185,vd1187),vf(vd1187,vd1201)) = vf(vd1185,vd1201),
inference(hyper_resolution,[status(thm)],[hi1,hi0,hi3,hi4,hi8,hi9,hi12,hi13]) ).
cnf(t4483,plain,
vplus(vf(vd1187,vd1185),vf(vd1187,vd1201)) = vf(vd1185,vd1201),
inference(step,[status(thm)],[t187,t3186]) ).
cnf(t4484,plain,
vplus(vf(vd1187,vd1185),vf(vd1201,vd1187)) = vf(vd1185,vd1201),
inference(step,[status(thm)],[t4483,t3159]) ).
cnf(t4485,plain,
vplus(vf(vd1187,vd1185),vf(vd1201,vd1187)) = vf(vd1201,vd1185),
inference(step,[status(thm)],[t4484,t3286]) ).
cnf(t3390,plain,
vplus(vf(vd1187,vd1185),vf(vd1201,vd1187)) = vf(vd1201,vd1185),
inference(orient,[status(thm)],[t4485]) ).
cnf(t4499,plain,
eq(vf(vd1201,vd1185),vf(vd1201,vd1185)) = false,
inference(step,[status(thm)],[t4498,t3390]) ).
cnf(t0,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t2534,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t4500,plain,
true = false,
inference(step,[status(thm)],[t4499,t2534]) ).
cnf(t4453,plain,
false = true,
inference(orient,[status(thm)],[t4500]) ).
fof(f2,axiom,
~ rR(vd1201,vd1185,vd1187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd2) ).
fof(f2_nnf,plain,
~ rR(vd1201,vd1185,vd1187),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
~ rR(vd1201,vd1185,vd1187),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
~ rR(vd1201,vd1185,vd1187),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f3,axiom,
vd1201 != vd1187,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd3) ).
fof(f3_nnf,plain,
vd1201 != vd1187,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
vd1201 != vd1187,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
vd1201 != vd1187,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(c8,plain,
( ~ rline(X0)
| ~ ron(vd1185,X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1187,X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(c18,plain,
vd1179 != vd1180,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(c19,plain,
vd1178 != vd1180,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(c20,plain,
vd1178 != vd1179,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
fof(f9,axiom,
~ rR(vd1185,vd1201,vd1187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd9) ).
fof(f9_nnf,plain,
~ rR(vd1185,vd1201,vd1187),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
~ rR(vd1185,vd1201,vd1187),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c29,plain,
~ rR(vd1185,vd1201,vd1187),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f16,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd16) ).
fof(f16_nnf,plain,
~ ron(vd1187,vd1197),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
~ ron(vd1187,vd1197),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c37,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(f25,axiom,
! [Vd434,Vd435,Vd439,Vd440] :
( ( ? [Vd437] :
( rpoint(Vd437)
& Vd434 = Vd437 )
& ? [Vd438] :
( rpoint(Vd438)
& Vd435 = Vd438 )
& rline(Vd440)
& Vd439 = Vd440
& rS(Vd434,Vd435,Vd439) )
=> ~ ron(Vd434,Vd439) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd25) ).
fof(f25_nnf,plain,
! [Vd434,Vd435,Vd439,Vd440] :
( ~ ron(Vd434,Vd439)
| ! [Vd437] :
( ~ rpoint(Vd437)
| Vd434 != Vd437 )
| ! [Vd438] :
( ~ rpoint(Vd438)
| Vd435 != Vd438 )
| ~ rline(Vd440)
| Vd439 != Vd440
| ~ rS(Vd434,Vd435,Vd439) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [Vd434,Vd435,Vd439,Vd440,Vd438,Vd437] :
( ~ ron(Vd434,Vd439)
| ~ rpoint(Vd437)
| Vd434 != Vd437
| ~ rpoint(Vd438)
| Vd435 != Vd438
| ~ rline(Vd440)
| Vd439 != Vd440
| ~ rS(Vd434,Vd435,Vd439) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c49,plain,
( ~ ron(X0,X2)
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rline(X3)
| X2 != X3
| ~ rS(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
fof(f27,axiom,
~ rR(vd1185,vd1201,vd1187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd27) ).
fof(f27_nnf,plain,
~ rR(vd1185,vd1201,vd1187),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
~ rR(vd1185,vd1201,vd1187),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c51,plain,
~ rR(vd1185,vd1201,vd1187),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
fof(f35,axiom,
~ rR(vd1186,vd1199,vd1185),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd35) ).
fof(f35_nnf,plain,
~ rR(vd1186,vd1199,vd1185),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
~ rR(vd1186,vd1199,vd1185),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c59,plain,
~ rR(vd1186,vd1199,vd1185),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
fof(f52,axiom,
! [Vd336,Vd337,Vd338,Vd339] :
( ( rpoint(Vd337)
& Vd336 = Vd337
& rcircle(Vd339)
& Vd338 = Vd339
& rinside(Vd336,Vd338) )
=> ~ ron(Vd336,Vd338) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd52) ).
fof(f52_nnf,plain,
! [Vd336,Vd337,Vd338,Vd339] :
( ~ ron(Vd336,Vd338)
| ~ rpoint(Vd337)
| Vd336 != Vd337
| ~ rcircle(Vd339)
| Vd338 != Vd339
| ~ rinside(Vd336,Vd338) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [Vd336,Vd338,Vd339,Vd337] :
( ~ ron(Vd336,Vd338)
| ~ rpoint(Vd337)
| Vd336 != Vd337
| ~ rcircle(Vd339)
| Vd338 != Vd339
| ~ rinside(Vd336,Vd338) ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c82,plain,
( ~ ron(X0,X2)
| ~ rpoint(X1)
| X0 != X1
| ~ rcircle(X3)
| X2 != X3
| ~ rinside(X0,X2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
fof(f53,axiom,
! [Vd280,Vd281] :
( ( ? [Vd283] :
( rcircle(Vd283)
& Vd280 = Vd283 )
& ? [Vd284] :
( rcircle(Vd284)
& Vd281 = Vd284 )
& rintersect(Vd280,Vd281) )
=> ? [Vd285,Vd286] :
( rpoint(Vd285)
& ron(Vd285,Vd280)
& ron(Vd285,Vd281)
& rpoint(Vd286)
& ron(Vd286,Vd280)
& ron(Vd286,Vd281)
& Vd285 != Vd286 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd53) ).
fof(f53_nnf,plain,
! [Vd280,Vd281] :
( ? [Vd285,Vd286] :
( rpoint(Vd285)
& ron(Vd285,Vd280)
& ron(Vd285,Vd281)
& rpoint(Vd286)
& ron(Vd286,Vd280)
& ron(Vd286,Vd281)
& Vd285 != Vd286 )
| ! [Vd283] :
( ~ rcircle(Vd283)
| Vd280 != Vd283 )
| ! [Vd284] :
( ~ rcircle(Vd284)
| Vd281 != Vd284 )
| ~ rintersect(Vd280,Vd281) ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
! [Vd280,Vd281,Vd284,Vd283] :
( ( rpoint(sk10(Vd280,Vd281))
& ron(sk10(Vd280,Vd281),Vd280)
& ron(sk10(Vd280,Vd281),Vd281)
& rpoint(sk11(Vd280,Vd281))
& ron(sk11(Vd280,Vd281),Vd280)
& ron(sk11(Vd280,Vd281),Vd281)
& sk10(Vd280,Vd281) != sk11(Vd280,Vd281) )
| ~ rcircle(Vd283)
| Vd280 != Vd283
| ~ rcircle(Vd284)
| Vd281 != Vd284
| ~ rintersect(Vd280,Vd281) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk10,sk11])],[f53_nnf]) ).
cnf(c83,plain,
( sk10(X0,X1) != sk11(X0,X1)
| ~ rcircle(X3)
| X0 != X3
| ~ rcircle(X2)
| X1 != X2
| ~ rintersect(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
fof(f70,axiom,
! [Vd713,Vd714] :
( ( rreal(Vd714)
& Vd713 = Vd714 )
=> ~ rless(Vd713,Vd713) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd70) ).
fof(f70_nnf,plain,
! [Vd713,Vd714] :
( ~ rless(Vd713,Vd713)
| ~ rreal(Vd714)
| Vd713 != Vd714 ),
inference(nnf_transformation,[status(thm)],[f70]) ).
fof(f70_sk,plain,
! [Vd713,Vd714] :
( ~ rless(Vd713,Vd713)
| ~ rreal(Vd714)
| Vd713 != Vd714 ),
inference(skolemisation,[status(esa)],[f70_nnf]) ).
cnf(c111,plain,
( ~ rless(X0,X0)
| ~ rreal(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
fof(f83,axiom,
! [Vd516,Vd517,Vd518,Vd523,Vd524,Vd525,Vd526] :
( ( ? [Vd520] :
( rline(Vd520)
& Vd516 = Vd520 )
& ? [Vd521] :
( rline(Vd521)
& Vd517 = Vd521 )
& ? [Vd522] :
( rline(Vd522)
& Vd518 = Vd522 )
& ? [Vd528] :
( rpoint(Vd528)
& Vd523 = Vd528 )
& ? [Vd529] :
( rpoint(Vd529)
& Vd524 = Vd529 )
& ? [Vd530] :
( rpoint(Vd530)
& Vd525 = Vd530 )
& ? [Vd531] :
( rpoint(Vd531)
& Vd526 = Vd531 )
& ron(Vd523,Vd516)
& ron(Vd523,Vd517)
& ron(Vd523,Vd518)
& ron(Vd524,Vd516)
& ron(Vd525,Vd518)
& ron(Vd526,Vd518)
& rS(Vd525,Vd526,Vd516)
& rS(Vd524,Vd525,Vd518) )
=> ~ rS(Vd524,Vd526,Vd517) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd83) ).
fof(f83_nnf,plain,
! [Vd516,Vd517,Vd518,Vd523,Vd524,Vd525,Vd526] :
( ~ rS(Vd524,Vd526,Vd517)
| ! [Vd520] :
( ~ rline(Vd520)
| Vd516 != Vd520 )
| ! [Vd521] :
( ~ rline(Vd521)
| Vd517 != Vd521 )
| ! [Vd522] :
( ~ rline(Vd522)
| Vd518 != Vd522 )
| ! [Vd528] :
( ~ rpoint(Vd528)
| Vd523 != Vd528 )
| ! [Vd529] :
( ~ rpoint(Vd529)
| Vd524 != Vd529 )
| ! [Vd530] :
( ~ rpoint(Vd530)
| Vd525 != Vd530 )
| ! [Vd531] :
( ~ rpoint(Vd531)
| Vd526 != Vd531 )
| ~ ron(Vd523,Vd516)
| ~ ron(Vd523,Vd517)
| ~ ron(Vd523,Vd518)
| ~ ron(Vd524,Vd516)
| ~ ron(Vd525,Vd518)
| ~ ron(Vd526,Vd518)
| ~ rS(Vd525,Vd526,Vd516)
| ~ rS(Vd524,Vd525,Vd518) ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [Vd524,Vd525,Vd518,Vd526,Vd516,Vd523,Vd517,Vd531,Vd530,Vd529,Vd528,Vd522,Vd521,Vd520] :
( ~ rS(Vd524,Vd526,Vd517)
| ~ rline(Vd520)
| Vd516 != Vd520
| ~ rline(Vd521)
| Vd517 != Vd521
| ~ rline(Vd522)
| Vd518 != Vd522
| ~ rpoint(Vd528)
| Vd523 != Vd528
| ~ rpoint(Vd529)
| Vd524 != Vd529
| ~ rpoint(Vd530)
| Vd525 != Vd530
| ~ rpoint(Vd531)
| Vd526 != Vd531
| ~ ron(Vd523,Vd516)
| ~ ron(Vd523,Vd517)
| ~ ron(Vd523,Vd518)
| ~ ron(Vd524,Vd516)
| ~ ron(Vd525,Vd518)
| ~ ron(Vd526,Vd518)
| ~ rS(Vd525,Vd526,Vd516)
| ~ rS(Vd524,Vd525,Vd518) ),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c134,plain,
( ~ rS(X4,X6,X1)
| ~ rline(X13)
| X0 != X13
| ~ rline(X12)
| X1 != X12
| ~ rline(X11)
| X2 != X11
| ~ rpoint(X10)
| X3 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rpoint(X8)
| X5 != X8
| ~ rpoint(X7)
| X6 != X7
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X3,X2)
| ~ ron(X4,X0)
| ~ ron(X5,X2)
| ~ ron(X6,X2)
| ~ rS(X5,X6,X0)
| ~ rS(X4,X5,X2) ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
fof(f85,axiom,
! [Vd489,Vd490,Vd491,Vd496,Vd497] :
( ( ? [Vd493] :
( rpoint(Vd493)
& Vd489 = Vd493 )
& ? [Vd494] :
( rpoint(Vd494)
& Vd490 = Vd494 )
& ? [Vd495] :
( rpoint(Vd495)
& Vd491 = Vd495 )
& rline(Vd497)
& Vd496 = Vd497
& rR(Vd490,Vd489,Vd491)
& ron(Vd490,Vd496) )
=> ~ rS(Vd489,Vd491,Vd496) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd85) ).
fof(f85_nnf,plain,
! [Vd489,Vd490,Vd491,Vd496,Vd497] :
( ~ rS(Vd489,Vd491,Vd496)
| ! [Vd493] :
( ~ rpoint(Vd493)
| Vd489 != Vd493 )
| ! [Vd494] :
( ~ rpoint(Vd494)
| Vd490 != Vd494 )
| ! [Vd495] :
( ~ rpoint(Vd495)
| Vd491 != Vd495 )
| ~ rline(Vd497)
| Vd496 != Vd497
| ~ rR(Vd490,Vd489,Vd491)
| ~ ron(Vd490,Vd496) ),
inference(nnf_transformation,[status(thm)],[f85]) ).
fof(f85_sk,plain,
! [Vd490,Vd496,Vd489,Vd491,Vd497,Vd495,Vd494,Vd493] :
( ~ rS(Vd489,Vd491,Vd496)
| ~ rpoint(Vd493)
| Vd489 != Vd493
| ~ rpoint(Vd494)
| Vd490 != Vd494
| ~ rpoint(Vd495)
| Vd491 != Vd495
| ~ rline(Vd497)
| Vd496 != Vd497
| ~ rR(Vd490,Vd489,Vd491)
| ~ ron(Vd490,Vd496) ),
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c136,plain,
( ~ rS(X0,X2,X3)
| ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rline(X4)
| X3 != X4
| ~ rR(X1,X0,X2)
| ~ ron(X1,X3) ),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
fof(f92,axiom,
! [Vd408,Vd409,Vd410,Vd411] :
( ( ? [Vd413] :
( rpoint(Vd413)
& Vd408 = Vd413 )
& ? [Vd414] :
( rpoint(Vd414)
& Vd409 = Vd414 )
& ? [Vd415] :
( rpoint(Vd415)
& Vd410 = Vd415 )
& ? [Vd416] :
( rpoint(Vd416)
& Vd411 = Vd416 )
& rR(Vd409,Vd408,Vd410)
& rR(Vd409,Vd408,Vd411) )
=> ~ rR(Vd409,Vd410,Vd411) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd92) ).
fof(f92_nnf,plain,
! [Vd408,Vd409,Vd410,Vd411] :
( ~ rR(Vd409,Vd410,Vd411)
| ! [Vd413] :
( ~ rpoint(Vd413)
| Vd408 != Vd413 )
| ! [Vd414] :
( ~ rpoint(Vd414)
| Vd409 != Vd414 )
| ! [Vd415] :
( ~ rpoint(Vd415)
| Vd410 != Vd415 )
| ! [Vd416] :
( ~ rpoint(Vd416)
| Vd411 != Vd416 )
| ~ rR(Vd409,Vd408,Vd410)
| ~ rR(Vd409,Vd408,Vd411) ),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
! [Vd409,Vd408,Vd411,Vd410,Vd416,Vd415,Vd414,Vd413] :
( ~ rR(Vd409,Vd410,Vd411)
| ~ rpoint(Vd413)
| Vd408 != Vd413
| ~ rpoint(Vd414)
| Vd409 != Vd414
| ~ rpoint(Vd415)
| Vd410 != Vd415
| ~ rpoint(Vd416)
| Vd411 != Vd416
| ~ rR(Vd409,Vd408,Vd410)
| ~ rR(Vd409,Vd408,Vd411) ),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c143,plain,
( ~ rR(X1,X2,X3)
| ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4
| ~ rR(X1,X0,X2)
| ~ rR(X1,X0,X3) ),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
fof(f97,axiom,
! [Vd340,Vd341,Vd342] :
( ( ? [Vd344] :
( rpoint(Vd344)
& Vd340 = Vd344 )
& ? [Vd345] :
( rpoint(Vd345)
& Vd341 = Vd345 )
& ? [Vd346] :
( rpoint(Vd346)
& Vd342 = Vd346 )
& rR(Vd341,Vd340,Vd342) )
=> ( rR(Vd341,Vd342,Vd340)
& Vd340 != Vd341
& Vd340 != Vd342
& ~ rR(Vd340,Vd341,Vd342) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd97) ).
fof(f97_nnf,plain,
! [Vd340,Vd341,Vd342] :
( ( rR(Vd341,Vd342,Vd340)
& Vd340 != Vd341
& Vd340 != Vd342
& ~ rR(Vd340,Vd341,Vd342) )
| ! [Vd344] :
( ~ rpoint(Vd344)
| Vd340 != Vd344 )
| ! [Vd345] :
( ~ rpoint(Vd345)
| Vd341 != Vd345 )
| ! [Vd346] :
( ~ rpoint(Vd346)
| Vd342 != Vd346 )
| ~ rR(Vd341,Vd340,Vd342) ),
inference(nnf_transformation,[status(thm)],[f97]) ).
fof(f97_sk,plain,
! [Vd341,Vd340,Vd342,Vd346,Vd345,Vd344] :
( ( rR(Vd341,Vd342,Vd340)
& Vd340 != Vd341
& Vd340 != Vd342
& ~ rR(Vd340,Vd341,Vd342) )
| ~ rpoint(Vd344)
| Vd340 != Vd344
| ~ rpoint(Vd345)
| Vd341 != Vd345
| ~ rpoint(Vd346)
| Vd342 != Vd346
| ~ rR(Vd341,Vd340,Vd342) ),
inference(skolemisation,[status(esa)],[f97_nnf]) ).
cnf(c148,plain,
( ~ rR(X0,X1,X2)
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X1,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(c149,plain,
( X0 != X2
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X1,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(c150,plain,
( X0 != X1
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X1,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
fof(f105,axiom,
! [Vd244,Vd245,Vd246,Vd247] :
( ( rcircle(Vd245)
& Vd244 = Vd245
& rline(Vd247)
& Vd246 = Vd247
& rintersect(Vd246,Vd244) )
=> ? [Vd248,Vd250] :
( rpoint(Vd248)
& ron(Vd248,Vd246)
& ron(Vd248,Vd244)
& rpoint(Vd250)
& ron(Vd250,Vd246)
& ron(Vd250,Vd244)
& Vd248 != Vd250 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd105) ).
fof(f105_nnf,plain,
! [Vd244,Vd245,Vd246,Vd247] :
( ? [Vd248,Vd250] :
( rpoint(Vd248)
& ron(Vd248,Vd246)
& ron(Vd248,Vd244)
& rpoint(Vd250)
& ron(Vd250,Vd246)
& ron(Vd250,Vd244)
& Vd248 != Vd250 )
| ~ rcircle(Vd245)
| Vd244 != Vd245
| ~ rline(Vd247)
| Vd246 != Vd247
| ~ rintersect(Vd246,Vd244) ),
inference(nnf_transformation,[status(thm)],[f105]) ).
fof(f105_sk,plain,
! [Vd246,Vd244,Vd247,Vd245] :
( ( rpoint(sk21(Vd244,Vd245,Vd246,Vd247))
& ron(sk21(Vd244,Vd245,Vd246,Vd247),Vd246)
& ron(sk21(Vd244,Vd245,Vd246,Vd247),Vd244)
& rpoint(sk22(Vd244,Vd245,Vd246,Vd247))
& ron(sk22(Vd244,Vd245,Vd246,Vd247),Vd246)
& ron(sk22(Vd244,Vd245,Vd246,Vd247),Vd244)
& sk21(Vd244,Vd245,Vd246,Vd247) != sk22(Vd244,Vd245,Vd246,Vd247) )
| ~ rcircle(Vd245)
| Vd244 != Vd245
| ~ rline(Vd247)
| Vd246 != Vd247
| ~ rintersect(Vd246,Vd244) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk21,sk22])],[f105_nnf]) ).
cnf(c170,plain,
( sk21(X0,X1,X2,X3) != sk22(X0,X1,X2,X3)
| ~ rcircle(X1)
| X0 != X1
| ~ rline(X3)
| X2 != X3
| ~ rintersect(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f105_sk]) ).
fof(f109,axiom,
! [Vd214,Vd215] :
( ( rcircle(Vd215)
& Vd214 = Vd215 )
=> ? [Vd216] :
( rpoint(Vd216)
& ~ rinside(Vd216,Vd214)
& ~ ron(Vd216,Vd214) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd109) ).
fof(f109_nnf,plain,
! [Vd214,Vd215] :
( ? [Vd216] :
( rpoint(Vd216)
& ~ rinside(Vd216,Vd214)
& ~ ron(Vd216,Vd214) )
| ~ rcircle(Vd215)
| Vd214 != Vd215 ),
inference(nnf_transformation,[status(thm)],[f109]) ).
fof(f109_sk,plain,
! [Vd214,Vd215] :
( ( rpoint(sk26(Vd214,Vd215))
& ~ rinside(sk26(Vd214,Vd215),Vd214)
& ~ ron(sk26(Vd214,Vd215),Vd214) )
| ~ rcircle(Vd215)
| Vd214 != Vd215 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk26])],[f109_nnf]) ).
cnf(c186,plain,
( ~ ron(sk26(X0,X1),X0)
| ~ rcircle(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
cnf(c187,plain,
( ~ rinside(sk26(X0,X1),X0)
| ~ rcircle(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f109_sk]) ).
fof(f111,axiom,
! [Vd200,Vd201,Vd202,Vd203] :
( ( rcircle(Vd201)
& Vd200 = Vd201
& ? [Vd205] :
( rpoint(Vd205)
& Vd202 = Vd205 )
& ? [Vd206] :
( rpoint(Vd206)
& Vd203 = Vd206 )
& ron(Vd202,Vd200)
& ron(Vd203,Vd200) )
=> ? [Vd208] :
( rpoint(Vd208)
& ron(Vd208,Vd200)
& Vd208 != Vd202
& Vd208 != Vd203 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd111) ).
fof(f111_nnf,plain,
! [Vd200,Vd201,Vd202,Vd203] :
( ? [Vd208] :
( rpoint(Vd208)
& ron(Vd208,Vd200)
& Vd208 != Vd202
& Vd208 != Vd203 )
| ~ rcircle(Vd201)
| Vd200 != Vd201
| ! [Vd205] :
( ~ rpoint(Vd205)
| Vd202 != Vd205 )
| ! [Vd206] :
( ~ rpoint(Vd206)
| Vd203 != Vd206 )
| ~ ron(Vd202,Vd200)
| ~ ron(Vd203,Vd200) ),
inference(nnf_transformation,[status(thm)],[f111]) ).
fof(f111_sk,plain,
! [Vd203,Vd200,Vd202,Vd206,Vd205,Vd201] :
( ( rpoint(sk28(Vd200,Vd201,Vd202,Vd203))
& ron(sk28(Vd200,Vd201,Vd202,Vd203),Vd200)
& sk28(Vd200,Vd201,Vd202,Vd203) != Vd202
& sk28(Vd200,Vd201,Vd202,Vd203) != Vd203 )
| ~ rcircle(Vd201)
| Vd200 != Vd201
| ~ rpoint(Vd205)
| Vd202 != Vd205
| ~ rpoint(Vd206)
| Vd203 != Vd206
| ~ ron(Vd202,Vd200)
| ~ ron(Vd203,Vd200) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk28])],[f111_nnf]) ).
cnf(c191,plain,
( sk28(X0,X1,X2,X3) != X3
| ~ rcircle(X1)
| X0 != X1
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4
| ~ ron(X2,X0)
| ~ ron(X3,X0) ),
inference(cnf_transformation,[status(esa)],[f111_sk]) ).
cnf(c192,plain,
( sk28(X0,X1,X2,X3) != X2
| ~ rcircle(X1)
| X0 != X1
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4
| ~ ron(X2,X0)
| ~ ron(X3,X0) ),
inference(cnf_transformation,[status(esa)],[f111_sk]) ).
fof(f112,axiom,
! [Vd194,Vd195,Vd196,Vd197] :
( ( rcircle(Vd195)
& Vd194 = Vd195
& rpoint(Vd197)
& Vd196 = Vd197
& ron(Vd196,Vd194) )
=> ? [Vd198] :
( rpoint(Vd198)
& ron(Vd198,Vd194)
& Vd198 != Vd196 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd112) ).
fof(f112_nnf,plain,
! [Vd194,Vd195,Vd196,Vd197] :
( ? [Vd198] :
( rpoint(Vd198)
& ron(Vd198,Vd194)
& Vd198 != Vd196 )
| ~ rcircle(Vd195)
| Vd194 != Vd195
| ~ rpoint(Vd197)
| Vd196 != Vd197
| ~ ron(Vd196,Vd194) ),
inference(nnf_transformation,[status(thm)],[f112]) ).
fof(f112_sk,plain,
! [Vd196,Vd194,Vd197,Vd195] :
( ( rpoint(sk29(Vd194,Vd195,Vd196,Vd197))
& ron(sk29(Vd194,Vd195,Vd196,Vd197),Vd194)
& sk29(Vd194,Vd195,Vd196,Vd197) != Vd196 )
| ~ rcircle(Vd195)
| Vd194 != Vd195
| ~ rpoint(Vd197)
| Vd196 != Vd197
| ~ ron(Vd196,Vd194) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk29])],[f112_nnf]) ).
cnf(c195,plain,
( sk29(X0,X1,X2,X3) != X2
| ~ rcircle(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f112_sk]) ).
fof(f118,axiom,
! [Vd138,Vd139,Vd140,Vd141,Vd146,Vd147] :
( ( rline(Vd139)
& Vd138 = Vd139
& ? [Vd143] :
( rpoint(Vd143)
& Vd140 = Vd143 )
& ? [Vd144] :
( rpoint(Vd144)
& Vd141 = Vd144 )
& ron(Vd140,Vd138)
& ron(Vd141,Vd138)
& rpoint(Vd147)
& rR(Vd141,Vd140,Vd146)
& Vd146 = Vd147 )
=> ? [Vd149] :
( rpoint(Vd149)
& rR(Vd141,Vd140,Vd149)
& Vd149 != Vd146 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd118) ).
fof(f118_nnf,plain,
! [Vd138,Vd139,Vd140,Vd141,Vd146,Vd147] :
( ? [Vd149] :
( rpoint(Vd149)
& rR(Vd141,Vd140,Vd149)
& Vd149 != Vd146 )
| ~ rline(Vd139)
| Vd138 != Vd139
| ! [Vd143] :
( ~ rpoint(Vd143)
| Vd140 != Vd143 )
| ! [Vd144] :
( ~ rpoint(Vd144)
| Vd141 != Vd144 )
| ~ ron(Vd140,Vd138)
| ~ ron(Vd141,Vd138)
| ~ rpoint(Vd147)
| ~ rR(Vd141,Vd140,Vd146)
| Vd146 != Vd147 ),
inference(nnf_transformation,[status(thm)],[f118]) ).
fof(f118_sk,plain,
! [Vd146,Vd147,Vd141,Vd140,Vd138,Vd144,Vd143,Vd139] :
( ( rpoint(sk35(Vd138,Vd139,Vd140,Vd141,Vd146,Vd147))
& rR(Vd141,Vd140,sk35(Vd138,Vd139,Vd140,Vd141,Vd146,Vd147))
& sk35(Vd138,Vd139,Vd140,Vd141,Vd146,Vd147) != Vd146 )
| ~ rline(Vd139)
| Vd138 != Vd139
| ~ rpoint(Vd143)
| Vd140 != Vd143
| ~ rpoint(Vd144)
| Vd141 != Vd144
| ~ ron(Vd140,Vd138)
| ~ ron(Vd141,Vd138)
| ~ rpoint(Vd147)
| ~ rR(Vd141,Vd140,Vd146)
| Vd146 != Vd147 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk35])],[f118_nnf]) ).
cnf(c214,plain,
( sk35(X0,X1,X2,X3,X4,X5) != X4
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ ron(X2,X0)
| ~ ron(X3,X0)
| ~ rpoint(X5)
| ~ rR(X3,X2,X4)
| X4 != X5 ),
inference(cnf_transformation,[status(esa)],[f118_sk]) ).
fof(f120,axiom,
! [Vd109,Vd110,Vd111,Vd112,Vd113,Vd114] :
( ( rline(Vd110)
& Vd109 = Vd110
& ? [Vd116] :
( rpoint(Vd116)
& Vd111 = Vd116 )
& ? [Vd117] :
( rpoint(Vd117)
& Vd112 = Vd117 )
& ? [Vd118] :
( rpoint(Vd118)
& Vd113 = Vd118 )
& ? [Vd119] :
( rpoint(Vd119)
& Vd114 = Vd119 )
& ron(Vd111,Vd109)
& ron(Vd112,Vd109)
& ron(Vd113,Vd109)
& rR(Vd113,Vd111,Vd112)
& rR(Vd114,Vd111,Vd112) )
=> ? [Vd123] :
( rpoint(Vd123)
& rR(Vd123,Vd111,Vd112)
& Vd123 != Vd113
& Vd123 != Vd114 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd120) ).
fof(f120_nnf,plain,
! [Vd109,Vd110,Vd111,Vd112,Vd113,Vd114] :
( ? [Vd123] :
( rpoint(Vd123)
& rR(Vd123,Vd111,Vd112)
& Vd123 != Vd113
& Vd123 != Vd114 )
| ~ rline(Vd110)
| Vd109 != Vd110
| ! [Vd116] :
( ~ rpoint(Vd116)
| Vd111 != Vd116 )
| ! [Vd117] :
( ~ rpoint(Vd117)
| Vd112 != Vd117 )
| ! [Vd118] :
( ~ rpoint(Vd118)
| Vd113 != Vd118 )
| ! [Vd119] :
( ~ rpoint(Vd119)
| Vd114 != Vd119 )
| ~ ron(Vd111,Vd109)
| ~ ron(Vd112,Vd109)
| ~ ron(Vd113,Vd109)
| ~ rR(Vd113,Vd111,Vd112)
| ~ rR(Vd114,Vd111,Vd112) ),
inference(nnf_transformation,[status(thm)],[f120]) ).
fof(f120_sk,plain,
! [Vd114,Vd111,Vd112,Vd113,Vd109,Vd119,Vd118,Vd117,Vd116,Vd110] :
( ( rpoint(sk37(Vd109,Vd110,Vd111,Vd112,Vd113,Vd114))
& rR(sk37(Vd109,Vd110,Vd111,Vd112,Vd113,Vd114),Vd111,Vd112)
& sk37(Vd109,Vd110,Vd111,Vd112,Vd113,Vd114) != Vd113
& sk37(Vd109,Vd110,Vd111,Vd112,Vd113,Vd114) != Vd114 )
| ~ rline(Vd110)
| Vd109 != Vd110
| ~ rpoint(Vd116)
| Vd111 != Vd116
| ~ rpoint(Vd117)
| Vd112 != Vd117
| ~ rpoint(Vd118)
| Vd113 != Vd118
| ~ rpoint(Vd119)
| Vd114 != Vd119
| ~ ron(Vd111,Vd109)
| ~ ron(Vd112,Vd109)
| ~ ron(Vd113,Vd109)
| ~ rR(Vd113,Vd111,Vd112)
| ~ rR(Vd114,Vd111,Vd112) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk37])],[f120_nnf]) ).
cnf(c219,plain,
( sk37(X0,X1,X2,X3,X4,X5) != X5
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X9)
| X2 != X9
| ~ rpoint(X8)
| X3 != X8
| ~ rpoint(X7)
| X4 != X7
| ~ rpoint(X6)
| X5 != X6
| ~ ron(X2,X0)
| ~ ron(X3,X0)
| ~ ron(X4,X0)
| ~ rR(X4,X2,X3)
| ~ rR(X5,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(c220,plain,
( sk37(X0,X1,X2,X3,X4,X5) != X4
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X9)
| X2 != X9
| ~ rpoint(X8)
| X3 != X8
| ~ rpoint(X7)
| X4 != X7
| ~ rpoint(X6)
| X5 != X6
| ~ ron(X2,X0)
| ~ ron(X3,X0)
| ~ ron(X4,X0)
| ~ rR(X4,X2,X3)
| ~ rR(X5,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
fof(f121,axiom,
! [Vd95,Vd96,Vd97,Vd98,Vd99] :
( ( rline(Vd96)
& Vd95 = Vd96
& ? [Vd101] :
( rpoint(Vd101)
& Vd97 = Vd101 )
& ? [Vd102] :
( rpoint(Vd102)
& Vd98 = Vd102 )
& ? [Vd103] :
( rpoint(Vd103)
& Vd99 = Vd103 )
& ron(Vd97,Vd95)
& ron(Vd98,Vd95)
& rR(Vd99,Vd97,Vd98) )
=> ? [Vd106] :
( rpoint(Vd106)
& rR(Vd106,Vd97,Vd98)
& Vd106 != Vd99 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd121) ).
fof(f121_nnf,plain,
! [Vd95,Vd96,Vd97,Vd98,Vd99] :
( ? [Vd106] :
( rpoint(Vd106)
& rR(Vd106,Vd97,Vd98)
& Vd106 != Vd99 )
| ~ rline(Vd96)
| Vd95 != Vd96
| ! [Vd101] :
( ~ rpoint(Vd101)
| Vd97 != Vd101 )
| ! [Vd102] :
( ~ rpoint(Vd102)
| Vd98 != Vd102 )
| ! [Vd103] :
( ~ rpoint(Vd103)
| Vd99 != Vd103 )
| ~ ron(Vd97,Vd95)
| ~ ron(Vd98,Vd95)
| ~ rR(Vd99,Vd97,Vd98) ),
inference(nnf_transformation,[status(thm)],[f121]) ).
fof(f121_sk,plain,
! [Vd99,Vd97,Vd98,Vd95,Vd103,Vd102,Vd101,Vd96] :
( ( rpoint(sk38(Vd95,Vd96,Vd97,Vd98,Vd99))
& rR(sk38(Vd95,Vd96,Vd97,Vd98,Vd99),Vd97,Vd98)
& sk38(Vd95,Vd96,Vd97,Vd98,Vd99) != Vd99 )
| ~ rline(Vd96)
| Vd95 != Vd96
| ~ rpoint(Vd101)
| Vd97 != Vd101
| ~ rpoint(Vd102)
| Vd98 != Vd102
| ~ rpoint(Vd103)
| Vd99 != Vd103
| ~ ron(Vd97,Vd95)
| ~ ron(Vd98,Vd95)
| ~ rR(Vd99,Vd97,Vd98) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk38])],[f121_nnf]) ).
cnf(c223,plain,
( sk38(X0,X1,X2,X3,X4) != X4
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ ron(X2,X0)
| ~ ron(X3,X0)
| ~ rR(X4,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
fof(f123,axiom,
! [Vd71,Vd72,Vd73,Vd74,Vd75] :
( ( rline(Vd72)
& Vd71 = Vd72
& ? [Vd77] :
( rpoint(Vd77)
& Vd73 = Vd77 )
& ? [Vd78] :
( rpoint(Vd78)
& Vd74 = Vd78 )
& ? [Vd79] :
( rpoint(Vd79)
& Vd75 = Vd79 )
& ron(Vd73,Vd71)
& ron(Vd74,Vd71)
& ron(Vd75,Vd71) )
=> ? [Vd81] :
( rpoint(Vd81)
& ron(Vd81,Vd71)
& Vd81 != Vd73
& Vd81 != Vd74 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd123) ).
fof(f123_nnf,plain,
! [Vd71,Vd72,Vd73,Vd74,Vd75] :
( ? [Vd81] :
( rpoint(Vd81)
& ron(Vd81,Vd71)
& Vd81 != Vd73
& Vd81 != Vd74 )
| ~ rline(Vd72)
| Vd71 != Vd72
| ! [Vd77] :
( ~ rpoint(Vd77)
| Vd73 != Vd77 )
| ! [Vd78] :
( ~ rpoint(Vd78)
| Vd74 != Vd78 )
| ! [Vd79] :
( ~ rpoint(Vd79)
| Vd75 != Vd79 )
| ~ ron(Vd73,Vd71)
| ~ ron(Vd74,Vd71)
| ~ ron(Vd75,Vd71) ),
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
! [Vd75,Vd71,Vd74,Vd73,Vd79,Vd78,Vd77,Vd72] :
( ( rpoint(sk40(Vd71,Vd72,Vd73,Vd74,Vd75))
& ron(sk40(Vd71,Vd72,Vd73,Vd74,Vd75),Vd71)
& sk40(Vd71,Vd72,Vd73,Vd74,Vd75) != Vd73
& sk40(Vd71,Vd72,Vd73,Vd74,Vd75) != Vd74 )
| ~ rline(Vd72)
| Vd71 != Vd72
| ~ rpoint(Vd77)
| Vd73 != Vd77
| ~ rpoint(Vd78)
| Vd74 != Vd78
| ~ rpoint(Vd79)
| Vd75 != Vd79
| ~ ron(Vd73,Vd71)
| ~ ron(Vd74,Vd71)
| ~ ron(Vd75,Vd71) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk40])],[f123_nnf]) ).
cnf(c228,plain,
( sk40(X0,X1,X2,X3,X4) != X3
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ ron(X2,X0)
| ~ ron(X3,X0)
| ~ ron(X4,X0) ),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
cnf(c229,plain,
( sk40(X0,X1,X2,X3,X4) != X2
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ ron(X2,X0)
| ~ ron(X3,X0)
| ~ ron(X4,X0) ),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
fof(f124,axiom,
! [Vd61,Vd62,Vd63,Vd64,Vd65,Vd66] :
( ( rline(Vd62)
& Vd61 = Vd62
& rpoint(Vd64)
& Vd63 = Vd64
& rpoint(Vd66)
& Vd65 = Vd66
& ron(Vd63,Vd61)
& ron(Vd65,Vd61) )
=> ? [Vd68] :
( rpoint(Vd68)
& ron(Vd68,Vd61)
& Vd68 != Vd63
& Vd68 != Vd65 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd124) ).
fof(f124_nnf,plain,
! [Vd61,Vd62,Vd63,Vd64,Vd65,Vd66] :
( ? [Vd68] :
( rpoint(Vd68)
& ron(Vd68,Vd61)
& Vd68 != Vd63
& Vd68 != Vd65 )
| ~ rline(Vd62)
| Vd61 != Vd62
| ~ rpoint(Vd64)
| Vd63 != Vd64
| ~ rpoint(Vd66)
| Vd65 != Vd66
| ~ ron(Vd63,Vd61)
| ~ ron(Vd65,Vd61) ),
inference(nnf_transformation,[status(thm)],[f124]) ).
fof(f124_sk,plain,
! [Vd65,Vd61,Vd63,Vd66,Vd64,Vd62] :
( ( rpoint(sk41(Vd61,Vd62,Vd63,Vd64,Vd65,Vd66))
& ron(sk41(Vd61,Vd62,Vd63,Vd64,Vd65,Vd66),Vd61)
& sk41(Vd61,Vd62,Vd63,Vd64,Vd65,Vd66) != Vd63
& sk41(Vd61,Vd62,Vd63,Vd64,Vd65,Vd66) != Vd65 )
| ~ rline(Vd62)
| Vd61 != Vd62
| ~ rpoint(Vd64)
| Vd63 != Vd64
| ~ rpoint(Vd66)
| Vd65 != Vd66
| ~ ron(Vd63,Vd61)
| ~ ron(Vd65,Vd61) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk41])],[f124_nnf]) ).
cnf(c232,plain,
( sk41(X0,X1,X2,X3,X4,X5) != X4
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ ron(X2,X0)
| ~ ron(X4,X0) ),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
cnf(c233,plain,
( sk41(X0,X1,X2,X3,X4,X5) != X2
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X5)
| X4 != X5
| ~ ron(X2,X0)
| ~ ron(X4,X0) ),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
fof(f125,axiom,
! [Vd55,Vd56,Vd57,Vd58] :
( ( rline(Vd56)
& Vd55 = Vd56
& rpoint(Vd58)
& Vd57 = Vd58
& ron(Vd57,Vd55) )
=> ? [Vd59] :
( rpoint(Vd59)
& ron(Vd59,Vd55)
& Vd59 != Vd57 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd125) ).
fof(f125_nnf,plain,
! [Vd55,Vd56,Vd57,Vd58] :
( ? [Vd59] :
( rpoint(Vd59)
& ron(Vd59,Vd55)
& Vd59 != Vd57 )
| ~ rline(Vd56)
| Vd55 != Vd56
| ~ rpoint(Vd58)
| Vd57 != Vd58
| ~ ron(Vd57,Vd55) ),
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [Vd57,Vd55,Vd58,Vd56] :
( ( rpoint(sk42(Vd55,Vd56,Vd57,Vd58))
& ron(sk42(Vd55,Vd56,Vd57,Vd58),Vd55)
& sk42(Vd55,Vd56,Vd57,Vd58) != Vd57 )
| ~ rline(Vd56)
| Vd55 != Vd56
| ~ rpoint(Vd58)
| Vd57 != Vd58
| ~ ron(Vd57,Vd55) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk42])],[f125_nnf]) ).
cnf(c236,plain,
( sk42(X0,X1,X2,X3) != X2
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
fof(f127,axiom,
! [Vd38,Vd39,Vd40,Vd41] :
( ( ? [Vd43] :
( rpoint(Vd43)
& Vd38 = Vd43 )
& ? [Vd44] :
( rpoint(Vd44)
& Vd39 = Vd44 )
& ? [Vd45] :
( rpoint(Vd45)
& Vd40 = Vd45 )
& ? [Vd46] :
( rpoint(Vd46)
& Vd41 = Vd46 ) )
=> ? [Vd47] :
( rpoint(Vd47)
& Vd47 != Vd38
& Vd47 != Vd39
& Vd47 != Vd40
& Vd47 != Vd41 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd127) ).
fof(f127_nnf,plain,
! [Vd38,Vd39,Vd40,Vd41] :
( ? [Vd47] :
( rpoint(Vd47)
& Vd47 != Vd38
& Vd47 != Vd39
& Vd47 != Vd40
& Vd47 != Vd41 )
| ! [Vd43] :
( ~ rpoint(Vd43)
| Vd38 != Vd43 )
| ! [Vd44] :
( ~ rpoint(Vd44)
| Vd39 != Vd44 )
| ! [Vd45] :
( ~ rpoint(Vd45)
| Vd40 != Vd45 )
| ! [Vd46] :
( ~ rpoint(Vd46)
| Vd41 != Vd46 ) ),
inference(nnf_transformation,[status(thm)],[f127]) ).
fof(f127_sk,plain,
! [Vd41,Vd46,Vd40,Vd45,Vd39,Vd44,Vd38,Vd43] :
( ( rpoint(sk44(Vd38,Vd39,Vd40,Vd41))
& sk44(Vd38,Vd39,Vd40,Vd41) != Vd38
& sk44(Vd38,Vd39,Vd40,Vd41) != Vd39
& sk44(Vd38,Vd39,Vd40,Vd41) != Vd40
& sk44(Vd38,Vd39,Vd40,Vd41) != Vd41 )
| ~ rpoint(Vd43)
| Vd38 != Vd43
| ~ rpoint(Vd44)
| Vd39 != Vd44
| ~ rpoint(Vd45)
| Vd40 != Vd45
| ~ rpoint(Vd46)
| Vd41 != Vd46 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk44])],[f127_nnf]) ).
cnf(c241,plain,
( sk44(X0,X1,X2,X3) != X3
| ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4 ),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(c242,plain,
( sk44(X0,X1,X2,X3) != X2
| ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4 ),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(c243,plain,
( sk44(X0,X1,X2,X3) != X1
| ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4 ),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(c244,plain,
( sk44(X0,X1,X2,X3) != X0
| ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rpoint(X4)
| X3 != X4 ),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
fof(f128,axiom,
! [Vd27,Vd28,Vd29] :
( ( ? [Vd31] :
( rpoint(Vd31)
& Vd27 = Vd31 )
& ? [Vd32] :
( rpoint(Vd32)
& Vd28 = Vd32 )
& ? [Vd33] :
( rpoint(Vd33)
& Vd29 = Vd33 ) )
=> ? [Vd34] :
( rpoint(Vd34)
& Vd34 != Vd27
& Vd34 != Vd28
& Vd34 != Vd29 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd128) ).
fof(f128_nnf,plain,
! [Vd27,Vd28,Vd29] :
( ? [Vd34] :
( rpoint(Vd34)
& Vd34 != Vd27
& Vd34 != Vd28
& Vd34 != Vd29 )
| ! [Vd31] :
( ~ rpoint(Vd31)
| Vd27 != Vd31 )
| ! [Vd32] :
( ~ rpoint(Vd32)
| Vd28 != Vd32 )
| ! [Vd33] :
( ~ rpoint(Vd33)
| Vd29 != Vd33 ) ),
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [Vd29,Vd33,Vd28,Vd32,Vd27,Vd31] :
( ( rpoint(sk45(Vd27,Vd28,Vd29))
& sk45(Vd27,Vd28,Vd29) != Vd27
& sk45(Vd27,Vd28,Vd29) != Vd28
& sk45(Vd27,Vd28,Vd29) != Vd29 )
| ~ rpoint(Vd31)
| Vd27 != Vd31
| ~ rpoint(Vd32)
| Vd28 != Vd32
| ~ rpoint(Vd33)
| Vd29 != Vd33 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk45])],[f128_nnf]) ).
cnf(c246,plain,
( sk45(X0,X1,X2) != X2
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3 ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(c247,plain,
( sk45(X0,X1,X2) != X1
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3 ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(c248,plain,
( sk45(X0,X1,X2) != X0
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3 ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
fof(f129,axiom,
! [Vd19,Vd20] :
( ( ? [Vd22] :
( rpoint(Vd22)
& Vd19 = Vd22 )
& ? [Vd23] :
( rpoint(Vd23)
& Vd20 = Vd23 ) )
=> ? [Vd24] :
( rpoint(Vd24)
& Vd24 != Vd19
& Vd24 != Vd20 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd129) ).
fof(f129_nnf,plain,
! [Vd19,Vd20] :
( ? [Vd24] :
( rpoint(Vd24)
& Vd24 != Vd19
& Vd24 != Vd20 )
| ! [Vd22] :
( ~ rpoint(Vd22)
| Vd19 != Vd22 )
| ! [Vd23] :
( ~ rpoint(Vd23)
| Vd20 != Vd23 ) ),
inference(nnf_transformation,[status(thm)],[f129]) ).
fof(f129_sk,plain,
! [Vd20,Vd23,Vd19,Vd22] :
( ( rpoint(sk46(Vd19,Vd20))
& sk46(Vd19,Vd20) != Vd19
& sk46(Vd19,Vd20) != Vd20 )
| ~ rpoint(Vd22)
| Vd19 != Vd22
| ~ rpoint(Vd23)
| Vd20 != Vd23 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk46])],[f129_nnf]) ).
cnf(c250,plain,
( sk46(X0,X1) != X1
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2 ),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
cnf(c251,plain,
( sk46(X0,X1) != X0
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2 ),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
fof(f130,axiom,
! [Vd15,Vd16] :
( ( rpoint(Vd16)
& Vd15 = Vd16 )
=> ? [Vd17] :
( rpoint(Vd17)
& Vd17 != Vd15 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd130) ).
fof(f130_nnf,plain,
! [Vd15,Vd16] :
( ? [Vd17] :
( rpoint(Vd17)
& Vd17 != Vd15 )
| ~ rpoint(Vd16)
| Vd15 != Vd16 ),
inference(nnf_transformation,[status(thm)],[f130]) ).
fof(f130_sk,plain,
! [Vd15,Vd16] :
( ( rpoint(sk47(Vd15,Vd16))
& sk47(Vd15,Vd16) != Vd15 )
| ~ rpoint(Vd16)
| Vd15 != Vd16 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk47])],[f130_nnf]) ).
cnf(c253,plain,
( sk47(X0,X1) != X0
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f130_sk]) ).
fof(f132,axiom,
! [Vd5,Vd6,Vd7,Vd9] :
( ( rtriangle(Vd9)
& vtriangle(Vd5,Vd6,Vd7) = Vd9 )
=> ( ? [Vd11] :
( rpoint(Vd11)
& Vd5 = Vd11 )
& ? [Vd12] :
( rpoint(Vd12)
& Vd6 = Vd12 )
& ? [Vd13] :
( rpoint(Vd13)
& Vd7 = Vd13 )
& Vd5 != Vd6
& Vd5 != Vd7
& Vd6 != Vd7 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd132) ).
fof(f132_nnf,plain,
! [Vd5,Vd6,Vd7,Vd9] :
( ( ? [Vd11] :
( rpoint(Vd11)
& Vd5 = Vd11 )
& ? [Vd12] :
( rpoint(Vd12)
& Vd6 = Vd12 )
& ? [Vd13] :
( rpoint(Vd13)
& Vd7 = Vd13 )
& Vd5 != Vd6
& Vd5 != Vd7
& Vd6 != Vd7 )
| ~ rtriangle(Vd9)
| vtriangle(Vd5,Vd6,Vd7) != Vd9 ),
inference(nnf_transformation,[status(thm)],[f132]) ).
fof(f132_sk,plain,
! [Vd5,Vd6,Vd7,Vd9] :
( ( rpoint(sk50(Vd5,Vd6,Vd7,Vd9))
& Vd5 = sk50(Vd5,Vd6,Vd7,Vd9)
& rpoint(sk49(Vd5,Vd6,Vd7,Vd9))
& Vd6 = sk49(Vd5,Vd6,Vd7,Vd9)
& rpoint(sk48(Vd5,Vd6,Vd7,Vd9))
& Vd7 = sk48(Vd5,Vd6,Vd7,Vd9)
& Vd5 != Vd6
& Vd5 != Vd7
& Vd6 != Vd7 )
| ~ rtriangle(Vd9)
| vtriangle(Vd5,Vd6,Vd7) != Vd9 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk48,sk49,sk50])],[f132_nnf]) ).
cnf(c256,plain,
( X1 != X2
| ~ rtriangle(X3)
| vtriangle(X0,X1,X2) != X3 ),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(c257,plain,
( X0 != X2
| ~ rtriangle(X3)
| vtriangle(X0,X1,X2) != X3 ),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(c258,plain,
( X0 != X1
| ~ rtriangle(X3)
| vtriangle(X0,X1,X2) != X3 ),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c2,c3,c8,c18,c19,c20,c29,c37,c49,c51,c59,c82,c83,c111,c134,c136,c143,c148,c149,c150,c170,c186,c187,c191,c192,c195,c214,c219,c220,c223,c228,c229,c232,c233,c236,c241,c242,c243,c244,c246,c247,c248,c250,c251,c253,c256,c257,c258]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t4453]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO300+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n020.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 : Wed Sep 23 11:52:47 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 61.72/8.27 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.72/8.27 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------