%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO290+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 : Thu Sep 24 12:24:50 PM UTC 2026
% Result : Theorem 0.13s 5.55s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 63
% Syntax : Number of formulae : 318 ( 116 unt; 42 def)
% Number of atoms : 1138 ( 323 equ)
% Maximal formula atoms : 26 ( 3 avg)
% Number of connectives : 1441 ( 621 ~; 637 |; 134 &)
% ( 44 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 42 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 21 con; 0-3 aty)
% Number of variables : 289 ( 255 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( rR(vd1185,vd1199,vd1186)
| rR(vd1199,vd1185,vd1186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ( rR(vd1185,vd1199,vd1186)
| rR(vd1199,vd1185,vd1186) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vd1199 != vd1185,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
ron(vd1185,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
ron(vd1200,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
ron(vd1199,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
vd1200 = vd1186,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Vd396,Vd397,Vd398,Vd403,Vd404] :
( ( ? [Vd400] :
( rpoint(Vd400)
& Vd396 = Vd400 )
& ? [Vd401] :
( rpoint(Vd401)
& Vd397 = Vd401 )
& ? [Vd402] :
( rpoint(Vd402)
& Vd398 = Vd402 )
& Vd396 != Vd397
& Vd396 != Vd398
& Vd397 != Vd398
& rline(Vd404)
& ron(Vd396,Vd403)
& ron(Vd397,Vd403)
& ron(Vd398,Vd403)
& Vd403 = Vd404 )
=> ( rR(Vd398,Vd396,Vd397)
| rR(Vd396,Vd397,Vd398)
| rR(Vd397,Vd396,Vd398) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
vf(vd1199,vd1200) = vf(vd1185,vd1186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
rline(vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
~ rR(vd1186,vd1199,vd1185),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
ron(vd1199,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
? [Vd1205] :
( rpoint(Vd1205)
& vd1201 = Vd1205 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
? [Vd1204] :
( rpoint(Vd1204)
& vd1200 = Vd1204 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
? [Vd1203] :
( rpoint(Vd1203)
& vd1199 = Vd1203 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,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') ).
fof(f31,axiom,
! [Vd748,Vd749] :
( ( ? [Vd751] :
( rpoint(Vd751)
& Vd748 = Vd751 )
& ? [Vd752] :
( rpoint(Vd752)
& Vd749 = Vd752 ) )
=> ( vf(Vd748,Vd749) = v0
<=> Vd748 = Vd749 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [Vd908,Vd909,Vd910,Vd911,Vd912,Vd919,Vd920] :
( ( ? [Vd914] :
( rpoint(Vd914)
& Vd908 = Vd914 )
& ? [Vd915] :
( rpoint(Vd915)
& Vd909 = Vd915 )
& ? [Vd916] :
( rpoint(Vd916)
& Vd910 = Vd916 )
& ? [Vd917] :
( rpoint(Vd917)
& Vd911 = Vd917 )
& ? [Vd918] :
( rpoint(Vd918)
& Vd912 = Vd918 )
& ? [Vd922] :
( rline(Vd922)
& Vd919 = Vd922 )
& ? [Vd923] :
( rline(Vd923)
& Vd920 = Vd923 )
& ron(Vd908,Vd919)
& ron(Vd909,Vd919)
& ron(Vd911,Vd919)
& ron(Vd910,Vd920)
& ron(Vd912,Vd920)
& Vd909 != Vd908
& Vd910 != Vd908
& Vd911 != Vd908
& Vd912 != Vd908
& ~ rR(Vd908,Vd909,Vd911)
& ~ rR(Vd908,Vd910,Vd912) )
=> vangle(Vd909,Vd908,Vd910) = vangle(Vd911,Vd908,Vd912) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [Vd594,Vd595,Vd596,Vd601,Vd602,Vd603,Vd604] :
( ( ? [Vd598] :
( rpoint(Vd598)
& Vd594 = Vd598 )
& ? [Vd599] :
( rpoint(Vd599)
& Vd595 = Vd599 )
& ? [Vd600] :
( rpoint(Vd600)
& Vd596 = Vd600 )
& rline(Vd602)
& Vd601 = Vd602
& rcircle(Vd604)
& Vd603 = Vd604
& ( rinside(Vd594,Vd603)
| ron(Vd594,Vd603) )
& ( rinside(Vd595,Vd603)
| ron(Vd595,Vd603) )
& rR(Vd596,Vd594,Vd595) )
=> rinside(Vd596,Vd603) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,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') ).
fof(f137,plain,
( ~ rR(vd1185,vd1199,vd1186)
& ~ rR(vd1199,vd1185,vd1186) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f138,plain,
~ rR(vd1199,vd1185,vd1186),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
~ rR(vd1185,vd1199,vd1186),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f140,plain,
vd1199 != vd1185,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f141,plain,
ron(vd1185,vd1197),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f142,plain,
ron(vd1200,vd1197),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f144,plain,
ron(vd1199,vd1197),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f145,plain,
vd1200 = vd1186,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f147,plain,
! [Vd396,Vd397,Vd398,Vd403,Vd404] :
( rR(Vd398,Vd396,Vd397)
| rR(Vd396,Vd397,Vd398)
| rR(Vd397,Vd396,Vd398)
| ! [Vd400] :
( ~ rpoint(Vd400)
| Vd396 != Vd400 )
| ! [Vd401] :
( ~ rpoint(Vd401)
| Vd397 != Vd401 )
| ! [Vd402] :
( ~ rpoint(Vd402)
| Vd398 != Vd402 )
| Vd396 = Vd397
| Vd396 = Vd398
| Vd397 = Vd398
| ~ rline(Vd404)
| ~ ron(Vd396,Vd403)
| ~ ron(Vd397,Vd403)
| ~ ron(Vd398,Vd403)
| Vd403 != Vd404 ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f148,plain,
! [Vd396,Vd397,Vd398] :
( rR(Vd398,Vd396,Vd397)
| rR(Vd396,Vd397,Vd398)
| rR(Vd397,Vd396,Vd398)
| ! [Vd400] :
( ~ rpoint(Vd400)
| Vd396 != Vd400 )
| ! [Vd401] :
( ~ rpoint(Vd401)
| Vd397 != Vd401 )
| ! [Vd402] :
( ~ rpoint(Vd402)
| Vd398 != Vd402 )
| Vd396 = Vd397
| Vd396 = Vd398
| Vd397 = Vd398
| ! [Vd404] :
( ~ rline(Vd404)
| ! [Vd403] :
( ~ ron(Vd396,Vd403)
| ~ ron(Vd397,Vd403)
| ~ ron(Vd398,Vd403)
| Vd403 != Vd404 ) ) ),
inference(miniscoping,[status(thm)],[f147]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rR(X2,X4,X3)
| rR(X4,X3,X2)
| rR(X3,X4,X2)
| ~ rpoint(X7)
| X4 != X7
| ~ rpoint(X6)
| X3 != X6
| ~ rpoint(X5)
| X2 != X5
| X4 = X3
| X4 = X2
| X3 = X2
| ~ rline(X1)
| ~ ron(X4,X0)
| ~ ron(X3,X0)
| ~ ron(X2,X0)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
vf(vd1199,vd1200) = vf(vd1185,vd1186),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f152,plain,
rline(vd1197),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f154,plain,
~ rR(vd1186,vd1199,vd1185),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f155,plain,
ron(vd1199,vd1197),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f162,plain,
( rpoint(sK0_skl)
& vd1201 = sK0_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1205,sK0_skl)],[f23]) ).
fof(f164,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f162]) ).
fof(f165,plain,
( rpoint(sK1_skl)
& vd1200 = sK1_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Vd1204,sK1_skl)],[f24]) ).
fof(f166,plain,
vd1200 = sK1_skl,
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f167,plain,
rpoint(sK1_skl),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f168,plain,
( rpoint(sK2_skl)
& vd1199 = sK2_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Vd1203,sK2_skl)],[f25]) ).
fof(f169,plain,
vd1199 = sK2_skl,
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f170,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f171,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f172,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(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f173,plain,
( rpoint(sK8_skl)
& vd1178 = sK8_skl
& rpoint(sK7_skl)
& vd1179 = sK7_skl
& rpoint(sK6_skl)
& vd1180 = sK6_skl
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& rpoint(sK5_skl)
& vd1185 = sK5_skl
& rpoint(sK4_skl)
& vd1186 = sK4_skl
& rpoint(sK3_skl)
& vd1187 = sK3_skl
& 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(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(Vd1191,sK3_skl),skolemize(Vd1190,sK4_skl),skolemize(Vd1189,sK5_skl),skolemize(Vd1184,sK6_skl),skolemize(Vd1183,sK7_skl),skolemize(Vd1182,sK8_skl)],[f172]) ).
fof(f175,plain,
vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f176,plain,
vf(vd1178,vd1180) = vf(vd1185,vd1187),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f177,plain,
vf(vd1178,vd1179) = vf(vd1185,vd1186),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f178,plain,
vd1187 = sK3_skl,
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f179,plain,
rpoint(sK3_skl),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f180,plain,
vd1186 = sK4_skl,
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f181,plain,
rpoint(sK4_skl),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f182,plain,
vd1185 = sK5_skl,
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f183,plain,
rpoint(sK5_skl),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f184,plain,
vd1179 != vd1180,
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f186,plain,
vd1178 != vd1179,
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f187,plain,
vd1180 = sK6_skl,
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f188,plain,
rpoint(sK6_skl),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f189,plain,
vd1179 = sK7_skl,
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f190,plain,
rpoint(sK7_skl),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f191,plain,
vd1178 = sK8_skl,
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f192,plain,
rpoint(sK8_skl),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f199,plain,
! [Vd748,Vd749] :
( ( vf(Vd748,Vd749) = v0
<=> Vd748 = Vd749 )
| ! [Vd751] :
( ~ rpoint(Vd751)
| Vd748 != Vd751 )
| ! [Vd752] :
( ~ rpoint(Vd752)
| Vd749 != Vd752 ) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f200,plain,
! [Vd748,Vd749] :
( ( ( Vd748 != Vd749
| vf(Vd748,Vd749) = v0 )
& ( Vd748 = Vd749
| vf(Vd748,Vd749) != v0 ) )
| ! [Vd751] :
( ~ rpoint(Vd751)
| Vd748 != Vd751 )
| ! [Vd752] :
( ~ rpoint(Vd752)
| Vd749 != Vd752 ) ),
inference(NNF_transformation,[status(thm)],[f199]) ).
fof(f201,plain,
! [X0,X1,X2,X3] :
( X2 = X0
| vf(X2,X0) != v0
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [X0,X1,X2,X3] :
( X2 != X0
| vf(X2,X0) = v0
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f313,plain,
! [Vd908,Vd909,Vd910,Vd911,Vd912,Vd919,Vd920] :
( vangle(Vd909,Vd908,Vd910) = vangle(Vd911,Vd908,Vd912)
| ! [Vd914] :
( ~ rpoint(Vd914)
| Vd908 != Vd914 )
| ! [Vd915] :
( ~ rpoint(Vd915)
| Vd909 != Vd915 )
| ! [Vd916] :
( ~ rpoint(Vd916)
| Vd910 != Vd916 )
| ! [Vd917] :
( ~ rpoint(Vd917)
| Vd911 != Vd917 )
| ! [Vd918] :
( ~ rpoint(Vd918)
| Vd912 != Vd918 )
| ! [Vd922] :
( ~ rline(Vd922)
| Vd919 != Vd922 )
| ! [Vd923] :
( ~ rline(Vd923)
| Vd920 != Vd923 )
| ~ ron(Vd908,Vd919)
| ~ ron(Vd909,Vd919)
| ~ ron(Vd911,Vd919)
| ~ ron(Vd910,Vd920)
| ~ ron(Vd912,Vd920)
| Vd909 = Vd908
| Vd910 = Vd908
| Vd911 = Vd908
| Vd912 = Vd908
| rR(Vd908,Vd909,Vd911)
| rR(Vd908,Vd910,Vd912) ),
inference(pre_NNF_transformation,[status(thm)],[f60]) ).
fof(f314,plain,
! [Vd908,Vd909,Vd910,Vd911,Vd912] :
( vangle(Vd909,Vd908,Vd910) = vangle(Vd911,Vd908,Vd912)
| ! [Vd914] :
( ~ rpoint(Vd914)
| Vd908 != Vd914 )
| ! [Vd915] :
( ~ rpoint(Vd915)
| Vd909 != Vd915 )
| ! [Vd916] :
( ~ rpoint(Vd916)
| Vd910 != Vd916 )
| ! [Vd917] :
( ~ rpoint(Vd917)
| Vd911 != Vd917 )
| ! [Vd918] :
( ~ rpoint(Vd918)
| Vd912 != Vd918 )
| ! [Vd919] :
( ! [Vd922] :
( ~ rline(Vd922)
| Vd919 != Vd922 )
| ! [Vd920] :
( ! [Vd923] :
( ~ rline(Vd923)
| Vd920 != Vd923 )
| ~ ron(Vd908,Vd919)
| ~ ron(Vd909,Vd919)
| ~ ron(Vd911,Vd919)
| ~ ron(Vd910,Vd920)
| ~ ron(Vd912,Vd920)
| Vd909 = Vd908
| Vd910 = Vd908
| Vd911 = Vd908
| Vd912 = Vd908
| rR(Vd908,Vd909,Vd911)
| rR(Vd908,Vd910,Vd912) ) ) ),
inference(miniscoping,[status(thm)],[f313]) ).
fof(f315,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13] :
( vangle(X3,X0,X1) = vangle(X4,X0,X2)
| ~ rpoint(X13)
| X0 != X13
| ~ rpoint(X12)
| X3 != X12
| ~ rpoint(X11)
| X1 != X11
| ~ rpoint(X10)
| X4 != X10
| ~ rpoint(X9)
| X2 != X9
| ~ rline(X8)
| X6 != X8
| ~ rline(X7)
| X5 != X7
| ~ ron(X0,X6)
| ~ ron(X3,X6)
| ~ ron(X4,X6)
| ~ ron(X1,X5)
| ~ ron(X2,X5)
| X3 = X0
| X1 = X0
| X4 = X0
| X2 = X0
| rR(X0,X3,X4)
| rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f345,plain,
v0 = vd684,
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f369,plain,
! [Vd594,Vd595,Vd596,Vd601,Vd602,Vd603,Vd604] :
( rinside(Vd596,Vd603)
| ! [Vd598] :
( ~ rpoint(Vd598)
| Vd594 != Vd598 )
| ! [Vd599] :
( ~ rpoint(Vd599)
| Vd595 != Vd599 )
| ! [Vd600] :
( ~ rpoint(Vd600)
| Vd596 != Vd600 )
| ~ rline(Vd602)
| Vd601 != Vd602
| ~ rcircle(Vd604)
| Vd603 != Vd604
| ( ~ rinside(Vd594,Vd603)
& ~ ron(Vd594,Vd603) )
| ( ~ rinside(Vd595,Vd603)
& ~ ron(Vd595,Vd603) )
| ~ rR(Vd596,Vd594,Vd595) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f370,definition,
! [Vd595,Vd603] :
( sP3_prd(Vd603,Vd595)
<=> ( ~ rinside(Vd595,Vd603)
& ~ ron(Vd595,Vd603) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f371,plain,
! [Vd594,Vd595,Vd596,Vd601,Vd602,Vd603,Vd604] :
( rinside(Vd596,Vd603)
| ! [Vd598] :
( ~ rpoint(Vd598)
| Vd594 != Vd598 )
| ! [Vd599] :
( ~ rpoint(Vd599)
| Vd595 != Vd599 )
| ! [Vd600] :
( ~ rpoint(Vd600)
| Vd596 != Vd600 )
| ~ rline(Vd602)
| Vd601 != Vd602
| ~ rcircle(Vd604)
| Vd603 != Vd604
| ( ~ rinside(Vd594,Vd603)
& ~ ron(Vd594,Vd603) )
| sP3_prd(Vd603,Vd595)
| ~ rR(Vd596,Vd594,Vd595) ),
inference(formula_renaming,[status(thm)],[f369,f370]) ).
fof(f372,plain,
! [Vd596,Vd603] :
( rinside(Vd596,Vd603)
| ! [Vd594] :
( ! [Vd598] :
( ~ rpoint(Vd598)
| Vd594 != Vd598 )
| ! [Vd595] :
( ! [Vd599] :
( ~ rpoint(Vd599)
| Vd595 != Vd599 )
| ! [Vd600] :
( ~ rpoint(Vd600)
| Vd596 != Vd600 )
| ! [Vd602] :
( ~ rline(Vd602)
| ! [Vd601] : Vd601 != Vd602
| ! [Vd604] :
( ~ rcircle(Vd604)
| Vd603 != Vd604
| ( ~ rinside(Vd594,Vd603)
& ~ ron(Vd594,Vd603) )
| sP3_prd(Vd603,Vd595)
| ~ rR(Vd596,Vd594,Vd595) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f371]) ).
fof(f373,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( rinside(X0,X3)
| ~ rpoint(X9)
| X1 != X9
| ~ rpoint(X8)
| X2 != X8
| ~ rpoint(X7)
| X0 != X7
| ~ rline(X6)
| X5 != X6
| ~ rcircle(X4)
| X3 != X4
| ~ ron(X1,X3)
| sP3_prd(X3,X2)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f374,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( rinside(X0,X3)
| ~ rpoint(X9)
| X1 != X9
| ~ rpoint(X8)
| X2 != X8
| ~ rpoint(X7)
| X0 != X7
| ~ rline(X6)
| X5 != X6
| ~ rcircle(X4)
| X3 != X4
| ~ rinside(X1,X3)
| sP3_prd(X3,X2)
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f414,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(pre_NNF_transformation,[status(thm)],[f90]) ).
fof(f415,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ rR(X1,X0,X2)
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f418,plain,
! [X0,X1,X2,X3,X4,X5] :
( rR(X0,X2,X1)
| ~ rpoint(X5)
| X1 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X2 != X3
| ~ rR(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f702,definition,
! [X0,X1,X2,X3,X4,X7,X8,X9] :
( sQ3_spl
<=> ( rinside(X0,X3)
| ~ rpoint(X9)
| X1 != X9
| ~ rpoint(X8)
| X2 != X8
| ~ rpoint(X7)
| X0 != X7
| ~ rcircle(X4)
| X3 != X4
| ~ ron(X1,X3)
| sP3_prd(X3,X2)
| ~ rR(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f705,definition,
! [X5,X6] :
( sQ4_spl
<=> ( ~ rline(X6)
| X5 != X6 ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f706,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ rline(X1)
| X0 != X1 ),
inference(component_clause,[status(thm)],[f705]) ).
fof(f708,plain,
( sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f373,f702,f705]) ).
fof(f709,definition,
! [X0,X1,X2,X3,X4,X7,X8,X9] :
( sQ5_spl
<=> ( rinside(X0,X3)
| ~ rpoint(X9)
| X1 != X9
| ~ rpoint(X8)
| X2 != X8
| ~ rpoint(X7)
| X0 != X7
| ~ rcircle(X4)
| X3 != X4
| ~ rinside(X1,X3)
| sP3_prd(X3,X2)
| ~ rR(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f374,f709,f705]) ).
fof(f720,plain,
! [X0,X1,X2,X3] :
( rR(X0,X3,X2)
| rR(X3,X2,X0)
| rR(X2,X3,X0)
| ~ rpoint(X3)
| ~ rpoint(X2)
| ~ rpoint(X0)
| X3 = X2
| X3 = X0
| X2 = X0
| ~ rline(X1)
| ~ ron(X3,X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f149]) ).
fof(f724,plain,
! [X0,X1] :
( X1 = X0
| vf(X1,X0) != v0
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f201]) ).
fof(f725,plain,
! [X1] :
( vf(X1,X1) = v0
| ~ rpoint(X1)
| ~ rpoint(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f202]) ).
fof(f726,plain,
! [X0] :
( vf(X0,X0) = v0
| ~ rpoint(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f725]) ).
fof(f779,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( vangle(X3,X0,X1) = vangle(X4,X0,X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rpoint(X1)
| ~ rpoint(X4)
| ~ rpoint(X2)
| ~ rline(X6)
| ~ rline(X5)
| ~ ron(X0,X6)
| ~ ron(X3,X6)
| ~ ron(X4,X6)
| ~ ron(X1,X5)
| ~ ron(X2,X5)
| X3 = X0
| X1 = X0
| X4 = X0
| X2 = X0
| rR(X0,X3,X4)
| rR(X0,X1,X2) ),
inference(destructive_equality_resolution,[status(thm)],[f315]) ).
fof(f806,plain,
! [X0,X1,X2] :
( ~ rR(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rR(X0,X1,X2) ),
inference(destructive_equality_resolution,[status(thm)],[f415]) ).
fof(f811,plain,
! [X0,X1,X2] :
( rR(X0,X2,X1)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rR(X0,X1,X2) ),
inference(destructive_equality_resolution,[status(thm)],[f418]) ).
fof(f938,plain,
! [X0] :
( ~ sQ4_spl
| ~ rline(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f706]) ).
fof(f944,definition,
! [X0] :
( sQ8_spl
<=> ( ~ rline(X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1199,X0)
| ~ ron(vd1185,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f945,plain,
! [X0] :
( ~ sQ8_spl
| ~ rline(X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1199,X0)
| ~ ron(vd1185,X0) ),
inference(component_clause,[status(thm)],[f944]) ).
fof(f947,definition,
( sQ9_spl
<=> vd1199 = vd1185 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f948,plain,
( ~ sQ9_spl
| vd1199 = vd1185 ),
inference(component_clause,[status(thm)],[f947]) ).
fof(f950,definition,
( sQ10_spl
<=> vd1186 = vd1185 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f951,plain,
( ~ sQ10_spl
| vd1186 = vd1185 ),
inference(component_clause,[status(thm)],[f950]) ).
fof(f959,definition,
( sQ13_spl
<=> rpoint(vd1199) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f961,plain,
( sQ13_spl
| ~ rpoint(vd1199) ),
inference(component_clause,[status(thm)],[f959]) ).
fof(f962,definition,
( sQ14_spl
<=> rpoint(vd1186) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f964,plain,
( sQ14_spl
| ~ rpoint(vd1186) ),
inference(component_clause,[status(thm)],[f962]) ).
fof(f1007,plain,
vf(vd1178,vd1179) = vf(vd1185,vd1200),
inference(backward_demodulation,[status(thm)],[f145,f177]) ).
fof(f1008,plain,
~ rR(vd1200,vd1199,vd1185),
inference(backward_demodulation,[status(thm)],[f145,f154]) ).
fof(f1010,plain,
~ rR(vd1185,vd1199,vd1200),
inference(backward_demodulation,[status(thm)],[f145,f139]) ).
fof(f1011,plain,
~ rR(vd1199,vd1185,vd1200),
inference(backward_demodulation,[status(thm)],[f145,f138]) ).
fof(f1012,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f152,f938]) ).
fof(f1013,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f1012]) ).
fof(f1016,plain,
sK1_skl = vd1186,
inference(backward_demodulation,[status(thm)],[f166,f145]) ).
fof(f1017,plain,
( sQ13_spl
| ~ rpoint(sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f169,f961]) ).
fof(f1018,plain,
sK2_skl != vd1185,
inference(backward_demodulation,[status(thm)],[f169,f140]) ).
fof(f1019,plain,
ron(sK5_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f182,f141]) ).
fof(f1020,plain,
ron(sK1_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f166,f142]) ).
fof(f1022,plain,
~ rR(sK5_skl,vd1199,vd1200),
inference(forward_demodulation,[status(thm)],[f182,f1010]) ).
fof(f1023,plain,
~ rR(sK5_skl,sK2_skl,vd1200),
inference(forward_demodulation,[status(thm)],[f169,f1022]) ).
fof(f1024,plain,
~ rR(sK5_skl,sK2_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f166,f1023]) ).
fof(f1025,plain,
~ rR(sK2_skl,vd1185,vd1200),
inference(forward_demodulation,[status(thm)],[f169,f1011]) ).
fof(f1026,plain,
~ rR(sK2_skl,sK5_skl,vd1200),
inference(forward_demodulation,[status(thm)],[f182,f1025]) ).
fof(f1027,plain,
~ rR(sK2_skl,sK5_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f166,f1026]) ).
fof(f1028,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1017,f170]) ).
fof(f1029,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f1028]) ).
fof(f1032,plain,
sK2_skl != sK5_skl,
inference(forward_demodulation,[status(thm)],[f182,f1018]) ).
fof(f1033,plain,
vf(vd1178,vd1179) = vf(sK5_skl,vd1200),
inference(forward_demodulation,[status(thm)],[f182,f1007]) ).
fof(f1034,plain,
vf(vd1178,vd1179) = vf(sK5_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f166,f1033]) ).
fof(f1036,plain,
~ rR(sK1_skl,vd1199,vd1185),
inference(forward_demodulation,[status(thm)],[f166,f1008]) ).
fof(f1037,plain,
~ rR(sK1_skl,sK2_skl,vd1185),
inference(forward_demodulation,[status(thm)],[f169,f1036]) ).
fof(f1038,plain,
~ rR(sK1_skl,sK2_skl,sK5_skl),
inference(forward_demodulation,[status(thm)],[f182,f1037]) ).
fof(f1057,definition,
( sQ22_spl
<=> sK2_skl = sK5_skl ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1058,plain,
( ~ sQ22_spl
| sK2_skl = sK5_skl ),
inference(component_clause,[status(thm)],[f1057]) ).
fof(f1066,definition,
( sQ25_spl
<=> rpoint(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1068,plain,
( sQ25_spl
| ~ rpoint(sK5_skl) ),
inference(component_clause,[status(thm)],[f1066]) ).
fof(f1069,definition,
( sQ26_spl
<=> rpoint(sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1071,plain,
( sQ26_spl
| ~ rpoint(sK2_skl) ),
inference(component_clause,[status(thm)],[f1069]) ).
fof(f1072,definition,
( sQ27_spl
<=> rpoint(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f1074,plain,
( sQ27_spl
| ~ rpoint(sK1_skl) ),
inference(component_clause,[status(thm)],[f1072]) ).
fof(f1104,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1071,f170]) ).
fof(f1105,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f1104]) ).
fof(f1106,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1074,f167]) ).
fof(f1107,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f1106]) ).
fof(f1108,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1058,f1032]) ).
fof(f1109,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f1108]) ).
fof(f1119,plain,
( sQ14_spl
| ~ rpoint(sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f180,f964]) ).
fof(f1120,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1119,f181]) ).
fof(f1121,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f1120]) ).
fof(f1123,plain,
( ~ sQ9_spl
| sK2_skl = vd1185 ),
inference(forward_demodulation,[status(thm)],[f169,f948]) ).
fof(f1124,plain,
( ~ sQ9_spl
| sK2_skl = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f182,f1123]) ).
fof(f1125,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1124,f1032]) ).
fof(f1126,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1125]) ).
fof(f1150,plain,
( ~ sQ10_spl
| sK4_skl = vd1185 ),
inference(forward_demodulation,[status(thm)],[f180,f951]) ).
fof(f1151,plain,
( ~ sQ10_spl
| sK4_skl = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f182,f1150]) ).
fof(f1152,plain,
! [X0] :
( ~ sQ8_spl
| ~ rline(X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1199,X0)
| ~ ron(sK5_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f182,f945]) ).
fof(f1153,plain,
! [X0] :
( ~ sQ8_spl
| ~ rline(X0)
| ~ ron(vd1186,X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f169,f1152]) ).
fof(f1154,plain,
! [X0] :
( ~ sQ8_spl
| ~ rline(X0)
| ~ ron(sK4_skl,X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0) ),
inference(forward_demodulation,[status(thm)],[f180,f1153]) ).
fof(f1156,plain,
vd1179 != sK6_skl,
inference(backward_demodulation,[status(thm)],[f187,f184]) ).
fof(f1157,plain,
vd1178 != sK7_skl,
inference(backward_demodulation,[status(thm)],[f189,f186]) ).
fof(f1158,plain,
sK1_skl = sK4_skl,
inference(forward_demodulation,[status(thm)],[f180,f1016]) ).
fof(f1159,plain,
ron(sK2_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f169,f144]) ).
fof(f1160,plain,
vf(sK2_skl,vd1200) = vf(vd1185,vd1186),
inference(forward_demodulation,[status(thm)],[f169,f150]) ).
fof(f1161,plain,
vf(sK2_skl,vd1200) = vf(sK5_skl,vd1186),
inference(forward_demodulation,[status(thm)],[f182,f1160]) ).
fof(f1162,plain,
vf(sK2_skl,vd1200) = vf(sK5_skl,sK4_skl),
inference(forward_demodulation,[status(thm)],[f180,f1161]) ).
fof(f1164,plain,
~ rR(sK2_skl,sK5_skl,sK4_skl),
inference(forward_demodulation,[status(thm)],[f1158,f1027]) ).
fof(f1165,plain,
! [X0] :
( rR(sK4_skl,sK2_skl,sK5_skl)
| rR(sK5_skl,sK2_skl,sK4_skl)
| ~ rpoint(sK2_skl)
| ~ rpoint(sK5_skl)
| ~ rpoint(sK4_skl)
| sK2_skl = sK5_skl
| sK2_skl = sK4_skl
| sK5_skl = sK4_skl
| ~ rline(X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1164,f720]) ).
fof(f1166,definition,
! [X0] :
( sQ38_spl
<=> ( ~ rline(X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK4_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1167,plain,
! [X0] :
( ~ sQ38_spl
| ~ rline(X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK4_skl,X0) ),
inference(component_clause,[status(thm)],[f1166]) ).
fof(f1169,definition,
( sQ39_spl
<=> sK5_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f1170,plain,
( ~ sQ39_spl
| sK5_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f1169]) ).
fof(f1171,plain,
( sQ39_spl
| sK5_skl != sK4_skl ),
inference(component_clause,[status(thm)],[f1169]) ).
fof(f1172,definition,
( sQ40_spl
<=> sK2_skl = sK4_skl ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f1173,plain,
( ~ sQ40_spl
| sK2_skl = sK4_skl ),
inference(component_clause,[status(thm)],[f1172]) ).
fof(f1175,definition,
( sQ41_spl
<=> rpoint(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1177,plain,
( sQ41_spl
| ~ rpoint(sK4_skl) ),
inference(component_clause,[status(thm)],[f1175]) ).
fof(f1178,definition,
( sQ42_spl
<=> rR(sK5_skl,sK2_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f1179,plain,
( ~ sQ42_spl
| rR(sK5_skl,sK2_skl,sK4_skl) ),
inference(component_clause,[status(thm)],[f1178]) ).
fof(f1181,definition,
( sQ43_spl
<=> rR(sK4_skl,sK2_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1182,plain,
( ~ sQ43_spl
| rR(sK4_skl,sK2_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f1181]) ).
fof(f1184,plain,
( sQ43_spl
| sQ42_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ41_spl
| sQ22_spl
| sQ40_spl
| sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1165,f1166,f1169,f1172,f1057,f1175,f1066,f1069,f1178,f1181]) ).
fof(f1185,plain,
( sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1177,f181]) ).
fof(f1186,plain,
sQ41_spl,
inference(contradiction_clause,[status(thm)],[f1185]) ).
fof(f1188,plain,
( ~ sQ40_spl
| vf(sK4_skl,vd1200) = vf(sK5_skl,sK4_skl) ),
inference(backward_demodulation,[status(thm)],[f1173,f1162]) ).
fof(f1204,plain,
( ~ sQ10_spl
| sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1151,f1171]) ).
fof(f1205,plain,
( ~ sQ10_spl
| sQ39_spl ),
inference(contradiction_clause,[status(thm)],[f1204]) ).
fof(f1267,plain,
( ~ sQ43_spl
| rR(sK4_skl,sK5_skl,sK2_skl)
| ~ rpoint(sK2_skl)
| ~ rpoint(sK4_skl)
| ~ rpoint(sK5_skl) ),
inference(resolution,[status(thm)],[f1182,f811]) ).
fof(f1268,plain,
( ~ sQ43_spl
| ~ rpoint(sK4_skl)
| ~ rpoint(sK2_skl)
| ~ rpoint(sK5_skl)
| ~ rR(sK2_skl,sK4_skl,sK5_skl) ),
inference(resolution,[status(thm)],[f1182,f806]) ).
fof(f1293,definition,
( sQ58_spl
<=> rR(sK4_skl,sK5_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f1294,plain,
( ~ sQ58_spl
| rR(sK4_skl,sK5_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f1293]) ).
fof(f1296,plain,
( ~ sQ43_spl
| sQ58_spl
| ~ sQ26_spl
| ~ sQ41_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1267,f1066,f1175,f1069,f1293,f1181]) ).
fof(f1297,definition,
( sQ59_spl
<=> rR(sK2_skl,sK4_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1300,plain,
( ~ sQ43_spl
| ~ sQ41_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f1268,f1297,f1066,f1069,f1175,f1181]) ).
fof(f1301,plain,
vf(sK8_skl,vd1179) = vf(sK5_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f191,f1034]) ).
fof(f1302,plain,
vf(sK8_skl,sK7_skl) = vf(sK5_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f189,f1301]) ).
fof(f1306,plain,
sK7_skl != sK6_skl,
inference(forward_demodulation,[status(thm)],[f189,f1156]) ).
fof(f1307,plain,
sK8_skl != sK7_skl,
inference(forward_demodulation,[status(thm)],[f191,f1157]) ).
fof(f1308,plain,
vd1200 = sK4_skl,
inference(backward_demodulation,[status(thm)],[f1158,f166]) ).
fof(f1310,plain,
vf(sK8_skl,sK7_skl) = vf(sK5_skl,sK4_skl),
inference(backward_demodulation,[status(thm)],[f1158,f1302]) ).
fof(f1311,plain,
~ rR(sK4_skl,sK2_skl,sK5_skl),
inference(backward_demodulation,[status(thm)],[f1158,f1038]) ).
fof(f1313,plain,
ron(sK2_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f169,f155]) ).
fof(f1314,plain,
~ ron(sK3_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f178,f171]) ).
fof(f1315,plain,
ron(sK4_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f1158,f1020]) ).
fof(f1332,plain,
( ~ sQ42_spl
| rR(sK5_skl,sK4_skl,sK2_skl)
| ~ rpoint(sK2_skl)
| ~ rpoint(sK5_skl)
| ~ rpoint(sK4_skl) ),
inference(resolution,[status(thm)],[f1179,f811]) ).
fof(f1333,plain,
( ~ sQ42_spl
| ~ rpoint(sK5_skl)
| ~ rpoint(sK2_skl)
| ~ rpoint(sK4_skl)
| ~ rR(sK2_skl,sK5_skl,sK4_skl) ),
inference(resolution,[status(thm)],[f1179,f806]) ).
fof(f1352,definition,
( sQ64_spl
<=> rR(sK5_skl,sK4_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1355,plain,
( ~ sQ42_spl
| sQ64_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f1332,f1175,f1066,f1069,f1352,f1178]) ).
fof(f1356,definition,
( sQ65_spl
<=> rR(sK2_skl,sK5_skl,sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1359,plain,
( ~ sQ42_spl
| ~ sQ25_spl
| ~ sQ26_spl
| ~ sQ41_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f1333,f1356,f1175,f1069,f1066,f1178]) ).
fof(f1360,plain,
~ rR(sK5_skl,sK2_skl,sK4_skl),
inference(forward_demodulation,[status(thm)],[f1158,f1024]) ).
fof(f1361,plain,
! [X0] :
( rR(sK4_skl,sK5_skl,sK2_skl)
| rR(sK2_skl,sK5_skl,sK4_skl)
| ~ rpoint(sK5_skl)
| ~ rpoint(sK2_skl)
| ~ rpoint(sK4_skl)
| sK5_skl = sK2_skl
| sK5_skl = sK4_skl
| sK2_skl = sK4_skl
| ~ rline(X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK4_skl,X0) ),
inference(resolution,[status(thm)],[f1360,f720]) ).
fof(f1362,plain,
( sQ58_spl
| sQ65_spl
| ~ sQ25_spl
| ~ sQ26_spl
| ~ sQ41_spl
| sQ22_spl
| sQ39_spl
| sQ40_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1361,f1166,f1172,f1169,f1057,f1175,f1069,f1066,f1356,f1293]) ).
fof(f1372,plain,
( ~ sQ58_spl
| ~ rpoint(sK4_skl)
| ~ rpoint(sK5_skl)
| ~ rpoint(sK2_skl)
| ~ rR(sK5_skl,sK4_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f1294,f806]) ).
fof(f1389,plain,
( ~ sQ58_spl
| ~ sQ41_spl
| ~ sQ25_spl
| ~ sQ26_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f1372,f1352,f1069,f1066,f1175,f1293]) ).
fof(f1392,plain,
( ~ sQ38_spl
| ~ rline(vd1197)
| ~ ron(sK5_skl,vd1197)
| ~ ron(sK4_skl,vd1197) ),
inference(resolution,[status(thm)],[f1167,f1313]) ).
fof(f1393,definition,
( sQ69_spl
<=> ron(sK4_skl,vd1197) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1395,plain,
( sQ69_spl
| ~ ron(sK4_skl,vd1197) ),
inference(component_clause,[status(thm)],[f1393]) ).
fof(f1396,definition,
( sQ70_spl
<=> ron(sK5_skl,vd1197) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1398,plain,
( sQ70_spl
| ~ ron(sK5_skl,vd1197) ),
inference(component_clause,[status(thm)],[f1396]) ).
fof(f1399,definition,
( sQ71_spl
<=> rline(vd1197) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1401,plain,
( sQ71_spl
| ~ rline(vd1197) ),
inference(component_clause,[status(thm)],[f1399]) ).
fof(f1402,plain,
( ~ sQ38_spl
| ~ sQ71_spl
| ~ sQ70_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f1392,f1393,f1396,f1399,f1166]) ).
fof(f1403,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1401,f152]) ).
fof(f1404,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f1403]) ).
fof(f1405,plain,
( sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1398,f1019]) ).
fof(f1406,plain,
sQ70_spl,
inference(contradiction_clause,[status(thm)],[f1405]) ).
fof(f1407,plain,
( sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1395,f1315]) ).
fof(f1408,plain,
sQ69_spl,
inference(contradiction_clause,[status(thm)],[f1407]) ).
fof(f1409,plain,
( ~ sQ40_spl
| vf(sK4_skl,sK4_skl) = vf(sK5_skl,sK4_skl) ),
inference(forward_demodulation,[status(thm)],[f1308,f1188]) ).
fof(f1472,plain,
( ~ sQ39_spl
| sK1_skl = sK5_skl ),
inference(backward_demodulation,[status(thm)],[f1170,f1158]) ).
fof(f1476,definition,
! [X0] :
( sQ79_spl
<=> ( ~ rline(X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1477,plain,
! [X0] :
( ~ sQ79_spl
| ~ rline(X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f1476]) ).
fof(f1485,definition,
( sQ82_spl
<=> rR(sK5_skl,sK5_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1486,plain,
( ~ sQ82_spl
| rR(sK5_skl,sK5_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f1485]) ).
fof(f1489,plain,
! [X0] :
( ~ sQ79_spl
| ~ rline(X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1477]) ).
fof(f1508,definition,
( sQ85_spl
<=> rpoint(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1510,plain,
( sQ85_spl
| ~ rpoint(sK0_skl) ),
inference(component_clause,[status(thm)],[f1508]) ).
fof(f1516,plain,
( sQ85_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1510,f164]) ).
fof(f1517,plain,
sQ85_spl,
inference(contradiction_clause,[status(thm)],[f1516]) ).
fof(f1568,plain,
( ~ sQ82_spl
| ~ rpoint(sK5_skl)
| ~ rpoint(sK5_skl)
| ~ rpoint(sK2_skl)
| ~ rR(sK5_skl,sK5_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f1486,f806]) ).
fof(f1598,plain,
( ~ sQ25_spl
| ~ sQ26_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f1568,f1485,f1069,f1066]) ).
fof(f1600,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1068,f183]) ).
fof(f1601,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f1600]) ).
fof(f1602,plain,
( ~ sQ8_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f1154,f1166,f944]) ).
fof(f1654,plain,
vangle(sK7_skl,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187),
inference(forward_demodulation,[status(thm)],[f189,f175]) ).
fof(f1655,plain,
vangle(sK7_skl,sK8_skl,vd1180) = vangle(vd1186,vd1185,vd1187),
inference(forward_demodulation,[status(thm)],[f191,f1654]) ).
fof(f1656,plain,
vangle(sK7_skl,sK8_skl,sK6_skl) = vangle(vd1186,vd1185,vd1187),
inference(forward_demodulation,[status(thm)],[f187,f1655]) ).
fof(f1657,plain,
vangle(sK7_skl,sK8_skl,sK6_skl) = vangle(sK4_skl,vd1185,vd1187),
inference(forward_demodulation,[status(thm)],[f180,f1656]) ).
fof(f1658,plain,
vangle(sK7_skl,sK8_skl,sK6_skl) = vangle(sK4_skl,sK5_skl,vd1187),
inference(forward_demodulation,[status(thm)],[f182,f1657]) ).
fof(f1659,plain,
vangle(sK7_skl,sK8_skl,sK6_skl) = vangle(sK4_skl,sK5_skl,sK3_skl),
inference(forward_demodulation,[status(thm)],[f178,f1658]) ).
fof(f1660,plain,
! [X0,X1,X2,X3] :
( vangle(X1,sK5_skl,X0) = vangle(sK7_skl,sK8_skl,sK6_skl)
| ~ rpoint(sK5_skl)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(sK4_skl)
| ~ rpoint(sK3_skl)
| ~ rline(X3)
| ~ rline(X2)
| ~ ron(sK5_skl,X3)
| ~ ron(X1,X3)
| ~ ron(sK4_skl,X3)
| ~ ron(X0,X2)
| ~ ron(sK3_skl,X2)
| X1 = sK5_skl
| X0 = sK5_skl
| sK4_skl = sK5_skl
| sK3_skl = sK5_skl
| rR(sK5_skl,X1,sK4_skl)
| rR(sK5_skl,X0,sK3_skl) ),
inference(paramodulation,[status(thm)],[f1659,f779]) ).
fof(f1661,plain,
! [X0,X1,X2,X3] :
( vangle(sK7_skl,sK8_skl,sK6_skl) = vangle(X1,sK5_skl,X0)
| ~ rpoint(sK5_skl)
| ~ rpoint(sK4_skl)
| ~ rpoint(sK3_skl)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rline(X3)
| ~ rline(X2)
| ~ ron(sK5_skl,X3)
| ~ ron(sK4_skl,X3)
| ~ ron(X1,X3)
| ~ ron(sK3_skl,X2)
| ~ ron(X0,X2)
| sK4_skl = sK5_skl
| sK3_skl = sK5_skl
| X1 = sK5_skl
| X0 = sK5_skl
| rR(sK5_skl,sK4_skl,X1)
| rR(sK5_skl,sK3_skl,X0) ),
inference(paramodulation,[status(thm)],[f1659,f779]) ).
fof(f1662,definition,
! [X0,X1,X2,X3] :
( sQ101_spl
<=> ( vangle(X1,sK5_skl,X0) = vangle(sK7_skl,sK8_skl,sK6_skl)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rline(X3)
| ~ rline(X2)
| ~ ron(sK5_skl,X3)
| ~ ron(X1,X3)
| ~ ron(sK4_skl,X3)
| ~ ron(X0,X2)
| ~ ron(sK3_skl,X2)
| X1 = sK5_skl
| X0 = sK5_skl
| rR(sK5_skl,X1,sK4_skl)
| rR(sK5_skl,X0,sK3_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1665,definition,
( sQ102_spl
<=> sK3_skl = sK5_skl ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1666,plain,
( ~ sQ102_spl
| sK3_skl = sK5_skl ),
inference(component_clause,[status(thm)],[f1665]) ).
fof(f1668,definition,
( sQ103_spl
<=> rpoint(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1670,plain,
( sQ103_spl
| ~ rpoint(sK3_skl) ),
inference(component_clause,[status(thm)],[f1668]) ).
fof(f1671,plain,
( ~ sQ25_spl
| ~ sQ41_spl
| ~ sQ103_spl
| sQ39_spl
| sQ102_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f1660,f1662,f1665,f1169,f1668,f1175,f1066]) ).
fof(f1672,definition,
! [X0,X1,X2,X3] :
( sQ104_spl
<=> ( vangle(sK7_skl,sK8_skl,sK6_skl) = vangle(X1,sK5_skl,X0)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rline(X3)
| ~ rline(X2)
| ~ ron(sK5_skl,X3)
| ~ ron(sK4_skl,X3)
| ~ ron(X1,X3)
| ~ ron(sK3_skl,X2)
| ~ ron(X0,X2)
| X1 = sK5_skl
| X0 = sK5_skl
| rR(sK5_skl,sK4_skl,X1)
| rR(sK5_skl,sK3_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1675,plain,
( ~ sQ25_spl
| ~ sQ41_spl
| ~ sQ103_spl
| sQ39_spl
| sQ102_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f1661,f1672,f1665,f1169,f1668,f1175,f1066]) ).
fof(f1676,plain,
( sQ103_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1670,f179]) ).
fof(f1677,plain,
sQ103_spl,
inference(contradiction_clause,[status(thm)],[f1676]) ).
fof(f1766,plain,
( ~ sQ40_spl
| vf(sK4_skl,sK4_skl) = vf(sK8_skl,sK7_skl) ),
inference(forward_demodulation,[status(thm)],[f1310,f1409]) ).
fof(f1769,plain,
( ~ sQ102_spl
| ~ ron(sK5_skl,vd1197) ),
inference(backward_demodulation,[status(thm)],[f1666,f1314]) ).
fof(f1773,plain,
( ~ sQ102_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f1769,f1396,f1665]) ).
fof(f1797,plain,
( ~ sQ39_spl
| sK4_skl = sK5_skl ),
inference(forward_demodulation,[status(thm)],[f1158,f1472]) ).
fof(f1817,definition,
( sQ119_spl
<=> sK5_skl = vd1199 ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f1818,plain,
( ~ sQ119_spl
| sK5_skl = vd1199 ),
inference(component_clause,[status(thm)],[f1817]) ).
fof(f1834,plain,
( ~ sQ119_spl
| sK5_skl = sK2_skl ),
inference(forward_demodulation,[status(thm)],[f169,f1818]) ).
fof(f1835,plain,
( ~ sQ119_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1834,f1032]) ).
fof(f1836,plain,
~ sQ119_spl,
inference(contradiction_clause,[status(thm)],[f1835]) ).
fof(f1850,plain,
vf(sK8_skl,vd1180) = vf(vd1185,vd1187),
inference(forward_demodulation,[status(thm)],[f191,f176]) ).
fof(f1851,plain,
vf(sK8_skl,sK6_skl) = vf(vd1185,vd1187),
inference(forward_demodulation,[status(thm)],[f187,f1850]) ).
fof(f1852,plain,
vf(sK8_skl,sK6_skl) = vf(sK5_skl,vd1187),
inference(forward_demodulation,[status(thm)],[f182,f1851]) ).
fof(f1853,plain,
vf(sK8_skl,sK6_skl) = vf(sK5_skl,sK3_skl),
inference(forward_demodulation,[status(thm)],[f178,f1852]) ).
fof(f1919,plain,
! [X0,X1] :
( X1 = X0
| vf(X1,X0) != vd684
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_demodulation,[status(thm)],[f345,f724]) ).
fof(f1920,plain,
( sK5_skl = sK3_skl
| vf(sK8_skl,sK6_skl) != vd684
| ~ rpoint(sK5_skl)
| ~ rpoint(sK3_skl) ),
inference(paramodulation,[status(thm)],[f1853,f1919]) ).
fof(f1921,definition,
( sQ123_spl
<=> vf(sK8_skl,sK6_skl) = vd684 ),
introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition]) ).
fof(f1924,plain,
( sQ102_spl
| ~ sQ123_spl
| ~ sQ25_spl
| ~ sQ103_spl ),
inference(split_clause,[status(thm)],[f1920,f1668,f1066,f1921,f1665]) ).
fof(f1925,plain,
! [X0] :
( vf(X0,X0) = vd684
| ~ rpoint(X0) ),
inference(forward_demodulation,[status(thm)],[f345,f726]) ).
fof(f1930,definition,
( sQ124_spl
<=> rpoint(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition]) ).
fof(f1932,plain,
( sQ124_spl
| ~ rpoint(sK6_skl) ),
inference(component_clause,[status(thm)],[f1930]) ).
fof(f1933,definition,
( sQ125_spl
<=> rpoint(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1935,plain,
( sQ125_spl
| ~ rpoint(sK7_skl) ),
inference(component_clause,[status(thm)],[f1933]) ).
fof(f1936,definition,
( sQ126_spl
<=> sK7_skl = sK6_skl ),
introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition]) ).
fof(f1937,plain,
( ~ sQ126_spl
| sK7_skl = sK6_skl ),
inference(component_clause,[status(thm)],[f1936]) ).
fof(f2028,definition,
! [X0] :
( sQ134_spl
<=> ( ~ rline(X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f2029,plain,
! [X0] :
( ~ sQ134_spl
| ~ rline(X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK5_skl,X0)
| ~ ron(sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f2028]) ).
fof(f2032,plain,
( ~ sQ39_spl
| vf(sK8_skl,sK7_skl) = vf(sK5_skl,sK5_skl) ),
inference(forward_demodulation,[status(thm)],[f1797,f1310]) ).
fof(f2033,plain,
( ~ sQ39_spl
| vf(sK8_skl,sK7_skl) = vd684
| ~ rpoint(sK5_skl) ),
inference(paramodulation,[status(thm)],[f2032,f1925]) ).
fof(f2035,definition,
( sQ135_spl
<=> vf(sK8_skl,sK7_skl) = vd684 ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f2036,plain,
( ~ sQ135_spl
| vf(sK8_skl,sK7_skl) = vd684 ),
inference(component_clause,[status(thm)],[f2035]) ).
fof(f2038,plain,
( ~ sQ39_spl
| sQ135_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f2033,f1066,f2035,f1169]) ).
fof(f2041,plain,
( ~ sQ135_spl
| sK8_skl = sK7_skl
| ~ rpoint(sK8_skl)
| ~ rpoint(sK7_skl) ),
inference(resolution,[status(thm)],[f2036,f1919]) ).
fof(f2043,definition,
( sQ136_spl
<=> rpoint(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f2045,plain,
( sQ136_spl
| ~ rpoint(sK8_skl) ),
inference(component_clause,[status(thm)],[f2043]) ).
fof(f2046,definition,
( sQ137_spl
<=> sK8_skl = sK7_skl ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f2047,plain,
( ~ sQ137_spl
| sK8_skl = sK7_skl ),
inference(component_clause,[status(thm)],[f2046]) ).
fof(f2049,plain,
( ~ sQ135_spl
| sQ137_spl
| ~ sQ136_spl
| ~ sQ125_spl ),
inference(split_clause,[status(thm)],[f2041,f1933,f2043,f2046,f2035]) ).
fof(f2054,plain,
( sQ125_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1935,f190]) ).
fof(f2055,plain,
sQ125_spl,
inference(contradiction_clause,[status(thm)],[f2054]) ).
fof(f2056,plain,
( sQ136_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2045,f192]) ).
fof(f2057,plain,
sQ136_spl,
inference(contradiction_clause,[status(thm)],[f2056]) ).
fof(f2058,plain,
( ~ sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2047,f1307]) ).
fof(f2059,plain,
~ sQ137_spl,
inference(contradiction_clause,[status(thm)],[f2058]) ).
fof(f2061,plain,
( ~ sQ40_spl
| vf(sK8_skl,sK7_skl) = vd684
| ~ rpoint(sK4_skl) ),
inference(paramodulation,[status(thm)],[f1766,f1925]) ).
fof(f2063,plain,
( ~ sQ40_spl
| sQ135_spl
| ~ sQ41_spl ),
inference(split_clause,[status(thm)],[f2061,f1175,f2035,f1172]) ).
fof(f2065,plain,
! [X0] :
( ~ sQ134_spl
| ~ rline(X0)
| ~ ron(sK5_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2029]) ).
fof(f2069,plain,
( ~ sQ126_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1937,f1306]) ).
fof(f2070,plain,
~ sQ126_spl,
inference(contradiction_clause,[status(thm)],[f2069]) ).
fof(f2071,plain,
( sQ124_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1932,f188]) ).
fof(f2072,plain,
sQ124_spl,
inference(contradiction_clause,[status(thm)],[f2071]) ).
fof(f2085,plain,
( ~ sQ134_spl
| ~ rline(vd1197) ),
inference(resolution,[status(thm)],[f2065,f1019]) ).
fof(f2088,plain,
( ~ sQ134_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f2085,f1399,f2028]) ).
fof(f2097,plain,
( ~ sQ79_spl
| ~ rline(vd1197)
| ~ ron(sK5_skl,vd1197) ),
inference(resolution,[status(thm)],[f1489,f1159]) ).
fof(f2100,plain,
( ~ sQ79_spl
| ~ sQ71_spl
| ~ sQ70_spl ),
inference(split_clause,[status(thm)],[f2097,f1396,f1399,f1476]) ).
fof(f2109,plain,
! [X0] :
( rR(sK5_skl,sK4_skl,sK2_skl)
| rR(sK2_skl,sK4_skl,sK5_skl)
| ~ rpoint(sK4_skl)
| ~ rpoint(sK2_skl)
| ~ rpoint(sK5_skl)
| sK4_skl = sK2_skl
| sK4_skl = sK5_skl
| sK2_skl = sK5_skl
| ~ rline(X0)
| ~ ron(sK4_skl,X0)
| ~ ron(sK2_skl,X0)
| ~ ron(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1311,f720]) ).
fof(f2110,plain,
( sQ64_spl
| sQ59_spl
| ~ sQ41_spl
| ~ sQ26_spl
| ~ sQ25_spl
| sQ40_spl
| sQ39_spl
| sQ22_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f2109,f1166,f1057,f1169,f1172,f1066,f1069,f1175,f1297,f1352]) ).
fof(f2111,plain,
$false,
inference(sat_refutation,[status(thm)],[f708,f712,f1013,f1029,f1105,f1107,f1109,f1121,f1126,f1184,f1186,f1205,f1296,f1300,f1355,f1359,f1362,f1389,f1402,f1404,f1406,f1408,f1517,f1598,f1601,f1602,f1671,f1675,f1677,f1773,f1836,f1924,f2038,f2049,f2055,f2057,f2059,f2063,f2070,f2072,f2088,f2100,f2110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO290+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n013.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sun Sep 20 15:09:12 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.13/5.40 % Drodi V4.1.1
% 0.13/5.55 % Refutation found
% 0.13/5.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/5.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/5.57 % Elapsed time: 0.179844 seconds
% 0.13/5.57 % CPU time: 1.117108 seconds
% 0.13/5.57 % Total memory used: 129.771 MB
% 0.13/5.57 % Net memory used: 128.206 MB
%------------------------------------------------------------------------------