%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO607+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 : n016.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:12 AM UTC 2026
% Result : Theorem 52.88s 14.62s
% Output : CNFRefutation 52.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 36
% Syntax : Number of formulae : 283 ( 141 unt; 0 def)
% Number of atoms : 497 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 359 ( 145 ~; 141 |; 36 &)
% ( 0 <=>; 37 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 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 : 450 ( 42 sgn 162 !; 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(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(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(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(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(ruleD52,axiom,
! [A,B,C,M] :
( ( midp(M,A,C)
& perp(A,B,B,C) )
=> cong(A,M,B,M) ),
file('theBenchmark.p',ruleD52) ).
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(exemplo6GDDFULL618069,conjecture,
! [A,B,C,D,E,F] :
( ( circle(F,B,D,C)
& circle(E,A,C,D)
& perp(D,A,D,B)
& midp(C,B,A) )
=> perp(E,D,D,F) ),
file('theBenchmark.p',exemplo6GDDFULL618069) ).
fof(exemplo6GDDFULL618069_neg,negated_conjecture,
~ ! [A,B,C,D,E,F] :
( ( circle(F,B,D,C)
& circle(E,A,C,D)
& perp(D,A,D,B)
& midp(C,B,A) )
=> perp(E,D,D,F) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL618069]) ).
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_172,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] :
( ~ perp(E,D,D,F)
& circle(F,B,D,C)
& circle(E,A,C,D)
& perp(D,A,D,B)
& midp(C,B,A) ),
inference(fof_nnf,[status(thm)],[exemplo6GDDFULL618069_neg]) ).
fof(sk_exemplo6GDDFULL618069_neg,plain,
( ~ perp(sK0,sK1,sK1,sK2)
& circle(sK2,sK4,sK1,sK5)
& circle(sK0,sK3,sK5,sK1)
& perp(sK1,sK3,sK1,sK4)
& midp(sK5,sK4,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK4,sK3,sK1,sK0,sK2]),skolemize(A,sK3),skolemize(B,sK4),skolemize(C,sK5),skolemize(D,sK1),skolemize(E,sK0),skolemize(F,sK2)],[nnf_95]) ).
cnf(c_177,negated_conjecture,
~ perp(sK0,sK1,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL618069_neg]) ).
cnf(c_178,negated_conjecture,
perp(sK1,sK3,sK1,sK4),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL618069_neg]) ).
cnf(c_179,negated_conjecture,
midp(sK5,sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL618069_neg]) ).
cnf(c_215,plain,
( coll(A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD69]) ).
cnf(c_216,plain,
( cong(A,B,A,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD68]) ).
cnf(c_217,plain,
( midp(A,B,C)
| ~ coll(A,B,C)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD67]) ).
cnf(c_218,plain,
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD66]) ).
cnf(c_220,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_221,plain,
( para(B,D,C,E)
| ~ midp(A,D,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD63]) ).
cnf(c_227,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_228,plain,
( perp(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD56]) ).
cnf(c_229,plain,
( cong(D,B,D,C)
| ~ perp(D,A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD55]) ).
cnf(c_231,plain,
( cong(A,D,B,D)
| ~ midp(D,A,C)
| ~ perp(A,B,B,C) ),
inference(clausify,[status(thm)],[ruleD52]) ).
cnf(c_235,plain,
( para(A,D,C,E)
| ~ midp(D,B,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD44]) ).
cnf(c_236,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_237,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_239,plain,
( eqangle(C,A,C,B,D,A,D,B)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD41]) ).
cnf(c_240,plain,
( eqangle(A,B,E,F,C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD40]) ).
cnf(c_256,plain,
( cong(C,D,A,B)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD24]) ).
cnf(c_257,plain,
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD23]) ).
cnf(c_261,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_263,plain,
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD17]) ).
cnf(c_264,plain,
( cyclic(B,A,C,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD16]) ).
cnf(c_265,plain,
( cyclic(A,C,B,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD15]) ).
cnf(c_266,plain,
( cyclic(A,B,D,C)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD14]) ).
cnf(c_267,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_268,plain,
( midp(A,C,B)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD11]) ).
cnf(c_269,plain,
( perp(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD10]) ).
cnf(c_270,plain,
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD9]) ).
cnf(c_271,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD8]) ).
cnf(c_272,plain,
( perp(A,B,D,C)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD7]) ).
cnf(c_274,plain,
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD5]) ).
cnf(c_275,plain,
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD4]) ).
cnf(c_276,plain,
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD3]) ).
cnf(c_277,plain,
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD2]) ).
cnf(c_278,plain,
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD1]) ).
cnf(c_293,plain,
( ~ cong(A,B,A,C)
| perp(B,C,C,C)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_172]) ).
cnf(c_318,plain,
( midp(A,D,D)
| ~ para(B,D,C,D)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_220]) ).
cnf(c_321,plain,
( perp(B,A,A,B)
| ~ cyclic(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_227]) ).
cnf(c_322,plain,
( perp(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_228]) ).
cnf(c_323,plain,
( para(A,A,C,C)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_235]) ).
cnf(c_324,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_236]) ).
cnf(c_325,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_236]) ).
cnf(c_327,plain,
( cyclic(B,C,D,D)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_263]) ).
cnf(c_328,plain,
( cyclic(B,C,C,D)
| ~ cong(A,B,A,D)
| ~ cong(A,B,A,C) ),
inference(factor,[status(thm)],[c_267]) ).
cnf(c_331,plain,
( para(A,B,A,B)
| ~ perp(A,B,A,B) ),
inference(factor,[status(thm)],[c_270]) ).
cnf(c_332,plain,
( coll(C,C,A)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_276]) ).
cnf(c_340,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_324]) ).
cnf(c_341,plain,
( cyclic(B,C,C,C)
| ~ cong(A,B,A,C) ),
inference(factor,[status(thm)],[c_328]) ).
cnf(c_446,plain,
coll(sK5,sK4,sK3),
inference(resolve,[status(thm)],[c_215,c_179]) ).
cnf(c_447,plain,
cong(sK5,sK4,sK5,sK3),
inference(resolve,[status(thm)],[c_216,c_179]) ).
cnf(c_451,plain,
( para(A,sK4,B,sK3)
| ~ midp(sK5,A,B) ),
inference(resolve,[status(thm)],[c_221,c_179]) ).
cnf(c_460,plain,
( para(sK5,A,sK3,B)
| ~ midp(A,sK4,B) ),
inference(resolve,[status(thm)],[c_235,c_179]) ).
cnf(c_462,plain,
midp(sK5,sK3,sK4),
inference(resolve,[status(thm)],[c_268,c_179]) ).
cnf(c_475,plain,
perp(sK1,sK3,sK4,sK1),
inference(resolve,[status(thm)],[c_272,c_178]) ).
cnf(c_485,plain,
coll(sK3,sK3,sK5),
inference(resolve,[status(thm)],[c_446,c_332]) ).
cnf(c_23287,plain,
( ~ cong(sK5,sK4,sK5,sK3)
| perp(sK4,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_446,c_293]) ).
cnf(c_497,plain,
perp(sK4,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_447,c_23287]) ).
cnf(c_498,plain,
coll(sK5,sK3,sK4),
inference(resolve,[status(thm)],[c_446,c_278]) ).
cnf(c_499,plain,
coll(sK4,sK5,sK3),
inference(resolve,[status(thm)],[c_446,c_277]) ).
cnf(c_537,plain,
cong(sK5,sK3,sK5,sK4),
inference(resolve,[status(thm)],[c_462,c_216]) ).
cnf(c_579,plain,
coll(sK3,sK5,sK3),
inference(resolve,[status(thm)],[c_485,c_278]) ).
cnf(c_603,plain,
coll(sK4,sK4,sK5),
inference(resolve,[status(thm)],[c_498,c_332]) ).
cnf(c_23288,plain,
( ~ cong(sK5,sK3,sK5,sK4)
| perp(sK3,sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_498,c_293]) ).
cnf(c_615,plain,
perp(sK3,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_537,c_23288]) ).
cnf(c_616,plain,
coll(sK3,sK5,sK4),
inference(resolve,[status(thm)],[c_498,c_277]) ).
cnf(c_635,plain,
coll(sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_499,c_332]) ).
cnf(c_713,plain,
coll(sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_579,c_332]) ).
cnf(c_770,plain,
coll(sK4,sK5,sK4),
inference(resolve,[status(thm)],[c_603,c_278]) ).
cnf(c_794,plain,
coll(sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_616,c_332]) ).
cnf(c_846,plain,
coll(sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_635,c_278]) ).
cnf(c_853,plain,
( midp(sK3,sK3,sK4)
| ~ cong(sK3,sK3,sK3,sK4) ),
inference(resolve,[status(thm)],[c_635,c_217]) ).
cnf(c_970,plain,
( cyclic(A,sK3,sK3,sK3)
| ~ eqangle(sK3,A,sK3,sK3,sK3,A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_713,c_237]) ).
cnf(c_974,plain,
( midp(sK3,sK3,sK3)
| ~ cong(sK3,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_713,c_217]) ).
cnf(c_1069,plain,
coll(sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_770,c_332]) ).
cnf(c_1082,plain,
( ~ cong(sK4,sK5,sK4,sK4)
| perp(sK5,sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_770,c_293]) ).
cnf(c_1083,plain,
coll(sK5,sK4,sK4),
inference(resolve,[status(thm)],[c_770,c_277]) ).
cnf(c_1124,plain,
coll(sK4,sK3,sK4),
inference(resolve,[status(thm)],[c_794,c_278]) ).
cnf(c_1126,plain,
( coll(sK3,A,sK4)
| ~ coll(sK4,sK4,A) ),
inference(resolve,[status(thm)],[c_794,c_276]) ).
cnf(c_1131,plain,
( midp(sK4,sK4,sK3)
| ~ cong(sK4,sK4,sK4,sK3) ),
inference(resolve,[status(thm)],[c_794,c_217]) ).
cnf(c_1198,plain,
coll(sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_846,c_277]) ).
cnf(c_1362,plain,
( coll(A,sK4,sK4)
| ~ coll(sK4,sK4,A) ),
inference(resolve,[status(thm)],[c_1069,c_276]) ).
cnf(c_1367,plain,
( midp(sK4,sK4,sK4)
| ~ cong(sK4,sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_1069,c_217]) ).
cnf(c_1407,plain,
( midp(sK5,sK4,sK4)
| ~ cong(sK5,sK4,sK5,sK4) ),
inference(resolve,[status(thm)],[c_1083,c_217]) ).
cnf(c_1435,plain,
coll(sK3,sK4,sK4),
inference(resolve,[status(thm)],[c_1124,c_277]) ).
cnf(c_1487,plain,
( midp(sK4,sK3,sK3)
| ~ cong(sK4,sK3,sK4,sK3) ),
inference(resolve,[status(thm)],[c_1198,c_217]) ).
cnf(c_1567,plain,
( midp(sK3,sK4,sK4)
| ~ cong(sK3,sK4,sK3,sK4) ),
inference(resolve,[status(thm)],[c_1435,c_217]) ).
cnf(c_1583,plain,
cyclic(sK4,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_447,c_341]) ).
cnf(c_1708,plain,
perp(sK4,sK1,sK1,sK3),
inference(resolve,[status(thm)],[c_475,c_271]) ).
cnf(c_1792,plain,
( cong(sK4,sK3,sK4,sK3)
| ~ midp(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_497,c_229]) ).
cnf(c_1884,plain,
cyclic(sK3,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_537,c_341]) ).
cnf(c_1999,plain,
( cong(sK3,sK4,sK3,sK4)
| ~ midp(sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_615,c_229]) ).
cnf(c_2031,plain,
( cong(sK4,sK3,sK3,sK3)
| ~ eqangle(sK3,sK4,sK3,sK3,sK3,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_1583,c_340]) ).
cnf(c_2032,plain,
cyclic(sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_1583,c_327]) ).
cnf(c_2040,plain,
cyclic(sK3,sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_1583,c_264]) ).
cnf(c_2089,plain,
perp(sK4,sK1,sK3,sK1),
inference(resolve,[status(thm)],[c_1708,c_272]) ).
cnf(c_2093,plain,
( cong(sK4,A,sK1,A)
| ~ midp(A,sK4,sK3) ),
inference(resolve,[status(thm)],[c_1708,c_231]) ).
cnf(c_2094,plain,
( cong(sK4,sK1,sK4,sK3)
| ~ midp(sK1,sK1,sK3) ),
inference(resolve,[status(thm)],[c_1708,c_229]) ).
cnf(c_2188,plain,
cyclic(sK4,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_1884,c_327]) ).
cnf(c_2235,plain,
( cong(sK3,sK3,sK3,sK3)
| ~ eqangle(sK3,sK3,sK3,sK3,sK3,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_2032,c_340]) ).
cnf(c_2243,plain,
eqangle(sK3,sK3,sK3,sK3,sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_2032,c_239]) ).
cnf(c_2266,plain,
cong(sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_2243,c_2235]) ).
cnf(c_2268,plain,
midp(sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_2266,c_974]) ).
cnf(c_2269,plain,
cong(sK4,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_2268,c_1792]) ).
cnf(c_2273,plain,
midp(sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_2269,c_1487]) ).
cnf(c_2285,plain,
para(sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_2268,c_323]) ).
cnf(c_2402,plain,
cyclic(sK3,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_2040,c_265]) ).
cnf(c_2476,plain,
( cong(sK4,sK3,sK4,sK1)
| ~ midp(sK1,sK3,sK1) ),
inference(resolve,[status(thm)],[c_2089,c_229]) ).
cnf(c_2527,plain,
( cong(sK4,sK4,sK4,sK4)
| ~ eqangle(sK4,sK4,sK4,sK4,sK4,sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_2188,c_340]) ).
cnf(c_2535,plain,
eqangle(sK4,sK4,sK4,sK4,sK4,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_2188,c_239]) ).
cnf(c_2558,plain,
cong(sK4,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_2535,c_2527]) ).
cnf(c_2560,plain,
midp(sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_2558,c_1367]) ).
cnf(c_2561,plain,
cong(sK3,sK4,sK3,sK4),
inference(resolve,[status(thm)],[c_2560,c_1999]) ).
cnf(c_2565,plain,
midp(sK3,sK4,sK4),
inference(resolve,[status(thm)],[c_2561,c_1567]) ).
cnf(c_3020,plain,
eqangle(sK3,sK3,A,B,sK3,sK3,A,B),
inference(resolve,[status(thm)],[c_2285,c_240]) ).
cnf(c_3031,plain,
cyclic(sK3,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_2402,c_266]) ).
cnf(c_3210,plain,
( perp(sK4,sK3,sK3,sK4)
| ~ cyclic(sK3,sK3,sK4,sK4) ),
inference(resolve,[status(thm)],[c_2561,c_321]) ).
cnf(c_3425,plain,
cyclic(sK3,sK3,sK4,sK4),
inference(resolve,[status(thm)],[c_3031,c_327]) ).
cnf(c_3458,plain,
perp(sK4,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_3425,c_3210]) ).
cnf(c_3627,plain,
perp(sK4,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_3458,c_272]) ).
cnf(c_3772,plain,
para(sK4,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_3627,c_331]) ).
cnf(c_3780,plain,
( cong(sK4,sK4,sK4,sK3)
| ~ midp(sK3,sK4,sK3) ),
inference(resolve,[status(thm)],[c_3627,c_229]) ).
cnf(c_3908,plain,
( midp(A,sK3,sK3)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_3772,c_318]) ).
cnf(c_3992,plain,
para(sK5,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_460,c_2565]) ).
cnf(c_3993,plain,
para(sK5,sK4,sK3,sK4),
inference(resolve,[status(thm)],[c_460,c_2560]) ).
cnf(c_3999,plain,
para(sK3,sK4,sK5,sK3),
inference(resolve,[status(thm)],[c_3992,c_274]) ).
cnf(c_4029,plain,
para(sK5,sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_3993,c_275]) ).
cnf(c_4083,plain,
para(sK3,sK4,sK3,sK5),
inference(resolve,[status(thm)],[c_3999,c_275]) ).
cnf(c_4114,plain,
para(sK4,sK3,sK5,sK4),
inference(resolve,[status(thm)],[c_4029,c_274]) ).
cnf(c_4197,plain,
para(sK3,sK5,sK3,sK4),
inference(resolve,[status(thm)],[c_4083,c_274]) ).
cnf(c_23289,plain,
( midp(A,sK5,sK4)
| ~ para(sK3,sK5,sK3,sK4)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_4083,c_220]) ).
cnf(c_4204,plain,
( midp(A,sK5,sK4)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_4197,c_23289]) ).
cnf(c_4225,plain,
para(sK4,sK3,sK4,sK5),
inference(resolve,[status(thm)],[c_4114,c_275]) ).
cnf(c_4340,plain,
para(sK4,sK5,sK4,sK3),
inference(resolve,[status(thm)],[c_4225,c_274]) ).
cnf(c_23290,plain,
( midp(A,sK5,sK3)
| ~ para(sK4,sK5,sK4,sK3)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_4225,c_220]) ).
cnf(c_4347,plain,
( midp(A,sK5,sK3)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_4340,c_23290]) ).
cnf(c_4448,plain,
midp(sK4,sK5,sK4),
inference(resolve,[status(thm)],[c_4204,c_2273]) ).
cnf(c_4473,plain,
cong(sK4,sK5,sK4,sK4),
inference(resolve,[status(thm)],[c_4448,c_216]) ).
cnf(c_4503,plain,
perp(sK5,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_4473,c_1082]) ).
cnf(c_23291,plain,
( cong(sK5,sK4,sK5,sK4)
| ~ midp(sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_4503,c_229]) ).
cnf(c_4756,plain,
cong(sK5,sK4,sK5,sK4),
inference(resolve,[status(thm)],[c_2560,c_23291]) ).
cnf(c_4787,plain,
midp(sK5,sK4,sK4),
inference(resolve,[status(thm)],[c_4756,c_1407]) ).
cnf(c_4790,plain,
midp(sK5,sK3,sK3),
inference(resolve,[status(thm)],[c_4787,c_3908]) ).
cnf(c_4792,plain,
para(sK4,sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_4787,c_451]) ).
cnf(c_4866,plain,
para(sK3,sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_4790,c_451]) ).
cnf(c_5664,plain,
para(sK4,sK3,sK4,sK4),
inference(resolve,[status(thm)],[c_4792,c_274]) ).
cnf(c_23292,plain,
( midp(A,sK4,sK3)
| ~ para(sK4,sK3,sK4,sK4)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_4792,c_220]) ).
cnf(c_5671,plain,
( midp(A,sK4,sK3)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_5664,c_23292]) ).
cnf(c_5727,plain,
eqangle(sK3,sK4,A,B,sK3,sK3,A,B),
inference(resolve,[status(thm)],[c_4866,c_240]) ).
cnf(c_5750,plain,
cong(sK4,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_5727,c_2031]) ).
cnf(c_6602,plain,
cong(sK3,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_5750,c_256]) ).
cnf(c_7228,plain,
cong(sK3,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_6602,c_257]) ).
cnf(c_7244,plain,
midp(sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_7228,c_853]) ).
cnf(c_7274,plain,
midp(sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_7244,c_268]) ).
cnf(c_7311,plain,
cong(sK4,sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_7274,c_3780]) ).
cnf(c_7321,plain,
midp(sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_7311,c_1131]) ).
cnf(c_11276,plain,
cong(sK4,sK4,sK1,sK4),
inference(resolve,[status(thm)],[c_2093,c_7321]) ).
cnf(c_11277,plain,
cong(sK4,sK3,sK1,sK3),
inference(resolve,[status(thm)],[c_2093,c_7274]) ).
cnf(c_11280,plain,
cong(sK4,sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_11276,c_257]) ).
cnf(c_11281,plain,
cong(sK1,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_11276,c_256]) ).
cnf(c_11291,plain,
cong(sK4,sK3,sK3,sK1),
inference(resolve,[status(thm)],[c_11277,c_257]) ).
cnf(c_11387,plain,
cong(sK4,sK1,sK4,sK4),
inference(resolve,[status(thm)],[c_11280,c_256]) ).
cnf(c_11437,plain,
perp(sK1,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_11281,c_322]) ).
cnf(c_11438,plain,
( perp(sK4,sK1,sK1,sK4)
| ~ cyclic(sK1,sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_11281,c_321]) ).
cnf(c_11464,plain,
cong(sK3,sK1,sK4,sK3),
inference(resolve,[status(thm)],[c_11291,c_256]) ).
cnf(c_11571,plain,
cyclic(sK1,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_11387,c_341]) ).
cnf(c_11673,plain,
perp(sK4,sK1,sK1,sK4),
inference(resolve,[status(thm)],[c_11571,c_11438]) ).
cnf(c_23293,plain,
( cong(sK1,sK4,sK1,sK4)
| ~ midp(sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_11437,c_229]) ).
cnf(c_11679,plain,
cong(sK1,sK4,sK1,sK4),
inference(resolve,[status(thm)],[c_2560,c_23293]) ).
cnf(c_11722,plain,
cong(sK3,sK1,sK3,sK4),
inference(resolve,[status(thm)],[c_11464,c_257]) ).
cnf(c_11871,plain,
perp(sK4,sK1,sK4,sK1),
inference(resolve,[status(thm)],[c_11673,c_272]) ).
cnf(c_11971,plain,
( midp(sK1,sK4,sK4)
| ~ coll(sK1,sK4,sK4) ),
inference(resolve,[status(thm)],[c_11679,c_217]) ).
cnf(c_12090,plain,
cong(sK3,sK4,sK3,sK1),
inference(resolve,[status(thm)],[c_11722,c_256]) ).
cnf(c_12568,plain,
para(sK4,sK1,sK4,sK1),
inference(resolve,[status(thm)],[c_11871,c_331]) ).
cnf(c_12701,plain,
( midp(sK3,sK4,sK1)
| ~ coll(sK3,sK4,sK1) ),
inference(resolve,[status(thm)],[c_12090,c_217]) ).
cnf(c_12968,plain,
coll(sK4,sK1,sK1),
inference(resolve,[status(thm)],[c_12568,c_218]) ).
cnf(c_12978,plain,
coll(sK1,sK1,sK4),
inference(resolve,[status(thm)],[c_12968,c_332]) ).
cnf(c_13015,plain,
coll(sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_12978,c_332]) ).
cnf(c_13100,plain,
coll(sK1,sK4,sK4),
inference(resolve,[status(thm)],[c_13015,c_1362]) ).
cnf(c_13101,plain,
coll(sK3,sK1,sK4),
inference(resolve,[status(thm)],[c_13015,c_1126]) ).
cnf(c_13136,plain,
midp(sK1,sK4,sK4),
inference(resolve,[status(thm)],[c_13100,c_11971]) ).
cnf(c_13347,plain,
coll(sK3,sK4,sK1),
inference(resolve,[status(thm)],[c_13101,c_278]) ).
cnf(c_13364,plain,
midp(sK3,sK4,sK1),
inference(resolve,[status(thm)],[c_13347,c_12701]) ).
cnf(c_13489,plain,
midp(sK1,sK4,sK3),
inference(resolve,[status(thm)],[c_13136,c_5671]) ).
cnf(c_13492,plain,
midp(sK1,sK5,sK3),
inference(resolve,[status(thm)],[c_13136,c_4347]) ).
cnf(c_13691,plain,
para(sK5,sK3,sK3,sK1),
inference(resolve,[status(thm)],[c_13364,c_460]) ).
cnf(c_13946,plain,
para(sK5,sK1,sK3,sK3),
inference(resolve,[status(thm)],[c_13489,c_460]) ).
cnf(c_23294,plain,
( midp(A,sK1,sK3)
| ~ para(sK5,sK1,sK3,sK3)
| ~ midp(A,sK5,sK3) ),
inference(resolve,[status(thm)],[c_13691,c_220]) ).
cnf(c_15265,plain,
( midp(A,sK1,sK3)
| ~ midp(A,sK5,sK3) ),
inference(resolve,[status(thm)],[c_13946,c_23294]) ).
cnf(c_16960,plain,
midp(sK1,sK1,sK3),
inference(resolve,[status(thm)],[c_15265,c_13492]) ).
cnf(c_16968,plain,
cong(sK4,sK1,sK4,sK3),
inference(resolve,[status(thm)],[c_16960,c_2094]) ).
cnf(c_16994,plain,
midp(sK1,sK3,sK1),
inference(resolve,[status(thm)],[c_16960,c_268]) ).
cnf(c_17014,plain,
cong(sK4,sK3,sK4,sK1),
inference(resolve,[status(thm)],[c_16994,c_2476]) ).
cnf(c_17230,plain,
cyclic(sK1,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_16968,c_341]) ).
cnf(c_17347,plain,
cyclic(sK3,sK1,sK1,sK1),
inference(resolve,[status(thm)],[c_17014,c_341]) ).
cnf(c_17824,plain,
cyclic(sK3,sK1,sK3,sK3),
inference(resolve,[status(thm)],[c_17230,c_264]) ).
cnf(c_17860,plain,
cyclic(sK1,sK3,sK1,sK1),
inference(resolve,[status(thm)],[c_17347,c_264]) ).
cnf(c_18124,plain,
cyclic(sK3,sK3,sK1,sK3),
inference(resolve,[status(thm)],[c_17824,c_265]) ).
cnf(c_18188,plain,
cyclic(sK1,sK1,sK3,sK1),
inference(resolve,[status(thm)],[c_17860,c_265]) ).
cnf(c_18326,plain,
cyclic(sK3,sK3,sK3,sK1),
inference(resolve,[status(thm)],[c_18124,c_266]) ).
cnf(c_18327,plain,
( cyclic(sK3,sK1,A,sK3)
| ~ cyclic(sK3,sK3,sK1,A) ),
inference(resolve,[status(thm)],[c_18124,c_263]) ).
cnf(c_18356,plain,
cyclic(sK1,sK1,sK1,sK3),
inference(resolve,[status(thm)],[c_18188,c_266]) ).
cnf(c_18401,plain,
cyclic(sK3,sK3,sK1,sK1),
inference(resolve,[status(thm)],[c_18326,c_327]) ).
cnf(c_18409,plain,
( cyclic(sK3,sK3,sK1,A)
| ~ cyclic(sK3,sK3,sK3,A) ),
inference(resolve,[status(thm)],[c_18326,c_263]) ).
cnf(c_18439,plain,
cyclic(sK1,sK1,sK3,sK3),
inference(resolve,[status(thm)],[c_18356,c_327]) ).
cnf(c_18513,plain,
cyclic(sK3,sK1,sK3,sK1),
inference(resolve,[status(thm)],[c_18401,c_265]) ).
cnf(c_18515,plain,
( cyclic(sK3,sK1,sK1,A)
| ~ cyclic(sK3,sK3,sK1,A) ),
inference(resolve,[status(thm)],[c_18401,c_263]) ).
cnf(c_18549,plain,
( cyclic(sK1,sK3,A,sK3)
| ~ cyclic(sK1,sK1,sK3,A) ),
inference(resolve,[status(thm)],[c_18439,c_263]) ).
cnf(c_18609,plain,
cyclic(sK3,sK1,sK1,sK3),
inference(resolve,[status(thm)],[c_18513,c_266]) ).
cnf(c_18630,plain,
( cyclic(sK1,sK1,sK3,A)
| ~ cyclic(sK3,sK1,sK1,A) ),
inference(resolve,[status(thm)],[c_18609,c_263]) ).
cnf(c_19730,plain,
( cong(sK3,A,sK3,A)
| ~ cyclic(sK3,A,sK3,A)
| ~ cyclic(sK3,A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_3020,c_325]) ).
cnf(c_19732,plain,
eqangle(A,B,sK3,sK3,A,B,sK3,sK3),
inference(resolve,[status(thm)],[c_3020,c_261]) ).
cnf(c_19739,plain,
cyclic(A,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_19732,c_970]) ).
cnf(c_19749,plain,
cyclic(sK3,A,sK3,sK3),
inference(resolve,[status(thm)],[c_19739,c_264]) ).
cnf(c_19752,plain,
( cong(sK3,A,sK3,A)
| ~ cyclic(sK3,A,sK3,A) ),
inference(resolve,[status(thm)],[c_19749,c_19730]) ).
cnf(c_19769,plain,
cyclic(sK3,sK3,A,sK3),
inference(resolve,[status(thm)],[c_19749,c_265]) ).
cnf(c_19785,plain,
cyclic(sK3,sK3,sK3,A),
inference(resolve,[status(thm)],[c_19769,c_266]) ).
cnf(c_19789,plain,
cyclic(sK3,sK3,sK1,A),
inference(resolve,[status(thm)],[c_19785,c_18409]) ).
cnf(c_19808,plain,
cyclic(sK3,sK1,sK1,A),
inference(resolve,[status(thm)],[c_19789,c_18515]) ).
cnf(c_19814,plain,
cyclic(sK3,sK1,A,sK3),
inference(resolve,[status(thm)],[c_19789,c_18327]) ).
cnf(c_19849,plain,
cyclic(sK1,sK1,sK3,A),
inference(resolve,[status(thm)],[c_19808,c_18630]) ).
cnf(c_19905,plain,
cyclic(sK1,sK3,A,sK3),
inference(resolve,[status(thm)],[c_19849,c_18549]) ).
cnf(c_23295,plain,
( cyclic(sK3,sK3,A,B)
| ~ cyclic(sK3,sK3,sK3,A) ),
inference(resolve,[status(thm)],[c_19785,c_263]) ).
cnf(c_20170,plain,
cyclic(sK3,sK3,A,B),
inference(resolve,[status(thm)],[c_19785,c_23295]) ).
cnf(c_23296,plain,
( cyclic(sK3,sK1,A,B)
| ~ cyclic(sK3,sK3,sK1,A) ),
inference(resolve,[status(thm)],[c_19789,c_263]) ).
cnf(c_20183,plain,
cyclic(sK3,sK1,A,B),
inference(resolve,[status(thm)],[c_20170,c_23296]) ).
cnf(c_23297,plain,
( cyclic(sK1,A,sK3,B)
| ~ cyclic(sK3,sK1,A,B) ),
inference(resolve,[status(thm)],[c_19814,c_263]) ).
cnf(c_20390,plain,
cyclic(sK1,A,sK3,B),
inference(resolve,[status(thm)],[c_20183,c_23297]) ).
cnf(c_23298,plain,
( cyclic(sK1,sK3,A,B)
| ~ cyclic(sK1,sK1,sK3,A) ),
inference(resolve,[status(thm)],[c_19849,c_263]) ).
cnf(c_20526,plain,
cyclic(sK1,sK3,A,B),
inference(resolve,[status(thm)],[c_20390,c_23298]) ).
cnf(c_23299,plain,
( cyclic(sK3,A,sK3,B)
| ~ cyclic(sK1,sK3,A,B) ),
inference(resolve,[status(thm)],[c_19905,c_263]) ).
cnf(c_20665,plain,
cyclic(sK3,A,sK3,B),
inference(resolve,[status(thm)],[c_20526,c_23299]) ).
cnf(c_20671,plain,
cong(sK3,A,sK3,A),
inference(resolve,[status(thm)],[c_20665,c_19752]) ).
cnf(c_23300,plain,
( perp(sK3,sK3,A,B)
| ~ cong(sK3,A,sK3,A) ),
inference(resolve,[status(thm)],[c_20671,c_228]) ).
cnf(c_21933,plain,
perp(sK3,sK3,A,B),
inference(resolve,[status(thm)],[c_20671,c_23300]) ).
cnf(c_23283,plain,
perp(A,B,sK3,sK3),
inference(resolve,[status(thm)],[c_21933,c_271]) ).
cnf(c_23301,plain,
( para(A,B,C,D)
| ~ perp(A,B,sK3,sK3) ),
inference(resolve,[status(thm)],[c_21933,c_270]) ).
cnf(c_23284,plain,
para(A,B,C,D),
inference(resolve,[status(thm)],[c_23283,c_23301]) ).
cnf(c_23302,plain,
( perp(A,B,C,D)
| ~ para(A,B,sK3,sK3) ),
inference(resolve,[status(thm)],[c_21933,c_269]) ).
cnf(c_23285,plain,
perp(A,B,C,D),
inference(resolve,[status(thm)],[c_23284,c_23302]) ).
cnf(c_23286,plain,
$false,
inference(resolve,[status(thm)],[c_23285,c_177]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO607+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.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:49:02 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 2512729 was started by sandbox on n016,
% 0.09/0.36 % Fri Sep 25 13:49:02 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 52.88/14.62
% 52.88/14.62 % given #500 (T,wt=10): 7378 para(c3,c1,c1,c1). [resolve(7274,a,460,a)].
% 52.88/14.62
% 52.88/14.62 % given #1000 (W,wt=13): 14461 -coll(c4,c4,A) | coll(A,c3,c4). [resolve(13755,a,276,b)].
% 52.88/14.62
% 52.88/14.62 % given #1500 (T,wt=10): 20670 cyclic(A,c1,B,c1). [back_unit_del(19770),unit_del(a,20665)].
% 52.88/14.62
% 52.88/14.62 % SZS status Theorem for theBenchmark
% 52.88/14.62
% 52.88/14.62 % Proof 1 at 2.21 (+ 0.65) seconds.
% 52.88/14.62 % Length of proof is 264.
% 52.88/14.62 % Level of proof is 64.
% 52.88/14.62 % Maximum clause weight is 34.000.
% 52.88/14.62 % Given clauses 1620.
% 52.88/14.62
% 52.88/14.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------