%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO571+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 : Sun Sep 27 07:18:08 AM UTC 2026
% Result : Theorem 35.34s 5.02s
% Output : CNFRefutation 35.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 41
% Syntax : Number of formulae : 290 ( 116 unt; 0 def)
% Number of atoms : 587 ( 0 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 498 ( 201 ~; 197 |; 58 &)
% ( 0 <=>; 42 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-4 aty)
% Number of variables : 850 ( 181 sgn 217 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ruleD1,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(A,C,B) ),
file('theBenchmark.p',ruleD1) ).
fof(ruleD2,axiom,
! [A,B,C] :
( coll(A,B,C)
=> coll(B,A,C) ),
file('theBenchmark.p',ruleD2) ).
fof(ruleD3,axiom,
! [A,B,C,D] :
( ( coll(A,B,D)
& coll(A,B,C) )
=> coll(C,D,A) ),
file('theBenchmark.p',ruleD3) ).
fof(ruleD5,axiom,
! [A,B,C,D] :
( para(A,B,C,D)
=> para(C,D,A,B) ),
file('theBenchmark.p',ruleD5) ).
fof(ruleD6,axiom,
! [A,B,C,D,E,F] :
( ( para(C,D,E,F)
& para(A,B,C,D) )
=> para(A,B,E,F) ),
file('theBenchmark.p',ruleD6) ).
fof(ruleD7,axiom,
! [A,B,C,D] :
( perp(A,B,C,D)
=> perp(A,B,D,C) ),
file('theBenchmark.p',ruleD7) ).
fof(ruleD8,axiom,
! [A,B,C,D] :
( perp(A,B,C,D)
=> perp(C,D,A,B) ),
file('theBenchmark.p',ruleD8) ).
fof(ruleD9,axiom,
! [A,B,C,D,E,F] :
( ( perp(C,D,E,F)
& perp(A,B,C,D) )
=> para(A,B,E,F) ),
file('theBenchmark.p',ruleD9) ).
fof(ruleD10,axiom,
! [A,B,C,D,E,F] :
( ( perp(C,D,E,F)
& para(A,B,C,D) )
=> perp(A,B,E,F) ),
file('theBenchmark.p',ruleD10) ).
fof(ruleD11,axiom,
! [A,B,M] :
( midp(M,B,A)
=> midp(M,A,B) ),
file('theBenchmark.p',ruleD11) ).
fof(ruleD12,axiom,
! [A,B,C,O] :
( ( cong(O,A,O,C)
& cong(O,A,O,B) )
=> circle(O,A,B,C) ),
file('theBenchmark.p',ruleD12) ).
fof(ruleD14,axiom,
! [A,B,C,D] :
( cyclic(A,B,C,D)
=> cyclic(A,B,D,C) ),
file('theBenchmark.p',ruleD14) ).
fof(ruleD15,axiom,
! [A,B,C,D] :
( cyclic(A,B,C,D)
=> cyclic(A,C,B,D) ),
file('theBenchmark.p',ruleD15) ).
fof(ruleD16,axiom,
! [A,B,C,D] :
( cyclic(A,B,C,D)
=> cyclic(B,A,C,D) ),
file('theBenchmark.p',ruleD16) ).
fof(ruleD17,axiom,
! [A,B,C,D,E] :
( ( cyclic(A,B,C,E)
& cyclic(A,B,C,D) )
=> cyclic(B,C,D,E) ),
file('theBenchmark.p',ruleD17) ).
fof(ruleD18,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,C,D,P,Q,U,V)
=> eqangle(B,A,C,D,P,Q,U,V) ),
file('theBenchmark.p',ruleD18) ).
fof(ruleD19,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('theBenchmark.p',ruleD19) ).
fof(ruleD21,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,C,D,P,Q,U,V)
=> eqangle(A,B,P,Q,C,D,U,V) ),
file('theBenchmark.p',ruleD21) ).
fof(ruleD22,axiom,
! [A,B,C,D,P,Q,U,V,E,F,G,H] :
( ( eqangle(P,Q,U,V,E,F,G,H)
& eqangle(A,B,C,D,P,Q,U,V) )
=> eqangle(A,B,C,D,E,F,G,H) ),
file('theBenchmark.p',ruleD22) ).
fof(ruleD23,axiom,
! [A,B,C,D] :
( cong(A,B,C,D)
=> cong(A,B,D,C) ),
file('theBenchmark.p',ruleD23) ).
fof(ruleD40,axiom,
! [A,B,C,D,P,Q] :
( para(A,B,C,D)
=> eqangle(A,B,P,Q,C,D,P,Q) ),
file('theBenchmark.p',ruleD40) ).
fof(ruleD41,axiom,
! [A,B,P,Q] :
( cyclic(A,B,P,Q)
=> eqangle(P,A,P,B,Q,A,Q,B) ),
file('theBenchmark.p',ruleD41) ).
fof(ruleD42b,axiom,
! [A,B,P,Q] :
( ( coll(P,Q,B)
& eqangle(P,A,P,B,Q,A,Q,B) )
=> cyclic(A,B,P,Q) ),
file('theBenchmark.p',ruleD42b) ).
fof(ruleD43,axiom,
! [A,B,C,P,Q,R] :
( ( eqangle(C,A,C,B,R,P,R,Q)
& cyclic(A,B,C,R)
& cyclic(A,B,C,Q)
& cyclic(A,B,C,P) )
=> cong(A,B,P,Q) ),
file('theBenchmark.p',ruleD43) ).
fof(ruleD44,axiom,
! [A,B,C,E,F] :
( ( midp(F,A,C)
& midp(E,A,B) )
=> para(E,F,B,C) ),
file('theBenchmark.p',ruleD44) ).
fof(ruleD45,axiom,
! [A,B,C,E,F] :
( ( coll(F,A,C)
& para(E,F,B,C)
& midp(E,A,B) )
=> midp(F,A,C) ),
file('theBenchmark.p',ruleD45) ).
fof(ruleD46,axiom,
! [A,B,O] :
( cong(O,A,O,B)
=> eqangle(O,A,A,B,A,B,O,B) ),
file('theBenchmark.p',ruleD46) ).
fof(ruleD48,axiom,
! [A,B,C,O,X] :
( ( perp(O,A,A,X)
& circle(O,A,B,C) )
=> eqangle(A,X,A,B,C,A,C,B) ),
file('theBenchmark.p',ruleD48) ).
fof(ruleD49,axiom,
! [A,B,C,O,X] :
( ( eqangle(A,X,A,B,C,A,C,B)
& circle(O,A,B,C) )
=> perp(O,A,A,X) ),
file('theBenchmark.p',ruleD49) ).
fof(ruleD50,axiom,
! [A,B,C,O,M] :
( ( midp(M,B,C)
& circle(O,A,B,C) )
=> eqangle(A,B,A,C,O,B,O,M) ),
file('theBenchmark.p',ruleD50) ).
fof(ruleD51,axiom,
! [A,B,C,O,M] :
( ( eqangle(A,B,A,C,O,B,O,M)
& coll(M,B,C)
& circle(O,A,B,C) )
=> midp(M,B,C) ),
file('theBenchmark.p',ruleD51) ).
fof(ruleD54,axiom,
! [A,B,C,D] :
( ( para(A,B,C,D)
& cyclic(A,B,C,D) )
=> eqangle(A,D,C,D,C,D,C,B) ),
file('theBenchmark.p',ruleD54) ).
fof(ruleD55,axiom,
! [A,B,M,O] :
( ( perp(O,M,A,B)
& midp(M,A,B) )
=> cong(O,A,O,B) ),
file('theBenchmark.p',ruleD55) ).
fof(ruleD56,axiom,
! [A,B,P,Q] :
( ( cong(A,Q,B,Q)
& cong(A,P,B,P) )
=> perp(A,B,P,Q) ),
file('theBenchmark.p',ruleD56) ).
fof(ruleD57,axiom,
! [A,B,P,Q] :
( ( cyclic(A,B,P,Q)
& cong(A,Q,B,Q)
& cong(A,P,B,P) )
=> perp(P,A,A,Q) ),
file('theBenchmark.p',ruleD57) ).
fof(ruleD64,axiom,
! [A,B,C,D,M] :
( ( para(A,D,B,C)
& para(A,C,B,D)
& midp(M,A,B) )
=> midp(M,C,D) ),
file('theBenchmark.p',ruleD64) ).
fof(ruleD66,axiom,
! [A,B,C] :
( para(A,B,A,C)
=> coll(A,B,C) ),
file('theBenchmark.p',ruleD66) ).
fof(ruleD67,axiom,
! [A,B,C] :
( ( coll(A,B,C)
& cong(A,B,A,C) )
=> midp(A,B,C) ),
file('theBenchmark.p',ruleD67) ).
fof(ruleD68,axiom,
! [A,B,C] :
( midp(A,B,C)
=> cong(A,B,A,C) ),
file('theBenchmark.p',ruleD68) ).
fof(ruleX14,axiom,
! [A,B,C,D] :
? [O] :
( ( cyclic(A,B,C,D)
& perp(A,C,C,B) )
=> circle(O,A,B,C) ),
file('theBenchmark.p',ruleX14) ).
fof(exemplo6GDDFULL214033,conjecture,
! [A,B,C,O,D,I,E,F,NWPNT1] :
( ( perp(A,B,B,F)
& perp(C,D,C,F)
& perp(A,B,A,E)
& perp(C,D,D,E)
& coll(I,C,D)
& coll(I,A,B)
& circle(O,A,D,NWPNT1)
& circle(O,A,B,C) )
=> eqangle(A,I,I,E,F,I,I,C) ),
file('theBenchmark.p',exemplo6GDDFULL214033) ).
fof(exemplo6GDDFULL214033_neg,negated_conjecture,
~ ! [A,B,C,O,D,I,E,F,NWPNT1] :
( ( perp(A,B,B,F)
& perp(C,D,C,F)
& perp(A,B,A,E)
& perp(C,D,D,E)
& coll(I,C,D)
& coll(I,A,B)
& circle(O,A,D,NWPNT1)
& circle(O,A,B,C) )
=> eqangle(A,I,I,E,F,I,I,C) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL214033]) ).
cnf(c_96,plain,
( eqangle(B,E,B,C,D,B,D,C)
| ~ perp(A,B,B,E)
| ~ circle(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD48]) ).
cnf(c_97,plain,
( circle(A,B,C,D)
| ~ cong(A,B,A,D)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD12]) ).
cnf(c_98,plain,
( perp(A,B,B,E)
| ~ eqangle(B,E,B,C,D,B,D,C)
| ~ circle(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD49]) ).
cnf(c_99,plain,
( eqangle(B,C,B,D,A,C,A,E)
| ~ midp(E,C,D)
| ~ circle(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD50]) ).
cnf(c_100,plain,
( midp(E,C,D)
| ~ eqangle(B,C,B,D,A,C,A,E)
| ~ coll(E,C,D)
| ~ circle(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD51]) ).
fof(nnf_90,plain,
! [A,B,C,D] :
? [O] :
( circle(O,A,B,C)
| ~ cyclic(A,B,C,D)
| ~ perp(A,C,C,B) ),
inference(fof_nnf,[status(thm)],[ruleX14]) ).
fof(sk_ruleX14,plain,
! [A,B,C,D] :
( circle(sK0(A,B,C,D),A,B,C)
| ~ cyclic(A,B,C,D)
| ~ perp(A,C,C,B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(O,sK0(A,B,C,D))],[nnf_90]) ).
cnf(c_108,plain,
( circle(sK0(A,C,B,D),A,C,B)
| ~ cyclic(A,C,B,D)
| ~ perp(A,B,B,C) ),
inference(split_conjunct,[status(thm)],[sk_ruleX14]) ).
cnf(c_139,plain,
( eqangle(A,E,A,C,B,A,B,C)
| ~ perp(sK0(A,C,B,D),A,A,E)
| ~ cyclic(A,C,B,D)
| ~ perp(A,B,B,C) ),
inference(resolve,[status(thm)],[c_108,c_96]) ).
cnf(c_142,plain,
( midp(E,C,B)
| ~ eqangle(A,C,A,B,sK0(A,C,B,D),C,sK0(A,C,B,D),E)
| ~ coll(E,C,B)
| ~ cyclic(A,C,B,D)
| ~ perp(A,B,B,C) ),
inference(resolve,[status(thm)],[c_108,c_100]) ).
cnf(c_174,plain,
( ~ cong(E,D,E,C)
| ~ cong(E,D,E,B)
| eqangle(D,B,D,C,E,B,E,A)
| ~ midp(A,B,C) ),
inference(resolve,[status(thm)],[c_99,c_97]) ).
cnf(c_175,plain,
( ~ cong(E,A,E,D)
| ~ cong(E,A,E,C)
| perp(E,A,A,B)
| ~ eqangle(A,B,A,C,D,A,D,C) ),
inference(resolve,[status(thm)],[c_98,c_97]) ).
cnf(c_176,plain,
( ~ cong(A,B,A,E)
| ~ cong(A,B,A,D)
| eqangle(B,C,B,D,E,B,E,D)
| ~ perp(A,B,B,C) ),
inference(resolve,[status(thm)],[c_96,c_97]) ).
fof(nnf_95,plain,
? [A,B,C,O,D,I,E,F,NWPNT1] :
( ~ eqangle(A,I,I,E,F,I,I,C)
& perp(A,B,B,F)
& perp(C,D,C,F)
& perp(A,B,A,E)
& perp(C,D,D,E)
& coll(I,C,D)
& coll(I,A,B)
& circle(O,A,D,NWPNT1)
& circle(O,A,B,C) ),
inference(fof_nnf,[status(thm)],[exemplo6GDDFULL214033_neg]) ).
fof(sk_exemplo6GDDFULL214033_neg,plain,
( ~ eqangle(sK1,sK2,sK2,sK3,sK4,sK2,sK2,sK5)
& perp(sK1,sK8,sK8,sK4)
& perp(sK5,sK6,sK5,sK4)
& perp(sK1,sK8,sK1,sK3)
& perp(sK5,sK6,sK6,sK3)
& coll(sK2,sK5,sK6)
& coll(sK2,sK1,sK8)
& circle(sK7,sK1,sK6,sK9)
& circle(sK7,sK1,sK8,sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK1,sK8,sK5,sK6,sK9,sK2,sK3,sK4]),skolemize(A,sK1),skolemize(B,sK8),skolemize(C,sK5),skolemize(O,sK7),skolemize(D,sK6),skolemize(I,sK2),skolemize(E,sK3),skolemize(F,sK4),skolemize(NWPNT1,sK9)],[nnf_95]) ).
cnf(c_177,negated_conjecture,
~ eqangle(sK1,sK2,sK2,sK3,sK4,sK2,sK2,sK5),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214033_neg]) ).
cnf(c_181,negated_conjecture,
perp(sK5,sK6,sK6,sK3),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214033_neg]) ).
cnf(c_182,negated_conjecture,
coll(sK2,sK5,sK6),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214033_neg]) ).
cnf(c_220,plain,
( cong(A,B,A,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD68]) ).
cnf(c_221,plain,
( midp(A,B,C)
| ~ coll(A,B,C)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD67]) ).
cnf(c_222,plain,
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD66]) ).
cnf(c_224,plain,
( midp(A,D,E)
| ~ para(B,E,C,D)
| ~ para(B,D,C,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD64]) ).
cnf(c_231,plain,
( perp(B,A,A,D)
| ~ cyclic(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD57]) ).
cnf(c_232,plain,
( perp(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD56]) ).
cnf(c_233,plain,
( cong(D,B,D,C)
| ~ perp(D,A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD55]) ).
cnf(c_234,plain,
( eqangle(A,D,C,D,C,D,C,B)
| ~ para(A,B,C,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD54]) ).
cnf(c_237,plain,
( eqangle(A,B,B,C,B,C,A,C)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD46]) ).
cnf(c_238,plain,
( midp(D,B,E)
| ~ coll(D,B,E)
| ~ para(A,D,C,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD45]) ).
cnf(c_239,plain,
( para(A,D,C,E)
| ~ midp(D,B,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD44]) ).
cnf(c_240,plain,
( cong(A,B,D,E)
| ~ eqangle(C,A,C,B,F,D,F,E)
| ~ cyclic(A,B,C,F)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD43]) ).
cnf(c_241,plain,
( cyclic(B,C,A,D)
| ~ coll(A,D,C)
| ~ eqangle(A,B,A,C,D,B,D,C) ),
inference(clausify,[status(thm)],[ruleD42b]) ).
cnf(c_243,plain,
( eqangle(C,A,C,B,D,A,D,B)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD41]) ).
cnf(c_244,plain,
( eqangle(A,B,E,F,C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD40]) ).
cnf(c_261,plain,
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD23]) ).
cnf(c_262,plain,
( eqangle(A,B,C,D,V8,V9,V10,V11)
| ~ eqangle(E,F,V6,V7,V8,V9,V10,V11)
| ~ eqangle(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[ruleD22]) ).
cnf(c_263,plain,
( eqangle(A,B,E,F,C,D,V6,V7)
| ~ eqangle(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[ruleD21]) ).
cnf(c_265,plain,
( eqangle(C,D,A,B,V6,V7,E,F)
| ~ eqangle(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[ruleD19]) ).
cnf(c_266,plain,
( eqangle(B,A,C,D,E,F,V6,V7)
| ~ eqangle(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[ruleD18]) ).
cnf(c_267,plain,
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD17]) ).
cnf(c_268,plain,
( cyclic(B,A,C,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD16]) ).
cnf(c_269,plain,
( cyclic(A,C,B,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD15]) ).
cnf(c_270,plain,
( cyclic(A,B,D,C)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD14]) ).
cnf(c_272,plain,
( midp(A,C,B)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD11]) ).
cnf(c_273,plain,
( perp(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD10]) ).
cnf(c_274,plain,
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD9]) ).
cnf(c_275,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD8]) ).
cnf(c_276,plain,
( perp(A,B,D,C)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD7]) ).
cnf(c_277,plain,
( para(A,B,E,F)
| ~ para(C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD6]) ).
cnf(c_278,plain,
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD5]) ).
cnf(c_280,plain,
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD3]) ).
cnf(c_281,plain,
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD2]) ).
cnf(c_282,plain,
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD1]) ).
cnf(c_300,plain,
( ~ cong(D,A,D,C)
| perp(D,A,A,B)
| ~ eqangle(A,B,A,C,C,A,C,C) ),
inference(factor,[status(thm)],[c_175]) ).
cnf(c_301,plain,
( ~ cong(A,B,A,D)
| eqangle(B,C,B,D,D,B,D,D)
| ~ perp(A,B,B,C) ),
inference(factor,[status(thm)],[c_176]) ).
cnf(c_322,plain,
( midp(A,D,D)
| ~ para(B,D,C,D)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_224]) ).
cnf(c_325,plain,
( perp(B,A,A,B)
| ~ cyclic(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_231]) ).
cnf(c_327,plain,
( para(A,A,C,C)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_239]) ).
cnf(c_328,plain,
( cong(A,B,D,D)
| ~ eqangle(C,A,C,B,E,D,E,D)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_240]) ).
cnf(c_330,plain,
( cong(A,B,D,E)
| ~ eqangle(C,A,C,B,E,D,E,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_240]) ).
cnf(c_331,plain,
( cyclic(B,C,D,D)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_267]) ).
cnf(c_336,plain,
( coll(C,C,A)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_280]) ).
cnf(c_344,plain,
( cong(A,B,D,D)
| ~ eqangle(C,A,C,B,D,D,D,D)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_328]) ).
cnf(c_572,plain,
( para(sK5,sK6,A,B)
| ~ perp(sK6,sK3,A,B) ),
inference(resolve,[status(thm)],[c_274,c_181]) ).
cnf(c_584,plain,
perp(sK6,sK3,sK5,sK6),
inference(resolve,[status(thm)],[c_275,c_181]) ).
cnf(c_601,plain,
coll(sK5,sK2,sK6),
inference(resolve,[status(thm)],[c_281,c_182]) ).
cnf(c_603,plain,
coll(sK2,sK6,sK5),
inference(resolve,[status(thm)],[c_282,c_182]) ).
cnf(c_617,plain,
coll(sK6,sK6,sK2),
inference(resolve,[status(thm)],[c_336,c_182]) ).
cnf(c_656,plain,
coll(sK6,sK6,sK5),
inference(resolve,[status(thm)],[c_601,c_336]) ).
cnf(c_670,plain,
coll(sK5,sK6,sK2),
inference(resolve,[status(thm)],[c_601,c_282]) ).
cnf(c_732,plain,
coll(sK5,sK5,sK2),
inference(resolve,[status(thm)],[c_603,c_336]) ).
cnf(c_824,plain,
coll(sK6,sK2,sK6),
inference(resolve,[status(thm)],[c_617,c_282]) ).
cnf(c_925,plain,
coll(sK5,sK5,sK6),
inference(resolve,[status(thm)],[c_656,c_336]) ).
cnf(c_985,plain,
( midp(sK5,sK6,sK2)
| ~ cong(sK5,sK6,sK5,sK2) ),
inference(resolve,[status(thm)],[c_670,c_221]) ).
cnf(c_1090,plain,
coll(sK5,sK2,sK5),
inference(resolve,[status(thm)],[c_732,c_282]) ).
cnf(c_1309,plain,
( midp(sK6,sK2,sK6)
| ~ eqangle(A,sK2,A,sK6,sK0(A,sK2,sK6,B),sK2,sK0(A,sK2,sK6,B),sK6)
| ~ cyclic(A,sK2,sK6,B)
| ~ perp(A,sK6,sK6,sK2) ),
inference(resolve,[status(thm)],[c_824,c_142]) ).
cnf(c_1483,plain,
coll(sK5,sK6,sK5),
inference(resolve,[status(thm)],[c_925,c_282]) ).
cnf(c_1486,plain,
( cyclic(A,sK6,sK5,sK5)
| ~ eqangle(sK5,A,sK5,sK6,sK5,A,sK5,sK6) ),
inference(resolve,[status(thm)],[c_925,c_241]) ).
cnf(c_1666,plain,
coll(sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_1090,c_336]) ).
cnf(c_2094,plain,
coll(sK6,sK5,sK5),
inference(resolve,[status(thm)],[c_1483,c_281]) ).
cnf(c_2305,plain,
( midp(sK5,sK5,sK5)
| ~ cong(sK5,sK5,sK5,sK5) ),
inference(resolve,[status(thm)],[c_1666,c_221]) ).
cnf(c_2584,plain,
( midp(sK6,sK5,sK5)
| ~ cong(sK6,sK5,sK6,sK5) ),
inference(resolve,[status(thm)],[c_2094,c_221]) ).
cnf(c_2640,plain,
perp(sK6,sK3,sK6,sK5),
inference(resolve,[status(thm)],[c_584,c_276]) ).
cnf(c_6585,plain,
para(sK5,sK6,sK6,sK5),
inference(resolve,[status(thm)],[c_572,c_2640]) ).
cnf(c_6586,plain,
para(sK5,sK6,sK5,sK6),
inference(resolve,[status(thm)],[c_572,c_584]) ).
cnf(c_6595,plain,
para(sK6,sK5,sK5,sK6),
inference(resolve,[status(thm)],[c_6585,c_278]) ).
cnf(c_6625,plain,
( midp(A,sK6,sK6)
| ~ midp(A,sK5,sK5) ),
inference(resolve,[status(thm)],[c_6586,c_322]) ).
cnf(c_6628,plain,
eqangle(sK5,sK6,A,B,sK5,sK6,A,B),
inference(resolve,[status(thm)],[c_6586,c_244]) ).
cnf(c_6653,plain,
( para(sK6,sK5,A,B)
| ~ para(sK5,sK6,A,B) ),
inference(resolve,[status(thm)],[c_6595,c_277]) ).
cnf(c_6726,plain,
( cong(sK6,sK5,sK6,sK5)
| ~ cyclic(sK6,sK5,sK5,sK5)
| ~ cyclic(sK6,sK5,sK5,sK6) ),
inference(resolve,[status(thm)],[c_6628,c_330]) ).
cnf(c_6729,plain,
eqangle(A,B,sK5,sK6,A,B,sK5,sK6),
inference(resolve,[status(thm)],[c_6628,c_265]) ).
cnf(c_6732,plain,
( cong(sK6,A,sK6,A)
| ~ cyclic(sK6,A,sK5,sK5)
| ~ cyclic(sK6,A,sK5,A)
| ~ cyclic(sK6,A,sK5,sK6) ),
inference(resolve,[status(thm)],[c_6628,c_240]) ).
cnf(c_6740,plain,
cyclic(A,sK6,sK5,sK5),
inference(resolve,[status(thm)],[c_6729,c_1486]) ).
cnf(c_6743,plain,
cyclic(sK6,sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_6740,c_331]) ).
cnf(c_6751,plain,
cyclic(A,sK5,sK6,sK5),
inference(resolve,[status(thm)],[c_6740,c_269]) ).
cnf(c_6752,plain,
cyclic(sK6,A,sK5,sK5),
inference(resolve,[status(thm)],[c_6740,c_268]) ).
cnf(c_6779,plain,
( cong(sK6,sK5,sK6,sK5)
| ~ cyclic(sK6,sK5,sK5,sK6) ),
inference(resolve,[status(thm)],[c_6752,c_6726]) ).
cnf(c_6791,plain,
( cong(sK6,A,sK6,A)
| ~ cyclic(sK6,A,sK5,A)
| ~ cyclic(sK6,A,sK5,sK6) ),
inference(resolve,[status(thm)],[c_6752,c_6732]) ).
cnf(c_6793,plain,
cyclic(sK5,sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_6743,c_331]) ).
cnf(c_6801,plain,
( cyclic(sK5,sK5,A,sK5)
| ~ cyclic(sK6,sK5,sK5,A) ),
inference(resolve,[status(thm)],[c_6743,c_267]) ).
cnf(c_6853,plain,
cyclic(A,sK5,sK5,sK6),
inference(resolve,[status(thm)],[c_6751,c_270]) ).
cnf(c_6854,plain,
cyclic(sK5,A,sK6,sK5),
inference(resolve,[status(thm)],[c_6751,c_268]) ).
cnf(c_6882,plain,
cong(sK6,sK5,sK6,sK5),
inference(resolve,[status(thm)],[c_6853,c_6779]) ).
cnf(c_6908,plain,
midp(sK6,sK5,sK5),
inference(resolve,[status(thm)],[c_6882,c_2584]) ).
cnf(c_6912,plain,
midp(sK6,sK6,sK6),
inference(resolve,[status(thm)],[c_6908,c_6625]) ).
cnf(c_7016,plain,
( cong(A,sK6,A,sK6)
| ~ perp(A,sK6,sK6,sK6) ),
inference(resolve,[status(thm)],[c_6912,c_233]) ).
cnf(c_7020,plain,
cong(sK6,sK6,sK6,sK6),
inference(resolve,[status(thm)],[c_6912,c_220]) ).
cnf(c_7071,plain,
cyclic(A,sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_6752,c_331]) ).
cnf(c_7079,plain,
cyclic(sK6,sK5,A,sK5),
inference(resolve,[status(thm)],[c_6752,c_269]) ).
cnf(c_7105,plain,
( eqangle(sK6,B,sK6,A,sK5,sK6,sK5,A)
| ~ perp(sK0(sK6,A,sK5,sK5),sK6,sK6,B)
| ~ perp(sK6,sK5,sK5,A) ),
inference(resolve,[status(thm)],[c_6752,c_139]) ).
cnf(c_7106,plain,
( cong(sK5,sK5,sK5,sK5)
| ~ eqangle(sK5,sK5,sK5,sK5,sK5,sK5,sK5,sK5) ),
inference(resolve,[status(thm)],[c_6793,c_344]) ).
cnf(c_7114,plain,
eqangle(sK5,sK5,sK5,sK5,sK5,sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_6793,c_243]) ).
cnf(c_7136,plain,
cong(sK5,sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_7114,c_7106]) ).
cnf(c_7138,plain,
midp(sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_7136,c_2305]) ).
cnf(c_7139,plain,
midp(sK5,sK6,sK6),
inference(resolve,[status(thm)],[c_7138,c_6625]) ).
cnf(c_7187,plain,
para(sK5,sK5,sK6,sK6),
inference(resolve,[status(thm)],[c_7139,c_327]) ).
cnf(c_7206,plain,
cong(sK5,sK6,sK5,sK6),
inference(resolve,[status(thm)],[c_7139,c_220]) ).
cnf(c_7251,plain,
cyclic(sK5,sK5,sK6,sK6),
inference(resolve,[status(thm)],[c_6853,c_331]) ).
cnf(c_7259,plain,
cyclic(sK5,A,sK5,sK6),
inference(resolve,[status(thm)],[c_6853,c_268]) ).
cnf(c_7314,plain,
cyclic(sK5,sK6,A,sK5),
inference(resolve,[status(thm)],[c_6854,c_269]) ).
cnf(c_7316,plain,
( cyclic(A,sK6,sK5,B)
| ~ cyclic(sK5,A,sK6,B) ),
inference(resolve,[status(thm)],[c_6854,c_267]) ).
cnf(c_7361,plain,
( perp(sK6,sK5,sK5,A)
| ~ eqangle(sK5,A,sK5,sK5,sK5,sK5,sK5,sK5) ),
inference(resolve,[status(thm)],[c_6882,c_300]) ).
cnf(c_7409,plain,
( perp(sK5,sK6,sK6,A)
| ~ cyclic(sK6,sK6,sK5,A)
| ~ cong(sK6,A,sK6,A) ),
inference(resolve,[status(thm)],[c_6882,c_231]) ).
cnf(c_7612,plain,
( perp(A,sK6,sK6,sK6)
| ~ cyclic(sK6,sK6,A,sK6)
| ~ cong(sK6,A,sK6,A) ),
inference(resolve,[status(thm)],[c_7020,c_231]) ).
cnf(c_7669,plain,
( cong(A,sK5,sK5,sK5)
| ~ eqangle(sK5,A,sK5,sK5,sK5,sK5,sK5,sK5) ),
inference(resolve,[status(thm)],[c_7071,c_344]) ).
cnf(c_7676,plain,
( perp(sK5,A,A,sK5)
| ~ cong(A,sK5,sK5,sK5) ),
inference(resolve,[status(thm)],[c_7071,c_325]) ).
cnf(c_7677,plain,
cyclic(sK5,A,sK5,sK5),
inference(resolve,[status(thm)],[c_7071,c_268]) ).
cnf(c_7709,plain,
cyclic(sK6,sK5,sK5,A),
inference(resolve,[status(thm)],[c_7079,c_270]) ).
cnf(c_7741,plain,
cyclic(sK5,sK5,A,sK5),
inference(resolve,[status(thm)],[c_7709,c_6801]) ).
cnf(c_7768,plain,
( eqangle(sK5,A,sK5,sK5,sK5,sK5,sK5,sK5)
| ~ perp(sK5,sK5,sK5,A) ),
inference(resolve,[status(thm)],[c_7136,c_301]) ).
cnf(c_7867,plain,
( perp(sK5,sK5,A,B)
| ~ perp(sK6,sK6,A,B) ),
inference(resolve,[status(thm)],[c_7187,c_273]) ).
cnf(c_7905,plain,
( eqangle(sK6,A,sK6,sK6,sK6,sK6,sK6,sK6)
| ~ perp(sK5,sK6,sK6,A) ),
inference(resolve,[status(thm)],[c_7206,c_301]) ).
cnf(c_8036,plain,
cyclic(sK5,sK6,sK6,sK6),
inference(resolve,[status(thm)],[c_7251,c_331]) ).
cnf(c_8044,plain,
( cyclic(sK5,sK6,sK6,A)
| ~ cyclic(sK5,sK5,sK6,A) ),
inference(resolve,[status(thm)],[c_7251,c_267]) ).
cnf(c_8066,plain,
cyclic(sK5,sK5,A,sK6),
inference(resolve,[status(thm)],[c_7259,c_269]) ).
cnf(c_8103,plain,
cyclic(sK5,sK6,sK5,A),
inference(resolve,[status(thm)],[c_7314,c_270]) ).
cnf(c_8105,plain,
( cyclic(sK6,A,sK5,B)
| ~ cyclic(sK5,sK6,A,B) ),
inference(resolve,[status(thm)],[c_7314,c_267]) ).
cnf(c_8206,plain,
( cyclic(A,sK5,B,sK5)
| ~ cyclic(sK5,A,sK5,B) ),
inference(resolve,[status(thm)],[c_7677,c_267]) ).
cnf(c_26568,plain,
( cyclic(sK5,sK5,A,B)
| ~ cyclic(sK6,sK5,sK5,A) ),
inference(resolve,[status(thm)],[c_7709,c_267]) ).
cnf(c_8236,plain,
cyclic(sK5,sK5,A,B),
inference(resolve,[status(thm)],[c_7709,c_26568]) ).
cnf(c_8274,plain,
cyclic(sK5,sK6,sK6,A),
inference(resolve,[status(thm)],[c_8236,c_8044]) ).
cnf(c_26569,plain,
( cyclic(sK5,A,sK5,B)
| ~ cyclic(sK5,sK5,A,B) ),
inference(resolve,[status(thm)],[c_7741,c_267]) ).
cnf(c_8338,plain,
cyclic(sK5,A,sK5,B),
inference(resolve,[status(thm)],[c_8236,c_26569]) ).
cnf(c_8366,plain,
cyclic(A,sK5,B,sK5),
inference(resolve,[status(thm)],[c_8338,c_8206]) ).
cnf(c_26570,plain,
( cyclic(sK6,sK6,A,sK6)
| ~ cyclic(sK5,sK6,sK6,A) ),
inference(resolve,[status(thm)],[c_8036,c_267]) ).
cnf(c_8452,plain,
cyclic(sK6,sK6,A,sK6),
inference(resolve,[status(thm)],[c_8274,c_26570]) ).
cnf(c_8475,plain,
( perp(A,sK6,sK6,sK6)
| ~ cong(sK6,A,sK6,A) ),
inference(resolve,[status(thm)],[c_8452,c_7612]) ).
cnf(c_26571,plain,
( cyclic(sK5,A,B,sK6)
| ~ cyclic(sK5,sK5,A,B) ),
inference(resolve,[status(thm)],[c_8066,c_267]) ).
cnf(c_8532,plain,
cyclic(sK5,A,B,sK6),
inference(resolve,[status(thm)],[c_8236,c_26571]) ).
cnf(c_26572,plain,
( cyclic(sK5,A,sK6,B)
| ~ cyclic(sK5,sK5,A,B) ),
inference(resolve,[status(thm)],[c_8066,c_267]) ).
cnf(c_8533,plain,
cyclic(sK5,A,sK6,B),
inference(resolve,[status(thm)],[c_8236,c_26572]) ).
cnf(c_8562,plain,
cyclic(A,sK6,sK5,B),
inference(resolve,[status(thm)],[c_8533,c_7316]) ).
cnf(c_8584,plain,
( perp(sK5,sK6,sK6,A)
| ~ cong(sK6,A,sK6,A) ),
inference(resolve,[status(thm)],[c_8562,c_7409]) ).
cnf(c_26573,plain,
( cyclic(sK6,sK5,A,B)
| ~ cyclic(sK5,sK6,sK5,A) ),
inference(resolve,[status(thm)],[c_8103,c_267]) ).
cnf(c_8614,plain,
cyclic(sK6,sK5,A,B),
inference(resolve,[status(thm)],[c_8562,c_26573]) ).
cnf(c_26574,plain,
( cyclic(sK5,A,B,C)
| ~ cyclic(sK5,sK5,A,B) ),
inference(resolve,[status(thm)],[c_8236,c_267]) ).
cnf(c_8696,plain,
cyclic(sK5,A,B,C),
inference(resolve,[status(thm)],[c_8236,c_26574]) ).
cnf(c_8720,plain,
( eqangle(sK5,C,sK5,sK5,A,sK5,A,sK5)
| ~ perp(sK0(sK5,sK5,A,B),sK5,sK5,C)
| ~ perp(sK5,A,A,sK5) ),
inference(resolve,[status(thm)],[c_8236,c_139]) ).
cnf(c_8724,plain,
cyclic(sK6,A,sK5,B),
inference(resolve,[status(thm)],[c_8696,c_8105]) ).
cnf(c_26575,plain,
( cong(sK6,A,sK6,A)
| ~ cyclic(sK6,A,sK5,A) ),
inference(resolve,[status(thm)],[c_8724,c_6791]) ).
cnf(c_8730,plain,
cong(sK6,A,sK6,A),
inference(resolve,[status(thm)],[c_8724,c_26575]) ).
cnf(c_8756,plain,
perp(sK5,sK6,sK6,A),
inference(resolve,[status(thm)],[c_8730,c_8584]) ).
cnf(c_8757,plain,
perp(A,sK6,sK6,sK6),
inference(resolve,[status(thm)],[c_8730,c_8475]) ).
cnf(c_8807,plain,
eqangle(sK6,A,sK6,sK6,sK6,sK6,sK6,sK6),
inference(resolve,[status(thm)],[c_8756,c_7905]) ).
cnf(c_8820,plain,
cong(A,sK6,A,sK6),
inference(resolve,[status(thm)],[c_8757,c_7016]) ).
cnf(c_9910,plain,
eqangle(A,B,A,sK5,sK5,B,sK5,sK5),
inference(resolve,[status(thm)],[c_8366,c_243]) ).
cnf(c_26576,plain,
( cyclic(A,B,sK6,C)
| ~ cyclic(sK5,A,B,C) ),
inference(resolve,[status(thm)],[c_8532,c_267]) ).
cnf(c_10140,plain,
cyclic(A,B,sK6,C),
inference(resolve,[status(thm)],[c_8696,c_26576]) ).
cnf(c_10191,plain,
( midp(sK6,sK2,sK6)
| ~ eqangle(A,sK2,A,sK6,sK0(A,sK2,sK6,B),sK2,sK0(A,sK2,sK6,B),sK6)
| ~ perp(A,sK6,sK6,sK2) ),
inference(resolve,[status(thm)],[c_10140,c_1309]) ).
cnf(c_10355,plain,
( eqangle(sK6,B,A,B,A,B,A,sK5)
| ~ para(sK6,sK5,A,B) ),
inference(resolve,[status(thm)],[c_8614,c_234]) ).
cnf(c_26577,plain,
( cyclic(A,B,C,D)
| ~ cyclic(sK5,A,B,C) ),
inference(resolve,[status(thm)],[c_8696,c_267]) ).
cnf(c_10590,plain,
cyclic(A,B,C,D),
inference(resolve,[status(thm)],[c_8696,c_26577]) ).
cnf(c_10739,plain,
eqangle(A,B,A,C,D,B,D,C),
inference(resolve,[status(thm)],[c_10590,c_243]) ).
cnf(c_10798,plain,
( midp(sK6,sK2,sK6)
| ~ perp(A,sK6,sK6,sK2) ),
inference(resolve,[status(thm)],[c_10739,c_10191]) ).
cnf(c_26578,plain,
( perp(sK6,sK6,A,B)
| ~ cong(sK6,A,sK6,A) ),
inference(resolve,[status(thm)],[c_8730,c_232]) ).
cnf(c_11365,plain,
perp(sK6,sK6,A,B),
inference(resolve,[status(thm)],[c_8730,c_26578]) ).
cnf(c_11408,plain,
perp(sK5,sK5,A,B),
inference(resolve,[status(thm)],[c_11365,c_7867]) ).
cnf(c_11809,plain,
eqangle(sK5,A,sK5,sK5,sK5,sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_11408,c_7768]) ).
cnf(c_11828,plain,
cong(A,sK5,sK5,sK5),
inference(resolve,[status(thm)],[c_11809,c_7669]) ).
cnf(c_11829,plain,
perp(sK6,sK5,sK5,A),
inference(resolve,[status(thm)],[c_11809,c_7361]) ).
cnf(c_11832,plain,
perp(sK5,A,A,sK5),
inference(resolve,[status(thm)],[c_11828,c_7676]) ).
cnf(c_11836,plain,
( eqangle(sK6,B,sK6,A,sK5,sK6,sK5,A)
| ~ perp(sK0(sK6,A,sK5,sK5),sK6,sK6,B) ),
inference(resolve,[status(thm)],[c_11829,c_7105]) ).
cnf(c_11849,plain,
( eqangle(sK5,C,sK5,sK5,A,sK5,A,sK5)
| ~ perp(sK0(sK5,sK5,A,B),sK5,sK5,C) ),
inference(resolve,[status(thm)],[c_11832,c_8720]) ).
cnf(c_26579,plain,
( para(C,sK6,A,B)
| ~ perp(sK6,sK6,A,B) ),
inference(resolve,[status(thm)],[c_8757,c_274]) ).
cnf(c_12075,plain,
para(A,sK6,B,C),
inference(resolve,[status(thm)],[c_11365,c_26579]) ).
cnf(c_12166,plain,
para(sK6,sK5,A,B),
inference(resolve,[status(thm)],[c_12075,c_6653]) ).
cnf(c_12591,plain,
eqangle(sK6,A,B,A,B,A,B,sK5),
inference(resolve,[status(thm)],[c_12166,c_10355]) ).
cnf(c_26580,plain,
( perp(B,sK6,sK6,A)
| ~ eqangle(sK6,A,sK6,sK6,sK6,sK6,sK6,sK6) ),
inference(resolve,[status(thm)],[c_8820,c_300]) ).
cnf(c_12828,plain,
perp(A,sK6,sK6,B),
inference(resolve,[status(thm)],[c_8807,c_26580]) ).
cnf(c_12890,plain,
eqangle(sK6,A,sK6,B,sK5,sK6,sK5,B),
inference(resolve,[status(thm)],[c_12828,c_11836]) ).
cnf(c_12896,plain,
midp(sK6,sK2,sK6),
inference(resolve,[status(thm)],[c_12828,c_10798]) ).
cnf(c_12971,plain,
midp(sK6,sK6,sK2),
inference(resolve,[status(thm)],[c_12896,c_272]) ).
cnf(c_26581,plain,
( cong(A,sK6,A,sK2)
| ~ perp(A,sK6,sK6,sK2) ),
inference(resolve,[status(thm)],[c_12971,c_233]) ).
cnf(c_13072,plain,
cong(A,sK6,A,sK2),
inference(resolve,[status(thm)],[c_12828,c_26581]) ).
cnf(c_13074,plain,
( midp(sK6,A,B)
| ~ para(sK6,B,sK2,A)
| ~ para(sK6,A,sK2,B) ),
inference(resolve,[status(thm)],[c_12971,c_224]) ).
cnf(c_13095,plain,
midp(sK5,sK6,sK2),
inference(resolve,[status(thm)],[c_13072,c_985]) ).
cnf(c_13529,plain,
midp(sK5,sK2,sK6),
inference(resolve,[status(thm)],[c_13095,c_272]) ).
cnf(c_13532,plain,
( midp(A,sK6,B)
| ~ coll(A,sK6,B)
| ~ para(sK5,A,sK2,B) ),
inference(resolve,[status(thm)],[c_13095,c_238]) ).
cnf(c_13916,plain,
( midp(A,sK2,B)
| ~ coll(A,sK2,B)
| ~ para(sK5,A,sK6,B) ),
inference(resolve,[status(thm)],[c_13529,c_238]) ).
cnf(c_16139,plain,
perp(A,B,sK6,sK6),
inference(resolve,[status(thm)],[c_11365,c_275]) ).
cnf(c_26582,plain,
( para(A,B,C,D)
| ~ perp(A,B,sK6,sK6) ),
inference(resolve,[status(thm)],[c_11365,c_274]) ).
cnf(c_16140,plain,
para(A,B,C,D),
inference(resolve,[status(thm)],[c_16139,c_26582]) ).
cnf(c_26583,plain,
( perp(A,B,C,D)
| ~ para(A,B,sK6,sK6) ),
inference(resolve,[status(thm)],[c_11365,c_273]) ).
cnf(c_16141,plain,
perp(A,B,C,D),
inference(resolve,[status(thm)],[c_16140,c_26583]) ).
cnf(c_16200,plain,
( midp(A,sK2,B)
| ~ coll(A,sK2,B) ),
inference(resolve,[status(thm)],[c_16140,c_13916]) ).
cnf(c_16230,plain,
( midp(A,sK6,B)
| ~ coll(A,sK6,B) ),
inference(resolve,[status(thm)],[c_16140,c_13532]) ).
cnf(c_26584,plain,
( midp(sK6,B,A)
| ~ para(sK6,A,sK2,B) ),
inference(resolve,[status(thm)],[c_16140,c_13074]) ).
cnf(c_16255,plain,
midp(sK6,A,B),
inference(resolve,[status(thm)],[c_16140,c_26584]) ).
cnf(c_18246,plain,
( midp(A,D,D)
| ~ midp(A,B,C) ),
inference(resolve,[status(thm)],[c_16140,c_322]) ).
cnf(c_18256,plain,
eqangle(A,B,C,D,E,F,C,D),
inference(resolve,[status(thm)],[c_16140,c_244]) ).
cnf(c_26585,plain,
( midp(A,E,D)
| ~ para(B,D,C,E)
| ~ midp(A,B,C) ),
inference(resolve,[status(thm)],[c_16140,c_224]) ).
cnf(c_18258,plain,
( midp(A,D,E)
| ~ midp(A,B,C) ),
inference(resolve,[status(thm)],[c_16140,c_26585]) ).
cnf(c_18260,plain,
coll(A,B,C),
inference(resolve,[status(thm)],[c_16140,c_222]) ).
cnf(c_18369,plain,
eqangle(sK5,A,sK5,sK5,B,sK5,B,sK5),
inference(resolve,[status(thm)],[c_16141,c_11849]) ).
cnf(c_18482,plain,
midp(A,sK6,B),
inference(resolve,[status(thm)],[c_18260,c_16230]) ).
cnf(c_18485,plain,
midp(A,sK2,B),
inference(resolve,[status(thm)],[c_18260,c_16200]) ).
cnf(c_18957,plain,
cong(sK6,A,sK6,B),
inference(resolve,[status(thm)],[c_16255,c_220]) ).
cnf(c_19148,plain,
cong(A,sK6,A,B),
inference(resolve,[status(thm)],[c_18482,c_220]) ).
cnf(c_19299,plain,
midp(A,B,sK2),
inference(resolve,[status(thm)],[c_18485,c_272]) ).
cnf(c_22295,plain,
cong(sK6,A,B,sK6),
inference(resolve,[status(thm)],[c_18957,c_261]) ).
cnf(c_26586,plain,
( ~ cong(sK6,D,sK6,B)
| eqangle(D,B,D,C,sK6,B,sK6,A)
| ~ midp(A,B,C) ),
inference(resolve,[status(thm)],[c_18957,c_174]) ).
cnf(c_22301,plain,
( eqangle(D,B,D,C,sK6,B,sK6,A)
| ~ midp(A,B,C) ),
inference(resolve,[status(thm)],[c_18957,c_26586]) ).
cnf(c_22334,plain,
eqangle(A,sK6,sK6,B,sK6,B,A,B),
inference(resolve,[status(thm)],[c_19148,c_237]) ).
cnf(c_26587,plain,
( ~ cong(sK6,C,sK6,B)
| eqangle(C,sK6,C,B,sK6,sK6,sK6,A)
| ~ midp(A,sK6,B) ),
inference(resolve,[status(thm)],[c_22295,c_174]) ).
cnf(c_26588,plain,
( ~ cong(sK6,A,sK6,B)
| eqangle(A,sK6,A,B,sK6,sK6,sK6,C) ),
inference(resolve,[status(thm)],[c_18482,c_26587]) ).
cnf(c_23116,plain,
eqangle(A,sK6,A,B,sK6,sK6,sK6,C),
inference(resolve,[status(thm)],[c_18957,c_26588]) ).
cnf(c_23463,plain,
midp(A,B,B),
inference(resolve,[status(thm)],[c_18246,c_19299]) ).
cnf(c_23527,plain,
midp(A,B,C),
inference(resolve,[status(thm)],[c_18258,c_23463]) ).
cnf(c_23537,plain,
eqangle(A,B,A,C,sK6,B,sK6,D),
inference(resolve,[status(thm)],[c_23527,c_22301]) ).
cnf(c_24030,plain,
( eqangle(F,A,F,sK5,B,C,D,E)
| ~ eqangle(sK5,A,sK5,sK5,B,C,D,E) ),
inference(resolve,[status(thm)],[c_9910,c_262]) ).
cnf(c_24083,plain,
eqangle(A,B,B,C,D,A,D,C),
inference(resolve,[status(thm)],[c_10739,c_266]) ).
cnf(c_24159,plain,
( eqangle(sK6,B,A,B,C,D,E,F)
| ~ eqangle(A,B,A,sK5,C,D,E,F) ),
inference(resolve,[status(thm)],[c_12591,c_262]) ).
cnf(c_24168,plain,
( eqangle(sK6,F,sK6,A,B,C,D,E)
| ~ eqangle(sK5,sK6,sK5,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_12890,c_262]) ).
cnf(c_24382,plain,
eqangle(A,B,C,D,A,B,E,F),
inference(resolve,[status(thm)],[c_18256,c_265]) ).
cnf(c_24421,plain,
( eqangle(sK5,F,sK5,sK5,B,C,D,E)
| ~ eqangle(A,sK5,A,sK5,B,C,D,E) ),
inference(resolve,[status(thm)],[c_18369,c_262]) ).
cnf(c_25143,plain,
( eqangle(B,sK6,sK6,A,C,D,E,F)
| ~ eqangle(sK6,A,B,A,C,D,E,F) ),
inference(resolve,[status(thm)],[c_22334,c_262]) ).
cnf(c_25199,plain,
( eqangle(F,sK6,F,V6,B,C,D,E)
| ~ eqangle(sK6,sK6,sK6,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_23116,c_262]) ).
cnf(c_25251,plain,
( eqangle(V6,A,V6,V7,C,D,E,F)
| ~ eqangle(sK6,A,sK6,B,C,D,E,F) ),
inference(resolve,[status(thm)],[c_23537,c_262]) ).
cnf(c_26016,plain,
( eqangle(B,V7,V7,C,D,E,F,V6)
| ~ eqangle(A,B,A,C,D,E,F,V6) ),
inference(resolve,[status(thm)],[c_24083,c_262]) ).
cnf(c_26493,plain,
eqangle(A,B,A,B,C,D,E,F),
inference(resolve,[status(thm)],[c_24382,c_263]) ).
cnf(c_26511,plain,
eqangle(sK5,A,sK5,sK5,B,C,D,E),
inference(resolve,[status(thm)],[c_26493,c_24421]) ).
cnf(c_26527,plain,
eqangle(A,B,A,sK5,C,D,E,F),
inference(resolve,[status(thm)],[c_26511,c_24030]) ).
cnf(c_26548,plain,
eqangle(sK6,A,B,A,C,D,E,F),
inference(resolve,[status(thm)],[c_26527,c_24159]) ).
cnf(c_26559,plain,
eqangle(A,sK6,sK6,B,C,D,E,F),
inference(resolve,[status(thm)],[c_26548,c_25143]) ).
cnf(c_26561,plain,
eqangle(A,sK6,A,B,C,D,E,F),
inference(resolve,[status(thm)],[c_26559,c_25199]) ).
cnf(c_26562,plain,
eqangle(sK6,A,sK6,B,C,D,E,F),
inference(resolve,[status(thm)],[c_26561,c_24168]) ).
cnf(c_26563,plain,
eqangle(A,B,A,C,D,E,F,V6),
inference(resolve,[status(thm)],[c_26562,c_25251]) ).
cnf(c_26566,plain,
eqangle(A,B,B,C,D,E,F,V6),
inference(resolve,[status(thm)],[c_26563,c_26016]) ).
cnf(c_26567,plain,
$false,
inference(resolve,[status(thm)],[c_26566,c_177]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO571+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.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.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 13:42:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.37 % Process 1718165 was started by sandbox2 on n009,
% 0.13/0.37 % Fri Sep 25 13:42:14 2026
% 0.13/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.39
% 0.13/0.39 % From the command line: assign(max_seconds, 300).
% 35.34/5.02
% 35.34/5.02 % given #500 (A,wt=36): 386 -cyclic(c3,c7,c5,A) | -midp(B,c7,c5) | eqangle(c3,c7,c3,c5,f16(c3,c7,c5,A),c7,f16(c3,c7,c5,A),B). [resolve(181,a,141,a)].
% 35.34/5.02
% 35.34/5.02 % given #1000 (T,wt=9): 11871 midp(c3,c1,c1). [back_unit_del(5849),unit_del(a,11848)].
% 35.34/5.02
% 35.34/5.02 % given #1500 (W,wt=10): 22385 cong(c7,A,A,c1). [resolve(19281,a,261,a)].
% 35.34/5.02
% 35.34/5.02 % given #2000 (T,wt=14): 20036 eqangle(c1,c6,c6,c5,c6,c5,c1,c5). [resolve(13826,a,237,a)].
% 35.34/5.02
% 35.34/5.02 % given #2500 (W,wt=14): 23972 eqratio(c3,c6,c3,c6,c6,c5,c6,c5). [resolve(9389,a,255,a)].
% 35.34/5.02
% 35.34/5.02 % SZS status Theorem for theBenchmark
% 35.34/5.02
% 35.34/5.02 % Proof 1 at 3.48 (+ 1.07) seconds.
% 35.34/5.02 % Length of proof is 264.
% 35.34/5.02 % Level of proof is 33.
% 35.34/5.02 % Maximum clause weight is 45.000.
% 35.34/5.02 % Given clauses 2839.
% 35.34/5.02
% 35.34/5.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------