%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO613+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:13 AM UTC 2026
% Result : Theorem 160.04s 21.87s
% Output : CNFRefutation 160.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 45
% Syntax : Number of formulae : 427 ( 216 unt; 0 def)
% Number of atoms : 773 ( 0 equ)
% Maximal formula atoms : 11 ( 1 avg)
% Number of connectives : 583 ( 237 ~; 233 |; 67 &)
% ( 0 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 17 ( 17 usr; 16 con; 0-4 aty)
% Number of variables : 849 ( 140 sgn 246 !; 18 ?)
% 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(ruleD4,axiom,
! [A,B,C,D] :
( para(A,B,C,D)
=> para(A,B,D,C) ),
file('theBenchmark.p',ruleD4) ).
fof(ruleD5,axiom,
! [A,B,C,D] :
( para(A,B,C,D)
=> para(C,D,A,B) ),
file('theBenchmark.p',ruleD5) ).
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(ruleD13,axiom,
! [A,B,C,D,O] :
( ( cong(O,A,O,D)
& cong(O,A,O,C)
& cong(O,A,O,B) )
=> cyclic(A,B,C,D) ),
file('theBenchmark.p',ruleD13) ).
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(ruleD24,axiom,
! [A,B,C,D] :
( cong(A,B,C,D)
=> cong(C,D,A,B) ),
file('theBenchmark.p',ruleD24) ).
fof(ruleD39,axiom,
! [A,B,C,D,P,Q] :
( eqangle(A,B,P,Q,C,D,P,Q)
=> para(A,B,C,D) ),
file('theBenchmark.p',ruleD39) ).
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(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(ruleD53,axiom,
! [A,B,C,O] :
( ( coll(O,A,C)
& circle(O,A,B,C) )
=> perp(A,B,B,C) ),
file('theBenchmark.p',ruleD53) ).
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(ruleD63,axiom,
! [A,B,C,D,M] :
( ( midp(M,C,D)
& midp(M,A,B) )
=> para(A,C,B,D) ),
file('theBenchmark.p',ruleD63) ).
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(ruleD69,axiom,
! [A,B,C] :
( midp(A,B,C)
=> coll(A,B,C) ),
file('theBenchmark.p',ruleD69) ).
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(exemplo6GDDFULL618075y,conjecture,
! [A,B,C,D,E,F,G,H,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6,NWPNT7,NWPNT8] :
( ( coll(H,C,G)
& coll(H,A,F)
& coll(G,B,F)
& circle(C,B,G,NWPNT8)
& circle(A,B,F,NWPNT7)
& midp(E,D,B)
& circle(C,B,D,NWPNT6)
& circle(A,B,D,NWPNT5)
& circle(C,B,NWPNT3,NWPNT4)
& circle(A,B,NWPNT1,NWPNT2) )
=> eqangle(F,D,D,G,A,H,H,C) ),
file('theBenchmark.p',exemplo6GDDFULL618075y) ).
fof(exemplo6GDDFULL618075y_neg,negated_conjecture,
~ ! [A,B,C,D,E,F,G,H,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6,NWPNT7,NWPNT8] :
( ( coll(H,C,G)
& coll(H,A,F)
& coll(G,B,F)
& circle(C,B,G,NWPNT8)
& circle(A,B,F,NWPNT7)
& midp(E,D,B)
& circle(C,B,D,NWPNT6)
& circle(A,B,D,NWPNT5)
& circle(C,B,NWPNT3,NWPNT4)
& circle(A,B,NWPNT1,NWPNT2) )
=> eqangle(F,D,D,G,A,H,H,C) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL618075y]) ).
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_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]) ).
cnf(c_101,plain,
( perp(B,C,C,D)
| ~ coll(A,B,D)
| ~ circle(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD53]) ).
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_199,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_232,plain,
( ~ cong(A,B,A,C)
| ~ cong(A,B,A,D)
| perp(B,D,D,C)
| ~ coll(A,B,C) ),
inference(resolve,[status(thm)],[c_101,c_97]) ).
cnf(c_233,plain,
( ~ cong(E,D,E,C)
| ~ cong(E,D,E,B)
| midp(A,B,C)
| ~ eqangle(D,B,D,C,E,B,E,A)
| ~ coll(A,B,C) ),
inference(resolve,[status(thm)],[c_100,c_97]) ).
fof(nnf_95,plain,
? [A,B,C,D,E,F,G,H,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6,NWPNT7,NWPNT8] :
( ~ eqangle(F,D,D,G,A,H,H,C)
& coll(H,C,G)
& coll(H,A,F)
& coll(G,B,F)
& circle(C,B,G,NWPNT8)
& circle(A,B,F,NWPNT7)
& midp(E,D,B)
& circle(C,B,D,NWPNT6)
& circle(A,B,D,NWPNT5)
& circle(C,B,NWPNT3,NWPNT4)
& circle(A,B,NWPNT1,NWPNT2) ),
inference(fof_nnf,[status(thm)],[exemplo6GDDFULL618075y_neg]) ).
fof(sk_exemplo6GDDFULL618075y_neg,plain,
( ~ eqangle(sK1,sK2,sK2,sK3,sK4,sK5,sK5,sK6)
& coll(sK5,sK6,sK3)
& coll(sK5,sK4,sK1)
& coll(sK3,sK8,sK1)
& circle(sK6,sK8,sK3,sK16)
& circle(sK4,sK8,sK1,sK15)
& midp(sK7,sK2,sK8)
& circle(sK6,sK8,sK2,sK14)
& circle(sK4,sK8,sK2,sK13)
& circle(sK6,sK8,sK11,sK12)
& circle(sK4,sK8,sK9,sK10) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK8,sK9,sK10,sK6,sK11,sK12,sK2,sK13,sK14,sK7,sK1,sK15,sK3,sK16,sK5]),skolemize(A,sK4),skolemize(B,sK8),skolemize(C,sK6),skolemize(D,sK2),skolemize(E,sK7),skolemize(F,sK1),skolemize(G,sK3),skolemize(H,sK5),skolemize(NWPNT1,sK9),skolemize(NWPNT2,sK10),skolemize(NWPNT3,sK11),skolemize(NWPNT4,sK12),skolemize(NWPNT5,sK13),skolemize(NWPNT6,sK14),skolemize(NWPNT7,sK15),skolemize(NWPNT8,sK16)],[nnf_95]) ).
cnf(c_237,negated_conjecture,
~ eqangle(sK1,sK2,sK2,sK3,sK4,sK5,sK5,sK6),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL618075y_neg]) ).
cnf(c_241,negated_conjecture,
midp(sK7,sK2,sK8),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL618075y_neg]) ).
cnf(c_277,plain,
( coll(A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD69]) ).
cnf(c_278,plain,
( cong(A,B,A,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD68]) ).
cnf(c_279,plain,
( midp(A,B,C)
| ~ coll(A,B,C)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD67]) ).
cnf(c_280,plain,
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD66]) ).
cnf(c_282,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_283,plain,
( para(B,D,C,E)
| ~ midp(A,D,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD63]) ).
cnf(c_289,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_290,plain,
( perp(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD56]) ).
cnf(c_291,plain,
( cong(D,B,D,C)
| ~ perp(D,A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD55]) ).
cnf(c_292,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_295,plain,
( eqangle(A,B,B,C,B,C,A,C)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD46]) ).
cnf(c_296,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_297,plain,
( para(A,D,C,E)
| ~ midp(D,B,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD44]) ).
cnf(c_298,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_299,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_301,plain,
( eqangle(C,A,C,B,D,A,D,B)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD41]) ).
cnf(c_302,plain,
( eqangle(A,B,E,F,C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD40]) ).
cnf(c_303,plain,
( para(A,B,E,F)
| ~ eqangle(A,B,C,D,E,F,C,D) ),
inference(clausify,[status(thm)],[ruleD39]) ).
cnf(c_318,plain,
( cong(C,D,A,B)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD24]) ).
cnf(c_319,plain,
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD23]) ).
cnf(c_320,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_321,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_323,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_324,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_325,plain,
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD17]) ).
cnf(c_326,plain,
( cyclic(B,A,C,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD16]) ).
cnf(c_327,plain,
( cyclic(A,C,B,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD15]) ).
cnf(c_328,plain,
( cyclic(A,B,D,C)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD14]) ).
cnf(c_329,plain,
( cyclic(B,C,D,E)
| ~ cong(A,B,A,E)
| ~ cong(A,B,A,D)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD13]) ).
cnf(c_330,plain,
( midp(A,C,B)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD11]) ).
cnf(c_331,plain,
( perp(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD10]) ).
cnf(c_332,plain,
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD9]) ).
cnf(c_333,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD8]) ).
cnf(c_334,plain,
( perp(A,B,D,C)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD7]) ).
cnf(c_336,plain,
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD5]) ).
cnf(c_337,plain,
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD4]) ).
cnf(c_338,plain,
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD3]) ).
cnf(c_339,plain,
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD2]) ).
cnf(c_340,plain,
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD1]) ).
cnf(c_355,plain,
( ~ cong(A,B,A,C)
| perp(B,C,C,C)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_232]) ).
cnf(c_380,plain,
( midp(A,D,D)
| ~ para(B,D,C,D)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_282]) ).
cnf(c_383,plain,
( perp(B,A,A,B)
| ~ cyclic(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_289]) ).
cnf(c_384,plain,
( perp(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_290]) ).
cnf(c_385,plain,
( para(A,A,C,C)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_297]) ).
cnf(c_387,plain,
( cong(A,B,D,E)
| ~ eqangle(C,A,C,B,D,D,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_298]) ).
cnf(c_388,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_298]) ).
cnf(c_389,plain,
( cyclic(B,C,D,D)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_325]) ).
cnf(c_390,plain,
( cyclic(B,C,C,D)
| ~ cong(A,B,A,D)
| ~ cong(A,B,A,C) ),
inference(factor,[status(thm)],[c_329]) ).
cnf(c_393,plain,
( para(A,B,A,B)
| ~ perp(A,B,A,B) ),
inference(factor,[status(thm)],[c_332]) ).
cnf(c_394,plain,
( coll(C,C,A)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_338]) ).
cnf(c_403,plain,
( cyclic(B,C,C,C)
| ~ cong(A,B,A,C) ),
inference(factor,[status(thm)],[c_390]) ).
cnf(c_529,plain,
coll(sK7,sK2,sK8),
inference(resolve,[status(thm)],[c_277,c_241]) ).
cnf(c_530,plain,
cong(sK7,sK2,sK7,sK8),
inference(resolve,[status(thm)],[c_278,c_241]) ).
cnf(c_531,plain,
( para(sK2,A,sK8,B)
| ~ midp(sK7,A,B) ),
inference(resolve,[status(thm)],[c_283,c_241]) ).
cnf(c_532,plain,
( para(A,sK2,B,sK8)
| ~ midp(sK7,A,B) ),
inference(resolve,[status(thm)],[c_283,c_241]) ).
cnf(c_545,plain,
( para(sK7,A,sK8,B)
| ~ midp(A,sK2,B) ),
inference(resolve,[status(thm)],[c_297,c_241]) ).
cnf(c_546,plain,
( para(A,sK7,B,sK8)
| ~ midp(A,sK2,B) ),
inference(resolve,[status(thm)],[c_297,c_241]) ).
cnf(c_547,plain,
midp(sK7,sK8,sK2),
inference(resolve,[status(thm)],[c_330,c_241]) ).
cnf(c_594,plain,
coll(sK8,sK8,sK7),
inference(resolve,[status(thm)],[c_529,c_394]) ).
cnf(c_595,plain,
coll(sK7,sK8,sK2),
inference(resolve,[status(thm)],[c_529,c_340]) ).
cnf(c_596,plain,
coll(sK2,sK7,sK8),
inference(resolve,[status(thm)],[c_529,c_339]) ).
cnf(c_607,plain,
( para(A,sK7,B,sK2)
| ~ midp(A,sK8,B) ),
inference(resolve,[status(thm)],[c_547,c_297]) ).
cnf(c_608,plain,
( para(sK7,A,sK2,B)
| ~ midp(A,sK8,B) ),
inference(resolve,[status(thm)],[c_547,c_297]) ).
cnf(c_611,plain,
cong(sK7,sK8,sK7,sK2),
inference(resolve,[status(thm)],[c_547,c_278]) ).
cnf(c_658,plain,
coll(sK7,sK7,sK8),
inference(resolve,[status(thm)],[c_594,c_394]) ).
cnf(c_659,plain,
coll(sK8,sK7,sK8),
inference(resolve,[status(thm)],[c_594,c_340]) ).
cnf(c_661,plain,
( coll(sK7,A,sK8)
| ~ coll(sK8,sK8,A) ),
inference(resolve,[status(thm)],[c_594,c_338]) ).
cnf(c_662,plain,
coll(sK2,sK2,sK7),
inference(resolve,[status(thm)],[c_595,c_394]) ).
cnf(c_663,plain,
coll(sK8,sK7,sK2),
inference(resolve,[status(thm)],[c_595,c_339]) ).
cnf(c_666,plain,
coll(sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_596,c_394]) ).
cnf(c_730,plain,
coll(sK7,sK8,sK7),
inference(resolve,[status(thm)],[c_658,c_340]) ).
cnf(c_733,plain,
coll(sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_659,c_394]) ).
cnf(c_734,plain,
coll(sK7,sK8,sK8),
inference(resolve,[status(thm)],[c_659,c_339]) ).
cnf(c_737,plain,
coll(sK7,sK7,sK2),
inference(resolve,[status(thm)],[c_662,c_394]) ).
cnf(c_741,plain,
coll(sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_663,c_394]) ).
cnf(c_746,plain,
coll(sK8,sK2,sK8),
inference(resolve,[status(thm)],[c_666,c_340]) ).
cnf(c_815,plain,
coll(sK8,sK7,sK7),
inference(resolve,[status(thm)],[c_730,c_339]) ).
cnf(c_821,plain,
coll(sK7,sK2,sK7),
inference(resolve,[status(thm)],[c_737,c_340]) ).
cnf(c_834,plain,
coll(sK2,sK8,sK8),
inference(resolve,[status(thm)],[c_746,c_339]) ).
cnf(c_879,plain,
coll(sK2,sK7,sK7),
inference(resolve,[status(thm)],[c_821,c_339]) ).
cnf(c_906,plain,
cyclic(sK2,sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_530,c_403]) ).
cnf(c_22907,plain,
( perp(sK2,sK8,sK8,sK8)
| ~ coll(sK7,sK2,sK8) ),
inference(resolve,[status(thm)],[c_530,c_355]) ).
cnf(c_922,plain,
perp(sK2,sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_529,c_22907]) ).
cnf(c_1043,plain,
cyclic(sK8,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_611,c_403]) ).
cnf(c_22908,plain,
( perp(sK8,sK2,sK2,sK2)
| ~ coll(sK7,sK8,sK2) ),
inference(resolve,[status(thm)],[c_611,c_355]) ).
cnf(c_1059,plain,
perp(sK8,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_595,c_22908]) ).
cnf(c_1100,plain,
cong(sK7,sK8,sK2,sK7),
inference(resolve,[status(thm)],[c_611,c_319]) ).
cnf(c_1136,plain,
cyclic(sK8,sK2,sK8,sK8),
inference(resolve,[status(thm)],[c_906,c_326]) ).
cnf(c_1139,plain,
eqangle(sK8,sK2,sK8,sK8,sK8,sK2,sK8,sK8),
inference(resolve,[status(thm)],[c_906,c_301]) ).
cnf(c_1155,plain,
perp(sK8,sK8,sK2,sK8),
inference(resolve,[status(thm)],[c_922,c_333]) ).
cnf(c_1208,plain,
cyclic(sK2,sK8,sK2,sK2),
inference(resolve,[status(thm)],[c_1043,c_326]) ).
cnf(c_1231,plain,
( cong(sK8,sK2,sK8,sK2)
| ~ midp(sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_1059,c_291]) ).
cnf(c_1249,plain,
cong(sK2,sK7,sK7,sK8),
inference(resolve,[status(thm)],[c_1100,c_318]) ).
cnf(c_1270,plain,
cyclic(sK8,sK8,sK2,sK8),
inference(resolve,[status(thm)],[c_1136,c_327]) ).
cnf(c_1290,plain,
perp(sK8,sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_1155,c_334]) ).
cnf(c_1324,plain,
cyclic(sK2,sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_1208,c_327]) ).
cnf(c_1357,plain,
cong(sK2,sK7,sK8,sK7),
inference(resolve,[status(thm)],[c_1249,c_319]) ).
cnf(c_1360,plain,
cyclic(sK8,sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_1270,c_328]) ).
cnf(c_1382,plain,
perp(sK8,sK2,sK8,sK8),
inference(resolve,[status(thm)],[c_1290,c_333]) ).
cnf(c_1403,plain,
cyclic(sK2,sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_1324,c_328]) ).
cnf(c_1441,plain,
perp(sK2,sK8,sK7,sK7),
inference(resolve,[status(thm)],[c_1357,c_384]) ).
cnf(c_1446,plain,
cyclic(sK8,sK8,sK2,sK2),
inference(resolve,[status(thm)],[c_1360,c_389]) ).
cnf(c_1473,plain,
( cong(sK8,sK8,sK8,sK8)
| ~ midp(sK2,sK8,sK8) ),
inference(resolve,[status(thm)],[c_1382,c_291]) ).
cnf(c_1492,plain,
cyclic(sK2,sK2,sK8,sK8),
inference(resolve,[status(thm)],[c_1403,c_389]) ).
cnf(c_1527,plain,
( cong(sK2,sK7,sK2,sK7)
| ~ midp(sK8,sK7,sK7) ),
inference(resolve,[status(thm)],[c_1441,c_291]) ).
cnf(c_1538,plain,
( perp(sK2,sK8,sK8,sK2)
| ~ cong(sK8,sK2,sK8,sK2) ),
inference(resolve,[status(thm)],[c_1446,c_383]) ).
cnf(c_1539,plain,
cyclic(sK8,sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_1446,c_327]) ).
cnf(c_1570,plain,
( perp(sK8,sK2,sK2,sK8)
| ~ cong(sK2,sK8,sK2,sK8) ),
inference(resolve,[status(thm)],[c_1492,c_383]) ).
cnf(c_1603,plain,
cyclic(sK2,sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_1539,c_326]) ).
cnf(c_2902,plain,
para(sK2,sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_531,c_547]) ).
cnf(c_2915,plain,
para(sK2,sK8,sK2,sK8),
inference(resolve,[status(thm)],[c_2902,c_337]) ).
cnf(c_2916,plain,
para(sK8,sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_2902,c_336]) ).
cnf(c_2918,plain,
( perp(sK2,sK8,A,B)
| ~ perp(sK8,sK2,A,B) ),
inference(resolve,[status(thm)],[c_2902,c_331]) ).
cnf(c_2947,plain,
eqangle(sK2,sK8,A,B,sK2,sK8,A,B),
inference(resolve,[status(thm)],[c_2915,c_302]) ).
cnf(c_2960,plain,
para(sK8,sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_2916,c_337]) ).
cnf(c_2980,plain,
( midp(A,sK2,sK2)
| ~ midp(A,sK8,sK8) ),
inference(resolve,[status(thm)],[c_2960,c_380]) ).
cnf(c_2983,plain,
eqangle(sK8,sK2,A,B,sK8,sK2,A,B),
inference(resolve,[status(thm)],[c_2960,c_302]) ).
cnf(c_22909,plain,
( cong(sK2,sK8,sK2,sK8)
| ~ cyclic(sK2,sK8,sK8,sK8)
| ~ cyclic(sK2,sK8,sK8,sK2) ),
inference(resolve,[status(thm)],[c_1139,c_388]) ).
cnf(c_22910,plain,
( cong(sK2,sK8,sK2,sK8)
| ~ cyclic(sK2,sK8,sK8,sK8) ),
inference(resolve,[status(thm)],[c_1603,c_22909]) ).
cnf(c_3028,plain,
cong(sK2,sK8,sK2,sK8),
inference(resolve,[status(thm)],[c_906,c_22910]) ).
cnf(c_3031,plain,
perp(sK8,sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_3028,c_1570]) ).
cnf(c_22911,plain,
( midp(sK2,sK8,sK8)
| ~ coll(sK2,sK8,sK8) ),
inference(resolve,[status(thm)],[c_3028,c_279]) ).
cnf(c_3109,plain,
midp(sK2,sK8,sK8),
inference(resolve,[status(thm)],[c_834,c_22911]) ).
cnf(c_3148,plain,
cong(sK8,sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_3109,c_1473]) ).
cnf(c_3152,plain,
midp(sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_3109,c_2980]) ).
cnf(c_3175,plain,
cong(sK8,sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_3152,c_1231]) ).
cnf(c_3184,plain,
perp(sK2,sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_3175,c_1538]) ).
cnf(c_3201,plain,
para(sK2,sK7,sK2,sK8),
inference(resolve,[status(thm)],[c_3152,c_546]) ).
cnf(c_3202,plain,
para(sK7,sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_3152,c_545]) ).
cnf(c_3204,plain,
para(sK2,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_3152,c_385]) ).
cnf(c_3236,plain,
perp(sK8,sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_3031,c_334]) ).
cnf(c_22912,plain,
( midp(sK8,sK8,sK8)
| ~ coll(sK8,sK8,sK8) ),
inference(resolve,[status(thm)],[c_3148,c_279]) ).
cnf(c_3343,plain,
midp(sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_733,c_22912]) ).
cnf(c_3366,plain,
midp(sK8,sK2,sK2),
inference(resolve,[status(thm)],[c_3343,c_2980]) ).
cnf(c_3368,plain,
para(sK8,sK7,sK8,sK2),
inference(resolve,[status(thm)],[c_3343,c_607]) ).
cnf(c_3391,plain,
para(sK7,sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_3366,c_545]) ).
cnf(c_3554,plain,
perp(sK2,sK8,sK2,sK8),
inference(resolve,[status(thm)],[c_3184,c_334]) ).
cnf(c_3579,plain,
para(sK2,sK8,sK2,sK7),
inference(resolve,[status(thm)],[c_3201,c_336]) ).
cnf(c_22913,plain,
( midp(A,sK8,sK7)
| ~ para(sK2,sK8,sK2,sK7)
| ~ midp(A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_3201,c_282]) ).
cnf(c_3585,plain,
( midp(A,sK8,sK7)
| ~ midp(A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_3579,c_22913]) ).
cnf(c_3602,plain,
( midp(sK2,A,sK2)
| ~ coll(sK2,A,sK2)
| ~ midp(sK7,A,sK8) ),
inference(resolve,[status(thm)],[c_3202,c_296]) ).
cnf(c_3616,plain,
eqangle(sK2,sK2,A,B,sK2,sK2,A,B),
inference(resolve,[status(thm)],[c_3204,c_302]) ).
cnf(c_3706,plain,
( cong(sK8,sK8,sK8,sK2)
| ~ midp(sK2,sK8,sK2) ),
inference(resolve,[status(thm)],[c_3236,c_291]) ).
cnf(c_3734,plain,
para(sK8,sK2,sK8,sK7),
inference(resolve,[status(thm)],[c_3368,c_336]) ).
cnf(c_22914,plain,
( midp(A,sK2,sK7)
| ~ para(sK8,sK2,sK8,sK7)
| ~ midp(A,sK8,sK8) ),
inference(resolve,[status(thm)],[c_3368,c_282]) ).
cnf(c_3740,plain,
( midp(A,sK2,sK7)
| ~ midp(A,sK8,sK8) ),
inference(resolve,[status(thm)],[c_3734,c_22914]) ).
cnf(c_3773,plain,
( perp(sK7,sK8,A,B)
| ~ perp(sK8,sK2,A,B) ),
inference(resolve,[status(thm)],[c_3391,c_331]) ).
cnf(c_3845,plain,
( cong(sK2,sK2,sK2,sK8)
| ~ midp(sK8,sK2,sK8) ),
inference(resolve,[status(thm)],[c_3554,c_291]) ).
cnf(c_3942,plain,
midp(sK8,sK8,sK7),
inference(resolve,[status(thm)],[c_3585,c_3366]) ).
cnf(c_3943,plain,
midp(sK2,sK8,sK7),
inference(resolve,[status(thm)],[c_3585,c_3152]) ).
cnf(c_3948,plain,
para(sK7,sK8,sK2,sK7),
inference(resolve,[status(thm)],[c_3942,c_608]) ).
cnf(c_3956,plain,
midp(sK8,sK7,sK8),
inference(resolve,[status(thm)],[c_3942,c_330]) ).
cnf(c_3961,plain,
cong(sK8,sK8,sK8,sK7),
inference(resolve,[status(thm)],[c_3942,c_278]) ).
cnf(c_3975,plain,
para(sK2,sK7,sK7,sK2),
inference(resolve,[status(thm)],[c_3943,c_607]) ).
cnf(c_4012,plain,
cong(sK8,sK7,sK8,sK8),
inference(resolve,[status(thm)],[c_3956,c_278]) ).
cnf(c_4046,plain,
para(sK7,sK8,sK7,sK2),
inference(resolve,[status(thm)],[c_3948,c_337]) ).
cnf(c_4082,plain,
cyclic(sK8,sK7,sK7,sK7),
inference(resolve,[status(thm)],[c_3961,c_403]) ).
cnf(c_4139,plain,
cong(sK8,sK8,sK7,sK8),
inference(resolve,[status(thm)],[c_3961,c_319]) ).
cnf(c_4185,plain,
para(sK2,sK7,sK2,sK7),
inference(resolve,[status(thm)],[c_3975,c_337]) ).
cnf(c_4278,plain,
cyclic(sK7,sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_4012,c_403]) ).
cnf(c_22915,plain,
( perp(sK7,sK8,sK8,sK8)
| ~ coll(sK8,sK7,sK8) ),
inference(resolve,[status(thm)],[c_4012,c_355]) ).
cnf(c_4294,plain,
perp(sK7,sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_659,c_22915]) ).
cnf(c_4443,plain,
para(sK7,sK2,sK7,sK8),
inference(resolve,[status(thm)],[c_4046,c_336]) ).
cnf(c_4447,plain,
eqangle(sK7,sK8,A,B,sK7,sK2,A,B),
inference(resolve,[status(thm)],[c_4046,c_302]) ).
cnf(c_22916,plain,
( midp(A,sK2,sK8)
| ~ para(sK7,sK2,sK7,sK8)
| ~ midp(A,sK7,sK7) ),
inference(resolve,[status(thm)],[c_4046,c_282]) ).
cnf(c_4449,plain,
( midp(A,sK2,sK8)
| ~ midp(A,sK7,sK7) ),
inference(resolve,[status(thm)],[c_4443,c_22916]) ).
cnf(c_4510,plain,
cyclic(sK7,sK8,sK7,sK7),
inference(resolve,[status(thm)],[c_4082,c_326]) ).
cnf(c_4512,plain,
( cyclic(sK7,sK7,sK7,A)
| ~ cyclic(sK8,sK7,sK7,A) ),
inference(resolve,[status(thm)],[c_4082,c_325]) ).
cnf(c_4552,plain,
cong(sK7,sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_4139,c_318]) ).
cnf(c_4572,plain,
eqangle(sK2,sK7,A,B,sK2,sK7,A,B),
inference(resolve,[status(thm)],[c_4185,c_302]) ).
cnf(c_22917,plain,
( perp(sK8,sK7,sK7,sK8)
| ~ cong(sK7,sK8,sK8,sK8) ),
inference(resolve,[status(thm)],[c_4278,c_383]) ).
cnf(c_4584,plain,
perp(sK8,sK7,sK7,sK8),
inference(resolve,[status(thm)],[c_4552,c_22917]) ).
cnf(c_22918,plain,
( cong(sK7,sK8,sK7,sK8)
| ~ midp(sK8,sK8,sK8) ),
inference(resolve,[status(thm)],[c_4294,c_291]) ).
cnf(c_4608,plain,
cong(sK7,sK8,sK7,sK8),
inference(resolve,[status(thm)],[c_3343,c_22918]) ).
cnf(c_4676,plain,
cyclic(sK7,sK7,sK8,sK7),
inference(resolve,[status(thm)],[c_4510,c_327]) ).
cnf(c_4728,plain,
perp(sK8,sK7,sK8,sK7),
inference(resolve,[status(thm)],[c_4584,c_334]) ).
cnf(c_4729,plain,
perp(sK7,sK8,sK8,sK7),
inference(resolve,[status(thm)],[c_4584,c_333]) ).
cnf(c_4828,plain,
cong(sK7,sK8,sK8,sK7),
inference(resolve,[status(thm)],[c_4608,c_319]) ).
cnf(c_22919,plain,
( midp(sK7,sK8,sK8)
| ~ coll(sK7,sK8,sK8) ),
inference(resolve,[status(thm)],[c_4608,c_279]) ).
cnf(c_4832,plain,
midp(sK7,sK8,sK8),
inference(resolve,[status(thm)],[c_734,c_22919]) ).
cnf(c_4865,plain,
midp(sK7,sK2,sK2),
inference(resolve,[status(thm)],[c_4832,c_2980]) ).
cnf(c_4930,plain,
midp(sK7,sK8,sK7),
inference(resolve,[status(thm)],[c_4865,c_3585]) ).
cnf(c_4933,plain,
para(sK2,sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_4865,c_532]) ).
cnf(c_4934,plain,
para(sK2,sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_4865,c_531]) ).
cnf(c_4992,plain,
para(sK7,sK7,sK7,sK7),
inference(resolve,[status(thm)],[c_4930,c_385]) ).
cnf(c_5064,plain,
cyclic(sK7,sK7,sK7,sK8),
inference(resolve,[status(thm)],[c_4676,c_328]) ).
cnf(c_5127,plain,
para(sK8,sK7,sK8,sK7),
inference(resolve,[status(thm)],[c_4728,c_393]) ).
cnf(c_5139,plain,
perp(sK7,sK8,sK7,sK8),
inference(resolve,[status(thm)],[c_4729,c_334]) ).
cnf(c_5191,plain,
cong(sK8,sK7,sK7,sK8),
inference(resolve,[status(thm)],[c_4828,c_318]) ).
cnf(c_5331,plain,
eqangle(sK2,sK2,A,B,sK2,sK8,A,B),
inference(resolve,[status(thm)],[c_4933,c_302]) ).
cnf(c_5347,plain,
( perp(sK2,sK2,A,B)
| ~ perp(sK8,sK2,A,B) ),
inference(resolve,[status(thm)],[c_4934,c_331]) ).
cnf(c_5510,plain,
eqangle(sK7,sK7,A,B,sK7,sK7,A,B),
inference(resolve,[status(thm)],[c_4992,c_302]) ).
cnf(c_5717,plain,
cyclic(sK7,sK7,sK8,sK8),
inference(resolve,[status(thm)],[c_5064,c_389]) ).
cnf(c_5765,plain,
eqangle(sK8,sK7,A,B,sK8,sK7,A,B),
inference(resolve,[status(thm)],[c_5127,c_302]) ).
cnf(c_5774,plain,
para(sK7,sK8,sK7,sK8),
inference(resolve,[status(thm)],[c_5139,c_393]) ).
cnf(c_5809,plain,
cong(sK8,sK7,sK8,sK7),
inference(resolve,[status(thm)],[c_5191,c_319]) ).
cnf(c_5930,plain,
cyclic(sK7,sK8,sK7,sK8),
inference(resolve,[status(thm)],[c_5717,c_327]) ).
cnf(c_5979,plain,
eqangle(sK7,sK8,A,B,sK7,sK8,A,B),
inference(resolve,[status(thm)],[c_5774,c_302]) ).
cnf(c_22920,plain,
( midp(sK8,sK7,sK7)
| ~ coll(sK8,sK7,sK7) ),
inference(resolve,[status(thm)],[c_5809,c_279]) ).
cnf(c_6064,plain,
midp(sK8,sK7,sK7),
inference(resolve,[status(thm)],[c_815,c_22920]) ).
cnf(c_6092,plain,
cong(sK2,sK7,sK2,sK7),
inference(resolve,[status(thm)],[c_6064,c_1527]) ).
cnf(c_6150,plain,
cyclic(sK8,sK7,sK7,sK8),
inference(resolve,[status(thm)],[c_5930,c_326]) ).
cnf(c_22921,plain,
( midp(sK2,sK7,sK7)
| ~ coll(sK2,sK7,sK7) ),
inference(resolve,[status(thm)],[c_6092,c_279]) ).
cnf(c_6359,plain,
midp(sK2,sK7,sK7),
inference(resolve,[status(thm)],[c_879,c_22921]) ).
cnf(c_6425,plain,
( cyclic(sK7,sK7,A,sK8)
| ~ cyclic(sK8,sK7,sK7,A) ),
inference(resolve,[status(thm)],[c_6150,c_325]) ).
cnf(c_6426,plain,
( cyclic(sK7,sK7,sK8,A)
| ~ cyclic(sK8,sK7,sK7,A) ),
inference(resolve,[status(thm)],[c_6150,c_325]) ).
cnf(c_6443,plain,
midp(sK7,sK2,sK7),
inference(resolve,[status(thm)],[c_3740,c_4832]) ).
cnf(c_6475,plain,
cong(sK7,sK2,sK7,sK7),
inference(resolve,[status(thm)],[c_6443,c_278]) ).
cnf(c_6713,plain,
cyclic(sK2,sK7,sK7,sK7),
inference(resolve,[status(thm)],[c_6475,c_403]) ).
cnf(c_7259,plain,
cyclic(sK7,sK2,sK7,sK7),
inference(resolve,[status(thm)],[c_6713,c_326]) ).
cnf(c_7373,plain,
cyclic(sK7,sK7,sK2,sK7),
inference(resolve,[status(thm)],[c_7259,c_327]) ).
cnf(c_7488,plain,
cyclic(sK7,sK7,sK7,sK2),
inference(resolve,[status(thm)],[c_7373,c_328]) ).
cnf(c_7592,plain,
cyclic(sK7,sK7,sK2,sK2),
inference(resolve,[status(thm)],[c_7488,c_389]) ).
cnf(c_7594,plain,
( cyclic(sK7,sK7,A,sK2)
| ~ cyclic(sK7,sK7,sK7,A) ),
inference(resolve,[status(thm)],[c_7488,c_325]) ).
cnf(c_7595,plain,
( cyclic(sK7,sK7,sK2,A)
| ~ cyclic(sK7,sK7,sK7,A) ),
inference(resolve,[status(thm)],[c_7488,c_325]) ).
cnf(c_7660,plain,
( cyclic(sK7,sK2,sK2,A)
| ~ cyclic(sK7,sK7,sK2,A) ),
inference(resolve,[status(thm)],[c_7592,c_325]) ).
cnf(c_7790,plain,
midp(sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_4449,c_6359]) ).
cnf(c_7791,plain,
midp(sK8,sK2,sK8),
inference(resolve,[status(thm)],[c_4449,c_6064]) ).
cnf(c_7803,plain,
cong(sK2,sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_7791,c_3845]) ).
cnf(c_7824,plain,
midp(sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_7790,c_330]) ).
cnf(c_7843,plain,
cong(sK8,sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_7824,c_3706]) ).
cnf(c_7852,plain,
para(sK8,sK7,sK8,sK8),
inference(resolve,[status(thm)],[c_7791,c_546]) ).
cnf(c_8175,plain,
cong(sK8,sK8,sK2,sK8),
inference(resolve,[status(thm)],[c_7843,c_319]) ).
cnf(c_8214,plain,
( midp(sK7,A,sK8)
| ~ coll(sK7,A,sK8)
| ~ midp(sK8,A,sK8) ),
inference(resolve,[status(thm)],[c_7852,c_296]) ).
cnf(c_8401,plain,
cong(sK2,sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_8175,c_318]) ).
cnf(c_8580,plain,
eqangle(A,B,sK2,sK8,A,B,sK2,sK8),
inference(resolve,[status(thm)],[c_2947,c_323]) ).
cnf(c_8598,plain,
( cyclic(sK2,A,sK8,sK8)
| ~ coll(sK8,sK8,A) ),
inference(resolve,[status(thm)],[c_2983,c_299]) ).
cnf(c_8741,plain,
( cong(sK2,A,sK2,A)
| ~ cyclic(sK2,A,sK2,A)
| ~ cyclic(sK2,A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_3616,c_387]) ).
cnf(c_8744,plain,
( cyclic(sK2,A,sK2,sK2)
| ~ coll(sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_3616,c_299]) ).
cnf(c_8897,plain,
( cong(sK8,A,sK2,A)
| ~ cyclic(sK8,A,sK7,sK7)
| ~ cyclic(sK8,A,sK7,A)
| ~ cyclic(sK8,A,sK7,sK2) ),
inference(resolve,[status(thm)],[c_4447,c_298]) ).
cnf(c_8934,plain,
( cyclic(sK7,A,sK2,sK2)
| ~ coll(sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_4572,c_299]) ).
cnf(c_9089,plain,
( cong(sK2,A,sK8,A)
| ~ cyclic(sK2,A,sK2,sK2)
| ~ cyclic(sK2,A,sK2,A)
| ~ cyclic(sK2,A,sK2,sK8) ),
inference(resolve,[status(thm)],[c_5331,c_298]) ).
cnf(c_9140,plain,
( cyclic(sK7,A,sK7,sK7)
| ~ coll(sK7,sK7,A) ),
inference(resolve,[status(thm)],[c_5510,c_299]) ).
cnf(c_9174,plain,
( cyclic(sK7,A,sK8,sK8)
| ~ coll(sK8,sK8,A) ),
inference(resolve,[status(thm)],[c_5765,c_299]) ).
cnf(c_9175,plain,
( cong(sK7,A,sK7,A)
| ~ cyclic(sK7,A,sK8,sK8)
| ~ cyclic(sK7,A,sK8,A)
| ~ cyclic(sK7,A,sK8,sK7) ),
inference(resolve,[status(thm)],[c_5765,c_298]) ).
cnf(c_9235,plain,
( cyclic(sK8,A,sK7,sK7)
| ~ coll(sK7,sK7,A) ),
inference(resolve,[status(thm)],[c_5979,c_299]) ).
cnf(c_9649,plain,
para(A,B,A,B),
inference(resolve,[status(thm)],[c_8580,c_303]) ).
cnf(c_22922,plain,
( cyclic(A,sK8,sK2,sK2)
| ~ coll(sK2,sK2,sK8) ),
inference(resolve,[status(thm)],[c_8580,c_299]) ).
cnf(c_9651,plain,
cyclic(A,sK8,sK2,sK2),
inference(resolve,[status(thm)],[c_741,c_22922]) ).
cnf(c_22923,plain,
( ~ cong(sK2,sK2,sK2,sK8)
| ~ cong(sK2,sK2,sK2,A)
| midp(sK8,A,sK8)
| ~ coll(sK8,A,sK8) ),
inference(resolve,[status(thm)],[c_8580,c_233]) ).
cnf(c_9656,plain,
( ~ cong(sK2,sK2,sK2,A)
| midp(sK8,A,sK8)
| ~ coll(sK8,A,sK8) ),
inference(resolve,[status(thm)],[c_7803,c_22923]) ).
cnf(c_9659,plain,
( midp(A,C,C)
| ~ midp(A,B,B) ),
inference(resolve,[status(thm)],[c_9649,c_380]) ).
cnf(c_9667,plain,
( midp(C,B,C)
| ~ coll(C,B,C)
| ~ midp(A,B,A) ),
inference(resolve,[status(thm)],[c_9649,c_296]) ).
cnf(c_9669,plain,
coll(A,B,B),
inference(resolve,[status(thm)],[c_9649,c_280]) ).
cnf(c_9832,plain,
coll(A,A,B),
inference(resolve,[status(thm)],[c_9669,c_394]) ).
cnf(c_9833,plain,
coll(A,B,A),
inference(resolve,[status(thm)],[c_9669,c_339]) ).
cnf(c_9840,plain,
cyclic(sK8,A,sK7,sK7),
inference(resolve,[status(thm)],[c_9832,c_9235]) ).
cnf(c_9841,plain,
cyclic(sK7,A,sK8,sK8),
inference(resolve,[status(thm)],[c_9832,c_9174]) ).
cnf(c_9842,plain,
cyclic(sK7,A,sK7,sK7),
inference(resolve,[status(thm)],[c_9832,c_9140]) ).
cnf(c_9843,plain,
cyclic(sK7,A,sK2,sK2),
inference(resolve,[status(thm)],[c_9832,c_8934]) ).
cnf(c_9845,plain,
cyclic(sK2,A,sK2,sK2),
inference(resolve,[status(thm)],[c_9832,c_8744]) ).
cnf(c_9847,plain,
cyclic(sK2,A,sK8,sK8),
inference(resolve,[status(thm)],[c_9832,c_8598]) ).
cnf(c_9992,plain,
coll(sK7,A,sK8),
inference(resolve,[status(thm)],[c_9832,c_661]) ).
cnf(c_10001,plain,
( midp(C,B,C)
| ~ midp(A,B,A) ),
inference(resolve,[status(thm)],[c_9833,c_9667]) ).
cnf(c_10002,plain,
( ~ cong(sK2,sK2,sK2,A)
| midp(sK8,A,sK8) ),
inference(resolve,[status(thm)],[c_9833,c_9656]) ).
cnf(c_10052,plain,
( midp(sK2,A,sK2)
| ~ midp(sK7,A,sK8) ),
inference(resolve,[status(thm)],[c_9833,c_3602]) ).
cnf(c_10059,plain,
( cong(sK8,A,sK2,A)
| ~ cyclic(sK8,A,sK7,A)
| ~ cyclic(sK8,A,sK7,sK2) ),
inference(resolve,[status(thm)],[c_9840,c_8897]) ).
cnf(c_10061,plain,
( cong(sK7,A,sK7,A)
| ~ cyclic(sK7,A,sK8,A)
| ~ cyclic(sK7,A,sK8,sK7) ),
inference(resolve,[status(thm)],[c_9841,c_9175]) ).
cnf(c_10073,plain,
( cong(sK2,A,sK8,A)
| ~ cyclic(sK2,A,sK2,A)
| ~ cyclic(sK2,A,sK2,sK8) ),
inference(resolve,[status(thm)],[c_9845,c_9089]) ).
cnf(c_10074,plain,
( cong(sK2,A,sK2,A)
| ~ cyclic(sK2,A,sK2,A) ),
inference(resolve,[status(thm)],[c_9845,c_8741]) ).
cnf(c_10319,plain,
( midp(sK7,A,sK8)
| ~ midp(sK8,A,sK8) ),
inference(resolve,[status(thm)],[c_9992,c_8214]) ).
cnf(c_10450,plain,
cyclic(A,sK2,sK8,sK2),
inference(resolve,[status(thm)],[c_9651,c_327]) ).
cnf(c_10468,plain,
cyclic(sK8,sK7,A,sK7),
inference(resolve,[status(thm)],[c_9840,c_327]) ).
cnf(c_10499,plain,
cyclic(sK7,sK7,A,sK7),
inference(resolve,[status(thm)],[c_9842,c_327]) ).
cnf(c_10513,plain,
cyclic(sK7,sK2,A,sK2),
inference(resolve,[status(thm)],[c_9843,c_327]) ).
cnf(c_10514,plain,
cyclic(A,sK7,sK2,sK2),
inference(resolve,[status(thm)],[c_9843,c_326]) ).
cnf(c_10516,plain,
( cyclic(A,sK2,sK2,B)
| ~ cyclic(sK7,A,sK2,B) ),
inference(resolve,[status(thm)],[c_9843,c_325]) ).
cnf(c_10569,plain,
cyclic(sK2,sK8,A,sK8),
inference(resolve,[status(thm)],[c_9847,c_327]) ).
cnf(c_10694,plain,
cyclic(A,sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_10450,c_328]) ).
cnf(c_10723,plain,
cyclic(sK8,sK7,sK7,A),
inference(resolve,[status(thm)],[c_10468,c_328]) ).
cnf(c_10724,plain,
cyclic(sK7,sK8,A,sK7),
inference(resolve,[status(thm)],[c_10468,c_326]) ).
cnf(c_10741,plain,
cyclic(sK7,sK7,sK8,A),
inference(resolve,[status(thm)],[c_10723,c_6426]) ).
cnf(c_10742,plain,
cyclic(sK7,sK7,A,sK8),
inference(resolve,[status(thm)],[c_10723,c_6425]) ).
cnf(c_10743,plain,
cyclic(sK7,sK7,sK7,A),
inference(resolve,[status(thm)],[c_10723,c_4512]) ).
cnf(c_10749,plain,
cyclic(sK7,sK7,sK2,A),
inference(resolve,[status(thm)],[c_10743,c_7595]) ).
cnf(c_10750,plain,
cyclic(sK7,sK7,A,sK2),
inference(resolve,[status(thm)],[c_10743,c_7594]) ).
cnf(c_10758,plain,
cyclic(sK7,sK2,sK2,A),
inference(resolve,[status(thm)],[c_10749,c_7660]) ).
cnf(c_10845,plain,
( cyclic(sK7,A,B,sK7)
| ~ cyclic(sK7,sK7,A,B) ),
inference(resolve,[status(thm)],[c_10499,c_325]) ).
cnf(c_10870,plain,
( cyclic(sK2,A,sK2,B)
| ~ cyclic(sK7,sK2,A,B) ),
inference(resolve,[status(thm)],[c_10513,c_325]) ).
cnf(c_10885,plain,
( eqangle(A,sK2,sK2,sK2,sK2,sK2,sK2,sK7)
| ~ para(A,sK7,sK2,sK2) ),
inference(resolve,[status(thm)],[c_10514,c_292]) ).
cnf(c_22924,plain,
( perp(A,sK2,sK2,sK8)
| ~ cong(sK2,sK8,sK8,sK8)
| ~ cong(sK2,A,sK8,A) ),
inference(resolve,[status(thm)],[c_10569,c_289]) ).
cnf(c_10952,plain,
( perp(A,sK2,sK2,sK8)
| ~ cong(sK2,A,sK8,A) ),
inference(resolve,[status(thm)],[c_8401,c_22924]) ).
cnf(c_11085,plain,
cyclic(sK2,A,sK2,sK8),
inference(resolve,[status(thm)],[c_10694,c_326]) ).
cnf(c_11099,plain,
( cong(sK2,A,sK8,A)
| ~ cyclic(sK2,A,sK2,A) ),
inference(resolve,[status(thm)],[c_11085,c_10073]) ).
cnf(c_22925,plain,
( cyclic(sK7,sK7,A,B)
| ~ cyclic(sK8,sK7,sK7,A) ),
inference(resolve,[status(thm)],[c_10723,c_325]) ).
cnf(c_11116,plain,
cyclic(sK7,sK7,A,B),
inference(resolve,[status(thm)],[c_10723,c_22925]) ).
cnf(c_11133,plain,
cyclic(sK7,A,B,sK7),
inference(resolve,[status(thm)],[c_11116,c_10845]) ).
cnf(c_11135,plain,
( cong(sK7,A,sK7,A)
| ~ cyclic(sK7,A,sK8,A) ),
inference(resolve,[status(thm)],[c_11133,c_10061]) ).
cnf(c_11137,plain,
( cyclic(sK8,A,sK7,B)
| ~ cyclic(sK7,sK8,A,B) ),
inference(resolve,[status(thm)],[c_10724,c_325]) ).
cnf(c_22926,plain,
( cyclic(sK7,sK8,A,B)
| ~ cyclic(sK7,sK7,sK8,A) ),
inference(resolve,[status(thm)],[c_10741,c_325]) ).
cnf(c_11152,plain,
cyclic(sK7,sK8,A,B),
inference(resolve,[status(thm)],[c_11116,c_22926]) ).
cnf(c_11165,plain,
cyclic(sK8,A,sK7,B),
inference(resolve,[status(thm)],[c_11152,c_11137]) ).
cnf(c_22927,plain,
( cong(sK8,A,sK2,A)
| ~ cyclic(sK8,A,sK7,A) ),
inference(resolve,[status(thm)],[c_11165,c_10059]) ).
cnf(c_11171,plain,
cong(sK8,A,sK2,A),
inference(resolve,[status(thm)],[c_11165,c_22927]) ).
cnf(c_22928,plain,
( cyclic(sK7,A,sK8,B)
| ~ cyclic(sK7,sK7,A,B) ),
inference(resolve,[status(thm)],[c_10742,c_325]) ).
cnf(c_11280,plain,
cyclic(sK7,A,sK8,B),
inference(resolve,[status(thm)],[c_11116,c_22928]) ).
cnf(c_22929,plain,
( perp(A,sK7,sK7,sK8)
| ~ cong(sK7,sK8,sK7,sK8)
| ~ cong(sK7,A,sK7,A) ),
inference(resolve,[status(thm)],[c_10742,c_289]) ).
cnf(c_11283,plain,
( perp(A,sK7,sK7,sK8)
| ~ cong(sK7,A,sK7,A) ),
inference(resolve,[status(thm)],[c_4608,c_22929]) ).
cnf(c_11296,plain,
cong(sK7,A,sK7,A),
inference(resolve,[status(thm)],[c_11280,c_11135]) ).
cnf(c_11300,plain,
perp(A,sK7,sK7,sK8),
inference(resolve,[status(thm)],[c_11296,c_11283]) ).
cnf(c_22930,plain,
( cyclic(sK7,sK2,A,B)
| ~ cyclic(sK7,sK7,sK2,A) ),
inference(resolve,[status(thm)],[c_10749,c_325]) ).
cnf(c_11403,plain,
cyclic(sK7,sK2,A,B),
inference(resolve,[status(thm)],[c_11116,c_22930]) ).
cnf(c_11417,plain,
cyclic(sK2,A,sK2,B),
inference(resolve,[status(thm)],[c_11403,c_10870]) ).
cnf(c_11424,plain,
cong(sK2,A,sK8,A),
inference(resolve,[status(thm)],[c_11417,c_11099]) ).
cnf(c_11426,plain,
cong(sK2,A,sK2,A),
inference(resolve,[status(thm)],[c_11417,c_10074]) ).
cnf(c_11434,plain,
perp(A,sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_11424,c_10952]) ).
cnf(c_22931,plain,
( cyclic(sK7,A,sK2,B)
| ~ cyclic(sK7,sK7,A,B) ),
inference(resolve,[status(thm)],[c_10750,c_325]) ).
cnf(c_11510,plain,
cyclic(sK7,A,sK2,B),
inference(resolve,[status(thm)],[c_11116,c_22931]) ).
cnf(c_11523,plain,
cyclic(A,sK2,sK2,B),
inference(resolve,[status(thm)],[c_11510,c_10516]) ).
cnf(c_11562,plain,
cyclic(sK2,sK2,A,A),
inference(resolve,[status(thm)],[c_10758,c_389]) ).
cnf(c_22932,plain,
( cyclic(sK2,sK2,A,B)
| ~ cyclic(sK7,sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_10758,c_325]) ).
cnf(c_11563,plain,
cyclic(sK2,sK2,A,B),
inference(resolve,[status(thm)],[c_11523,c_22932]) ).
cnf(c_22933,plain,
( perp(sK8,sK2,A,B)
| ~ cong(sK8,A,sK2,A) ),
inference(resolve,[status(thm)],[c_11171,c_290]) ).
cnf(c_12190,plain,
perp(sK8,sK2,A,B),
inference(resolve,[status(thm)],[c_11171,c_22933]) ).
cnf(c_12195,plain,
perp(sK2,sK2,A,B),
inference(resolve,[status(thm)],[c_12190,c_5347]) ).
cnf(c_12198,plain,
perp(sK7,sK8,A,B),
inference(resolve,[status(thm)],[c_12190,c_3773]) ).
cnf(c_12204,plain,
perp(sK2,sK8,A,B),
inference(resolve,[status(thm)],[c_12190,c_2918]) ).
cnf(c_22934,plain,
( para(C,sK7,A,B)
| ~ perp(sK7,sK8,A,B) ),
inference(resolve,[status(thm)],[c_11300,c_332]) ).
cnf(c_12946,plain,
para(A,sK7,B,C),
inference(resolve,[status(thm)],[c_12198,c_22934]) ).
cnf(c_12974,plain,
eqangle(A,sK2,sK2,sK2,sK2,sK2,sK2,sK7),
inference(resolve,[status(thm)],[c_12946,c_10885]) ).
cnf(c_22935,plain,
( eqangle(sK2,C,sK2,A,sK2,sK2,sK2,A)
| ~ perp(sK0(sK2,A,sK2,B),sK2,sK2,C)
| ~ perp(sK2,sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_11417,c_199]) ).
cnf(c_13445,plain,
( eqangle(sK2,C,sK2,A,sK2,sK2,sK2,A)
| ~ perp(sK0(sK2,A,sK2,B),sK2,sK2,C) ),
inference(resolve,[status(thm)],[c_12195,c_22935]) ).
cnf(c_22936,plain,
( para(C,sK2,A,B)
| ~ perp(sK2,sK8,A,B) ),
inference(resolve,[status(thm)],[c_11434,c_332]) ).
cnf(c_13528,plain,
para(A,sK2,B,C),
inference(resolve,[status(thm)],[c_12204,c_22936]) ).
cnf(c_13947,plain,
eqangle(sK2,A,sK2,sK2,B,A,B,sK2),
inference(resolve,[status(thm)],[c_11523,c_301]) ).
cnf(c_22937,plain,
( eqangle(A,B,sK2,B,sK2,B,sK2,sK2)
| ~ para(A,sK2,sK2,B) ),
inference(resolve,[status(thm)],[c_11523,c_292]) ).
cnf(c_13948,plain,
eqangle(A,B,sK2,B,sK2,B,sK2,sK2),
inference(resolve,[status(thm)],[c_13528,c_22937]) ).
cnf(c_22938,plain,
( perp(A,sK2,sK2,A)
| ~ cong(sK2,A,sK2,A) ),
inference(resolve,[status(thm)],[c_11562,c_383]) ).
cnf(c_13983,plain,
perp(A,sK2,sK2,A),
inference(resolve,[status(thm)],[c_11426,c_22938]) ).
cnf(c_22939,plain,
( perp(A,sK2,sK2,B)
| ~ cong(sK2,B,sK2,B)
| ~ cong(sK2,A,sK2,A) ),
inference(resolve,[status(thm)],[c_11563,c_289]) ).
cnf(c_22940,plain,
( perp(B,sK2,sK2,A)
| ~ cong(sK2,A,sK2,A) ),
inference(resolve,[status(thm)],[c_11426,c_22939]) ).
cnf(c_13997,plain,
perp(A,sK2,sK2,B),
inference(resolve,[status(thm)],[c_11426,c_22940]) ).
cnf(c_14008,plain,
eqangle(sK2,A,sK2,B,sK2,sK2,sK2,B),
inference(resolve,[status(thm)],[c_13997,c_13445]) ).
cnf(c_14481,plain,
perp(A,B,sK8,sK2),
inference(resolve,[status(thm)],[c_12190,c_333]) ).
cnf(c_22941,plain,
( para(A,B,C,D)
| ~ perp(A,B,sK8,sK2) ),
inference(resolve,[status(thm)],[c_12190,c_332]) ).
cnf(c_14482,plain,
para(A,B,C,D),
inference(resolve,[status(thm)],[c_14481,c_22941]) ).
cnf(c_14505,plain,
eqangle(A,B,C,D,E,F,C,D),
inference(resolve,[status(thm)],[c_14482,c_302]) ).
cnf(c_14825,plain,
perp(sK2,A,A,sK2),
inference(resolve,[status(thm)],[c_13983,c_333]) ).
cnf(c_14840,plain,
( cong(B,sK2,B,A)
| ~ midp(sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_13997,c_291]) ).
cnf(c_14952,plain,
perp(sK2,A,sK2,A),
inference(resolve,[status(thm)],[c_14825,c_334]) ).
cnf(c_14978,plain,
( cong(sK2,sK2,sK2,A)
| ~ midp(A,sK2,A) ),
inference(resolve,[status(thm)],[c_14952,c_291]) ).
cnf(c_14984,plain,
midp(sK2,A,A),
inference(resolve,[status(thm)],[c_9659,c_6359]) ).
cnf(c_15001,plain,
midp(A,sK2,A),
inference(resolve,[status(thm)],[c_10001,c_14984]) ).
cnf(c_15008,plain,
cong(sK2,sK2,sK2,A),
inference(resolve,[status(thm)],[c_15001,c_14978]) ).
cnf(c_15124,plain,
midp(sK8,A,sK8),
inference(resolve,[status(thm)],[c_15008,c_10002]) ).
cnf(c_15160,plain,
midp(sK7,A,sK8),
inference(resolve,[status(thm)],[c_15124,c_10319]) ).
cnf(c_15201,plain,
midp(sK2,A,sK2),
inference(resolve,[status(thm)],[c_15160,c_10052]) ).
cnf(c_15671,plain,
midp(sK2,sK2,A),
inference(resolve,[status(thm)],[c_15201,c_330]) ).
cnf(c_15675,plain,
cong(A,sK2,A,B),
inference(resolve,[status(thm)],[c_15671,c_14840]) ).
cnf(c_17098,plain,
eqangle(A,sK2,sK2,B,sK2,B,A,B),
inference(resolve,[status(thm)],[c_15675,c_295]) ).
cnf(c_19867,plain,
eqangle(sK2,sK2,A,sK2,sK2,sK7,sK2,sK2),
inference(resolve,[status(thm)],[c_12974,c_323]) ).
cnf(c_20005,plain,
eqangle(sK2,A,B,A,sK2,sK2,B,sK2),
inference(resolve,[status(thm)],[c_13947,c_321]) ).
cnf(c_20008,plain,
eqangle(A,B,sK2,A,sK2,A,sK2,sK2),
inference(resolve,[status(thm)],[c_13948,c_324]) ).
cnf(c_20042,plain,
eqangle(sK2,A,sK2,sK2,sK2,B,sK2,B),
inference(resolve,[status(thm)],[c_14008,c_321]) ).
cnf(c_20219,plain,
eqangle(A,B,C,D,A,B,E,F),
inference(resolve,[status(thm)],[c_14505,c_323]) ).
cnf(c_20503,plain,
( eqangle(B,sK2,sK2,A,C,D,E,F)
| ~ eqangle(sK2,A,B,A,C,D,E,F) ),
inference(resolve,[status(thm)],[c_17098,c_320]) ).
cnf(c_22507,plain,
( eqangle(sK2,sK2,E,sK2,A,B,C,D)
| ~ eqangle(sK2,sK7,sK2,sK2,A,B,C,D) ),
inference(resolve,[status(thm)],[c_19867,c_320]) ).
cnf(c_22606,plain,
( eqangle(sK2,F,A,F,B,C,D,E)
| ~ eqangle(sK2,sK2,A,sK2,B,C,D,E) ),
inference(resolve,[status(thm)],[c_20005,c_320]) ).
cnf(c_22608,plain,
( eqangle(A,F,sK2,A,B,C,D,E)
| ~ eqangle(sK2,A,sK2,sK2,B,C,D,E) ),
inference(resolve,[status(thm)],[c_20008,c_320]) ).
cnf(c_22631,plain,
( eqangle(sK2,F,sK2,sK2,B,C,D,E)
| ~ eqangle(sK2,A,sK2,A,B,C,D,E) ),
inference(resolve,[status(thm)],[c_20042,c_320]) ).
cnf(c_22785,plain,
eqangle(A,B,A,B,C,D,E,F),
inference(resolve,[status(thm)],[c_20219,c_321]) ).
cnf(c_22790,plain,
eqangle(sK2,A,sK2,sK2,B,C,D,E),
inference(resolve,[status(thm)],[c_22785,c_22631]) ).
cnf(c_22862,plain,
eqangle(A,B,sK2,A,C,D,E,F),
inference(resolve,[status(thm)],[c_22790,c_22608]) ).
cnf(c_22864,plain,
eqangle(sK2,sK2,A,sK2,B,C,D,E),
inference(resolve,[status(thm)],[c_22862,c_22507]) ).
cnf(c_22890,plain,
eqangle(sK2,A,B,A,C,D,E,F),
inference(resolve,[status(thm)],[c_22864,c_22606]) ).
cnf(c_22905,plain,
eqangle(A,sK2,sK2,B,C,D,E,F),
inference(resolve,[status(thm)],[c_22890,c_20503]) ).
cnf(c_22906,plain,
$false,
inference(resolve,[status(thm)],[c_22905,c_237]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO613+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n018.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Fri Sep 25 13:46:37 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 2080912 was started by sandbox on n018,
% 0.17/0.44 % Fri Sep 25 13:46:37 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.48
% 0.17/0.48 % From the command line: assign(max_seconds, 300).
% 160.04/21.87
% 160.04/21.87 % given #500 (T,wt=9): 1869 coll(c3,c6,c2). [resolve(1809,a,624,a)].
% 160.04/21.87
% 160.04/21.87 % given #1000 (W,wt=13): 1720 -coll(c7,c6,A) | coll(A,c1,c7). [resolve(1694,a,338,b)].
% 160.04/21.87
% 160.04/21.87 % given #1500 (T,wt=13): 2428 -coll(c8,c5,A) | coll(A,c4,c8). [resolve(2397,a,338,b)].
% 160.04/21.87
% 160.04/21.87 % given #2000 (T,wt=9): 6444 midp(c2,c4,c5). [resolve(3740,a,3343,a)].
% 160.04/21.87
% 160.04/21.87 % given #2500 (W,wt=9): 9896 coll(c4,A,c7). [back_unit_del(2489),unit_del(a,9832)].
% 160.04/21.87
% 160.04/21.87 % given #3000 (T,wt=10): 14567 cong(A,c2,c4,A). [resolve(12485,a,319,a)].
% 160.04/21.87
% 160.04/21.87 % given #3500 (T,wt=14): 9376 eqangle(c5,c4,c2,c5,c2,c4,c5,c4). [resolve(7125,a,323,a)].
% 160.04/21.87
% 160.04/21.87 % given #4000 (W,wt=14): 18264 eqangle(c5,c4,c2,c4,c4,c2,c5,c2). [resolve(8626,a,323,a)].
% 160.04/21.87
% 160.04/21.87 % given #4500 (T,wt=14): 19466 eqangle(c5,A,A,c2,c2,c5,c2,c2). [resolve(10820,a,324,a)].
% 160.04/21.87
% 160.04/21.87 % SZS status Theorem for theBenchmark
% 160.04/21.87
% 160.04/21.87 % Proof 1 at 3.85 (+ 1.09) seconds.
% 160.04/21.87 % Length of proof is 387.
% 160.04/21.87 % Level of proof is 48.
% 160.04/21.87 % Maximum clause weight is 38.000.
% 160.04/21.87 % Given clauses 4893.
% 160.04/21.87
% 160.04/21.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------