%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GEO299+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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 58.18s 8.27s
% Output : Proof 58.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 38
% Syntax : Number of formulae : 223 ( 98 unt; 0 def)
% Number of atoms : 1290 ( 581 equ)
% Maximal formula atoms : 23 ( 5 avg)
% Number of connectives : 1918 ( 851 ~; 657 |; 385 &)
% ( 0 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 38 ( 7 avg)
% Maximal term depth : 10 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 45 ( 45 usr; 19 con; 0-6 aty)
% Number of variables : 748 ( 3 sgn 391 !; 106 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,conjecture,
vf(vd1185,vd1187) = vplus(vf(vd1185,vd1201),vf(vd1201,vd1187)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd0) ).
fof(f0_neg,negated_conjecture,
vf(vd1185,vd1187) != vplus(vf(vd1185,vd1201),vf(vd1201,vd1187)),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
vf(vd1185,vd1187) != vplus(vf(vd1185,vd1201),vf(vd1201,vd1187)),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
vf(vd1185,vd1187) != vplus(vf(vd1185,vd1201),vf(vd1201,vd1187)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
vf(vd1185,vd1187) != vplus(vf(vd1185,vd1201),vf(vd1201,vd1187)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t190,plain,
eq(vf(vd1185,vd1187),vplus(vf(vd1185,vd1201),vf(vd1201,vd1187))) = false,
inference(equality_encoding,[status(esa)],[c0]) ).
fof(f66,axiom,
vd1199 = vd1185,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd66) ).
fof(f66_nnf,plain,
vd1199 = vd1185,
inference(nnf_transformation,[status(thm)],[f66]) ).
cnf(c98,plain,
vd1199 = vd1185,
inference(cnf_transformation,[status(esa)],[f66_nnf]) ).
cnf(t0,plain,
vd1199 = vd1185,
inference(equality_encoding,[status(esa)],[c98]) ).
cnf(t3565,plain,
vd1185 = vd1199,
inference(orient,[status(thm)],[t0]) ).
cnf(t5110,plain,
eq(vf(vd1199,vd1187),vplus(vf(vd1185,vd1201),vf(vd1201,vd1187))) = false,
inference(step,[status(thm)],[t190,t3565]) ).
fof(f56,axiom,
! [Vd761,Vd762] :
( ( ? [Vd764] :
( rpoint(Vd764)
& Vd761 = Vd764 )
& ? [Vd765] :
( rpoint(Vd765)
& Vd762 = Vd765 ) )
=> vf(Vd761,Vd762) = vf(Vd762,Vd761) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd56) ).
fof(f56_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)],[f56]) ).
fof(f56_sk,plain,
! [Vd762,Vd765,Vd761,Vd764] :
( vf(Vd761,Vd762) = vf(Vd762,Vd761)
| ~ rpoint(Vd764)
| Vd761 != Vd764
| ~ rpoint(Vd765)
| Vd762 != Vd765 ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c85,plain,
( vf(X0,X1) = vf(X1,X0)
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2 ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(hi72,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)],[c85]) ).
fof(f20,axiom,
? [Vd1205] :
( rpoint(Vd1205)
& vd1201 = Vd1205 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd20) ).
fof(f20_nnf,plain,
? [Vd1205] :
( rpoint(Vd1205)
& vd1201 = Vd1205 ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
( rpoint(sk0)
& vd1201 = sk0 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f20_nnf]) ).
cnf(c20,plain,
vd1201 = sk0,
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi16,axiom,
vd1201 = sk0,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(c21,plain,
rpoint(sk0),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi17,axiom,
rpoint(sk0) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
fof(f24,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/sandbox2/benchmark/theBenchmark.p',qtd24) ).
fof(f24_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)],[f24]) ).
fof(f24_sk,plain,
! [Vd1195] :
( rpoint(sk7)
& vd1178 = sk7
& rpoint(sk6)
& vd1179 = sk6
& rpoint(sk5)
& vd1180 = sk5
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& rpoint(sk4)
& vd1185 = sk4
& rpoint(sk3)
& vd1186 = sk3
& rpoint(sk2)
& vd1187 = sk2
& 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,[sk2,sk3,sk4,sk5,sk6,sk7])],[f24_nnf]) ).
cnf(c34,plain,
vd1185 = sk4,
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi28,axiom,
vd1185 = sk4,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(c35,plain,
rpoint(sk4),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi29,axiom,
rpoint(sk4) = true,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(t174,plain,
vf(vd1201,vd1185) = vf(vd1185,vd1201),
inference(hyper_resolution,[status(thm)],[hi72,hi16,hi17,hi28,hi29]) ).
cnf(t3216,plain,
vf(vd1185,vd1201) = vf(vd1201,vd1185),
inference(orient,[status(thm)],[t174]) ).
cnf(t5111,plain,
eq(vf(vd1199,vd1187),vplus(vf(vd1201,vd1185),vf(vd1201,vd1187))) = false,
inference(step,[status(thm)],[t5110,t3216]) ).
cnf(t5112,plain,
eq(vf(vd1199,vd1187),vplus(vf(vd1201,vd1199),vf(vd1201,vd1187))) = false,
inference(step,[status(thm)],[t5111,t3565]) ).
cnf(t4233,plain,
eq(vf(vd1199,vd1187),vplus(vf(vd1201,vd1199),vf(vd1201,vd1187))) = false,
inference(orient,[status(thm)],[t5112]) ).
fof(f80,axiom,
vf(vd1199,vd1201) = vf(vd1185,vd1187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd80) ).
fof(f80_nnf,plain,
vf(vd1199,vd1201) = vf(vd1185,vd1187),
inference(nnf_transformation,[status(thm)],[f80]) ).
cnf(c122,plain,
vf(vd1199,vd1201) = vf(vd1185,vd1187),
inference(cnf_transformation,[status(esa)],[f80_nnf]) ).
cnf(t172,plain,
vf(vd1199,vd1201) = vf(vd1185,vd1187),
inference(equality_encoding,[status(esa)],[c122]) ).
fof(f21,axiom,
? [Vd1203] :
( rpoint(Vd1203)
& vd1199 = Vd1203 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd21) ).
fof(f21_nnf,plain,
? [Vd1203] :
( rpoint(Vd1203)
& vd1199 = Vd1203 ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
( rpoint(sk1)
& vd1199 = sk1 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f21_nnf]) ).
cnf(c22,plain,
vd1199 = sk1,
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(hi18,axiom,
vd1199 = sk1,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(c23,plain,
rpoint(sk1),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(hi19,axiom,
rpoint(sk1) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t180,plain,
vf(vd1201,vd1199) = vf(vd1199,vd1201),
inference(hyper_resolution,[status(thm)],[hi72,hi16,hi17,hi18,hi19]) ).
cnf(t3190,plain,
vf(vd1199,vd1201) = vf(vd1201,vd1199),
inference(orient,[status(thm)],[t180]) ).
cnf(t5059,plain,
vf(vd1201,vd1199) = vf(vd1185,vd1187),
inference(step,[status(thm)],[t172,t3190]) ).
cnf(c30,plain,
vd1187 = sk2,
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi24,axiom,
vd1187 = sk2,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(c31,plain,
rpoint(sk2),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(hi25,axiom,
rpoint(sk2) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t159,plain,
vf(vd1187,vd1185) = vf(vd1185,vd1187),
inference(hyper_resolution,[status(thm)],[hi72,hi24,hi25,hi28,hi29]) ).
cnf(t3317,plain,
vf(vd1185,vd1187) = vf(vd1187,vd1185),
inference(orient,[status(thm)],[t159]) ).
cnf(t5060,plain,
vf(vd1201,vd1199) = vf(vd1187,vd1185),
inference(step,[status(thm)],[t5059,t3317]) ).
cnf(t3374,plain,
vf(vd1187,vd1185) = vf(vd1201,vd1199),
inference(orient,[status(thm)],[t5060]) ).
cnf(t5077,plain,
vf(vd1187,vd1199) = vf(vd1201,vd1199),
inference(step,[status(thm)],[t3374,t3565]) ).
cnf(t169,plain,
vf(vd1199,vd1187) = vf(vd1187,vd1199),
inference(hyper_resolution,[status(thm)],[hi72,hi18,hi19,hi24,hi25]) ).
cnf(t3291,plain,
vf(vd1187,vd1199) = vf(vd1199,vd1187),
inference(orient,[status(thm)],[t169]) ).
cnf(t5078,plain,
vf(vd1199,vd1187) = vf(vd1201,vd1199),
inference(step,[status(thm)],[t5077,t3291]) ).
cnf(t3566,plain,
vf(vd1199,vd1187) = vf(vd1201,vd1199),
inference(rw,[status(thm)],[t5078]) ).
cnf(t4275,plain,
vf(vd1199,vd1187) = vf(vd1201,vd1199),
inference(orient,[status(thm)],[t3566]) ).
cnf(t5119,plain,
eq(vf(vd1201,vd1199),vplus(vf(vd1201,vd1199),vf(vd1201,vd1187))) = false,
inference(step,[status(thm)],[t4233,t4275]) ).
cnf(t4300,plain,
eq(vf(vd1201,vd1199),vplus(vf(vd1201,vd1199),vf(vd1201,vd1187))) = false,
inference(rw,[status(thm)],[t5119]) ).
fof(f6,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/sandbox2/benchmark/theBenchmark.p',qtd6) ).
fof(f6_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)],[f6]) ).
fof(f6_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)],[f6_nnf]) ).
cnf(c6,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)],[f6_sk]) ).
cnf(hi2,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)],[c6]) ).
fof(f1,axiom,
rR(vd1201,vd1185,vd1187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd1) ).
fof(f1_nnf,plain,
rR(vd1201,vd1185,vd1187),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
rR(vd1201,vd1185,vd1187),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(hi0,axiom,
rR(vd1201,vd1185,vd1187) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t189,plain,
vplus(vf(vd1185,vd1201),vf(vd1201,vd1187)) = vf(vd1185,vd1187),
inference(hyper_resolution,[status(thm)],[hi2,hi0,hi24,hi25,hi16,hi17,hi28,hi29]) ).
cnf(t5068,plain,
vplus(vf(vd1201,vd1185),vf(vd1201,vd1187)) = vf(vd1185,vd1187),
inference(step,[status(thm)],[t189,t3216]) ).
cnf(t5061,plain,
vf(vd1185,vd1187) = vf(vd1201,vd1199),
inference(step,[status(thm)],[t3317,t3374]) ).
cnf(t3375,plain,
vf(vd1185,vd1187) = vf(vd1201,vd1199),
inference(orient,[status(thm)],[t5061]) ).
cnf(t5069,plain,
vplus(vf(vd1201,vd1185),vf(vd1201,vd1187)) = vf(vd1201,vd1199),
inference(step,[status(thm)],[t5068,t3375]) ).
cnf(t3476,plain,
vplus(vf(vd1201,vd1185),vf(vd1201,vd1187)) = vf(vd1201,vd1199),
inference(orient,[status(thm)],[t5069]) ).
cnf(t5082,plain,
vplus(vf(vd1201,vd1199),vf(vd1201,vd1187)) = vf(vd1201,vd1199),
inference(step,[status(thm)],[t3476,t3565]) ).
cnf(t3570,plain,
vplus(vf(vd1201,vd1199),vf(vd1201,vd1187)) = vf(vd1201,vd1199),
inference(rw,[status(thm)],[t5082]) ).
cnf(t4413,plain,
vplus(vf(vd1201,vd1199),vf(vd1201,vd1187)) = vf(vd1201,vd1199),
inference(orient,[status(thm)],[t3570]) ).
cnf(t5159,plain,
eq(vf(vd1201,vd1199),vf(vd1201,vd1199)) = false,
inference(step,[status(thm)],[t4300,t4413]) ).
cnf(t1,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t2537,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t5160,plain,
true = false,
inference(step,[status(thm)],[t5159,t2537]) ).
cnf(t5032,plain,
false = true,
inference(orient,[status(thm)],[t5160]) ).
fof(f3,axiom,
vd1201 != vd1187,
file('/export/starexec/sandbox2/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]) ).
fof(f4,axiom,
~ rR(vd1185,vd1201,vd1187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd4) ).
fof(f4_nnf,plain,
~ rR(vd1185,vd1201,vd1187),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
~ rR(vd1185,vd1201,vd1187),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
~ rR(vd1185,vd1201,vd1187),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
fof(f5,axiom,
~ rR(vd1185,vd1201,vd1187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd5) ).
fof(f5_nnf,plain,
~ rR(vd1185,vd1201,vd1187),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
~ rR(vd1185,vd1201,vd1187),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
~ rR(vd1185,vd1201,vd1187),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f22,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd22) ).
fof(f22_nnf,plain,
~ ron(vd1187,vd1197),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
~ ron(vd1187,vd1197),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c24,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(c26,plain,
( ~ rline(X0)
| ~ ron(vd1185,X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1187,X0) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(c36,plain,
vd1179 != vd1180,
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(c37,plain,
vd1178 != vd1180,
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(c38,plain,
vd1178 != vd1179,
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
fof(f31,axiom,
! [Vd713,Vd714] :
( ( rreal(Vd714)
& Vd713 = Vd714 )
=> ~ rless(Vd713,Vd713) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd31) ).
fof(f31_nnf,plain,
! [Vd713,Vd714] :
( ~ rless(Vd713,Vd713)
| ~ rreal(Vd714)
| Vd713 != Vd714 ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [Vd713,Vd714] :
( ~ rless(Vd713,Vd713)
| ~ rreal(Vd714)
| Vd713 != Vd714 ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c59,plain,
( ~ rless(X0,X0)
| ~ rreal(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
fof(f33,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/sandbox2/benchmark/theBenchmark.p',qtd33) ).
fof(f33_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)],[f33]) ).
fof(f33_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)],[f33_nnf]) ).
cnf(c61,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)],[f33_sk]) ).
fof(f34,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/sandbox2/benchmark/theBenchmark.p',qtd34) ).
fof(f34_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)],[f34]) ).
fof(f34_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)],[f34_nnf]) ).
cnf(c62,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)],[f34_sk]) ).
fof(f43,axiom,
~ rR(vd1186,vd1199,vd1185),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd43) ).
fof(f43_nnf,plain,
~ rR(vd1186,vd1199,vd1185),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
~ rR(vd1186,vd1199,vd1185),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c71,plain,
~ rR(vd1186,vd1199,vd1185),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
fof(f76,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/sandbox2/benchmark/theBenchmark.p',qtd76) ).
fof(f76_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)],[f76]) ).
fof(f76_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)],[f76_nnf]) ).
cnf(c108,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)],[f76_sk]) ).
cnf(c109,plain,
( X0 != X2
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X1,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
cnf(c110,plain,
( X0 != X1
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X1,X0,X2) ),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
fof(f98,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/sandbox2/benchmark/theBenchmark.p',qtd98) ).
fof(f98_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)],[f98]) ).
fof(f98_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)],[f98_nnf]) ).
cnf(c152,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)],[f98_sk]) ).
fof(f106,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/sandbox2/benchmark/theBenchmark.p',qtd106) ).
fof(f106_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)],[f106]) ).
fof(f106_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)],[f106_nnf]) ).
cnf(c160,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)],[f106_sk]) ).
fof(f110,axiom,
! [Vd336,Vd337,Vd338,Vd339] :
( ( rpoint(Vd337)
& Vd336 = Vd337
& rcircle(Vd339)
& Vd338 = Vd339
& rinside(Vd336,Vd338) )
=> ~ ron(Vd336,Vd338) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd110) ).
fof(f110_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)],[f110]) ).
fof(f110_sk,plain,
! [Vd336,Vd338,Vd339,Vd337] :
( ~ ron(Vd336,Vd338)
| ~ rpoint(Vd337)
| Vd336 != Vd337
| ~ rcircle(Vd339)
| Vd338 != Vd339
| ~ rinside(Vd336,Vd338) ),
inference(skolemisation,[status(esa)],[f110_nnf]) ).
cnf(c164,plain,
( ~ ron(X0,X2)
| ~ rpoint(X1)
| X0 != X1
| ~ rcircle(X3)
| X2 != X3
| ~ rinside(X0,X2) ),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
fof(f115,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/sandbox2/benchmark/theBenchmark.p',qtd115) ).
fof(f115_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)],[f115]) ).
fof(f115_sk,plain,
! [Vd280,Vd281,Vd284,Vd283] :
( ( rpoint(sk20(Vd280,Vd281))
& ron(sk20(Vd280,Vd281),Vd280)
& ron(sk20(Vd280,Vd281),Vd281)
& rpoint(sk21(Vd280,Vd281))
& ron(sk21(Vd280,Vd281),Vd280)
& ron(sk21(Vd280,Vd281),Vd281)
& sk20(Vd280,Vd281) != sk21(Vd280,Vd281) )
| ~ rcircle(Vd283)
| Vd280 != Vd283
| ~ rcircle(Vd284)
| Vd281 != Vd284
| ~ rintersect(Vd280,Vd281) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk20,sk21])],[f115_nnf]) ).
cnf(c175,plain,
( sk20(X0,X1) != sk21(X0,X1)
| ~ rcircle(X3)
| X0 != X3
| ~ rcircle(X2)
| X1 != X2
| ~ rintersect(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f115_sk]) ).
fof(f118,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/sandbox2/benchmark/theBenchmark.p',qtd118) ).
fof(f118_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)],[f118]) ).
fof(f118_sk,plain,
! [Vd246,Vd244,Vd247,Vd245] :
( ( rpoint(sk24(Vd244,Vd245,Vd246,Vd247))
& ron(sk24(Vd244,Vd245,Vd246,Vd247),Vd246)
& ron(sk24(Vd244,Vd245,Vd246,Vd247),Vd244)
& rpoint(sk25(Vd244,Vd245,Vd246,Vd247))
& ron(sk25(Vd244,Vd245,Vd246,Vd247),Vd246)
& ron(sk25(Vd244,Vd245,Vd246,Vd247),Vd244)
& sk24(Vd244,Vd245,Vd246,Vd247) != sk25(Vd244,Vd245,Vd246,Vd247) )
| ~ rcircle(Vd245)
| Vd244 != Vd245
| ~ rline(Vd247)
| Vd246 != Vd247
| ~ rintersect(Vd246,Vd244) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk24,sk25])],[f118_nnf]) ).
cnf(c189,plain,
( sk24(X0,X1,X2,X3) != sk25(X0,X1,X2,X3)
| ~ rcircle(X1)
| X0 != X1
| ~ rline(X3)
| X2 != X3
| ~ rintersect(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f118_sk]) ).
fof(f121,axiom,
! [Vd214,Vd215] :
( ( rcircle(Vd215)
& Vd214 = Vd215 )
=> ? [Vd216] :
( rpoint(Vd216)
& ~ rinside(Vd216,Vd214)
& ~ ron(Vd216,Vd214) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd121) ).
fof(f121_nnf,plain,
! [Vd214,Vd215] :
( ? [Vd216] :
( rpoint(Vd216)
& ~ rinside(Vd216,Vd214)
& ~ ron(Vd216,Vd214) )
| ~ rcircle(Vd215)
| Vd214 != Vd215 ),
inference(nnf_transformation,[status(thm)],[f121]) ).
fof(f121_sk,plain,
! [Vd214,Vd215] :
( ( rpoint(sk28(Vd214,Vd215))
& ~ rinside(sk28(Vd214,Vd215),Vd214)
& ~ ron(sk28(Vd214,Vd215),Vd214) )
| ~ rcircle(Vd215)
| Vd214 != Vd215 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk28])],[f121_nnf]) ).
cnf(c202,plain,
( ~ ron(sk28(X0,X1),X0)
| ~ rcircle(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
cnf(c203,plain,
( ~ rinside(sk28(X0,X1),X0)
| ~ rcircle(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
fof(f123,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/sandbox2/benchmark/theBenchmark.p',qtd123) ).
fof(f123_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)],[f123]) ).
fof(f123_sk,plain,
! [Vd203,Vd200,Vd202,Vd206,Vd205,Vd201] :
( ( rpoint(sk30(Vd200,Vd201,Vd202,Vd203))
& ron(sk30(Vd200,Vd201,Vd202,Vd203),Vd200)
& sk30(Vd200,Vd201,Vd202,Vd203) != Vd202
& sk30(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,[sk30])],[f123_nnf]) ).
cnf(c207,plain,
( sk30(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)],[f123_sk]) ).
cnf(c208,plain,
( sk30(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)],[f123_sk]) ).
fof(f124,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/sandbox2/benchmark/theBenchmark.p',qtd124) ).
fof(f124_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)],[f124]) ).
fof(f124_sk,plain,
! [Vd196,Vd194,Vd197,Vd195] :
( ( rpoint(sk31(Vd194,Vd195,Vd196,Vd197))
& ron(sk31(Vd194,Vd195,Vd196,Vd197),Vd194)
& sk31(Vd194,Vd195,Vd196,Vd197) != Vd196 )
| ~ rcircle(Vd195)
| Vd194 != Vd195
| ~ rpoint(Vd197)
| Vd196 != Vd197
| ~ ron(Vd196,Vd194) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk31])],[f124_nnf]) ).
cnf(c211,plain,
( sk31(X0,X1,X2,X3) != X2
| ~ rcircle(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
fof(f130,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/sandbox2/benchmark/theBenchmark.p',qtd130) ).
fof(f130_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)],[f130]) ).
fof(f130_sk,plain,
! [Vd146,Vd147,Vd141,Vd140,Vd138,Vd144,Vd143,Vd139] :
( ( rpoint(sk37(Vd138,Vd139,Vd140,Vd141,Vd146,Vd147))
& rR(Vd141,Vd140,sk37(Vd138,Vd139,Vd140,Vd141,Vd146,Vd147))
& sk37(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,[sk37])],[f130_nnf]) ).
cnf(c230,plain,
( sk37(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)],[f130_sk]) ).
fof(f132,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/sandbox2/benchmark/theBenchmark.p',qtd132) ).
fof(f132_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)],[f132]) ).
fof(f132_sk,plain,
! [Vd114,Vd111,Vd112,Vd113,Vd109,Vd119,Vd118,Vd117,Vd116,Vd110] :
( ( rpoint(sk39(Vd109,Vd110,Vd111,Vd112,Vd113,Vd114))
& rR(sk39(Vd109,Vd110,Vd111,Vd112,Vd113,Vd114),Vd111,Vd112)
& sk39(Vd109,Vd110,Vd111,Vd112,Vd113,Vd114) != Vd113
& sk39(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,[sk39])],[f132_nnf]) ).
cnf(c235,plain,
( sk39(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)],[f132_sk]) ).
cnf(c236,plain,
( sk39(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)],[f132_sk]) ).
fof(f133,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/sandbox2/benchmark/theBenchmark.p',qtd133) ).
fof(f133_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)],[f133]) ).
fof(f133_sk,plain,
! [Vd99,Vd97,Vd98,Vd95,Vd103,Vd102,Vd101,Vd96] :
( ( rpoint(sk40(Vd95,Vd96,Vd97,Vd98,Vd99))
& rR(sk40(Vd95,Vd96,Vd97,Vd98,Vd99),Vd97,Vd98)
& sk40(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,[sk40])],[f133_nnf]) ).
cnf(c239,plain,
( sk40(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)],[f133_sk]) ).
fof(f135,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/sandbox2/benchmark/theBenchmark.p',qtd135) ).
fof(f135_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)],[f135]) ).
fof(f135_sk,plain,
! [Vd75,Vd71,Vd74,Vd73,Vd79,Vd78,Vd77,Vd72] :
( ( rpoint(sk42(Vd71,Vd72,Vd73,Vd74,Vd75))
& ron(sk42(Vd71,Vd72,Vd73,Vd74,Vd75),Vd71)
& sk42(Vd71,Vd72,Vd73,Vd74,Vd75) != Vd73
& sk42(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,[sk42])],[f135_nnf]) ).
cnf(c244,plain,
( sk42(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)],[f135_sk]) ).
cnf(c245,plain,
( sk42(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)],[f135_sk]) ).
fof(f136,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/sandbox2/benchmark/theBenchmark.p',qtd136) ).
fof(f136_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)],[f136]) ).
fof(f136_sk,plain,
! [Vd65,Vd61,Vd63,Vd66,Vd64,Vd62] :
( ( rpoint(sk43(Vd61,Vd62,Vd63,Vd64,Vd65,Vd66))
& ron(sk43(Vd61,Vd62,Vd63,Vd64,Vd65,Vd66),Vd61)
& sk43(Vd61,Vd62,Vd63,Vd64,Vd65,Vd66) != Vd63
& sk43(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,[sk43])],[f136_nnf]) ).
cnf(c248,plain,
( sk43(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)],[f136_sk]) ).
cnf(c249,plain,
( sk43(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)],[f136_sk]) ).
fof(f137,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/sandbox2/benchmark/theBenchmark.p',qtd137) ).
fof(f137_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)],[f137]) ).
fof(f137_sk,plain,
! [Vd57,Vd55,Vd58,Vd56] :
( ( rpoint(sk44(Vd55,Vd56,Vd57,Vd58))
& ron(sk44(Vd55,Vd56,Vd57,Vd58),Vd55)
& sk44(Vd55,Vd56,Vd57,Vd58) != Vd57 )
| ~ rline(Vd56)
| Vd55 != Vd56
| ~ rpoint(Vd58)
| Vd57 != Vd58
| ~ ron(Vd57,Vd55) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk44])],[f137_nnf]) ).
cnf(c252,plain,
( sk44(X0,X1,X2,X3) != X2
| ~ rline(X1)
| X0 != X1
| ~ rpoint(X3)
| X2 != X3
| ~ ron(X2,X0) ),
inference(cnf_transformation,[status(esa)],[f137_sk]) ).
fof(f139,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/sandbox2/benchmark/theBenchmark.p',qtd139) ).
fof(f139_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)],[f139]) ).
fof(f139_sk,plain,
! [Vd41,Vd46,Vd40,Vd45,Vd39,Vd44,Vd38,Vd43] :
( ( rpoint(sk46(Vd38,Vd39,Vd40,Vd41))
& sk46(Vd38,Vd39,Vd40,Vd41) != Vd38
& sk46(Vd38,Vd39,Vd40,Vd41) != Vd39
& sk46(Vd38,Vd39,Vd40,Vd41) != Vd40
& sk46(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,[sk46])],[f139_nnf]) ).
cnf(c257,plain,
( sk46(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)],[f139_sk]) ).
cnf(c258,plain,
( sk46(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)],[f139_sk]) ).
cnf(c259,plain,
( sk46(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)],[f139_sk]) ).
cnf(c260,plain,
( sk46(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)],[f139_sk]) ).
fof(f140,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/sandbox2/benchmark/theBenchmark.p',qtd140) ).
fof(f140_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)],[f140]) ).
fof(f140_sk,plain,
! [Vd29,Vd33,Vd28,Vd32,Vd27,Vd31] :
( ( rpoint(sk47(Vd27,Vd28,Vd29))
& sk47(Vd27,Vd28,Vd29) != Vd27
& sk47(Vd27,Vd28,Vd29) != Vd28
& sk47(Vd27,Vd28,Vd29) != Vd29 )
| ~ rpoint(Vd31)
| Vd27 != Vd31
| ~ rpoint(Vd32)
| Vd28 != Vd32
| ~ rpoint(Vd33)
| Vd29 != Vd33 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk47])],[f140_nnf]) ).
cnf(c262,plain,
( sk47(X0,X1,X2) != X2
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3 ),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
cnf(c263,plain,
( sk47(X0,X1,X2) != X1
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3 ),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
cnf(c264,plain,
( sk47(X0,X1,X2) != X0
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3 ),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
fof(f141,axiom,
! [Vd19,Vd20] :
( ( ? [Vd22] :
( rpoint(Vd22)
& Vd19 = Vd22 )
& ? [Vd23] :
( rpoint(Vd23)
& Vd20 = Vd23 ) )
=> ? [Vd24] :
( rpoint(Vd24)
& Vd24 != Vd19
& Vd24 != Vd20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd141) ).
fof(f141_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)],[f141]) ).
fof(f141_sk,plain,
! [Vd20,Vd23,Vd19,Vd22] :
( ( rpoint(sk48(Vd19,Vd20))
& sk48(Vd19,Vd20) != Vd19
& sk48(Vd19,Vd20) != Vd20 )
| ~ rpoint(Vd22)
| Vd19 != Vd22
| ~ rpoint(Vd23)
| Vd20 != Vd23 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk48])],[f141_nnf]) ).
cnf(c266,plain,
( sk48(X0,X1) != X1
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2 ),
inference(cnf_transformation,[status(esa)],[f141_sk]) ).
cnf(c267,plain,
( sk48(X0,X1) != X0
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2 ),
inference(cnf_transformation,[status(esa)],[f141_sk]) ).
fof(f142,axiom,
! [Vd15,Vd16] :
( ( rpoint(Vd16)
& Vd15 = Vd16 )
=> ? [Vd17] :
( rpoint(Vd17)
& Vd17 != Vd15 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd142) ).
fof(f142_nnf,plain,
! [Vd15,Vd16] :
( ? [Vd17] :
( rpoint(Vd17)
& Vd17 != Vd15 )
| ~ rpoint(Vd16)
| Vd15 != Vd16 ),
inference(nnf_transformation,[status(thm)],[f142]) ).
fof(f142_sk,plain,
! [Vd15,Vd16] :
( ( rpoint(sk49(Vd15,Vd16))
& sk49(Vd15,Vd16) != Vd15 )
| ~ rpoint(Vd16)
| Vd15 != Vd16 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk49])],[f142_nnf]) ).
cnf(c269,plain,
( sk49(X0,X1) != X0
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f142_sk]) ).
fof(f144,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/sandbox2/benchmark/theBenchmark.p',qtd144) ).
fof(f144_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)],[f144]) ).
fof(f144_sk,plain,
! [Vd5,Vd6,Vd7,Vd9] :
( ( rpoint(sk52(Vd5,Vd6,Vd7,Vd9))
& Vd5 = sk52(Vd5,Vd6,Vd7,Vd9)
& rpoint(sk51(Vd5,Vd6,Vd7,Vd9))
& Vd6 = sk51(Vd5,Vd6,Vd7,Vd9)
& rpoint(sk50(Vd5,Vd6,Vd7,Vd9))
& Vd7 = sk50(Vd5,Vd6,Vd7,Vd9)
& Vd5 != Vd6
& Vd5 != Vd7
& Vd6 != Vd7 )
| ~ rtriangle(Vd9)
| vtriangle(Vd5,Vd6,Vd7) != Vd9 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk50,sk51,sk52])],[f144_nnf]) ).
cnf(c272,plain,
( X1 != X2
| ~ rtriangle(X3)
| vtriangle(X0,X1,X2) != X3 ),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
cnf(c273,plain,
( X0 != X2
| ~ rtriangle(X3)
| vtriangle(X0,X1,X2) != X3 ),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
cnf(c274,plain,
( X0 != X1
| ~ rtriangle(X3)
| vtriangle(X0,X1,X2) != X3 ),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c3,c4,c5,c24,c26,c36,c37,c38,c59,c61,c62,c71,c108,c109,c110,c152,c160,c164,c175,c189,c202,c203,c207,c208,c211,c230,c235,c236,c239,c244,c245,c248,c249,c252,c257,c258,c259,c260,c262,c263,c264,c266,c267,c269,c272,c273,c274]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t5032]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO299+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 11:46:31 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 58.18/8.27 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.18/8.27 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------