%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO575+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 : n010.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:08 AM UTC 2026
% Result : Theorem 40.49s 5.68s
% Output : CNFRefutation 40.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 32
% Syntax : Number of formulae : 285 ( 146 unt; 0 def)
% Number of atoms : 520 ( 0 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 391 ( 156 ~; 152 |; 50 &)
% ( 0 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-8 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-4 aty)
% Number of variables : 553 ( 86 sgn 162 !; 11 ?)
% 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(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(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(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(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(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(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(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(ruleX11,axiom,
! [A,B,C,O] :
? [P] :
( circle(O,A,B,C)
=> perp(P,A,A,O) ),
file('theBenchmark.p',ruleX11) ).
fof(exemplo6GDDFULL214037,conjecture,
! [A,B,C,O,H,C1,A1,NWPNT1,NWPNT2] :
( ( coll(A1,A,H)
& circle(O,A,A1,NWPNT2)
& coll(C1,C,H)
& circle(O,C,C1,NWPNT1)
& perp(B,C,A,H)
& perp(A,C,B,H)
& perp(A,B,C,H)
& circle(O,A,B,C) )
=> cong(B,A1,B,C1) ),
file('theBenchmark.p',exemplo6GDDFULL214037) ).
fof(exemplo6GDDFULL214037_neg,negated_conjecture,
~ ! [A,B,C,O,H,C1,A1,NWPNT1,NWPNT2] :
( ( coll(A1,A,H)
& circle(O,A,A1,NWPNT2)
& coll(C1,C,H)
& circle(O,C,C1,NWPNT1)
& perp(B,C,A,H)
& perp(A,C,B,H)
& perp(A,B,C,H)
& circle(O,A,B,C) )
=> cong(B,A1,B,C1) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL214037]) ).
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,O,H,C1,A1,NWPNT1,NWPNT2] :
( ~ cong(B,A1,B,C1)
& coll(A1,A,H)
& circle(O,A,A1,NWPNT2)
& coll(C1,C,H)
& circle(O,C,C1,NWPNT1)
& perp(B,C,A,H)
& perp(A,C,B,H)
& perp(A,B,C,H)
& circle(O,A,B,C) ),
inference(fof_nnf,[status(thm)],[exemplo6GDDFULL214037_neg]) ).
fof(sk_exemplo6GDDFULL214037_neg,plain,
( ~ cong(sK3,sK7,sK3,sK5)
& coll(sK7,sK2,sK8)
& circle(sK1,sK2,sK7,sK9)
& coll(sK5,sK4,sK8)
& circle(sK1,sK4,sK5,sK6)
& perp(sK3,sK4,sK2,sK8)
& perp(sK2,sK4,sK3,sK8)
& perp(sK2,sK3,sK4,sK8)
& circle(sK1,sK2,sK3,sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK8,sK5,sK6,sK7,sK9]),skolemize(A,sK2),skolemize(B,sK3),skolemize(C,sK4),skolemize(O,sK1),skolemize(H,sK8),skolemize(C1,sK5),skolemize(A1,sK7),skolemize(NWPNT1,sK6),skolemize(NWPNT2,sK9)],[nnf_95]) ).
cnf(c_109,negated_conjecture,
circle(sK1,sK2,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214037_neg]) ).
cnf(c_110,negated_conjecture,
circle(sK1,sK4,sK5,sK6),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214037_neg]) ).
cnf(c_131,negated_conjecture,
perp(sK0(sK4,sK5,sK6,sK1),sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_110,c_102]) ).
cnf(c_144,negated_conjecture,
( perp(sK2,sK3,sK3,sK4)
| ~ coll(sK1,sK2,sK4) ),
inference(resolve,[status(thm)],[c_109,c_101]) ).
cnf(c_145,negated_conjecture,
perp(sK0(sK2,sK3,sK4,sK1),sK2,sK2,sK1),
inference(resolve,[status(thm)],[c_109,c_102]) ).
cnf(c_188,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_192,negated_conjecture,
~ cong(sK3,sK7,sK3,sK5),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214037_neg]) ).
cnf(c_193,negated_conjecture,
coll(sK7,sK2,sK8),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214037_neg]) ).
cnf(c_194,negated_conjecture,
coll(sK5,sK4,sK8),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214037_neg]) ).
cnf(c_195,negated_conjecture,
perp(sK3,sK4,sK2,sK8),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214037_neg]) ).
cnf(c_196,negated_conjecture,
perp(sK2,sK4,sK3,sK8),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214037_neg]) ).
cnf(c_197,negated_conjecture,
perp(sK2,sK3,sK4,sK8),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214037_neg]) ).
cnf(c_236,plain,
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD66]) ).
cnf(c_238,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_245,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_246,plain,
( perp(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD56]) ).
cnf(c_247,plain,
( cong(D,B,D,C)
| ~ perp(D,A,B,C)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD55]) ).
cnf(c_249,plain,
( cong(A,D,B,D)
| ~ midp(D,A,C)
| ~ perp(A,B,B,C) ),
inference(clausify,[status(thm)],[ruleD52]) ).
cnf(c_252,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_254,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_255,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_258,plain,
( eqangle(A,B,E,F,C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD40]) ).
cnf(c_259,plain,
( para(A,B,E,F)
| ~ eqangle(A,B,C,D,E,F,C,D) ),
inference(clausify,[status(thm)],[ruleD39]) ).
cnf(c_274,plain,
( cong(C,D,A,B)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD24]) ).
cnf(c_275,plain,
( cong(A,B,D,C)
| ~ cong(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD23]) ).
cnf(c_279,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_281,plain,
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD17]) ).
cnf(c_282,plain,
( cyclic(B,A,C,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD16]) ).
cnf(c_283,plain,
( cyclic(A,C,B,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD15]) ).
cnf(c_284,plain,
( cyclic(A,B,D,C)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD14]) ).
cnf(c_286,plain,
( midp(A,C,B)
| ~ midp(A,B,C) ),
inference(clausify,[status(thm)],[ruleD11]) ).
cnf(c_288,plain,
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD9]) ).
cnf(c_289,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD8]) ).
cnf(c_290,plain,
( perp(A,B,D,C)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD7]) ).
cnf(c_292,plain,
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD5]) ).
cnf(c_293,plain,
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD4]) ).
cnf(c_294,plain,
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD3]) ).
cnf(c_295,plain,
( coll(B,A,C)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD2]) ).
cnf(c_296,plain,
( coll(A,C,B)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD1]) ).
cnf(c_312,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_188]) ).
cnf(c_336,plain,
( midp(A,D,D)
| ~ para(B,D,C,D)
| ~ midp(A,B,C) ),
inference(factor,[status(thm)],[c_238]) ).
cnf(c_339,plain,
( perp(B,A,A,B)
| ~ cyclic(A,C,B,B)
| ~ cong(A,B,C,B) ),
inference(factor,[status(thm)],[c_245]) ).
cnf(c_342,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_254]) ).
cnf(c_345,plain,
( cyclic(B,C,D,D)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_281]) ).
cnf(c_350,plain,
( coll(C,C,A)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_294]) ).
cnf(c_448,plain,
( para(sK2,sK3,A,B)
| ~ perp(sK4,sK8,A,B) ),
inference(resolve,[status(thm)],[c_288,c_197]) ).
cnf(c_450,plain,
( para(sK3,sK4,A,B)
| ~ perp(sK2,sK8,A,B) ),
inference(resolve,[status(thm)],[c_288,c_195]) ).
cnf(c_455,plain,
( para(A,B,sK3,sK8)
| ~ perp(A,B,sK2,sK4) ),
inference(resolve,[status(thm)],[c_288,c_196]) ).
cnf(c_456,plain,
( para(A,B,sK2,sK8)
| ~ perp(A,B,sK3,sK4) ),
inference(resolve,[status(thm)],[c_288,c_195]) ).
cnf(c_457,plain,
( para(A,B,sK2,sK1)
| ~ perp(A,B,sK0(sK2,sK3,sK4,sK1),sK2) ),
inference(resolve,[status(thm)],[c_288,c_145]) ).
cnf(c_458,plain,
( para(A,B,sK4,sK1)
| ~ perp(A,B,sK0(sK4,sK5,sK6,sK1),sK4) ),
inference(resolve,[status(thm)],[c_288,c_131]) ).
cnf(c_460,plain,
perp(sK4,sK8,sK2,sK3),
inference(resolve,[status(thm)],[c_289,c_197]) ).
cnf(c_462,plain,
perp(sK2,sK8,sK3,sK4),
inference(resolve,[status(thm)],[c_289,c_195]) ).
cnf(c_463,plain,
perp(sK2,sK1,sK0(sK2,sK3,sK4,sK1),sK2),
inference(resolve,[status(thm)],[c_289,c_145]) ).
cnf(c_464,plain,
perp(sK4,sK1,sK0(sK4,sK5,sK6,sK1),sK4),
inference(resolve,[status(thm)],[c_289,c_131]) ).
cnf(c_467,plain,
perp(sK2,sK4,sK8,sK3),
inference(resolve,[status(thm)],[c_290,c_196]) ).
cnf(c_477,plain,
coll(sK2,sK7,sK8),
inference(resolve,[status(thm)],[c_295,c_193]) ).
cnf(c_478,plain,
coll(sK5,sK8,sK4),
inference(resolve,[status(thm)],[c_296,c_194]) ).
cnf(c_480,plain,
coll(sK8,sK8,sK5),
inference(resolve,[status(thm)],[c_350,c_194]) ).
cnf(c_486,plain,
coll(sK8,sK8,sK2),
inference(resolve,[status(thm)],[c_477,c_350]) ).
cnf(c_493,plain,
( coll(sK4,A,sK5)
| ~ coll(sK5,sK8,A) ),
inference(resolve,[status(thm)],[c_478,c_294]) ).
cnf(c_500,plain,
( coll(A,sK5,sK8)
| ~ coll(sK8,sK8,A) ),
inference(resolve,[status(thm)],[c_480,c_294]) ).
cnf(c_501,plain,
( coll(sK5,A,sK8)
| ~ coll(sK8,sK8,A) ),
inference(resolve,[status(thm)],[c_480,c_294]) ).
cnf(c_514,plain,
coll(sK2,sK2,sK8),
inference(resolve,[status(thm)],[c_486,c_350]) ).
cnf(c_557,plain,
( coll(A,sK8,sK2)
| ~ coll(sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_514,c_294]) ).
cnf(c_624,plain,
perp(sK4,sK8,sK3,sK2),
inference(resolve,[status(thm)],[c_460,c_290]) ).
cnf(c_652,plain,
perp(sK2,sK8,sK4,sK3),
inference(resolve,[status(thm)],[c_462,c_290]) ).
cnf(c_695,plain,
perp(sK8,sK3,sK2,sK4),
inference(resolve,[status(thm)],[c_467,c_289]) ).
cnf(c_904,plain,
coll(sK2,sK5,sK8),
inference(resolve,[status(thm)],[c_500,c_486]) ).
cnf(c_907,plain,
coll(sK5,sK2,sK8),
inference(resolve,[status(thm)],[c_904,c_295]) ).
cnf(c_918,plain,
coll(sK5,sK8,sK2),
inference(resolve,[status(thm)],[c_907,c_296]) ).
cnf(c_937,plain,
coll(sK4,sK2,sK5),
inference(resolve,[status(thm)],[c_918,c_493]) ).
cnf(c_981,plain,
coll(sK4,sK5,sK2),
inference(resolve,[status(thm)],[c_937,c_296]) ).
cnf(c_1031,plain,
( coll(A,sK2,sK4)
| ~ coll(sK4,sK5,A) ),
inference(resolve,[status(thm)],[c_981,c_294]) ).
cnf(c_1160,plain,
para(sK2,sK3,sK3,sK2),
inference(resolve,[status(thm)],[c_448,c_624]) ).
cnf(c_1161,plain,
para(sK2,sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_448,c_460]) ).
cnf(c_1166,plain,
para(sK3,sK2,sK2,sK3),
inference(resolve,[status(thm)],[c_1160,c_292]) ).
cnf(c_1181,plain,
eqangle(sK2,sK3,A,B,sK2,sK3,A,B),
inference(resolve,[status(thm)],[c_1161,c_258]) ).
cnf(c_1184,plain,
coll(sK2,sK3,sK3),
inference(resolve,[status(thm)],[c_1161,c_236]) ).
cnf(c_1192,plain,
coll(sK3,sK2,sK3),
inference(resolve,[status(thm)],[c_1184,c_295]) ).
cnf(c_1202,plain,
coll(sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_1192,c_350]) ).
cnf(c_1215,plain,
para(sK3,sK4,sK4,sK3),
inference(resolve,[status(thm)],[c_450,c_652]) ).
cnf(c_1216,plain,
para(sK3,sK4,sK3,sK4),
inference(resolve,[status(thm)],[c_450,c_462]) ).
cnf(c_1280,plain,
para(sK8,sK3,sK3,sK8),
inference(resolve,[status(thm)],[c_455,c_695]) ).
cnf(c_1312,plain,
para(sK2,sK1,sK2,sK1),
inference(resolve,[status(thm)],[c_463,c_457]) ).
cnf(c_1345,plain,
para(sK4,sK1,sK4,sK1),
inference(resolve,[status(thm)],[c_464,c_458]) ).
cnf(c_1499,plain,
para(sK3,sK2,sK3,sK2),
inference(resolve,[status(thm)],[c_1166,c_293]) ).
cnf(c_1544,plain,
para(sK4,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_1215,c_292]) ).
cnf(c_1559,plain,
eqangle(sK3,sK4,A,B,sK3,sK4,A,B),
inference(resolve,[status(thm)],[c_1216,c_258]) ).
cnf(c_1600,plain,
para(sK8,sK3,sK8,sK3),
inference(resolve,[status(thm)],[c_1280,c_293]) ).
cnf(c_1654,plain,
( midp(A,sK1,sK1)
| ~ midp(A,sK2,sK2) ),
inference(resolve,[status(thm)],[c_1312,c_336]) ).
cnf(c_1657,plain,
para(sK2,sK1,sK1,sK2),
inference(resolve,[status(thm)],[c_1312,c_293]) ).
cnf(c_1658,plain,
eqangle(sK2,sK1,A,B,sK2,sK1,A,B),
inference(resolve,[status(thm)],[c_1312,c_258]) ).
cnf(c_1661,plain,
coll(sK2,sK1,sK1),
inference(resolve,[status(thm)],[c_1312,c_236]) ).
cnf(c_1668,plain,
coll(sK1,sK1,sK2),
inference(resolve,[status(thm)],[c_1661,c_350]) ).
cnf(c_1680,plain,
coll(sK2,sK2,sK1),
inference(resolve,[status(thm)],[c_1668,c_350]) ).
cnf(c_1694,plain,
coll(sK1,sK8,sK2),
inference(resolve,[status(thm)],[c_1680,c_557]) ).
cnf(c_1724,plain,
coll(sK1,sK2,sK8),
inference(resolve,[status(thm)],[c_1694,c_296]) ).
cnf(c_1756,plain,
coll(sK8,sK8,sK1),
inference(resolve,[status(thm)],[c_1724,c_350]) ).
cnf(c_1823,plain,
coll(sK5,sK1,sK8),
inference(resolve,[status(thm)],[c_1756,c_501]) ).
cnf(c_1926,plain,
coll(sK5,sK8,sK1),
inference(resolve,[status(thm)],[c_1823,c_296]) ).
cnf(c_2002,plain,
coll(sK4,sK1,sK5),
inference(resolve,[status(thm)],[c_1926,c_493]) ).
cnf(c_2067,plain,
coll(sK4,sK5,sK1),
inference(resolve,[status(thm)],[c_2002,c_296]) ).
cnf(c_2156,plain,
para(sK4,sK1,sK1,sK4),
inference(resolve,[status(thm)],[c_1345,c_293]) ).
cnf(c_2166,plain,
( midp(A,sK2,sK2)
| ~ midp(A,sK3,sK3) ),
inference(resolve,[status(thm)],[c_1499,c_336]) ).
cnf(c_2169,plain,
eqangle(sK3,sK2,A,B,sK3,sK2,A,B),
inference(resolve,[status(thm)],[c_1499,c_258]) ).
cnf(c_2233,plain,
para(sK4,sK3,sK4,sK3),
inference(resolve,[status(thm)],[c_1544,c_293]) ).
cnf(c_2260,plain,
eqangle(sK8,sK3,A,B,sK8,sK3,A,B),
inference(resolve,[status(thm)],[c_1600,c_258]) ).
cnf(c_2336,plain,
para(sK1,sK2,sK2,sK1),
inference(resolve,[status(thm)],[c_1657,c_292]) ).
cnf(c_2352,plain,
para(sK1,sK4,sK4,sK1),
inference(resolve,[status(thm)],[c_2156,c_292]) ).
cnf(c_2379,plain,
eqangle(sK4,sK3,A,B,sK4,sK3,A,B),
inference(resolve,[status(thm)],[c_2233,c_258]) ).
cnf(c_2412,plain,
para(sK1,sK2,sK1,sK2),
inference(resolve,[status(thm)],[c_2336,c_293]) ).
cnf(c_2428,plain,
para(sK1,sK4,sK1,sK4),
inference(resolve,[status(thm)],[c_2352,c_293]) ).
cnf(c_2443,plain,
eqangle(sK1,sK2,A,B,sK1,sK2,A,B),
inference(resolve,[status(thm)],[c_2412,c_258]) ).
cnf(c_2455,plain,
eqangle(sK1,sK4,A,B,sK1,sK4,A,B),
inference(resolve,[status(thm)],[c_2428,c_258]) ).
cnf(c_2617,plain,
coll(sK1,sK2,sK4),
inference(resolve,[status(thm)],[c_1031,c_2067]) ).
cnf(c_2619,negated_conjecture,
perp(sK2,sK3,sK3,sK4),
inference(resolve,[status(thm)],[c_2617,c_144]) ).
cnf(c_2708,plain,
para(sK2,sK3,sK2,sK8),
inference(resolve,[status(thm)],[c_2619,c_456]) ).
cnf(c_2759,plain,
eqangle(sK2,sK3,A,B,sK2,sK8,A,B),
inference(resolve,[status(thm)],[c_2708,c_258]) ).
cnf(c_4256,plain,
eqangle(A,B,sK2,sK3,A,B,sK2,sK3),
inference(resolve,[status(thm)],[c_1181,c_279]) ).
cnf(c_4258,plain,
( cyclic(sK3,A,sK2,sK2)
| ~ coll(sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_1181,c_255]) ).
cnf(c_4310,plain,
( cyclic(sK4,A,sK3,sK3)
| ~ coll(sK3,sK3,A) ),
inference(resolve,[status(thm)],[c_1559,c_255]) ).
cnf(c_4398,plain,
( cyclic(sK1,A,sK2,sK2)
| ~ coll(sK2,sK2,A) ),
inference(resolve,[status(thm)],[c_1658,c_255]) ).
cnf(c_4399,plain,
( cong(sK1,A,sK1,A)
| ~ cyclic(sK1,A,sK2,sK2)
| ~ cyclic(sK1,A,sK2,A)
| ~ cyclic(sK1,A,sK2,sK1) ),
inference(resolve,[status(thm)],[c_1658,c_254]) ).
cnf(c_4426,plain,
( cyclic(sK2,A,sK3,sK3)
| ~ coll(sK3,sK3,A) ),
inference(resolve,[status(thm)],[c_2169,c_255]) ).
cnf(c_4434,plain,
( ~ cong(sK3,sK3,sK3,A)
| ~ cong(sK3,sK3,sK3,sK2)
| midp(A,sK2,A)
| ~ coll(A,sK2,A) ),
inference(resolve,[status(thm)],[c_2169,c_188]) ).
cnf(c_18118,plain,
( ~ cong(sK8,sK8,sK8,sK3)
| midp(sK3,sK3,sK3)
| ~ coll(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_2260,c_312]) ).
cnf(c_4483,plain,
( ~ cong(sK8,sK8,sK8,sK3)
| midp(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_1202,c_18118]) ).
cnf(c_4486,plain,
( cyclic(sK3,A,sK8,sK8)
| ~ coll(sK8,sK8,A) ),
inference(resolve,[status(thm)],[c_2260,c_255]) ).
cnf(c_4556,plain,
( cyclic(sK3,A,sK4,sK4)
| ~ coll(sK4,sK4,A) ),
inference(resolve,[status(thm)],[c_2379,c_255]) ).
cnf(c_4557,plain,
( cong(sK3,A,sK3,A)
| ~ cyclic(sK3,A,sK4,sK4)
| ~ cyclic(sK3,A,sK4,A)
| ~ cyclic(sK3,A,sK4,sK3) ),
inference(resolve,[status(thm)],[c_2379,c_254]) ).
cnf(c_4598,plain,
( cyclic(sK2,A,sK1,sK1)
| ~ coll(sK1,sK1,A) ),
inference(resolve,[status(thm)],[c_2443,c_255]) ).
cnf(c_4599,plain,
( cong(sK2,A,sK2,A)
| ~ cyclic(sK2,A,sK1,sK1)
| ~ cyclic(sK2,A,sK1,A)
| ~ cyclic(sK2,A,sK1,sK2) ),
inference(resolve,[status(thm)],[c_2443,c_254]) ).
cnf(c_4612,plain,
( cyclic(sK4,A,sK1,sK1)
| ~ coll(sK1,sK1,A) ),
inference(resolve,[status(thm)],[c_2455,c_255]) ).
cnf(c_4626,plain,
( cong(sK3,sK8,sK8,sK8)
| ~ cyclic(sK3,sK8,sK2,sK2)
| ~ cyclic(sK3,sK8,sK2,sK8) ),
inference(resolve,[status(thm)],[c_2759,c_342]) ).
cnf(c_4812,plain,
para(A,B,A,B),
inference(resolve,[status(thm)],[c_4256,c_259]) ).
cnf(c_4820,plain,
( ~ cong(sK2,sK2,sK2,sK3)
| ~ cong(sK2,sK2,sK2,A)
| midp(sK3,A,sK3)
| ~ coll(sK3,A,sK3) ),
inference(resolve,[status(thm)],[c_4256,c_188]) ).
cnf(c_4828,plain,
( midp(A,C,C)
| ~ midp(A,B,B) ),
inference(resolve,[status(thm)],[c_4812,c_336]) ).
cnf(c_4836,plain,
( midp(C,B,C)
| ~ coll(C,B,C)
| ~ midp(A,B,A) ),
inference(resolve,[status(thm)],[c_4812,c_252]) ).
cnf(c_4838,plain,
coll(A,B,B),
inference(resolve,[status(thm)],[c_4812,c_236]) ).
cnf(c_4917,plain,
coll(A,A,B),
inference(resolve,[status(thm)],[c_4838,c_350]) ).
cnf(c_4918,plain,
coll(A,B,A),
inference(resolve,[status(thm)],[c_4838,c_295]) ).
cnf(c_4925,plain,
cyclic(sK4,A,sK1,sK1),
inference(resolve,[status(thm)],[c_4917,c_4612]) ).
cnf(c_4926,plain,
cyclic(sK2,A,sK1,sK1),
inference(resolve,[status(thm)],[c_4917,c_4598]) ).
cnf(c_4927,plain,
cyclic(sK3,A,sK4,sK4),
inference(resolve,[status(thm)],[c_4917,c_4556]) ).
cnf(c_4930,plain,
cyclic(sK3,A,sK8,sK8),
inference(resolve,[status(thm)],[c_4917,c_4486]) ).
cnf(c_4932,plain,
cyclic(sK2,A,sK3,sK3),
inference(resolve,[status(thm)],[c_4917,c_4426]) ).
cnf(c_4934,plain,
cyclic(sK1,A,sK2,sK2),
inference(resolve,[status(thm)],[c_4917,c_4398]) ).
cnf(c_4938,plain,
cyclic(sK4,A,sK3,sK3),
inference(resolve,[status(thm)],[c_4917,c_4310]) ).
cnf(c_4940,plain,
cyclic(sK3,A,sK2,sK2),
inference(resolve,[status(thm)],[c_4917,c_4258]) ).
cnf(c_5042,plain,
( midp(C,B,C)
| ~ midp(A,B,A) ),
inference(resolve,[status(thm)],[c_4918,c_4836]) ).
cnf(c_5043,plain,
( ~ cong(sK2,sK2,sK2,sK3)
| ~ cong(sK2,sK2,sK2,A)
| midp(sK3,A,sK3) ),
inference(resolve,[status(thm)],[c_4918,c_4820]) ).
cnf(c_5051,plain,
( ~ cong(sK3,sK3,sK3,A)
| ~ cong(sK3,sK3,sK3,sK2)
| midp(A,sK2,A) ),
inference(resolve,[status(thm)],[c_4918,c_4434]) ).
cnf(c_5087,plain,
( cong(sK2,A,sK2,A)
| ~ cyclic(sK2,A,sK1,A)
| ~ cyclic(sK2,A,sK1,sK2) ),
inference(resolve,[status(thm)],[c_4926,c_4599]) ).
cnf(c_5093,plain,
( cong(sK3,A,sK3,A)
| ~ cyclic(sK3,A,sK4,A)
| ~ cyclic(sK3,A,sK4,sK3) ),
inference(resolve,[status(thm)],[c_4927,c_4557]) ).
cnf(c_5114,plain,
( cong(sK1,A,sK1,A)
| ~ cyclic(sK1,A,sK2,A)
| ~ cyclic(sK1,A,sK2,sK1) ),
inference(resolve,[status(thm)],[c_4934,c_4399]) ).
cnf(c_5138,plain,
( cong(sK3,sK8,sK8,sK8)
| ~ cyclic(sK3,sK8,sK2,sK8) ),
inference(resolve,[status(thm)],[c_4940,c_4626]) ).
cnf(c_18119,plain,
( coll(B,C,A)
| ~ coll(A,A,B) ),
inference(resolve,[status(thm)],[c_4917,c_294]) ).
cnf(c_5280,plain,
coll(A,B,C),
inference(resolve,[status(thm)],[c_4917,c_18119]) ).
cnf(c_5290,plain,
( midp(D,B,E)
| ~ para(A,D,C,E)
| ~ midp(A,B,C) ),
inference(resolve,[status(thm)],[c_5280,c_252]) ).
cnf(c_5348,plain,
cyclic(sK4,sK1,A,sK1),
inference(resolve,[status(thm)],[c_4925,c_283]) ).
cnf(c_5364,plain,
cyclic(sK2,sK1,A,sK1),
inference(resolve,[status(thm)],[c_4926,c_283]) ).
cnf(c_5381,plain,
cyclic(sK3,sK4,A,sK4),
inference(resolve,[status(thm)],[c_4927,c_283]) ).
cnf(c_5430,plain,
cyclic(sK3,sK8,A,sK8),
inference(resolve,[status(thm)],[c_4930,c_283]) ).
cnf(c_5445,plain,
cong(sK3,sK8,sK8,sK8),
inference(resolve,[status(thm)],[c_5430,c_5138]) ).
cnf(c_5464,plain,
cyclic(sK2,sK3,A,sK3),
inference(resolve,[status(thm)],[c_4932,c_283]) ).
cnf(c_5498,plain,
cyclic(sK1,sK2,A,sK2),
inference(resolve,[status(thm)],[c_4934,c_283]) ).
cnf(c_5563,plain,
cyclic(sK4,sK3,A,sK3),
inference(resolve,[status(thm)],[c_4938,c_283]) ).
cnf(c_5737,plain,
cyclic(sK4,sK1,sK1,A),
inference(resolve,[status(thm)],[c_5348,c_284]) ).
cnf(c_5770,plain,
cyclic(sK1,sK2,A,sK1),
inference(resolve,[status(thm)],[c_5364,c_282]) ).
cnf(c_5815,plain,
cyclic(sK3,sK4,sK4,A),
inference(resolve,[status(thm)],[c_5381,c_284]) ).
cnf(c_5816,plain,
cyclic(sK4,sK3,A,sK4),
inference(resolve,[status(thm)],[c_5381,c_282]) ).
cnf(c_5959,plain,
cong(sK8,sK8,sK3,sK8),
inference(resolve,[status(thm)],[c_5445,c_274]) ).
cnf(c_6010,plain,
cyclic(sK2,sK3,sK3,A),
inference(resolve,[status(thm)],[c_5464,c_284]) ).
cnf(c_6134,plain,
cyclic(sK1,sK2,sK2,A),
inference(resolve,[status(thm)],[c_5498,c_284]) ).
cnf(c_6135,plain,
cyclic(sK2,sK1,A,sK2),
inference(resolve,[status(thm)],[c_5498,c_282]) ).
cnf(c_6259,plain,
cyclic(sK3,sK4,A,sK3),
inference(resolve,[status(thm)],[c_5563,c_282]) ).
cnf(c_6483,plain,
cyclic(sK1,sK1,A,A),
inference(resolve,[status(thm)],[c_5737,c_345]) ).
cnf(c_18120,plain,
( cyclic(sK1,sK1,A,B)
| ~ cyclic(sK4,sK1,sK1,A) ),
inference(resolve,[status(thm)],[c_5737,c_281]) ).
cnf(c_6485,plain,
cyclic(sK1,sK1,A,B),
inference(resolve,[status(thm)],[c_5737,c_18120]) ).
cnf(c_6700,plain,
cyclic(sK1,A,sK2,sK1),
inference(resolve,[status(thm)],[c_5770,c_283]) ).
cnf(c_6702,plain,
( cyclic(sK2,A,sK1,B)
| ~ cyclic(sK1,sK2,A,B) ),
inference(resolve,[status(thm)],[c_5770,c_281]) ).
cnf(c_6716,plain,
( cong(sK1,A,sK1,A)
| ~ cyclic(sK1,A,sK2,A) ),
inference(resolve,[status(thm)],[c_6700,c_5114]) ).
cnf(c_18121,plain,
( cyclic(sK4,sK4,A,B)
| ~ cyclic(sK3,sK4,sK4,A) ),
inference(resolve,[status(thm)],[c_5815,c_281]) ).
cnf(c_6853,plain,
cyclic(sK4,sK4,A,B),
inference(resolve,[status(thm)],[c_5815,c_18121]) ).
cnf(c_6869,plain,
( cyclic(sK3,A,sK4,B)
| ~ cyclic(sK4,sK3,A,B) ),
inference(resolve,[status(thm)],[c_5816,c_281]) ).
cnf(c_7598,plain,
cong(sK8,sK8,sK8,sK3),
inference(resolve,[status(thm)],[c_5959,c_275]) ).
cnf(c_7604,plain,
midp(sK3,sK3,sK3),
inference(resolve,[status(thm)],[c_7598,c_4483]) ).
cnf(c_7605,plain,
midp(sK3,sK2,sK2),
inference(resolve,[status(thm)],[c_7604,c_2166]) ).
cnf(c_7624,plain,
midp(sK3,sK1,sK1),
inference(resolve,[status(thm)],[c_7605,c_1654]) ).
cnf(c_7985,plain,
cyclic(sK3,sK3,A,A),
inference(resolve,[status(thm)],[c_6010,c_345]) ).
cnf(c_8157,plain,
cyclic(sK2,sK2,A,A),
inference(resolve,[status(thm)],[c_6134,c_345]) ).
cnf(c_8173,plain,
cyclic(sK2,A,sK1,sK2),
inference(resolve,[status(thm)],[c_6135,c_283]) ).
cnf(c_8189,plain,
( cong(sK2,A,sK2,A)
| ~ cyclic(sK2,A,sK1,A) ),
inference(resolve,[status(thm)],[c_8173,c_5087]) ).
cnf(c_8418,plain,
cyclic(sK3,A,sK4,sK3),
inference(resolve,[status(thm)],[c_6259,c_283]) ).
cnf(c_8434,plain,
( cong(sK3,A,sK3,A)
| ~ cyclic(sK3,A,sK4,A) ),
inference(resolve,[status(thm)],[c_8418,c_5093]) ).
cnf(c_8614,plain,
( perp(A,sK1,sK1,A)
| ~ cong(sK1,A,sK1,A) ),
inference(resolve,[status(thm)],[c_6483,c_339]) ).
cnf(c_18122,plain,
( cyclic(sK1,A,B,A)
| ~ cyclic(sK1,sK1,A,B) ),
inference(resolve,[status(thm)],[c_6483,c_281]) ).
cnf(c_8615,plain,
cyclic(sK1,A,B,A),
inference(resolve,[status(thm)],[c_6485,c_18122]) ).
cnf(c_8628,plain,
cong(sK1,A,sK1,A),
inference(resolve,[status(thm)],[c_8615,c_6716]) ).
cnf(c_8629,plain,
perp(A,sK1,sK1,A),
inference(resolve,[status(thm)],[c_8628,c_8614]) ).
cnf(c_18123,plain,
( cyclic(sK1,A,B,C)
| ~ cyclic(sK1,sK1,A,B) ),
inference(resolve,[status(thm)],[c_6485,c_281]) ).
cnf(c_8677,plain,
cyclic(sK1,A,B,C),
inference(resolve,[status(thm)],[c_6485,c_18123]) ).
cnf(c_8689,plain,
cyclic(sK2,A,sK1,B),
inference(resolve,[status(thm)],[c_8677,c_6702]) ).
cnf(c_8745,plain,
cong(sK2,A,sK2,A),
inference(resolve,[status(thm)],[c_8689,c_8189]) ).
cnf(c_18124,plain,
( cyclic(sK4,A,B,C)
| ~ cyclic(sK4,sK4,A,B) ),
inference(resolve,[status(thm)],[c_6853,c_281]) ).
cnf(c_9003,plain,
cyclic(sK4,A,B,C),
inference(resolve,[status(thm)],[c_6853,c_18124]) ).
cnf(c_9019,plain,
cyclic(sK3,A,sK4,B),
inference(resolve,[status(thm)],[c_9003,c_6869]) ).
cnf(c_9118,plain,
cong(sK3,A,sK3,A),
inference(resolve,[status(thm)],[c_9019,c_8434]) ).
cnf(c_18125,plain,
( perp(A,sK3,sK3,A)
| ~ cong(sK3,A,sK3,A) ),
inference(resolve,[status(thm)],[c_7985,c_339]) ).
cnf(c_9906,plain,
perp(A,sK3,sK3,A),
inference(resolve,[status(thm)],[c_9118,c_18125]) ).
cnf(c_18126,plain,
( perp(A,sK2,sK2,A)
| ~ cong(sK2,A,sK2,A) ),
inference(resolve,[status(thm)],[c_8157,c_339]) ).
cnf(c_10205,plain,
perp(A,sK2,sK2,A),
inference(resolve,[status(thm)],[c_8745,c_18126]) ).
cnf(c_18127,plain,
( perp(sK1,sK1,A,B)
| ~ cong(sK1,A,sK1,A) ),
inference(resolve,[status(thm)],[c_8628,c_246]) ).
cnf(c_10836,plain,
perp(sK1,sK1,A,B),
inference(resolve,[status(thm)],[c_8628,c_18127]) ).
cnf(c_11006,plain,
( cong(B,A,sK1,A)
| ~ midp(A,B,B) ),
inference(resolve,[status(thm)],[c_8629,c_249]) ).
cnf(c_12891,plain,
perp(sK3,A,A,sK3),
inference(resolve,[status(thm)],[c_9906,c_289]) ).
cnf(c_13066,plain,
perp(sK2,A,A,sK2),
inference(resolve,[status(thm)],[c_10205,c_289]) ).
cnf(c_13232,plain,
perp(A,B,sK1,sK1),
inference(resolve,[status(thm)],[c_10836,c_289]) ).
cnf(c_18128,plain,
( para(A,B,C,D)
| ~ perp(A,B,sK1,sK1) ),
inference(resolve,[status(thm)],[c_10836,c_288]) ).
cnf(c_13233,plain,
para(A,B,C,D),
inference(resolve,[status(thm)],[c_13232,c_18128]) ).
cnf(c_13246,plain,
( midp(D,B,E)
| ~ midp(A,B,C) ),
inference(resolve,[status(thm)],[c_13233,c_5290]) ).
cnf(c_13883,plain,
perp(sK3,A,sK3,A),
inference(resolve,[status(thm)],[c_12891,c_290]) ).
cnf(c_13922,plain,
perp(sK2,A,sK2,A),
inference(resolve,[status(thm)],[c_13066,c_290]) ).
cnf(c_14184,plain,
( cong(sK3,sK3,sK3,A)
| ~ midp(A,sK3,A) ),
inference(resolve,[status(thm)],[c_13883,c_247]) ).
cnf(c_14195,plain,
( cong(sK2,sK2,sK2,A)
| ~ midp(A,sK2,A) ),
inference(resolve,[status(thm)],[c_13922,c_247]) ).
cnf(c_14230,plain,
midp(sK3,A,A),
inference(resolve,[status(thm)],[c_4828,c_7624]) ).
cnf(c_14239,plain,
midp(A,sK3,A),
inference(resolve,[status(thm)],[c_5042,c_14230]) ).
cnf(c_14241,plain,
cong(sK3,sK3,sK3,A),
inference(resolve,[status(thm)],[c_14239,c_14184]) ).
cnf(c_18129,plain,
( ~ cong(sK3,sK3,sK3,A)
| midp(A,sK2,A) ),
inference(resolve,[status(thm)],[c_14241,c_5051]) ).
cnf(c_14273,plain,
midp(A,sK2,A),
inference(resolve,[status(thm)],[c_14241,c_18129]) ).
cnf(c_14306,plain,
cong(sK2,sK2,sK2,A),
inference(resolve,[status(thm)],[c_14273,c_14195]) ).
cnf(c_18130,plain,
( ~ cong(sK2,sK2,sK2,sK3)
| midp(sK3,A,sK3) ),
inference(resolve,[status(thm)],[c_14306,c_5043]) ).
cnf(c_14340,plain,
midp(sK3,A,sK3),
inference(resolve,[status(thm)],[c_14306,c_18130]) ).
cnf(c_14493,plain,
midp(A,B,A),
inference(resolve,[status(thm)],[c_14340,c_5042]) ).
cnf(c_14988,plain,
midp(A,B,B),
inference(resolve,[status(thm)],[c_14493,c_4828]) ).
cnf(c_14993,plain,
midp(A,A,B),
inference(resolve,[status(thm)],[c_14493,c_286]) ).
cnf(c_15060,plain,
cong(A,B,sK1,B),
inference(resolve,[status(thm)],[c_14988,c_11006]) ).
cnf(c_18131,plain,
( perp(A,sK1,B,C)
| ~ cong(A,B,sK1,B) ),
inference(resolve,[status(thm)],[c_15060,c_246]) ).
cnf(c_17127,plain,
perp(A,sK1,B,C),
inference(resolve,[status(thm)],[c_15060,c_18131]) ).
cnf(c_17762,plain,
( cong(C,A,C,B)
| ~ midp(sK1,A,B) ),
inference(resolve,[status(thm)],[c_17127,c_247]) ).
cnf(c_17953,plain,
midp(A,B,C),
inference(resolve,[status(thm)],[c_13246,c_14993]) ).
cnf(c_18116,plain,
cong(A,B,A,C),
inference(resolve,[status(thm)],[c_17953,c_17762]) ).
cnf(c_18117,plain,
$false,
inference(resolve,[status(thm)],[c_18116,c_192]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO575+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.18/0.44 % Computer : n010.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Fri Sep 25 13:42:59 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 893141 was started by sandbox on n010,
% 0.18/0.45 % Fri Sep 25 13:42:59 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.49
% 0.18/0.49 % From the command line: assign(max_seconds, 300).
% 40.49/5.68
% 40.49/5.68 % given #500 (W,wt=13): 574 -coll(c1,c7,A) | coll(c1,A,c1). [resolve(527,a,294,a)].
% 40.49/5.68
% 40.49/5.68 % given #1000 (T,wt=13): 1103 -coll(c6,c7,A) | coll(c3,A,c6). [resolve(1053,a,294,a)].
% 40.49/5.68
% 40.49/5.68 % given #1500 (W,wt=13): 2516 -coll(c1,c4,A) | coll(c6,A,c1). [resolve(2500,a,294,a)].
% 40.49/5.68
% 40.49/5.68 % given #2000 (T,wt=10): 5595 cyclic(c2,c1,A,c1). [resolve(4940,a,283,a)].
% 40.49/5.68
% 40.49/5.68 % given #2500 (W,wt=10): 9148 perp(c2,c5,A,c1). [back_unit_del(8527),unit_del(a,9119)].
% 40.49/5.68
% 40.49/5.68 % given #3000 (T,wt=10): 14994 cong(A,B,A,A). [resolve(14493,a,234,a)].
% 40.49/5.68
% 40.49/5.68 % SZS status Theorem for theBenchmark
% 40.49/5.68
% 40.49/5.68 % Proof 1 at 3.62 (+ 1.08) seconds.
% 40.49/5.68 % Length of proof is 266.
% 40.49/5.68 % Level of proof is 39.
% 40.49/5.68 % Maximum clause weight is 34.000.
% 40.49/5.68 % Given clauses 3314.
% 40.49/5.68
% 40.49/5.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------