%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO294+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 : n004.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 168.08s 22.51s
% Output : CNFRefutation 27.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 41
% Syntax : Number of formulae : 174 ( 69 unt; 23 def)
% Number of atoms : 523 ( 171 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 579 ( 230 ~; 223 |; 97 &)
% ( 25 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 24 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 21 con; 0-3 aty)
% Number of variables : 151 ( 127 !; 24 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
ron(vd1201,vd1232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ron(vd1201,vd1232),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vangle(vd1201,vd1185,vd1187) = v0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
vd1199 = vd1185,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [Vd862,Vd863,Vd864,Vd865,Vd866,Vd867,Vd868,Vd869] :
( ( rpoint(Vd863)
& Vd862 = Vd863
& rpoint(Vd865)
& Vd864 = Vd865
& rpoint(Vd867)
& Vd866 = Vd867
& rline(Vd869)
& Vd868 = Vd869
& Vd862 != Vd864
& Vd862 != Vd866
& ron(Vd862,Vd868)
& ron(Vd864,Vd868) )
=> ( ( ron(Vd866,Vd868)
& ~ rR(Vd862,Vd864,Vd866) )
<=> vangle(Vd864,Vd862,Vd866) = v0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
( ? [Vd1182] :
( rpoint(Vd1182)
& vd1178 = Vd1182 )
& ? [Vd1183] :
( rpoint(Vd1183)
& vd1179 = Vd1183 )
& ? [Vd1184] :
( rpoint(Vd1184)
& vd1180 = Vd1184 )
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& ? [Vd1189] :
( rpoint(Vd1189)
& vd1185 = Vd1189 )
& ? [Vd1190] :
( rpoint(Vd1190)
& vd1186 = Vd1190 )
& ? [Vd1191] :
( rpoint(Vd1191)
& vd1187 = Vd1191 )
& vf(vd1178,vd1179) = vf(vd1185,vd1186)
& vf(vd1178,vd1180) = vf(vd1185,vd1187)
& vangle(vd1179,vd1178,vd1180) = vangle(vd1186,vd1185,vd1187)
& ~ ? [Vd1195] :
( rline(Vd1195)
& ron(vd1185,Vd1195)
& ron(vd1186,Vd1195)
& ron(vd1187,Vd1195) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
ron(vd1199,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
? [Vd1205] :
( rpoint(Vd1205)
& vd1201 = Vd1205 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
rline(vd1234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
ron(vd1187,vd1232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
ron(vd1185,vd1232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
rline(vd1232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
rline(vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
~ ron(vd1187,vd1197),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
v0 = vd684,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f121,axiom,
! [Vd52,Vd53] :
( ( rline(Vd53)
& Vd52 = Vd53 )
=> ? [Vd54] :
( rpoint(Vd54)
& ron(Vd54,Vd52) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,axiom,
! [Vd19,Vd20] :
( ( ? [Vd22] :
( rpoint(Vd22)
& Vd19 = Vd22 )
& ? [Vd23] :
( rpoint(Vd23)
& Vd20 = Vd23 ) )
=> ? [Vd24] :
( rpoint(Vd24)
& Vd24 != Vd19
& Vd24 != Vd20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,axiom,
rpoint(vd14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f155,axiom,
! [Vd767,Vd768,Vd769] :
( ( ? [Vd771] :
( rpoint(Vd771)
& Vd767 = Vd771 )
& ? [Vd772] :
( rpoint(Vd772)
& Vd768 = Vd772 )
& ? [Vd773] :
( rpoint(Vd773)
& Vd769 = Vd773 )
& Vd767 != Vd768
& Vd767 != Vd769 )
=> vangle(Vd767,Vd768,Vd769) = vangle(Vd769,Vd768,Vd767) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,plain,
~ ron(vd1201,vd1232),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f157,plain,
vangle(vd1201,vd1185,vd1187) = v0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f161,plain,
vd1199 = vd1185,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f163,plain,
! [Vd862,Vd863,Vd864,Vd865,Vd866,Vd867,Vd868,Vd869] :
( ( ( ron(Vd866,Vd868)
& ~ rR(Vd862,Vd864,Vd866) )
<=> vangle(Vd864,Vd862,Vd866) = v0 )
| ~ rpoint(Vd863)
| Vd862 != Vd863
| ~ rpoint(Vd865)
| Vd864 != Vd865
| ~ rpoint(Vd867)
| Vd866 != Vd867
| ~ rline(Vd869)
| Vd868 != Vd869
| Vd862 = Vd864
| Vd862 = Vd866
| ~ ron(Vd862,Vd868)
| ~ ron(Vd864,Vd868) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f164,plain,
! [Vd862,Vd863,Vd864,Vd865,Vd866,Vd867,Vd868,Vd869] :
( ( ( vangle(Vd864,Vd862,Vd866) != v0
| ( ron(Vd866,Vd868)
& ~ rR(Vd862,Vd864,Vd866) ) )
& ( vangle(Vd864,Vd862,Vd866) = v0
| ~ ron(Vd866,Vd868)
| rR(Vd862,Vd864,Vd866) ) )
| ~ rpoint(Vd863)
| Vd862 != Vd863
| ~ rpoint(Vd865)
| Vd864 != Vd865
| ~ rpoint(Vd867)
| Vd866 != Vd867
| ~ rline(Vd869)
| Vd868 != Vd869
| Vd862 = Vd864
| Vd862 = Vd866
| ~ ron(Vd862,Vd868)
| ~ ron(Vd864,Vd868) ),
inference(NNF_transformation,[status(thm)],[f163]) ).
fof(f165,plain,
! [Vd862,Vd864,Vd866,Vd868] :
( ( ( vangle(Vd864,Vd862,Vd866) != v0
| ( ron(Vd866,Vd868)
& ~ rR(Vd862,Vd864,Vd866) ) )
& ( vangle(Vd864,Vd862,Vd866) = v0
| ~ ron(Vd866,Vd868)
| rR(Vd862,Vd864,Vd866) ) )
| ! [Vd863] :
( ~ rpoint(Vd863)
| Vd862 != Vd863
| ! [Vd865] :
( ~ rpoint(Vd865)
| Vd864 != Vd865
| ! [Vd867] :
( ~ rpoint(Vd867)
| Vd866 != Vd867
| ! [Vd869] :
( ~ rline(Vd869)
| Vd868 != Vd869
| Vd862 = Vd864
| Vd862 = Vd866
| ~ ron(Vd862,Vd868)
| ~ ron(Vd864,Vd868) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f164]) ).
fof(f168,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( vangle(X0,X2,X3) != v0
| ron(X3,X1)
| ~ rpoint(X7)
| X2 != X7
| ~ rpoint(X6)
| X0 != X6
| ~ rpoint(X5)
| X3 != X5
| ~ rline(X4)
| X1 != X4
| X2 = X0
| X2 = X3
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f179,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)],[f16]) ).
fof(f180,plain,
( rpoint(sK5_skl)
& vd1178 = sK5_skl
& rpoint(sK4_skl)
& vd1179 = sK4_skl
& rpoint(sK3_skl)
& vd1180 = sK3_skl
& vd1178 != vd1179
& vd1178 != vd1180
& vd1179 != vd1180
& rpoint(sK2_skl)
& vd1185 = sK2_skl
& rpoint(sK1_skl)
& vd1186 = sK1_skl
& rpoint(sK0_skl)
& vd1187 = sK0_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,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(Vd1191,sK0_skl),skolemize(Vd1190,sK1_skl),skolemize(Vd1189,sK2_skl),skolemize(Vd1184,sK3_skl),skolemize(Vd1183,sK4_skl),skolemize(Vd1182,sK5_skl)],[f179]) ).
fof(f185,plain,
vd1187 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f186,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f189,plain,
vd1185 = sK2_skl,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f190,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f192,plain,
vd1178 != vd1180,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f194,plain,
vd1180 = sK3_skl,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f195,plain,
rpoint(sK3_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f196,plain,
vd1179 = sK4_skl,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f197,plain,
rpoint(sK4_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f198,plain,
vd1178 = sK5_skl,
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f199,plain,
rpoint(sK5_skl),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f206,plain,
ron(vd1199,vd1197),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f212,plain,
( rpoint(sK6_skl)
& vd1201 = sK6_skl ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(Vd1205,sK6_skl)],[f27]) ).
fof(f213,plain,
vd1201 = sK6_skl,
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f214,plain,
rpoint(sK6_skl),
inference(cnf_transformation,[status(thm)],[f212]) ).
fof(f230,plain,
rline(vd1234),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f231,plain,
ron(vd1187,vd1232),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f232,plain,
ron(vd1185,vd1232),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f233,plain,
rline(vd1232),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f239,plain,
rline(vd1197),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f252,plain,
~ ron(vd1187,vd1197),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f281,plain,
v0 = vd684,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f568,plain,
! [Vd52,Vd53] :
( ? [Vd54] :
( rpoint(Vd54)
& ron(Vd54,Vd52) )
| ~ rline(Vd53)
| Vd52 != Vd53 ),
inference(pre_NNF_transformation,[status(thm)],[f121]) ).
fof(f569,plain,
! [Vd52] :
( ? [Vd54] :
( rpoint(Vd54)
& ron(Vd54,Vd52) )
| ! [Vd53] :
( ~ rline(Vd53)
| Vd52 != Vd53 ) ),
inference(miniscoping,[status(thm)],[f568]) ).
fof(f570,plain,
! [Vd52] :
( ( rpoint(sK42_skl(Vd52))
& ron(sK42_skl(Vd52),Vd52) )
| ! [Vd53] :
( ~ rline(Vd53)
| Vd52 != Vd53 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42_skl]),skolemize(Vd54,sK42_skl(Vd52))],[f569]) ).
fof(f572,plain,
! [X0,X1] :
( rpoint(sK42_skl(X0))
| ~ rline(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f570]) ).
fof(f586,plain,
! [Vd19,Vd20] :
( ? [Vd24] :
( rpoint(Vd24)
& Vd24 != Vd19
& Vd24 != Vd20 )
| ! [Vd22] :
( ~ rpoint(Vd22)
| Vd19 != Vd22 )
| ! [Vd23] :
( ~ rpoint(Vd23)
| Vd20 != Vd23 ) ),
inference(pre_NNF_transformation,[status(thm)],[f124]) ).
fof(f587,plain,
! [Vd19,Vd20] :
( ( rpoint(sK45_skl(Vd20,Vd19))
& sK45_skl(Vd20,Vd19) != Vd19
& sK45_skl(Vd20,Vd19) != Vd20 )
| ! [Vd22] :
( ~ rpoint(Vd22)
| Vd19 != Vd22 )
| ! [Vd23] :
( ~ rpoint(Vd23)
| Vd20 != Vd23 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45_skl]),skolemize(Vd24,sK45_skl(Vd20,Vd19))],[f586]) ).
fof(f590,plain,
! [X0,X1,X2,X3] :
( rpoint(sK45_skl(X0,X2))
| ~ rpoint(X3)
| X2 != X3
| ~ rpoint(X1)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f587]) ).
fof(f596,plain,
rpoint(vd14),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f696,plain,
! [Vd767,Vd768,Vd769] :
( vangle(Vd767,Vd768,Vd769) = vangle(Vd769,Vd768,Vd767)
| ! [Vd771] :
( ~ rpoint(Vd771)
| Vd767 != Vd771 )
| ! [Vd772] :
( ~ rpoint(Vd772)
| Vd768 != Vd772 )
| ! [Vd773] :
( ~ rpoint(Vd773)
| Vd769 != Vd773 )
| Vd767 = Vd768
| Vd767 = Vd769 ),
inference(pre_NNF_transformation,[status(thm)],[f155]) ).
fof(f697,plain,
! [X0,X1,X2,X3,X4,X5] :
( vangle(X0,X2,X1) = vangle(X1,X2,X0)
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X2 != X4
| ~ rpoint(X3)
| X1 != X3
| X0 = X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f696]) ).
fof(f775,plain,
! [X0,X1,X2,X3] :
( vangle(X0,X2,X3) != v0
| ron(X3,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rline(X1)
| X2 = X0
| X2 = X3
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f168]) ).
fof(f929,plain,
! [X0] :
( rpoint(sK42_skl(X0))
| ~ rline(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f572]) ).
fof(f941,plain,
! [X0,X1] :
( rpoint(sK45_skl(X0,X1))
| ~ rpoint(X1)
| ~ rpoint(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f590]) ).
fof(f988,plain,
! [X0,X1,X2] :
( vangle(X0,X2,X1) = vangle(X1,X2,X0)
| ~ rpoint(X0)
| ~ rpoint(X2)
| ~ rpoint(X1)
| X0 = X2
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f697]) ).
fof(f998,plain,
ron(vd1199,vd1232),
inference(backward_demodulation,[status(thm)],[f161,f232]) ).
fof(f999,plain,
vangle(vd1201,vd1199,vd1187) = v0,
inference(forward_demodulation,[status(thm)],[f161,f157]) ).
fof(f1002,plain,
rpoint(vd1187),
inference(forward_demodulation,[status(thm)],[f185,f186]) ).
fof(f1004,plain,
vd1199 = sK2_skl,
inference(forward_demodulation,[status(thm)],[f161,f189]) ).
fof(f1005,plain,
rpoint(vd1199),
inference(forward_demodulation,[status(thm)],[f1004,f190]) ).
fof(f1006,plain,
rpoint(vd1180),
inference(forward_demodulation,[status(thm)],[f194,f195]) ).
fof(f1007,plain,
rpoint(vd1179),
inference(forward_demodulation,[status(thm)],[f196,f197]) ).
fof(f1014,plain,
rpoint(vd1178),
inference(forward_demodulation,[status(thm)],[f198,f199]) ).
fof(f1015,plain,
rpoint(vd1201),
inference(forward_demodulation,[status(thm)],[f213,f214]) ).
fof(f1026,plain,
vangle(vd1201,vd1199,vd1187) = vd684,
inference(backward_demodulation,[status(thm)],[f281,f999]) ).
fof(f1027,plain,
! [X0,X1,X2,X3] :
( vangle(X0,X2,X3) != vd684
| ron(X3,X1)
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| ~ rline(X1)
| X2 = X0
| X2 = X3
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f281,f775]) ).
fof(f1028,plain,
! [X0,X1] :
( vangle(X0,X1,vd1201) != vd684
| ~ rpoint(X1)
| ~ rpoint(X0)
| ~ rpoint(vd1201)
| ~ rline(vd1232)
| X1 = X0
| X1 = vd1201
| ~ ron(X1,vd1232)
| ~ ron(X0,vd1232) ),
inference(resolution,[status(thm)],[f1027,f156]) ).
fof(f1029,definition,
! [X0,X1] :
( sQ11_spl
<=> ( vangle(X0,X1,vd1201) != vd684
| ~ rpoint(X1)
| ~ rpoint(X0)
| X1 = X0
| X1 = vd1201
| ~ ron(X1,vd1232)
| ~ ron(X0,vd1232) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f1030,plain,
! [X0,X1] :
( ~ sQ11_spl
| vangle(X0,X1,vd1201) != vd684
| ~ rpoint(X1)
| ~ rpoint(X0)
| X1 = X0
| X1 = vd1201
| ~ ron(X1,vd1232)
| ~ ron(X0,vd1232) ),
inference(component_clause,[status(thm)],[f1029]) ).
fof(f1032,definition,
( sQ12_spl
<=> rline(vd1232) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f1034,plain,
( sQ12_spl
| ~ rline(vd1232) ),
inference(component_clause,[status(thm)],[f1032]) ).
fof(f1035,definition,
( sQ13_spl
<=> rpoint(vd1201) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( sQ13_spl
| ~ rpoint(vd1201) ),
inference(component_clause,[status(thm)],[f1035]) ).
fof(f1038,plain,
( ~ sQ13_spl
| ~ sQ12_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f1028,f1029,f1032,f1035]) ).
fof(f1039,plain,
( sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1037,f1015]) ).
fof(f1040,plain,
sQ13_spl,
inference(contradiction_clause,[status(thm)],[f1039]) ).
fof(f1049,definition,
( sQ15_spl
<=> rline(vd1197) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f1051,plain,
( sQ15_spl
| ~ rline(vd1197) ),
inference(component_clause,[status(thm)],[f1049]) ).
fof(f1052,definition,
( sQ16_spl
<=> rpoint(vd1187) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f1054,plain,
( sQ16_spl
| ~ rpoint(vd1187) ),
inference(component_clause,[status(thm)],[f1052]) ).
fof(f1056,plain,
( sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1054,f1002]) ).
fof(f1057,plain,
sQ16_spl,
inference(contradiction_clause,[status(thm)],[f1056]) ).
fof(f1068,definition,
( sQ18_spl
<=> ron(vd1199,vd1232) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f1070,plain,
( sQ18_spl
| ~ ron(vd1199,vd1232) ),
inference(component_clause,[status(thm)],[f1068]) ).
fof(f1076,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1034,f233]) ).
fof(f1077,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1076]) ).
fof(f1080,definition,
( sQ20_spl
<=> vd1199 = vd1201 ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1081,plain,
( ~ sQ20_spl
| vd1199 = vd1201 ),
inference(component_clause,[status(thm)],[f1080]) ).
fof(f1089,definition,
( sQ23_spl
<=> rpoint(vd1199) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f1091,plain,
( sQ23_spl
| ~ rpoint(vd1199) ),
inference(component_clause,[status(thm)],[f1089]) ).
fof(f1101,plain,
( sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1070,f998]) ).
fof(f1102,plain,
sQ18_spl,
inference(contradiction_clause,[status(thm)],[f1101]) ).
fof(f1156,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1091,f1005]) ).
fof(f1157,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1156]) ).
fof(f1176,plain,
( ~ sQ20_spl
| ~ ron(vd1199,vd1232) ),
inference(backward_demodulation,[status(thm)],[f1081,f156]) ).
fof(f1179,plain,
( ~ sQ20_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1176,f1068,f1080]) ).
fof(f1296,definition,
( sQ44_spl
<=> vd1199 = vd1187 ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1297,plain,
( ~ sQ44_spl
| vd1199 = vd1187 ),
inference(component_clause,[status(thm)],[f1296]) ).
fof(f1494,plain,
! [X0] :
( ~ sQ11_spl
| vangle(X0,vd1199,vd1201) != vd684
| ~ rpoint(vd1199)
| ~ rpoint(X0)
| vd1199 = X0
| vd1199 = vd1201
| ~ ron(X0,vd1232) ),
inference(resolution,[status(thm)],[f1030,f998]) ).
fof(f1498,definition,
! [X0] :
( sQ59_spl
<=> ( vangle(X0,vd1199,vd1201) != vd684
| ~ rpoint(X0)
| vd1199 = X0
| ~ ron(X0,vd1232) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f1499,plain,
! [X0] :
( ~ sQ59_spl
| vangle(X0,vd1199,vd1201) != vd684
| ~ rpoint(X0)
| vd1199 = X0
| ~ ron(X0,vd1232) ),
inference(component_clause,[status(thm)],[f1498]) ).
fof(f1501,plain,
( ~ sQ11_spl
| ~ sQ23_spl
| sQ20_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f1494,f1498,f1080,f1089,f1029]) ).
fof(f1512,definition,
( sQ63_spl
<=> vd1187 = vd1201 ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1513,plain,
( ~ sQ63_spl
| vd1187 = vd1201 ),
inference(component_clause,[status(thm)],[f1512]) ).
fof(f1750,plain,
( ~ sQ44_spl
| ~ ron(vd1199,vd1197) ),
inference(backward_demodulation,[status(thm)],[f1297,f252]) ).
fof(f1766,plain,
( ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1750,f206]) ).
fof(f1767,plain,
~ sQ44_spl,
inference(contradiction_clause,[status(thm)],[f1766]) ).
fof(f1901,definition,
( sQ101_spl
<=> vangle(vd1187,vd1199,vd1201) = vd684 ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f1926,plain,
( ~ sQ63_spl
| ~ ron(vd1187,vd1232) ),
inference(backward_demodulation,[status(thm)],[f1513,f156]) ).
fof(f1978,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1926,f231]) ).
fof(f1979,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f1978]) ).
fof(f2032,plain,
( ~ sQ59_spl
| vangle(vd1187,vd1199,vd1201) != vd684
| ~ rpoint(vd1187)
| vd1199 = vd1187 ),
inference(resolution,[status(thm)],[f1499,f231]) ).
fof(f2036,plain,
( ~ sQ59_spl
| ~ sQ101_spl
| ~ sQ16_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f2032,f1296,f1052,f1901,f1498]) ).
fof(f2319,definition,
( sQ145_spl
<=> rpoint(vd14) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f2321,plain,
( sQ145_spl
| ~ rpoint(vd14) ),
inference(component_clause,[status(thm)],[f2319]) ).
fof(f2363,plain,
( sQ145_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2321,f596]) ).
fof(f2364,plain,
sQ145_spl,
inference(contradiction_clause,[status(thm)],[f2363]) ).
fof(f2565,definition,
( sQ168_spl
<=> rpoint(vd1178) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f2567,plain,
( sQ168_spl
| ~ rpoint(vd1178) ),
inference(component_clause,[status(thm)],[f2565]) ).
fof(f2612,plain,
( sQ168_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2567,f1014]) ).
fof(f2613,plain,
sQ168_spl,
inference(contradiction_clause,[status(thm)],[f2612]) ).
fof(f2709,definition,
( sQ189_spl
<=> rpoint(vd1179) ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f2711,plain,
( sQ189_spl
| ~ rpoint(vd1179) ),
inference(component_clause,[status(thm)],[f2709]) ).
fof(f2753,plain,
( sQ189_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2711,f1007]) ).
fof(f2754,plain,
sQ189_spl,
inference(contradiction_clause,[status(thm)],[f2753]) ).
fof(f2797,definition,
( sQ201_spl
<=> rpoint(vd1180) ),
introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition]) ).
fof(f2799,plain,
( sQ201_spl
| ~ rpoint(vd1180) ),
inference(component_clause,[status(thm)],[f2797]) ).
fof(f2841,plain,
( sQ201_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2799,f1006]) ).
fof(f2842,plain,
sQ201_spl,
inference(contradiction_clause,[status(thm)],[f2841]) ).
fof(f4210,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1051,f239]) ).
fof(f4211,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f4210]) ).
fof(f5702,definition,
( sQ511_spl
<=> vd1180 = vd1178 ),
introduced(definition,[new_symbols(definition,[sQ511_spl])],[split_symbol_definition]) ).
fof(f5703,plain,
( ~ sQ511_spl
| vd1180 = vd1178 ),
inference(component_clause,[status(thm)],[f5702]) ).
fof(f6216,definition,
( sQ578_spl
<=> ron(vd1187,vd1197) ),
introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition]) ).
fof(f6217,plain,
( ~ sQ578_spl
| ron(vd1187,vd1197) ),
inference(component_clause,[status(thm)],[f6216]) ).
fof(f6221,plain,
( ~ sQ578_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6217,f252]) ).
fof(f6222,plain,
~ sQ578_spl,
inference(contradiction_clause,[status(thm)],[f6221]) ).
fof(f6372,plain,
( ~ sQ511_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5703,f192]) ).
fof(f6373,plain,
~ sQ511_spl,
inference(contradiction_clause,[status(thm)],[f6372]) ).
fof(f7650,definition,
( sQ705_spl
<=> rpoint(sK42_skl(vd1234)) ),
introduced(definition,[new_symbols(definition,[sQ705_spl])],[split_symbol_definition]) ).
fof(f7652,plain,
( sQ705_spl
| ~ rpoint(sK42_skl(vd1234)) ),
inference(component_clause,[status(thm)],[f7650]) ).
fof(f7675,plain,
( sQ705_spl
| ~ rline(vd1234) ),
inference(resolution,[status(thm)],[f7652,f929]) ).
fof(f7676,plain,
( sQ705_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7675,f230]) ).
fof(f7677,plain,
sQ705_spl,
inference(contradiction_clause,[status(thm)],[f7676]) ).
fof(f8099,definition,
( sQ734_spl
<=> rline(vd1234) ),
introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition]) ).
fof(f8101,plain,
( sQ734_spl
| ~ rline(vd1234) ),
inference(component_clause,[status(thm)],[f8099]) ).
fof(f8687,plain,
! [X0] :
( rpoint(sK45_skl(X0,vd1180))
| ~ rpoint(X0) ),
inference(resolution,[status(thm)],[f941,f1006]) ).
fof(f15880,plain,
rpoint(sK45_skl(vd14,vd1180)),
inference(resolution,[status(thm)],[f8687,f596]) ).
fof(f17213,definition,
! [X15,X16,X17,X18] :
( sQ1105_spl
<=> vf(X15,X16) != vf(X17,X18) ),
introduced(definition,[new_symbols(definition,[sQ1105_spl])],[split_symbol_definition]) ).
fof(f17214,plain,
! [X0,X1,X2,X3] :
( ~ sQ1105_spl
| vf(X0,X1) != vf(X2,X3) ),
inference(component_clause,[status(thm)],[f17213]) ).
fof(f17284,definition,
! [X13,X14,X15,X16,X17,X18] :
( sQ1120_spl
<=> vangle(X13,X14,X15) != vangle(X16,X17,X18) ),
introduced(definition,[new_symbols(definition,[sQ1120_spl])],[split_symbol_definition]) ).
fof(f17285,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ1120_spl
| vangle(X0,X1,X2) != vangle(X3,X4,X5) ),
inference(component_clause,[status(thm)],[f17284]) ).
fof(f17503,plain,
( ~ sQ1105_spl
| $false ),
inference(equality_resolution,[status(thm)],[f17214]) ).
fof(f17504,definition,
! [X0] :
( sQ1136_spl
<=> ~ rpoint(X0) ),
introduced(definition,[new_symbols(definition,[sQ1136_spl])],[split_symbol_definition]) ).
fof(f17505,plain,
! [X0] :
( ~ sQ1136_spl
| ~ rpoint(X0) ),
inference(component_clause,[status(thm)],[f17504]) ).
fof(f17508,plain,
~ sQ1105_spl,
inference(contradiction_clause,[status(thm)],[f17503]) ).
fof(f17520,plain,
( ~ sQ1136_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f15880,f17505]) ).
fof(f17571,plain,
~ sQ1136_spl,
inference(contradiction_clause,[status(thm)],[f17520]) ).
fof(f19189,plain,
( ~ sQ1120_spl
| $false ),
inference(equality_resolution,[status(thm)],[f17285]) ).
fof(f19190,plain,
~ sQ1120_spl,
inference(contradiction_clause,[status(thm)],[f19189]) ).
fof(f21210,plain,
( sQ734_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8101,f230]) ).
fof(f21211,plain,
sQ734_spl,
inference(contradiction_clause,[status(thm)],[f21210]) ).
fof(f23819,plain,
( vangle(vd1187,vd1199,vd1201) = vd684
| ~ rpoint(vd1187)
| ~ rpoint(vd1199)
| ~ rpoint(vd1201)
| vd1187 = vd1199
| vd1187 = vd1201 ),
inference(paramodulation,[status(thm)],[f1026,f988]) ).
fof(f23821,plain,
( sQ101_spl
| ~ sQ16_spl
| ~ sQ23_spl
| ~ sQ13_spl
| sQ44_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f23819,f1512,f1296,f1035,f1089,f1052,f1901]) ).
fof(f23822,plain,
$false,
inference(sat_refutation,[status(thm)],[f1038,f1040,f1057,f1077,f1102,f1157,f1179,f1501,f1767,f1979,f2036,f2364,f2613,f2754,f2842,f4211,f6222,f6373,f7677,f17508,f17571,f19190,f21211,f23821]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO294+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n004.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Sun Sep 20 15:09:21 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.50 % Drodi V4.1.1
% 168.08/22.51 % Refutation found
% 168.08/22.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 168.08/22.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 27.65/22.56 % Elapsed time: 22.087728 seconds
% 27.65/22.56 % CPU time: 168.775022 seconds
% 27.65/22.56 % Total memory used: 300.118 MB
% 27.65/22.56 % Net memory used: 278.232 MB
%------------------------------------------------------------------------------