%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO542+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 : n015.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:04 AM UTC 2026
% Result : Theorem 92.59s 14.26s
% Output : CNFRefutation 92.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 30
% Syntax : Number of formulae : 182 ( 77 unt; 0 def)
% Number of atoms : 357 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 288 ( 113 ~; 109 |; 35 &)
% ( 0 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 8 ( 8 usr; 7 con; 0-4 aty)
% Number of variables : 355 ( 2 sgn 145 !; 9 ?)
% 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(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(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(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(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(ruleD51,axiom,
! [A,B,C,O,M] :
( ( eqangle(A,B,A,C,O,B,O,M)
& coll(M,B,C)
& circle(O,A,B,C) )
=> midp(M,B,C) ),
file('theBenchmark.p',ruleD51) ).
fof(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(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(ruleX11,axiom,
! [A,B,C,O] :
? [P] :
( circle(O,A,B,C)
=> perp(P,A,A,O) ),
file('theBenchmark.p',ruleX11) ).
fof(exemplo6GDDFULL012002,conjecture,
! [A,B,C,A1,B1,C1,O] :
( ( circle(O,A,B,C)
& midp(C1,B,A)
& midp(B1,C,A)
& midp(A1,C,B) )
=> perp(O,A1,B1,C1) ),
file('theBenchmark.p',exemplo6GDDFULL012002) ).
fof(exemplo6GDDFULL012002_neg,negated_conjecture,
~ ! [A,B,C,A1,B1,C1,O] :
( ( circle(O,A,B,C)
& midp(C1,B,A)
& midp(B1,C,A)
& midp(A1,C,B) )
=> perp(O,A1,B1,C1) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL012002]) ).
cnf(c_97,plain,
( circle(A,B,C,D)
| ~ cong(A,B,A,D)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD12]) ).
cnf(c_100,plain,
( midp(E,C,D)
| ~ eqangle(B,C,B,D,A,C,A,E)
| ~ coll(E,C,D)
| ~ circle(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD51]) ).
cnf(c_101,plain,
( perp(B,C,C,D)
| ~ coll(A,B,D)
| ~ circle(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD53]) ).
fof(nnf_87,plain,
! [A,B,C,O] :
? [P] :
( perp(P,A,A,O)
| ~ circle(O,A,B,C) ),
inference(fof_nnf,[status(thm)],[ruleX11]) ).
fof(sk_ruleX11,plain,
! [A,B,C,O] :
( perp(sK0(A,B,C,O),A,A,O)
| ~ circle(O,A,B,C) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(P,sK0(A,B,C,O))],[nnf_87]) ).
cnf(c_102,plain,
( perp(sK0(B,C,D,A),B,B,A)
| ~ circle(A,B,C,D) ),
inference(split_conjunct,[status(thm)],[sk_ruleX11]) ).
fof(nnf_95,plain,
? [A,B,C,A1,B1,C1,O] :
( ~ perp(O,A1,B1,C1)
& circle(O,A,B,C)
& midp(C1,B,A)
& midp(B1,C,A)
& midp(A1,C,B) ),
inference(fof_nnf,[status(thm)],[exemplo6GDDFULL012002_neg]) ).
fof(sk_exemplo6GDDFULL012002_neg,plain,
( ~ perp(sK1,sK5,sK6,sK7)
& circle(sK1,sK2,sK3,sK4)
& midp(sK7,sK3,sK2)
& midp(sK6,sK4,sK2)
& midp(sK5,sK4,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK4,sK3,sK6,sK2,sK7,sK1]),skolemize(A,sK2),skolemize(B,sK3),skolemize(C,sK4),skolemize(A1,sK5),skolemize(B1,sK6),skolemize(C1,sK7),skolemize(O,sK1)],[nnf_95]) ).
cnf(c_109,negated_conjecture,
circle(sK1,sK2,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL012002_neg]) ).
cnf(c_115,negated_conjecture,
perp(sK0(sK2,sK3,sK4,sK1),sK2,sK2,sK1),
inference(resolve,[status(thm)],[c_109,c_102]) ).
cnf(c_157,plain,
( ~ cong(A,B,A,C)
| ~ cong(A,B,A,D)
| perp(B,D,D,C)
| ~ coll(A,B,C) ),
inference(resolve,[status(thm)],[c_101,c_97]) ).
cnf(c_158,plain,
( ~ cong(E,D,E,C)
| ~ cong(E,D,E,B)
| midp(A,B,C)
| ~ eqangle(D,B,D,C,E,B,E,A)
| ~ coll(A,B,C) ),
inference(resolve,[status(thm)],[c_100,c_97]) ).
cnf(c_162,negated_conjecture,
~ perp(sK1,sK5,sK6,sK7),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL012002_neg]) ).
cnf(c_163,negated_conjecture,
midp(sK7,sK3,sK2),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL012002_neg]) ).
cnf(c_164,negated_conjecture,
midp(sK6,sK4,sK2),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL012002_neg]) ).
cnf(c_165,negated_conjecture,
midp(sK5,sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL012002_neg]) ).
cnf(c_201,plain,
( coll(A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD69]) ).
cnf(c_202,plain,
( cong(A,B,A,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD68]) ).
cnf(c_203,plain,
( midp(A,B,C)
| ~ coll(A,B,C)
| ~ cong(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD67]) ).
cnf(c_204,plain,
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD66]) ).
cnf(c_206,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_207,plain,
( para(B,D,C,E)
| ~ midp(A,D,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD63]) ).
cnf(c_214,plain,
( perp(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD56]) ).
cnf(c_217,plain,
( cong(A,D,B,D)
| ~ midp(D,A,C)
| ~ perp(A,B,B,C) ),
inference(clausify,[status(thm)],[ruleD52]) ).
cnf(c_221,plain,
( para(A,D,C,E)
| ~ midp(D,B,E)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD44]) ).
cnf(c_222,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_225,plain,
( eqangle(C,A,C,B,D,A,D,B)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD41]) ).
cnf(c_241,plain,
( cong(A,B,E,F)
| ~ cong(C,D,E,F)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD25]) ).
cnf(c_242,plain,
( cong(C,D,A,B)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD24]) ).
cnf(c_243,plain,
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD23]) ).
cnf(c_249,plain,
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD17]) ).
cnf(c_253,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_254,plain,
( midp(A,C,B)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD11]) ).
cnf(c_255,plain,
( perp(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD10]) ).
cnf(c_256,plain,
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD9]) ).
cnf(c_257,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD8]) ).
cnf(c_258,plain,
( perp(A,B,D,C)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD7]) ).
cnf(c_261,plain,
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD4]) ).
cnf(c_262,plain,
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD3]) ).
cnf(c_263,plain,
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD2]) ).
cnf(c_264,plain,
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD1]) ).
cnf(c_279,plain,
( ~ cong(A,B,A,C)
| perp(B,C,C,C)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_157]) ).
cnf(c_280,plain,
( ~ cong(D,C,D,B)
| midp(A,B,B)
| ~ eqangle(C,B,C,B,D,B,D,A)
| ~ coll(A,B,B) ),
inference(factor,[status(thm)],[c_158]) ).
cnf(c_304,plain,
( midp(A,D,D)
| ~ para(B,D,C,D)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_206]) ).
cnf(c_310,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_222]) ).
cnf(c_313,plain,
( cyclic(B,C,D,D)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_249]) ).
cnf(c_314,plain,
( cyclic(B,C,C,D)
| ~ cong(A,B,A,D)
| ~ cong(A,B,A,C) ),
inference(factor,[status(thm)],[c_253]) ).
cnf(c_318,plain,
( coll(C,C,A)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_262]) ).
cnf(c_326,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_310]) ).
cnf(c_327,plain,
( cyclic(B,C,C,C)
| ~ cong(A,B,A,C) ),
inference(factor,[status(thm)],[c_314]) ).
cnf(c_369,plain,
coll(sK5,sK4,sK3),
inference(resolve,[status(thm)],[c_201,c_165]) ).
cnf(c_371,plain,
coll(sK7,sK3,sK2),
inference(resolve,[status(thm)],[c_201,c_163]) ).
cnf(c_372,plain,
cong(sK5,sK4,sK5,sK3),
inference(resolve,[status(thm)],[c_202,c_165]) ).
cnf(c_374,plain,
cong(sK7,sK3,sK7,sK2),
inference(resolve,[status(thm)],[c_202,c_163]) ).
cnf(c_375,plain,
( para(sK4,A,sK3,B)
| ~ midp(sK5,A,B) ),
inference(resolve,[status(thm)],[c_207,c_165]) ).
cnf(c_378,plain,
( para(A,sK4,B,sK3)
| ~ midp(sK5,A,B) ),
inference(resolve,[status(thm)],[c_207,c_165]) ).
cnf(c_380,plain,
( para(A,sK3,B,sK2)
| ~ midp(sK7,A,B) ),
inference(resolve,[status(thm)],[c_207,c_163]) ).
cnf(c_389,plain,
midp(sK5,sK3,sK4),
inference(resolve,[status(thm)],[c_254,c_165]) ).
cnf(c_390,plain,
midp(sK6,sK2,sK4),
inference(resolve,[status(thm)],[c_254,c_164]) ).
cnf(c_391,plain,
midp(sK7,sK2,sK3),
inference(resolve,[status(thm)],[c_254,c_163]) ).
cnf(c_393,plain,
( para(A,B,sK2,sK1)
| ~ perp(A,B,sK0(sK2,sK3,sK4,sK1),sK2) ),
inference(resolve,[status(thm)],[c_256,c_115]) ).
cnf(c_394,plain,
perp(sK2,sK1,sK0(sK2,sK3,sK4,sK1),sK2),
inference(resolve,[status(thm)],[c_257,c_115]) ).
cnf(c_418,plain,
coll(sK3,sK3,sK5),
inference(resolve,[status(thm)],[c_369,c_318]) ).
cnf(c_419,plain,
coll(sK5,sK3,sK4),
inference(resolve,[status(thm)],[c_369,c_264]) ).
cnf(c_428,plain,
coll(sK2,sK2,sK7),
inference(resolve,[status(thm)],[c_371,c_318]) ).
cnf(c_429,plain,
coll(sK7,sK2,sK3),
inference(resolve,[status(thm)],[c_371,c_264]) ).
cnf(c_443,plain,
( para(A,sK3,B,sK4)
| ~ midp(sK5,A,B) ),
inference(resolve,[status(thm)],[c_389,c_207]) ).
cnf(c_445,plain,
cong(sK5,sK3,sK5,sK4),
inference(resolve,[status(thm)],[c_389,c_202]) ).
cnf(c_465,plain,
( para(A,sK6,B,sK4)
| ~ midp(A,sK2,B) ),
inference(resolve,[status(thm)],[c_390,c_221]) ).
cnf(c_490,plain,
( para(A,sK2,B,sK3)
| ~ midp(sK7,A,B) ),
inference(resolve,[status(thm)],[c_391,c_207]) ).
cnf(c_491,plain,
( para(sK2,A,sK3,B)
| ~ midp(sK7,A,B) ),
inference(resolve,[status(thm)],[c_391,c_207]) ).
cnf(c_492,plain,
cong(sK7,sK2,sK7,sK3),
inference(resolve,[status(thm)],[c_391,c_202]) ).
cnf(c_504,plain,
coll(sK3,sK5,sK3),
inference(resolve,[status(thm)],[c_418,c_264]) ).
cnf(c_530,plain,
coll(sK2,sK7,sK2),
inference(resolve,[status(thm)],[c_428,c_264]) ).
cnf(c_531,plain,
( coll(A,sK7,sK2)
| ~ coll(sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_428,c_262]) ).
cnf(c_535,plain,
( coll(A,sK3,sK7)
| ~ coll(sK7,sK2,A) ),
inference(resolve,[status(thm)],[c_429,c_262]) ).
cnf(c_545,plain,
coll(sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_504,c_318]) ).
cnf(c_546,plain,
coll(sK5,sK3,sK3),
inference(resolve,[status(thm)],[c_504,c_263]) ).
cnf(c_605,plain,
coll(sK7,sK2,sK2),
inference(resolve,[status(thm)],[c_530,c_263]) ).
cnf(c_812,plain,
cyclic(sK4,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_372,c_327]) ).
cnf(c_869,plain,
cong(sK5,sK4,sK3,sK5),
inference(resolve,[status(thm)],[c_372,c_243]) ).
cnf(c_870,plain,
( cong(A,B,sK5,sK3)
| ~ cong(A,B,sK5,sK4) ),
inference(resolve,[status(thm)],[c_372,c_241]) ).
cnf(c_1004,plain,
( cong(A,B,sK7,sK2)
| ~ cong(A,B,sK7,sK3) ),
inference(resolve,[status(thm)],[c_374,c_241]) ).
cnf(c_44101,plain,
( perp(sK3,sK4,sK4,sK4)
| ~ coll(sK5,sK3,sK4) ),
inference(resolve,[status(thm)],[c_445,c_279]) ).
cnf(c_1155,plain,
perp(sK3,sK4,sK4,sK4),
inference(resolve,[status(thm)],[c_419,c_44101]) ).
cnf(c_1404,plain,
cyclic(sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_812,c_313]) ).
cnf(c_1436,plain,
cong(sK3,sK5,sK5,sK4),
inference(resolve,[status(thm)],[c_869,c_242]) ).
cnf(c_1591,plain,
( cong(sK3,A,sK4,A)
| ~ midp(A,sK3,sK4) ),
inference(resolve,[status(thm)],[c_1155,c_217]) ).
cnf(c_1682,plain,
para(sK4,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_375,c_389]) ).
cnf(c_1717,plain,
eqangle(sK3,sK3,sK3,sK3,sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_1404,c_225]) ).
cnf(c_1743,plain,
cong(sK3,sK5,sK4,sK5),
inference(resolve,[status(thm)],[c_1436,c_243]) ).
cnf(c_1824,plain,
para(sK2,sK3,sK3,sK2),
inference(resolve,[status(thm)],[c_380,c_391]) ).
cnf(c_1853,plain,
( perp(sK4,sK3,A,B)
| ~ perp(sK3,sK4,A,B) ),
inference(resolve,[status(thm)],[c_1682,c_255]) ).
cnf(c_1948,plain,
( perp(sK3,sK4,A,sK5)
| ~ cong(sK3,A,sK4,A) ),
inference(resolve,[status(thm)],[c_1743,c_214]) ).
cnf(c_2084,plain,
para(sK2,sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_1824,c_261]) ).
cnf(c_2168,plain,
para(sK2,sK1,sK2,sK1),
inference(resolve,[status(thm)],[c_394,c_393]) ).
cnf(c_2464,plain,
( midp(A,sK3,sK3)
| ~ midp(A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_2084,c_304]) ).
cnf(c_2564,plain,
( midp(A,sK1,sK1)
| ~ midp(A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_2168,c_304]) ).
cnf(c_2571,plain,
coll(sK2,sK1,sK1),
inference(resolve,[status(thm)],[c_2168,c_204]) ).
cnf(c_2578,plain,
coll(sK1,sK1,sK2),
inference(resolve,[status(thm)],[c_2571,c_318]) ).
cnf(c_2586,plain,
coll(sK2,sK2,sK1),
inference(resolve,[status(thm)],[c_2578,c_318]) ).
cnf(c_3730,plain,
para(sK7,sK6,sK3,sK4),
inference(resolve,[status(thm)],[c_465,c_391]) ).
cnf(c_3758,plain,
para(sK7,sK6,sK4,sK3),
inference(resolve,[status(thm)],[c_3730,c_261]) ).
cnf(c_3797,plain,
( perp(sK7,sK6,A,B)
| ~ perp(sK4,sK3,A,B) ),
inference(resolve,[status(thm)],[c_3758,c_255]) ).
cnf(c_4412,plain,
coll(sK1,sK7,sK2),
inference(resolve,[status(thm)],[c_531,c_2586]) ).
cnf(c_4420,plain,
coll(sK7,sK1,sK2),
inference(resolve,[status(thm)],[c_4412,c_263]) ).
cnf(c_4429,plain,
coll(sK7,sK2,sK1),
inference(resolve,[status(thm)],[c_4420,c_264]) ).
cnf(c_4440,plain,
coll(sK1,sK3,sK7),
inference(resolve,[status(thm)],[c_4429,c_535]) ).
cnf(c_4462,plain,
coll(sK1,sK7,sK3),
inference(resolve,[status(thm)],[c_4440,c_264]) ).
cnf(c_4487,plain,
coll(sK3,sK3,sK1),
inference(resolve,[status(thm)],[c_4462,c_318]) ).
cnf(c_4506,plain,
coll(sK3,sK1,sK3),
inference(resolve,[status(thm)],[c_4487,c_264]) ).
cnf(c_4537,plain,
coll(sK1,sK3,sK3),
inference(resolve,[status(thm)],[c_4506,c_263]) ).
cnf(c_6282,plain,
cong(sK5,sK3,sK5,sK3),
inference(resolve,[status(thm)],[c_870,c_445]) ).
cnf(c_44102,plain,
( midp(sK5,sK3,sK3)
| ~ coll(sK5,sK3,sK3) ),
inference(resolve,[status(thm)],[c_6282,c_203]) ).
cnf(c_6350,plain,
midp(sK5,sK3,sK3),
inference(resolve,[status(thm)],[c_546,c_44102]) ).
cnf(c_6400,plain,
para(sK3,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_6350,c_443]) ).
cnf(c_6405,plain,
para(sK3,sK4,sK3,sK3),
inference(resolve,[status(thm)],[c_6350,c_378]) ).
cnf(c_44103,plain,
( midp(A,sK3,sK4)
| ~ para(sK3,sK4,sK3,sK3)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_6400,c_206]) ).
cnf(c_7050,plain,
( midp(A,sK3,sK4)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_6405,c_44103]) ).
cnf(c_11071,plain,
cong(sK7,sK2,sK7,sK2),
inference(resolve,[status(thm)],[c_1004,c_492]) ).
cnf(c_44104,plain,
( midp(sK7,sK2,sK2)
| ~ coll(sK7,sK2,sK2) ),
inference(resolve,[status(thm)],[c_11071,c_203]) ).
cnf(c_11162,plain,
midp(sK7,sK2,sK2),
inference(resolve,[status(thm)],[c_605,c_44104]) ).
cnf(c_11169,plain,
midp(sK7,sK1,sK1),
inference(resolve,[status(thm)],[c_11162,c_2564]) ).
cnf(c_11170,plain,
midp(sK7,sK3,sK3),
inference(resolve,[status(thm)],[c_11162,c_2464]) ).
cnf(c_11274,plain,
para(sK2,sK1,sK3,sK1),
inference(resolve,[status(thm)],[c_11169,c_491]) ).
cnf(c_11361,plain,
para(sK3,sK2,sK3,sK3),
inference(resolve,[status(thm)],[c_11170,c_490]) ).
cnf(c_11384,plain,
para(sK3,sK3,sK3,sK2),
inference(resolve,[status(thm)],[c_11170,c_380]) ).
cnf(c_11937,plain,
( midp(A,sK1,sK1)
| ~ midp(A,sK2,sK3) ),
inference(resolve,[status(thm)],[c_11274,c_304]) ).
cnf(c_44105,plain,
( midp(A,sK2,sK3)
| ~ para(sK3,sK3,sK3,sK2)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_11361,c_206]) ).
cnf(c_12114,plain,
( midp(A,sK2,sK3)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_11384,c_44105]) ).
cnf(c_44106,plain,
( cong(sK3,sK3,sK3,sK3)
| ~ cyclic(sK3,sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_1717,c_326]) ).
cnf(c_23313,plain,
cong(sK3,sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_1404,c_44106]) ).
cnf(c_44107,plain,
( ~ cong(sK3,sK3,sK3,sK3)
| midp(sK3,sK3,sK3)
| ~ coll(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_1717,c_280]) ).
cnf(c_44108,plain,
( ~ cong(sK3,sK3,sK3,sK3)
| midp(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_545,c_44107]) ).
cnf(c_23315,plain,
midp(sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_23313,c_44108]) ).
cnf(c_23347,plain,
midp(sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_23315,c_12114]) ).
cnf(c_23538,plain,
midp(sK3,sK1,sK1),
inference(resolve,[status(thm)],[c_23347,c_11937]) ).
cnf(c_23920,plain,
cong(sK3,sK1,sK3,sK1),
inference(resolve,[status(thm)],[c_23538,c_202]) ).
cnf(c_25239,plain,
cong(sK3,sK1,sK1,sK3),
inference(resolve,[status(thm)],[c_23920,c_243]) ).
cnf(c_26459,plain,
cong(sK1,sK3,sK3,sK1),
inference(resolve,[status(thm)],[c_25239,c_242]) ).
cnf(c_27758,plain,
cong(sK1,sK3,sK1,sK3),
inference(resolve,[status(thm)],[c_26459,c_243]) ).
cnf(c_44109,plain,
( midp(sK1,sK3,sK3)
| ~ coll(sK1,sK3,sK3) ),
inference(resolve,[status(thm)],[c_27758,c_203]) ).
cnf(c_28410,plain,
midp(sK1,sK3,sK3),
inference(resolve,[status(thm)],[c_4537,c_44109]) ).
cnf(c_28416,plain,
midp(sK1,sK3,sK4),
inference(resolve,[status(thm)],[c_28410,c_7050]) ).
cnf(c_28597,plain,
cong(sK3,sK1,sK4,sK1),
inference(resolve,[status(thm)],[c_28416,c_1591]) ).
cnf(c_33224,plain,
perp(sK3,sK4,sK1,sK5),
inference(resolve,[status(thm)],[c_1948,c_28597]) ).
cnf(c_33704,plain,
perp(sK4,sK3,sK1,sK5),
inference(resolve,[status(thm)],[c_33224,c_1853]) ).
cnf(c_43033,plain,
perp(sK7,sK6,sK1,sK5),
inference(resolve,[status(thm)],[c_3797,c_33704]) ).
cnf(c_43770,plain,
perp(sK1,sK5,sK7,sK6),
inference(resolve,[status(thm)],[c_43033,c_257]) ).
cnf(c_44110,plain,
perp(sK1,sK5,sK6,sK7),
inference(resolve,[status(thm)],[c_43770,c_258]) ).
cnf(c_44100,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_162,c_44110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO542+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.05/0.35 % Computer : n015.cluster.edu
% 0.05/0.35 % Model : x86_64 x86_64
% 0.05/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.35 % Memory : 8046.5625MB
% 0.05/0.35 % OS : Linux 6.8.0-71-generic
% 0.05/0.35 % CPULimit : 300
% 0.05/0.35 % WCLimit : 300
% 0.05/0.35 % DateTime : Fri Sep 25 13:44:12 UTC 2026
% 0.05/0.36 % CPUTime :
% 0.05/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.05/0.36 % Process 1494451 was started by sandbox on n015,
% 0.05/0.36 % Fri Sep 25 13:44:12 2026
% 0.05/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).
% 92.59/14.26
% 92.59/14.26 % given #500 (T,wt=7): 2479 para(c3,c1,c4,c6). [resolve(2096,a,260,a)].
% 92.59/14.26
% 92.59/14.26 % given #1000 (A,wt=15): 741 para(f6(c1,c3,c3,c1,c5,c5),c5,c1,c3). [resolve(349,a,390,a)].
% 92.59/14.26
% 92.59/14.26 % given #1500 (T,wt=10): 4201 -coll(c6,c5,A) | coll(A,c5,c6). [resolve(4157,a,262,b)].
% 92.59/14.26
% 92.59/14.26 % given #2000 (A,wt=28): 1045 -midp(A,c3,c1) | -para(c3,c3,B,A) | -coll(c3,c1,B) | coll(f8(c3,c1,C,c3,c1,B,A),A,B). [resolve(413,a,180,c)].
% 92.59/14.26
% 92.59/14.26 % given #2500 (T,wt=7): 18990 cong(c1,c4,c2,c4). [resolve(18953,a,243,a)].
% 92.59/14.26
% 92.59/14.26 % given #3000 (A,wt=15): 1306 -coll(A,c6,c2) | eqratio(A,c6,c6,c2,A,c6,c6,c2). [resolve(480,a,303,a)].
% 92.59/14.26
% 92.59/14.26 % given #3500 (T,wt=7): 25245 para(c3,c2,c4,c1). [resolve(23966,a,260,a)].
% 92.59/14.26
% 92.59/14.26 % given #4000 (A,wt=12): 1642 -perp(A,B,c1,c3) | para(A,B,c3,c3). [resolve(1249,a,256,b)].
% 92.59/14.26
% 92.59/14.26 % given #4500 (T,wt=7): 32213 cong(c3,c2,c4,c2). [resolve(31740,a,242,a)].
% 92.59/14.26
% 92.59/14.26 % given #5000 (A,wt=19): 2114 -cong(c1,A,c1,B) | cong(c1,A,c1,f9(c3,c3,A,B,c1)). [resolve(1835,a,179,b)].
% 92.59/14.26
% 92.59/14.26 % given #5500 (T,wt=7): 37653 para(c5,c4,c7,c5). [resolve(2275,a,29858,a)].
% 92.59/14.26
% 92.59/14.26 % given #6000 (A,wt=19): 2627 -midp(A,c3,B) | para(A,f6(c3,c2,c3,c2,c4,c4),B,c2). [resolve(406,a,221,b)].
% 92.59/14.26
% 92.59/14.26 % given #6500 (T,wt=7): 39974 cyclic(c4,c2,c1,c2). [resolve(39252,a,251,a)].
% 92.59/14.26
% 92.59/14.26 % given #7000 (A,wt=17): 3238 -coll(f16(c2,c1,c2,c1),c2,c2) | perp(c2,c1,c1,c2). [resolve(3021,a,128,b),unit_del(a,1873)].
% 92.59/14.26
% 92.59/14.26 % given #7500 (T,wt=7): 42388 cong(c1,c7,c2,c1). [resolve(41872,a,243,a)].
% 92.59/14.26
% 92.59/14.26 % SZS status Theorem for theBenchmark
% 92.59/14.26
% 92.59/14.26 % Proof 1 at 4.49 (+ 1.25) seconds.
% 92.59/14.26 % Length of proof is 167.
% 92.59/14.26 % Level of proof is 23.
% 92.59/14.26 % Maximum clause weight is 31.000.
% 92.59/14.26 % Given clauses 7988.
% 92.59/14.26
% 92.59/14.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------