%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU440+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 08:46:22 AM UTC 2026
% Result : Theorem 19.62s 3.08s
% Output : CNFRefutation 19.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 17
% Syntax : Number of formulae : 120 ( 60 unt; 0 def)
% Number of atoms : 203 ( 74 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 148 ( 65 ~; 51 |; 9 &)
% ( 2 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-5 aty)
% Number of variables : 161 ( 7 sgn 58 !; 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_k10_relset_1,axiom,
! [A,B,C,D] :
( m1_relset_1(C,A,B)
=> m1_subset_1(k10_relset_1(A,B,C,D),k1_zfmisc_1(B)) ),
file('theBenchmark.p',dt_k10_relset_1) ).
fof(dt_k4_relat_1,axiom,
! [A] :
( v1_relat_1(A)
=> v1_relat_1(k4_relat_1(A)) ),
file('theBenchmark.p',dt_k4_relat_1) ).
fof(dt_k6_relset_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> m2_relset_1(k6_relset_1(A,B,C),B,A) ),
file('theBenchmark.p',dt_k6_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(involutiveness_k4_relat_1,axiom,
! [A] :
( v1_relat_1(A)
=> k4_relat_1(k4_relat_1(A)) = A ),
file('theBenchmark.p',involutiveness_k4_relat_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_k6_relset_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> k6_relset_1(A,B,C) = k4_relat_1(C) ),
file('theBenchmark.p',redefinition_k6_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(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(t54_relat_1,axiom,
! [A] :
( v1_relat_1(A)
=> ! [B] :
( v1_relat_1(B)
=> k4_relat_1(k5_relat_1(A,B)) = k5_relat_1(k4_relat_1(B),k4_relat_1(A)) ) ),
file('theBenchmark.p',t54_relat_1) ).
fof(t52_relset_2,conjecture,
! [A,B,C,D] :
( m2_relset_1(D,A,B)
=> ! [E] :
( m2_relset_1(E,B,C)
=> ( r1_tarski(k1_funct_5(k9_relset_2(A,B,C,D,E)),k1_funct_5(D))
& k1_funct_5(k9_relset_2(A,B,C,D,E)) = k10_relset_1(B,A,k6_relset_1(A,B,D),k1_funct_5(E)) ) ) ),
file('theBenchmark.p',t52_relset_2) ).
fof(t52_relset_2_neg,negated_conjecture,
~ ! [A,B,C,D] :
( m2_relset_1(D,A,B)
=> ! [E] :
( m2_relset_1(E,B,C)
=> ( r1_tarski(k1_funct_5(k9_relset_2(A,B,C,D,E)),k1_funct_5(D))
& k1_funct_5(k9_relset_2(A,B,C,D,E)) = k10_relset_1(B,A,k6_relset_1(A,B,D),k1_funct_5(E)) ) ) ),
inference(assume_negation,[status(cth)],[t52_relset_2]) ).
cnf(c_63,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_64,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_65,plain,
( m2_relset_1(k6_relset_1(B,C,A),C,B)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[dt_k6_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(C,B,k6_relset_1(B,C,A),C) = k1_funct_5(A)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[t51_relset_2]) ).
fof(nnf_62,plain,
? [A,B,C,D] :
( ? [E] :
( ( ~ r1_tarski(k1_funct_5(k9_relset_2(A,B,C,D,E)),k1_funct_5(D))
| k10_relset_1(B,A,k6_relset_1(A,B,D),k1_funct_5(E)) != k1_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)],[t52_relset_2_neg]) ).
fof(sk_t52_relset_2_neg,plain,
( ( ~ r1_tarski(k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k1_funct_5(sK0))
| k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),k1_funct_5(sK3)) != k1_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_62]) ).
cnf(c_71,negated_conjecture,
m2_relset_1(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t52_relset_2_neg]) ).
cnf(c_72,negated_conjecture,
m2_relset_1(sK3,sK2,sK4),
inference(split_conjunct,[status(thm)],[sk_t52_relset_2_neg]) ).
cnf(c_75,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_76,plain,
( m1_subset_1(k10_relset_1(B,C,A,D),k1_zfmisc_1(C))
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[dt_k10_relset_1]) ).
cnf(c_77,plain,
( v1_relat_1(k4_relat_1(A))
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[dt_k4_relat_1]) ).
cnf(c_99,plain,
( k4_relat_1(k4_relat_1(A)) = A
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[involutiveness_k4_relat_1]) ).
cnf(c_110,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_111,plain,
( k10_relset_1(B,C,A,D) = k9_relat_1(A,D)
| ~ m1_relset_1(A,B,C) ),
inference(copy,[status(thm)],[c_110]) ).
cnf(c_114,plain,
( k4_relat_1(A) = k6_relset_1(B,C,A)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_k6_relset_1]) ).
cnf(c_115,plain,
( k6_relset_1(B,C,A) = k4_relat_1(A)
| ~ m1_relset_1(A,B,C) ),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_116,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_117,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_116]) ).
cnf(c_119,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_120,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_126,plain,
( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_129,plain,
( k5_relat_1(k4_relat_1(B),k4_relat_1(A)) = k4_relat_1(k5_relat_1(A,B))
| ~ v1_relat_1(B)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[t54_relat_1]) ).
cnf(c_130,plain,
( k4_relat_1(k5_relat_1(A,B)) = k5_relat_1(k4_relat_1(B),k4_relat_1(A))
| ~ v1_relat_1(B)
| ~ v1_relat_1(A) ),
inference(copy,[status(thm)],[c_129]) ).
cnf(c_135,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k1_funct_5(sK0))
| k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),k1_funct_5(sK3)) != k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) ),
inference(split_conjunct,[status(thm)],[sk_t52_relset_2_neg]) ).
cnf(c_136,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k1_funct_5(sK0))
| k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) != k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),k1_funct_5(sK3)) ),
inference(copy,[status(thm)],[c_135]) ).
cnf(c_141,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_67,c_64]) ).
cnf(c_142,plain,
( ~ m1_relset_1(C,A,B)
| m1_relset_1(k6_relset_1(A,B,C),B,A) ),
inference(resolve,[status(thm)],[c_67,c_65]) ).
cnf(c_146,plain,
( ~ m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(C,A)))
| ~ m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(B,C)))
| k10_relset_1(A,B,k6_relset_1(B,A,k9_relset_2(B,C,A,D,E)),A) = k1_funct_5(k9_relset_2(B,C,A,D,E)) ),
inference(resolve,[status(thm)],[c_69,c_64]) ).
cnf(c_147,plain,
( ~ m1_relset_1(C,A,B)
| k10_relset_1(A,B,k6_relset_1(B,A,k6_relset_1(A,B,C)),A) = k1_funct_5(k6_relset_1(A,B,C)) ),
inference(resolve,[status(thm)],[c_69,c_65]) ).
cnf(c_159,negated_conjecture,
m1_relset_1(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_71,c_67]) ).
cnf(c_160,negated_conjecture,
m1_subset_1(sK0,k1_zfmisc_1(k2_zfmisc_1(sK1,sK2))),
inference(resolve,[status(thm)],[c_71,c_63]) ).
cnf(c_164,negated_conjecture,
m1_relset_1(sK3,sK2,sK4),
inference(resolve,[status(thm)],[c_72,c_67]) ).
cnf(c_165,negated_conjecture,
m1_subset_1(sK3,k1_zfmisc_1(k2_zfmisc_1(sK2,sK4))),
inference(resolve,[status(thm)],[c_72,c_63]) ).
cnf(c_402,plain,
m1_relset_1(k6_relset_1(sK1,sK2,sK0),sK2,sK1),
inference(resolve,[status(thm)],[c_159,c_142]) ).
cnf(c_404,plain,
k6_relset_1(sK1,sK2,sK0) = k4_relat_1(sK0),
inference(resolve,[status(thm)],[c_159,c_115]) ).
cnf(c_411,plain,
m1_relset_1(k4_relat_1(sK0),sK2,sK1),
inference(paramod,[status(thm)],[c_404,c_402]) ).
cnf(c_415,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k1_funct_5(sK0))
| k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) != k10_relset_1(sK2,sK1,k4_relat_1(sK0),k1_funct_5(sK3)) ),
inference(paramod,[status(thm)],[c_404,c_136]) ).
cnf(c_420,plain,
( ~ m1_subset_1(B,k1_zfmisc_1(k2_zfmisc_1(sK2,A)))
| k10_relset_1(A,sK1,k6_relset_1(sK1,A,k9_relset_2(sK1,sK2,A,sK0,B)),A) = k1_funct_5(k9_relset_2(sK1,sK2,A,sK0,B)) ),
inference(resolve,[status(thm)],[c_160,c_146]) ).
cnf(c_422,plain,
( ~ 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_160,c_141]) ).
cnf(c_430,plain,
( 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_160,c_117]) ).
cnf(c_431,plain,
v1_relat_1(sK0),
inference(resolve,[status(thm)],[c_160,c_75]) ).
cnf(c_434,plain,
m1_relset_1(k6_relset_1(sK2,sK4,sK3),sK4,sK2),
inference(resolve,[status(thm)],[c_164,c_142]) ).
cnf(c_436,plain,
k6_relset_1(sK2,sK4,sK3) = k4_relat_1(sK3),
inference(resolve,[status(thm)],[c_164,c_115]) ).
cnf(c_443,plain,
m1_relset_1(k4_relat_1(sK3),sK4,sK2),
inference(paramod,[status(thm)],[c_436,c_434]) ).
cnf(c_462,plain,
v1_relat_1(sK3),
inference(resolve,[status(thm)],[c_165,c_75]) ).
cnf(c_555,plain,
( k4_relat_1(k5_relat_1(sK0,A)) = k5_relat_1(k4_relat_1(A),k4_relat_1(sK0))
| ~ v1_relat_1(A) ),
inference(resolve,[status(thm)],[c_431,c_130]) ).
cnf(c_561,plain,
k4_relat_1(k4_relat_1(sK0)) = sK0,
inference(resolve,[status(thm)],[c_431,c_99]) ).
cnf(c_570,plain,
v1_relat_1(k4_relat_1(sK0)),
inference(resolve,[status(thm)],[c_431,c_77]) ).
cnf(c_583,plain,
k4_relat_1(k4_relat_1(sK3)) = sK3,
inference(resolve,[status(thm)],[c_462,c_99]) ).
cnf(c_592,plain,
v1_relat_1(k4_relat_1(sK3)),
inference(resolve,[status(thm)],[c_462,c_77]) ).
cnf(c_737,plain,
( k9_relat_1(k5_relat_1(A,k4_relat_1(sK0)),B) = k9_relat_1(k4_relat_1(sK0),k9_relat_1(A,B))
| ~ v1_relat_1(A) ),
inference(resolve,[status(thm)],[c_570,c_120]) ).
cnf(c_739,plain,
( r1_tarski(k9_relat_1(k4_relat_1(sK0),A),k9_relat_1(k4_relat_1(sK0),B))
| ~ r1_tarski(A,B) ),
inference(resolve,[status(thm)],[c_570,c_119]) ).
cnf(c_2051,plain,
k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,k6_relset_1(sK2,sK1,k4_relat_1(sK0))),sK2) = k1_funct_5(k6_relset_1(sK2,sK1,k4_relat_1(sK0))),
inference(resolve,[status(thm)],[c_411,c_147]) ).
cnf(c_16840,plain,
k6_relset_1(sK2,sK1,k4_relat_1(sK0)) = k4_relat_1(k4_relat_1(sK0)),
inference(resolve,[status(thm)],[c_411,c_115]) ).
cnf(c_2054,plain,
k6_relset_1(sK2,sK1,k4_relat_1(sK0)) = sK0,
inference(paramod,[status(thm)],[c_561,c_16840]) ).
cnf(c_2056,plain,
k10_relset_1(sK2,sK1,k4_relat_1(sK0),A) = k9_relat_1(k4_relat_1(sK0),A),
inference(resolve,[status(thm)],[c_411,c_111]) ).
cnf(c_16841,plain,
k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),sK2) = k1_funct_5(k6_relset_1(sK2,sK1,k4_relat_1(sK0))),
inference(paramod,[status(thm)],[c_2054,c_2051]) ).
cnf(c_16842,plain,
k10_relset_1(sK2,sK1,k4_relat_1(sK0),sK2) = k1_funct_5(k6_relset_1(sK2,sK1,k4_relat_1(sK0))),
inference(paramod,[status(thm)],[c_404,c_16841]) ).
cnf(c_16843,plain,
k9_relat_1(k4_relat_1(sK0),sK2) = k1_funct_5(k6_relset_1(sK2,sK1,k4_relat_1(sK0))),
inference(paramod,[status(thm)],[c_2056,c_16842]) ).
cnf(c_16844,plain,
k9_relat_1(k4_relat_1(sK0),sK2) = k1_funct_5(sK0),
inference(paramod,[status(thm)],[c_2054,c_16843]) ).
cnf(c_2060,plain,
k1_funct_5(sK0) = k9_relat_1(k4_relat_1(sK0),sK2),
inference(copy,[status(thm)],[c_16844]) ).
cnf(c_16845,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k1_funct_5(sK0))
| k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) != k9_relat_1(k4_relat_1(sK0),k1_funct_5(sK3)) ),
inference(paramod,[status(thm)],[c_2056,c_415]) ).
cnf(c_2062,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k9_relat_1(k4_relat_1(sK0),sK2))
| k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) != k9_relat_1(k4_relat_1(sK0),k1_funct_5(sK3)) ),
inference(paramod,[status(thm)],[c_2060,c_16845]) ).
cnf(c_2288,plain,
k10_relset_1(sK4,sK2,k6_relset_1(sK2,sK4,k6_relset_1(sK4,sK2,k4_relat_1(sK3))),sK4) = k1_funct_5(k6_relset_1(sK4,sK2,k4_relat_1(sK3))),
inference(resolve,[status(thm)],[c_443,c_147]) ).
cnf(c_16846,plain,
k6_relset_1(sK4,sK2,k4_relat_1(sK3)) = k4_relat_1(k4_relat_1(sK3)),
inference(resolve,[status(thm)],[c_443,c_115]) ).
cnf(c_2291,plain,
k6_relset_1(sK4,sK2,k4_relat_1(sK3)) = sK3,
inference(paramod,[status(thm)],[c_583,c_16846]) ).
cnf(c_2293,plain,
k10_relset_1(sK4,sK2,k4_relat_1(sK3),A) = k9_relat_1(k4_relat_1(sK3),A),
inference(resolve,[status(thm)],[c_443,c_111]) ).
cnf(c_16847,plain,
m1_subset_1(k10_relset_1(sK4,sK2,k4_relat_1(sK3),A),k1_zfmisc_1(sK2)),
inference(resolve,[status(thm)],[c_443,c_76]) ).
cnf(c_2296,plain,
m1_subset_1(k9_relat_1(k4_relat_1(sK3),A),k1_zfmisc_1(sK2)),
inference(paramod,[status(thm)],[c_2293,c_16847]) ).
cnf(c_16848,plain,
k10_relset_1(sK4,sK2,k6_relset_1(sK2,sK4,sK3),sK4) = k1_funct_5(k6_relset_1(sK4,sK2,k4_relat_1(sK3))),
inference(paramod,[status(thm)],[c_2291,c_2288]) ).
cnf(c_16849,plain,
k10_relset_1(sK4,sK2,k4_relat_1(sK3),sK4) = k1_funct_5(k6_relset_1(sK4,sK2,k4_relat_1(sK3))),
inference(paramod,[status(thm)],[c_436,c_16848]) ).
cnf(c_16850,plain,
k9_relat_1(k4_relat_1(sK3),sK4) = k1_funct_5(k6_relset_1(sK4,sK2,k4_relat_1(sK3))),
inference(paramod,[status(thm)],[c_2293,c_16849]) ).
cnf(c_16851,plain,
k9_relat_1(k4_relat_1(sK3),sK4) = k1_funct_5(sK3),
inference(paramod,[status(thm)],[c_2291,c_16850]) ).
cnf(c_2297,plain,
k1_funct_5(sK3) = k9_relat_1(k4_relat_1(sK3),sK4),
inference(copy,[status(thm)],[c_16851]) ).
cnf(c_2299,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k9_relat_1(k4_relat_1(sK0),sK2))
| k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)) != k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)) ),
inference(paramod,[status(thm)],[c_2297,c_2062]) ).
cnf(c_7324,plain,
k10_relset_1(sK4,sK1,k6_relset_1(sK1,sK4,k9_relset_2(sK1,sK2,sK4,sK0,sK3)),sK4) = k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),
inference(resolve,[status(thm)],[c_420,c_165]) ).
cnf(c_7361,plain,
m1_relset_1(k9_relset_2(sK1,sK2,sK4,sK0,sK3),sK1,sK4),
inference(resolve,[status(thm)],[c_422,c_165]) ).
cnf(c_7436,plain,
k9_relset_2(sK1,sK2,sK4,sK0,sK3) = k5_relat_1(sK0,sK3),
inference(resolve,[status(thm)],[c_430,c_165]) ).
cnf(c_7466,plain,
m1_relset_1(k5_relat_1(sK0,sK3),sK1,sK4),
inference(paramod,[status(thm)],[c_7436,c_7361]) ).
cnf(c_16852,plain,
k10_relset_1(sK4,sK1,k6_relset_1(sK1,sK4,k5_relat_1(sK0,sK3)),sK4) = k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),
inference(paramod,[status(thm)],[c_7436,c_7324]) ).
cnf(c_7467,plain,
k10_relset_1(sK4,sK1,k6_relset_1(sK1,sK4,k5_relat_1(sK0,sK3)),sK4) = k1_funct_5(k5_relat_1(sK0,sK3)),
inference(paramod,[status(thm)],[c_7436,c_16852]) ).
cnf(c_16853,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k9_relset_2(sK1,sK2,sK4,sK0,sK3)),k9_relat_1(k4_relat_1(sK0),sK2))
| k1_funct_5(k5_relat_1(sK0,sK3)) != k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)) ),
inference(paramod,[status(thm)],[c_7436,c_2299]) ).
cnf(c_7469,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k5_relat_1(sK0,sK3)),k9_relat_1(k4_relat_1(sK0),sK2))
| k1_funct_5(k5_relat_1(sK0,sK3)) != k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)) ),
inference(paramod,[status(thm)],[c_7436,c_16853]) ).
cnf(c_7472,plain,
m1_relset_1(k6_relset_1(sK1,sK4,k5_relat_1(sK0,sK3)),sK4,sK1),
inference(resolve,[status(thm)],[c_7466,c_142]) ).
cnf(c_7474,plain,
k6_relset_1(sK1,sK4,k5_relat_1(sK0,sK3)) = k4_relat_1(k5_relat_1(sK0,sK3)),
inference(resolve,[status(thm)],[c_7466,c_115]) ).
cnf(c_7481,plain,
m1_relset_1(k4_relat_1(k5_relat_1(sK0,sK3)),sK4,sK1),
inference(paramod,[status(thm)],[c_7474,c_7472]) ).
cnf(c_7484,plain,
k10_relset_1(sK4,sK1,k4_relat_1(k5_relat_1(sK0,sK3)),sK4) = k1_funct_5(k5_relat_1(sK0,sK3)),
inference(paramod,[status(thm)],[c_7474,c_7467]) ).
cnf(c_11499,plain,
k4_relat_1(k5_relat_1(sK0,sK3)) = k5_relat_1(k4_relat_1(sK3),k4_relat_1(sK0)),
inference(resolve,[status(thm)],[c_555,c_462]) ).
cnf(c_11557,plain,
k10_relset_1(sK4,sK1,k5_relat_1(k4_relat_1(sK3),k4_relat_1(sK0)),sK4) = k1_funct_5(k5_relat_1(sK0,sK3)),
inference(paramod,[status(thm)],[c_11499,c_7484]) ).
cnf(c_11560,plain,
m1_relset_1(k5_relat_1(k4_relat_1(sK3),k4_relat_1(sK0)),sK4,sK1),
inference(paramod,[status(thm)],[c_11499,c_7481]) ).
cnf(c_13384,plain,
r1_tarski(k9_relat_1(k4_relat_1(sK3),A),sK2),
inference(resolve,[status(thm)],[c_2296,c_126]) ).
cnf(c_15525,plain,
k9_relat_1(k5_relat_1(k4_relat_1(sK3),k4_relat_1(sK0)),A) = k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),A)),
inference(resolve,[status(thm)],[c_737,c_592]) ).
cnf(c_15581,plain,
r1_tarski(k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),A)),k9_relat_1(k4_relat_1(sK0),sK2)),
inference(resolve,[status(thm)],[c_739,c_13384]) ).
cnf(c_16854,plain,
k10_relset_1(sK4,sK1,k5_relat_1(k4_relat_1(sK3),k4_relat_1(sK0)),A) = k9_relat_1(k5_relat_1(k4_relat_1(sK3),k4_relat_1(sK0)),A),
inference(resolve,[status(thm)],[c_11560,c_111]) ).
cnf(c_16827,plain,
k10_relset_1(sK4,sK1,k5_relat_1(k4_relat_1(sK3),k4_relat_1(sK0)),A) = k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),A)),
inference(paramod,[status(thm)],[c_15525,c_16854]) ).
cnf(c_16855,plain,
k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)) = k1_funct_5(k5_relat_1(sK0,sK3)),
inference(paramod,[status(thm)],[c_16827,c_11557]) ).
cnf(c_16831,plain,
k1_funct_5(k5_relat_1(sK0,sK3)) = k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)),
inference(copy,[status(thm)],[c_16855]) ).
cnf(c_16856,negated_conjecture,
( ~ r1_tarski(k1_funct_5(k5_relat_1(sK0,sK3)),k9_relat_1(k4_relat_1(sK0),sK2))
| k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)) != k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)) ),
inference(paramod,[status(thm)],[c_16831,c_7469]) ).
cnf(c_16857,negated_conjecture,
( ~ r1_tarski(k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)),k9_relat_1(k4_relat_1(sK0),sK2))
| k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)) != k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)) ),
inference(paramod,[status(thm)],[c_16831,c_16856]) ).
cnf(c_16858,negated_conjecture,
~ r1_tarski(k9_relat_1(k4_relat_1(sK0),k9_relat_1(k4_relat_1(sK3),sK4)),k9_relat_1(k4_relat_1(sK0),sK2)),
inference(copy,[status(thm)],[c_16857]) ).
cnf(c_16839,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_15581,c_16858]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU440+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n010.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sat Sep 26 09:53:45 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 3058813 was started by sandbox2 on n010,
% 0.09/0.38 % Sat Sep 26 09:53:45 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.40
% 0.09/0.40 % From the command line: assign(max_seconds, 300).
% 19.62/3.08
% 19.62/3.08 % given #500 (T,wt=20): 3365 v1_relat_1(k5_relat_1(c7,k4_relat_1(c3))). [resolve(569,a,258,a)].
% 19.62/3.08
% 19.62/3.08 % given #1000 (A,wt=40): 737 -v1_relat_1(A) | k9_relat_1(k5_relat_1(A,k4_relat_1(c7)),B) = k9_relat_1(k4_relat_1(c7),k9_relat_1(A,B)). [resolve(570,a,120,b)].
% 19.62/3.08
% 19.62/3.08 % SZS status Theorem for theBenchmark
% 19.62/3.08
% 19.62/3.08 % Proof 1 at 1.58 (+ 0.55) seconds.
% 19.62/3.08 % Length of proof is 98.
% 19.62/3.08 % Level of proof is 11.
% 19.62/3.08 % Maximum clause weight is 53.000.
% 19.62/3.08 % Given clauses 1123.
% 19.62/3.08
% 19.62/3.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------