%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO289+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 : n011.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.89s 0.75s
% Output : CNFRefutation 1.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 3
% Syntax : Number of formulae : 78 ( 29 unt; 0 def)
% Number of atoms : 789 ( 412 equ)
% Maximal formula atoms : 27 ( 10 avg)
% Number of connectives : 1202 ( 491 ~; 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,vd1158,vd1157) = vangle(vd1163,vd1165,vd1164),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
vangle(vd1156,vd1158,vd1157) != vangle(vd1163,vd1165,vd1164),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f5,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/sandbox/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,Vd1187,Vd1186) = vangle(Vd1178,Vd1180,Vd1179) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,plain,
vangle(vd1156,vd1158,vd1157) != vangle(vd1163,vd1165,vd1164),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f162,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)],[f5]) ).
fof(f163,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)],[f162]) ).
fof(f164,plain,
! [X0] :
( ~ rline(X0)
| ~ ron(vd1163,X0)
| ~ ron(vd1164,X0)
| ~ ron(vd1165,X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f165,plain,
vangle(vd1157,vd1156,vd1158) = vangle(vd1164,vd1163,vd1165),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f166,plain,
vf(vd1156,vd1158) = vf(vd1163,vd1165),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f167,plain,
vf(vd1156,vd1157) = vf(vd1163,vd1164),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f168,plain,
vd1165 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f169,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f170,plain,
vd1164 = sK1_skl,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f171,plain,
rpoint(sK1_skl),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f172,plain,
vd1163 = sK2_skl,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f173,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f174,plain,
vd1157 != vd1158,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f175,plain,
vd1156 != vd1158,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f176,plain,
vd1156 != vd1157,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f177,plain,
vd1158 = sK3_skl,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f178,plain,
rpoint(sK3_skl),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f179,plain,
vd1157 = sK4_skl,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f180,plain,
rpoint(sK4_skl),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f181,plain,
vd1156 = sK5_skl,
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f182,plain,
rpoint(sK5_skl),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f183,plain,
! [Vd1178,Vd1179,Vd1180,Vd1185,Vd1186,Vd1187] :
( vangle(Vd1185,Vd1187,Vd1186) = vangle(Vd1178,Vd1180,Vd1179)
| ! [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(f184,plain,
! [Vd1178,Vd1179,Vd1180,Vd1185,Vd1186,Vd1187] :
( vangle(Vd1185,Vd1187,Vd1186) = vangle(Vd1178,Vd1180,Vd1179)
| ! [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(sK6_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178))
& ron(Vd1185,sK6_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178))
& ron(Vd1186,sK6_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178))
& ron(Vd1187,sK6_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(Vd1195,sK6_skl(Vd1187,Vd1186,Vd1185,Vd1180,Vd1179,Vd1178))],[f183]) ).
fof(f185,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( vangle(X2,X0,X1) = vangle(X5,X3,X4)
| ~ 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,sK6_skl(X0,X1,X2,X3,X4,X5)) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f186,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( vangle(X2,X1,X0) = vangle(X5,X3,X4)
| ~ 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,sK6_skl(X1,X0,X2,X3,X4,X5)) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f187,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( vangle(X0,X1,X2) = vangle(X5,X3,X4)
| ~ 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,sK6_skl(X1,X2,X0,X3,X4,X5)) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f188,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( vangle(X2,X0,X1) = vangle(X5,X3,X4)
| ~ 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(sK6_skl(X0,X1,X2,X3,X4,X5)) ),
inference(cnf_transformation,[status(thm)],[f184]) ).
fof(f965,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X2,X0,X1) = vangle(X5,X3,X4)
| ~ 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,sK6_skl(X0,X1,X2,X3,X4,X5)) ),
inference(destructive_equality_resolution,[status(thm)],[f185]) ).
fof(f966,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X2,X1,X0) = vangle(X5,X3,X4)
| ~ 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,sK6_skl(X1,X0,X2,X3,X4,X5)) ),
inference(destructive_equality_resolution,[status(thm)],[f186]) ).
fof(f967,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X0,X1,X2) = vangle(X5,X3,X4)
| ~ 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,sK6_skl(X1,X2,X0,X3,X4,X5)) ),
inference(destructive_equality_resolution,[status(thm)],[f187]) ).
fof(f968,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X2,X0,X1) = vangle(X5,X3,X4)
| ~ 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(sK6_skl(X0,X1,X2,X3,X4,X5)) ),
inference(destructive_equality_resolution,[status(thm)],[f188]) ).
fof(f1491,plain,
rpoint(vd1165),
inference(forward_demodulation,[status(thm)],[f168,f169]) ).
fof(f1492,plain,
rpoint(vd1164),
inference(forward_demodulation,[status(thm)],[f170,f171]) ).
fof(f1493,plain,
rpoint(vd1163),
inference(forward_demodulation,[status(thm)],[f172,f173]) ).
fof(f1494,plain,
rpoint(vd1158),
inference(forward_demodulation,[status(thm)],[f177,f178]) ).
fof(f1495,plain,
rpoint(vd1157),
inference(forward_demodulation,[status(thm)],[f179,f180]) ).
fof(f1496,plain,
rpoint(vd1156),
inference(forward_demodulation,[status(thm)],[f181,f182]) ).
fof(f1503,plain,
! [X0,X1,X2,X3,X4] :
( ~ rline(sK6_skl(X4,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK6_skl(X4,vd1164,X3,X2,X0,X1))
| ~ ron(vd1165,sK6_skl(X4,vd1164,X3,X2,X0,X1))
| vangle(X3,X4,vd1164) = vangle(X1,X2,X0)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| ~ rpoint(vd1164)
| ~ rpoint(X4)
| vf(X1,X0) != vf(X3,vd1164)
| vf(X1,X2) != vf(X3,X4)
| vangle(X0,X1,X2) != vangle(vd1164,X3,X4) ),
inference(resolution,[status(thm)],[f966,f164]) ).
fof(f1506,plain,
! [X0,X1,X2,X3,X4] :
( ~ rline(sK6_skl(X4,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK6_skl(X4,vd1164,X3,X2,X0,X1))
| ~ ron(vd1165,sK6_skl(X4,vd1164,X3,X2,X0,X1))
| vangle(X3,X4,vd1164) = vangle(X1,X2,X0)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| ~ rpoint(X4)
| vf(X1,X0) != vf(X3,vd1164)
| vf(X1,X2) != vf(X3,X4)
| vangle(X0,X1,X2) != vangle(vd1164,X3,X4) ),
inference(forward_subsumption_resolution,[status(thm)],[f1503,f1492]) ).
fof(f1507,plain,
! [X0,X1,X2,X3] :
( vangle(X3,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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(sK6_skl(vd1165,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK6_skl(vd1165,vd1164,X3,X2,X0,X1))
| vangle(X3,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| ~ rpoint(vd1165)
| vf(X1,X0) != vf(X3,vd1164)
| vf(X1,X2) != vf(X3,vd1165)
| vangle(X0,X1,X2) != vangle(vd1164,X3,vd1165) ),
inference(resolution,[status(thm)],[f1506,f965]) ).
fof(f1508,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(vd1164)
| ~ rline(sK6_skl(vd1165,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK6_skl(vd1165,vd1164,X3,X2,X0,X1))
| vangle(X3,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| ~ rpoint(X3)
| ~ rpoint(vd1165)
| 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)],[f1507]) ).
fof(f1509,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(vd1164)
| ~ rline(sK6_skl(vd1165,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK6_skl(vd1165,vd1164,X3,X2,X0,X1))
| vangle(X3,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)],[f1508,f1491]) ).
fof(f1575,plain,
! [X0,X1,X2,X3] :
( ~ rline(sK6_skl(vd1165,vd1164,X3,X2,X0,X1))
| ~ ron(vd1163,sK6_skl(vd1165,vd1164,X3,X2,X0,X1))
| vangle(X3,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)],[f1509,f1492]) ).
fof(f1576,plain,
! [X0,X1,X2] :
( vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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) ),
inference(resolution,[status(thm)],[f1575,f967]) ).
fof(f1577,plain,
! [X0,X1,X2] :
( vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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) ),
inference(forward_demodulation,[status(thm)],[f165,f1576]) ).
fof(f1578,plain,
! [X0,X1,X2] :
( vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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) ),
inference(forward_demodulation,[status(thm)],[f166,f1577]) ).
fof(f1579,plain,
! [X0,X1,X2] :
( vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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_demodulation,[status(thm)],[f167,f1578]) ).
fof(f1580,plain,
! [X0,X1,X2] :
( vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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_demodulation,[status(thm)],[f165,f1579]) ).
fof(f1581,plain,
! [X0,X1,X2] :
( vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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_demodulation,[status(thm)],[f166,f1580]) ).
fof(f1582,plain,
! [X0,X1,X2] :
( vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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_demodulation,[status(thm)],[f167,f1581]) ).
fof(f1583,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ 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(duplicate_literals_removal,[status(thm)],[f1582]) ).
fof(f1584,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1164)
| ~ rpoint(vd1165)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| 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)],[f1583,f1493]) ).
fof(f1599,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1164)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,X2,X0,X1))
| vangle(vd1163,vd1165,vd1164) = vangle(X1,X2,X0)
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(X2)
| X1 = X0
| X1 = X2
| X0 = X2
| 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)],[f1584,f1491]) ).
fof(f1601,plain,
( ~ rpoint(vd1164)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,vd1158,vd1157,vd1156))
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158
| vf(vd1156,vd1157) != vf(vd1156,vd1157)
| vf(vd1156,vd1158) != vf(vd1156,vd1158)
| vangle(vd1157,vd1156,vd1158) != vangle(vd1157,vd1156,vd1158) ),
inference(resolution,[status(thm)],[f1599,f159]) ).
fof(f1607,plain,
( ~ rpoint(vd1164)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,vd1158,vd1157,vd1156))
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158
| vd1157 = vd1158 ),
inference(trivial_equality_resolution,[status(thm)],[f1601]) ).
fof(f1608,plain,
( ~ rpoint(vd1164)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,vd1158,vd1157,vd1156))
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157
| vd1156 = vd1158 ),
inference(forward_subsumption_resolution,[status(thm)],[f1607,f174]) ).
fof(f1620,plain,
( ~ rpoint(vd1164)
| ~ rline(sK6_skl(vd1165,vd1164,vd1163,vd1158,vd1157,vd1156))
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157 ),
inference(forward_subsumption_resolution,[status(thm)],[f1608,f175]) ).
fof(f1621,plain,
( vangle(vd1163,vd1165,vd1164) = vangle(vd1156,vd1158,vd1157)
| ~ 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(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157 ),
inference(resolution,[status(thm)],[f1620,f968]) ).
fof(f1622,plain,
( vangle(vd1163,vd1165,vd1164) = vangle(vd1156,vd1158,vd1157)
| ~ 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(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157 ),
inference(forward_demodulation,[status(thm)],[f165,f1621]) ).
fof(f1623,plain,
( vangle(vd1163,vd1165,vd1164) = vangle(vd1156,vd1158,vd1157)
| ~ 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(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157 ),
inference(forward_demodulation,[status(thm)],[f166,f1622]) ).
fof(f1624,plain,
( vangle(vd1163,vd1165,vd1164) = vangle(vd1156,vd1158,vd1157)
| ~ 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(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157 ),
inference(forward_demodulation,[status(thm)],[f167,f1623]) ).
fof(f1625,plain,
( vangle(vd1163,vd1165,vd1164) = vangle(vd1156,vd1158,vd1157)
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1165)
| vf(vd1156,vd1157) != vf(vd1156,vd1157)
| vf(vd1156,vd1158) != vf(vd1156,vd1158)
| vangle(vd1157,vd1156,vd1158) != vangle(vd1157,vd1156,vd1158)
| ~ rpoint(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157 ),
inference(duplicate_literals_removal,[status(thm)],[f1624]) ).
fof(f1626,plain,
( vangle(vd1163,vd1165,vd1164) = vangle(vd1156,vd1158,vd1157)
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1165)
| ~ rpoint(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158)
| vd1156 = vd1157 ),
inference(trivial_equality_resolution,[status(thm)],[f1625]) ).
fof(f1627,plain,
( vangle(vd1163,vd1165,vd1164) = vangle(vd1156,vd1158,vd1157)
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1165)
| ~ rpoint(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157)
| ~ rpoint(vd1158) ),
inference(forward_subsumption_resolution,[status(thm)],[f1626,f176]) ).
fof(f1628,plain,
( vangle(vd1163,vd1165,vd1164) = vangle(vd1156,vd1158,vd1157)
| vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1165)
| ~ rpoint(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157) ),
inference(forward_subsumption_resolution,[status(thm)],[f1627,f1494]) ).
fof(f1629,plain,
( vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1165)
| ~ rpoint(vd1164)
| ~ rpoint(vd1156)
| ~ rpoint(vd1157) ),
inference(resolution,[status(thm)],[f1628,f159]) ).
fof(f1630,plain,
( vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1165)
| ~ rpoint(vd1164)
| ~ rpoint(vd1156) ),
inference(forward_subsumption_resolution,[status(thm)],[f1629,f1495]) ).
fof(f1631,plain,
( vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1165)
| ~ rpoint(vd1164) ),
inference(forward_subsumption_resolution,[status(thm)],[f1630,f1496]) ).
fof(f1632,plain,
( vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163)
| ~ rpoint(vd1165) ),
inference(resolution,[status(thm)],[f1631,f1492]) ).
fof(f1633,plain,
( vd1156 = vd1158
| vd1157 = vd1158
| ~ rpoint(vd1163) ),
inference(forward_subsumption_resolution,[status(thm)],[f1632,f1491]) ).
fof(f1634,plain,
( vd1156 = vd1158
| vd1157 = vd1158 ),
inference(forward_subsumption_resolution,[status(thm)],[f1633,f1493]) ).
fof(f1635,plain,
vd1156 = vd1158,
inference(resolution,[status(thm)],[f1634,f174]) ).
fof(f1642,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1635,f175]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO289+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 15:10:25 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.43 % Drodi V4.1.1
% 1.89/0.75 % Refutation found
% 1.89/0.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.89/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.62/0.77 % Elapsed time: 0.391006 seconds
% 0.62/0.77 % CPU time: 2.470192 seconds
% 0.62/0.77 % Total memory used: 156.707 MB
% 0.62/0.77 % Net memory used: 155.477 MB
%------------------------------------------------------------------------------