%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO600+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:25:20 PM UTC 2026
% Result : Theorem 4.80s 1.07s
% Output : CNFRefutation 4.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 11
% Syntax : Number of formulae : 54 ( 13 unt; 0 def)
% Number of atoms : 168 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 151 ( 37 ~; 32 |; 70 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 39 ( 8 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-8 aty)
% Number of functors : 23 ( 23 usr; 23 con; 0-0 aty)
% Number of variables : 268 ( 222 !; 46 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(A,C,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(B,A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B,C,D] :
( ( coll(A,B,D)
& coll(A,B,C) )
=> coll(C,D,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B,C,D] :
( para(A,B,C,D)
=> para(A,B,D,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B,M] :
( midp(M,B,A)
=> midp(M,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,C,D,P,Q,U,V)
=> eqangle(C,D,A,B,U,V,P,Q) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [A,B,C,D,P,Q] :
( eqangle(A,B,P,Q,C,D,P,Q)
=> para(A,B,C,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A,B,C,D,P,Q] :
( para(A,B,C,D)
=> eqangle(A,B,P,Q,C,D,P,Q) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A,B,C,D,M] :
( ( midp(M,C,D)
& midp(M,A,B) )
=> para(A,C,B,D) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [A,B,C] :
( para(A,B,A,C)
=> coll(A,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,conjecture,
! [A,B,C,D,E,F,G,H,I,J,K,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6,NWPNT7,NWPNT8,NWPNT9,NWPNT01,NWPNT11,NWPNT21] :
( ( circle(J,B,K,NWPNT21)
& circle(F,E,K,NWPNT11)
& circle(J,B,NWPNT9,NWPNT01)
& midp(J,B,E)
& circle(G,E,I,NWPNT8)
& coll(I,A,B)
& circle(G,E,H,NWPNT7)
& circle(F,E,H,NWPNT6)
& circle(G,E,NWPNT4,NWPNT5)
& circle(F,E,NWPNT2,NWPNT3)
& midp(G,A,E)
& midp(F,C,E)
& circle(D,A,E,NWPNT1)
& circle(D,A,B,C) )
=> coll(I,H,K) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,negated_conjecture,
~ ! [A,B,C,D,E,F,G,H,I,J,K,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6,NWPNT7,NWPNT8,NWPNT9,NWPNT01,NWPNT11,NWPNT21] :
( ( circle(J,B,K,NWPNT21)
& circle(F,E,K,NWPNT11)
& circle(J,B,NWPNT9,NWPNT01)
& midp(J,B,E)
& circle(G,E,I,NWPNT8)
& coll(I,A,B)
& circle(G,E,H,NWPNT7)
& circle(F,E,H,NWPNT6)
& circle(G,E,NWPNT4,NWPNT5)
& circle(F,E,NWPNT2,NWPNT3)
& midp(G,A,E)
& midp(F,C,E)
& circle(D,A,E,NWPNT1)
& circle(D,A,B,C) )
=> coll(I,H,K) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f97,plain,
! [A,B,C] :
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f98,plain,
! [X0,X1,X2] :
( coll(X0,X2,X1)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f99,plain,
! [A,B,C] :
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f100,plain,
! [X0,X1,X2] :
( coll(X1,X0,X2)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
! [A,B,C,D] :
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f102,plain,
! [A,C,D] :
( coll(C,D,A)
| ! [B] :
( ~ coll(A,B,D)
| ~ coll(A,B,C) ) ),
inference(miniscoping,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1,X2,X3] :
( coll(X2,X3,X0)
| ~ coll(X0,X1,X3)
| ~ coll(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
! [A,B,C,D] :
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f105,plain,
! [X0,X1,X2,X3] :
( para(X0,X1,X3,X2)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f121,plain,
! [A,B,M] :
( midp(M,A,B)
| ~ midp(M,B,A) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f122,plain,
! [X0,X1,X2] :
( midp(X0,X2,X1)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f139,plain,
! [A,B,C,D,P,Q,U,V] :
( eqangle(C,D,A,B,U,V,P,Q)
| ~ eqangle(A,B,C,D,P,Q,U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f140,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( eqangle(X2,X3,X0,X1,X6,X7,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X6,X7) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f184,plain,
! [A,B,C,D,P,Q] :
( para(A,B,C,D)
| ~ eqangle(A,B,P,Q,C,D,P,Q) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f185,plain,
! [A,B,C,D] :
( para(A,B,C,D)
| ! [P,Q] : ~ eqangle(A,B,P,Q,C,D,P,Q) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f186,plain,
! [X0,X1,X2,X3,X4,X5] :
( para(X0,X1,X4,X5)
| ~ eqangle(X0,X1,X2,X3,X4,X5,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f187,plain,
! [A,B,C,D,P,Q] :
( eqangle(A,B,P,Q,C,D,P,Q)
| ~ para(A,B,C,D) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f188,plain,
! [A,B,C,D] :
( ! [P,Q] : eqangle(A,B,P,Q,C,D,P,Q)
| ~ para(A,B,C,D) ),
inference(miniscoping,[status(thm)],[f187]) ).
fof(f189,plain,
! [X0,X1,X2,X3,X4,X5] :
( eqangle(X0,X1,X4,X5,X2,X3,X4,X5)
| ~ para(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f188]) ).
fof(f247,plain,
! [A,B,C,D,M] :
( para(A,C,B,D)
| ~ midp(M,C,D)
| ~ midp(M,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f248,plain,
! [A,B,C,D] :
( para(A,C,B,D)
| ! [M] :
( ~ midp(M,C,D)
| ~ midp(M,A,B) ) ),
inference(miniscoping,[status(thm)],[f247]) ).
fof(f249,plain,
! [X0,X1,X2,X3,X4] :
( para(X1,X3,X2,X4)
| ~ midp(X0,X3,X4)
| ~ midp(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f248]) ).
fof(f255,plain,
! [A,B,C] :
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f256,plain,
! [X0,X1,X2] :
( coll(X0,X1,X2)
| ~ para(X0,X1,X0,X2) ),
inference(cnf_transformation,[status(thm)],[f255]) ).
fof(f369,plain,
? [A,B,C,D,E,F,G,H,I,J,K,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6,NWPNT7,NWPNT8,NWPNT9,NWPNT01,NWPNT11,NWPNT21] :
( ~ coll(I,H,K)
& circle(J,B,K,NWPNT21)
& circle(F,E,K,NWPNT11)
& circle(J,B,NWPNT9,NWPNT01)
& midp(J,B,E)
& circle(G,E,I,NWPNT8)
& coll(I,A,B)
& circle(G,E,H,NWPNT7)
& circle(F,E,H,NWPNT6)
& circle(G,E,NWPNT4,NWPNT5)
& circle(F,E,NWPNT2,NWPNT3)
& midp(G,A,E)
& midp(F,C,E)
& circle(D,A,E,NWPNT1)
& circle(D,A,B,C) ),
inference(pre_NNF_transformation,[status(thm)],[f96]) ).
fof(f370,plain,
? [H,I,K] :
( ~ coll(I,H,K)
& ? [B,J] :
( ? [NWPNT21] : circle(J,B,K,NWPNT21)
& ? [E,F] :
( ? [NWPNT11] : circle(F,E,K,NWPNT11)
& ? [NWPNT9,NWPNT01] : circle(J,B,NWPNT9,NWPNT01)
& midp(J,B,E)
& ? [G] :
( ? [NWPNT8] : circle(G,E,I,NWPNT8)
& ? [A] :
( coll(I,A,B)
& ? [NWPNT7] : circle(G,E,H,NWPNT7)
& ? [NWPNT6] : circle(F,E,H,NWPNT6)
& ? [NWPNT4,NWPNT5] : circle(G,E,NWPNT4,NWPNT5)
& ? [NWPNT2,NWPNT3] : circle(F,E,NWPNT2,NWPNT3)
& midp(G,A,E)
& ? [C] :
( midp(F,C,E)
& ? [D] :
( ? [NWPNT1] : circle(D,A,E,NWPNT1)
& circle(D,A,B,C) ) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f369]) ).
fof(f371,plain,
( ~ coll(sK21_skl,sK20_skl,sK22_skl)
& circle(sK24_skl,sK23_skl,sK22_skl,sK42_skl)
& circle(sK26_skl,sK25_skl,sK22_skl,sK41_skl)
& circle(sK24_skl,sK23_skl,sK39_skl,sK40_skl)
& midp(sK24_skl,sK23_skl,sK25_skl)
& circle(sK27_skl,sK25_skl,sK21_skl,sK38_skl)
& coll(sK21_skl,sK28_skl,sK23_skl)
& circle(sK27_skl,sK25_skl,sK20_skl,sK37_skl)
& circle(sK26_skl,sK25_skl,sK20_skl,sK36_skl)
& circle(sK27_skl,sK25_skl,sK34_skl,sK35_skl)
& circle(sK26_skl,sK25_skl,sK32_skl,sK33_skl)
& midp(sK27_skl,sK28_skl,sK25_skl)
& midp(sK26_skl,sK29_skl,sK25_skl)
& circle(sK30_skl,sK28_skl,sK25_skl,sK31_skl)
& circle(sK30_skl,sK28_skl,sK23_skl,sK29_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl,sK31_skl,sK32_skl,sK33_skl,sK34_skl,sK35_skl,sK36_skl,sK37_skl,sK38_skl,sK39_skl,sK40_skl,sK41_skl,sK42_skl]),skolemize(H,sK20_skl),skolemize(I,sK21_skl),skolemize(K,sK22_skl),skolemize(B,sK23_skl),skolemize(J,sK24_skl),skolemize(E,sK25_skl),skolemize(F,sK26_skl),skolemize(G,sK27_skl),skolemize(A,sK28_skl),skolemize(C,sK29_skl),skolemize(D,sK30_skl),skolemize(NWPNT1,sK31_skl),skolemize(NWPNT2,sK32_skl),skolemize(NWPNT3,sK33_skl),skolemize(NWPNT4,sK34_skl),skolemize(NWPNT5,sK35_skl),skolemize(NWPNT6,sK36_skl),skolemize(NWPNT7,sK37_skl),skolemize(NWPNT8,sK38_skl),skolemize(NWPNT9,sK39_skl),skolemize(NWPNT01,sK40_skl),skolemize(NWPNT11,sK41_skl),skolemize(NWPNT21,sK42_skl)],[f370]) ).
fof(f382,plain,
midp(sK24_skl,sK23_skl,sK25_skl),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f386,plain,
~ coll(sK21_skl,sK20_skl,sK22_skl),
inference(cnf_transformation,[status(thm)],[f371]) ).
fof(f399,plain,
midp(sK24_skl,sK25_skl,sK23_skl),
inference(resolution,[status(thm)],[f122,f382]) ).
fof(f2023,plain,
! [X0,X1] :
( para(sK23_skl,X0,sK25_skl,X1)
| ~ midp(sK24_skl,X0,X1) ),
inference(resolution,[status(thm)],[f249,f382]) ).
fof(f2801,plain,
para(sK23_skl,sK25_skl,sK25_skl,sK23_skl),
inference(resolution,[status(thm)],[f2023,f399]) ).
fof(f2853,plain,
para(sK23_skl,sK25_skl,sK23_skl,sK25_skl),
inference(resolution,[status(thm)],[f2801,f105]) ).
fof(f2873,plain,
! [X0,X1] : eqangle(sK23_skl,sK25_skl,X0,X1,sK23_skl,sK25_skl,X0,X1),
inference(resolution,[status(thm)],[f2853,f189]) ).
fof(f6819,plain,
! [X0,X1] : eqangle(X0,X1,sK23_skl,sK25_skl,X0,X1,sK23_skl,sK25_skl),
inference(resolution,[status(thm)],[f2873,f140]) ).
fof(f7895,plain,
! [X0,X1] : para(X0,X1,X0,X1),
inference(resolution,[status(thm)],[f6819,f186]) ).
fof(f7917,plain,
! [X0,X1] : coll(X0,X1,X1),
inference(resolution,[status(thm)],[f7895,f256]) ).
fof(f8426,plain,
! [X0,X1] : coll(X0,X1,X0),
inference(resolution,[status(thm)],[f7917,f100]) ).
fof(f8878,plain,
! [X0,X1] : coll(X0,X0,X1),
inference(resolution,[status(thm)],[f8426,f98]) ).
fof(f8935,plain,
! [X0,X1,X2] :
( coll(X2,X1,X0)
| ~ coll(X0,X0,X1) ),
inference(resolution,[status(thm)],[f8878,f103]) ).
fof(f8938,plain,
! [X0,X1,X2] : coll(X0,X1,X2),
inference(forward_subsumption_resolution,[status(thm)],[f8935,f8878]) ).
fof(f8964,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f386,f8938]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO600+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n017.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 17:43:11 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 4.80/1.07 % Refutation found
% 4.80/1.07 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.80/1.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.29/1.11 % Elapsed time: 0.735931 seconds
% 0.29/1.11 % CPU time: 5.532484 seconds
% 0.29/1.11 % Total memory used: 142.872 MB
% 0.29/1.11 % Net memory used: 137.022 MB
%------------------------------------------------------------------------------