%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO342+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 : n026.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 1.55s 0.88s
% Output : CNFRefutation 1.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 3
% Syntax : Number of formulae : 33 ( 9 unt; 0 def)
% Number of atoms : 134 ( 46 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 168 ( 67 ~; 62 |; 38 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 41 ( 32 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
? [Vd1416] :
( rline(Vd1416)
& ron(vd1401,Vd1416)
& ron(vd1399,Vd1416) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ? [Vd1416] :
( rline(Vd1416)
& ron(vd1401,Vd1416)
& ron(vd1399,Vd1416) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f9,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(f36,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(f126,plain,
! [Vd1416] :
( ~ rline(Vd1416)
| ~ ron(vd1401,Vd1416)
| ~ ron(vd1399,Vd1416) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f127,plain,
! [X0] :
( ~ rline(X0)
| ~ ron(vd1401,X0)
| ~ ron(vd1399,X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f134,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)],[f9]) ).
fof(f140,plain,
vd1399 != vd1401,
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f142,plain,
vd1401 = sK0_skl,
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f143,plain,
rpoint(sK0_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f146,plain,
vd1399 = sK2_skl,
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f147,plain,
rpoint(sK2_skl),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f232,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)],[f36]) ).
fof(f233,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))],[f232]) ).
fof(f234,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)],[f233]) ).
fof(f235,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)],[f233]) ).
fof(f236,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)],[f233]) ).
fof(f721,plain,
! [X0,X1] :
( ron(X1,sK7_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f234]) ).
fof(f722,plain,
! [X0,X1] :
( ron(X0,sK7_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f235]) ).
fof(f723,plain,
! [X0,X1] :
( rline(sK7_skl(X1,X0))
| ~ rpoint(X0)
| ~ rpoint(X1)
| X0 = X1 ),
inference(destructive_equality_resolution,[status(thm)],[f236]) ).
fof(f916,plain,
rpoint(vd1401),
inference(forward_demodulation,[status(thm)],[f142,f143]) ).
fof(f918,plain,
rpoint(vd1399),
inference(forward_demodulation,[status(thm)],[f146,f147]) ).
fof(f1084,plain,
! [X0] :
( ~ rline(sK7_skl(vd1401,X0))
| ~ ron(vd1399,sK7_skl(vd1401,X0))
| ~ rpoint(X0)
| ~ rpoint(vd1401)
| X0 = vd1401 ),
inference(resolution,[status(thm)],[f721,f127]) ).
fof(f1102,plain,
! [X0] :
( ~ rline(sK7_skl(vd1401,X0))
| ~ ron(vd1399,sK7_skl(vd1401,X0))
| ~ rpoint(X0)
| X0 = vd1401 ),
inference(forward_subsumption_resolution,[status(thm)],[f1084,f916]) ).
fof(f1226,plain,
( ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| vd1399 = vd1401
| ~ rline(sK7_skl(vd1401,vd1399))
| ~ rpoint(vd1399)
| vd1399 = vd1401 ),
inference(resolution,[status(thm)],[f1102,f722]) ).
fof(f1227,plain,
( ~ rpoint(vd1401)
| ~ rline(sK7_skl(vd1401,vd1399))
| ~ rpoint(vd1399)
| vd1399 = vd1401 ),
inference(duplicate_literals_removal,[status(thm)],[f1226]) ).
fof(f1228,plain,
( ~ rpoint(vd1401)
| ~ rline(sK7_skl(vd1401,vd1399))
| ~ rpoint(vd1399) ),
inference(forward_subsumption_resolution,[status(thm)],[f1227,f140]) ).
fof(f1229,plain,
( ~ rpoint(vd1401)
| ~ rline(sK7_skl(vd1401,vd1399)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1228,f918]) ).
fof(f1230,plain,
( ~ rpoint(vd1399)
| ~ rpoint(vd1401)
| vd1399 = vd1401
| ~ rpoint(vd1401) ),
inference(resolution,[status(thm)],[f1229,f723]) ).
fof(f1231,plain,
( ~ rpoint(vd1399)
| vd1399 = vd1401
| ~ rpoint(vd1401) ),
inference(duplicate_literals_removal,[status(thm)],[f1230]) ).
fof(f1232,plain,
( ~ rpoint(vd1399)
| vd1399 = vd1401 ),
inference(forward_subsumption_resolution,[status(thm)],[f1231,f916]) ).
fof(f1234,plain,
~ rpoint(vd1399),
inference(forward_subsumption_resolution,[status(thm)],[f1232,f140]) ).
fof(f1235,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f918,f1234]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO342+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n026.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:33:06 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 1.55/0.88 % Refutation found
% 1.55/0.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.55/0.88 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.55/0.89 % Elapsed time: 0.516865 seconds
% 1.55/0.89 % CPU time: 3.744977 seconds
% 1.55/0.89 % Total memory used: 137.700 MB
% 1.55/0.89 % Net memory used: 135.340 MB
%------------------------------------------------------------------------------