%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO590+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 : n005.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:10 AM UTC 2026
% Result : Theorem 229.42s 30.58s
% Output : CNFRefutation 229.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 28
% Syntax : Number of formulae : 282 ( 157 unt; 0 def)
% Number of atoms : 484 ( 0 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 338 ( 136 ~; 132 |; 41 &)
% ( 0 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-4 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-7 aty)
% Number of variables : 384 ( 19 sgn 140 !; 8 ?)
% 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(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(ruleD25,axiom,
! [A,B,C,D,E,F] :
( ( cong(C,D,E,F)
& cong(A,B,C,D) )
=> cong(A,B,E,F) ),
file('theBenchmark.p',ruleD25) ).
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(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(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(ruleX7,axiom,
! [A,B,C,D,M,N,Q] :
? [P] :
( ( coll(D,A,B)
& coll(C,A,B)
& midp(N,C,D)
& midp(M,A,B) )
=> midp(P,A,Q) ),
file('theBenchmark.p',ruleX7) ).
fof(exemplo6GDDFULL416052,conjecture,
! [C,D,E,O,A,F] :
( ( coll(F,D,E)
& coll(F,C,A)
& perp(E,O,E,A)
& perp(C,D,C,A)
& midp(O,D,C)
& perp(E,C,E,D) )
=> cong(A,E,A,F) ),
file('theBenchmark.p',exemplo6GDDFULL416052) ).
fof(exemplo6GDDFULL416052_neg,negated_conjecture,
~ ! [C,D,E,O,A,F] :
( ( coll(F,D,E)
& coll(F,C,A)
& perp(E,O,E,A)
& perp(C,D,C,A)
& midp(O,D,C)
& perp(E,C,E,D) )
=> cong(A,E,A,F) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL416052]) ).
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,
? [C,D,E,O,A,F] :
( ~ cong(A,E,A,F)
& coll(F,D,E)
& coll(F,C,A)
& perp(E,O,E,A)
& perp(C,D,C,A)
& midp(O,D,C)
& perp(E,C,E,D) ),
inference(fof_nnf,[status(thm)],[exemplo6GDDFULL416052_neg]) ).
fof(sk_exemplo6GDDFULL416052_neg,plain,
( ~ cong(sK0,sK1,sK0,sK2)
& coll(sK2,sK3,sK1)
& coll(sK2,sK4,sK0)
& perp(sK1,sK5,sK1,sK0)
& perp(sK4,sK3,sK4,sK0)
& midp(sK5,sK3,sK4)
& perp(sK1,sK4,sK1,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK4,sK3,sK5,sK0,sK2]),skolemize(C,sK4),skolemize(D,sK3),skolemize(E,sK1),skolemize(O,sK5),skolemize(A,sK0),skolemize(F,sK2)],[nnf_95]) ).
cnf(c_147,negated_conjecture,
~ cong(sK0,sK1,sK0,sK2),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL416052_neg]) ).
cnf(c_148,negated_conjecture,
coll(sK2,sK3,sK1),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL416052_neg]) ).
cnf(c_149,negated_conjecture,
coll(sK2,sK4,sK0),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL416052_neg]) ).
cnf(c_150,negated_conjecture,
perp(sK1,sK5,sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL416052_neg]) ).
cnf(c_151,negated_conjecture,
perp(sK4,sK3,sK4,sK0),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL416052_neg]) ).
cnf(c_152,negated_conjecture,
midp(sK5,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL416052_neg]) ).
cnf(c_153,negated_conjecture,
perp(sK1,sK4,sK1,sK3),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL416052_neg]) ).
fof(nnf_83,plain,
! [A,B,C,D,M,N,Q] :
? [P] :
( midp(P,A,Q)
| ~ coll(D,A,B)
| ~ coll(C,A,B)
| ~ midp(N,C,D)
| ~ midp(M,A,B) ),
inference(fof_nnf,[status(thm)],[ruleX7]) ).
fof(sk_ruleX7,plain,
! [A,B,C,D,M,N,Q] :
( midp(sK6(A,B,C,D,M,N,Q),A,Q)
| ~ coll(D,A,B)
| ~ coll(C,A,B)
| ~ midp(N,C,D)
| ~ midp(M,A,B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(P,sK6(A,B,C,D,M,N,Q))],[nnf_83]) ).
cnf(c_170,plain,
( midp(sK6(B,C,E,F,A,D,V6),B,V6)
| ~ coll(F,B,C)
| ~ coll(E,B,C)
| ~ midp(D,E,F)
| ~ midp(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_ruleX7]) ).
cnf(c_189,plain,
( coll(A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD69]) ).
cnf(c_190,plain,
( cong(A,B,A,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD68]) ).
cnf(c_191,plain,
( midp(A,B,C)
| ~ coll(A,B,C)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD67]) ).
cnf(c_192,plain,
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD66]) ).
cnf(c_194,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_195,plain,
( para(B,D,C,E)
| ~ midp(A,D,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD63]) ).
cnf(c_202,plain,
( perp(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD56]) ).
cnf(c_203,plain,
( cong(D,B,D,C)
| ~ perp(D,A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD55]) ).
cnf(c_205,plain,
( cong(A,D,B,D)
| ~ midp(D,A,C)
| ~ perp(A,B,B,C) ),
inference(clausify,[status(thm)],[ruleD52]) ).
cnf(c_208,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_209,plain,
( para(A,D,C,E)
| ~ midp(D,B,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD44]) ).
cnf(c_229,plain,
( cong(A,B,E,F)
| ~ cong(C,D,E,F)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD25]) ).
cnf(c_230,plain,
( cong(C,D,A,B)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD24]) ).
cnf(c_231,plain,
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD23]) ).
cnf(c_242,plain,
( midp(A,C,B)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD11]) ).
cnf(c_243,plain,
( perp(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD10]) ).
cnf(c_244,plain,
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD9]) ).
cnf(c_245,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD8]) ).
cnf(c_246,plain,
( perp(A,B,D,C)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD7]) ).
cnf(c_248,plain,
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD5]) ).
cnf(c_249,plain,
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD4]) ).
cnf(c_250,plain,
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD3]) ).
cnf(c_251,plain,
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD2]) ).
cnf(c_252,plain,
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD1]) ).
cnf(c_267,plain,
( ~ cong(A,B,A,C)
| perp(B,C,C,C)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_142]) ).
cnf(c_285,plain,
( midp(sK6(B,C,B,C,A,A,D),B,D)
| ~ coll(C,B,C)
| ~ coll(B,B,C)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_170]) ).
cnf(c_292,plain,
( midp(A,D,D)
| ~ para(B,D,C,D)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_194]) ).
cnf(c_293,plain,
( para(B,B,C,C)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_195]) ).
cnf(c_296,plain,
( perp(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_202]) ).
cnf(c_306,plain,
( coll(C,C,A)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_250]) ).
cnf(c_351,plain,
coll(sK5,sK3,sK4),
inference(resolve,[status(thm)],[c_189,c_152]) ).
cnf(c_352,plain,
cong(sK5,sK3,sK5,sK4),
inference(resolve,[status(thm)],[c_190,c_152]) ).
cnf(c_353,plain,
( para(sK3,A,sK4,B)
| ~ midp(sK5,A,B) ),
inference(resolve,[status(thm)],[c_195,c_152]) ).
cnf(c_354,plain,
( para(A,sK3,B,sK4)
| ~ midp(sK5,A,B) ),
inference(resolve,[status(thm)],[c_195,c_152]) ).
cnf(c_358,plain,
( para(sK5,A,sK4,B)
| ~ midp(A,sK3,B) ),
inference(resolve,[status(thm)],[c_209,c_152]) ).
cnf(c_360,plain,
midp(sK5,sK4,sK3),
inference(resolve,[status(thm)],[c_242,c_152]) ).
cnf(c_361,plain,
( para(sK1,sK4,A,B)
| ~ perp(sK1,sK3,A,B) ),
inference(resolve,[status(thm)],[c_244,c_153]) ).
cnf(c_363,plain,
( para(sK1,sK5,A,B)
| ~ perp(sK1,sK0,A,B) ),
inference(resolve,[status(thm)],[c_244,c_150]) ).
cnf(c_364,plain,
( para(A,B,sK1,sK3)
| ~ perp(A,B,sK1,sK4) ),
inference(resolve,[status(thm)],[c_244,c_153]) ).
cnf(c_365,plain,
( para(A,B,sK4,sK0)
| ~ perp(A,B,sK4,sK3) ),
inference(resolve,[status(thm)],[c_244,c_151]) ).
cnf(c_366,plain,
( para(A,B,sK1,sK0)
| ~ perp(A,B,sK1,sK5) ),
inference(resolve,[status(thm)],[c_244,c_150]) ).
cnf(c_367,plain,
perp(sK1,sK3,sK1,sK4),
inference(resolve,[status(thm)],[c_245,c_153]) ).
cnf(c_369,plain,
perp(sK1,sK0,sK1,sK5),
inference(resolve,[status(thm)],[c_245,c_150]) ).
cnf(c_370,plain,
perp(sK1,sK4,sK3,sK1),
inference(resolve,[status(thm)],[c_246,c_153]) ).
cnf(c_378,plain,
coll(sK3,sK2,sK1),
inference(resolve,[status(thm)],[c_251,c_148]) ).
cnf(c_379,plain,
coll(sK2,sK0,sK4),
inference(resolve,[status(thm)],[c_252,c_149]) ).
cnf(c_380,plain,
coll(sK2,sK1,sK3),
inference(resolve,[status(thm)],[c_252,c_148]) ).
cnf(c_381,plain,
( midp(sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),sK3,A)
| ~ coll(sK4,sK3,sK4)
| ~ coll(sK3,sK3,sK4) ),
inference(resolve,[status(thm)],[c_285,c_152]) ).
cnf(c_388,plain,
coll(sK0,sK0,sK2),
inference(resolve,[status(thm)],[c_306,c_149]) ).
cnf(c_390,plain,
coll(sK4,sK4,sK5),
inference(resolve,[status(thm)],[c_351,c_306]) ).
cnf(c_391,plain,
coll(sK5,sK4,sK3),
inference(resolve,[status(thm)],[c_351,c_252]) ).
cnf(c_392,plain,
coll(sK3,sK5,sK4),
inference(resolve,[status(thm)],[c_351,c_251]) ).
cnf(c_405,plain,
( para(A,sK4,B,sK3)
| ~ midp(sK5,A,B) ),
inference(resolve,[status(thm)],[c_360,c_195]) ).
cnf(c_407,plain,
cong(sK5,sK4,sK5,sK3),
inference(resolve,[status(thm)],[c_360,c_190]) ).
cnf(c_422,plain,
coll(sK1,sK1,sK3),
inference(resolve,[status(thm)],[c_378,c_306]) ).
cnf(c_424,plain,
( coll(A,sK1,sK3)
| ~ coll(sK3,sK2,A) ),
inference(resolve,[status(thm)],[c_378,c_250]) ).
cnf(c_425,plain,
( coll(sK1,A,sK3)
| ~ coll(sK3,sK2,A) ),
inference(resolve,[status(thm)],[c_378,c_250]) ).
cnf(c_426,plain,
coll(sK4,sK4,sK2),
inference(resolve,[status(thm)],[c_379,c_306]) ).
cnf(c_428,plain,
( coll(A,sK4,sK2)
| ~ coll(sK2,sK0,A) ),
inference(resolve,[status(thm)],[c_379,c_250]) ).
cnf(c_432,plain,
( coll(A,sK3,sK2)
| ~ coll(sK2,sK1,A) ),
inference(resolve,[status(thm)],[c_380,c_250]) ).
cnf(c_436,plain,
( coll(A,sK2,sK0)
| ~ coll(sK0,sK0,A) ),
inference(resolve,[status(thm)],[c_388,c_250]) ).
cnf(c_442,plain,
coll(sK5,sK5,sK4),
inference(resolve,[status(thm)],[c_390,c_306]) ).
cnf(c_443,plain,
coll(sK4,sK5,sK4),
inference(resolve,[status(thm)],[c_390,c_252]) ).
cnf(c_445,plain,
( coll(sK5,A,sK4)
| ~ coll(sK4,sK4,A) ),
inference(resolve,[status(thm)],[c_390,c_250]) ).
cnf(c_446,plain,
coll(sK3,sK3,sK5),
inference(resolve,[status(thm)],[c_391,c_306]) ).
cnf(c_447,plain,
coll(sK4,sK5,sK3),
inference(resolve,[status(thm)],[c_391,c_251]) ).
cnf(c_449,plain,
( coll(sK3,A,sK5)
| ~ coll(sK5,sK4,A) ),
inference(resolve,[status(thm)],[c_391,c_250]) ).
cnf(c_450,plain,
coll(sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_392,c_306]) ).
cnf(c_463,plain,
coll(sK3,sK3,sK1),
inference(resolve,[status(thm)],[c_422,c_306]) ).
cnf(c_525,plain,
coll(sK5,sK4,sK5),
inference(resolve,[status(thm)],[c_442,c_252]) ).
cnf(c_549,plain,
coll(sK5,sK4,sK4),
inference(resolve,[status(thm)],[c_443,c_251]) ).
cnf(c_552,plain,
coll(sK5,sK5,sK3),
inference(resolve,[status(thm)],[c_446,c_306]) ).
cnf(c_556,plain,
coll(sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_447,c_306]) ).
cnf(c_560,plain,
( midp(sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),sK3,A)
| ~ coll(sK4,sK3,sK4) ),
inference(resolve,[status(thm)],[c_556,c_381]) ).
cnf(c_561,plain,
coll(sK4,sK3,sK4),
inference(resolve,[status(thm)],[c_450,c_252]) ).
cnf(c_564,plain,
midp(sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),sK3,A),
inference(resolve,[status(thm)],[c_561,c_560]) ).
cnf(c_590,plain,
( coll(sK1,A,sK3)
| ~ coll(sK3,sK3,A) ),
inference(resolve,[status(thm)],[c_463,c_250]) ).
cnf(c_670,plain,
coll(sK4,sK5,sK5),
inference(resolve,[status(thm)],[c_525,c_251]) ).
cnf(c_686,plain,
coll(sK5,sK3,sK5),
inference(resolve,[status(thm)],[c_552,c_252]) ).
cnf(c_735,plain,
coll(sK3,sK5,sK5),
inference(resolve,[status(thm)],[c_686,c_251]) ).
cnf(c_40123,plain,
( perp(sK3,sK4,sK4,sK4)
| ~ coll(sK5,sK3,sK4) ),
inference(resolve,[status(thm)],[c_352,c_267]) ).
cnf(c_775,plain,
perp(sK3,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_351,c_40123]) ).
cnf(c_816,plain,
cong(sK5,sK3,sK4,sK5),
inference(resolve,[status(thm)],[c_352,c_231]) ).
cnf(c_817,plain,
( cong(A,B,sK5,sK4)
| ~ cong(A,B,sK5,sK3) ),
inference(resolve,[status(thm)],[c_352,c_229]) ).
cnf(c_871,plain,
perp(sK1,sK0,sK5,sK1),
inference(resolve,[status(thm)],[c_369,c_246]) ).
cnf(c_879,plain,
perp(sK3,sK1,sK1,sK4),
inference(resolve,[status(thm)],[c_370,c_245]) ).
cnf(c_40124,plain,
( perp(sK4,sK3,sK3,sK3)
| ~ coll(sK5,sK4,sK3) ),
inference(resolve,[status(thm)],[c_407,c_267]) ).
cnf(c_991,plain,
perp(sK4,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_391,c_40124]) ).
cnf(c_1032,plain,
cong(sK5,sK4,sK3,sK5),
inference(resolve,[status(thm)],[c_407,c_231]) ).
cnf(c_1079,plain,
perp(sK4,sK4,sK3,sK4),
inference(resolve,[status(thm)],[c_775,c_245]) ).
cnf(c_1101,plain,
cong(sK4,sK5,sK5,sK3),
inference(resolve,[status(thm)],[c_816,c_230]) ).
cnf(c_1150,plain,
( cong(sK3,A,sK1,A)
| ~ midp(A,sK3,sK4) ),
inference(resolve,[status(thm)],[c_879,c_205]) ).
cnf(c_1266,plain,
perp(sK3,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_991,c_245]) ).
cnf(c_1290,plain,
cong(sK3,sK5,sK5,sK4),
inference(resolve,[status(thm)],[c_1032,c_230]) ).
cnf(c_1331,plain,
perp(sK4,sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_1079,c_246]) ).
cnf(c_1371,plain,
para(sK4,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_354,c_360]) ).
cnf(c_1497,plain,
perp(sK3,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_1266,c_246]) ).
cnf(c_1526,plain,
cong(sK3,sK5,sK4,sK5),
inference(resolve,[status(thm)],[c_1290,c_231]) ).
cnf(c_1581,plain,
para(sK4,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_1371,c_249]) ).
cnf(c_1621,plain,
para(sK1,sK4,sK1,sK4),
inference(resolve,[status(thm)],[c_361,c_367]) ).
cnf(c_1628,plain,
perp(sK3,sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_1497,c_245]) ).
cnf(c_1656,plain,
perp(sK3,sK4,sK5,sK5),
inference(resolve,[status(thm)],[c_1526,c_296]) ).
cnf(c_1707,plain,
para(sK1,sK5,sK5,sK1),
inference(resolve,[status(thm)],[c_363,c_871]) ).
cnf(c_1710,plain,
para(sK1,sK3,sK1,sK3),
inference(resolve,[status(thm)],[c_364,c_367]) ).
cnf(c_1711,plain,
( midp(A,sK3,sK3)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_1581,c_292]) ).
cnf(c_1760,plain,
( midp(A,sK4,sK4)
| ~ midp(A,sK1,sK1) ),
inference(resolve,[status(thm)],[c_1621,c_292]) ).
cnf(c_1766,plain,
coll(sK1,sK4,sK4),
inference(resolve,[status(thm)],[c_1621,c_192]) ).
cnf(c_1773,plain,
coll(sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_1766,c_306]) ).
cnf(c_1784,plain,
para(sK4,sK4,sK4,sK0),
inference(resolve,[status(thm)],[c_365,c_1331]) ).
cnf(c_1785,plain,
para(sK3,sK3,sK4,sK0),
inference(resolve,[status(thm)],[c_365,c_1266]) ).
cnf(c_1789,plain,
para(sK1,sK0,sK1,sK0),
inference(resolve,[status(thm)],[c_366,c_369]) ).
cnf(c_1805,plain,
( para(sK3,sK4,A,B)
| ~ perp(sK3,sK3,A,B) ),
inference(resolve,[status(thm)],[c_1628,c_244]) ).
cnf(c_1814,plain,
( cong(sK3,sK5,sK3,sK5)
| ~ midp(sK4,sK5,sK5) ),
inference(resolve,[status(thm)],[c_1656,c_203]) ).
cnf(c_1861,plain,
para(sK5,sK1,sK1,sK5),
inference(resolve,[status(thm)],[c_1707,c_248]) ).
cnf(c_1924,plain,
( midp(A,sK3,sK3)
| ~ midp(A,sK1,sK1) ),
inference(resolve,[status(thm)],[c_1710,c_292]) ).
cnf(c_2010,plain,
para(sK4,sK0,sK4,sK4),
inference(resolve,[status(thm)],[c_1784,c_248]) ).
cnf(c_40125,plain,
( midp(A,sK4,sK0)
| ~ para(sK4,sK0,sK4,sK4)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_1784,c_194]) ).
cnf(c_2017,plain,
( midp(A,sK4,sK0)
| ~ midp(A,sK4,sK4) ),
inference(resolve,[status(thm)],[c_2010,c_40125]) ).
cnf(c_2028,plain,
para(sK4,sK0,sK3,sK3),
inference(resolve,[status(thm)],[c_1785,c_248]) ).
cnf(c_2133,plain,
coll(sK1,sK0,sK0),
inference(resolve,[status(thm)],[c_1789,c_192]) ).
cnf(c_2140,plain,
coll(sK0,sK0,sK1),
inference(resolve,[status(thm)],[c_2133,c_306]) ).
cnf(c_2216,plain,
para(sK5,sK1,sK5,sK1),
inference(resolve,[status(thm)],[c_1861,c_249]) ).
cnf(c_2409,plain,
( perp(sK4,sK0,A,B)
| ~ perp(sK3,sK3,A,B) ),
inference(resolve,[status(thm)],[c_2028,c_243]) ).
cnf(c_2544,plain,
( midp(A,sK1,sK1)
| ~ midp(A,sK5,sK5) ),
inference(resolve,[status(thm)],[c_2216,c_292]) ).
cnf(c_2608,plain,
coll(sK1,sK2,sK0),
inference(resolve,[status(thm)],[c_436,c_2140]) ).
cnf(c_2610,plain,
coll(sK2,sK1,sK0),
inference(resolve,[status(thm)],[c_2608,c_251]) ).
cnf(c_2621,plain,
coll(sK0,sK3,sK2),
inference(resolve,[status(thm)],[c_2610,c_432]) ).
cnf(c_2631,plain,
coll(sK0,sK2,sK3),
inference(resolve,[status(thm)],[c_2621,c_252]) ).
cnf(c_2651,plain,
coll(sK2,sK0,sK3),
inference(resolve,[status(thm)],[c_2631,c_251]) ).
cnf(c_2679,plain,
coll(sK3,sK4,sK2),
inference(resolve,[status(thm)],[c_2651,c_428]) ).
cnf(c_2713,plain,
coll(sK3,sK2,sK4),
inference(resolve,[status(thm)],[c_2679,c_252]) ).
cnf(c_2743,plain,
coll(sK1,sK4,sK3),
inference(resolve,[status(thm)],[c_2713,c_425]) ).
cnf(c_2754,plain,
coll(sK5,sK1,sK4),
inference(resolve,[status(thm)],[c_445,c_1773]) ).
cnf(c_2756,plain,
coll(sK5,sK2,sK4),
inference(resolve,[status(thm)],[c_445,c_426]) ).
cnf(c_2778,plain,
coll(sK1,sK3,sK4),
inference(resolve,[status(thm)],[c_2743,c_252]) ).
cnf(c_2805,plain,
coll(sK5,sK4,sK2),
inference(resolve,[status(thm)],[c_2756,c_252]) ).
cnf(c_2828,plain,
( coll(sK4,A,sK1)
| ~ coll(sK1,sK3,A) ),
inference(resolve,[status(thm)],[c_2778,c_250]) ).
cnf(c_2855,plain,
coll(sK3,sK2,sK5),
inference(resolve,[status(thm)],[c_2805,c_449]) ).
cnf(c_2920,plain,
coll(sK5,sK1,sK3),
inference(resolve,[status(thm)],[c_2855,c_424]) ).
cnf(c_3148,plain,
para(sK3,sK3,A,A),
inference(resolve,[status(thm)],[c_564,c_293]) ).
cnf(c_3156,plain,
midp(sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),A,sK3),
inference(resolve,[status(thm)],[c_564,c_242]) ).
cnf(c_3159,plain,
( para(B,sK3,C,A)
| ~ midp(sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),B,C) ),
inference(resolve,[status(thm)],[c_564,c_195]) ).
cnf(c_3161,plain,
cong(sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),sK3,sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),A),
inference(resolve,[status(thm)],[c_564,c_190]) ).
cnf(c_3162,plain,
coll(sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),sK3,A),
inference(resolve,[status(thm)],[c_564,c_189]) ).
cnf(c_3215,plain,
( perp(sK3,sK3,B,C)
| ~ perp(A,A,B,C) ),
inference(resolve,[status(thm)],[c_3148,c_243]) ).
cnf(c_3827,plain,
cong(sK3,sK5,sK1,sK5),
inference(resolve,[status(thm)],[c_1150,c_152]) ).
cnf(c_3829,plain,
cong(sK3,sK5,sK5,sK1),
inference(resolve,[status(thm)],[c_3827,c_231]) ).
cnf(c_3851,plain,
cong(sK5,sK1,sK3,sK5),
inference(resolve,[status(thm)],[c_3829,c_230]) ).
cnf(c_3873,plain,
cong(sK5,sK1,sK5,sK3),
inference(resolve,[status(thm)],[c_3851,c_231]) ).
cnf(c_40126,plain,
( midp(sK5,sK1,sK3)
| ~ coll(sK5,sK1,sK3) ),
inference(resolve,[status(thm)],[c_3873,c_191]) ).
cnf(c_3966,plain,
midp(sK5,sK1,sK3),
inference(resolve,[status(thm)],[c_2920,c_40126]) ).
cnf(c_4004,plain,
para(sK3,sK1,sK4,sK3),
inference(resolve,[status(thm)],[c_3966,c_353]) ).
cnf(c_4021,plain,
midp(sK5,sK3,sK1),
inference(resolve,[status(thm)],[c_3966,c_242]) ).
cnf(c_4047,plain,
para(sK3,sK4,sK1,sK3),
inference(resolve,[status(thm)],[c_4021,c_405]) ).
cnf(c_4051,plain,
para(sK3,sK3,sK4,sK1),
inference(resolve,[status(thm)],[c_4021,c_353]) ).
cnf(c_4290,plain,
para(sK3,sK1,sK3,sK4),
inference(resolve,[status(thm)],[c_4004,c_249]) ).
cnf(c_40127,plain,
( midp(A,sK3,sK1)
| ~ para(sK3,sK3,sK4,sK1)
| ~ midp(A,sK3,sK4) ),
inference(resolve,[status(thm)],[c_4004,c_194]) ).
cnf(c_4296,plain,
( midp(A,sK3,sK1)
| ~ midp(A,sK3,sK4) ),
inference(resolve,[status(thm)],[c_4051,c_40127]) ).
cnf(c_4324,plain,
para(sK3,sK4,sK3,sK1),
inference(resolve,[status(thm)],[c_4047,c_249]) ).
cnf(c_40128,plain,
( midp(A,sK4,sK1)
| ~ para(sK3,sK4,sK3,sK1)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_4290,c_194]) ).
cnf(c_4643,plain,
( midp(A,sK4,sK1)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_4324,c_40128]) ).
cnf(c_5915,plain,
cong(sK5,sK1,sK5,sK4),
inference(resolve,[status(thm)],[c_817,c_3873]) ).
cnf(c_5917,plain,
cong(sK4,sK5,sK5,sK4),
inference(resolve,[status(thm)],[c_817,c_1101]) ).
cnf(c_5918,plain,
cong(sK5,sK4,sK5,sK4),
inference(resolve,[status(thm)],[c_817,c_407]) ).
cnf(c_40129,plain,
( perp(sK1,sK4,sK4,sK4)
| ~ coll(sK5,sK1,sK4) ),
inference(resolve,[status(thm)],[c_5915,c_267]) ).
cnf(c_6004,plain,
perp(sK1,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_2754,c_40129]) ).
cnf(c_40130,plain,
( midp(sK5,sK1,sK4)
| ~ coll(sK5,sK1,sK4) ),
inference(resolve,[status(thm)],[c_5915,c_191]) ).
cnf(c_6050,plain,
midp(sK5,sK1,sK4),
inference(resolve,[status(thm)],[c_2754,c_40130]) ).
cnf(c_6105,plain,
para(sK1,sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_6050,c_405]) ).
cnf(c_6106,plain,
para(sK1,sK3,sK4,sK4),
inference(resolve,[status(thm)],[c_6050,c_354]) ).
cnf(c_6258,plain,
cong(sK4,sK5,sK4,sK5),
inference(resolve,[status(thm)],[c_5917,c_231]) ).
cnf(c_40131,plain,
( midp(sK5,sK4,sK4)
| ~ coll(sK5,sK4,sK4) ),
inference(resolve,[status(thm)],[c_5918,c_191]) ).
cnf(c_6323,plain,
midp(sK5,sK4,sK4),
inference(resolve,[status(thm)],[c_549,c_40131]) ).
cnf(c_6371,plain,
midp(sK5,sK3,sK3),
inference(resolve,[status(thm)],[c_6323,c_1711]) ).
cnf(c_7036,plain,
( cong(sK1,sK4,sK1,sK4)
| ~ midp(sK4,sK4,sK4) ),
inference(resolve,[status(thm)],[c_6004,c_203]) ).
cnf(c_40132,plain,
( midp(A,sK3,sK4)
| ~ para(sK1,sK3,sK4,sK4)
| ~ midp(A,sK1,sK4) ),
inference(resolve,[status(thm)],[c_6105,c_194]) ).
cnf(c_7203,plain,
( midp(A,sK3,sK4)
| ~ midp(A,sK1,sK4) ),
inference(resolve,[status(thm)],[c_6106,c_40132]) ).
cnf(c_40133,plain,
( midp(sK4,sK5,sK5)
| ~ coll(sK4,sK5,sK5) ),
inference(resolve,[status(thm)],[c_6258,c_191]) ).
cnf(c_7443,plain,
midp(sK4,sK5,sK5),
inference(resolve,[status(thm)],[c_670,c_40133]) ).
cnf(c_7466,plain,
cong(sK3,sK5,sK3,sK5),
inference(resolve,[status(thm)],[c_7443,c_1814]) ).
cnf(c_7471,plain,
midp(sK4,sK1,sK1),
inference(resolve,[status(thm)],[c_7443,c_2544]) ).
cnf(c_7516,plain,
midp(sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_7471,c_1924]) ).
cnf(c_7517,plain,
midp(sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_7471,c_1760]) ).
cnf(c_7565,plain,
cong(sK1,sK4,sK1,sK4),
inference(resolve,[status(thm)],[c_7517,c_7036]) ).
cnf(c_40134,plain,
( midp(sK3,sK5,sK5)
| ~ coll(sK3,sK5,sK5) ),
inference(resolve,[status(thm)],[c_7466,c_191]) ).
cnf(c_9457,plain,
midp(sK3,sK5,sK5),
inference(resolve,[status(thm)],[c_735,c_40134]) ).
cnf(c_9502,plain,
midp(sK3,sK1,sK1),
inference(resolve,[status(thm)],[c_9457,c_2544]) ).
cnf(c_9551,plain,
midp(sK3,sK4,sK4),
inference(resolve,[status(thm)],[c_9502,c_1760]) ).
cnf(c_9775,plain,
midp(sK3,sK4,sK0),
inference(resolve,[status(thm)],[c_9551,c_2017]) ).
cnf(c_40135,plain,
( midp(sK1,sK4,sK4)
| ~ coll(sK1,sK4,sK4) ),
inference(resolve,[status(thm)],[c_7565,c_191]) ).
cnf(c_10181,plain,
midp(sK1,sK4,sK4),
inference(resolve,[status(thm)],[c_1766,c_40135]) ).
cnf(c_10210,plain,
midp(sK1,sK4,sK0),
inference(resolve,[status(thm)],[c_10181,c_2017]) ).
cnf(c_10378,plain,
cong(sK1,sK4,sK1,sK0),
inference(resolve,[status(thm)],[c_10210,c_190]) ).
cnf(c_13216,plain,
cong(sK1,sK4,sK0,sK1),
inference(resolve,[status(thm)],[c_10378,c_231]) ).
cnf(c_14847,plain,
cong(sK0,sK1,sK1,sK4),
inference(resolve,[status(thm)],[c_13216,c_230]) ).
cnf(c_16228,plain,
cong(sK0,sK1,sK4,sK1),
inference(resolve,[status(thm)],[c_14847,c_231]) ).
cnf(c_16848,plain,
( perp(sK0,sK4,sK1,A)
| ~ cong(sK0,A,sK4,A) ),
inference(resolve,[status(thm)],[c_16228,c_202]) ).
cnf(c_17909,plain,
midp(sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_4643,c_7516]) ).
cnf(c_18180,plain,
midp(sK4,sK1,sK4),
inference(resolve,[status(thm)],[c_17909,c_242]) ).
cnf(c_19207,plain,
midp(sK4,sK3,sK4),
inference(resolve,[status(thm)],[c_7203,c_18180]) ).
cnf(c_19357,plain,
midp(sK4,sK3,sK1),
inference(resolve,[status(thm)],[c_19207,c_4296]) ).
cnf(c_19897,plain,
para(sK5,sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_19357,c_358]) ).
cnf(c_20902,plain,
( midp(sK4,A,sK1)
| ~ coll(sK4,A,sK1)
| ~ midp(sK5,A,sK4) ),
inference(resolve,[status(thm)],[c_19897,c_208]) ).
cnf(c_35064,plain,
para(A,sK3,sK3,A),
inference(resolve,[status(thm)],[c_3159,c_3156]) ).
cnf(c_35073,plain,
para(A,sK3,A,sK3),
inference(resolve,[status(thm)],[c_35064,c_249]) ).
cnf(c_35074,plain,
para(sK3,A,A,sK3),
inference(resolve,[status(thm)],[c_35064,c_248]) ).
cnf(c_35082,plain,
coll(A,sK3,sK3),
inference(resolve,[status(thm)],[c_35073,c_192]) ).
cnf(c_35126,plain,
coll(sK3,sK3,A),
inference(resolve,[status(thm)],[c_35082,c_306]) ).
cnf(c_35141,plain,
coll(sK1,A,sK3),
inference(resolve,[status(thm)],[c_35126,c_590]) ).
cnf(c_40136,plain,
( perp(sK3,A,A,A)
| ~ coll(sK6(sK3,sK4,sK3,sK4,sK5,sK5,A),sK3,A) ),
inference(resolve,[status(thm)],[c_3161,c_267]) ).
cnf(c_35395,plain,
perp(sK3,A,A,A),
inference(resolve,[status(thm)],[c_3162,c_40136]) ).
cnf(c_35910,plain,
coll(sK1,sK3,A),
inference(resolve,[status(thm)],[c_35141,c_252]) ).
cnf(c_35920,plain,
coll(sK4,A,sK1),
inference(resolve,[status(thm)],[c_35910,c_2828]) ).
cnf(c_35982,plain,
( midp(sK4,A,sK1)
| ~ midp(sK5,A,sK4) ),
inference(resolve,[status(thm)],[c_35920,c_20902]) ).
cnf(c_36673,plain,
para(sK3,A,sK3,A),
inference(resolve,[status(thm)],[c_35074,c_249]) ).
cnf(c_36693,plain,
perp(A,A,sK3,A),
inference(resolve,[status(thm)],[c_35395,c_245]) ).
cnf(c_37044,plain,
( midp(A,B,B)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_36673,c_292]) ).
cnf(c_37186,plain,
perp(sK3,sK3,sK3,A),
inference(resolve,[status(thm)],[c_36693,c_3215]) ).
cnf(c_37668,plain,
perp(sK4,sK0,sK3,A),
inference(resolve,[status(thm)],[c_37186,c_2409]) ).
cnf(c_37669,plain,
para(sK3,sK4,sK3,A),
inference(resolve,[status(thm)],[c_37186,c_1805]) ).
cnf(c_37912,plain,
perp(sK4,sK0,A,sK3),
inference(resolve,[status(thm)],[c_37668,c_246]) ).
cnf(c_37918,plain,
para(sK3,A,sK3,sK4),
inference(resolve,[status(thm)],[c_37669,c_248]) ).
cnf(c_40137,plain,
( midp(A,B,sK4)
| ~ para(sK3,B,sK3,sK4)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_37669,c_194]) ).
cnf(c_37923,plain,
( midp(A,B,sK4)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_37918,c_40137]) ).
cnf(c_37975,plain,
perp(A,sK3,sK4,sK0),
inference(resolve,[status(thm)],[c_37912,c_245]) ).
cnf(c_40138,plain,
( cong(A,sK4,A,sK0)
| ~ midp(sK3,sK4,sK0) ),
inference(resolve,[status(thm)],[c_37975,c_203]) ).
cnf(c_38026,plain,
cong(A,sK4,A,sK0),
inference(resolve,[status(thm)],[c_9775,c_40138]) ).
cnf(c_38056,plain,
cong(A,sK4,sK0,A),
inference(resolve,[status(thm)],[c_38026,c_231]) ).
cnf(c_38074,plain,
cong(sK0,A,A,sK4),
inference(resolve,[status(thm)],[c_38056,c_230]) ).
cnf(c_38126,plain,
cong(sK0,A,sK4,A),
inference(resolve,[status(thm)],[c_38074,c_231]) ).
cnf(c_38134,plain,
perp(sK0,sK4,sK1,A),
inference(resolve,[status(thm)],[c_38126,c_16848]) ).
cnf(c_38505,plain,
( cong(sK0,sK1,sK0,A)
| ~ midp(sK4,sK1,A) ),
inference(resolve,[status(thm)],[c_38134,c_203]) ).
cnf(c_39767,plain,
midp(sK5,A,A),
inference(resolve,[status(thm)],[c_37044,c_6371]) ).
cnf(c_39825,plain,
midp(sK5,A,sK4),
inference(resolve,[status(thm)],[c_37923,c_39767]) ).
cnf(c_39838,plain,
midp(sK4,A,sK1),
inference(resolve,[status(thm)],[c_39825,c_35982]) ).
cnf(c_40118,plain,
midp(sK4,sK1,A),
inference(resolve,[status(thm)],[c_39838,c_242]) ).
cnf(c_40121,plain,
cong(sK0,sK1,sK0,A),
inference(resolve,[status(thm)],[c_40118,c_38505]) ).
cnf(c_40122,plain,
$false,
inference(resolve,[status(thm)],[c_40121,c_147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO590+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.41 % Computer : n005.cluster.edu
% 0.17/0.41 % Model : x86_64 x86_64
% 0.17/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.41 % Memory : 8046.5625MB
% 0.17/0.41 % OS : Linux 6.8.0-71-generic
% 0.17/0.41 % CPULimit : 300
% 0.17/0.41 % WCLimit : 300
% 0.17/0.41 % DateTime : Fri Sep 25 13:43:16 UTC 2026
% 0.17/0.41 % CPUTime :
% 0.17/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.42 % Process 3607872 was started by sandbox on n005,
% 0.17/0.42 % Fri Sep 25 13:43:17 2026
% 0.17/0.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.46
% 0.17/0.46 % From the command line: assign(max_seconds, 300).
% 229.42/30.58
% 229.42/30.58 % given #500 (T,wt=9): 2667 coll(c5,c2,c3). [resolve(2645,a,252,a)].
% 229.42/30.58
% 229.42/30.58 % given #1000 (A,wt=37): 652 -perp(c5,f10(c3,c3,c5,c4),c3,c3) | perp(c5,f10(c5,c3,c3,f10(c3,c3,c5,c4)),c3,c3). [resolve(330,a,163,b)].
% 229.42/30.58
% 229.42/30.58 % given #1500 (T,wt=9): 10211 midp(c3,c5,c1). [resolve(10181,a,2016,a)].
% 229.42/30.58
% 229.42/30.58 % given #2000 (A,wt=34): 1006 -cong(A,c1,A,B) | c4 = A | cong(f13(c1,c2,B,B,A,c4),c4,c4,c1) | -cong(A,c1,A,c2). [resolve(407,a,261,b)].
% 229.42/30.58
% 229.42/30.58 % given #2500 (T,wt=10): 23024 para(c4,c3,c2,c4). [resolve(22735,a,404,a)].
% 229.42/30.58
% 229.42/30.58 % given #3000 (A,wt=19): 1428 perp(c2,f10(c2,c1,c3,c3),c3,c1). [resolve(1147,a,163,a),unit_del(a,1348)].
% 229.42/30.58
% 229.42/30.58 % given #3500 (T,wt=13): 20895 -midp(A,c3,c1) | midp(A,c1,c4). [back_unit_del(20828),unit_del(b,20885)].
% 229.42/30.58
% 229.42/30.58 % given #4000 (A,wt=15): 1972 -cyclic(c2,c2,c1,A) | cyclic(c2,c1,A,c1). [resolve(1723,a,237,b)].
% 229.42/30.58
% 229.42/30.58 % given #4500 (T,wt=14): 7035 -midp(A,c3,c1) | cong(c3,A,c1,A). [resolve(6004,a,205,a)].
% 229.42/30.58
% 229.42/30.58 % given #5000 (A,wt=28): 2378 -midp(f6(c1,c2,c1,c2,c4,c4),A,c1) | -coll(c4,A,c1) | midp(c4,A,c1). [resolve(400,a,208,b)].
% 229.42/30.58
% 229.42/30.58 % given #5500 (T,wt=14): 18106 eqratio(c2,c1,c1,c3,c4,c2,c2,c1). [resolve(17908,a,350,a)].
% 229.42/30.58
% 229.42/30.58 % given #6000 (A,wt=18): 3111 coll(f11(c3,c3,c2,c1),c1,c3). [resolve(1793,a,543,a)].
% 229.42/30.58
% 229.42/30.58 % given #6500 (T,wt=10): 37089 cyclic(c4,c4,A,c1). [back_unit_del(24074),unit_del(a,37063)].
% 229.42/30.58
% 229.42/30.58 % given #7000 (A,wt=33): 3565 para(f6(c2,A,c2,c1,f7(c2,c1,c1,c2,c4,c4,A),c4),c4,c2,c2). [resolve(704,a,338,a)].
% 229.42/30.58
% 229.42/30.58 % given #7500 (T,wt=13): 35690 -midp(c1,A,c4) | midp(c3,A,c1). [back_unit_del(21476),unit_del(b,35629)].
% 229.42/30.58
% 229.42/30.58 % SZS status Theorem for theBenchmark
% 229.42/30.58
% 229.42/30.58 % Proof 1 at 4.55 (+ 1.38) seconds.
% 229.42/30.58 % Length of proof is 261.
% 229.42/30.58 % Level of proof is 24.
% 229.42/30.58 % Maximum clause weight is 37.000.
% 229.42/30.58 % Given clauses 7987.
% 229.42/30.58
% 229.42/30.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------