%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SET675+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 08:36:47 AM UTC 2026
% Result : Theorem 0.09s 0.43s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 12
% Syntax : Number of formulae : 90 ( 26 unt; 0 def)
% Number of atoms : 227 ( 94 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 250 ( 113 ~; 92 |; 11 &)
% ( 1 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-4 aty)
% Number of variables : 141 ( 6 sgn 34 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(p1,axiom,
! [B] :
( ilf_type(B,binary_relation_type)
=> image(B,domain_of(B)) = range_of(B) ),
file('theBenchmark.p',p1) ).
fof(p2,axiom,
! [B] :
( ilf_type(B,binary_relation_type)
=> inverse2(B,range_of(B)) = domain_of(B) ),
file('theBenchmark.p',p2) ).
fof(p3,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ( inverse4(B,C,D,C) = domain(B,C,D)
& image4(B,C,D,B) = range(B,C,D) ) ) ) ),
file('theBenchmark.p',p3) ).
fof(p4,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ! [E] :
( ilf_type(E,relation_type(B,C))
=> ilf_type(E,subset_type(cross_product(B,C))) )
& ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> ilf_type(D,relation_type(B,C)) ) ) ) ),
file('theBenchmark.p',p4) ).
fof(p12,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(B,binary_relation_type)
<=> ( ilf_type(B,set_type)
& relation_like(B) ) ) ),
file('theBenchmark.p',p12) ).
fof(p23,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> relation_like(D) ) ) ),
file('theBenchmark.p',p23) ).
fof(p27,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> domain(B,C,D) = domain_of(D) ) ) ),
file('theBenchmark.p',p27) ).
fof(p29,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> range(B,C,D) = range_of(D) ) ) ),
file('theBenchmark.p',p29) ).
fof(p31,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ! [E] :
( ilf_type(E,set_type)
=> image4(B,C,D,E) = image(D,E) ) ) ) ),
file('theBenchmark.p',p31) ).
fof(p33,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ! [E] :
( ilf_type(E,set_type)
=> inverse4(B,C,D,E) = inverse2(D,E) ) ) ) ),
file('theBenchmark.p',p33) ).
fof(p35,axiom,
! [B] : ilf_type(B,set_type),
file('theBenchmark.p',p35) ).
fof(prove_relset_1_39,conjecture,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(C,B))
=> ( inverse4(C,B,D,image4(C,B,D,C)) = domain(C,B,D)
& image4(C,B,D,inverse4(C,B,D,B)) = range(C,B,D) ) ) ) ),
file('theBenchmark.p',prove_relset_1_39) ).
fof(prove_relset_1_39_neg,negated_conjecture,
~ ! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(C,B))
=> ( inverse4(C,B,D,image4(C,B,D,C)) = domain(C,B,D)
& image4(C,B,D,inverse4(C,B,D,B)) = range(C,B,D) ) ) ) ),
inference(assume_negation,[status(cth)],[prove_relset_1_39]) ).
cnf(c_37,plain,
( ~ relation_like(A)
| ilf_type(A,binary_relation_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p12]) ).
cnf(c_45,plain,
( relation_like(C)
| ~ ilf_type(C,subset_type(cross_product(A,B)))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p23]) ).
cnf(c_51,plain,
( ilf_type(C,binary_relation_type)
| ~ ilf_type(C,set_type)
| ~ ilf_type(C,subset_type(cross_product(A,B)))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_45,c_37]) ).
fof(nnf_36,plain,
? [B] :
( ? [C] :
( ? [D] :
( ( domain(C,B,D) != inverse4(C,B,D,image4(C,B,D,C))
| range(C,B,D) != image4(C,B,D,inverse4(C,B,D,B)) )
& ilf_type(D,relation_type(C,B)) )
& ilf_type(C,set_type) )
& ilf_type(B,set_type) ),
inference(fof_nnf,[status(thm)],[prove_relset_1_39_neg]) ).
fof(sk_prove_relset_1_39_neg,plain,
( ( domain(sK0,sK1,sK2) != inverse4(sK0,sK1,sK2,image4(sK0,sK1,sK2,sK0))
| range(sK0,sK1,sK2) != image4(sK0,sK1,sK2,inverse4(sK0,sK1,sK2,sK1)) )
& ilf_type(sK2,relation_type(sK0,sK1))
& ilf_type(sK0,set_type)
& ilf_type(sK1,set_type) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK2]),skolemize(B,sK1),skolemize(C,sK0),skolemize(D,sK2)],[nnf_36]) ).
cnf(c_63,negated_conjecture,
( domain(sK0,sK1,sK2) != inverse4(sK0,sK1,sK2,image4(sK0,sK1,sK2,sK0))
| range(sK0,sK1,sK2) != image4(sK0,sK1,sK2,inverse4(sK0,sK1,sK2,sK1)) ),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_39_neg]) ).
cnf(c_274,negated_conjecture,
( domain(sK0,sK1,sK2) != inverse4(sK0,sK1,sK2,image4(sK0,sK1,sK2,sK0))
| image4(sK0,sK1,sK2,inverse4(sK0,sK1,sK2,sK1)) != range(sK0,sK1,sK2) ),
inference(copy,[status(thm)],[c_63]) ).
cnf(c_64,negated_conjecture,
( inverse4(sK0,sK1,sK2,image4(sK0,sK1,sK2,sK0)) != domain(sK0,sK1,sK2)
| image4(sK0,sK1,sK2,inverse4(sK0,sK1,sK2,sK1)) != range(sK0,sK1,sK2) ),
inference(copy,[status(thm)],[c_274]) ).
cnf(c_65,negated_conjecture,
ilf_type(sK2,relation_type(sK0,sK1)),
inference(split_conjunct,[status(thm)],[sk_prove_relset_1_39_neg]) ).
cnf(c_68,plain,
ilf_type(A,set_type),
inference(clausify,[status(thm)],[p35]) ).
cnf(c_71,plain,
( inverse4(A,B,C,D) = inverse2(C,D)
| ~ ilf_type(D,set_type)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p33]) ).
cnf(c_275,plain,
( inverse4(C,A,B,D) = inverse2(B,D)
| ~ ilf_type(D,set_type)
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_68,c_71]) ).
cnf(c_276,plain,
( inverse4(B,C,A,D) = inverse2(A,D)
| ~ ilf_type(D,set_type)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_275]) ).
cnf(c_72,plain,
( inverse4(B,C,A,D) = inverse2(A,D)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_276]) ).
cnf(c_75,plain,
( image4(A,B,C,D) = image(C,D)
| ~ ilf_type(D,set_type)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p31]) ).
cnf(c_277,plain,
( image4(C,A,B,D) = image(B,D)
| ~ ilf_type(D,set_type)
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_68,c_75]) ).
cnf(c_278,plain,
( image4(B,C,A,D) = image(A,D)
| ~ ilf_type(D,set_type)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_277]) ).
cnf(c_76,plain,
( image4(B,C,A,D) = image(A,D)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_278]) ).
cnf(c_79,plain,
( range(A,B,C) = range_of(C)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p29]) ).
cnf(c_279,plain,
( range(C,A,B) = range_of(B)
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_68,c_79]) ).
cnf(c_80,plain,
( range(B,C,A) = range_of(A)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_279]) ).
cnf(c_83,plain,
( domain(A,B,C) = domain_of(C)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p27]) ).
cnf(c_280,plain,
( domain(C,A,B) = domain_of(B)
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_68,c_83]) ).
cnf(c_84,plain,
( domain(B,C,A) = domain_of(A)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_280]) ).
cnf(c_134,plain,
( ilf_type(C,subset_type(cross_product(A,B)))
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p4]) ).
cnf(c_281,plain,
( ilf_type(B,subset_type(cross_product(C,A)))
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_68,c_134]) ).
cnf(c_135,plain,
( ilf_type(A,subset_type(cross_product(B,C)))
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_281]) ).
cnf(c_138,plain,
( domain(A,B,C) = inverse4(A,B,C,B)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p3]) ).
cnf(c_282,plain,
( inverse4(A,B,C,B) = domain(A,B,C)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(copy,[status(thm)],[c_138]) ).
cnf(c_283,plain,
( inverse4(C,A,B,A) = domain(C,A,B)
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_68,c_282]) ).
cnf(c_139,plain,
( inverse4(B,C,A,C) = domain(B,C,A)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_283]) ).
cnf(c_140,plain,
( range(A,B,C) = image4(A,B,C,A)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(clausify,[status(thm)],[p3]) ).
cnf(c_284,plain,
( image4(A,B,C,A) = range(A,B,C)
| ~ ilf_type(C,relation_type(A,B))
| ~ ilf_type(B,set_type)
| ~ ilf_type(A,set_type) ),
inference(copy,[status(thm)],[c_140]) ).
cnf(c_285,plain,
( image4(C,A,B,C) = range(C,A,B)
| ~ ilf_type(B,relation_type(C,A))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_68,c_284]) ).
cnf(c_141,plain,
( image4(B,C,A,B) = range(B,C,A)
| ~ ilf_type(A,relation_type(B,C)) ),
inference(resolve,[status(thm)],[c_68,c_285]) ).
cnf(c_142,plain,
( inverse2(A,range_of(A)) = domain_of(A)
| ~ ilf_type(A,binary_relation_type) ),
inference(clausify,[status(thm)],[p2]) ).
cnf(c_143,plain,
( range_of(A) = image(A,domain_of(A))
| ~ ilf_type(A,binary_relation_type) ),
inference(clausify,[status(thm)],[p1]) ).
cnf(c_286,plain,
( ilf_type(B,binary_relation_type)
| ~ ilf_type(B,set_type)
| ~ ilf_type(B,subset_type(cross_product(C,A)))
| ~ ilf_type(A,set_type) ),
inference(resolve,[status(thm)],[c_68,c_51]) ).
cnf(c_287,plain,
( ilf_type(A,binary_relation_type)
| ~ ilf_type(A,set_type)
| ~ ilf_type(A,subset_type(cross_product(B,C))) ),
inference(resolve,[status(thm)],[c_68,c_286]) ).
cnf(c_170,plain,
( ilf_type(A,binary_relation_type)
| ~ ilf_type(A,subset_type(cross_product(B,C))) ),
inference(resolve,[status(thm)],[c_68,c_287]) ).
cnf(c_174,plain,
inverse4(sK0,sK1,sK2,A) = inverse2(sK2,A),
inference(resolve,[status(thm)],[c_72,c_65]) ).
cnf(c_288,negated_conjecture,
( inverse4(sK0,sK1,sK2,image4(sK0,sK1,sK2,sK0)) != domain(sK0,sK1,sK2)
| image4(sK0,sK1,sK2,inverse2(sK2,sK1)) != range(sK0,sK1,sK2) ),
inference(paramod,[status(thm)],[c_174,c_64]) ).
cnf(c_176,negated_conjecture,
( inverse2(sK2,image4(sK0,sK1,sK2,sK0)) != domain(sK0,sK1,sK2)
| image4(sK0,sK1,sK2,inverse2(sK2,sK1)) != range(sK0,sK1,sK2) ),
inference(paramod,[status(thm)],[c_174,c_288]) ).
cnf(c_178,plain,
image4(sK0,sK1,sK2,A) = image(sK2,A),
inference(resolve,[status(thm)],[c_76,c_65]) ).
cnf(c_289,negated_conjecture,
( inverse2(sK2,image4(sK0,sK1,sK2,sK0)) != domain(sK0,sK1,sK2)
| image(sK2,inverse2(sK2,sK1)) != range(sK0,sK1,sK2) ),
inference(paramod,[status(thm)],[c_178,c_176]) ).
cnf(c_290,negated_conjecture,
( inverse2(sK2,image(sK2,sK0)) != domain(sK0,sK1,sK2)
| image(sK2,inverse2(sK2,sK1)) != range(sK0,sK1,sK2) ),
inference(paramod,[status(thm)],[c_178,c_289]) ).
cnf(c_291,negated_conjecture,
( inverse2(sK2,image(sK2,sK0)) != domain(sK0,sK1,sK2)
| range(sK0,sK1,sK2) != image(sK2,inverse2(sK2,sK1)) ),
inference(copy,[status(thm)],[c_290]) ).
cnf(c_180,negated_conjecture,
( domain(sK0,sK1,sK2) != inverse2(sK2,image(sK2,sK0))
| range(sK0,sK1,sK2) != image(sK2,inverse2(sK2,sK1)) ),
inference(copy,[status(thm)],[c_291]) ).
cnf(c_182,plain,
range(sK0,sK1,sK2) = range_of(sK2),
inference(resolve,[status(thm)],[c_80,c_65]) ).
cnf(c_184,negated_conjecture,
( domain(sK0,sK1,sK2) != inverse2(sK2,image(sK2,sK0))
| range_of(sK2) != image(sK2,inverse2(sK2,sK1)) ),
inference(paramod,[status(thm)],[c_182,c_180]) ).
cnf(c_186,plain,
domain(sK0,sK1,sK2) = domain_of(sK2),
inference(resolve,[status(thm)],[c_84,c_65]) ).
cnf(c_188,negated_conjecture,
( domain_of(sK2) != inverse2(sK2,image(sK2,sK0))
| range_of(sK2) != image(sK2,inverse2(sK2,sK1)) ),
inference(paramod,[status(thm)],[c_186,c_184]) ).
cnf(c_213,plain,
ilf_type(sK2,subset_type(cross_product(sK0,sK1))),
inference(resolve,[status(thm)],[c_135,c_65]) ).
cnf(c_292,negated_conjecture,
inverse4(sK0,sK1,sK2,sK1) = domain(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_139,c_65]) ).
cnf(c_293,negated_conjecture,
inverse2(sK2,sK1) = domain(sK0,sK1,sK2),
inference(paramod,[status(thm)],[c_174,c_292]) ).
cnf(c_294,negated_conjecture,
inverse2(sK2,sK1) = domain_of(sK2),
inference(paramod,[status(thm)],[c_186,c_293]) ).
cnf(c_216,negated_conjecture,
domain_of(sK2) = inverse2(sK2,sK1),
inference(copy,[status(thm)],[c_294]) ).
cnf(c_295,negated_conjecture,
( inverse2(sK2,sK1) != inverse2(sK2,image(sK2,sK0))
| range_of(sK2) != image(sK2,inverse2(sK2,sK1)) ),
inference(paramod,[status(thm)],[c_216,c_188]) ).
cnf(c_218,negated_conjecture,
( inverse2(sK2,image(sK2,sK0)) != inverse2(sK2,sK1)
| range_of(sK2) != image(sK2,inverse2(sK2,sK1)) ),
inference(copy,[status(thm)],[c_295]) ).
cnf(c_296,negated_conjecture,
image4(sK0,sK1,sK2,sK0) = range(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_141,c_65]) ).
cnf(c_297,negated_conjecture,
image(sK2,sK0) = range(sK0,sK1,sK2),
inference(paramod,[status(thm)],[c_178,c_296]) ).
cnf(c_298,negated_conjecture,
image(sK2,sK0) = range_of(sK2),
inference(paramod,[status(thm)],[c_182,c_297]) ).
cnf(c_221,negated_conjecture,
range_of(sK2) = image(sK2,sK0),
inference(copy,[status(thm)],[c_298]) ).
cnf(c_299,negated_conjecture,
( inverse2(sK2,image(sK2,sK0)) != inverse2(sK2,sK1)
| image(sK2,sK0) != image(sK2,inverse2(sK2,sK1)) ),
inference(paramod,[status(thm)],[c_221,c_218]) ).
cnf(c_223,negated_conjecture,
( inverse2(sK2,image(sK2,sK0)) != inverse2(sK2,sK1)
| image(sK2,inverse2(sK2,sK1)) != image(sK2,sK0) ),
inference(copy,[status(thm)],[c_299]) ).
cnf(c_269,plain,
ilf_type(sK2,binary_relation_type),
inference(resolve,[status(thm)],[c_213,c_170]) ).
cnf(c_300,plain,
range_of(sK2) = image(sK2,domain_of(sK2)),
inference(resolve,[status(thm)],[c_269,c_143]) ).
cnf(c_301,plain,
image(sK2,sK0) = image(sK2,domain_of(sK2)),
inference(paramod,[status(thm)],[c_221,c_300]) ).
cnf(c_302,plain,
image(sK2,sK0) = image(sK2,inverse2(sK2,sK1)),
inference(paramod,[status(thm)],[c_216,c_301]) ).
cnf(c_271,plain,
image(sK2,inverse2(sK2,sK1)) = image(sK2,sK0),
inference(copy,[status(thm)],[c_302]) ).
cnf(c_303,plain,
inverse2(sK2,range_of(sK2)) = domain_of(sK2),
inference(resolve,[status(thm)],[c_269,c_142]) ).
cnf(c_304,plain,
inverse2(sK2,image(sK2,sK0)) = domain_of(sK2),
inference(paramod,[status(thm)],[c_221,c_303]) ).
cnf(c_272,plain,
inverse2(sK2,image(sK2,sK0)) = inverse2(sK2,sK1),
inference(paramod,[status(thm)],[c_216,c_304]) ).
cnf(c_305,negated_conjecture,
( inverse2(sK2,image(sK2,sK0)) != inverse2(sK2,sK1)
| image(sK2,sK0) != image(sK2,sK0) ),
inference(paramod,[status(thm)],[c_271,c_223]) ).
cnf(c_306,negated_conjecture,
( inverse2(sK2,sK1) != inverse2(sK2,sK1)
| image(sK2,sK0) != image(sK2,sK0) ),
inference(paramod,[status(thm)],[c_272,c_305]) ).
cnf(c_307,negated_conjecture,
inverse2(sK2,sK1) != inverse2(sK2,sK1),
inference(copy,[status(thm)],[c_306]) ).
cnf(c_273,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_307]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET675+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n015.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 08:07:44 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.38 % Process 3532395 was started by sandbox2 on n015,
% 0.09/0.38 % Sat Sep 26 08:07:44 2026
% 0.09/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 0.09/0.43
% 0.09/0.43 % SZS status Theorem for theBenchmark
% 0.09/0.43
% 0.09/0.43 % Proof 1 at 0.02 (+ 0.01) seconds.
% 0.09/0.43 % Length of proof is 53.
% 0.09/0.43 % Level of proof is 10.
% 0.09/0.43 % Maximum clause weight is 28.000.
% 0.09/0.43 % Given clauses 63.
% 0.09/0.43
% 0.09/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------