%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU441+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:46:22 AM UTC 2026
% Result : Theorem 3.02s 0.81s
% Output : CNFRefutation 3.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 14
% Syntax : Number of formulae : 81 ( 34 unt; 0 def)
% Number of atoms : 148 ( 47 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 116 ( 49 ~; 38 |; 10 &)
% ( 2 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-5 aty)
% Number of variables : 133 ( 2 sgn 51 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_relset_1,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('theBenchmark.p',cc1_relset_1) ).
fof(dt_k5_relset_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> m1_subset_1(k5_relset_1(A,B,C),k1_zfmisc_1(B)) ),
file('theBenchmark.p',dt_k5_relset_1) ).
fof(dt_k9_relset_2,axiom,
! [A,B,C,D,E] :
( ( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(B,C)))
& m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) )
=> m2_relset_1(k9_relset_2(A,B,C,D,E),A,C) ),
file('theBenchmark.p',dt_k9_relset_2) ).
fof(dt_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('theBenchmark.p',dt_m2_relset_1) ).
fof(redefinition_k10_relset_1,axiom,
! [A,B,C,D] :
( m1_relset_1(C,A,B)
=> k10_relset_1(A,B,C,D) = k9_relat_1(C,D) ),
file('theBenchmark.p',redefinition_k10_relset_1) ).
fof(redefinition_k5_relset_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> k5_relset_1(A,B,C) = k2_relat_1(C) ),
file('theBenchmark.p',redefinition_k5_relset_1) ).
fof(redefinition_k9_relset_2,axiom,
! [A,B,C,D,E] :
( ( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(B,C)))
& m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B))) )
=> k9_relset_2(A,B,C,D,E) = k5_relat_1(D,E) ),
file('theBenchmark.p',redefinition_k9_relset_2) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t156_relat_1,axiom,
! [A,B,C] :
( v1_relat_1(C)
=> ( r1_tarski(A,B)
=> r1_tarski(k9_relat_1(C,A),k9_relat_1(C,B)) ) ),
file('theBenchmark.p',t156_relat_1) ).
fof(t159_relat_1,axiom,
! [A,B] :
( v1_relat_1(B)
=> ! [C] :
( v1_relat_1(C)
=> k9_relat_1(k5_relat_1(B,C),A) = k9_relat_1(C,k9_relat_1(B,A)) ) ),
file('theBenchmark.p',t159_relat_1) ).
fof(t21_funct_5,axiom,
! [A] :
( v1_relat_1(A)
=> ( k2_funct_5(A) = k2_relat_1(A)
& k1_funct_5(A) = k1_relat_1(A) ) ),
file('theBenchmark.p',t21_funct_5) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t51_relset_2,axiom,
! [A,B,C] :
( m2_relset_1(C,B,A)
=> ( k2_funct_5(C) = k10_relset_1(B,A,C,B)
& k1_funct_5(C) = k10_relset_1(A,B,k6_relset_1(B,A,C),A) ) ),
file('theBenchmark.p',t51_relset_2) ).
fof(t53_relset_2,conjecture,
! [A,B,C,D] :
( m2_relset_1(D,A,B)
=> ! [E] :
( m2_relset_1(E,B,C)
=> ( r1_tarski(k2_funct_5(k9_relset_2(A,B,C,D,E)),k2_funct_5(E))
& k2_funct_5(k9_relset_2(A,B,C,D,E)) = k10_relset_1(B,C,E,k2_funct_5(D)) ) ) ),
file('theBenchmark.p',t53_relset_2) ).
fof(t53_relset_2_neg,negated_conjecture,
~ ! [A,B,C,D] :
( m2_relset_1(D,A,B)
=> ! [E] :
( m2_relset_1(E,B,C)
=> ( r1_tarski(k2_funct_5(k9_relset_2(A,B,C,D,E)),k2_funct_5(E))
& k2_funct_5(k9_relset_2(A,B,C,D,E)) = k10_relset_1(B,C,E,k2_funct_5(D)) ) ) ),
inference(assume_negation,[status(cth)],[t53_relset_2]) ).
cnf(c_62,plain,
( m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C)))
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[dt_m2_relset_1]) ).
cnf(c_63,plain,
( m2_relset_1(k9_relset_2(B,C,E,A,D),B,E)
| ~ m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(C,E)))
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(clausify,[status(thm)],[dt_k9_relset_2]) ).
cnf(c_66,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_67,plain,
( ~ m1_relset_1(A,B,C)
| m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_69,plain,
( k10_relset_1(B,C,A,B) = k2_funct_5(A)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[t51_relset_2]) ).
fof(nnf_61,plain,
? [A,B,C,D] :
( ? [E] :
( ( ~ r1_tarski(k2_funct_5(k9_relset_2(A,B,C,D,E)),k2_funct_5(E))
| k10_relset_1(B,C,E,k2_funct_5(D)) != k2_funct_5(k9_relset_2(A,B,C,D,E)) )
& m2_relset_1(E,B,C) )
& m2_relset_1(D,A,B) ),
inference(fof_nnf,[status(thm)],[t53_relset_2_neg]) ).
fof(sk_t53_relset_2_neg,plain,
( ( ~ r1_tarski(k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k2_funct_5(sK3))
| k10_relset_1(sK2,sK4,sK3,k2_funct_5(sK0)) != k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) )
& m2_relset_1(sK3,sK2,sK4)
& m2_relset_1(sK0,sK1,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(A,sK1),skolemize(B,sK2),skolemize(C,sK4),skolemize(D,sK0),skolemize(E,sK3)],[nnf_61]) ).
cnf(c_70,negated_conjecture,
m2_relset_1(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t53_relset_2_neg]) ).
cnf(c_71,negated_conjecture,
m2_relset_1(sK3,sK2,sK4),
inference(split_conjunct,[status(thm)],[sk_t53_relset_2_neg]) ).
cnf(c_74,plain,
( v1_relat_1(A)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(clausify,[status(thm)],[cc1_relset_1]) ).
cnf(c_78,plain,
( m1_subset_1(k5_relset_1(B,C,A),k1_zfmisc_1(C))
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[dt_k5_relset_1]) ).
cnf(c_109,plain,
( k9_relat_1(A,D) = k10_relset_1(B,C,A,D)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_k10_relset_1]) ).
cnf(c_110,plain,
( k10_relset_1(B,C,A,D) = k9_relat_1(A,D)
| ~ m1_relset_1(A,B,C) ),
inference(copy,[status(thm)],[c_109]) ).
cnf(c_111,plain,
( k2_relat_1(A) = k5_relset_1(B,C,A)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_k5_relset_1]) ).
cnf(c_112,plain,
( k5_relset_1(B,C,A) = k2_relat_1(A)
| ~ m1_relset_1(A,B,C) ),
inference(copy,[status(thm)],[c_111]) ).
cnf(c_114,plain,
( k5_relat_1(A,D) = k9_relset_2(B,C,E,A,D)
| ~ m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(C,E)))
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(clausify,[status(thm)],[redefinition_k9_relset_2]) ).
cnf(c_115,plain,
( k9_relset_2(B,C,E,A,D) = k5_relat_1(A,D)
| ~ m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(C,E)))
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_117,plain,
( r1_tarski(k9_relat_1(A,B),k9_relat_1(A,C))
| ~ r1_tarski(B,C)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[t156_relat_1]) ).
cnf(c_118,plain,
( k9_relat_1(k5_relat_1(A,B),C) = k9_relat_1(B,k9_relat_1(A,C))
| ~ v1_relat_1(B)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[t159_relat_1]) ).
cnf(c_122,plain,
( k2_relat_1(A) = k2_funct_5(A)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[t21_funct_5]) ).
cnf(c_124,plain,
( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_131,negated_conjecture,
( ~ r1_tarski(k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k2_funct_5(sK3))
| k10_relset_1(sK2,sK4,sK3,k2_funct_5(sK0)) != k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) ),
inference(split_conjunct,[status(thm)],[sk_t53_relset_2_neg]) ).
cnf(c_132,negated_conjecture,
( ~ r1_tarski(k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k2_funct_5(sK3))
| k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) != k10_relset_1(sK2,sK4,sK3,k2_funct_5(sK0)) ),
inference(copy,[status(thm)],[c_131]) ).
cnf(c_137,plain,
( ~ m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(B,C)))
| ~ m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B)))
| m1_relset_1(k9_relset_2(A,B,C,D,E),A,C) ),
inference(resolve,[status(thm)],[c_66,c_63]) ).
cnf(c_148,plain,
( ~ m1_relset_1(C,A,B)
| k10_relset_1(A,B,C,A) = k2_funct_5(C) ),
inference(resolve,[status(thm)],[c_69,c_67]) ).
cnf(c_155,negated_conjecture,
m1_relset_1(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_70,c_66]) ).
cnf(c_156,negated_conjecture,
m1_subset_1(sK0,k1_zfmisc_1(k2_zfmisc_1(sK1,sK2))),
inference(resolve,[status(thm)],[c_70,c_62]) ).
cnf(c_160,negated_conjecture,
m1_relset_1(sK3,sK2,sK4),
inference(resolve,[status(thm)],[c_71,c_66]) ).
cnf(c_161,negated_conjecture,
m1_subset_1(sK3,k1_zfmisc_1(k2_zfmisc_1(sK2,sK4))),
inference(resolve,[status(thm)],[c_71,c_62]) ).
cnf(c_516,plain,
k5_relset_1(sK1,sK2,sK0) = k2_relat_1(sK0),
inference(resolve,[status(thm)],[c_155,c_112]) ).
cnf(c_517,plain,
k10_relset_1(sK1,sK2,sK0,A) = k9_relat_1(sK0,A),
inference(resolve,[status(thm)],[c_155,c_110]) ).
cnf(c_7026,negated_conjecture,
m1_subset_1(k5_relset_1(sK1,sK2,sK0),k1_zfmisc_1(sK2)),
inference(resolve,[status(thm)],[c_155,c_78]) ).
cnf(c_519,negated_conjecture,
m1_subset_1(k2_relat_1(sK0),k1_zfmisc_1(sK2)),
inference(paramod,[status(thm)],[c_516,c_7026]) ).
cnf(c_7027,negated_conjecture,
k10_relset_1(sK1,sK2,sK0,sK1) = k2_funct_5(sK0),
inference(resolve,[status(thm)],[c_148,c_155]) ).
cnf(c_522,negated_conjecture,
k9_relat_1(sK0,sK1) = k2_funct_5(sK0),
inference(paramod,[status(thm)],[c_517,c_7027]) ).
cnf(c_540,plain,
v1_relat_1(sK0),
inference(resolve,[status(thm)],[c_156,c_74]) ).
cnf(c_593,plain,
k10_relset_1(sK2,sK4,sK3,A) = k9_relat_1(sK3,A),
inference(resolve,[status(thm)],[c_160,c_110]) ).
cnf(c_7028,negated_conjecture,
k10_relset_1(sK2,sK4,sK3,sK2) = k2_funct_5(sK3),
inference(resolve,[status(thm)],[c_148,c_160]) ).
cnf(c_598,negated_conjecture,
k9_relat_1(sK3,sK2) = k2_funct_5(sK3),
inference(paramod,[status(thm)],[c_593,c_7028]) ).
cnf(c_603,negated_conjecture,
( ~ r1_tarski(k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k2_funct_5(sK3))
| k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) != k9_relat_1(sK3,k2_funct_5(sK0)) ),
inference(paramod,[status(thm)],[c_593,c_132]) ).
cnf(c_617,plain,
v1_relat_1(sK3),
inference(resolve,[status(thm)],[c_161,c_74]) ).
cnf(c_7029,negated_conjecture,
( ~ m1_subset_1(B,k1_zfmisc_1(k2_zfmisc_1(sK2,A)))
| m1_relset_1(k9_relset_2(sK1,sK2,A,sK0,B),sK1,A) ),
inference(resolve,[status(thm)],[c_137,c_156]) ).
cnf(c_632,negated_conjecture,
m1_relset_1(k9_relset_2(sK1,sK2,sK4,sK0,sK3),sK1,sK4),
inference(resolve,[status(thm)],[c_7029,c_161]) ).
cnf(c_7030,negated_conjecture,
( k9_relset_2(sK1,sK2,B,sK0,A) = k5_relat_1(sK0,A)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(sK2,B))) ),
inference(resolve,[status(thm)],[c_115,c_156]) ).
cnf(c_646,negated_conjecture,
k9_relset_2(sK1,sK2,sK4,sK0,sK3) = k5_relat_1(sK0,sK3),
inference(resolve,[status(thm)],[c_7030,c_161]) ).
cnf(c_654,negated_conjecture,
m1_relset_1(k5_relat_1(sK0,sK3),sK1,sK4),
inference(paramod,[status(thm)],[c_646,c_632]) ).
cnf(c_7031,negated_conjecture,
( ~ r1_tarski(k2_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k2_funct_5(sK3))
| k2_funct_5(k5_relat_1(sK0,sK3)) != k9_relat_1(sK3,k2_funct_5(sK0)) ),
inference(paramod,[status(thm)],[c_646,c_603]) ).
cnf(c_657,negated_conjecture,
( ~ r1_tarski(k2_funct_5(k5_relat_1(sK0,sK3)),k2_funct_5(sK3))
| k2_funct_5(k5_relat_1(sK0,sK3)) != k9_relat_1(sK3,k2_funct_5(sK0)) ),
inference(paramod,[status(thm)],[c_646,c_7031]) ).
cnf(c_731,plain,
k2_relat_1(sK0) = k2_funct_5(sK0),
inference(resolve,[status(thm)],[c_540,c_122]) ).
cnf(c_767,negated_conjecture,
m1_subset_1(k2_funct_5(sK0),k1_zfmisc_1(sK2)),
inference(paramod,[status(thm)],[c_731,c_519]) ).
cnf(c_7032,plain,
( k9_relat_1(k5_relat_1(sK0,A),B) = k9_relat_1(A,k9_relat_1(sK0,B))
| ~ v1_relat_1(A) ),
inference(resolve,[status(thm)],[c_118,c_540]) ).
cnf(c_785,plain,
k9_relat_1(k5_relat_1(sK0,sK3),A) = k9_relat_1(sK3,k9_relat_1(sK0,A)),
inference(resolve,[status(thm)],[c_7032,c_617]) ).
cnf(c_5784,plain,
r1_tarski(k2_funct_5(sK0),sK2),
inference(resolve,[status(thm)],[c_767,c_124]) ).
cnf(c_7033,plain,
( r1_tarski(k9_relat_1(sK3,A),k9_relat_1(sK3,B))
| ~ r1_tarski(A,B) ),
inference(resolve,[status(thm)],[c_117,c_617]) ).
cnf(c_7034,plain,
r1_tarski(k9_relat_1(sK3,k2_funct_5(sK0)),k9_relat_1(sK3,sK2)),
inference(resolve,[status(thm)],[c_7033,c_5784]) ).
cnf(c_5801,plain,
r1_tarski(k9_relat_1(sK3,k2_funct_5(sK0)),k2_funct_5(sK3)),
inference(paramod,[status(thm)],[c_598,c_7034]) ).
cnf(c_7035,plain,
k10_relset_1(sK1,sK4,k5_relat_1(sK0,sK3),A) = k9_relat_1(k5_relat_1(sK0,sK3),A),
inference(resolve,[status(thm)],[c_654,c_110]) ).
cnf(c_7013,plain,
k10_relset_1(sK1,sK4,k5_relat_1(sK0,sK3),A) = k9_relat_1(sK3,k9_relat_1(sK0,A)),
inference(paramod,[status(thm)],[c_785,c_7035]) ).
cnf(c_7036,plain,
k10_relset_1(sK1,sK4,k5_relat_1(sK0,sK3),sK1) = k2_funct_5(k5_relat_1(sK0,sK3)),
inference(resolve,[status(thm)],[c_148,c_654]) ).
cnf(c_7037,plain,
k9_relat_1(sK3,k9_relat_1(sK0,sK1)) = k2_funct_5(k5_relat_1(sK0,sK3)),
inference(paramod,[status(thm)],[c_7013,c_7036]) ).
cnf(c_7038,plain,
k9_relat_1(sK3,k2_funct_5(sK0)) = k2_funct_5(k5_relat_1(sK0,sK3)),
inference(paramod,[status(thm)],[c_522,c_7037]) ).
cnf(c_7017,plain,
k2_funct_5(k5_relat_1(sK0,sK3)) = k9_relat_1(sK3,k2_funct_5(sK0)),
inference(copy,[status(thm)],[c_7038]) ).
cnf(c_7039,negated_conjecture,
( ~ r1_tarski(k2_funct_5(k5_relat_1(sK0,sK3)),k2_funct_5(sK3))
| k9_relat_1(sK3,k2_funct_5(sK0)) != k9_relat_1(sK3,k2_funct_5(sK0)) ),
inference(paramod,[status(thm)],[c_7017,c_657]) ).
cnf(c_7040,negated_conjecture,
( ~ r1_tarski(k9_relat_1(sK3,k2_funct_5(sK0)),k2_funct_5(sK3))
| k9_relat_1(sK3,k2_funct_5(sK0)) != k9_relat_1(sK3,k2_funct_5(sK0)) ),
inference(paramod,[status(thm)],[c_7017,c_7039]) ).
cnf(c_7041,negated_conjecture,
~ r1_tarski(k9_relat_1(sK3,k2_funct_5(sK0)),k2_funct_5(sK3)),
inference(copy,[status(thm)],[c_7040]) ).
cnf(c_7025,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_5801,c_7041]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU441+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n001.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 26 10:00:12 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 1566243 was started by sandbox on n001,
% 0.07/0.35 % Sat Sep 26 10:00:12 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.36
% 0.11/0.36 % From the command line: assign(max_seconds, 300).
% 3.02/0.81
% 3.02/0.81 % SZS status Theorem for theBenchmark
% 3.02/0.81
% 3.02/0.81 % Proof 1 at 0.30 (+ 0.13) seconds.
% 3.02/0.81 % Length of proof is 62.
% 3.02/0.81 % Level of proof is 8.
% 3.02/0.81 % Maximum clause weight is 39.000.
% 3.02/0.81 % Given clauses 324.
% 3.02/0.81
% 3.02/0.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------