%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO298+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 : n026.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:52 PM UTC 2026
% Result : Theorem 0.23s 5.83s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 83
% Syntax : Number of formulae : 337 ( 96 unt; 51 def)
% Number of atoms : 1407 ( 363 equ)
% Maximal formula atoms : 29 ( 4 avg)
% Number of connectives : 1857 ( 787 ~; 858 |; 146 &)
% ( 53 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 43 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 62 ( 60 usr; 51 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 24 con; 0-3 aty)
% Number of variables : 409 ( 371 !; 38 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( rR(vd1187,vd1185,vd1201)
| rR(vd1201,vd1185,vd1187) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ( rR(vd1187,vd1185,vd1201)
| rR(vd1201,vd1185,vd1187) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vd1201 != vd1187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
~ rR(vd1185,vd1201,vd1187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,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(f8,axiom,
ron(vd1187,vd1232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
? [Vd1205] :
( rpoint(Vd1205)
& vd1201 = Vd1205 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
rline(vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,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(f15,axiom,
ron(vd1187,vd1232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
ron(vd1199,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
vd1200 = vd1186,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
? [Vd1204] :
( rpoint(Vd1204)
& vd1200 = Vd1204 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
? [Vd1203] :
( rpoint(Vd1203)
& vd1199 = Vd1203 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
ron(vd1185,vd1232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
ron(vd1186,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
vf(vd1199,vd1201) = vf(vd1185,vd1187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
( ~ ron(vd1201,vd1232)
=> ( rS(vd1186,vd1201,vd1232)
| rS(vd1200,vd1187,vd1234) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
( ~ ron(vd1201,vd1232)
=> ~ rS(vd1200,vd1187,vd1234) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
( ~ ron(vd1201,vd1232)
=> ~ rS(vd1186,vd1201,vd1232) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
rline(vd1234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
rline(vd1232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
vd1199 = vd1185,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
( vd1199 != vd1185
=> ( rR(vd1199,vd1185,vd1186)
| rR(vd1185,vd1199,vd1186) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
( vd1199 != vd1185
=> ~ rR(vd1185,vd1199,vd1186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,axiom,
( vd1199 != vd1185
=> ~ rR(vd1199,vd1185,vd1186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,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(f57,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [Vd362,Vd363,Vd364,Vd369,Vd370] :
( ( ? [Vd366] :
( rpoint(Vd366)
& Vd362 = Vd366 )
& ? [Vd367] :
( rpoint(Vd367)
& Vd363 = Vd367 )
& ? [Vd368] :
( rpoint(Vd368)
& Vd364 = Vd368 )
& rline(Vd370)
& rR(Vd363,Vd362,Vd364)
& ron(Vd362,Vd369)
& ron(Vd364,Vd369)
& Vd369 = Vd370 )
=> ron(Vd363,Vd369) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [Vd352,Vd353,Vd354,Vd359,Vd360] :
( ( ? [Vd356] :
( rpoint(Vd356)
& Vd352 = Vd356 )
& ? [Vd357] :
( rpoint(Vd357)
& Vd353 = Vd357 )
& ? [Vd358] :
( rpoint(Vd358)
& Vd354 = Vd358 )
& rline(Vd360)
& rR(Vd353,Vd352,Vd354)
& ron(Vd352,Vd359)
& ron(Vd353,Vd359)
& Vd359 = Vd360 )
=> ron(Vd354,Vd359) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,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(f155,axiom,
! [Vd933,Vd934,Vd935,Vd936,Vd937,Vd944,Vd945,Vd946] :
( ( ? [Vd939] :
( rpoint(Vd939)
& Vd933 = Vd939 )
& ? [Vd940] :
( rpoint(Vd940)
& Vd934 = Vd940 )
& ? [Vd941] :
( rpoint(Vd941)
& Vd935 = Vd941 )
& ? [Vd942] :
( rpoint(Vd942)
& Vd936 = Vd942 )
& ? [Vd943] :
( rpoint(Vd943)
& Vd937 = Vd943 )
& ? [Vd948] :
( rline(Vd948)
& Vd944 = Vd948 )
& ? [Vd949] :
( rline(Vd949)
& Vd945 = Vd949 )
& ? [Vd950] :
( rline(Vd950)
& Vd946 = Vd950 )
& ron(Vd933,Vd944)
& ron(Vd934,Vd944)
& ron(Vd934,Vd945)
& ron(Vd935,Vd945)
& ron(Vd935,Vd946)
& ron(Vd936,Vd946)
& Vd934 != Vd935
& rS(Vd933,Vd936,Vd945)
& rless(vplus(vangle(Vd933,Vd934,Vd935),vangle(Vd934,Vd935,Vd936)),vplus(vperp,vperp)) )
=> ( rintersect(Vd944,Vd945)
& ( ( ron(Vd937,Vd944)
& ron(Vd937,Vd945) )
=> rS(Vd937,Vd933,Vd945) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f160,plain,
( ~ rR(vd1187,vd1185,vd1201)
& ~ rR(vd1201,vd1185,vd1187) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f161,plain,
~ rR(vd1201,vd1185,vd1187),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f162,plain,
~ rR(vd1187,vd1185,vd1201),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f163,plain,
vd1201 != vd1187,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f164,plain,
~ rR(vd1185,vd1201,vd1187),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f166,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)],[f6]) ).
fof(f167,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)],[f166]) ).
fof(f168,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)],[f167]) ).
fof(f170,plain,
ron(vd1187,vd1232),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f172,plain,
( rpoint(sK0_skl)
& vd1201 = sK0_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1205,sK0_skl)],[f10]) ).
fof(f173,plain,
vd1201 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f174,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f175,plain,
rline(vd1197),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f176,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)],[f12]) ).
fof(f177,plain,
( rpoint(sK6_skl)
& vd1178 = sK6_skl
& rpoint(sK5_skl)
& vd1179 = sK5_skl
& rpoint(sK4_skl)
& vd1180 = sK4_skl
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& rpoint(sK3_skl)
& vd1185 = sK3_skl
& rpoint(sK2_skl)
& vd1186 = sK2_skl
& rpoint(sK1_skl)
& vd1187 = sK1_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,[sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(Vd1191,sK1_skl),skolemize(Vd1190,sK2_skl),skolemize(Vd1189,sK3_skl),skolemize(Vd1184,sK4_skl),skolemize(Vd1183,sK5_skl),skolemize(Vd1182,sK6_skl)],[f176]) ).
fof(f182,plain,
vd1187 = sK1_skl,
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f183,plain,
rpoint(sK1_skl),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f184,plain,
vd1186 = sK2_skl,
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f185,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f186,plain,
vd1185 = sK3_skl,
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f187,plain,
rpoint(sK3_skl),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f201,plain,
ron(vd1187,vd1232),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f204,plain,
ron(vd1199,vd1197),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f205,plain,
vd1200 = vd1186,
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f212,plain,
( rpoint(sK7_skl)
& vd1200 = sK7_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Vd1204,sK7_skl)],[f26]) ).
fof(f213,plain,
vd1200 = sK7_skl,
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f215,plain,
( rpoint(sK8_skl)
& vd1199 = sK8_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Vd1203,sK8_skl)],[f27]) ).
fof(f216,plain,
vd1199 = sK8_skl,
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f217,plain,
rpoint(sK8_skl),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f219,plain,
ron(vd1185,vd1232),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f222,plain,
ron(vd1186,vd1197),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f226,plain,
vf(vd1199,vd1201) = vf(vd1185,vd1187),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f227,plain,
( rS(vd1186,vd1201,vd1232)
| rS(vd1200,vd1187,vd1234)
| ron(vd1201,vd1232) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f228,plain,
( rS(vd1186,vd1201,vd1232)
| rS(vd1200,vd1187,vd1234)
| ron(vd1201,vd1232) ),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f229,plain,
( ~ rS(vd1200,vd1187,vd1234)
| ron(vd1201,vd1232) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f230,plain,
( ~ rS(vd1200,vd1187,vd1234)
| ron(vd1201,vd1232) ),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f231,plain,
( ~ rS(vd1186,vd1201,vd1232)
| ron(vd1201,vd1232) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f232,plain,
( ~ rS(vd1186,vd1201,vd1232)
| ron(vd1201,vd1232) ),
inference(cnf_transformation,[status(thm)],[f231]) ).
fof(f236,plain,
rline(vd1234),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f238,plain,
rline(vd1232),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f240,plain,
vd1199 = vd1185,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f241,plain,
( rR(vd1199,vd1185,vd1186)
| rR(vd1185,vd1199,vd1186)
| vd1199 = vd1185 ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f242,plain,
( rR(vd1199,vd1185,vd1186)
| rR(vd1185,vd1199,vd1186)
| vd1199 = vd1185 ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f243,plain,
( ~ rR(vd1185,vd1199,vd1186)
| vd1199 = vd1185 ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f244,plain,
( ~ rR(vd1185,vd1199,vd1186)
| vd1199 = vd1185 ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f245,plain,
( ~ rR(vd1199,vd1185,vd1186)
| vd1199 = vd1185 ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f246,plain,
( ~ rR(vd1199,vd1185,vd1186)
| vd1199 = vd1185 ),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f257,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)],[f55]) ).
fof(f258,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)],[f257]) ).
fof(f259,plain,
! [X0,X1,X2,X3] :
( X2 = X0
| vf(X2,X0) != v0
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f260,plain,
! [X0,X1,X2,X3] :
( X2 != X0
| vf(X2,X0) = v0
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f266,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f320,plain,
! [Vd362,Vd363,Vd364,Vd369,Vd370] :
( ron(Vd363,Vd369)
| ! [Vd366] :
( ~ rpoint(Vd366)
| Vd362 != Vd366 )
| ! [Vd367] :
( ~ rpoint(Vd367)
| Vd363 != Vd367 )
| ! [Vd368] :
( ~ rpoint(Vd368)
| Vd364 != Vd368 )
| ~ rline(Vd370)
| ~ rR(Vd363,Vd362,Vd364)
| ~ ron(Vd362,Vd369)
| ~ ron(Vd364,Vd369)
| Vd369 != Vd370 ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f321,plain,
! [Vd363,Vd369] :
( ron(Vd363,Vd369)
| ! [Vd362] :
( ! [Vd366] :
( ~ rpoint(Vd366)
| Vd362 != Vd366 )
| ! [Vd367] :
( ~ rpoint(Vd367)
| Vd363 != Vd367 )
| ! [Vd364] :
( ! [Vd368] :
( ~ rpoint(Vd368)
| Vd364 != Vd368 )
| ! [Vd370] :
( ~ rline(Vd370)
| ~ rR(Vd363,Vd362,Vd364)
| ~ ron(Vd362,Vd369)
| ~ ron(Vd364,Vd369)
| Vd369 != Vd370 ) ) ) ),
inference(miniscoping,[status(thm)],[f320]) ).
fof(f322,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(X4,X0)
| ~ rpoint(X7)
| X3 != X7
| ~ rpoint(X6)
| X4 != X6
| ~ rpoint(X5)
| X2 != X5
| ~ rline(X1)
| ~ rR(X4,X3,X2)
| ~ ron(X3,X0)
| ~ ron(X2,X0)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f321]) ).
fof(f368,plain,
v0 = vd684,
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f385,plain,
! [Vd352,Vd353,Vd354,Vd359,Vd360] :
( ron(Vd354,Vd359)
| ! [Vd356] :
( ~ rpoint(Vd356)
| Vd352 != Vd356 )
| ! [Vd357] :
( ~ rpoint(Vd357)
| Vd353 != Vd357 )
| ! [Vd358] :
( ~ rpoint(Vd358)
| Vd354 != Vd358 )
| ~ rline(Vd360)
| ~ rR(Vd353,Vd352,Vd354)
| ~ ron(Vd352,Vd359)
| ~ ron(Vd353,Vd359)
| Vd359 != Vd360 ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f386,plain,
! [Vd354,Vd359] :
( ron(Vd354,Vd359)
| ! [Vd352] :
( ! [Vd356] :
( ~ rpoint(Vd356)
| Vd352 != Vd356 )
| ! [Vd353] :
( ! [Vd357] :
( ~ rpoint(Vd357)
| Vd353 != Vd357 )
| ! [Vd358] :
( ~ rpoint(Vd358)
| Vd354 != Vd358 )
| ! [Vd360] :
( ~ rline(Vd360)
| ~ rR(Vd353,Vd352,Vd354)
| ~ ron(Vd352,Vd359)
| ~ ron(Vd353,Vd359)
| Vd359 != Vd360 ) ) ) ),
inference(miniscoping,[status(thm)],[f385]) ).
fof(f387,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ron(X4,X0)
| ~ rpoint(X7)
| X3 != X7
| ~ rpoint(X6)
| X2 != X6
| ~ rpoint(X5)
| X4 != X5
| ~ rline(X1)
| ~ rR(X2,X3,X4)
| ~ ron(X3,X0)
| ~ ron(X2,X0)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f436,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)],[f104]) ).
fof(f437,definition,
! [Vd595,Vd603] :
( sP3_prd(Vd603,Vd595)
<=> ( ~ rinside(Vd595,Vd603)
& ~ ron(Vd595,Vd603) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f438,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)],[f436,f437]) ).
fof(f439,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)],[f438]) ).
fof(f440,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)],[f439]) ).
fof(f441,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)],[f439]) ).
fof(f697,plain,
! [Vd933,Vd934,Vd935,Vd936,Vd937,Vd944,Vd945,Vd946] :
( ( rintersect(Vd944,Vd945)
& ( rS(Vd937,Vd933,Vd945)
| ~ ron(Vd937,Vd944)
| ~ ron(Vd937,Vd945) ) )
| ! [Vd939] :
( ~ rpoint(Vd939)
| Vd933 != Vd939 )
| ! [Vd940] :
( ~ rpoint(Vd940)
| Vd934 != Vd940 )
| ! [Vd941] :
( ~ rpoint(Vd941)
| Vd935 != Vd941 )
| ! [Vd942] :
( ~ rpoint(Vd942)
| Vd936 != Vd942 )
| ! [Vd943] :
( ~ rpoint(Vd943)
| Vd937 != Vd943 )
| ! [Vd948] :
( ~ rline(Vd948)
| Vd944 != Vd948 )
| ! [Vd949] :
( ~ rline(Vd949)
| Vd945 != Vd949 )
| ! [Vd950] :
( ~ rline(Vd950)
| Vd946 != Vd950 )
| ~ ron(Vd933,Vd944)
| ~ ron(Vd934,Vd944)
| ~ ron(Vd934,Vd945)
| ~ ron(Vd935,Vd945)
| ~ ron(Vd935,Vd946)
| ~ ron(Vd936,Vd946)
| Vd934 = Vd935
| ~ rS(Vd933,Vd936,Vd945)
| ~ rless(vplus(vangle(Vd933,Vd934,Vd935),vangle(Vd934,Vd935,Vd936)),vplus(vperp,vperp)) ),
inference(pre_NNF_transformation,[status(thm)],[f155]) ).
fof(f698,plain,
! [Vd933,Vd937,Vd944,Vd945] :
( ( rintersect(Vd944,Vd945)
& ( rS(Vd937,Vd933,Vd945)
| ~ ron(Vd937,Vd944)
| ~ ron(Vd937,Vd945) ) )
| ! [Vd939] :
( ~ rpoint(Vd939)
| Vd933 != Vd939 )
| ! [Vd934] :
( ! [Vd940] :
( ~ rpoint(Vd940)
| Vd934 != Vd940 )
| ! [Vd935] :
( ! [Vd941] :
( ~ rpoint(Vd941)
| Vd935 != Vd941 )
| ! [Vd936] :
( ! [Vd942] :
( ~ rpoint(Vd942)
| Vd936 != Vd942 )
| ! [Vd943] :
( ~ rpoint(Vd943)
| Vd937 != Vd943 )
| ! [Vd948] :
( ~ rline(Vd948)
| Vd944 != Vd948 )
| ! [Vd949] :
( ~ rline(Vd949)
| Vd945 != Vd949 )
| ! [Vd946] :
( ! [Vd950] :
( ~ rline(Vd950)
| Vd946 != Vd950 )
| ~ ron(Vd933,Vd944)
| ~ ron(Vd934,Vd944)
| ~ ron(Vd934,Vd945)
| ~ ron(Vd935,Vd945)
| ~ ron(Vd935,Vd946)
| ~ ron(Vd936,Vd946)
| Vd934 = Vd935
| ~ rS(Vd933,Vd936,Vd945)
| ~ rless(vplus(vangle(Vd933,Vd934,Vd935),vangle(Vd934,Vd935,Vd936)),vplus(vperp,vperp)) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f697]) ).
fof(f700,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15] :
( rintersect(X6,X4)
| ~ rpoint(X15)
| X0 != X15
| ~ rpoint(X14)
| X1 != X14
| ~ rpoint(X13)
| X2 != X13
| ~ rpoint(X12)
| X3 != X12
| ~ rpoint(X11)
| X10 != X11
| ~ rline(X9)
| X6 != X9
| ~ rline(X8)
| X4 != X8
| ~ rline(X7)
| X5 != X7
| ~ ron(X0,X6)
| ~ ron(X1,X6)
| ~ ron(X1,X4)
| ~ ron(X2,X4)
| ~ ron(X2,X5)
| ~ ron(X3,X5)
| X1 = X2
| ~ rS(X0,X3,X4)
| ~ rless(vplus(vangle(X0,X1,X2),vangle(X1,X2,X3)),vplus(vperp,vperp)) ),
inference(cnf_transformation,[status(thm)],[f698]) ).
fof(f744,definition,
( sQ0_spl
<=> ron(vd1201,vd1232) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f745,plain,
( ~ sQ0_spl
| ron(vd1201,vd1232) ),
inference(component_clause,[status(thm)],[f744]) ).
fof(f747,definition,
( sQ1_spl
<=> rS(vd1200,vd1187,vd1234) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f750,definition,
( sQ2_spl
<=> rS(vd1186,vd1201,vd1232) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f753,plain,
( sQ2_spl
| sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f228,f744,f747,f750]) ).
fof(f754,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f230,f744,f747]) ).
fof(f755,plain,
( ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f232,f744,f750]) ).
fof(f756,definition,
( sQ3_spl
<=> vd1199 = vd1185 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f757,plain,
( ~ sQ3_spl
| vd1199 = vd1185 ),
inference(component_clause,[status(thm)],[f756]) ).
fof(f759,definition,
( sQ4_spl
<=> rR(vd1185,vd1199,vd1186) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f762,definition,
( sQ5_spl
<=> rR(vd1199,vd1185,vd1186) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f765,plain,
( sQ5_spl
| sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f242,f756,f759,f762]) ).
fof(f766,plain,
( ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f244,f756,f759]) ).
fof(f767,plain,
( ~ sQ5_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f246,f756,f762]) ).
fof(f780,definition,
! [X0,X1,X2,X3,X4,X7,X8,X9] :
( sQ9_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,[sQ9_spl])],[split_symbol_definition]) ).
fof(f783,definition,
! [X5,X6] :
( sQ10_spl
<=> ( ~ rline(X6)
| X5 != X6 ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f784,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ rline(X1)
| X0 != X1 ),
inference(component_clause,[status(thm)],[f783]) ).
fof(f786,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f440,f780,f783]) ).
fof(f787,definition,
! [X0,X1,X2,X3,X4,X7,X8,X9] :
( sQ11_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,[sQ11_spl])],[split_symbol_definition]) ).
fof(f790,plain,
( sQ10_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f441,f787,f783]) ).
fof(f791,definition,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X12,X13,X14,X15] :
( sQ12_spl
<=> ( rintersect(X6,X4)
| ~ rpoint(X15)
| X0 != X15
| ~ rpoint(X14)
| X1 != X14
| ~ rpoint(X13)
| X2 != X13
| ~ rpoint(X12)
| X3 != X12
| ~ rline(X9)
| X6 != X9
| ~ rline(X8)
| X4 != X8
| ~ rline(X7)
| X5 != X7
| ~ ron(X0,X6)
| ~ ron(X1,X6)
| ~ ron(X1,X4)
| ~ ron(X2,X4)
| ~ ron(X2,X5)
| ~ ron(X3,X5)
| X1 = X2
| ~ rS(X0,X3,X4)
| ~ rless(vplus(vangle(X0,X1,X2),vangle(X1,X2,X3)),vplus(vperp,vperp)) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f794,definition,
! [X10,X11] :
( sQ13_spl
<=> ( ~ rpoint(X11)
| X10 != X11 ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f795,plain,
! [X0,X1] :
( ~ sQ13_spl
| ~ rpoint(X1)
| X0 != X1 ),
inference(component_clause,[status(thm)],[f794]) ).
fof(f797,plain,
( sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f700,f791,f794]) ).
fof(f798,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)],[f168]) ).
fof(f804,plain,
! [X0,X1] :
( X1 = X0
| vf(X1,X0) != v0
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f259]) ).
fof(f805,plain,
! [X1] :
( vf(X1,X1) = v0
| ~ rpoint(X1)
| ~ rpoint(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f260]) ).
fof(f806,plain,
! [X0] :
( vf(X0,X0) = v0
| ~ rpoint(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f805]) ).
fof(f833,plain,
! [X0,X1,X2,X3] :
( ron(X3,X1)
| ~ rpoint(X2)
| ~ rpoint(X3)
| ~ rpoint(X0)
| ~ rline(X1)
| ~ rR(X3,X2,X0)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f322]) ).
fof(f862,plain,
! [X0,X1,X2,X3] :
( ron(X3,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rline(X1)
| ~ rR(X0,X2,X3)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f387]) ).
fof(f1016,plain,
! [X0] :
( ~ sQ10_spl
| ~ rline(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f784]) ).
fof(f1025,definition,
( sQ15_spl
<=> vd1201 = vd1187 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1026,plain,
( ~ sQ15_spl
| vd1201 = vd1187 ),
inference(component_clause,[status(thm)],[f1025]) ).
fof(f1028,definition,
( sQ16_spl
<=> vd1185 = vd1187 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1029,plain,
( ~ sQ16_spl
| vd1185 = vd1187 ),
inference(component_clause,[status(thm)],[f1028]) ).
fof(f1034,definition,
( sQ18_spl
<=> rpoint(vd1187) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1036,plain,
( sQ18_spl
| ~ rpoint(vd1187) ),
inference(component_clause,[status(thm)],[f1034]) ).
fof(f1037,definition,
( sQ19_spl
<=> rpoint(vd1201) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f1039,plain,
( sQ19_spl
| ~ rpoint(vd1201) ),
inference(component_clause,[status(thm)],[f1037]) ).
fof(f1040,definition,
( sQ20_spl
<=> rpoint(vd1185) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1042,plain,
( sQ20_spl
| ~ rpoint(vd1185) ),
inference(component_clause,[status(thm)],[f1040]) ).
fof(f1082,plain,
! [X0,X1,X2,X3,X4] :
( rR(X3,X0,X2)
| rR(X2,X0,X3)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X3)
| X0 = X2
| X0 = X3
| X2 = X3
| ~ rline(X4)
| ~ ron(X0,X4)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ron(X3,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(resolution,[status(thm)],[f862,f798]) ).
fof(f1083,plain,
! [X0,X1,X2,X3,X4] :
( rR(X3,X0,X2)
| rR(X2,X0,X3)
| X0 = X2
| X0 = X3
| X2 = X3
| ~ rline(X4)
| ~ ron(X0,X4)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ron(X3,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f1082]) ).
fof(f1084,plain,
! [X0,X1,X2,X3,X4] :
( rR(X3,X0,X2)
| X0 = X2
| X0 = X3
| X2 = X3
| ~ rline(X4)
| ~ ron(X0,X4)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ron(X3,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1083,f862]) ).
fof(f1087,plain,
vf(vd1199,sK0_skl) = vf(vd1185,vd1187),
inference(backward_demodulation,[status(thm)],[f173,f226]) ).
fof(f1088,plain,
( sQ19_spl
| ~ rpoint(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f173,f1039]) ).
fof(f1089,plain,
~ rR(vd1185,sK0_skl,vd1187),
inference(backward_demodulation,[status(thm)],[f173,f164]) ).
fof(f1090,plain,
sK0_skl != vd1187,
inference(backward_demodulation,[status(thm)],[f173,f163]) ).
fof(f1091,plain,
~ rR(vd1187,vd1185,sK0_skl),
inference(backward_demodulation,[status(thm)],[f173,f162]) ).
fof(f1092,plain,
~ rR(sK0_skl,vd1185,vd1187),
inference(backward_demodulation,[status(thm)],[f173,f161]) ).
fof(f1093,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f175,f1016]) ).
fof(f1094,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f1093]) ).
fof(f1101,plain,
ron(sK1_skl,vd1232),
inference(forward_demodulation,[status(thm)],[f182,f170]) ).
fof(f1103,plain,
~ rR(sK1_skl,vd1185,sK0_skl),
inference(forward_demodulation,[status(thm)],[f182,f1091]) ).
fof(f1104,plain,
~ rR(sK1_skl,sK3_skl,sK0_skl),
inference(forward_demodulation,[status(thm)],[f186,f1103]) ).
fof(f1105,plain,
~ rR(sK0_skl,sK3_skl,vd1187),
inference(forward_demodulation,[status(thm)],[f186,f1092]) ).
fof(f1106,plain,
~ rR(sK0_skl,sK3_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f182,f1105]) ).
fof(f1107,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1088,f174]) ).
fof(f1108,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f1107]) ).
fof(f1109,plain,
( sQ20_spl
| ~ rpoint(sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f186,f1042]) ).
fof(f1110,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1109,f187]) ).
fof(f1111,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f1110]) ).
fof(f1113,plain,
( sQ18_spl
| ~ rpoint(sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f182,f1036]) ).
fof(f1114,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1113,f183]) ).
fof(f1115,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1114]) ).
fof(f1120,plain,
sK0_skl != sK1_skl,
inference(forward_demodulation,[status(thm)],[f182,f1090]) ).
fof(f1127,plain,
~ rR(sK3_skl,sK0_skl,vd1187),
inference(forward_demodulation,[status(thm)],[f186,f1089]) ).
fof(f1156,definition,
( sQ30_spl
<=> rpoint(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1158,plain,
( sQ30_spl
| ~ rpoint(sK3_skl) ),
inference(component_clause,[status(thm)],[f1156]) ).
fof(f1159,definition,
( sQ31_spl
<=> rpoint(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1161,plain,
( sQ31_spl
| ~ rpoint(sK1_skl) ),
inference(component_clause,[status(thm)],[f1159]) ).
fof(f1181,plain,
( ~ sQ15_spl
| vd1201 = sK1_skl ),
inference(forward_demodulation,[status(thm)],[f182,f1026]) ).
fof(f1182,plain,
( ~ sQ16_spl
| sK3_skl = vd1187 ),
inference(forward_demodulation,[status(thm)],[f186,f1029]) ).
fof(f1183,plain,
( ~ sQ16_spl
| sK3_skl = sK1_skl ),
inference(forward_demodulation,[status(thm)],[f182,f1182]) ).
fof(f1186,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1158,f187]) ).
fof(f1187,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1186]) ).
fof(f1188,plain,
vf(vd1199,sK0_skl) = vf(sK3_skl,vd1187),
inference(forward_demodulation,[status(thm)],[f186,f1087]) ).
fof(f1189,plain,
vf(vd1199,sK0_skl) = vf(sK3_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f182,f1188]) ).
fof(f1190,plain,
~ rR(sK3_skl,sK0_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f182,f1127]) ).
fof(f1191,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1161,f183]) ).
fof(f1192,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f1191]) ).
fof(f1197,definition,
( sQ36_spl
<=> sK0_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f1198,plain,
( ~ sQ36_spl
| sK0_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f1197]) ).
fof(f1200,definition,
( sQ37_spl
<=> sK3_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f1201,plain,
( ~ sQ37_spl
| sK3_skl = sK0_skl ),
inference(component_clause,[status(thm)],[f1200]) ).
fof(f1203,definition,
( sQ38_spl
<=> rpoint(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f1205,plain,
( sQ38_spl
| ~ rpoint(sK0_skl) ),
inference(component_clause,[status(thm)],[f1203]) ).
fof(f1214,plain,
vd1200 = sK2_skl,
inference(forward_demodulation,[status(thm)],[f184,f205]) ).
fof(f1216,plain,
rpoint(sK7_skl),
inference(backward_demodulation,[status(thm)],[f1218,f185]) ).
fof(f1217,plain,
vd1186 = sK7_skl,
inference(backward_demodulation,[status(thm)],[f1218,f184]) ).
fof(f1218,plain,
sK2_skl = sK7_skl,
inference(forward_demodulation,[status(thm)],[f1214,f213]) ).
fof(f1219,plain,
vf(sK8_skl,sK0_skl) = vf(sK3_skl,sK1_skl),
inference(backward_demodulation,[status(thm)],[f216,f1189]) ).
fof(f1220,plain,
sK8_skl = vd1185,
inference(forward_demodulation,[status(thm)],[f216,f240]) ).
fof(f1221,plain,
~ rR(sK8_skl,sK0_skl,sK1_skl),
inference(backward_demodulation,[status(thm)],[f1225,f1190]) ).
fof(f1225,plain,
sK8_skl = sK3_skl,
inference(forward_demodulation,[status(thm)],[f186,f1220]) ).
fof(f1242,plain,
~ rR(sK0_skl,sK8_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f1225,f1106]) ).
fof(f1251,definition,
( sQ43_spl
<=> sK0_skl = sK8_skl ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f1252,plain,
( ~ sQ43_spl
| sK0_skl = sK8_skl ),
inference(component_clause,[status(thm)],[f1251]) ).
fof(f1254,definition,
( sQ44_spl
<=> rpoint(sK8_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1256,plain,
( sQ44_spl
| ~ rpoint(sK8_skl) ),
inference(component_clause,[status(thm)],[f1254]) ).
fof(f1261,plain,
( ~ sQ16_spl
| sK8_skl = sK1_skl ),
inference(forward_demodulation,[status(thm)],[f1225,f1183]) ).
fof(f1263,plain,
~ rR(sK1_skl,sK8_skl,sK0_skl),
inference(forward_demodulation,[status(thm)],[f1225,f1104]) ).
fof(f1265,definition,
! [X0] :
( sQ46_spl
<=> ( ~ rline(X0)
| ~ ron(sK1_skl,X0)
| ~ ron(sK8_skl,X0)
| ~ ron(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f1266,plain,
! [X0] :
( ~ sQ46_spl
| ~ rline(X0)
| ~ ron(sK1_skl,X0)
| ~ ron(sK8_skl,X0)
| ~ ron(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f1265]) ).
fof(f1268,definition,
( sQ47_spl
<=> sK1_skl = sK8_skl ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f1269,plain,
( ~ sQ47_spl
| sK1_skl = sK8_skl ),
inference(component_clause,[status(thm)],[f1268]) ).
fof(f1278,plain,
( sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1256,f217]) ).
fof(f1279,plain,
sQ44_spl,
inference(contradiction_clause,[status(thm)],[f1278]) ).
fof(f1292,plain,
( ~ sQ37_spl
| sK8_skl = sK0_skl ),
inference(forward_demodulation,[status(thm)],[f1225,f1201]) ).
fof(f1300,plain,
! [X0] :
( ~ sQ13_spl
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f795]) ).
fof(f1306,plain,
( ~ sQ37_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f1292,f1251,f1200]) ).
fof(f1309,plain,
vf(sK8_skl,sK0_skl) = vf(sK8_skl,sK1_skl),
inference(forward_demodulation,[status(thm)],[f1225,f1219]) ).
fof(f1321,plain,
( ~ sQ13_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f217,f1300]) ).
fof(f1326,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f1321]) ).
fof(f1327,plain,
( ~ sQ3_spl
| sK8_skl = vd1185 ),
inference(forward_demodulation,[status(thm)],[f216,f757]) ).
fof(f1380,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f174,f1205]) ).
fof(f1381,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f1380]) ).
fof(f1388,plain,
( ~ sQ43_spl
| vf(sK8_skl,sK8_skl) = vf(sK8_skl,sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f1252,f1309]) ).
fof(f1390,plain,
ron(sK1_skl,vd1232),
inference(forward_demodulation,[status(thm)],[f182,f201]) ).
fof(f1406,plain,
! [X0] :
( rR(sK1_skl,sK8_skl,sK0_skl)
| rR(sK0_skl,sK8_skl,sK1_skl)
| ~ rpoint(sK8_skl)
| ~ rpoint(sK0_skl)
| ~ rpoint(sK1_skl)
| sK8_skl = sK0_skl
| sK8_skl = sK1_skl
| sK0_skl = sK1_skl
| ~ rline(X0)
| ~ ron(sK8_skl,X0)
| ~ ron(sK0_skl,X0)
| ~ ron(sK1_skl,X0) ),
inference(resolution,[status(thm)],[f798,f1221]) ).
fof(f1413,definition,
( sQ55_spl
<=> rR(sK0_skl,sK8_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f1414,plain,
( ~ sQ55_spl
| rR(sK0_skl,sK8_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f1413]) ).
fof(f1416,definition,
( sQ56_spl
<=> rR(sK1_skl,sK8_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f1417,plain,
( ~ sQ56_spl
| rR(sK1_skl,sK8_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f1416]) ).
fof(f1419,plain,
( sQ56_spl
| sQ55_spl
| ~ sQ44_spl
| ~ sQ38_spl
| ~ sQ31_spl
| sQ43_spl
| sQ47_spl
| sQ36_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f1406,f1265,f1197,f1268,f1251,f1159,f1203,f1254,f1413,f1416]) ).
fof(f1421,definition,
( sQ57_spl
<=> rR(sK8_skl,sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
( ~ sQ57_spl
| rR(sK8_skl,sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f1421]) ).
fof(f1428,definition,
! [X0] :
( sQ59_spl
<=> ( ~ rline(X0)
| ~ ron(sK7_skl,X0)
| ~ ron(sK8_skl,X0)
| ~ ron(sK8_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1429,plain,
! [X0] :
( ~ sQ59_spl
| ~ rline(X0)
| ~ ron(sK7_skl,X0)
| ~ ron(sK8_skl,X0)
| ~ ron(sK8_skl,X0) ),
inference(component_clause,[status(thm)],[f1428]) ).
fof(f1434,definition,
( sQ61_spl
<=> rpoint(sK7_skl) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f1436,plain,
( sQ61_spl
| ~ rpoint(sK7_skl) ),
inference(component_clause,[status(thm)],[f1434]) ).
fof(f1442,plain,
( sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1436,f1216]) ).
fof(f1443,plain,
sQ61_spl,
inference(contradiction_clause,[status(thm)],[f1442]) ).
fof(f1444,plain,
! [X0] :
( ~ sQ59_spl
| ~ rline(X0)
| ~ ron(sK7_skl,X0)
| ~ ron(sK8_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1429]) ).
fof(f1445,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1422,f1221]) ).
fof(f1446,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f1445]) ).
fof(f1447,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1417,f1263]) ).
fof(f1448,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f1447]) ).
fof(f1449,plain,
( ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1414,f1242]) ).
fof(f1450,plain,
~ sQ55_spl,
inference(contradiction_clause,[status(thm)],[f1449]) ).
fof(f1468,plain,
ron(sK8_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f216,f204]) ).
fof(f1470,plain,
( ~ sQ3_spl
| ron(sK8_skl,vd1232) ),
inference(forward_demodulation,[status(thm)],[f1327,f219]) ).
fof(f1488,definition,
! [X0] :
( sQ63_spl
<=> ( ron(sK1_skl,X0)
| ~ rline(X0)
| ~ ron(sK8_skl,X0)
| ~ ron(sK8_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1489,plain,
! [X0] :
( ~ sQ63_spl
| ron(sK1_skl,X0)
| ~ rline(X0)
| ~ ron(sK8_skl,X0)
| ~ ron(sK8_skl,X0) ),
inference(component_clause,[status(thm)],[f1488]) ).
fof(f1497,plain,
! [X0] :
( ~ sQ63_spl
| ron(sK1_skl,X0)
| ~ rline(X0)
| ~ ron(sK8_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1489]) ).
fof(f1503,definition,
( sQ65_spl
<=> ron(sK8_skl,vd1232) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f1505,plain,
( sQ65_spl
| ~ ron(sK8_skl,vd1232) ),
inference(component_clause,[status(thm)],[f1503]) ).
fof(f1506,definition,
( sQ66_spl
<=> rline(vd1232) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f1508,plain,
( sQ66_spl
| ~ rline(vd1232) ),
inference(component_clause,[status(thm)],[f1506]) ).
fof(f1510,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1508,f238]) ).
fof(f1511,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f1510]) ).
fof(f1512,plain,
( sQ65_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1505,f1470]) ).
fof(f1513,plain,
( sQ65_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f1512]) ).
fof(f1529,plain,
( ~ sQ63_spl
| ron(sK1_skl,vd1197)
| ~ rline(vd1197) ),
inference(resolution,[status(thm)],[f1497,f1468]) ).
fof(f1530,definition,
( sQ68_spl
<=> ron(sK1_skl,vd1232) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f1532,plain,
( sQ68_spl
| ~ ron(sK1_skl,vd1232) ),
inference(component_clause,[status(thm)],[f1530]) ).
fof(f1534,definition,
( sQ69_spl
<=> rline(vd1197) ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f1536,plain,
( sQ69_spl
| ~ rline(vd1197) ),
inference(component_clause,[status(thm)],[f1534]) ).
fof(f1537,definition,
( sQ70_spl
<=> ron(sK1_skl,vd1197) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1538,plain,
( ~ sQ70_spl
| ron(sK1_skl,vd1197) ),
inference(component_clause,[status(thm)],[f1537]) ).
fof(f1540,plain,
( ~ sQ63_spl
| sQ70_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f1529,f1534,f1537,f1488]) ).
fof(f1541,plain,
( sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1536,f175]) ).
fof(f1542,plain,
sQ69_spl,
inference(contradiction_clause,[status(thm)],[f1541]) ).
fof(f1554,plain,
ron(sK7_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f1217,f222]) ).
fof(f1555,plain,
( ~ sQ59_spl
| ~ rline(vd1197)
| ~ ron(sK8_skl,vd1197) ),
inference(resolution,[status(thm)],[f1554,f1444]) ).
fof(f1556,definition,
( sQ71_spl
<=> ron(sK8_skl,vd1197) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1558,plain,
( sQ71_spl
| ~ ron(sK8_skl,vd1197) ),
inference(component_clause,[status(thm)],[f1556]) ).
fof(f1559,plain,
( ~ sQ59_spl
| ~ sQ69_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f1555,f1556,f1534,f1428]) ).
fof(f1560,plain,
( sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1558,f1468]) ).
fof(f1561,plain,
sQ71_spl,
inference(contradiction_clause,[status(thm)],[f1560]) ).
fof(f1567,definition,
( sQ73_spl
<=> rline(vd1234) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1569,plain,
( sQ73_spl
| ~ rline(vd1234) ),
inference(component_clause,[status(thm)],[f1567]) ).
fof(f1571,plain,
( sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1569,f236]) ).
fof(f1572,plain,
sQ73_spl,
inference(contradiction_clause,[status(thm)],[f1571]) ).
fof(f1576,plain,
~ ron(sK1_skl,vd1197),
inference(forward_demodulation,[status(thm)],[f182,f266]) ).
fof(f1577,plain,
( ~ sQ0_spl
| ron(sK0_skl,vd1232) ),
inference(forward_demodulation,[status(thm)],[f173,f745]) ).
fof(f1596,plain,
( ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1538,f1576]) ).
fof(f1597,plain,
~ sQ70_spl,
inference(contradiction_clause,[status(thm)],[f1596]) ).
fof(f1600,plain,
( ~ sQ0_spl
| ~ sQ46_spl
| ~ rline(vd1232)
| ~ ron(sK1_skl,vd1232)
| ~ ron(sK8_skl,vd1232) ),
inference(resolution,[status(thm)],[f1266,f1577]) ).
fof(f1602,plain,
( ~ sQ0_spl
| ~ sQ46_spl
| ~ sQ66_spl
| ~ sQ68_spl
| ~ sQ65_spl ),
inference(split_clause,[status(thm)],[f1600,f1503,f1530,f1506,f1265,f744]) ).
fof(f1607,plain,
( ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1198,f1120]) ).
fof(f1608,plain,
~ sQ36_spl,
inference(contradiction_clause,[status(thm)],[f1607]) ).
fof(f1623,plain,
( ~ sQ15_spl
| sK0_skl = sK1_skl ),
inference(forward_demodulation,[status(thm)],[f173,f1181]) ).
fof(f1624,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1623,f1120]) ).
fof(f1625,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1624]) ).
fof(f1634,plain,
( sQ68_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1532,f1390]) ).
fof(f1635,plain,
sQ68_spl,
inference(contradiction_clause,[status(thm)],[f1634]) ).
fof(f1647,plain,
( ~ sQ47_spl
| ~ ron(sK8_skl,vd1197) ),
inference(backward_demodulation,[status(thm)],[f1269,f1576]) ).
fof(f1656,plain,
( ~ sQ47_spl
| ~ sQ71_spl ),
inference(split_clause,[status(thm)],[f1647,f1556,f1268]) ).
fof(f1745,plain,
! [X0,X1] :
( X1 = X0
| vf(X1,X0) != vd684
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(forward_demodulation,[status(thm)],[f368,f804]) ).
fof(f1747,plain,
( ~ sQ43_spl
| sK8_skl = sK1_skl
| vf(sK8_skl,sK8_skl) != vd684
| ~ rpoint(sK8_skl)
| ~ rpoint(sK1_skl) ),
inference(paramodulation,[status(thm)],[f1388,f1745]) ).
fof(f1754,definition,
( sQ81_spl
<=> vf(sK8_skl,sK8_skl) = vd684 ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1756,plain,
( sQ81_spl
| vf(sK8_skl,sK8_skl) != vd684 ),
inference(component_clause,[status(thm)],[f1754]) ).
fof(f1761,plain,
( ~ sQ43_spl
| sQ47_spl
| ~ sQ81_spl
| ~ sQ44_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f1747,f1159,f1254,f1754,f1268,f1251]) ).
fof(f1777,plain,
( ~ sQ16_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f1261,f1268,f1028]) ).
fof(f1790,plain,
! [X0,X1,X2,X3,X4] :
( X0 = X2
| X0 = X3
| X2 = X3
| ~ rline(X4)
| ~ ron(X0,X4)
| ~ ron(X2,X4)
| ~ ron(X3,X4)
| ron(X3,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1084,f833]) ).
fof(f1792,plain,
! [X0,X1,X2] :
( X0 = sK1_skl
| X0 = X1
| sK1_skl = X1
| ~ rline(X2)
| ~ ron(X0,X2)
| ~ ron(sK1_skl,X2)
| ~ ron(X1,X2)
| ron(X1,vd1232)
| ~ rpoint(sK1_skl)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(vd1232)
| ~ ron(X0,vd1232) ),
inference(resolution,[status(thm)],[f1790,f1101]) ).
fof(f1794,plain,
! [X0,X1,X2] :
( X0 = sK7_skl
| X0 = X1
| sK7_skl = X1
| ~ rline(X2)
| ~ ron(X0,X2)
| ~ ron(sK7_skl,X2)
| ~ ron(X1,X2)
| ron(X1,vd1197)
| ~ rpoint(sK7_skl)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(vd1197)
| ~ ron(X0,vd1197) ),
inference(resolution,[status(thm)],[f1790,f1554]) ).
fof(f1800,plain,
! [X0,X1,X2] :
( X0 = sK8_skl
| X0 = X1
| sK8_skl = X1
| ~ rline(X2)
| ~ ron(X0,X2)
| ~ ron(sK8_skl,X2)
| ~ ron(X1,X2)
| ron(X1,vd1197)
| ~ rpoint(sK8_skl)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(vd1197)
| ~ ron(X0,vd1197) ),
inference(resolution,[status(thm)],[f1790,f1468]) ).
fof(f1802,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = sK1_skl
| X2 = sK1_skl
| ~ rline(vd1232)
| ~ ron(X0,vd1232)
| ~ ron(X2,vd1232)
| ron(sK1_skl,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(sK1_skl)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(resolution,[status(thm)],[f1790,f1101]) ).
fof(f1804,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = sK7_skl
| X2 = sK7_skl
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X2,vd1197)
| ron(sK7_skl,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(sK7_skl)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(resolution,[status(thm)],[f1790,f1554]) ).
fof(f1810,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = sK8_skl
| X2 = sK8_skl
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X2,vd1197)
| ron(sK8_skl,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(sK8_skl)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(resolution,[status(thm)],[f1790,f1468]) ).
fof(f1812,plain,
! [X0,X1,X2] :
( X0 = sK1_skl
| X0 = X2
| sK1_skl = X2
| ~ rline(vd1232)
| ~ ron(X0,vd1232)
| ~ ron(X2,vd1232)
| ron(X2,X1)
| ~ rpoint(sK1_skl)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rline(X1)
| ~ ron(sK1_skl,X1)
| ~ ron(X0,X1) ),
inference(resolution,[status(thm)],[f1790,f1101]) ).
fof(f1814,plain,
! [X0,X1,X2] :
( X0 = sK7_skl
| X0 = X2
| sK7_skl = X2
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X2,vd1197)
| ron(X2,X1)
| ~ rpoint(sK7_skl)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rline(X1)
| ~ ron(sK7_skl,X1)
| ~ ron(X0,X1) ),
inference(resolution,[status(thm)],[f1790,f1554]) ).
fof(f1820,plain,
! [X0,X1,X2] :
( X0 = sK8_skl
| X0 = X2
| sK8_skl = X2
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X2,vd1197)
| ron(X2,X1)
| ~ rpoint(sK8_skl)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rline(X1)
| ~ ron(sK8_skl,X1)
| ~ ron(X0,X1) ),
inference(resolution,[status(thm)],[f1790,f1468]) ).
fof(f1831,definition,
! [X0,X1,X2] :
( sQ84_spl
<=> ( X0 = sK1_skl
| X0 = X1
| sK1_skl = X1
| ~ rline(X2)
| ~ ron(X0,X2)
| ~ ron(sK1_skl,X2)
| ~ ron(X1,X2)
| ron(X1,vd1232)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X0,vd1232) ) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f1832,plain,
! [X0,X1,X2] :
( ~ sQ84_spl
| X0 = sK1_skl
| X0 = X1
| sK1_skl = X1
| ~ rline(X2)
| ~ ron(X0,X2)
| ~ ron(sK1_skl,X2)
| ~ ron(X1,X2)
| ron(X1,vd1232)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X0,vd1232) ),
inference(component_clause,[status(thm)],[f1831]) ).
fof(f1834,plain,
( ~ sQ31_spl
| ~ sQ66_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f1792,f1831,f1506,f1159]) ).
fof(f1842,definition,
! [X0,X1,X2] :
( sQ87_spl
<=> ( X0 = sK7_skl
| X0 = X1
| sK7_skl = X1
| ~ rline(X2)
| ~ ron(X0,X2)
| ~ ron(sK7_skl,X2)
| ~ ron(X1,X2)
| ron(X1,vd1197)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X0,vd1197) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1845,plain,
( ~ sQ61_spl
| ~ sQ69_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f1794,f1842,f1534,f1434]) ).
fof(f1857,definition,
! [X0,X1,X2] :
( sQ90_spl
<=> ( X0 = sK8_skl
| X0 = X1
| sK8_skl = X1
| ~ rline(X2)
| ~ ron(X0,X2)
| ~ ron(sK8_skl,X2)
| ~ ron(X1,X2)
| ron(X1,vd1197)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X0,vd1197) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f1860,plain,
( ~ sQ44_spl
| ~ sQ69_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f1800,f1857,f1534,f1254]) ).
fof(f1865,definition,
! [X0,X1,X2] :
( sQ92_spl
<=> ( X0 = X2
| X0 = sK1_skl
| X2 = sK1_skl
| ~ ron(X0,vd1232)
| ~ ron(X2,vd1232)
| ron(sK1_skl,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f1868,plain,
( ~ sQ66_spl
| ~ sQ31_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f1802,f1865,f1159,f1506]) ).
fof(f1873,definition,
! [X0,X1,X2] :
( sQ94_spl
<=> ( X0 = X2
| X0 = sK7_skl
| X2 = sK7_skl
| ~ ron(X0,vd1197)
| ~ ron(X2,vd1197)
| ron(sK7_skl,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f1876,plain,
( ~ sQ69_spl
| ~ sQ61_spl
| sQ94_spl ),
inference(split_clause,[status(thm)],[f1804,f1873,f1434,f1534]) ).
fof(f1888,definition,
! [X0,X1,X2] :
( sQ97_spl
<=> ( X0 = X2
| X0 = sK8_skl
| X2 = sK8_skl
| ~ ron(X0,vd1197)
| ~ ron(X2,vd1197)
| ron(sK8_skl,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f1891,plain,
( ~ sQ69_spl
| ~ sQ44_spl
| sQ97_spl ),
inference(split_clause,[status(thm)],[f1810,f1888,f1254,f1534]) ).
fof(f1896,definition,
! [X0,X1,X2] :
( sQ99_spl
<=> ( X0 = sK1_skl
| X0 = X2
| sK1_skl = X2
| ~ ron(X0,vd1232)
| ~ ron(X2,vd1232)
| ron(X2,X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rline(X1)
| ~ ron(sK1_skl,X1)
| ~ ron(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f1899,plain,
( ~ sQ66_spl
| ~ sQ31_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f1812,f1896,f1159,f1506]) ).
fof(f1904,definition,
! [X0,X1,X2] :
( sQ101_spl
<=> ( X0 = sK7_skl
| X0 = X2
| sK7_skl = X2
| ~ ron(X0,vd1197)
| ~ ron(X2,vd1197)
| ron(X2,X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rline(X1)
| ~ ron(sK7_skl,X1)
| ~ ron(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1907,plain,
( ~ sQ69_spl
| ~ sQ61_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f1814,f1904,f1434,f1534]) ).
fof(f1928,definition,
! [X0,X1,X2] :
( sQ107_spl
<=> ( X0 = sK8_skl
| X0 = X2
| sK8_skl = X2
| ~ ron(X0,vd1197)
| ~ ron(X2,vd1197)
| ron(X2,X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rline(X1)
| ~ ron(sK8_skl,X1)
| ~ ron(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1931,plain,
( ~ sQ69_spl
| ~ sQ44_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f1820,f1928,f1254,f1534]) ).
fof(f1937,plain,
! [X0,X1] :
( ~ sQ84_spl
| X0 = sK1_skl
| X0 = X1
| sK1_skl = X1
| ~ rline(vd1232)
| ~ ron(X0,vd1232)
| ~ ron(X1,vd1232)
| ron(X1,vd1232)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X0,vd1232) ),
inference(resolution,[status(thm)],[f1832,f1101]) ).
fof(f1938,definition,
! [X0,X1] :
( sQ108_spl
<=> ( X0 = sK1_skl
| X0 = X1
| sK1_skl = X1
| ~ ron(X0,vd1232)
| ~ ron(X1,vd1232)
| ron(X1,vd1232)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X0,vd1232) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1941,plain,
( ~ sQ84_spl
| ~ sQ66_spl
| sQ108_spl ),
inference(split_clause,[status(thm)],[f1937,f1938,f1506,f1831]) ).
fof(f1967,definition,
( sQ112_spl
<=> sK7_skl = sK1_skl ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1968,plain,
( ~ sQ112_spl
| sK7_skl = sK1_skl ),
inference(component_clause,[status(thm)],[f1967]) ).
fof(f2012,plain,
( ~ sQ112_spl
| ~ ron(sK7_skl,vd1197) ),
inference(backward_demodulation,[status(thm)],[f1968,f1576]) ).
fof(f2021,plain,
( ~ sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2012,f1554]) ).
fof(f2022,plain,
~ sQ112_spl,
inference(contradiction_clause,[status(thm)],[f2021]) ).
fof(f2050,plain,
! [X0] :
( vf(X0,X0) = vd684
| ~ rpoint(X0) ),
inference(forward_demodulation,[status(thm)],[f368,f806]) ).
fof(f2051,plain,
( sQ81_spl
| ~ rpoint(sK8_skl) ),
inference(resolution,[status(thm)],[f2050,f1756]) ).
fof(f2053,plain,
( sQ81_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f2051,f1254,f1754]) ).
fof(f2054,plain,
$false,
inference(sat_refutation,[status(thm)],[f753,f754,f755,f765,f766,f767,f786,f790,f797,f1094,f1108,f1111,f1115,f1187,f1192,f1279,f1306,f1326,f1381,f1419,f1443,f1446,f1448,f1450,f1511,f1513,f1540,f1542,f1559,f1561,f1572,f1597,f1602,f1608,f1625,f1635,f1656,f1761,f1777,f1834,f1845,f1860,f1868,f1876,f1891,f1899,f1907,f1931,f1941,f2022,f2053]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO298+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/5.45 % Computer : n026.cluster.edu
% 0.19/5.45 % Model : x86_64 x86_64
% 0.19/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.45 % Memory : 8046.5625MB
% 0.19/5.45 % OS : Linux 6.8.0-71-generic
% 0.19/5.45 % CPULimit : 300
% 0.19/5.45 % WCLimit : 300
% 0.19/5.45 % DateTime : Sun Sep 20 15:15:43 UTC 2026
% 0.19/5.46 % CPUTime :
% 0.23/5.50 % Drodi V4.1.1
% 0.23/5.83 % Refutation found
% 0.23/5.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/5.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.23/5.87 % Elapsed time: 0.392923 seconds
% 0.23/5.87 % CPU time: 2.321542 seconds
% 0.23/5.87 % Total memory used: 132.054 MB
% 0.23/5.87 % Net memory used: 130.325 MB
%------------------------------------------------------------------------------