%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO341+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 : n019.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:56 PM UTC 2026
% Result : Theorem 25.79s 3.92s
% Output : CNFRefutation 25.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 11
% Syntax : Number of formulae : 117 ( 25 unt; 0 def)
% Number of atoms : 846 ( 229 equ)
% Maximal formula atoms : 17 ( 7 avg)
% Number of connectives : 1345 ( 616 ~; 651 |; 72 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-3 aty)
% Number of variables : 284 ( 265 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
vangle(vd1399,vd1401,vd1409) = vangle(vd1399,vd1409,vd1401),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
vangle(vd1399,vd1401,vd1409) != vangle(vd1399,vd1409,vd1401),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
vd1409 != vd1401,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
vf(vd1399,vd1401) = vf(vd1399,vd1409),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
rS(vd1401,vd1409,vd1406),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
rpoint(vd1409),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
( ? [Vd1403] :
( rpoint(Vd1403)
& vd1399 = Vd1403 )
& ? [Vd1404] :
( rpoint(Vd1404)
& vd1400 = Vd1404 )
& ? [Vd1405] :
( rpoint(Vd1405)
& vd1401 = Vd1405 )
& vd1399 != vd1400
& vd1399 != vd1401
& vd1400 != vd1401
& rline(vd1407)
& ron(vd1399,vd1406)
& ron(vd1400,vd1406)
& vd1406 = vd1407 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [Vd1271,Vd1272,Vd1273] :
( ( ? [Vd1275] :
( rpoint(Vd1275)
& Vd1271 = Vd1275 )
& ? [Vd1276] :
( rpoint(Vd1276)
& Vd1272 = Vd1276 )
& ? [Vd1277] :
( rpoint(Vd1277)
& Vd1273 = Vd1277 )
& Vd1271 != Vd1272
& Vd1271 != Vd1273
& Vd1272 != Vd1273
& vf(Vd1271,Vd1272) = vf(Vd1271,Vd1273) )
=> ! [Vd1279,Vd1280,Vd1282,Vd1283] :
( ( rpoint(Vd1280)
& rR(Vd1272,Vd1271,Vd1279)
& rpoint(Vd1283)
& rR(Vd1273,Vd1271,Vd1282)
& Vd1282 = Vd1283
& Vd1279 = Vd1280 )
=> vangle(Vd1271,Vd1272,Vd1273) = vangle(Vd1271,Vd1273,Vd1272) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [Vd425,Vd426,Vd430,Vd431] :
( ( ? [Vd428] :
( rpoint(Vd428)
& Vd425 = Vd428 )
& ? [Vd429] :
( rpoint(Vd429)
& Vd426 = Vd429 )
& rline(Vd431)
& Vd430 = Vd431
& rS(Vd425,Vd426,Vd430) )
=> rS(Vd426,Vd425,Vd430) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [Vd217,Vd218] :
( ( ? [Vd220] :
( rpoint(Vd220)
& Vd217 = Vd220 )
& ? [Vd221] :
( rpoint(Vd221)
& Vd218 = Vd221 )
& Vd217 != Vd218 )
=> ? [Vd223] :
( rline(Vd223)
& ron(Vd217,Vd223)
& ron(Vd218,Vd223) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [Vd127,Vd128,Vd129,Vd130] :
( ( rline(Vd128)
& Vd127 = Vd128
& ? [Vd132] :
( rpoint(Vd132)
& Vd129 = Vd132 )
& ? [Vd133] :
( rpoint(Vd133)
& Vd130 = Vd133 )
& ron(Vd129,Vd127)
& ron(Vd130,Vd127)
& Vd129 != Vd130 )
=> ? [Vd136] :
( rpoint(Vd136)
& rR(Vd130,Vd129,Vd136) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,plain,
vangle(vd1399,vd1401,vd1409) != vangle(vd1399,vd1409,vd1401),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f126,plain,
vd1409 != vd1401,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f128,plain,
vf(vd1399,vd1401) = vf(vd1399,vd1409),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f129,plain,
rS(vd1401,vd1409,vd1406),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f130,plain,
rpoint(vd1409),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f131,plain,
( rpoint(sK2_skl)
& vd1399 = sK2_skl
& rpoint(sK1_skl)
& vd1400 = sK1_skl
& rpoint(sK0_skl)
& vd1401 = sK0_skl
& vd1399 != vd1400
& vd1399 != vd1401
& vd1400 != vd1401
& rline(vd1407)
& ron(vd1399,vd1406)
& ron(vd1400,vd1406)
& vd1406 = vd1407 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(Vd1405,sK0_skl),skolemize(Vd1404,sK1_skl),skolemize(Vd1403,sK2_skl)],[f8]) ).
fof(f132,plain,
vd1406 = vd1407,
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f134,plain,
ron(vd1399,vd1406),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f135,plain,
rline(vd1407),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f137,plain,
vd1399 != vd1401,
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f139,plain,
vd1401 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f140,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f143,plain,
vd1399 = sK2_skl,
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f144,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f150,plain,
! [Vd1271,Vd1272,Vd1273] :
( ! [Vd1279,Vd1280,Vd1282,Vd1283] :
( vangle(Vd1271,Vd1272,Vd1273) = vangle(Vd1271,Vd1273,Vd1272)
| ~ rpoint(Vd1280)
| ~ rR(Vd1272,Vd1271,Vd1279)
| ~ rpoint(Vd1283)
| ~ rR(Vd1273,Vd1271,Vd1282)
| Vd1282 != Vd1283
| Vd1279 != Vd1280 )
| ! [Vd1275] :
( ~ rpoint(Vd1275)
| Vd1271 != Vd1275 )
| ! [Vd1276] :
( ~ rpoint(Vd1276)
| Vd1272 != Vd1276 )
| ! [Vd1277] :
( ~ rpoint(Vd1277)
| Vd1273 != Vd1277 )
| Vd1271 = Vd1272
| Vd1271 = Vd1273
| Vd1272 = Vd1273
| vf(Vd1271,Vd1272) != vf(Vd1271,Vd1273) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f151,plain,
! [Vd1271,Vd1272,Vd1273] :
( vangle(Vd1271,Vd1272,Vd1273) = vangle(Vd1271,Vd1273,Vd1272)
| ! [Vd1280] :
( ~ rpoint(Vd1280)
| ! [Vd1279] :
( ~ rR(Vd1272,Vd1271,Vd1279)
| ! [Vd1283] :
( ~ rpoint(Vd1283)
| ! [Vd1282] :
( ~ rR(Vd1273,Vd1271,Vd1282)
| Vd1282 != Vd1283
| Vd1279 != Vd1280 ) ) ) )
| ! [Vd1275] :
( ~ rpoint(Vd1275)
| Vd1271 != Vd1275 )
| ! [Vd1276] :
( ~ rpoint(Vd1276)
| Vd1272 != Vd1276 )
| ! [Vd1277] :
( ~ rpoint(Vd1277)
| Vd1273 != Vd1277 )
| Vd1271 = Vd1272
| Vd1271 = Vd1273
| Vd1272 = Vd1273
| vf(Vd1271,Vd1272) != vf(Vd1271,Vd1273) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( vangle(X0,X1,X2) = vangle(X0,X2,X1)
| ~ rpoint(X7)
| ~ rR(X1,X0,X6)
| ~ rpoint(X9)
| ~ rR(X2,X0,X8)
| X8 != X9
| X6 != X7
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rpoint(X3)
| X2 != X3
| X0 = X1
| X0 = X2
| X1 = X2
| vf(X0,X1) != vf(X0,X2) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f212,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)],[f30]) ).
fof(f213,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)],[f212]) ).
fof(f214,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)],[f213]) ).
fof(f215,plain,
! [Vd425,Vd426,Vd430,Vd431] :
( rS(Vd426,Vd425,Vd430)
| ! [Vd428] :
( ~ rpoint(Vd428)
| Vd425 != Vd428 )
| ! [Vd429] :
( ~ rpoint(Vd429)
| Vd426 != Vd429 )
| ~ rline(Vd431)
| Vd430 != Vd431
| ~ rS(Vd425,Vd426,Vd430) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f216,plain,
! [Vd425,Vd426,Vd430] :
( rS(Vd426,Vd425,Vd430)
| ! [Vd428] :
( ~ rpoint(Vd428)
| Vd425 != Vd428 )
| ! [Vd429] :
( ~ rpoint(Vd429)
| Vd426 != Vd429 )
| ! [Vd431] :
( ~ rline(Vd431)
| Vd430 != Vd431
| ~ rS(Vd425,Vd426,Vd430) ) ),
inference(miniscoping,[status(thm)],[f215]) ).
fof(f217,plain,
! [X0,X1,X2,X3,X4,X5] :
( rS(X1,X0,X2)
| ~ rpoint(X5)
| X0 != X5
| ~ rpoint(X4)
| X1 != X4
| ~ rline(X3)
| X2 != X3
| ~ rS(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f216]) ).
fof(f229,plain,
! [Vd217,Vd218] :
( ? [Vd223] :
( rline(Vd223)
& ron(Vd217,Vd223)
& ron(Vd218,Vd223) )
| ! [Vd220] :
( ~ rpoint(Vd220)
| Vd217 != Vd220 )
| ! [Vd221] :
( ~ rpoint(Vd221)
| Vd218 != Vd221 )
| Vd217 = Vd218 ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f230,plain,
! [Vd217,Vd218] :
( ( rline(sK7_skl(Vd218,Vd217))
& ron(Vd217,sK7_skl(Vd218,Vd217))
& ron(Vd218,sK7_skl(Vd218,Vd217)) )
| ! [Vd220] :
( ~ rpoint(Vd220)
| Vd217 != Vd220 )
| ! [Vd221] :
( ~ rpoint(Vd221)
| Vd218 != Vd221 )
| Vd217 = Vd218 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Vd223,sK7_skl(Vd218,Vd217))],[f229]) ).
fof(f231,plain,
! [X0,X1,X2,X3] :
( ron(X1,sK7_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f232,plain,
! [X0,X1,X2,X3] :
( ron(X0,sK7_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f233,plain,
! [X0,X1,X2,X3] :
( rline(sK7_skl(X1,X0))
| ~ rpoint(X3)
| X0 != X3
| ~ rpoint(X2)
| X1 != X2
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f520,plain,
! [Vd127,Vd128,Vd129,Vd130] :
( ? [Vd136] :
( rpoint(Vd136)
& rR(Vd130,Vd129,Vd136) )
| ~ rline(Vd128)
| Vd127 != Vd128
| ! [Vd132] :
( ~ rpoint(Vd132)
| Vd129 != Vd132 )
| ! [Vd133] :
( ~ rpoint(Vd133)
| Vd130 != Vd133 )
| ~ ron(Vd129,Vd127)
| ~ ron(Vd130,Vd127)
| Vd129 = Vd130 ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f521,plain,
! [Vd129,Vd130] :
( ? [Vd136] :
( rpoint(Vd136)
& rR(Vd130,Vd129,Vd136) )
| ! [Vd128] :
( ~ rline(Vd128)
| ! [Vd127] :
( Vd127 != Vd128
| ! [Vd132] :
( ~ rpoint(Vd132)
| Vd129 != Vd132 )
| ! [Vd133] :
( ~ rpoint(Vd133)
| Vd130 != Vd133 )
| ~ ron(Vd129,Vd127)
| ~ ron(Vd130,Vd127)
| Vd129 = Vd130 ) ) ),
inference(miniscoping,[status(thm)],[f520]) ).
fof(f522,plain,
! [Vd129,Vd130] :
( ( rpoint(sK38_skl(Vd130,Vd129))
& rR(Vd130,Vd129,sK38_skl(Vd130,Vd129)) )
| ! [Vd128] :
( ~ rline(Vd128)
| ! [Vd127] :
( Vd127 != Vd128
| ! [Vd132] :
( ~ rpoint(Vd132)
| Vd129 != Vd132 )
| ! [Vd133] :
( ~ rpoint(Vd133)
| Vd130 != Vd133 )
| ~ ron(Vd129,Vd127)
| ~ ron(Vd130,Vd127)
| Vd129 = Vd130 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl]),skolemize(Vd136,sK38_skl(Vd130,Vd129))],[f521]) ).
fof(f523,plain,
! [X0,X1,X2,X3,X4,X5] :
( rR(X1,X0,sK38_skl(X1,X0))
| ~ rline(X5)
| X2 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X1 != X3
| ~ ron(X0,X2)
| ~ ron(X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f522]) ).
fof(f524,plain,
! [X0,X1,X2,X3,X4,X5] :
( rpoint(sK38_skl(X1,X0))
| ~ rline(X5)
| X2 != X5
| ~ rpoint(X4)
| X0 != X4
| ~ rpoint(X3)
| X1 != X3
| ~ ron(X0,X2)
| ~ ron(X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f522]) ).
fof(f675,plain,
! [X0,X1,X2,X3,X4] :
( vangle(X0,X1,X2) = vangle(X0,X2,X1)
| ~ rpoint(X4)
| ~ rR(X1,X0,X4)
| ~ rpoint(X3)
| ~ rR(X2,X0,X3)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rpoint(X2)
| X0 = X1
| X0 = X2
| X1 = X2
| vf(X0,X1) != vf(X0,X2) ),
inference(destructive_equality_resolution,[status(thm)],[f152]) ).
fof(f708,plain,
! [X0,X1,X2] :
( ~ ron(X0,X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(X2)
| ~ rS(X0,X1,X2) ),
inference(destructive_equality_resolution,[status(thm)],[f214]) ).
fof(f709,plain,
! [X0,X1,X2] :
( rS(X1,X0,X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ rline(X2)
| ~ rS(X0,X1,X2) ),
inference(destructive_equality_resolution,[status(thm)],[f217]) ).
fof(f718,plain,
! [X0,X1] :
( ron(X1,sK7_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f231]) ).
fof(f719,plain,
! [X0,X1] :
( ron(X0,sK7_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f232]) ).
fof(f720,plain,
! [X0,X1] :
( rline(sK7_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f233]) ).
fof(f845,plain,
! [X0,X1,X2] :
( rR(X1,X0,sK38_skl(X1,X0))
| ~ rline(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X0,X2)
| ~ ron(X1,X2)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f523]) ).
fof(f846,plain,
! [X0,X1,X2] :
( rpoint(sK38_skl(X1,X0))
| ~ rline(X2)
| ~ rpoint(X0)
| ~ rpoint(X1)
| ~ ron(X0,X2)
| ~ ron(X1,X2)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f524]) ).
fof(f914,plain,
rline(vd1406),
inference(forward_demodulation,[status(thm)],[f132,f135]) ).
fof(f915,plain,
rpoint(vd1401),
inference(forward_demodulation,[status(thm)],[f139,f140]) ).
fof(f917,plain,
rpoint(vd1399),
inference(forward_demodulation,[status(thm)],[f143,f144]) ).
fof(f925,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(X0)
| ~ rR(vd1409,vd1399,X0)
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ rpoint(vd1409)
| vd1399 = vd1401
| vd1399 = vd1409
| vd1401 = vd1409
| vf(vd1399,vd1401) != vf(vd1399,vd1409) ),
inference(resolution,[status(thm)],[f675,f125]) ).
fof(f929,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(X0)
| ~ rR(vd1409,vd1399,X0)
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ rpoint(vd1409)
| vd1399 = vd1401
| vd1399 = vd1409
| vd1401 = vd1409
| vf(vd1399,vd1401) != vf(vd1399,vd1401) ),
inference(forward_demodulation,[status(thm)],[f128,f925]) ).
fof(f930,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(X0)
| ~ rR(vd1409,vd1399,X0)
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ rpoint(vd1409)
| vd1399 = vd1401
| vd1399 = vd1409
| vd1401 = vd1409 ),
inference(trivial_equality_resolution,[status(thm)],[f929]) ).
fof(f931,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(X0)
| ~ rR(vd1409,vd1399,X0)
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ rpoint(vd1409)
| vd1399 = vd1401
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f930,f126]) ).
fof(f949,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(X0)
| ~ rR(vd1409,vd1399,X0)
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ rpoint(vd1409)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f931,f137]) ).
fof(f1256,plain,
( rS(vd1409,vd1401,vd1406)
| ~ rpoint(vd1401)
| ~ rpoint(vd1409)
| ~ rline(vd1406) ),
inference(resolution,[status(thm)],[f709,f129]) ).
fof(f1260,plain,
( rS(vd1409,vd1401,vd1406)
| ~ rpoint(vd1401)
| ~ rpoint(vd1409) ),
inference(forward_subsumption_resolution,[status(thm)],[f1256,f914]) ).
fof(f1262,plain,
( rS(vd1409,vd1401,vd1406)
| ~ rpoint(vd1401) ),
inference(forward_subsumption_resolution,[status(thm)],[f1260,f130]) ).
fof(f1264,plain,
( ~ ron(vd1409,vd1406)
| ~ rpoint(vd1409)
| ~ rpoint(vd1401)
| ~ rline(vd1406)
| ~ rpoint(vd1401) ),
inference(resolution,[status(thm)],[f1262,f708]) ).
fof(f1266,plain,
( ~ ron(vd1409,vd1406)
| ~ rpoint(vd1409)
| ~ rline(vd1406)
| ~ rpoint(vd1401) ),
inference(duplicate_literals_removal,[status(thm)],[f1264]) ).
fof(f1267,plain,
( ~ ron(vd1409,vd1406)
| ~ rpoint(vd1409)
| ~ rline(vd1406) ),
inference(forward_subsumption_resolution,[status(thm)],[f1266,f915]) ).
fof(f1268,plain,
( ~ ron(vd1409,vd1406)
| ~ rpoint(vd1409) ),
inference(forward_subsumption_resolution,[status(thm)],[f1267,f914]) ).
fof(f1906,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(sK38_skl(vd1409,vd1399))
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ rpoint(vd1409)
| vd1399 = vd1409
| ~ rline(X0)
| ~ rpoint(vd1399)
| ~ rpoint(vd1409)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f845,f949]) ).
fof(f1918,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(sK38_skl(vd1409,vd1399))
| ~ rpoint(vd1401)
| ~ rline(X0)
| ~ rpoint(vd1399)
| ~ rpoint(vd1409)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(duplicate_literals_removal,[status(thm)],[f1906]) ).
fof(f1919,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(sK38_skl(vd1409,vd1399))
| ~ rpoint(vd1401)
| ~ rline(X0)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f1918,f130]) ).
fof(f2090,plain,
! [X0,X1] :
( ~ rpoint(X1)
| ~ rR(vd1401,vd1399,X1)
| ~ rpoint(sK38_skl(vd1409,vd1399))
| ~ rpoint(vd1401)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f1919,f917]) ).
fof(f2091,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| vd1399 = vd1401
| ~ rpoint(sK38_skl(vd1401,vd1399))
| ~ rpoint(sK38_skl(vd1409,vd1399))
| ~ rpoint(vd1401)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f2090,f845]) ).
fof(f2092,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| vd1399 = vd1401
| ~ rpoint(sK38_skl(vd1401,vd1399))
| ~ rpoint(sK38_skl(vd1409,vd1399))
| ~ rpoint(vd1401)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(duplicate_literals_removal,[status(thm)],[f2091]) ).
fof(f2093,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| vd1399 = vd1401
| ~ rpoint(sK38_skl(vd1401,vd1399))
| ~ rpoint(sK38_skl(vd1409,vd1399))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2092,f915]) ).
fof(f2094,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rpoint(sK38_skl(vd1401,vd1399))
| ~ rpoint(sK38_skl(vd1409,vd1399))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2093,f137]) ).
fof(f2095,plain,
! [X0,X1,X2] :
( ~ rline(X2)
| ~ rpoint(vd1399)
| ~ rpoint(vd1409)
| ~ ron(vd1399,X2)
| ~ ron(vd1409,X2)
| vd1399 = vd1409
| ~ rline(X1)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rpoint(sK38_skl(vd1401,vd1399))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f2094,f846]) ).
fof(f2096,plain,
! [X0,X1,X2] :
( ~ rline(X2)
| ~ rpoint(vd1409)
| ~ ron(vd1399,X2)
| ~ ron(vd1409,X2)
| ~ rline(X1)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rpoint(sK38_skl(vd1401,vd1399))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(duplicate_literals_removal,[status(thm)],[f2095]) ).
fof(f2097,plain,
! [X0,X1,X2] :
( ~ rline(X2)
| ~ rpoint(vd1409)
| ~ ron(vd1399,X2)
| ~ ron(vd1409,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rpoint(sK38_skl(vd1401,vd1399))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2096,f917]) ).
fof(f2098,plain,
! [X0,X1,X2] :
( ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1409,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rpoint(sK38_skl(vd1401,vd1399))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2097,f130]) ).
fof(f2099,plain,
! [X0,X1,X2,X3] :
( ~ rline(X3)
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ ron(vd1399,X3)
| ~ ron(vd1401,X3)
| vd1399 = vd1401
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1409,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f2098,f846]) ).
fof(f2100,plain,
! [X0,X1,X2,X3] :
( ~ rline(X3)
| ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| ~ ron(vd1399,X3)
| ~ ron(vd1401,X3)
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1409,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2099,f137]) ).
fof(f2101,plain,
! [X0,X1,X2,X3] :
( ~ rline(X3)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X3)
| ~ ron(vd1401,X3)
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1409,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2100,f915]) ).
fof(f2111,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(vd1409)
| ~ rpoint(X2)
| vd1409 = X2
| ~ rline(X3)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X3)
| ~ ron(vd1401,X3)
| ~ rline(sK7_skl(X2,vd1409))
| ~ ron(vd1399,sK7_skl(X2,vd1409))
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f2101,f719]) ).
fof(f2128,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(vd1409)
| ~ rpoint(X2)
| vd1409 = X2
| ~ rline(X3)
| ~ rpoint(vd1399)
| ~ ron(vd1399,X3)
| ~ ron(vd1401,X3)
| ~ ron(vd1399,sK7_skl(X2,vd1409))
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2111,f720]) ).
fof(f2790,plain,
! [X0,X1,X2,X3] :
( ~ rpoint(vd1409)
| ~ rpoint(X2)
| vd1409 = X2
| ~ rline(X3)
| ~ ron(vd1399,X3)
| ~ ron(vd1401,X3)
| ~ ron(vd1399,sK7_skl(X2,vd1409))
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2128,f917]) ).
fof(f2791,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1409)
| ~ rpoint(vd1399)
| vd1409 = vd1399
| ~ rpoint(vd1409)
| ~ rpoint(vd1399)
| vd1409 = vd1399
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1401,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f2790,f718]) ).
fof(f2792,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1409)
| ~ rpoint(vd1399)
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1401,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(duplicate_literals_removal,[status(thm)],[f2791]) ).
fof(f2793,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1409)
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1401,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2792,f917]) ).
fof(f2794,plain,
! [X0,X1,X2] :
( ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1401,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1409,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2793,f130]) ).
fof(f2804,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1409)
| ~ rpoint(X0)
| vd1409 = X0
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1401,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(sK7_skl(X0,vd1409))
| ~ ron(vd1399,sK7_skl(X0,vd1409))
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f2794,f719]) ).
fof(f2818,plain,
! [X0,X1,X2] :
( ~ rpoint(vd1409)
| ~ rpoint(X0)
| vd1409 = X0
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1401,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ ron(vd1399,sK7_skl(X0,vd1409))
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2804,f720]) ).
fof(f5353,plain,
! [X0,X1,X2] :
( ~ rpoint(X0)
| vd1409 = X0
| ~ rline(X2)
| ~ ron(vd1399,X2)
| ~ ron(vd1401,X2)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ ron(vd1399,sK7_skl(X0,vd1409))
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f2818,f130]) ).
fof(f5354,plain,
! [X0,X1] :
( ~ rpoint(vd1409)
| ~ rpoint(vd1399)
| vd1409 = vd1399
| ~ rpoint(vd1399)
| vd1409 = vd1399
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f5353,f718]) ).
fof(f5355,plain,
! [X0,X1] :
( ~ rpoint(vd1409)
| ~ rpoint(vd1399)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(duplicate_literals_removal,[status(thm)],[f5354]) ).
fof(f5356,plain,
! [X0,X1] :
( ~ rpoint(vd1409)
| ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5355,f917]) ).
fof(f5357,plain,
! [X0,X1] :
( ~ rline(X1)
| ~ ron(vd1399,X1)
| ~ ron(vd1401,X1)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5356,f130]) ).
fof(f5365,plain,
! [X0,X1] :
( ~ rpoint(vd1401)
| ~ rpoint(X1)
| vd1401 = X1
| ~ rline(sK7_skl(X1,vd1401))
| ~ ron(vd1399,sK7_skl(X1,vd1401))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f5357,f719]) ).
fof(f5377,plain,
! [X0,X1] :
( ~ rpoint(vd1401)
| ~ rpoint(X1)
| vd1401 = X1
| ~ ron(vd1399,sK7_skl(X1,vd1401))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5365,f720]) ).
fof(f5818,plain,
! [X0,X1] :
( ~ rpoint(X1)
| vd1401 = X1
| ~ ron(vd1399,sK7_skl(X1,vd1401))
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5377,f915]) ).
fof(f5819,plain,
! [X0] :
( ~ rpoint(vd1401)
| ~ rpoint(vd1399)
| vd1401 = vd1399
| ~ rpoint(vd1399)
| vd1401 = vd1399
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f5818,f718]) ).
fof(f5820,plain,
! [X0] :
( ~ rpoint(vd1401)
| ~ rpoint(vd1399)
| vd1401 = vd1399
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(duplicate_literals_removal,[status(thm)],[f5819]) ).
fof(f5821,plain,
! [X0] :
( ~ rpoint(vd1401)
| ~ rpoint(vd1399)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5820,f137]) ).
fof(f5822,plain,
! [X0] :
( ~ rpoint(vd1401)
| ~ rline(X0)
| ~ ron(vd1399,X0)
| ~ ron(vd1401,X0)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5821,f917]) ).
fof(f5830,plain,
! [X0] :
( ~ rpoint(vd1401)
| ~ rpoint(X0)
| vd1401 = X0
| ~ rpoint(vd1401)
| ~ rline(sK7_skl(X0,vd1401))
| ~ ron(vd1399,sK7_skl(X0,vd1401))
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f5822,f719]) ).
fof(f5845,plain,
! [X0] :
( ~ rpoint(X0)
| vd1401 = X0
| ~ rpoint(vd1401)
| ~ rline(sK7_skl(X0,vd1401))
| ~ ron(vd1399,sK7_skl(X0,vd1401))
| vd1399 = vd1409 ),
inference(duplicate_literals_removal,[status(thm)],[f5830]) ).
fof(f5846,plain,
! [X0] :
( ~ rpoint(X0)
| vd1401 = X0
| ~ rpoint(vd1401)
| ~ ron(vd1399,sK7_skl(X0,vd1401))
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5845,f720]) ).
fof(f5849,plain,
! [X0] :
( ~ rpoint(X0)
| vd1401 = X0
| ~ ron(vd1399,sK7_skl(X0,vd1401))
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5846,f915]) ).
fof(f5850,plain,
( ~ rpoint(vd1401)
| ~ rpoint(vd1399)
| vd1401 = vd1399
| ~ rpoint(vd1399)
| vd1401 = vd1399
| vd1399 = vd1409 ),
inference(resolution,[status(thm)],[f5849,f718]) ).
fof(f5851,plain,
( ~ rpoint(vd1401)
| ~ rpoint(vd1399)
| vd1401 = vd1399
| vd1399 = vd1409 ),
inference(duplicate_literals_removal,[status(thm)],[f5850]) ).
fof(f5852,plain,
( ~ rpoint(vd1401)
| ~ rpoint(vd1399)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5851,f137]) ).
fof(f5853,plain,
( ~ rpoint(vd1401)
| vd1399 = vd1409 ),
inference(forward_subsumption_resolution,[status(thm)],[f5852,f917]) ).
fof(f5854,plain,
vd1399 = vd1409,
inference(resolution,[status(thm)],[f5853,f915]) ).
fof(f6016,plain,
( ~ ron(vd1399,vd1406)
| ~ rpoint(vd1409) ),
inference(backward_demodulation,[status(thm)],[f5854,f1268]) ).
fof(f6131,plain,
( ~ ron(vd1399,vd1406)
| ~ rpoint(vd1399) ),
inference(forward_demodulation,[status(thm)],[f5854,f6016]) ).
fof(f6132,plain,
~ ron(vd1399,vd1406),
inference(forward_subsumption_resolution,[status(thm)],[f6131,f917]) ).
fof(f6182,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6132,f134]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO341+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n019.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 20 15:31:06 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.15/0.42 % Drodi V4.1.1
% 25.79/3.92 % Refutation found
% 25.79/3.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 25.79/3.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 25.79/3.95 % Elapsed time: 3.555285 seconds
% 25.79/3.95 % CPU time: 27.755424 seconds
% 25.79/3.95 % Total memory used: 226.288 MB
% 25.79/3.95 % Net memory used: 212.825 MB
%------------------------------------------------------------------------------