%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO295+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:24:51 PM UTC 2026
% Result : Theorem 0.14s 1.06s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 24
% Syntax : Number of formulae : 152 ( 56 unt; 0 def)
% Number of atoms : 1181 ( 393 equ)
% Maximal formula atoms : 33 ( 7 avg)
% Number of connectives : 1686 ( 657 ~; 918 |; 103 &)
% ( 2 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 42 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 20 con; 0-3 aty)
% Number of variables : 255 ( 228 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1186,vd1185,vd1201) = vplus(vangle(vd1186,vd1185,vd1187),vangle(vd1187,vd1185,vd1201)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
vangle(vd1186,vd1185,vd1201) != vplus(vangle(vd1186,vd1185,vd1187),vangle(vd1187,vd1185,vd1201)),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
rS(vd1200,vd1187,vd1234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
~ ron(vd1201,vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Vd874,Vd875,Vd876,Vd877,Vd883,Vd884] :
( ( ? [Vd879] :
( rpoint(Vd879)
& Vd874 = Vd879 )
& ? [Vd880] :
( rpoint(Vd880)
& Vd875 = Vd880 )
& ? [Vd881] :
( rpoint(Vd881)
& Vd876 = Vd881 )
& ? [Vd882] :
( rpoint(Vd882)
& Vd877 = Vd882 )
& ? [Vd886] :
( rline(Vd886)
& Vd883 = Vd886 )
& ? [Vd887] :
( rline(Vd887)
& Vd884 = Vd887 )
& ron(Vd874,Vd883)
& ron(Vd874,Vd884)
& ron(Vd875,Vd883)
& ron(Vd876,Vd884)
& Vd874 != Vd875
& Vd874 != Vd876
& ~ ron(Vd877,Vd883)
& ~ ron(Vd877,Vd884)
& Vd883 != Vd884 )
=> ( vangle(Vd875,Vd874,Vd876) = vplus(vangle(Vd875,Vd874,Vd877),vangle(Vd877,Vd874,Vd876))
<=> ( rS(Vd875,Vd877,Vd884)
& rS(Vd876,Vd877,Vd883) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
ron(vd1201,vd1234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
ron(vd1185,vd1234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
rline(vd1234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
ron(vd1187,vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
ron(vd1185,vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
rline(vd1232),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
ron(vd1185,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
rS(vd1201,vd1187,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
? [Vd1205] :
( rpoint(Vd1205)
& vd1201 = Vd1205 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
rline(vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
( ? [Vd1182] :
( rpoint(Vd1182)
& vd1178 = Vd1182 )
& ? [Vd1183] :
( rpoint(Vd1183)
& vd1179 = Vd1183 )
& ? [Vd1184] :
( rpoint(Vd1184)
& vd1180 = Vd1184 )
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& ? [Vd1189] :
( rpoint(Vd1189)
& vd1185 = Vd1189 )
& ? [Vd1190] :
( rpoint(Vd1190)
& vd1186 = Vd1190 )
& ? [Vd1191] :
( rpoint(Vd1191)
& vd1187 = Vd1191 )
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& ~ ? [Vd1195] :
( rline(Vd1195)
& ron(vd1185,Vd1195)
& ron(vd1186,Vd1195)
& ron(vd1187,Vd1195) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [Vd434,Vd435,Vd439,Vd440] :
( ( ? [Vd437] :
( rpoint(Vd437)
& Vd434 = Vd437 )
& ? [Vd438] :
( rpoint(Vd438)
& Vd435 = Vd438 )
& rline(Vd440)
& Vd439 = Vd440
& rS(Vd434,Vd435,Vd439) )
=> ~ ron(Vd434,Vd439) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Vd314,Vd315,Vd319,Vd320] :
( ( ? [Vd317] :
( rpoint(Vd317)
& Vd314 = Vd317 )
& ? [Vd318] :
( rpoint(Vd318)
& Vd315 = Vd318 )
& Vd314 != Vd315
& ? [Vd323] :
( rline(Vd323)
& Vd319 = Vd323 )
& ? [Vd324] :
( rline(Vd324)
& Vd320 = Vd324 )
& ron(Vd314,Vd319)
& ron(Vd314,Vd320)
& ron(Vd315,Vd319)
& ron(Vd315,Vd320) )
=> Vd319 = Vd320 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
ron(vd1200,vd1197),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
vd1200 = vd1186,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
? [Vd1204] :
( rpoint(Vd1204)
& vd1200 = Vd1204 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
( vd1199 != vd1185
=> ( rR(vd1199,vd1185,vd1186)
| rR(vd1185,vd1199,vd1186) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
( vd1199 != vd1185
=> ~ rR(vd1185,vd1199,vd1186) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
( vd1199 != vd1185
=> ~ rR(vd1199,vd1185,vd1186) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f152,plain,
vangle(vd1186,vd1185,vd1201) != vplus(vangle(vd1186,vd1185,vd1187),vangle(vd1187,vd1185,vd1201)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f153,plain,
rS(vd1200,vd1187,vd1234),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f155,plain,
~ ron(vd1201,vd1232),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f156,plain,
! [Vd874,Vd875,Vd876,Vd877,Vd883,Vd884] :
( ( vangle(Vd875,Vd874,Vd876) = vplus(vangle(Vd875,Vd874,Vd877),vangle(Vd877,Vd874,Vd876))
<=> ( rS(Vd875,Vd877,Vd884)
& rS(Vd876,Vd877,Vd883) ) )
| ! [Vd879] :
( ~ rpoint(Vd879)
| Vd874 != Vd879 )
| ! [Vd880] :
( ~ rpoint(Vd880)
| Vd875 != Vd880 )
| ! [Vd881] :
( ~ rpoint(Vd881)
| Vd876 != Vd881 )
| ! [Vd882] :
( ~ rpoint(Vd882)
| Vd877 != Vd882 )
| ! [Vd886] :
( ~ rline(Vd886)
| Vd883 != Vd886 )
| ! [Vd887] :
( ~ rline(Vd887)
| Vd884 != Vd887 )
| ~ ron(Vd874,Vd883)
| ~ ron(Vd874,Vd884)
| ~ ron(Vd875,Vd883)
| ~ ron(Vd876,Vd884)
| Vd874 = Vd875
| Vd874 = Vd876
| ron(Vd877,Vd883)
| ron(Vd877,Vd884)
| Vd883 = Vd884 ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f157,plain,
! [Vd874,Vd875,Vd876,Vd877,Vd883,Vd884] :
( ( ( ~ rS(Vd875,Vd877,Vd884)
| ~ rS(Vd876,Vd877,Vd883)
| vangle(Vd875,Vd874,Vd876) = vplus(vangle(Vd875,Vd874,Vd877),vangle(Vd877,Vd874,Vd876)) )
& ( ( rS(Vd875,Vd877,Vd884)
& rS(Vd876,Vd877,Vd883) )
| vangle(Vd875,Vd874,Vd876) != vplus(vangle(Vd875,Vd874,Vd877),vangle(Vd877,Vd874,Vd876)) ) )
| ! [Vd879] :
( ~ rpoint(Vd879)
| Vd874 != Vd879 )
| ! [Vd880] :
( ~ rpoint(Vd880)
| Vd875 != Vd880 )
| ! [Vd881] :
( ~ rpoint(Vd881)
| Vd876 != Vd881 )
| ! [Vd882] :
( ~ rpoint(Vd882)
| Vd877 != Vd882 )
| ! [Vd886] :
( ~ rline(Vd886)
| Vd883 != Vd886 )
| ! [Vd887] :
( ~ rline(Vd887)
| Vd884 != Vd887 )
| ~ ron(Vd874,Vd883)
| ~ ron(Vd874,Vd884)
| ~ ron(Vd875,Vd883)
| ~ ron(Vd876,Vd884)
| Vd874 = Vd875
| Vd874 = Vd876
| ron(Vd877,Vd883)
| ron(Vd877,Vd884)
| Vd883 = Vd884 ),
inference(NNF_transformation,[status(thm)],[f156]) ).
fof(f159,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( rS(X5,X2,X1)
| vangle(X5,X3,X4) != vplus(vangle(X5,X3,X2),vangle(X2,X3,X4))
| ~ rpoint(X11)
| X3 != X11
| ~ rpoint(X10)
| X5 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rpoint(X8)
| X2 != X8
| ~ rline(X7)
| X0 != X7
| ~ rline(X6)
| X1 != X6
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X5,X0)
| ~ ron(X4,X1)
| X3 = X5
| X3 = X4
| ron(X2,X0)
| ron(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f160,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( ~ rS(X5,X2,X1)
| ~ rS(X4,X2,X0)
| vangle(X5,X3,X4) = vplus(vangle(X5,X3,X2),vangle(X2,X3,X4))
| ~ rpoint(X11)
| X3 != X11
| ~ rpoint(X10)
| X5 != X10
| ~ rpoint(X9)
| X4 != X9
| ~ rpoint(X8)
| X2 != X8
| ~ rline(X7)
| X0 != X7
| ~ rline(X6)
| X1 != X6
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X5,X0)
| ~ ron(X4,X1)
| X3 = X5
| X3 = X4
| ron(X2,X0)
| ron(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f161,plain,
ron(vd1201,vd1234),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f162,plain,
ron(vd1185,vd1234),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f163,plain,
rline(vd1234),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f164,plain,
ron(vd1187,vd1232),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f165,plain,
ron(vd1185,vd1232),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f166,plain,
rline(vd1232),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f167,plain,
ron(vd1185,vd1197),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f168,plain,
rS(vd1201,vd1187,vd1197),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f169,plain,
( rpoint(sK0_skl)
& vd1201 = sK0_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1205,sK0_skl)],[f15]) ).
fof(f170,plain,
vd1201 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f171,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f172,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f173,plain,
rline(vd1197),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f174,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)],[f18]) ).
fof(f175,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)],[f174]) ).
fof(f176,plain,
! [X0] :
( ~ rline(X0)
| ~ ron(vd1185,X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1187,X0) ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f180,plain,
vd1187 = sK1_skl,
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f181,plain,
rpoint(sK1_skl),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f184,plain,
vd1185 = sK3_skl,
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f185,plain,
rpoint(sK3_skl),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f201,plain,
! [Vd434,Vd435,Vd439,Vd440] :
( ~ ron(Vd434,Vd439)
| ! [Vd437] :
( ~ rpoint(Vd437)
| Vd434 != Vd437 )
| ! [Vd438] :
( ~ rpoint(Vd438)
| Vd435 != Vd438 )
| ~ rline(Vd440)
| Vd439 != Vd440
| ~ rS(Vd434,Vd435,Vd439) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f202,plain,
! [Vd434,Vd439] :
( ~ ron(Vd434,Vd439)
| ! [Vd437] :
( ~ rpoint(Vd437)
| Vd434 != Vd437 )
| ! [Vd435] :
( ! [Vd438] :
( ~ rpoint(Vd438)
| Vd435 != Vd438 )
| ! [Vd440] :
( ~ rline(Vd440)
| Vd439 != Vd440
| ~ rS(Vd434,Vd435,Vd439) ) ) ),
inference(miniscoping,[status(thm)],[f201]) ).
fof(f203,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ ron(X0,X2)
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rline(X3)
| X2 != X3
| ~ rS(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f204,plain,
! [Vd314,Vd315,Vd319,Vd320] :
( Vd319 = Vd320
| ! [Vd317] :
( ~ rpoint(Vd317)
| Vd314 != Vd317 )
| ! [Vd318] :
( ~ rpoint(Vd318)
| Vd315 != Vd318 )
| Vd314 = Vd315
| ! [Vd323] :
( ~ rline(Vd323)
| Vd319 != Vd323 )
| ! [Vd324] :
( ~ rline(Vd324)
| Vd320 != Vd324 )
| ~ ron(Vd314,Vd319)
| ~ ron(Vd314,Vd320)
| ~ ron(Vd315,Vd319)
| ~ ron(Vd315,Vd320) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f205,plain,
! [Vd319,Vd320] :
( Vd319 = Vd320
| ! [Vd314] :
( ! [Vd317] :
( ~ rpoint(Vd317)
| Vd314 != Vd317 )
| ! [Vd315] :
( ! [Vd318] :
( ~ rpoint(Vd318)
| Vd315 != Vd318 )
| Vd314 = Vd315
| ! [Vd323] :
( ~ rline(Vd323)
| Vd319 != Vd323 )
| ! [Vd324] :
( ~ rline(Vd324)
| Vd320 != Vd324 )
| ~ ron(Vd314,Vd319)
| ~ ron(Vd314,Vd320)
| ~ ron(Vd315,Vd319)
| ~ ron(Vd315,Vd320) ) ) ),
inference(miniscoping,[status(thm)],[f204]) ).
fof(f206,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( X2 = X1
| ~ rpoint(X7)
| X3 != X7
| ~ rpoint(X6)
| X0 != X6
| X3 = X0
| ~ rline(X5)
| X2 != X5
| ~ rline(X4)
| X1 != X4
| ~ ron(X3,X2)
| ~ ron(X3,X1)
| ~ ron(X0,X2)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f207,plain,
ron(vd1200,vd1197),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f215,plain,
vd1200 = vd1186,
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f222,plain,
( rpoint(sK7_skl)
& vd1200 = sK7_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Vd1204,sK7_skl)],[f37]) ).
fof(f223,plain,
vd1200 = sK7_skl,
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f224,plain,
rpoint(sK7_skl),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f273,plain,
( rR(vd1199,vd1185,vd1186)
| rR(vd1185,vd1199,vd1186)
| vd1199 = vd1185 ),
inference(pre_NNF_transformation,[status(thm)],[f48]) ).
fof(f274,plain,
( rR(vd1199,vd1185,vd1186)
| rR(vd1185,vd1199,vd1186)
| vd1199 = vd1185 ),
inference(cnf_transformation,[status(thm)],[f273]) ).
fof(f275,plain,
( ~ rR(vd1185,vd1199,vd1186)
| vd1199 = vd1185 ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f276,plain,
( ~ rR(vd1185,vd1199,vd1186)
| vd1199 = vd1185 ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f277,plain,
( ~ rR(vd1199,vd1185,vd1186)
| vd1199 = vd1185 ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f278,plain,
( ~ rR(vd1199,vd1185,vd1186)
| vd1199 = vd1185 ),
inference(cnf_transformation,[status(thm)],[f277]) ).
fof(f724,plain,
! [X0,X1,X2,X3,X4,X5] :
( rS(X5,X2,X1)
| vangle(X5,X3,X4) != vplus(vangle(X5,X3,X2),vangle(X2,X3,X4))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X2)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X5,X0)
| ~ ron(X4,X1)
| X3 = X5
| X3 = X4
| ron(X2,X0)
| ron(X2,X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f159]) ).
fof(f725,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ rS(X5,X2,X1)
| ~ rS(X4,X2,X0)
| vangle(X5,X3,X4) = vplus(vangle(X5,X3,X2),vangle(X2,X3,X4))
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X2)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X5,X0)
| ~ ron(X4,X1)
| X3 = X5
| X3 = X4
| ron(X2,X0)
| ron(X2,X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f160]) ).
fof(f729,plain,
! [X0,X1,X2] :
( ~ ron(X0,X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(X2)
| ~ rS(X0,X1,X2) ),
inference(destructive_equality_resolution,[status(thm)],[f203]) ).
fof(f730,plain,
! [X0,X1,X2,X3] :
( X2 = X1
| ~ rpoint(X3)
| ~ rpoint(X0)
| X3 = X0
| ~ rline(X2)
| ~ rline(X1)
| ~ ron(X3,X2)
| ~ ron(X3,X1)
| ~ ron(X0,X2)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f206]) ).
fof(f949,plain,
vd1199 = vd1185,
inference(backward_subsumption_resolution,[status(thm)],[f278,f950]) ).
fof(f950,plain,
( rR(vd1199,vd1185,vd1186)
| vd1199 = vd1185 ),
inference(forward_subsumption_resolution,[status(thm)],[f274,f276]) ).
fof(f952,plain,
! [X0] :
( ~ rline(X0)
| ~ ron(vd1199,X0)
| ~ ron(vd1186,X0)
| ~ ron(vd1187,X0) ),
inference(backward_demodulation,[status(thm)],[f949,f176]) ).
fof(f955,plain,
vangle(vd1186,vd1185,vd1201) != vplus(vangle(vd1186,vd1185,vd1187),vangle(vd1187,vd1199,vd1201)),
inference(backward_demodulation,[status(thm)],[f949,f152]) ).
fof(f956,plain,
vangle(vd1186,vd1199,vd1201) != vplus(vangle(vd1186,vd1185,vd1187),vangle(vd1187,vd1199,vd1201)),
inference(forward_demodulation,[status(thm)],[f949,f955]) ).
fof(f957,plain,
vangle(vd1186,vd1199,vd1201) != vplus(vangle(vd1186,vd1199,vd1187),vangle(vd1187,vd1199,vd1201)),
inference(forward_demodulation,[status(thm)],[f949,f956]) ).
fof(f958,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rS(X5,X2,X7)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X2)
| ~ rline(X6)
| ~ rline(X7)
| ~ ron(X3,X6)
| ~ ron(X3,X7)
| ~ ron(X5,X6)
| ~ ron(X4,X7)
| X3 = X5
| X3 = X4
| ron(X2,X6)
| ron(X2,X7)
| X6 = X7
| ~ rS(X5,X2,X1)
| ~ rS(X4,X2,X0)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X2)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X5,X0)
| ~ ron(X4,X1)
| X3 = X5
| X3 = X4
| ron(X2,X0)
| ron(X2,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f725,f724]) ).
fof(f962,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( rS(X5,X2,X7)
| ~ rline(X6)
| ~ rline(X7)
| ~ ron(X3,X6)
| ~ ron(X3,X7)
| ~ ron(X5,X6)
| ~ ron(X4,X7)
| ron(X2,X6)
| ron(X2,X7)
| X6 = X7
| ~ rS(X5,X2,X1)
| ~ rS(X4,X2,X0)
| ~ rpoint(X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X2)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(X3,X0)
| ~ ron(X3,X1)
| ~ ron(X5,X0)
| ~ ron(X4,X1)
| X3 = X5
| X3 = X4
| ron(X2,X0)
| ron(X2,X1)
| X0 = X1 ),
inference(duplicate_literals_removal,[status(thm)],[f958]) ).
fof(f966,plain,
rpoint(vd1201),
inference(forward_demodulation,[status(thm)],[f170,f171]) ).
fof(f967,plain,
rpoint(vd1187),
inference(forward_demodulation,[status(thm)],[f180,f181]) ).
fof(f969,plain,
vd1199 = sK3_skl,
inference(forward_demodulation,[status(thm)],[f949,f184]) ).
fof(f970,plain,
rpoint(vd1199),
inference(forward_demodulation,[status(thm)],[f969,f185]) ).
fof(f971,plain,
! [X0,X1] :
( ~ rS(vd1186,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rpoint(vd1186)
| ~ rpoint(vd1201)
| ~ rpoint(vd1187)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1186,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1186
| vd1199 = vd1201
| ron(vd1187,X0)
| ron(vd1187,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f957,f725]) ).
fof(f972,plain,
! [X0,X1] :
( ~ rS(vd1186,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rpoint(vd1186)
| ~ rpoint(vd1201)
| ~ rpoint(vd1187)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1186,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1186
| vd1199 = vd1201
| ron(vd1187,X1)
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f971,f952]) ).
fof(f973,plain,
! [X0,X1] :
( ~ rS(vd1186,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rpoint(vd1186)
| ~ rpoint(vd1201)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1186,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1186
| vd1199 = vd1201
| ron(vd1187,X1)
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f972,f967]) ).
fof(f974,plain,
! [X0,X1,X2,X3,X4] :
( rS(vd1200,vd1187,X4)
| ~ rline(X3)
| ~ rline(X4)
| ~ ron(X1,X3)
| ~ ron(X1,X4)
| ~ ron(vd1200,X3)
| ~ ron(X2,X4)
| ron(vd1187,X3)
| ron(vd1187,X4)
| X3 = X4
| ~ rS(X2,vd1187,X0)
| ~ rpoint(X1)
| ~ rpoint(vd1200)
| ~ rpoint(X2)
| ~ rpoint(vd1187)
| ~ rline(X0)
| ~ rline(vd1234)
| ~ ron(X1,X0)
| ~ ron(X1,vd1234)
| ~ ron(vd1200,X0)
| ~ ron(X2,vd1234)
| X1 = vd1200
| X1 = X2
| ron(vd1187,X0)
| ron(vd1187,vd1234)
| X0 = vd1234 ),
inference(resolution,[status(thm)],[f962,f153]) ).
fof(f975,plain,
! [X0,X1,X2,X3,X4] :
( rS(vd1200,vd1187,X4)
| ~ rline(X3)
| ~ rline(X4)
| ~ ron(X1,X3)
| ~ ron(X1,X4)
| ~ ron(vd1200,X3)
| ~ ron(X2,X4)
| ron(vd1187,X3)
| ron(vd1187,X4)
| X3 = X4
| ~ rS(X2,vd1187,X0)
| ~ rpoint(X1)
| ~ rpoint(vd1200)
| ~ rpoint(X2)
| ~ rpoint(vd1187)
| ~ rline(X0)
| ~ ron(X1,X0)
| ~ ron(X1,vd1234)
| ~ ron(vd1200,X0)
| ~ ron(X2,vd1234)
| X1 = vd1200
| X1 = X2
| ron(vd1187,X0)
| ron(vd1187,vd1234)
| X0 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f974,f163]) ).
fof(f976,plain,
! [X0,X1,X2,X3,X4] :
( rS(vd1200,vd1187,X4)
| ~ rline(X3)
| ~ rline(X4)
| ~ ron(X1,X3)
| ~ ron(X1,X4)
| ~ ron(vd1200,X3)
| ~ ron(X2,X4)
| ron(vd1187,X3)
| ron(vd1187,X4)
| X3 = X4
| ~ rS(X2,vd1187,X0)
| ~ rpoint(X1)
| ~ rpoint(vd1200)
| ~ rpoint(X2)
| ~ rline(X0)
| ~ ron(X1,X0)
| ~ ron(X1,vd1234)
| ~ ron(vd1200,X0)
| ~ ron(X2,vd1234)
| X1 = vd1200
| X1 = X2
| ron(vd1187,X0)
| ron(vd1187,vd1234)
| X0 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f975,f967]) ).
fof(f997,plain,
! [X0,X1] :
( ~ rS(vd1200,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rpoint(vd1186)
| ~ rpoint(vd1201)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1186,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1186
| vd1199 = vd1201
| ron(vd1187,X1)
| X0 = X1 ),
inference(backward_demodulation,[status(thm)],[f215,f973]) ).
fof(f1002,plain,
! [X0] :
( ~ rline(X0)
| ~ ron(vd1199,X0)
| ~ ron(vd1200,X0)
| ~ ron(vd1187,X0) ),
inference(backward_demodulation,[status(thm)],[f215,f952]) ).
fof(f1030,plain,
! [X0,X1] :
( ~ rS(vd1200,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rpoint(vd1186)
| ~ rpoint(vd1201)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1186,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X1)
| X0 = X1 ),
inference(forward_demodulation,[status(thm)],[f215,f997]) ).
fof(f1031,plain,
! [X0,X1] :
( ~ rS(vd1200,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rpoint(vd1186)
| ~ rpoint(vd1201)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1200,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X1)
| X0 = X1 ),
inference(forward_demodulation,[status(thm)],[f215,f1030]) ).
fof(f1032,plain,
! [X0,X1] :
( ~ rS(vd1200,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rpoint(vd1200)
| ~ rpoint(vd1201)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1200,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X1)
| X0 = X1 ),
inference(forward_demodulation,[status(thm)],[f215,f1031]) ).
fof(f1033,plain,
! [X0,X1] :
( ~ rS(vd1200,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rpoint(vd1200)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1200,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X1)
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1032,f966]) ).
fof(f1035,plain,
! [X0,X1,X2,X3,X4] :
( rS(vd1200,vd1187,X4)
| ~ rline(X3)
| ~ rline(X4)
| ~ ron(X1,X3)
| ~ ron(X1,X4)
| ~ ron(vd1200,X3)
| ~ ron(X2,X4)
| ron(vd1187,X3)
| ron(vd1187,X4)
| X3 = X4
| ~ rS(X2,vd1187,X0)
| ~ rpoint(X1)
| ~ rpoint(X2)
| ~ rline(X0)
| ~ ron(X1,X0)
| ~ ron(X1,vd1234)
| ~ ron(vd1200,X0)
| ~ ron(X2,vd1234)
| X1 = vd1200
| X1 = X2
| ron(vd1187,X0)
| ron(vd1187,vd1234)
| X0 = vd1234 ),
inference(backward_subsumption_resolution,[status(thm)],[f976,f1036]) ).
fof(f1036,plain,
rpoint(vd1200),
inference(forward_demodulation,[status(thm)],[f223,f224]) ).
fof(f1037,plain,
ron(vd1199,vd1234),
inference(forward_demodulation,[status(thm)],[f949,f162]) ).
fof(f1044,plain,
! [X0,X1] :
( ~ rS(vd1200,vd1187,X1)
| ~ rS(vd1201,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rline(X0)
| ~ rline(X1)
| ~ ron(vd1199,X0)
| ~ ron(vd1199,X1)
| ~ ron(vd1200,X0)
| ~ ron(vd1201,X1)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X1)
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1033,f1036]) ).
fof(f1047,plain,
( ~ rline(vd1232)
| ~ ron(vd1199,vd1232)
| ~ ron(vd1200,vd1232) ),
inference(resolution,[status(thm)],[f1002,f164]) ).
fof(f1048,plain,
( ~ ron(vd1199,vd1232)
| ~ ron(vd1200,vd1232) ),
inference(forward_subsumption_resolution,[status(thm)],[f1047,f166]) ).
fof(f1051,plain,
~ ron(vd1200,vd1232),
inference(backward_subsumption_resolution,[status(thm)],[f1048,f1052]) ).
fof(f1052,plain,
ron(vd1199,vd1232),
inference(forward_demodulation,[status(thm)],[f949,f165]) ).
fof(f1053,plain,
ron(vd1199,vd1197),
inference(forward_demodulation,[status(thm)],[f949,f167]) ).
fof(f1056,plain,
! [X0] :
( ~ rS(vd1200,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rline(vd1197)
| ~ rline(X0)
| ~ ron(vd1199,vd1197)
| ~ ron(vd1199,X0)
| ~ ron(vd1200,vd1197)
| ~ ron(vd1201,X0)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X0)
| vd1197 = X0 ),
inference(resolution,[status(thm)],[f168,f1044]) ).
fof(f1057,plain,
! [X0,X1,X2] :
( rS(vd1200,vd1187,X2)
| ~ rline(X1)
| ~ rline(X2)
| ~ ron(X0,X1)
| ~ ron(X0,X2)
| ~ ron(vd1200,X1)
| ~ ron(vd1201,X2)
| ron(vd1187,X1)
| ron(vd1187,X2)
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| ~ ron(vd1200,vd1197)
| ~ ron(vd1201,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1197)
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(resolution,[status(thm)],[f168,f1035]) ).
fof(f1059,plain,
! [X0] :
( ~ rS(vd1200,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rline(vd1197)
| ~ rline(X0)
| ~ ron(vd1199,vd1197)
| ~ ron(vd1199,X0)
| ~ ron(vd1201,X0)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X0)
| vd1197 = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1056,f207]) ).
fof(f1060,plain,
! [X0,X1,X2] :
( rS(vd1200,vd1187,X2)
| ~ rline(X1)
| ~ rline(X2)
| ~ ron(X0,X1)
| ~ ron(X0,X2)
| ~ ron(vd1200,X1)
| ~ ron(vd1201,X2)
| ron(vd1187,X1)
| ron(vd1187,X2)
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| ~ ron(vd1200,vd1197)
| ~ ron(vd1201,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1057,f172]) ).
fof(f1169,plain,
! [X0] :
( ~ rS(vd1200,vd1187,X0)
| ~ rpoint(vd1199)
| ~ rline(vd1197)
| ~ rline(X0)
| ~ ron(vd1199,X0)
| ~ ron(vd1201,X0)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X0)
| vd1197 = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1059,f1053]) ).
fof(f1241,plain,
! [X0,X1,X2] :
( rS(vd1200,vd1187,X2)
| ~ rline(X1)
| ~ rline(X2)
| ~ ron(X0,X1)
| ~ ron(X0,X2)
| ~ ron(vd1200,X1)
| ~ ron(vd1201,X2)
| ron(vd1187,X1)
| ron(vd1187,X2)
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| ~ ron(vd1200,vd1197)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1060,f161]) ).
fof(f1243,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1199)
| ~ rline(vd1197)
| ~ rline(X2)
| ~ ron(vd1199,X2)
| ~ ron(vd1201,X2)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,X2)
| vd1197 = X2
| ~ rline(X1)
| ~ rline(X2)
| ~ ron(X0,X1)
| ~ ron(X0,X2)
| ~ ron(vd1200,X1)
| ~ ron(vd1201,X2)
| ron(vd1187,X1)
| ron(vd1187,X2)
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| ~ ron(vd1200,vd1197)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(resolution,[status(thm)],[f1241,f1169]) ).
fof(f1253,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,X2)
| vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = X2
| ~ rline(X1)
| ~ rline(X2)
| ~ ron(X0,X1)
| ~ ron(X0,X2)
| ~ ron(vd1200,X1)
| ~ ron(vd1201,X2)
| ron(vd1187,X1)
| ron(vd1187,X2)
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| ~ ron(vd1200,vd1197)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(duplicate_literals_removal,[status(thm)],[f1243]) ).
fof(f1254,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,X2)
| vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = X2
| ~ rline(X1)
| ~ rline(X2)
| ~ ron(X0,X1)
| ~ ron(X0,X2)
| ~ ron(vd1200,X1)
| ~ ron(vd1201,X2)
| ron(vd1187,X1)
| ron(vd1187,X2)
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1253,f207]) ).
fof(f1269,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,X2)
| vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = X2
| ~ rline(X1)
| ~ rline(X2)
| ~ ron(X0,X1)
| ~ ron(X0,X2)
| ~ ron(vd1200,X1)
| ~ ron(vd1201,X2)
| ron(vd1187,X1)
| ron(vd1187,X2)
| X1 = X2
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1254,f173]) ).
fof(f1270,plain,
! [X0,X1] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1234)
| vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| ~ rline(X1)
| ~ rline(vd1234)
| ~ ron(X0,X1)
| ~ ron(X0,vd1234)
| ~ ron(vd1200,X1)
| ron(vd1187,X1)
| ron(vd1187,vd1234)
| X1 = vd1234
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(resolution,[status(thm)],[f1269,f161]) ).
fof(f1275,plain,
! [X0,X1] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1234)
| vd1199 = vd1200
| vd1199 = vd1201
| ~ rline(X1)
| ~ rline(vd1234)
| ~ ron(X0,X1)
| ~ ron(vd1200,X1)
| ron(vd1187,X1)
| X1 = vd1234
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(duplicate_literals_removal,[status(thm)],[f1270]) ).
fof(f1276,plain,
! [X0,X1] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1234)
| vd1199 = vd1200
| vd1199 = vd1201
| ~ rline(X1)
| ~ rline(vd1234)
| ~ ron(X0,X1)
| ~ ron(vd1200,X1)
| ron(vd1187,X1)
| X1 = vd1234
| ~ rpoint(X0)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1275,f966]) ).
fof(f1281,plain,
! [X0,X1] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1234)
| vd1199 = vd1200
| vd1199 = vd1201
| ~ rline(X1)
| ~ ron(X0,X1)
| ~ ron(vd1200,X1)
| ron(vd1187,X1)
| X1 = vd1234
| ~ rpoint(X0)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1276,f163]) ).
fof(f1282,plain,
! [X0] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1234)
| vd1199 = vd1200
| vd1199 = vd1201
| ~ rline(vd1197)
| ~ ron(X0,vd1197)
| ron(vd1187,vd1197)
| vd1197 = vd1234
| ~ rpoint(X0)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(resolution,[status(thm)],[f1281,f207]) ).
fof(f1284,plain,
! [X0] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1234)
| vd1199 = vd1200
| vd1199 = vd1201
| ~ rline(vd1197)
| ron(vd1187,vd1197)
| ~ rpoint(X0)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(duplicate_literals_removal,[status(thm)],[f1282]) ).
fof(f1285,plain,
! [X0] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1234)
| vd1199 = vd1200
| vd1199 = vd1201
| ~ rline(vd1197)
| ~ rpoint(X0)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1284,f172]) ).
fof(f1287,plain,
! [X0] :
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1234)
| vd1199 = vd1200
| vd1199 = vd1201
| ~ rpoint(X0)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1285,f173]) ).
fof(f1288,plain,
! [X0] :
( ~ rpoint(vd1199)
| vd1199 = vd1200
| vd1199 = vd1201
| ~ rpoint(X0)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(resolution,[status(thm)],[f1287,f1037]) ).
fof(f1289,plain,
! [X0] :
( vd1199 = vd1200
| vd1199 = vd1201
| ~ rpoint(X0)
| ~ ron(X0,vd1197)
| ~ ron(X0,vd1234)
| X0 = vd1200
| X0 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1288,f970]) ).
fof(f1291,plain,
( vd1199 = vd1200
| vd1199 = vd1201
| ~ rpoint(vd1199)
| ~ ron(vd1199,vd1197)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(resolution,[status(thm)],[f1289,f1037]) ).
fof(f1294,plain,
( ~ rpoint(vd1199)
| ~ ron(vd1199,vd1197)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(duplicate_literals_removal,[status(thm)],[f1291]) ).
fof(f1295,plain,
( ~ rpoint(vd1199)
| vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1294,f1053]) ).
fof(f1296,plain,
( vd1199 = vd1200
| vd1199 = vd1201
| ron(vd1187,vd1234)
| vd1197 = vd1234 ),
inference(forward_subsumption_resolution,[status(thm)],[f1295,f970]) ).
fof(f1337,plain,
! [X0,X1] :
( vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| vd1234 = X0
| ~ rpoint(X1)
| ~ rpoint(vd1187)
| X1 = vd1187
| ~ rline(vd1234)
| ~ rline(X0)
| ~ ron(X1,vd1234)
| ~ ron(X1,X0)
| ~ ron(vd1187,X0) ),
inference(resolution,[status(thm)],[f730,f1296]) ).
fof(f1371,plain,
! [X0,X1] :
( vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| vd1234 = X0
| ~ rpoint(X1)
| ~ rpoint(vd1187)
| X1 = vd1187
| ~ rline(X0)
| ~ ron(X1,vd1234)
| ~ ron(X1,X0)
| ~ ron(vd1187,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1337,f163]) ).
fof(f1391,plain,
! [X0,X1] :
( vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| vd1234 = X0
| ~ rpoint(X1)
| X1 = vd1187
| ~ rline(X0)
| ~ ron(X1,vd1234)
| ~ ron(X1,X0)
| ~ ron(vd1187,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1371,f967]) ).
fof(f1393,plain,
! [X0] :
( vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| vd1234 = vd1232
| ~ rpoint(X0)
| X0 = vd1187
| ~ rline(vd1232)
| ~ ron(X0,vd1234)
| ~ ron(X0,vd1232) ),
inference(resolution,[status(thm)],[f1391,f164]) ).
fof(f1394,plain,
! [X0] :
( vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| vd1234 = vd1232
| ~ rpoint(X0)
| X0 = vd1187
| ~ ron(X0,vd1234)
| ~ ron(X0,vd1232) ),
inference(forward_subsumption_resolution,[status(thm)],[f1393,f166]) ).
fof(f1396,plain,
( vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| vd1234 = vd1232
| ~ rpoint(vd1199)
| vd1199 = vd1187
| ~ ron(vd1199,vd1232) ),
inference(resolution,[status(thm)],[f1394,f1037]) ).
fof(f1398,plain,
( vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| vd1234 = vd1232
| ~ rpoint(vd1199)
| vd1199 = vd1187 ),
inference(forward_subsumption_resolution,[status(thm)],[f1396,f1052]) ).
fof(f1399,plain,
( vd1199 = vd1200
| vd1199 = vd1201
| vd1197 = vd1234
| vd1234 = vd1232
| vd1199 = vd1187 ),
inference(forward_subsumption_resolution,[status(thm)],[f1398,f970]) ).
fof(f1409,plain,
( vd1199 = vd1200
| vd1197 = vd1234
| vd1234 = vd1232
| vd1199 = vd1187
| ~ ron(vd1199,vd1232) ),
inference(paramodulation,[status(thm)],[f1399,f155]) ).
fof(f1415,plain,
( vd1199 = vd1200
| vd1197 = vd1234
| vd1234 = vd1232
| vd1199 = vd1187 ),
inference(forward_subsumption_resolution,[status(thm)],[f1409,f1052]) ).
fof(f1436,plain,
( vd1199 = vd1200
| vd1197 = vd1234
| vd1234 = vd1232
| ~ ron(vd1199,vd1197) ),
inference(paramodulation,[status(thm)],[f1415,f172]) ).
fof(f1463,plain,
( vd1199 = vd1200
| vd1197 = vd1234
| vd1234 = vd1232 ),
inference(forward_subsumption_resolution,[status(thm)],[f1436,f1053]) ).
fof(f1482,plain,
( vd1197 = vd1234
| vd1234 = vd1232
| ~ ron(vd1199,vd1232) ),
inference(paramodulation,[status(thm)],[f1463,f1051]) ).
fof(f1494,plain,
( vd1197 = vd1234
| vd1234 = vd1232 ),
inference(forward_subsumption_resolution,[status(thm)],[f1482,f1052]) ).
fof(f1498,plain,
( vd1197 = vd1234
| ron(vd1201,vd1232) ),
inference(paramodulation,[status(thm)],[f1494,f161]) ).
fof(f1504,plain,
vd1197 = vd1234,
inference(forward_subsumption_resolution,[status(thm)],[f1498,f155]) ).
fof(f1513,plain,
rS(vd1200,vd1187,vd1197),
inference(backward_demodulation,[status(thm)],[f1504,f153]) ).
fof(f1530,plain,
( ~ ron(vd1200,vd1197)
| ~ rpoint(vd1200)
| ~ rpoint(vd1187)
| ~ rline(vd1197) ),
inference(resolution,[status(thm)],[f1513,f729]) ).
fof(f1532,plain,
( ~ ron(vd1200,vd1197)
| ~ rpoint(vd1200)
| ~ rpoint(vd1187) ),
inference(forward_subsumption_resolution,[status(thm)],[f1530,f173]) ).
fof(f1534,plain,
( ~ ron(vd1200,vd1197)
| ~ rpoint(vd1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f1532,f967]) ).
fof(f1535,plain,
~ rpoint(vd1200),
inference(resolution,[status(thm)],[f1534,f207]) ).
fof(f1536,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1535,f1036]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO295+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.53 % Computer : n020.cluster.edu
% 0.09/0.53 % Model : x86_64 x86_64
% 0.09/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.53 % Memory : 8046.5625MB
% 0.09/0.53 % OS : Linux 6.8.0-71-generic
% 0.09/0.53 % CPULimit : 300
% 0.09/0.53 % WCLimit : 300
% 0.09/0.53 % DateTime : Sun Sep 20 15:11:32 UTC 2026
% 0.09/0.53 % CPUTime :
% 0.14/0.56 % Drodi V4.1.1
% 0.14/1.06 % Refutation found
% 0.14/1.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/1.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/1.09 % Elapsed time: 0.539858 seconds
% 0.14/1.09 % CPU time: 3.937167 seconds
% 0.14/1.09 % Total memory used: 146.598 MB
% 0.14/1.09 % Net memory used: 142.301 MB
%------------------------------------------------------------------------------