%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRA010+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:30:40 PM UTC 2026
% Result : Theorem 0.14s 5.44s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 2
% Syntax : Number of formulae : 28 ( 8 unt; 0 def)
% Number of atoms : 96 ( 18 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 101 ( 33 ~; 33 |; 27 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 2 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 68 ( 53 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
! [P,V1,V2] :
( ( ! [E1,E2] :
( ( sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
=> ? [E3] : triangle(E1,E2,E3) )
& path(V1,V2,P) )
=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
( complete
=> ! [P,V1,V2] :
( ( ! [E1,E2] :
( ( sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
=> ? [E3] : triangle(E1,E2,E3) )
& path(V1,V2,P) )
=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ ( complete
=> ! [P,V1,V2] :
( ( ! [E1,E2] :
( ( sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
=> ? [E3] : triangle(E1,E2,E3) )
& path(V1,V2,P) )
=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f109,plain,
! [P,V1,V2] :
( number_of_in(sequential_pairs,P) = number_of_in(triangles,P)
| ? [E1,E2] :
( ! [E3] : ~ triangle(E1,E2,E3)
& sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
| ~ path(V1,V2,P) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f110,plain,
! [P] :
( number_of_in(sequential_pairs,P) = number_of_in(triangles,P)
| ? [E1,E2] :
( ! [E3] : ~ triangle(E1,E2,E3)
& sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
| ! [V1,V2] : ~ path(V1,V2,P) ),
inference(miniscoping,[status(thm)],[f109]) ).
fof(f111,plain,
! [P] :
( number_of_in(sequential_pairs,P) = number_of_in(triangles,P)
| ( ! [E3] : ~ triangle(sK6_skl(P),sK7_skl(P),E3)
& sequential(sK6_skl(P),sK7_skl(P))
& on_path(sK7_skl(P),P)
& on_path(sK6_skl(P),P) )
| ! [V1,V2] : ~ path(V1,V2,P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(E1,sK6_skl(P)),skolemize(E2,sK7_skl(P))],[f110]) ).
fof(f112,plain,
! [X0,X1,X2] :
( number_of_in(sequential_pairs,X2) = number_of_in(triangles,X2)
| on_path(sK6_skl(X2),X2)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [X0,X1,X2] :
( number_of_in(sequential_pairs,X2) = number_of_in(triangles,X2)
| on_path(sK7_skl(X2),X2)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f114,plain,
! [X0,X1,X2] :
( number_of_in(sequential_pairs,X2) = number_of_in(triangles,X2)
| sequential(sK6_skl(X2),sK7_skl(X2))
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( number_of_in(sequential_pairs,X2) = number_of_in(triangles,X2)
| ~ triangle(sK6_skl(X2),sK7_skl(X2),X3)
| ~ path(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f121,plain,
( ? [P,V1,V2] :
( number_of_in(sequential_pairs,P) != number_of_in(triangles,P)
& ! [E1,E2] :
( ? [E3] : triangle(E1,E2,E3)
| ~ sequential(E1,E2)
| ~ on_path(E2,P)
| ~ on_path(E1,P) )
& path(V1,V2,P) )
& complete ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f122,plain,
( ? [P] :
( number_of_in(sequential_pairs,P) != number_of_in(triangles,P)
& ! [E1,E2] :
( ? [E3] : triangle(E1,E2,E3)
| ~ sequential(E1,E2)
| ~ on_path(E2,P)
| ~ on_path(E1,P) )
& ? [V1,V2] : path(V1,V2,P) )
& complete ),
inference(miniscoping,[status(thm)],[f121]) ).
fof(f123,plain,
( number_of_in(sequential_pairs,sK9_skl) != number_of_in(triangles,sK9_skl)
& ! [E1,E2] :
( triangle(E1,E2,sK12_skl(E2,E1))
| ~ sequential(E1,E2)
| ~ on_path(E2,sK9_skl)
| ~ on_path(E1,sK9_skl) )
& path(sK10_skl,sK11_skl,sK9_skl)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl,sK11_skl,sK12_skl]),skolemize(P,sK9_skl),skolemize(V1,sK10_skl),skolemize(V2,sK11_skl),skolemize(E3,sK12_skl(E2,E1))],[f122]) ).
fof(f125,plain,
path(sK10_skl,sK11_skl,sK9_skl),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f126,plain,
! [X0,X1] :
( triangle(X0,X1,sK12_skl(X1,X0))
| ~ sequential(X0,X1)
| ~ on_path(X1,sK9_skl)
| ~ on_path(X0,sK9_skl) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f127,plain,
number_of_in(sequential_pairs,sK9_skl) != number_of_in(triangles,sK9_skl),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f264,plain,
( number_of_in(sequential_pairs,sK9_skl) = number_of_in(triangles,sK9_skl)
| on_path(sK6_skl(sK9_skl),sK9_skl) ),
inference(resolution,[status(thm)],[f112,f125]) ).
fof(f265,plain,
on_path(sK6_skl(sK9_skl),sK9_skl),
inference(forward_subsumption_resolution,[status(thm)],[f264,f127]) ).
fof(f268,plain,
( number_of_in(sequential_pairs,sK9_skl) = number_of_in(triangles,sK9_skl)
| on_path(sK7_skl(sK9_skl),sK9_skl) ),
inference(resolution,[status(thm)],[f113,f125]) ).
fof(f269,plain,
on_path(sK7_skl(sK9_skl),sK9_skl),
inference(forward_subsumption_resolution,[status(thm)],[f268,f127]) ).
fof(f274,plain,
! [X0] :
( triangle(sK6_skl(sK9_skl),X0,sK12_skl(X0,sK6_skl(sK9_skl)))
| ~ sequential(sK6_skl(sK9_skl),X0)
| ~ on_path(X0,sK9_skl) ),
inference(resolution,[status(thm)],[f265,f126]) ).
fof(f313,plain,
( number_of_in(sequential_pairs,sK9_skl) = number_of_in(triangles,sK9_skl)
| sequential(sK6_skl(sK9_skl),sK7_skl(sK9_skl)) ),
inference(resolution,[status(thm)],[f114,f125]) ).
fof(f314,plain,
sequential(sK6_skl(sK9_skl),sK7_skl(sK9_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f313,f127]) ).
fof(f592,plain,
( triangle(sK6_skl(sK9_skl),sK7_skl(sK9_skl),sK12_skl(sK7_skl(sK9_skl),sK6_skl(sK9_skl)))
| ~ on_path(sK7_skl(sK9_skl),sK9_skl) ),
inference(resolution,[status(thm)],[f274,f314]) ).
fof(f593,plain,
triangle(sK6_skl(sK9_skl),sK7_skl(sK9_skl),sK12_skl(sK7_skl(sK9_skl),sK6_skl(sK9_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f592,f269]) ).
fof(f1164,plain,
! [X0,X1] :
( number_of_in(sequential_pairs,sK9_skl) = number_of_in(triangles,sK9_skl)
| ~ path(X0,X1,sK9_skl) ),
inference(resolution,[status(thm)],[f593,f115]) ).
fof(f1171,plain,
! [X0,X1] : ~ path(X0,X1,sK9_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1164,f127]) ).
fof(f1173,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f125,f1171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA010+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n013.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Sun Sep 20 18:20:26 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 % Drodi V4.1.1
% 0.14/5.44 % Refutation found
% 0.14/5.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/5.48 % Elapsed time: 0.087318 seconds
% 0.14/5.48 % CPU time: 0.452963 seconds
% 0.14/5.48 % Total memory used: 89.623 MB
% 0.14/5.48 % Net memory used: 89.041 MB
%------------------------------------------------------------------------------