%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO288+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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:24:50 PM UTC 2026
% Result : Theorem 1.97s 0.70s
% Output : CNFRefutation 1.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 3
% Syntax : Number of formulae : 78 ( 29 unt; 0 def)
% Number of atoms : 789 ( 411 equ)
% Maximal formula atoms : 27 ( 10 avg)
% Number of connectives : 1203 ( 492 ~; 626 |; 84 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 33 ( 12 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-6 aty)
% Number of variables : 182 ( 161 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1156,vd1157,vd1158) = vangle(vd1163,vd1164,vd1165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
vangle(vd1156,vd1157,vd1158) != vangle(vd1163,vd1164,vd1165),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f4,axiom,
( ? [Vd1160] :
( rpoint(Vd1160)
& vd1156 = Vd1160 )
& ? [Vd1161] :
( rpoint(Vd1161)
& vd1157 = Vd1161 )
& ? [Vd1162] :
( rpoint(Vd1162)
& vd1158 = Vd1162 )
& vd1156 != vd1157
& vd1156 != vd1158
& vd1157 != vd1158
& ? [Vd1167] :
( rpoint(Vd1167)
& vd1163 = Vd1167 )
& ? [Vd1168] :
( rpoint(Vd1168)
& vd1164 = Vd1168 )
& ? [Vd1169] :
( rpoint(Vd1169)
& vd1165 = Vd1169 )
& vf(vd1156,vd1157) = vf(vd1163,vd1164)
& vf(vd1156,vd1158) = vf(vd1163,vd1165)
& vangle(vd1157,vd1156,vd1158) = vangle(vd1164,vd1163,vd1165)
& ~ ? [Vd1173] :
( rline(Vd1173)
& ron(vd1163,Vd1173)
& ron(vd1164,Vd1173)
& ron(vd1165,Vd1173) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [Vd1178,Vd1179,Vd1180,Vd1185,Vd1186,Vd1187] :
( ( ? [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) ) )
=> vangle(Vd1185,Vd1186,Vd1187) = vangle(Vd1178,Vd1179,Vd1180) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,plain,
vangle(vd1156,vd1157,vd1158) != vangle(vd1163,vd1164,vd1165),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f160,plain,
( ? [Vd1160] :
( rpoint(Vd1160)
& vd1156 = Vd1160 )
& ? [Vd1161] :
( rpoint(Vd1161)
& vd1157 = Vd1161 )
& ? [Vd1162] :
( rpoint(Vd1162)
& vd1158 = Vd1162 )
& vd1156 != vd1157
& vd1156 != vd1158
& vd1157 != vd1158
& ? [Vd1167] :
( rpoint(Vd1167)
& vd1163 = Vd1167 )
& ? [Vd1168] :
( rpoint(Vd1168)
& vd1164 = Vd1168 )
& ? [Vd1169] :
( rpoint(Vd1169)
& vd1165 = Vd1169 )
& vf(vd1156,vd1157) = vf(vd1163,vd1164)
& vf(vd1156,vd1158) = vf(vd1163,vd1165)
& vangle(vd1157,vd1156,vd1158) = vangle(vd1164,vd1163,vd1165)
& ! [Vd1173] :
( ~ rline(Vd1173)
| ~ ron(vd1163,Vd1173)
| ~ ron(vd1164,Vd1173)
| ~ ron(vd1165,Vd1173) ) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f161,plain,
( rpoint(sK5_skl)
& vd1156 = sK5_skl
& rpoint(sK4_skl)
& vd1157 = sK4_skl
& rpoint(sK3_skl)
& vd1158 = sK3_skl
& vd1156 != vd1157
& vd1156 != vd1158
& vd1157 != vd1158
& rpoint(sK2_skl)
& vd1163 = sK2_skl
& rpoint(sK1_skl)
& vd1164 = sK1_skl
& rpoint(sK0_skl)
& vd1165 = sK0_skl
& vf(vd1156,vd1157) = vf(vd1163,vd1164)
& vf(vd1156,vd1158) = vf(vd1163,vd1165)
& vangle(vd1157,vd1156,vd1158) = vangle(vd1164,vd1163,vd1165)
& ! [Vd1173] :
( ~ rline(Vd1173)
| ~ ron(vd1163,Vd1173)
| ~ ron(vd1164,Vd1173)
| ~ ron(vd1165,Vd1173) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(Vd1169,sK0_skl),skolemize(Vd1168,sK1_skl),skolemize(Vd1167,sK2_skl),skolemize(Vd1162,sK3_skl),skolemize(Vd1161,sK4_skl),skolemize(Vd1160,sK5_skl)],[f160]) ).
fof(f162,plain,
! [X0] :
( ~ rline(X0)
| ~ ron(vd1163,X0)
| ~ ron(vd1164,X0)
| ~ ron(vd1165,X0) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f163,plain,
vangle(vd1157,vd1156,vd1158) = vangle(vd1164,vd1163,vd1165),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f164,plain,
vf(vd1156,vd1158) = vf(vd1163,vd1165),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f165,plain,
vf(vd1156,vd1157) = vf(vd1163,vd1164),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f166,plain,
vd1165 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f167,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f168,plain,
vd1164 = sK1_skl,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f169,plain,
rpoint(sK1_skl),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f170,plain,
vd1163 = sK2_skl,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f171,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f172,plain,
vd1157 != vd1158,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f173,plain,
vd1156 != vd1158,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f174,plain,
vd1156 != vd1157,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f175,plain,
vd1158 = sK3_skl,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f176,plain,
rpoint(sK3_skl),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f177,plain,
vd1157 = sK4_skl,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f178,plain,
rpoint(sK4_skl),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f179,plain,
vd1156 = sK5_skl,
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f180,plain,
rpoint(sK5_skl),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f187,plain,
! [Vd1178,Vd1179,Vd1180,Vd1185,Vd1186,Vd1187] :
( vangle(Vd1185,Vd1186,Vd1187) = vangle(Vd1178,Vd1179,Vd1180)
| ! [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)],[f6]) ).
fof(f188,plain,
! [Vd1178,Vd1179,Vd1180,Vd1185,Vd1186,Vd1187] :
( vangle(Vd1185,Vd1186,Vd1187) = vangle(Vd1178,Vd1179,Vd1180)
| ! [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)
| ( rline(sK7_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178))
& ron(Vd1185,sK7_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178))
& ron(Vd1186,sK7_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178))
& ron(Vd1187,sK7_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Vd1195,sK7_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178))],[f187]) ).
fof(f189,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( vangle(X2,X1,X0) = vangle(X5,X4,X3)
| ~ rpoint(X11)
| X5 != X11
| ~ rpoint(X10)
| X4 != X10
| ~ rpoint(X9)
| X3 != X9
| X5 = X4
| X5 = X3
| X4 = X3
| ~ rpoint(X8)
| X2 != X8
| ~ rpoint(X7)
| X1 != X7
| ~ rpoint(X6)
| X0 != X6
| vf(X5,X4) != vf(X2,X1)
| vf(X5,X3) != vf(X2,X0)
| vangle(X4,X5,X3) != vangle(X1,X2,X0)
| ron(X0,sK7_skl(X0,X1,X2,X3,X4,X5)) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f190,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( vangle(X2,X0,X1) = vangle(X5,X4,X3)
| ~ rpoint(X11)
| X5 != X11
| ~ rpoint(X10)
| X4 != X10
| ~ rpoint(X9)
| X3 != X9
| X5 = X4
| X5 = X3
| X4 = X3
| ~ rpoint(X8)
| X2 != X8
| ~ rpoint(X7)
| X0 != X7
| ~ rpoint(X6)
| X1 != X6
| vf(X5,X4) != vf(X2,X0)
| vf(X5,X3) != vf(X2,X1)
| vangle(X4,X5,X3) != vangle(X0,X2,X1)
| ron(X0,sK7_skl(X1,X0,X2,X3,X4,X5)) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f191,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( vangle(X0,X2,X1) = vangle(X5,X4,X3)
| ~ rpoint(X11)
| X5 != X11
| ~ rpoint(X10)
| X4 != X10
| ~ rpoint(X9)
| X3 != X9
| X5 = X4
| X5 = X3
| X4 = X3
| ~ rpoint(X8)
| X0 != X8
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X1 != X6
| vf(X5,X4) != vf(X0,X2)
| vf(X5,X3) != vf(X0,X1)
| vangle(X4,X5,X3) != vangle(X2,X0,X1)
| ron(X0,sK7_skl(X1,X2,X0,X3,X4,X5)) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f192,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( vangle(X2,X1,X0) = vangle(X5,X4,X3)
| ~ rpoint(X11)
| X5 != X11
| ~ rpoint(X10)
| X4 != X10
| ~ rpoint(X9)
| X3 != X9
| X5 = X4
| X5 = X3
| X4 = X3
| ~ rpoint(X8)
| X2 != X8
| ~ rpoint(X7)
| X1 != X7
| ~ rpoint(X6)
| X0 != X6
| vf(X5,X4) != vf(X2,X1)
| vf(X5,X3) != vf(X2,X0)
| vangle(X4,X5,X3) != vangle(X1,X2,X0)
| rline(sK7_skl(X0,X1,X2,X3,X4,X5)) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f967,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X2,X1,X0) = vangle(X5,X4,X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| X5 = X4
| X5 = X3
| X4 = X3
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| vf(X5,X4) != vf(X2,X1)
| vf(X5,X3) != vf(X2,X0)
| vangle(X4,X5,X3) != vangle(X1,X2,X0)
| ron(X0,sK7_skl(X0,X1,X2,X3,X4,X5)) ),
inference(destructive_equality_resolution,[status(thm)],[f189]) ).
fof(f968,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X2,X0,X1) = vangle(X5,X4,X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| X5 = X4
| X5 = X3
| X4 = X3
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| vf(X5,X4) != vf(X2,X0)
| vf(X5,X3) != vf(X2,X1)
| vangle(X4,X5,X3) != vangle(X0,X2,X1)
| ron(X0,sK7_skl(X1,X0,X2,X3,X4,X5)) ),
inference(destructive_equality_resolution,[status(thm)],[f190]) ).
fof(f969,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X0,X2,X1) = vangle(X5,X4,X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| X5 = X4
| X5 = X3
| X4 = X3
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X1)
| vf(X5,X4) != vf(X0,X2)
| vf(X5,X3) != vf(X0,X1)
| vangle(X4,X5,X3) != vangle(X2,X0,X1)
| ron(X0,sK7_skl(X1,X2,X0,X3,X4,X5)) ),
inference(destructive_equality_resolution,[status(thm)],[f191]) ).
fof(f970,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X2,X1,X0) = vangle(X5,X4,X3)
| ~ rpoint(X5)
| ~ rpoint(X4)
| ~ rpoint(X3)
| X5 = X4
| X5 = X3
| X4 = X3
| ~ rpoint(X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| vf(X5,X4) != vf(X2,X1)
| vf(X5,X3) != vf(X2,X0)
| vangle(X4,X5,X3) != vangle(X1,X2,X0)
| rline(sK7_skl(X0,X1,X2,X3,X4,X5)) ),
inference(destructive_equality_resolution,[status(thm)],[f192]) ).
fof(f1486,plain,
rpoint(vd1165),
inference(forward_demodulation,[status(thm)],[f166,f167]) ).
fof(f1487,plain,
rpoint(vd1164),
inference(forward_demodulation,[status(thm)],[f168,f169]) ).
fof(f1488,plain,
rpoint(vd1163),
inference(forward_demodulation,[status(thm)],[f170,f171]) ).
fof(f1489,plain,
rpoint(vd1158),
inference(forward_demodulation,[status(thm)],[f175,f176]) ).
fof(f1490,plain,
rpoint(vd1157),
inference(forward_demodulation,[status(thm)],[f177,f178]) ).
fof(f1491,plain,
rpoint(vd1156),
inference(forward_demodulation,[status(thm)],[f179,f180]) ).
fof(f1539,plain,
! [X0,X1,X2,X3,X4] :
( ~ rline(sK7_skl(vd1165,X3,X4,X2,X0,X1))
| ~ ron(vd1163,sK7_skl(vd1165,X3,X4,X2,X0,X1))
| ~ ron(vd1164,sK7_skl(vd1165,X3,X4,X2,X0,X1))
| vangle(X4,X3,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X4)
| ~ rpoint(X3)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(X4,X3)
| vf(X1,X2) != vf(X4,vd1165)
| vangle(X0,X1,X2) != vangle(X3,X4,vd1165) ),
inference(resolution,[status(thm)],[f967,f162]) ).
fof(f1540,plain,
! [X0,X1,X2,X3,X4] :
( ~ rline(sK7_skl(vd1165,X3,X4,X2,X0,X1))
| ~ ron(vd1163,sK7_skl(vd1165,X3,X4,X2,X0,X1))
| ~ ron(vd1164,sK7_skl(vd1165,X3,X4,X2,X0,X1))
| vangle(X4,X3,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X4)
| ~ rpoint(X3)
| vf(X1,X0) != vf(X4,X3)
| vf(X1,X2) != vf(X4,vd1165)
| vangle(X0,X1,X2) != vangle(X3,X4,vd1165) ),
inference(forward_subsumption_resolution,[status(thm)],[f1539,f1486]) ).
fof(f1562,plain,
! [X0,X1,X2,X3] :
( vangle(X3,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(X3,vd1164)
| vf(X1,X2) != vf(X3,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,X3,vd1165)
| ~ rline(sK7_skl(vd1165,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK7_skl(vd1165,vd1164,X3,X2,X0,X1))
| vangle(X3,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| ~ rpoint(vd1164)
| vf(X1,X0) != vf(X3,vd1164)
| vf(X1,X2) != vf(X3,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,X3,vd1165) ),
inference(resolution,[status(thm)],[f1540,f968]) ).
fof(f1563,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(vd1165)
| ~ rline(sK7_skl(vd1165,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK7_skl(vd1165,vd1164,X3,X2,X0,X1))
| vangle(X3,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| ~ rpoint(vd1164)
| vf(X1,X0) != vf(X3,vd1164)
| vf(X1,X2) != vf(X3,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,X3,vd1165) ),
inference(duplicate_literals_removal,[status(thm)],[f1562]) ).
fof(f1564,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(vd1165)
| ~ rline(sK7_skl(vd1165,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK7_skl(vd1165,vd1164,X3,X2,X0,X1))
| vangle(X3,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| vf(X1,X0) != vf(X3,vd1164)
| vf(X1,X2) != vf(X3,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,X3,vd1165) ),
inference(forward_subsumption_resolution,[status(thm)],[f1563,f1487]) ).
fof(f1586,plain,
! [X0,X1,X2,X3] :
( ~ rline(sK7_skl(vd1165,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK7_skl(vd1165,vd1164,X3,X2,X0,X1))
| vangle(X3,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| vf(X1,X0) != vf(X3,vd1164)
| vf(X1,X2) != vf(X3,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,X3,vd1165) ),
inference(forward_subsumption_resolution,[status(thm)],[f1564,f1486]) ).
fof(f1602,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1163,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,vd1163,vd1165)
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1163,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,vd1163,vd1165) ),
inference(resolution,[status(thm)],[f969,f1586]) ).
fof(f1606,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1163,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,vd1163,vd1165)
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1163,vd1165)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(forward_demodulation,[status(thm)],[f163,f1602]) ).
fof(f1607,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1163,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,vd1163,vd1165)
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(forward_demodulation,[status(thm)],[f164,f1606]) ).
fof(f1608,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1163,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,vd1163,vd1165)
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(vd1156,vd1157)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(forward_demodulation,[status(thm)],[f165,f1607]) ).
fof(f1609,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1163,vd1165)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158)
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(vd1156,vd1157)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(forward_demodulation,[status(thm)],[f163,f1608]) ).
fof(f1610,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| vf(X1,X0) != vf(vd1163,vd1164)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158)
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(vd1156,vd1157)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(forward_demodulation,[status(thm)],[f164,f1609]) ).
fof(f1611,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| vf(X1,X0) != vf(vd1156,vd1157)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158)
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(vd1156,vd1157)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(forward_demodulation,[status(thm)],[f165,f1610]) ).
fof(f1612,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(vd1156,vd1157)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(duplicate_literals_removal,[status(thm)],[f1611]) ).
fof(f1613,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| vf(X1,X0) != vf(vd1156,vd1157)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(forward_subsumption_resolution,[status(thm)],[f1612,f1486]) ).
fof(f1677,plain,
! [X0,X1,X2] :
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1164,vd1165) = vangle(X1,X0,X2)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(vd1163)
| vf(X1,X0) != vf(vd1156,vd1157)
| vf(X1,X2) != vf(vd1156,vd1158)
| vangle(X0,X1,X2) != vangle(vd1157,vd1156,vd1158) ),
inference(forward_subsumption_resolution,[status(thm)],[f1613,f1487]) ).
fof(f1680,plain,
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,vd1158,vd1157,vd1156))
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| vf(vd1156,vd1157) != vf(vd1156,vd1157)
| vf(vd1156,vd1158) != vf(vd1156,vd1158)
| vangle(vd1157,vd1156,vd1158) != vangle(vd1157,vd1156,vd1158) ),
inference(resolution,[status(thm)],[f1677,f158]) ).
fof(f1686,plain,
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,vd1158,vd1157,vd1156))
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163) ),
inference(trivial_equality_resolution,[status(thm)],[f1680]) ).
fof(f1687,plain,
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,vd1158,vd1157,vd1156))
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158 ),
inference(forward_subsumption_resolution,[status(thm)],[f1686,f1488]) ).
fof(f1693,plain,
( ~ rline(sK7_skl(vd1165,vd1164,vd1163,vd1158,vd1157,vd1156))
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158 ),
inference(forward_subsumption_resolution,[status(thm)],[f1687,f172]) ).
fof(f1694,plain,
( vangle(vd1163,vd1164,vd1165) = vangle(vd1156,vd1157,vd1158)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(vd1156,vd1157) != vf(vd1163,vd1164)
| vf(vd1156,vd1158) != vf(vd1163,vd1165)
| vangle(vd1157,vd1156,vd1158) != vangle(vd1164,vd1163,vd1165)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158 ),
inference(resolution,[status(thm)],[f1693,f970]) ).
fof(f1695,plain,
( vangle(vd1163,vd1164,vd1165) = vangle(vd1156,vd1157,vd1158)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(vd1156,vd1157) != vf(vd1163,vd1164)
| vf(vd1156,vd1158) != vf(vd1163,vd1165)
| vangle(vd1157,vd1156,vd1158) != vangle(vd1157,vd1156,vd1158)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158 ),
inference(forward_demodulation,[status(thm)],[f163,f1694]) ).
fof(f1696,plain,
( vangle(vd1163,vd1164,vd1165) = vangle(vd1156,vd1157,vd1158)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(vd1156,vd1157) != vf(vd1163,vd1164)
| vf(vd1156,vd1158) != vf(vd1156,vd1158)
| vangle(vd1157,vd1156,vd1158) != vangle(vd1157,vd1156,vd1158)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158 ),
inference(forward_demodulation,[status(thm)],[f164,f1695]) ).
fof(f1697,plain,
( vangle(vd1163,vd1164,vd1165) = vangle(vd1156,vd1157,vd1158)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(vd1156,vd1157) != vf(vd1156,vd1157)
| vf(vd1156,vd1158) != vf(vd1156,vd1158)
| vangle(vd1157,vd1156,vd1158) != vangle(vd1157,vd1156,vd1158)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158 ),
inference(forward_demodulation,[status(thm)],[f165,f1696]) ).
fof(f1698,plain,
( vangle(vd1163,vd1164,vd1165) = vangle(vd1156,vd1157,vd1158)
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| vf(vd1156,vd1157) != vf(vd1156,vd1157)
| vf(vd1156,vd1158) != vf(vd1156,vd1158)
| vangle(vd1157,vd1156,vd1158) != vangle(vd1157,vd1156,vd1158)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158 ),
inference(duplicate_literals_removal,[status(thm)],[f1697]) ).
fof(f1699,plain,
( vangle(vd1163,vd1164,vd1165) = vangle(vd1156,vd1157,vd1158)
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158 ),
inference(trivial_equality_resolution,[status(thm)],[f1698]) ).
fof(f1700,plain,
( vangle(vd1163,vd1164,vd1165) = vangle(vd1156,vd1157,vd1158)
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157 ),
inference(forward_subsumption_resolution,[status(thm)],[f1699,f173]) ).
fof(f1719,plain,
( vangle(vd1163,vd1164,vd1165) = vangle(vd1156,vd1157,vd1158)
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158) ),
inference(forward_subsumption_resolution,[status(thm)],[f1700,f174]) ).
fof(f1720,plain,
( vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158) ),
inference(resolution,[status(thm)],[f1719,f158]) ).
fof(f1721,plain,
( vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157) ),
inference(forward_subsumption_resolution,[status(thm)],[f1720,f1489]) ).
fof(f1722,plain,
( vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| ~ rpoint(vd1156) ),
inference(forward_subsumption_resolution,[status(thm)],[f1721,f1490]) ).
fof(f1723,plain,
( vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164)
| ~ rpoint(vd1156) ),
inference(resolution,[status(thm)],[f1722,f1486]) ).
fof(f1726,plain,
( vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1164) ),
inference(forward_subsumption_resolution,[status(thm)],[f1723,f1491]) ).
fof(f1729,plain,
( vd1157 = vd1158
| ~ rpoint(vd1163) ),
inference(forward_subsumption_resolution,[status(thm)],[f1726,f1487]) ).
fof(f1730,plain,
vd1157 = vd1158,
inference(resolution,[status(thm)],[f1729,f1488]) ).
fof(f1731,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1730,f172]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO288+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n014.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 15:08:35 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.42 % Drodi V4.1.1
% 1.97/0.70 % Refutation found
% 1.97/0.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.97/0.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.97/0.73 % Elapsed time: 0.369390 seconds
% 1.97/0.73 % CPU time: 2.234751 seconds
% 1.97/0.73 % Total memory used: 156.435 MB
% 1.97/0.73 % Net memory used: 155.218 MB
%------------------------------------------------------------------------------