%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO656+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 : n014.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:19 AM UTC 2026
% Result : Theorem 33.39s 10.22s
% Output : CNFRefutation 33.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 39
% Syntax : Number of formulae : 344 ( 187 unt; 0 def)
% Number of atoms : 569 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 382 ( 157 ~; 153 |; 32 &)
% ( 0 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 465 ( 3 sgn 191 !; 6 ?)
% 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(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(ruleD20,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,C,D,P,Q,U,V)
=> eqangle(P,Q,U,V,A,B,C,D) ),
file('theBenchmark.p',ruleD20) ).
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(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(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(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(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(ruleD73,axiom,
! [A,B,C,D,P,Q,U,V] :
( ( para(P,Q,U,V)
& eqangle(A,B,C,D,P,Q,U,V) )
=> para(A,B,C,D) ),
file('theBenchmark.p',ruleD73) ).
fof(exemplo6GDDFULLmoreE02314,conjecture,
! [A,B,C,D,E,F] :
( ( eqangle(F,D,D,B,F,D,D,C)
& eqangle(E,D,D,A,E,D,D,C)
& midp(D,B,A) )
=> para(E,F,A,B) ),
file('theBenchmark.p',exemplo6GDDFULLmoreE02314) ).
fof(exemplo6GDDFULLmoreE02314_neg,negated_conjecture,
~ ! [A,B,C,D,E,F] :
( ( eqangle(F,D,D,B,F,D,D,C)
& eqangle(E,D,D,A,E,D,D,C)
& midp(D,B,A) )
=> para(E,F,A,B) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULLmoreE02314]) ).
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_101,plain,
( perp(B,C,C,D)
| ~ coll(A,B,D)
| ~ circle(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD53]) ).
cnf(c_142,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]) ).
fof(nnf_95,plain,
? [A,B,C,D,E,F] :
( ~ para(E,F,A,B)
& eqangle(F,D,D,B,F,D,D,C)
& eqangle(E,D,D,A,E,D,D,C)
& midp(D,B,A) ),
inference(fof_nnf,[status(thm)],[exemplo6GDDFULLmoreE02314_neg]) ).
fof(sk_exemplo6GDDFULLmoreE02314_neg,plain,
( ~ para(sK0,sK1,sK2,sK3)
& eqangle(sK1,sK4,sK4,sK3,sK1,sK4,sK4,sK5)
& eqangle(sK0,sK4,sK4,sK2,sK0,sK4,sK4,sK5)
& midp(sK4,sK3,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK3,sK2,sK0,sK5,sK1]),skolemize(A,sK2),skolemize(B,sK3),skolemize(C,sK5),skolemize(D,sK4),skolemize(E,sK0),skolemize(F,sK1)],[nnf_95]) ).
cnf(c_147,negated_conjecture,
~ para(sK0,sK1,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULLmoreE02314_neg]) ).
cnf(c_148,negated_conjecture,
eqangle(sK1,sK4,sK4,sK3,sK1,sK4,sK4,sK5),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULLmoreE02314_neg]) ).
cnf(c_149,negated_conjecture,
eqangle(sK0,sK4,sK4,sK2,sK0,sK4,sK4,sK5),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULLmoreE02314_neg]) ).
cnf(c_150,negated_conjecture,
midp(sK4,sK3,sK2),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULLmoreE02314_neg]) ).
cnf(c_183,plain,
( para(A,B,C,D)
| ~ para(E,F,V6,V7)
| ~ eqangle(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[ruleD73]) ).
cnf(c_186,plain,
( coll(A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD69]) ).
cnf(c_187,plain,
( cong(A,B,A,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD68]) ).
cnf(c_188,plain,
( midp(A,B,C)
| ~ coll(A,B,C)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD67]) ).
cnf(c_189,plain,
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD66]) ).
cnf(c_191,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_192,plain,
( para(B,D,C,E)
| ~ midp(A,D,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD63]) ).
cnf(c_198,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_199,plain,
( perp(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD56]) ).
cnf(c_200,plain,
( cong(D,B,D,C)
| ~ perp(D,A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD55]) ).
cnf(c_205,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_206,plain,
( para(A,D,C,E)
| ~ midp(D,B,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD44]) ).
cnf(c_207,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_210,plain,
( eqangle(C,A,C,B,D,A,D,B)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD41]) ).
cnf(c_211,plain,
( eqangle(A,B,E,F,C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD40]) ).
cnf(c_212,plain,
( para(A,B,E,F)
| ~ eqangle(A,B,C,D,E,F,C,D) ),
inference(clausify,[status(thm)],[ruleD39]) ).
cnf(c_227,plain,
( cong(C,D,A,B)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD24]) ).
cnf(c_228,plain,
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD23]) ).
cnf(c_230,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_231,plain,
( eqangle(E,F,V6,V7,A,B,C,D)
| ~ eqangle(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[ruleD20]) ).
cnf(c_232,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_233,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_234,plain,
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD17]) ).
cnf(c_235,plain,
( cyclic(B,A,C,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD16]) ).
cnf(c_236,plain,
( cyclic(A,C,B,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD15]) ).
cnf(c_237,plain,
( cyclic(A,B,D,C)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD14]) ).
cnf(c_238,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_239,plain,
( midp(A,C,B)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD11]) ).
cnf(c_241,plain,
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD9]) ).
cnf(c_242,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD8]) ).
cnf(c_243,plain,
( perp(A,B,D,C)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD7]) ).
cnf(c_245,plain,
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD5]) ).
cnf(c_246,plain,
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD4]) ).
cnf(c_247,plain,
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD3]) ).
cnf(c_248,plain,
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD2]) ).
cnf(c_249,plain,
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD1]) ).
cnf(c_264,plain,
( ~ cong(A,B,A,C)
| perp(B,C,C,C)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_142]) ).
cnf(c_289,plain,
( midp(A,D,D)
| ~ para(B,D,C,D)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_191]) ).
cnf(c_290,plain,
( para(B,B,C,C)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_192]) ).
cnf(c_292,plain,
( perp(B,A,A,B)
| ~ cyclic(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_198]) ).
cnf(c_293,plain,
( perp(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_199]) ).
cnf(c_295,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_207]) ).
cnf(c_298,plain,
( cyclic(B,C,D,D)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_234]) ).
cnf(c_299,plain,
( cyclic(B,C,C,D)
| ~ cong(A,B,A,D)
| ~ cong(A,B,A,C) ),
inference(factor,[status(thm)],[c_238]) ).
cnf(c_302,plain,
( para(A,B,A,B)
| ~ perp(A,B,A,B) ),
inference(factor,[status(thm)],[c_241]) ).
cnf(c_303,plain,
( coll(C,C,A)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_247]) ).
cnf(c_311,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_295]) ).
cnf(c_312,plain,
( cyclic(B,C,C,C)
| ~ cong(A,B,A,C) ),
inference(factor,[status(thm)],[c_299]) ).
cnf(c_346,plain,
coll(sK4,sK3,sK2),
inference(resolve,[status(thm)],[c_186,c_150]) ).
cnf(c_347,plain,
cong(sK4,sK3,sK4,sK2),
inference(resolve,[status(thm)],[c_187,c_150]) ).
cnf(c_348,plain,
( midp(sK4,A,B)
| ~ para(sK3,B,sK2,A)
| ~ para(sK3,A,sK2,B) ),
inference(resolve,[status(thm)],[c_191,c_150]) ).
cnf(c_351,plain,
( para(A,sK3,B,sK2)
| ~ midp(sK4,A,B) ),
inference(resolve,[status(thm)],[c_192,c_150]) ).
cnf(c_356,plain,
( midp(A,sK3,B)
| ~ coll(A,sK3,B)
| ~ para(sK4,A,sK2,B) ),
inference(resolve,[status(thm)],[c_205,c_150]) ).
cnf(c_357,plain,
( para(sK4,A,sK2,B)
| ~ midp(A,sK3,B) ),
inference(resolve,[status(thm)],[c_206,c_150]) ).
cnf(c_358,plain,
( para(A,sK4,B,sK2)
| ~ midp(A,sK3,B) ),
inference(resolve,[status(thm)],[c_206,c_150]) ).
cnf(c_363,plain,
eqangle(sK0,sK4,sK0,sK4,sK4,sK2,sK4,sK5),
inference(resolve,[status(thm)],[c_230,c_149]) ).
cnf(c_364,plain,
eqangle(sK1,sK4,sK1,sK4,sK4,sK3,sK4,sK5),
inference(resolve,[status(thm)],[c_230,c_148]) ).
cnf(c_366,plain,
eqangle(sK1,sK4,sK4,sK5,sK1,sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_231,c_148]) ).
cnf(c_367,plain,
eqangle(sK4,sK2,sK0,sK4,sK4,sK5,sK0,sK4),
inference(resolve,[status(thm)],[c_232,c_149]) ).
cnf(c_368,plain,
eqangle(sK4,sK3,sK1,sK4,sK4,sK5,sK1,sK4),
inference(resolve,[status(thm)],[c_232,c_148]) ).
cnf(c_370,plain,
eqangle(sK4,sK1,sK4,sK3,sK1,sK4,sK4,sK5),
inference(resolve,[status(thm)],[c_233,c_148]) ).
cnf(c_371,plain,
midp(sK4,sK2,sK3),
inference(resolve,[status(thm)],[c_239,c_150]) ).
cnf(c_379,plain,
coll(sK2,sK2,sK4),
inference(resolve,[status(thm)],[c_346,c_303]) ).
cnf(c_46178,plain,
( ~ cong(sK4,sK3,sK4,sK2)
| perp(sK3,sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_346,c_264]) ).
cnf(c_391,plain,
perp(sK3,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_347,c_46178]) ).
cnf(c_392,plain,
coll(sK4,sK2,sK3),
inference(resolve,[status(thm)],[c_346,c_249]) ).
cnf(c_393,plain,
coll(sK3,sK4,sK2),
inference(resolve,[status(thm)],[c_346,c_248]) ).
cnf(c_423,plain,
( para(A,sK4,B,sK3)
| ~ midp(A,sK2,B) ),
inference(resolve,[status(thm)],[c_371,c_206]) ).
cnf(c_424,plain,
( para(sK4,A,sK3,B)
| ~ midp(A,sK2,B) ),
inference(resolve,[status(thm)],[c_371,c_206]) ).
cnf(c_431,plain,
cong(sK4,sK2,sK4,sK3),
inference(resolve,[status(thm)],[c_371,c_187]) ).
cnf(c_458,plain,
coll(sK4,sK4,sK2),
inference(resolve,[status(thm)],[c_379,c_303]) ).
cnf(c_473,plain,
coll(sK2,sK4,sK2),
inference(resolve,[status(thm)],[c_379,c_249]) ).
cnf(c_497,plain,
coll(sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_392,c_303]) ).
cnf(c_46179,plain,
( ~ cong(sK4,sK2,sK4,sK3)
| perp(sK2,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_392,c_264]) ).
cnf(c_509,plain,
perp(sK2,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_431,c_46179]) ).
cnf(c_510,plain,
coll(sK2,sK4,sK3),
inference(resolve,[status(thm)],[c_392,c_248]) ).
cnf(c_511,plain,
( coll(A,sK3,sK4)
| ~ coll(sK4,sK2,A) ),
inference(resolve,[status(thm)],[c_392,c_247]) ).
cnf(c_512,plain,
( coll(sK3,A,sK4)
| ~ coll(sK4,sK2,A) ),
inference(resolve,[status(thm)],[c_392,c_247]) ).
cnf(c_529,plain,
coll(sK2,sK2,sK3),
inference(resolve,[status(thm)],[c_393,c_303]) ).
cnf(c_582,plain,
coll(sK4,sK2,sK4),
inference(resolve,[status(thm)],[c_458,c_249]) ).
cnf(c_607,plain,
coll(sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_473,c_303]) ).
cnf(c_628,plain,
( midp(sK2,sK4,sK2)
| ~ cong(sK2,sK4,sK2,sK2) ),
inference(resolve,[status(thm)],[c_473,c_188]) ).
cnf(c_664,plain,
coll(sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_497,c_249]) ).
cnf(c_688,plain,
coll(sK3,sK3,sK2),
inference(resolve,[status(thm)],[c_510,c_303]) ).
cnf(c_740,plain,
coll(sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_529,c_249]) ).
cnf(c_747,plain,
( midp(sK2,sK2,sK3)
| ~ cong(sK2,sK2,sK2,sK3) ),
inference(resolve,[status(thm)],[c_529,c_188]) ).
cnf(c_816,plain,
( coll(A,sK4,sK4)
| ~ coll(sK4,sK2,A) ),
inference(resolve,[status(thm)],[c_582,c_247]) ).
cnf(c_868,plain,
( midp(sK2,sK2,sK2)
| ~ cong(sK2,sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_607,c_188]) ).
cnf(c_963,plain,
coll(sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_664,c_303]) ).
cnf(c_976,plain,
( ~ cong(sK3,sK4,sK3,sK3)
| perp(sK4,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_664,c_264]) ).
cnf(c_977,plain,
coll(sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_664,c_248]) ).
cnf(c_1018,plain,
coll(sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_688,c_249]) ).
cnf(c_1025,plain,
( midp(sK3,sK3,sK2)
| ~ cong(sK3,sK3,sK3,sK2) ),
inference(resolve,[status(thm)],[c_688,c_188]) ).
cnf(c_1092,plain,
coll(sK3,sK2,sK2),
inference(resolve,[status(thm)],[c_740,c_248]) ).
cnf(c_1261,plain,
( midp(sK3,sK3,sK3)
| ~ cong(sK3,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_963,c_188]) ).
cnf(c_1301,plain,
( midp(sK4,sK3,sK3)
| ~ cong(sK4,sK3,sK4,sK3) ),
inference(resolve,[status(thm)],[c_977,c_188]) ).
cnf(c_1329,plain,
coll(sK2,sK3,sK3),
inference(resolve,[status(thm)],[c_1018,c_248]) ).
cnf(c_1381,plain,
( midp(sK3,sK2,sK2)
| ~ cong(sK3,sK2,sK3,sK2) ),
inference(resolve,[status(thm)],[c_1092,c_188]) ).
cnf(c_1461,plain,
( midp(sK2,sK3,sK3)
| ~ cong(sK2,sK3,sK2,sK3) ),
inference(resolve,[status(thm)],[c_1329,c_188]) ).
cnf(c_1482,plain,
cyclic(sK3,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_347,c_312]) ).
cnf(c_1654,plain,
( para(sK3,sK2,A,B)
| ~ perp(sK2,sK2,A,B) ),
inference(resolve,[status(thm)],[c_391,c_241]) ).
cnf(c_1657,plain,
( cong(sK3,sK2,sK3,sK2)
| ~ midp(sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_391,c_200]) ).
cnf(c_1750,plain,
cyclic(sK2,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_431,c_312]) ).
cnf(c_1865,plain,
( cong(sK2,sK3,sK2,sK3)
| ~ midp(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_509,c_200]) ).
cnf(c_1902,plain,
( cong(sK3,sK2,sK2,sK2)
| ~ eqangle(sK2,sK3,sK2,sK2,sK2,sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_1482,c_311]) ).
cnf(c_1903,plain,
cyclic(sK2,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_1482,c_298]) ).
cnf(c_1911,plain,
cyclic(sK2,sK3,sK2,sK2),
inference(resolve,[status(thm)],[c_1482,c_235]) ).
cnf(c_2001,plain,
cyclic(sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_1750,c_298]) ).
cnf(c_2009,plain,
cyclic(sK3,sK2,sK3,sK3),
inference(resolve,[status(thm)],[c_1750,c_235]) ).
cnf(c_2057,plain,
( cong(sK2,sK2,sK2,sK2)
| ~ eqangle(sK2,sK2,sK2,sK2,sK2,sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_1903,c_311]) ).
cnf(c_2065,plain,
eqangle(sK2,sK2,sK2,sK2,sK2,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_1903,c_210]) ).
cnf(c_2088,plain,
cong(sK2,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_2065,c_2057]) ).
cnf(c_2090,plain,
midp(sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_2088,c_868]) ).
cnf(c_2091,plain,
cong(sK3,sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_2090,c_1657]) ).
cnf(c_2095,plain,
midp(sK3,sK2,sK2),
inference(resolve,[status(thm)],[c_2091,c_1381]) ).
cnf(c_2224,plain,
cyclic(sK2,sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_1911,c_236]) ).
cnf(c_2295,plain,
( cong(sK3,sK3,sK3,sK3)
| ~ eqangle(sK3,sK3,sK3,sK3,sK3,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_2001,c_311]) ).
cnf(c_2303,plain,
eqangle(sK3,sK3,sK3,sK3,sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_2001,c_210]) ).
cnf(c_2326,plain,
cong(sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_2303,c_2295]) ).
cnf(c_2328,plain,
midp(sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_2326,c_1261]) ).
cnf(c_2329,plain,
cong(sK2,sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_2328,c_1865]) ).
cnf(c_2333,plain,
midp(sK2,sK3,sK3),
inference(resolve,[status(thm)],[c_2329,c_1461]) ).
cnf(c_2470,plain,
cyclic(sK3,sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_2009,c_236]) ).
cnf(c_2667,plain,
( perp(sK2,sK3,sK3,sK2)
| ~ cyclic(sK3,sK3,sK2,sK2) ),
inference(resolve,[status(thm)],[c_2091,c_292]) ).
cnf(c_2816,plain,
cyclic(sK2,sK2,sK2,sK3),
inference(resolve,[status(thm)],[c_2224,c_237]) ).
cnf(c_2988,plain,
( perp(sK3,sK2,sK2,sK3)
| ~ cyclic(sK2,sK2,sK3,sK3) ),
inference(resolve,[status(thm)],[c_2329,c_292]) ).
cnf(c_3138,plain,
cyclic(sK3,sK3,sK3,sK2),
inference(resolve,[status(thm)],[c_2470,c_237]) ).
cnf(c_3209,plain,
cyclic(sK2,sK2,sK3,sK3),
inference(resolve,[status(thm)],[c_2816,c_298]) ).
cnf(c_3242,plain,
perp(sK3,sK2,sK2,sK3),
inference(resolve,[status(thm)],[c_3209,c_2988]) ).
cnf(c_3305,plain,
cyclic(sK3,sK3,sK2,sK2),
inference(resolve,[status(thm)],[c_3138,c_298]) ).
cnf(c_3338,plain,
perp(sK2,sK3,sK3,sK2),
inference(resolve,[status(thm)],[c_3305,c_2667]) ).
cnf(c_3417,plain,
perp(sK3,sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_3242,c_243]) ).
cnf(c_3486,plain,
perp(sK2,sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_3338,c_243]) ).
cnf(c_3595,plain,
para(sK3,sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_3417,c_302]) ).
cnf(c_3603,plain,
( cong(sK3,sK3,sK3,sK2)
| ~ midp(sK2,sK3,sK2) ),
inference(resolve,[status(thm)],[c_3417,c_200]) ).
cnf(c_3651,plain,
para(sK2,sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_3486,c_302]) ).
cnf(c_3750,plain,
( midp(A,sK2,sK2)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_3595,c_289]) ).
cnf(c_3786,plain,
( midp(A,sK3,sK3)
| ~ midp(A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_3651,c_289]) ).
cnf(c_3930,plain,
para(sK4,sK2,sK2,sK3),
inference(resolve,[status(thm)],[c_357,c_2333]) ).
cnf(c_3936,plain,
para(sK4,sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_3930,c_246]) ).
cnf(c_3937,plain,
para(sK2,sK3,sK4,sK2),
inference(resolve,[status(thm)],[c_3930,c_245]) ).
cnf(c_3996,plain,
para(sK3,sK2,sK4,sK2),
inference(resolve,[status(thm)],[c_3936,c_245]) ).
cnf(c_4022,plain,
para(sK2,sK3,sK2,sK4),
inference(resolve,[status(thm)],[c_3937,c_246]) ).
cnf(c_4122,plain,
( midp(A,sK2,sK2)
| ~ midp(A,sK3,sK4) ),
inference(resolve,[status(thm)],[c_3996,c_289]) ).
cnf(c_4125,plain,
para(sK3,sK2,sK2,sK4),
inference(resolve,[status(thm)],[c_3996,c_246]) ).
cnf(c_4162,plain,
para(sK2,sK4,sK2,sK3),
inference(resolve,[status(thm)],[c_4022,c_245]) ).
cnf(c_46180,plain,
( midp(A,sK4,sK3)
| ~ para(sK2,sK4,sK2,sK3)
| ~ midp(A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_4022,c_191]) ).
cnf(c_4169,plain,
( midp(A,sK4,sK3)
| ~ midp(A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_4162,c_46180]) ).
cnf(c_4459,plain,
midp(sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_4169,c_2095]) ).
cnf(c_4493,plain,
cong(sK3,sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_4459,c_187]) ).
cnf(c_4523,plain,
perp(sK4,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_4493,c_976]) ).
cnf(c_46181,plain,
( cong(sK4,sK3,sK4,sK3)
| ~ midp(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_4523,c_200]) ).
cnf(c_4802,plain,
cong(sK4,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_2328,c_46181]) ).
cnf(c_4834,plain,
midp(sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_4802,c_1301]) ).
cnf(c_4837,plain,
midp(sK4,sK2,sK2),
inference(resolve,[status(thm)],[c_4834,c_3750]) ).
cnf(c_4928,plain,
midp(sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_4837,c_4169]) ).
cnf(c_4929,plain,
para(sK2,sK3,sK2,sK2),
inference(resolve,[status(thm)],[c_4837,c_351]) ).
cnf(c_5040,plain,
midp(sK4,sK3,sK4),
inference(resolve,[status(thm)],[c_4928,c_239]) ).
cnf(c_5079,plain,
para(sK4,sK4,sK2,sK4),
inference(resolve,[status(thm)],[c_5040,c_357]) ).
cnf(c_5882,plain,
eqangle(sK2,sK3,A,B,sK2,sK2,A,B),
inference(resolve,[status(thm)],[c_4929,c_211]) ).
cnf(c_5905,plain,
cong(sK3,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_5882,c_1902]) ).
cnf(c_6166,plain,
( midp(sK4,sK4,sK2)
| ~ para(sK3,sK4,sK2,sK2) ),
inference(resolve,[status(thm)],[c_348,c_4125]) ).
cnf(c_6172,plain,
para(sK4,sK4,sK4,sK2),
inference(resolve,[status(thm)],[c_5079,c_246]) ).
cnf(c_6772,plain,
cong(sK2,sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_5905,c_227]) ).
cnf(c_6961,plain,
para(sK4,sK2,sK4,sK4),
inference(resolve,[status(thm)],[c_6172,c_245]) ).
cnf(c_46182,plain,
( midp(A,sK2,sK4)
| ~ para(sK4,sK2,sK4,sK4)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_6172,c_191]) ).
cnf(c_6968,plain,
( midp(A,sK2,sK4)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_6961,c_46182]) ).
cnf(c_7449,plain,
cong(sK2,sK2,sK2,sK3),
inference(resolve,[status(thm)],[c_6772,c_228]) ).
cnf(c_7466,plain,
midp(sK2,sK2,sK3),
inference(resolve,[status(thm)],[c_7449,c_747]) ).
cnf(c_7509,plain,
midp(sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_7466,c_239]) ).
cnf(c_7546,plain,
cong(sK3,sK3,sK3,sK2),
inference(resolve,[status(thm)],[c_7509,c_3603]) ).
cnf(c_7557,plain,
midp(sK3,sK3,sK2),
inference(resolve,[status(thm)],[c_7546,c_1025]) ).
cnf(c_7627,plain,
para(sK2,sK4,sK2,sK2),
inference(resolve,[status(thm)],[c_7509,c_358]) ).
cnf(c_7681,plain,
para(sK3,sK4,sK2,sK2),
inference(resolve,[status(thm)],[c_7557,c_358]) ).
cnf(c_7737,plain,
midp(sK4,sK4,sK2),
inference(resolve,[status(thm)],[c_7681,c_6166]) ).
cnf(c_7785,plain,
cong(sK4,sK4,sK4,sK2),
inference(resolve,[status(thm)],[c_7737,c_187]) ).
cnf(c_8201,plain,
( para(sK0,sK4,sK0,sK4)
| ~ para(sK4,sK2,sK4,sK5) ),
inference(resolve,[status(thm)],[c_363,c_183]) ).
cnf(c_8429,plain,
( para(sK1,sK4,sK1,sK4)
| ~ para(sK4,sK3,sK4,sK5) ),
inference(resolve,[status(thm)],[c_364,c_183]) ).
cnf(c_8985,plain,
eqangle(sK2,sK4,A,B,sK2,sK2,A,B),
inference(resolve,[status(thm)],[c_7627,c_211]) ).
cnf(c_9080,plain,
( para(sK1,sK4,sK4,sK5)
| ~ para(sK1,sK4,sK4,sK3) ),
inference(resolve,[status(thm)],[c_366,c_183]) ).
cnf(c_9112,plain,
cyclic(sK4,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_7785,c_312]) ).
cnf(c_9437,plain,
para(sK4,sK2,sK4,sK5),
inference(resolve,[status(thm)],[c_367,c_212]) ).
cnf(c_9440,plain,
para(sK0,sK4,sK0,sK4),
inference(resolve,[status(thm)],[c_9437,c_8201]) ).
cnf(c_9609,plain,
para(sK4,sK3,sK4,sK5),
inference(resolve,[status(thm)],[c_368,c_212]) ).
cnf(c_9612,plain,
para(sK1,sK4,sK1,sK4),
inference(resolve,[status(thm)],[c_9609,c_8429]) ).
cnf(c_46183,plain,
( cong(sK4,sK2,sK2,sK2)
| ~ eqangle(sK2,sK4,sK2,sK2,sK2,sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_9112,c_311]) ).
cnf(c_9692,plain,
cong(sK4,sK2,sK2,sK2),
inference(resolve,[status(thm)],[c_8985,c_46183]) ).
cnf(c_46184,plain,
( perp(sK2,sK4,sK4,sK2)
| ~ cong(sK4,sK2,sK2,sK2) ),
inference(resolve,[status(thm)],[c_9112,c_292]) ).
cnf(c_9698,plain,
perp(sK2,sK4,sK4,sK2),
inference(resolve,[status(thm)],[c_9692,c_46184]) ).
cnf(c_9838,plain,
para(sK4,sK5,sK4,sK2),
inference(resolve,[status(thm)],[c_9437,c_245]) ).
cnf(c_9848,plain,
coll(sK4,sK2,sK5),
inference(resolve,[status(thm)],[c_9437,c_189]) ).
cnf(c_9868,plain,
coll(sK5,sK4,sK4),
inference(resolve,[status(thm)],[c_9848,c_816]) ).
cnf(c_9869,plain,
coll(sK3,sK5,sK4),
inference(resolve,[status(thm)],[c_9848,c_512]) ).
cnf(c_9870,plain,
coll(sK5,sK3,sK4),
inference(resolve,[status(thm)],[c_9848,c_511]) ).
cnf(c_9958,plain,
( para(sK4,sK1,sK4,sK3)
| ~ para(sK1,sK4,sK4,sK5) ),
inference(resolve,[status(thm)],[c_370,c_183]) ).
cnf(c_10064,plain,
( midp(sK5,sK4,sK4)
| ~ cong(sK5,sK4,sK5,sK4) ),
inference(resolve,[status(thm)],[c_9868,c_188]) ).
cnf(c_10095,plain,
coll(sK3,sK4,sK5),
inference(resolve,[status(thm)],[c_9869,c_249]) ).
cnf(c_10119,plain,
( midp(sK5,sK3,sK4)
| ~ para(sK4,sK5,sK2,sK4) ),
inference(resolve,[status(thm)],[c_9870,c_356]) ).
cnf(c_10390,plain,
coll(sK5,sK5,sK3),
inference(resolve,[status(thm)],[c_10095,c_303]) ).
cnf(c_11054,plain,
coll(sK5,sK3,sK5),
inference(resolve,[status(thm)],[c_10390,c_249]) ).
cnf(c_11387,plain,
coll(sK3,sK5,sK5),
inference(resolve,[status(thm)],[c_11054,c_248]) ).
cnf(c_11486,plain,
( midp(sK3,sK5,sK5)
| ~ cong(sK3,sK5,sK3,sK5) ),
inference(resolve,[status(thm)],[c_11387,c_188]) ).
cnf(c_11502,plain,
( midp(A,sK4,sK4)
| ~ midp(A,sK0,sK0) ),
inference(resolve,[status(thm)],[c_9440,c_289]) ).
cnf(c_11505,plain,
para(sK0,sK4,sK4,sK0),
inference(resolve,[status(thm)],[c_9440,c_246]) ).
cnf(c_11509,plain,
coll(sK0,sK4,sK4),
inference(resolve,[status(thm)],[c_9440,c_189]) ).
cnf(c_11531,plain,
coll(sK4,sK4,sK0),
inference(resolve,[status(thm)],[c_11509,c_303]) ).
cnf(c_11578,plain,
coll(sK0,sK0,sK4),
inference(resolve,[status(thm)],[c_11531,c_303]) ).
cnf(c_11827,plain,
coll(sK0,sK4,sK0),
inference(resolve,[status(thm)],[c_11578,c_249]) ).
cnf(c_12029,plain,
coll(sK0,sK0,sK0),
inference(resolve,[status(thm)],[c_11827,c_303]) ).
cnf(c_12742,plain,
( midp(sK0,sK0,sK0)
| ~ cong(sK0,sK0,sK0,sK0) ),
inference(resolve,[status(thm)],[c_12029,c_188]) ).
cnf(c_13222,plain,
( midp(A,sK4,sK4)
| ~ midp(A,sK1,sK1) ),
inference(resolve,[status(thm)],[c_9612,c_289]) ).
cnf(c_13225,plain,
para(sK1,sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_9612,c_246]) ).
cnf(c_13229,plain,
coll(sK1,sK4,sK4),
inference(resolve,[status(thm)],[c_9612,c_189]) ).
cnf(c_13249,plain,
coll(sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_13229,c_303]) ).
cnf(c_13296,plain,
coll(sK1,sK1,sK4),
inference(resolve,[status(thm)],[c_13249,c_303]) ).
cnf(c_13545,plain,
coll(sK1,sK4,sK1),
inference(resolve,[status(thm)],[c_13296,c_249]) ).
cnf(c_13759,plain,
coll(sK1,sK1,sK1),
inference(resolve,[status(thm)],[c_13545,c_303]) ).
cnf(c_14503,plain,
( midp(sK1,sK1,sK1)
| ~ cong(sK1,sK1,sK1,sK1) ),
inference(resolve,[status(thm)],[c_13759,c_188]) ).
cnf(c_46185,plain,
( cong(sK2,sK4,sK2,sK2)
| ~ midp(sK4,sK4,sK2) ),
inference(resolve,[status(thm)],[c_9698,c_200]) ).
cnf(c_14851,plain,
cong(sK2,sK4,sK2,sK2),
inference(resolve,[status(thm)],[c_7737,c_46185]) ).
cnf(c_14875,plain,
midp(sK2,sK4,sK2),
inference(resolve,[status(thm)],[c_14851,c_628]) ).
cnf(c_15208,plain,
para(sK4,sK5,sK2,sK4),
inference(resolve,[status(thm)],[c_9838,c_246]) ).
cnf(c_15224,plain,
midp(sK5,sK3,sK4),
inference(resolve,[status(thm)],[c_15208,c_10119]) ).
cnf(c_15225,plain,
midp(sK5,sK2,sK2),
inference(resolve,[status(thm)],[c_15224,c_4122]) ).
cnf(c_15257,plain,
cong(sK5,sK3,sK5,sK4),
inference(resolve,[status(thm)],[c_15224,c_187]) ).
cnf(c_15294,plain,
midp(sK5,sK3,sK3),
inference(resolve,[status(thm)],[c_15225,c_3786]) ).
cnf(c_15445,plain,
cong(sK5,sK3,sK5,sK3),
inference(resolve,[status(thm)],[c_15294,c_187]) ).
cnf(c_15464,plain,
para(sK4,sK0,sK0,sK4),
inference(resolve,[status(thm)],[c_11505,c_245]) ).
cnf(c_15634,plain,
para(sK4,sK1,sK1,sK4),
inference(resolve,[status(thm)],[c_13225,c_245]) ).
cnf(c_16116,plain,
cong(sK5,sK3,sK4,sK5),
inference(resolve,[status(thm)],[c_15257,c_228]) ).
cnf(c_16483,plain,
cong(sK5,sK3,sK3,sK5),
inference(resolve,[status(thm)],[c_15445,c_228]) ).
cnf(c_16515,plain,
para(sK4,sK0,sK4,sK0),
inference(resolve,[status(thm)],[c_15464,c_246]) ).
cnf(c_16625,plain,
para(sK4,sK1,sK4,sK1),
inference(resolve,[status(thm)],[c_15634,c_246]) ).
cnf(c_16783,plain,
cong(sK4,sK5,sK5,sK3),
inference(resolve,[status(thm)],[c_16116,c_227]) ).
cnf(c_16931,plain,
cong(sK3,sK5,sK5,sK3),
inference(resolve,[status(thm)],[c_16483,c_227]) ).
cnf(c_16935,plain,
( midp(A,sK0,sK0)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_16515,c_289]) ).
cnf(c_16981,plain,
( midp(A,sK1,sK1)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_16625,c_289]) ).
cnf(c_17039,plain,
cong(sK4,sK5,sK3,sK5),
inference(resolve,[status(thm)],[c_16783,c_228]) ).
cnf(c_17338,plain,
cong(sK3,sK5,sK3,sK5),
inference(resolve,[status(thm)],[c_16931,c_228]) ).
cnf(c_17345,plain,
midp(sK3,sK5,sK5),
inference(resolve,[status(thm)],[c_17338,c_11486]) ).
cnf(c_17440,plain,
perp(sK4,sK3,sK5,sK5),
inference(resolve,[status(thm)],[c_17039,c_293]) ).
cnf(c_46186,plain,
( cong(sK4,sK5,sK4,sK5)
| ~ midp(sK3,sK5,sK5) ),
inference(resolve,[status(thm)],[c_17440,c_200]) ).
cnf(c_17775,plain,
cong(sK4,sK5,sK4,sK5),
inference(resolve,[status(thm)],[c_17345,c_46186]) ).
cnf(c_18010,plain,
cong(sK4,sK5,sK5,sK4),
inference(resolve,[status(thm)],[c_17775,c_228]) ).
cnf(c_18235,plain,
cong(sK5,sK4,sK4,sK5),
inference(resolve,[status(thm)],[c_18010,c_227]) ).
cnf(c_18550,plain,
cong(sK5,sK4,sK5,sK4),
inference(resolve,[status(thm)],[c_18235,c_228]) ).
cnf(c_18557,plain,
midp(sK5,sK4,sK4),
inference(resolve,[status(thm)],[c_18550,c_10064]) ).
cnf(c_26458,plain,
midp(sK5,sK0,sK0),
inference(resolve,[status(thm)],[c_16935,c_18557]) ).
cnf(c_26486,plain,
para(sK0,sK0,sK0,sK0),
inference(resolve,[status(thm)],[c_26458,c_290]) ).
cnf(c_26500,plain,
cong(sK5,sK0,sK5,sK0),
inference(resolve,[status(thm)],[c_26458,c_187]) ).
cnf(c_26676,plain,
eqangle(sK0,sK0,A,B,sK0,sK0,A,B),
inference(resolve,[status(thm)],[c_26486,c_211]) ).
cnf(c_26678,plain,
cyclic(sK0,sK0,sK0,sK0),
inference(resolve,[status(thm)],[c_26500,c_312]) ).
cnf(c_46187,plain,
( cong(sK0,sK0,sK0,sK0)
| ~ eqangle(sK0,sK0,sK0,sK0,sK0,sK0,sK0,sK0) ),
inference(resolve,[status(thm)],[c_26678,c_311]) ).
cnf(c_26923,plain,
cong(sK0,sK0,sK0,sK0),
inference(resolve,[status(thm)],[c_26676,c_46187]) ).
cnf(c_26927,plain,
midp(sK0,sK0,sK0),
inference(resolve,[status(thm)],[c_26923,c_12742]) ).
cnf(c_26928,plain,
midp(sK0,sK4,sK4),
inference(resolve,[status(thm)],[c_26927,c_11502]) ).
cnf(c_26973,plain,
midp(sK0,sK2,sK4),
inference(resolve,[status(thm)],[c_26928,c_6968]) ).
cnf(c_27266,plain,
para(sK4,sK0,sK3,sK4),
inference(resolve,[status(thm)],[c_26973,c_424]) ).
cnf(c_28041,plain,
para(sK4,sK0,sK4,sK3),
inference(resolve,[status(thm)],[c_27266,c_246]) ).
cnf(c_28784,plain,
para(sK4,sK3,sK4,sK0),
inference(resolve,[status(thm)],[c_28041,c_245]) ).
cnf(c_46188,plain,
( midp(A,sK3,sK0)
| ~ para(sK4,sK3,sK4,sK0)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_28041,c_191]) ).
cnf(c_28791,plain,
( midp(A,sK3,sK0)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_28784,c_46188]) ).
cnf(c_29442,plain,
midp(sK0,sK1,sK1),
inference(resolve,[status(thm)],[c_16981,c_26928]) ).
cnf(c_29471,plain,
para(sK1,sK1,sK1,sK1),
inference(resolve,[status(thm)],[c_29442,c_290]) ).
cnf(c_29485,plain,
cong(sK0,sK1,sK0,sK1),
inference(resolve,[status(thm)],[c_29442,c_187]) ).
cnf(c_29711,plain,
eqangle(sK1,sK1,A,B,sK1,sK1,A,B),
inference(resolve,[status(thm)],[c_29471,c_211]) ).
cnf(c_29713,plain,
cyclic(sK1,sK1,sK1,sK1),
inference(resolve,[status(thm)],[c_29485,c_312]) ).
cnf(c_46189,plain,
( cong(sK1,sK1,sK1,sK1)
| ~ eqangle(sK1,sK1,sK1,sK1,sK1,sK1,sK1,sK1) ),
inference(resolve,[status(thm)],[c_29713,c_311]) ).
cnf(c_29976,plain,
cong(sK1,sK1,sK1,sK1),
inference(resolve,[status(thm)],[c_29711,c_46189]) ).
cnf(c_29979,plain,
midp(sK1,sK1,sK1),
inference(resolve,[status(thm)],[c_29976,c_14503]) ).
cnf(c_29980,plain,
midp(sK1,sK4,sK4),
inference(resolve,[status(thm)],[c_29979,c_13222]) ).
cnf(c_30026,plain,
midp(sK1,sK2,sK4),
inference(resolve,[status(thm)],[c_29980,c_6968]) ).
cnf(c_30346,plain,
para(sK1,sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_30026,c_423]) ).
cnf(c_30364,plain,
para(sK1,sK4,sK4,sK5),
inference(resolve,[status(thm)],[c_30346,c_9080]) ).
cnf(c_30366,plain,
para(sK4,sK1,sK4,sK3),
inference(resolve,[status(thm)],[c_30364,c_9958]) ).
cnf(c_31020,plain,
para(sK4,sK3,sK4,sK1),
inference(resolve,[status(thm)],[c_30366,c_245]) ).
cnf(c_46190,plain,
( midp(A,sK3,sK1)
| ~ para(sK4,sK3,sK4,sK1)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_30366,c_191]) ).
cnf(c_31027,plain,
( midp(A,sK3,sK1)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_31020,c_46190]) ).
cnf(c_33063,plain,
midp(sK1,sK3,sK0),
inference(resolve,[status(thm)],[c_28791,c_29980]) ).
cnf(c_33074,plain,
para(sK4,sK1,sK2,sK0),
inference(resolve,[status(thm)],[c_33063,c_357]) ).
cnf(c_38200,plain,
midp(sK0,sK3,sK1),
inference(resolve,[status(thm)],[c_31027,c_26928]) ).
cnf(c_38232,plain,
para(sK4,sK0,sK2,sK1),
inference(resolve,[status(thm)],[c_38200,c_357]) ).
cnf(c_46191,plain,
( midp(A,sK1,sK0)
| ~ para(sK4,sK1,sK2,sK0)
| ~ midp(A,sK4,sK2) ),
inference(resolve,[status(thm)],[c_38232,c_191]) ).
cnf(c_38546,plain,
( midp(A,sK1,sK0)
| ~ midp(A,sK4,sK2) ),
inference(resolve,[status(thm)],[c_33074,c_46191]) ).
cnf(c_45420,plain,
midp(sK2,sK1,sK0),
inference(resolve,[status(thm)],[c_38546,c_14875]) ).
cnf(c_45493,plain,
cong(sK2,sK1,sK2,sK0),
inference(resolve,[status(thm)],[c_45420,c_187]) ).
cnf(c_45653,plain,
cong(sK2,sK1,sK0,sK2),
inference(resolve,[status(thm)],[c_45493,c_228]) ).
cnf(c_45823,plain,
cong(sK0,sK2,sK2,sK1),
inference(resolve,[status(thm)],[c_45653,c_227]) ).
cnf(c_45919,plain,
cong(sK0,sK2,sK1,sK2),
inference(resolve,[status(thm)],[c_45823,c_228]) ).
cnf(c_45981,plain,
perp(sK0,sK1,sK2,sK2),
inference(resolve,[status(thm)],[c_45919,c_293]) ).
cnf(c_46054,plain,
perp(sK2,sK2,sK0,sK1),
inference(resolve,[status(thm)],[c_45981,c_242]) ).
cnf(c_46111,plain,
para(sK3,sK2,sK0,sK1),
inference(resolve,[status(thm)],[c_46054,c_1654]) ).
cnf(c_46150,plain,
para(sK0,sK1,sK3,sK2),
inference(resolve,[status(thm)],[c_46111,c_245]) ).
cnf(c_46192,plain,
para(sK0,sK1,sK2,sK3),
inference(resolve,[status(thm)],[c_46150,c_246]) ).
cnf(c_46177,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_147,c_46192]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO656+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/5.37 % Computer : n014.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Fri Sep 25 13:46:37 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.38 % Process 362700 was started by sandbox2 on n014,
% 0.09/5.38 % Fri Sep 25 13:46:37 2026
% 0.09/5.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/5.40
% 0.14/5.40 % From the command line: assign(max_seconds, 300).
% 33.39/10.22
% 33.39/10.22 % given #500 (T,wt=10): 6922 perp(c1,c1,c4,c4). [resolve(5958,a,242,a)].
% 33.39/10.22
% 33.39/10.22 % given #1000 (W,wt=10): 20456 para(c4,c2,c2,c3). [resolve(20237,a,424,a)].
% 33.39/10.22
% 33.39/10.22 % given #1500 (T,wt=9): 25916 midp(c3,c4,c3). [back_unit_del(10516),unit_del(a,25898)].
% 33.39/10.22
% 33.39/10.22 % given #2000 (T,wt=10): 31338 cong(c3,c6,c6,c2). [resolve(30795,a,227,a)].
% 33.39/10.22
% 33.39/10.22 % given #2500 (A,wt=23): 782 -para(A,c1,B,c4) | -coll(c2,A,B) | eqratio(c2,A,A,B,c2,c1,c1,c4). [resolve(543,a,190,c)].
% 33.39/10.22
% 33.39/10.22 % given #3000 (T,wt=13): 29801 -midp(A,c1,c2) | midp(A,c6,c6). [resolve(29564,a,289,b)].
% 33.39/10.22
% 33.39/10.22 % given #3500 (W,wt=10): 42024 perp(c3,c3,c3,c6). [resolve(41754,a,243,a)].
% 33.39/10.22
% 33.39/10.22 % given #4000 (T,wt=10): 44682 cyclic(c2,c2,c1,c5). [resolve(44457,a,236,a)].
% 33.39/10.22
% 33.39/10.22 % SZS status Theorem for theBenchmark
% 33.39/10.22
% 33.39/10.22 % Proof 1 at 3.66 (+ 1.09) seconds.
% 33.39/10.22 % Length of proof is 326.
% 33.39/10.22 % Level of proof is 57.
% 33.39/10.22 % Maximum clause weight is 34.000.
% 33.39/10.22 % Given clauses 4403.
% 33.39/10.22
% 33.39/10.22 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------