%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO563+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 : n020.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:07 AM UTC 2026
% Result : Theorem 24.50s 4.05s
% Output : CNFRefutation 24.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 20
% Syntax : Number of formulae : 108 ( 48 unt; 0 def)
% Number of atoms : 213 ( 0 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 158 ( 53 ~; 49 |; 35 &)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-8 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-4 aty)
% Number of variables : 352 ( 55 sgn 130 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(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(ruleD21,axiom,
! [A,B,C,D,P,Q,U,V] :
( eqangle(A,B,C,D,P,Q,U,V)
=> eqangle(A,B,P,Q,C,D,U,V) ),
file('theBenchmark.p',ruleD21) ).
fof(ruleD22,axiom,
! [A,B,C,D,P,Q,U,V,E,F,G,H] :
( ( eqangle(P,Q,U,V,E,F,G,H)
& eqangle(A,B,C,D,P,Q,U,V) )
=> eqangle(A,B,C,D,E,F,G,H) ),
file('theBenchmark.p',ruleD22) ).
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(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(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(exemplo6GDDFULL214024,conjecture,
! [Q,R,P,O1,S,Y,O,X,I,NWPNT1,NWPNT2] :
( ( coll(I,Y,X)
& coll(I,R,S)
& circle(O,Q,X,NWPNT2)
& circle(O,Y,P,Q)
& coll(Y,Q,S)
& circle(O1,Q,S,NWPNT1)
& circle(O1,Q,R,P) )
=> eqangle(R,I,I,X,R,P,P,X) ),
file('theBenchmark.p',exemplo6GDDFULL214024) ).
fof(exemplo6GDDFULL214024_neg,negated_conjecture,
~ ! [Q,R,P,O1,S,Y,O,X,I,NWPNT1,NWPNT2] :
( ( coll(I,Y,X)
& coll(I,R,S)
& circle(O,Q,X,NWPNT2)
& circle(O,Y,P,Q)
& coll(Y,Q,S)
& circle(O1,Q,S,NWPNT1)
& circle(O1,Q,R,P) )
=> eqangle(R,I,I,X,R,P,P,X) ),
inference(assume_negation,[status(cth)],[exemplo6GDDFULL214024]) ).
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,
? [Q,R,P,O1,S,Y,O,X,I,NWPNT1,NWPNT2] :
( ~ eqangle(R,I,I,X,R,P,P,X)
& coll(I,Y,X)
& coll(I,R,S)
& circle(O,Q,X,NWPNT2)
& circle(O,Y,P,Q)
& coll(Y,Q,S)
& circle(O1,Q,S,NWPNT1)
& circle(O1,Q,R,P) ),
inference(fof_nnf,[status(thm)],[exemplo6GDDFULL214024_neg]) ).
fof(sk_exemplo6GDDFULL214024_neg,plain,
( ~ eqangle(sK3,sK9,sK9,sK7,sK3,sK4,sK4,sK7)
& coll(sK9,sK6,sK7)
& coll(sK9,sK3,sK10)
& circle(sK5,sK2,sK7,sK8)
& circle(sK5,sK6,sK4,sK2)
& coll(sK6,sK2,sK10)
& circle(sK1,sK2,sK10,sK11)
& circle(sK1,sK2,sK3,sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK10,sK11,sK6,sK5,sK7,sK8,sK9]),skolemize(Q,sK2),skolemize(R,sK3),skolemize(P,sK4),skolemize(O1,sK1),skolemize(S,sK10),skolemize(Y,sK6),skolemize(O,sK5),skolemize(X,sK7),skolemize(I,sK9),skolemize(NWPNT1,sK11),skolemize(NWPNT2,sK8)],[nnf_95]) ).
cnf(c_109,negated_conjecture,
circle(sK1,sK2,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214024_neg]) ).
cnf(c_111,negated_conjecture,
circle(sK5,sK6,sK4,sK2),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214024_neg]) ).
cnf(c_112,negated_conjecture,
circle(sK5,sK2,sK7,sK8),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214024_neg]) ).
cnf(c_118,negated_conjecture,
perp(sK0(sK2,sK7,sK8,sK5),sK2,sK2,sK5),
inference(resolve,[status(thm)],[c_112,c_102]) ).
cnf(c_132,negated_conjecture,
perp(sK0(sK6,sK4,sK2,sK5),sK6,sK6,sK5),
inference(resolve,[status(thm)],[c_111,c_102]) ).
cnf(c_160,negated_conjecture,
perp(sK0(sK2,sK3,sK4,sK1),sK2,sK2,sK1),
inference(resolve,[status(thm)],[c_109,c_102]) ).
cnf(c_207,negated_conjecture,
~ eqangle(sK3,sK9,sK9,sK7,sK3,sK4,sK4,sK7),
inference(split_conjunct,[status(thm)],[sk_exemplo6GDDFULL214024_neg]) ).
cnf(c_249,plain,
( coll(A,B,C)
| ~ para(A,B,A,C) ),
inference(clausify,[status(thm)],[ruleD66]) ).
cnf(c_259,plain,
( perp(A,C,B,D)
| ~ cong(A,D,C,D)
| ~ cong(A,B,C,B) ),
inference(clausify,[status(thm)],[ruleD56]) ).
cnf(c_267,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_268,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_271,plain,
( eqangle(A,B,E,F,C,D,E,F)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD40]) ).
cnf(c_272,plain,
( para(A,B,E,F)
| ~ eqangle(A,B,C,D,E,F,C,D) ),
inference(clausify,[status(thm)],[ruleD39]) ).
cnf(c_289,plain,
( eqangle(A,B,C,D,V8,V9,V10,V11)
| ~ eqangle(E,F,V6,V7,V8,V9,V10,V11)
| ~ eqangle(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[ruleD22]) ).
cnf(c_290,plain,
( eqangle(A,B,E,F,C,D,V6,V7)
| ~ eqangle(A,B,C,D,E,F,V6,V7) ),
inference(clausify,[status(thm)],[ruleD21]) ).
cnf(c_292,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_294,plain,
( cyclic(B,C,D,E)
| ~ cyclic(A,B,C,E)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD17]) ).
cnf(c_295,plain,
( cyclic(B,A,C,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD16]) ).
cnf(c_296,plain,
( cyclic(A,C,B,D)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD15]) ).
cnf(c_297,plain,
( cyclic(A,B,D,C)
| ~ cyclic(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD14]) ).
cnf(c_301,plain,
( para(A,B,E,F)
| ~ perp(C,D,E,F)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD9]) ).
cnf(c_302,plain,
( perp(C,D,A,B)
| ~ perp(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD8]) ).
cnf(c_305,plain,
( para(C,D,A,B)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD5]) ).
cnf(c_306,plain,
( para(A,B,D,C)
| ~ para(A,B,C,D) ),
inference(clausify,[status(thm)],[ruleD4]) ).
cnf(c_307,plain,
( coll(C,D,A)
| ~ coll(A,B,D)
| ~ coll(A,B,C) ),
inference(clausify,[status(thm)],[ruleD3]) ).
cnf(c_358,plain,
( cyclic(B,C,D,D)
| ~ cyclic(A,B,C,D) ),
inference(factor,[status(thm)],[c_294]) ).
cnf(c_363,plain,
( coll(C,C,A)
| ~ coll(A,B,C) ),
inference(factor,[status(thm)],[c_307]) ).
cnf(c_461,plain,
( para(A,B,sK2,sK1)
| ~ perp(A,B,sK0(sK2,sK3,sK4,sK1),sK2) ),
inference(resolve,[status(thm)],[c_301,c_160]) ).
cnf(c_463,plain,
( para(A,B,sK6,sK5)
| ~ perp(A,B,sK0(sK6,sK4,sK2,sK5),sK6) ),
inference(resolve,[status(thm)],[c_301,c_132]) ).
cnf(c_464,plain,
( para(A,B,sK2,sK5)
| ~ perp(A,B,sK0(sK2,sK7,sK8,sK5),sK2) ),
inference(resolve,[status(thm)],[c_301,c_118]) ).
cnf(c_465,plain,
perp(sK2,sK1,sK0(sK2,sK3,sK4,sK1),sK2),
inference(resolve,[status(thm)],[c_302,c_160]) ).
cnf(c_467,plain,
perp(sK6,sK5,sK0(sK6,sK4,sK2,sK5),sK6),
inference(resolve,[status(thm)],[c_302,c_132]) ).
cnf(c_468,plain,
perp(sK2,sK5,sK0(sK2,sK7,sK8,sK5),sK2),
inference(resolve,[status(thm)],[c_302,c_118]) ).
cnf(c_1094,plain,
para(sK2,sK1,sK2,sK1),
inference(resolve,[status(thm)],[c_465,c_461]) ).
cnf(c_1131,plain,
eqangle(sK2,sK1,A,B,sK2,sK1,A,B),
inference(resolve,[status(thm)],[c_1094,c_271]) ).
cnf(c_1173,plain,
para(sK6,sK5,sK6,sK5),
inference(resolve,[status(thm)],[c_467,c_463]) ).
cnf(c_1189,plain,
para(sK2,sK5,sK2,sK5),
inference(resolve,[status(thm)],[c_468,c_464]) ).
cnf(c_1669,plain,
para(sK6,sK5,sK5,sK6),
inference(resolve,[status(thm)],[c_1173,c_306]) ).
cnf(c_1670,plain,
eqangle(sK6,sK5,A,B,sK6,sK5,A,B),
inference(resolve,[status(thm)],[c_1173,c_271]) ).
cnf(c_2105,plain,
para(sK2,sK5,sK5,sK2),
inference(resolve,[status(thm)],[c_1189,c_306]) ).
cnf(c_2135,plain,
para(sK5,sK6,sK6,sK5),
inference(resolve,[status(thm)],[c_1669,c_305]) ).
cnf(c_2176,plain,
para(sK5,sK2,sK2,sK5),
inference(resolve,[status(thm)],[c_2105,c_305]) ).
cnf(c_2204,plain,
para(sK5,sK6,sK5,sK6),
inference(resolve,[status(thm)],[c_2135,c_306]) ).
cnf(c_2248,plain,
para(sK5,sK2,sK5,sK2),
inference(resolve,[status(thm)],[c_2176,c_306]) ).
cnf(c_2263,plain,
eqangle(sK5,sK6,A,B,sK5,sK6,A,B),
inference(resolve,[status(thm)],[c_2204,c_271]) ).
cnf(c_2293,plain,
eqangle(sK5,sK2,A,B,sK5,sK2,A,B),
inference(resolve,[status(thm)],[c_2248,c_271]) ).
cnf(c_2911,plain,
eqangle(A,B,sK2,sK1,A,B,sK2,sK1),
inference(resolve,[status(thm)],[c_1131,c_292]) ).
cnf(c_4373,plain,
( cyclic(sK5,A,sK6,sK6)
| ~ coll(sK6,sK6,A) ),
inference(resolve,[status(thm)],[c_1670,c_268]) ).
cnf(c_4374,plain,
( cong(sK5,A,sK5,A)
| ~ cyclic(sK5,A,sK6,sK6)
| ~ cyclic(sK5,A,sK6,A)
| ~ cyclic(sK5,A,sK6,sK5) ),
inference(resolve,[status(thm)],[c_1670,c_267]) ).
cnf(c_4490,plain,
( cyclic(sK6,A,sK5,sK5)
| ~ coll(sK5,sK5,A) ),
inference(resolve,[status(thm)],[c_2263,c_268]) ).
cnf(c_4514,plain,
( cyclic(sK2,A,sK5,sK5)
| ~ coll(sK5,sK5,A) ),
inference(resolve,[status(thm)],[c_2293,c_268]) ).
cnf(c_4556,plain,
para(A,B,A,B),
inference(resolve,[status(thm)],[c_2911,c_272]) ).
cnf(c_4581,plain,
coll(A,B,B),
inference(resolve,[status(thm)],[c_4556,c_249]) ).
cnf(c_4647,plain,
coll(A,A,B),
inference(resolve,[status(thm)],[c_4581,c_363]) ).
cnf(c_4655,plain,
cyclic(sK2,A,sK5,sK5),
inference(resolve,[status(thm)],[c_4647,c_4514]) ).
cnf(c_4656,plain,
cyclic(sK6,A,sK5,sK5),
inference(resolve,[status(thm)],[c_4647,c_4490]) ).
cnf(c_4659,plain,
cyclic(sK5,A,sK6,sK6),
inference(resolve,[status(thm)],[c_4647,c_4373]) ).
cnf(c_4810,plain,
( cong(sK5,A,sK5,A)
| ~ cyclic(sK5,A,sK6,A)
| ~ cyclic(sK5,A,sK6,sK5) ),
inference(resolve,[status(thm)],[c_4659,c_4374]) ).
cnf(c_5083,plain,
cyclic(sK2,sK5,A,sK5),
inference(resolve,[status(thm)],[c_4655,c_296]) ).
cnf(c_5099,plain,
cyclic(sK6,sK5,A,sK5),
inference(resolve,[status(thm)],[c_4656,c_296]) ).
cnf(c_5326,plain,
cyclic(sK2,sK5,sK5,A),
inference(resolve,[status(thm)],[c_5083,c_297]) ).
cnf(c_5359,plain,
cyclic(sK5,sK6,A,sK5),
inference(resolve,[status(thm)],[c_5099,c_295]) ).
cnf(c_5791,plain,
cyclic(sK5,sK5,A,A),
inference(resolve,[status(thm)],[c_5326,c_358]) ).
cnf(c_11728,plain,
( cyclic(sK5,sK5,A,B)
| ~ cyclic(sK2,sK5,sK5,A) ),
inference(resolve,[status(thm)],[c_5326,c_294]) ).
cnf(c_5793,plain,
cyclic(sK5,sK5,A,B),
inference(resolve,[status(thm)],[c_5326,c_11728]) ).
cnf(c_6002,plain,
cyclic(sK5,A,sK6,sK5),
inference(resolve,[status(thm)],[c_5359,c_296]) ).
cnf(c_6018,plain,
( cong(sK5,A,sK5,A)
| ~ cyclic(sK5,A,sK6,A) ),
inference(resolve,[status(thm)],[c_6002,c_4810]) ).
cnf(c_11729,plain,
( cyclic(sK5,A,B,A)
| ~ cyclic(sK5,sK5,A,B) ),
inference(resolve,[status(thm)],[c_5791,c_294]) ).
cnf(c_6536,plain,
cyclic(sK5,A,B,A),
inference(resolve,[status(thm)],[c_5793,c_11729]) ).
cnf(c_6549,plain,
cong(sK5,A,sK5,A),
inference(resolve,[status(thm)],[c_6536,c_6018]) ).
cnf(c_11730,plain,
( perp(sK5,sK5,A,B)
| ~ cong(sK5,A,sK5,A) ),
inference(resolve,[status(thm)],[c_6549,c_259]) ).
cnf(c_7550,plain,
perp(sK5,sK5,A,B),
inference(resolve,[status(thm)],[c_6549,c_11730]) ).
cnf(c_8637,plain,
perp(A,B,sK5,sK5),
inference(resolve,[status(thm)],[c_7550,c_302]) ).
cnf(c_11731,plain,
( para(A,B,C,D)
| ~ perp(A,B,sK5,sK5) ),
inference(resolve,[status(thm)],[c_7550,c_301]) ).
cnf(c_8638,plain,
para(A,B,C,D),
inference(resolve,[status(thm)],[c_8637,c_11731]) ).
cnf(c_8654,plain,
eqangle(A,B,C,D,E,F,C,D),
inference(resolve,[status(thm)],[c_8638,c_271]) ).
cnf(c_10794,plain,
eqangle(A,B,C,D,A,B,E,F),
inference(resolve,[status(thm)],[c_8654,c_292]) ).
cnf(c_10795,plain,
eqangle(A,B,C,D,E,F,E,F),
inference(resolve,[status(thm)],[c_8654,c_290]) ).
cnf(c_11637,plain,
eqangle(A,B,A,B,C,D,E,F),
inference(resolve,[status(thm)],[c_10794,c_290]) ).
cnf(c_11732,plain,
( eqangle(V6,V7,V8,V9,C,D,E,F)
| ~ eqangle(A,B,A,B,C,D,E,F) ),
inference(resolve,[status(thm)],[c_10795,c_289]) ).
cnf(c_11726,plain,
eqangle(A,B,C,D,E,F,V6,V7),
inference(resolve,[status(thm)],[c_11637,c_11732]) ).
cnf(c_11727,plain,
$false,
inference(resolve,[status(thm)],[c_11726,c_207]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO563+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.44 % Computer : n020.cluster.edu
% 0.20/0.44 % Model : x86_64 x86_64
% 0.20/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.44 % Memory : 8046.5625MB
% 0.20/0.44 % OS : Linux 6.8.0-71-generic
% 0.20/0.44 % CPULimit : 300
% 0.20/0.44 % WCLimit : 300
% 0.20/0.44 % DateTime : Fri Sep 25 13:42:34 UTC 2026
% 0.20/0.44 % CPUTime :
% 0.20/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.20/0.45 % Process 3048293 was started by sandbox on n020,
% 0.20/0.45 % Fri Sep 25 13:42:34 2026
% 0.20/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.20/0.48
% 0.20/0.48 % From the command line: assign(max_seconds, 300).
% 24.50/4.05
% 24.50/4.05 % given #500 (W,wt=9): 965 coll(c2,c8,c2). [resolve(900,a,309,a)].
% 24.50/4.05
% 24.50/4.05 % given #1000 (T,wt=9): 2461 coll(c7,c1,c2). [resolve(2454,a,309,a)].
% 24.50/4.05
% 24.50/4.05 % given #1500 (W,wt=13): 1601 -coll(c8,c8,A) | coll(c4,A,c8). [resolve(1556,a,307,a)].
% 24.50/4.05
% 24.50/4.05 % given #2000 (T,wt=13): 2745 -coll(c4,c7,A) | coll(c1,A,c4). [resolve(2728,a,307,a)].
% 24.50/4.05
% 24.50/4.05 % given #2500 (W,wt=10): 6686 cong(c6,A,c6,A). [back_unit_del(6355),unit_del(a,6630)].
% 24.50/4.05
% 24.50/4.05 % given #3000 (T,wt=14): 6835 eqangle(c7,A,c7,c7,c6,A,c6,c7). [resolve(6121,a,270,a)].
% 24.50/4.05
% 24.50/4.05 % given #3500 (W,wt=14): 10589 eqangle(A,c1,c1,A,c1,A,c1,c7). [resolve(7635,a,293,a)].
% 24.50/4.05
% 24.50/4.05 % SZS status Theorem for theBenchmark
% 24.50/4.05
% 24.50/4.05 % Proof 1 at 2.61 (+ 0.89) seconds.
% 24.50/4.05 % Length of proof is 98.
% 24.50/4.05 % Level of proof is 23.
% 24.50/4.05 % Maximum clause weight is 34.000.
% 24.50/4.05 % Given clauses 3650.
% 24.50/4.05
% 24.50/4.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------