%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO340+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 : 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:56 PM UTC 2026
% Result : Theorem 0.10s 0.45s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 3
% Syntax : Number of formulae : 45 ( 24 unt; 0 def)
% Number of atoms : 229 ( 101 equ)
% Maximal formula atoms : 20 ( 5 avg)
% Number of connectives : 315 ( 131 ~; 129 |; 52 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-7 aty)
% Number of variables : 52 ( 44 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [Vd1394] :
( rpoint(Vd1394)
& rS(vd1386,Vd1394,vd1391)
& vf(vd1384,vd1386) = vf(vd1384,Vd1394)
& vf(vd1385,vd1386) = vf(vd1385,Vd1394)
& Vd1394 != vd1386 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ? [Vd1394] :
( rpoint(Vd1394)
& rS(vd1386,Vd1394,vd1391)
& vf(vd1384,vd1386) = vf(vd1384,Vd1394)
& vf(vd1385,vd1386) = vf(vd1385,Vd1394)
& Vd1394 != vd1386 ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
( ? [Vd1388] :
( rpoint(Vd1388)
& vd1384 = Vd1388 )
& ? [Vd1389] :
( rpoint(Vd1389)
& vd1385 = Vd1389 )
& ? [Vd1390] :
( rpoint(Vd1390)
& vd1386 = Vd1390 )
& vd1384 != vd1385
& vd1384 != vd1386
& vd1385 != vd1386
& rline(vd1392)
& ron(vd1384,vd1391)
& ron(vd1385,vd1391)
& vd1391 = vd1392 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [Vd1399,Vd1400,Vd1401,Vd1406,Vd1407] :
( ( ? [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 )
=> ! [Vd1409] :
( ( rpoint(Vd1409)
& rS(Vd1401,Vd1409,Vd1406)
& vf(Vd1399,Vd1401) = vf(Vd1399,Vd1409)
& vf(Vd1400,Vd1401) = vf(Vd1400,Vd1409)
& Vd1409 != Vd1401 )
=> ! [Vd1415] :
( Vd1415 = vskolem1416(Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407)
=> ! [Vd1418] : Vd1418 != vskolem1419(Vd1415,Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,plain,
( rpoint(sK0_skl)
& rS(vd1386,sK0_skl,vd1391)
& vf(vd1384,vd1386) = vf(vd1384,sK0_skl)
& vf(vd1385,vd1386) = vf(vd1385,sK0_skl)
& sK0_skl != vd1386 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Vd1394,sK0_skl)],[f2]) ).
fof(f127,plain,
sK0_skl != vd1386,
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f128,plain,
vf(vd1385,vd1386) = vf(vd1385,sK0_skl),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f129,plain,
vf(vd1384,vd1386) = vf(vd1384,sK0_skl),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f130,plain,
rS(vd1386,sK0_skl,vd1391),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f131,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f132,plain,
( rpoint(sK3_skl)
& vd1384 = sK3_skl
& rpoint(sK2_skl)
& vd1385 = sK2_skl
& rpoint(sK1_skl)
& vd1386 = sK1_skl
& vd1384 != vd1385
& vd1384 != vd1386
& vd1385 != vd1386
& rline(vd1392)
& ron(vd1384,vd1391)
& ron(vd1385,vd1391)
& vd1391 = vd1392 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(Vd1390,sK1_skl),skolemize(Vd1389,sK2_skl),skolemize(Vd1388,sK3_skl)],[f3]) ).
fof(f133,plain,
vd1391 = vd1392,
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
ron(vd1385,vd1391),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f135,plain,
ron(vd1384,vd1391),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f136,plain,
rline(vd1392),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f137,plain,
vd1385 != vd1386,
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f138,plain,
vd1384 != vd1386,
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f139,plain,
vd1384 != vd1385,
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f140,plain,
vd1386 = sK1_skl,
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f141,plain,
rpoint(sK1_skl),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f142,plain,
vd1385 = sK2_skl,
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f143,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f144,plain,
vd1384 = sK3_skl,
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f145,plain,
rpoint(sK3_skl),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f146,plain,
! [Vd1399,Vd1400,Vd1401,Vd1406,Vd1407] :
( ! [Vd1409] :
( ! [Vd1415] :
( ! [Vd1418] : Vd1418 != vskolem1419(Vd1415,Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407)
| Vd1415 != vskolem1416(Vd1409,Vd1399,Vd1400,Vd1401,Vd1406,Vd1407) )
| ~ rpoint(Vd1409)
| ~ rS(Vd1401,Vd1409,Vd1406)
| vf(Vd1399,Vd1401) != vf(Vd1399,Vd1409)
| vf(Vd1400,Vd1401) != vf(Vd1400,Vd1409)
| Vd1409 = Vd1401 )
| ! [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 ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f147,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10] :
( X10 != vskolem1419(X9,X8,X3,X2,X4,X0,X1)
| X9 != vskolem1416(X8,X3,X2,X4,X0,X1)
| ~ rpoint(X8)
| ~ rS(X4,X8,X0)
| vf(X3,X4) != vf(X3,X8)
| vf(X2,X4) != vf(X2,X8)
| X8 = X4
| ~ rpoint(X7)
| X3 != X7
| ~ rpoint(X6)
| X2 != X6
| ~ rpoint(X5)
| X4 != X5
| X3 = X2
| X3 = X4
| X2 = X4
| ~ rline(X1)
| ~ ron(X3,X0)
| ~ ron(X2,X0)
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f691,plain,
! [X0,X1,X2,X3,X4] :
( ~ rpoint(X4)
| ~ rS(X3,X4,X1)
| vf(X2,X3) != vf(X2,X4)
| vf(X0,X3) != vf(X0,X4)
| X4 = X3
| ~ rpoint(X2)
| ~ rpoint(X0)
| ~ rpoint(X3)
| X2 = X0
| X2 = X3
| X0 = X3
| ~ rline(X1)
| ~ ron(X2,X1)
| ~ ron(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f147]) ).
fof(f943,plain,
rline(vd1391),
inference(forward_demodulation,[status(thm)],[f133,f136]) ).
fof(f944,plain,
rpoint(vd1386),
inference(forward_demodulation,[status(thm)],[f140,f141]) ).
fof(f945,plain,
rpoint(vd1385),
inference(forward_demodulation,[status(thm)],[f142,f143]) ).
fof(f946,plain,
rpoint(vd1384),
inference(forward_demodulation,[status(thm)],[f144,f145]) ).
fof(f947,plain,
! [X0,X1] :
( ~ rpoint(sK0_skl)
| ~ rS(vd1386,sK0_skl,X1)
| vf(X0,vd1386) != vf(X0,sK0_skl)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(X0)
| ~ rpoint(vd1386)
| vd1384 = X0
| vd1384 = vd1386
| X0 = vd1386
| ~ rline(X1)
| ~ ron(vd1384,X1)
| ~ ron(X0,X1) ),
inference(resolution,[status(thm)],[f691,f129]) ).
fof(f958,plain,
! [X0,X1] :
( ~ rpoint(sK0_skl)
| ~ rS(vd1386,sK0_skl,X1)
| vf(X0,vd1386) != vf(X0,sK0_skl)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(X0)
| ~ rpoint(vd1386)
| vd1384 = X0
| X0 = vd1386
| ~ rline(X1)
| ~ ron(vd1384,X1)
| ~ ron(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f947,f138]) ).
fof(f966,plain,
! [X0,X1] :
( ~ rpoint(sK0_skl)
| ~ rS(vd1386,sK0_skl,X1)
| vf(X0,vd1386) != vf(X0,sK0_skl)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(X0)
| vd1384 = X0
| X0 = vd1386
| ~ rline(X1)
| ~ ron(vd1384,X1)
| ~ ron(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f958,f944]) ).
fof(f968,plain,
! [X0] :
( ~ rpoint(sK0_skl)
| ~ rS(vd1386,sK0_skl,X0)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(vd1385)
| vd1384 = vd1385
| vd1385 = vd1386
| ~ rline(X0)
| ~ ron(vd1384,X0)
| ~ ron(vd1385,X0) ),
inference(resolution,[status(thm)],[f966,f128]) ).
fof(f971,plain,
! [X0] :
( ~ rpoint(sK0_skl)
| ~ rS(vd1386,sK0_skl,X0)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(vd1385)
| vd1384 = vd1385
| ~ rline(X0)
| ~ ron(vd1384,X0)
| ~ ron(vd1385,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f968,f137]) ).
fof(f974,plain,
! [X0] :
( ~ rpoint(sK0_skl)
| ~ rS(vd1386,sK0_skl,X0)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(vd1385)
| ~ rline(X0)
| ~ ron(vd1384,X0)
| ~ ron(vd1385,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f971,f139]) ).
fof(f975,plain,
( ~ rpoint(sK0_skl)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(vd1385)
| ~ rline(vd1391)
| ~ ron(vd1384,vd1391)
| ~ ron(vd1385,vd1391) ),
inference(resolution,[status(thm)],[f974,f130]) ).
fof(f976,plain,
( ~ rpoint(sK0_skl)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(vd1385)
| ~ rline(vd1391)
| ~ ron(vd1384,vd1391) ),
inference(forward_subsumption_resolution,[status(thm)],[f975,f134]) ).
fof(f977,plain,
( ~ rpoint(sK0_skl)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(vd1385)
| ~ rline(vd1391) ),
inference(forward_subsumption_resolution,[status(thm)],[f976,f135]) ).
fof(f978,plain,
( ~ rpoint(sK0_skl)
| sK0_skl = vd1386
| ~ rpoint(vd1384)
| ~ rpoint(vd1385) ),
inference(resolution,[status(thm)],[f977,f943]) ).
fof(f979,plain,
( ~ rpoint(sK0_skl)
| sK0_skl = vd1386
| ~ rpoint(vd1384) ),
inference(forward_subsumption_resolution,[status(thm)],[f978,f945]) ).
fof(f986,plain,
( ~ rpoint(sK0_skl)
| sK0_skl = vd1386 ),
inference(forward_subsumption_resolution,[status(thm)],[f979,f946]) ).
fof(f987,plain,
sK0_skl = vd1386,
inference(resolution,[status(thm)],[f986,f131]) ).
fof(f988,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f987,f127]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO340+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 15:29:24 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 0.10/0.45 % Refutation found
% 0.10/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.48 % Elapsed time: 0.107378 seconds
% 0.10/0.48 % CPU time: 0.441188 seconds
% 0.10/0.48 % Total memory used: 124.679 MB
% 0.10/0.48 % Net memory used: 124.103 MB
%------------------------------------------------------------------------------