%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU427+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 : n012.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:18 AM UTC 2026
% Result : Theorem 29.74s 4.73s
% Output : CNFRefutation 29.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 16
% Syntax : Number of formulae : 85 ( 40 unt; 0 def)
% Number of atoms : 156 ( 62 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 115 ( 44 ~; 36 |; 14 &)
% ( 1 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 6 con; 0-4 aty)
% Number of variables : 149 ( 4 sgn 53 !; 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(commutativity_k2_xboole_0,axiom,
! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A),
file('theBenchmark.p',commutativity_k2_xboole_0) ).
fof(d4_relset_2,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(A))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> k7_relset_2(A,B,C,D) = k8_setfam_1(B,k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,D),k3_pua2mss1(C))) ) ),
file('theBenchmark.p',d4_relset_2) ).
fof(dt_k4_subset_1,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A)) )
=> m1_subset_1(k4_subset_1(A,B,C),k1_zfmisc_1(A)) ),
file('theBenchmark.p',dt_k4_subset_1) ).
fof(dt_k5_relset_2,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( v1_funct_1(k5_relset_2(A,B))
& v1_relat_1(k5_relset_2(A,B)) ) ),
file('theBenchmark.p',dt_k5_relset_2) ).
fof(dt_k6_relset_2,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A)))
=> ( m2_relset_1(k6_relset_2(A,B,C),k1_zfmisc_1(B),k1_zfmisc_1(A))
& v1_funct_2(k6_relset_2(A,B,C),k1_zfmisc_1(B),k1_zfmisc_1(A))
& v1_funct_1(k6_relset_2(A,B,C)) ) ),
file('theBenchmark.p',dt_k6_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_k4_relset_2,axiom,
! [A,B,C,D] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,k1_zfmisc_1(B))))
=> k4_relset_2(A,B,C,D) = k9_relat_1(C,D) ),
file('theBenchmark.p',redefinition_k4_relset_2) ).
fof(redefinition_k4_subset_1,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A)) )
=> k4_subset_1(A,B,C) = k2_xboole_0(B,C) ),
file('theBenchmark.p',redefinition_k4_subset_1) ).
fof(redefinition_k6_relset_2,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A)))
=> k6_relset_2(A,B,C) = k5_relset_2(B,C) ),
file('theBenchmark.p',redefinition_k6_relset_2) ).
fof(redefinition_k8_relset_2,axiom,
! [A,B,C,D] :
( ( m1_subset_1(D,k1_zfmisc_1(k2_zfmisc_1(A,B)))
& m1_subset_1(C,k1_zfmisc_1(A)) )
=> k8_relset_2(A,B,C,D) = k7_relset_2(A,B,C,D) ),
file('theBenchmark.p',redefinition_k8_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(t153_relat_1,axiom,
! [A,B,C] :
( v1_relat_1(C)
=> k9_relat_1(C,k2_xboole_0(A,B)) = k2_xboole_0(k9_relat_1(C,A),k9_relat_1(C,B)) ),
file('theBenchmark.p',t153_relat_1) ).
fof(t1_boole,axiom,
! [A] : k2_xboole_0(A,k1_xboole_0) = A,
file('theBenchmark.p',t1_boole) ).
fof(t3_relset_2,axiom,
! [A,B] : k3_pua2mss1(k2_xboole_0(A,B)) = k2_xboole_0(k3_pua2mss1(A),k3_pua2mss1(B)),
file('theBenchmark.p',t3_relset_2) ).
fof(t26_relset_2,conjecture,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(A))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(A))
=> ! [E] :
( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> ( k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,E),k3_pua2mss1(C)) = k1_xboole_0
=> k8_relset_2(A,B,k4_subset_1(A,C,D),E) = k8_relset_2(A,B,D,E) ) ) ) ),
file('theBenchmark.p',t26_relset_2) ).
fof(t26_relset_2_neg,negated_conjecture,
~ ! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(A))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(A))
=> ! [E] :
( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> ( k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,E),k3_pua2mss1(C)) = k1_xboole_0
=> k8_relset_2(A,B,k4_subset_1(A,C,D),E) = k8_relset_2(A,B,D,E) ) ) ) ),
inference(assume_negation,[status(cth)],[t26_relset_2]) ).
cnf(c_63,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_64,plain,
( ~ m1_relset_1(A,B,C)
| m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_66,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_67,plain,
( m2_relset_1(k6_relset_2(C,B,A),k1_zfmisc_1(B),k1_zfmisc_1(C))
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(clausify,[status(thm)],[dt_k6_relset_2]) ).
cnf(c_68,plain,
( ~ m1_relset_1(A,B,C)
| m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(resolve,[status(thm)],[c_66,c_64]) ).
cnf(c_69,plain,
( m1_relset_1(k6_relset_2(C,B,A),k1_zfmisc_1(B),k1_zfmisc_1(C))
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(resolve,[status(thm)],[c_67,c_63]) ).
cnf(c_80,plain,
( ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,A)))
| m1_subset_1(k6_relset_2(A,B,C),k1_zfmisc_1(k2_zfmisc_1(k1_zfmisc_1(B),k1_zfmisc_1(A)))) ),
inference(resolve,[status(thm)],[c_68,c_69]) ).
fof(nnf_59,plain,
? [A,B,C] :
( ? [D] :
( ? [E] :
( k8_relset_2(A,B,k4_subset_1(A,C,D),E) != k8_relset_2(A,B,D,E)
& k4_relset_2(k1_zfmisc_1(A),B,k6_relset_2(B,A,E),k3_pua2mss1(C)) = k1_xboole_0
& m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B))) )
& m1_subset_1(D,k1_zfmisc_1(A)) )
& m1_subset_1(C,k1_zfmisc_1(A)) ),
inference(fof_nnf,[status(thm)],[t26_relset_2_neg]) ).
fof(sk_t26_relset_2_neg,plain,
( k8_relset_2(sK0,sK1,k4_subset_1(sK0,sK2,sK3),sK4) != k8_relset_2(sK0,sK1,sK3,sK4)
& k4_relset_2(k1_zfmisc_1(sK0),sK1,k6_relset_2(sK1,sK0,sK4),k3_pua2mss1(sK2)) = k1_xboole_0
& m1_subset_1(sK4,k1_zfmisc_1(k2_zfmisc_1(sK0,sK1)))
& m1_subset_1(sK3,k1_zfmisc_1(sK0))
& m1_subset_1(sK2,k1_zfmisc_1(sK0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK0,sK3,sK4,sK1]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2),skolemize(D,sK3),skolemize(E,sK4)],[nnf_59]) ).
cnf(c_83,negated_conjecture,
k8_relset_2(sK0,sK1,k4_subset_1(sK0,sK2,sK3),sK4) != k8_relset_2(sK0,sK1,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_t26_relset_2_neg]) ).
cnf(c_84,negated_conjecture,
k4_relset_2(k1_zfmisc_1(sK0),sK1,k6_relset_2(sK1,sK0,sK4),k3_pua2mss1(sK2)) = k1_xboole_0,
inference(split_conjunct,[status(thm)],[sk_t26_relset_2_neg]) ).
cnf(c_85,negated_conjecture,
m1_subset_1(sK4,k1_zfmisc_1(k2_zfmisc_1(sK0,sK1))),
inference(split_conjunct,[status(thm)],[sk_t26_relset_2_neg]) ).
cnf(c_86,negated_conjecture,
m1_subset_1(sK3,k1_zfmisc_1(sK0)),
inference(split_conjunct,[status(thm)],[sk_t26_relset_2_neg]) ).
cnf(c_87,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(sK0)),
inference(split_conjunct,[status(thm)],[sk_t26_relset_2_neg]) ).
cnf(c_93,plain,
k2_xboole_0(k3_pua2mss1(A),k3_pua2mss1(B)) = k3_pua2mss1(k2_xboole_0(A,B)),
inference(clausify,[status(thm)],[t3_relset_2]) ).
cnf(c_94,plain,
k3_pua2mss1(k2_xboole_0(A,B)) = k2_xboole_0(k3_pua2mss1(A),k3_pua2mss1(B)),
inference(copy,[status(thm)],[c_93]) ).
cnf(c_97,plain,
k2_xboole_0(A,k1_xboole_0) = A,
inference(clausify,[status(thm)],[t1_boole]) ).
cnf(c_98,plain,
( k9_relat_1(A,k2_xboole_0(B,C)) = k2_xboole_0(k9_relat_1(A,B),k9_relat_1(A,C))
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[t153_relat_1]) ).
cnf(c_99,plain,
( k7_relset_2(B,D,A,C) = k8_relset_2(B,D,A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,D)))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[redefinition_k8_relset_2]) ).
cnf(c_100,plain,
( k8_relset_2(B,D,A,C) = k7_relset_2(B,D,A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,D)))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(copy,[status(thm)],[c_99]) ).
cnf(c_101,plain,
( k5_relset_2(B,A) = k6_relset_2(C,B,A)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(clausify,[status(thm)],[redefinition_k6_relset_2]) ).
cnf(c_102,plain,
( k6_relset_2(C,B,A) = k5_relset_2(B,A)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(copy,[status(thm)],[c_101]) ).
cnf(c_103,plain,
( k2_xboole_0(A,C) = k4_subset_1(B,A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[redefinition_k4_subset_1]) ).
cnf(c_104,plain,
( k4_subset_1(B,A,C) = k2_xboole_0(A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(copy,[status(thm)],[c_103]) ).
cnf(c_105,plain,
( k9_relat_1(A,D) = k4_relset_2(B,C,A,D)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,k1_zfmisc_1(C)))) ),
inference(clausify,[status(thm)],[redefinition_k4_relset_2]) ).
cnf(c_106,plain,
( k4_relset_2(B,C,A,D) = k9_relat_1(A,D)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,k1_zfmisc_1(C)))) ),
inference(copy,[status(thm)],[c_105]) ).
cnf(c_128,plain,
( v1_relat_1(k5_relset_2(B,A))
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[dt_k5_relset_2]) ).
cnf(c_129,plain,
( m1_subset_1(k4_subset_1(B,A,C),k1_zfmisc_1(B))
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[dt_k4_subset_1]) ).
cnf(c_131,plain,
( k8_setfam_1(D,k4_relset_2(k1_zfmisc_1(B),D,k6_relset_2(D,B,C),k3_pua2mss1(A))) = k7_relset_2(B,D,A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,D)))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[d4_relset_2]) ).
cnf(c_132,plain,
( k7_relset_2(B,D,A,C) = k8_setfam_1(D,k4_relset_2(k1_zfmisc_1(B),D,k6_relset_2(D,B,C),k3_pua2mss1(A)))
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(B,D)))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(copy,[status(thm)],[c_131]) ).
cnf(c_134,plain,
k2_xboole_0(A,B) = k2_xboole_0(B,A),
inference(clausify,[status(thm)],[commutativity_k2_xboole_0]) ).
cnf(c_135,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_146,plain,
m1_subset_1(k6_relset_2(sK1,sK0,sK4),k1_zfmisc_1(k2_zfmisc_1(k1_zfmisc_1(sK0),k1_zfmisc_1(sK1)))),
inference(resolve,[status(thm)],[c_85,c_80]) ).
cnf(c_173,plain,
( k8_relset_2(sK0,B,sK3,A) = k7_relset_2(sK0,B,sK3,A)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(sK0,B))) ),
inference(resolve,[status(thm)],[c_100,c_86]) ).
cnf(c_181,plain,
( k8_relset_2(sK0,sK1,A,sK4) = k7_relset_2(sK0,sK1,A,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(sK0)) ),
inference(resolve,[status(thm)],[c_100,c_85]) ).
cnf(c_186,plain,
k6_relset_2(sK1,sK0,sK4) = k5_relset_2(sK0,sK4),
inference(resolve,[status(thm)],[c_102,c_85]) ).
cnf(c_191,plain,
m1_subset_1(k5_relset_2(sK0,sK4),k1_zfmisc_1(k2_zfmisc_1(k1_zfmisc_1(sK0),k1_zfmisc_1(sK1)))),
inference(paramod,[status(thm)],[c_186,c_146]) ).
cnf(c_192,negated_conjecture,
k4_relset_2(k1_zfmisc_1(sK0),sK1,k5_relset_2(sK0,sK4),k3_pua2mss1(sK2)) = k1_xboole_0,
inference(paramod,[status(thm)],[c_186,c_84]) ).
cnf(c_197,plain,
( k4_subset_1(sK0,sK2,A) = k2_xboole_0(sK2,A)
| ~ m1_subset_1(A,k1_zfmisc_1(sK0)) ),
inference(resolve,[status(thm)],[c_104,c_87]) ).
cnf(c_297,plain,
( m1_subset_1(k4_subset_1(sK0,sK2,A),k1_zfmisc_1(sK0))
| ~ m1_subset_1(A,k1_zfmisc_1(sK0)) ),
inference(resolve,[status(thm)],[c_129,c_87]) ).
cnf(c_326,plain,
( k7_relset_2(sK0,B,sK3,A) = k8_setfam_1(B,k4_relset_2(k1_zfmisc_1(sK0),B,k6_relset_2(B,sK0,A),k3_pua2mss1(sK3)))
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(sK0,B))) ),
inference(resolve,[status(thm)],[c_132,c_86]) ).
cnf(c_59796,negated_conjecture,
( k7_relset_2(sK0,sK1,A,sK4) = k8_setfam_1(sK1,k4_relset_2(k1_zfmisc_1(sK0),sK1,k6_relset_2(sK1,sK0,sK4),k3_pua2mss1(A)))
| ~ m1_subset_1(A,k1_zfmisc_1(sK0)) ),
inference(resolve,[status(thm)],[c_132,c_85]) ).
cnf(c_336,negated_conjecture,
( k7_relset_2(sK0,sK1,A,sK4) = k8_setfam_1(sK1,k4_relset_2(k1_zfmisc_1(sK0),sK1,k5_relset_2(sK0,sK4),k3_pua2mss1(A)))
| ~ m1_subset_1(A,k1_zfmisc_1(sK0)) ),
inference(paramod,[status(thm)],[c_186,c_59796]) ).
cnf(c_352,plain,
k2_xboole_0(k1_xboole_0,A) = A,
inference(paramod,[status(thm)],[c_134,c_97]) ).
cnf(c_355,plain,
v1_relat_1(sK4),
inference(resolve,[status(thm)],[c_135,c_85]) ).
cnf(c_389,plain,
v1_relat_1(k5_relset_2(A,sK4)),
inference(resolve,[status(thm)],[c_355,c_128]) ).
cnf(c_458,plain,
k9_relat_1(k5_relset_2(A,sK4),k2_xboole_0(B,C)) = k2_xboole_0(k9_relat_1(k5_relset_2(A,sK4),B),k9_relat_1(k5_relset_2(A,sK4),C)),
inference(resolve,[status(thm)],[c_389,c_98]) ).
cnf(c_675,plain,
k8_relset_2(sK0,sK1,sK3,sK4) = k7_relset_2(sK0,sK1,sK3,sK4),
inference(resolve,[status(thm)],[c_173,c_85]) ).
cnf(c_680,negated_conjecture,
k8_relset_2(sK0,sK1,k4_subset_1(sK0,sK2,sK3),sK4) != k7_relset_2(sK0,sK1,sK3,sK4),
inference(paramod,[status(thm)],[c_675,c_83]) ).
cnf(c_1028,plain,
k4_relset_2(k1_zfmisc_1(sK0),sK1,k5_relset_2(sK0,sK4),A) = k9_relat_1(k5_relset_2(sK0,sK4),A),
inference(resolve,[status(thm)],[c_191,c_106]) ).
cnf(c_1038,negated_conjecture,
( k7_relset_2(sK0,sK1,A,sK4) = k8_setfam_1(sK1,k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(A)))
| ~ m1_subset_1(A,k1_zfmisc_1(sK0)) ),
inference(paramod,[status(thm)],[c_1028,c_336]) ).
cnf(c_1039,negated_conjecture,
k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(sK2)) = k1_xboole_0,
inference(paramod,[status(thm)],[c_1028,c_192]) ).
cnf(c_1224,plain,
k4_subset_1(sK0,sK2,sK3) = k2_xboole_0(sK2,sK3),
inference(resolve,[status(thm)],[c_197,c_86]) ).
cnf(c_1226,negated_conjecture,
k8_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) != k7_relset_2(sK0,sK1,sK3,sK4),
inference(paramod,[status(thm)],[c_1224,c_680]) ).
cnf(c_59797,negated_conjecture,
m1_subset_1(k4_subset_1(sK0,sK2,sK3),k1_zfmisc_1(sK0)),
inference(resolve,[status(thm)],[c_297,c_86]) ).
cnf(c_1283,negated_conjecture,
m1_subset_1(k2_xboole_0(sK2,sK3),k1_zfmisc_1(sK0)),
inference(paramod,[status(thm)],[c_1224,c_59797]) ).
cnf(c_1296,plain,
k8_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) = k7_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4),
inference(resolve,[status(thm)],[c_1283,c_181]) ).
cnf(c_1311,negated_conjecture,
k7_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) != k7_relset_2(sK0,sK1,sK3,sK4),
inference(paramod,[status(thm)],[c_1296,c_1226]) ).
cnf(c_59798,negated_conjecture,
k7_relset_2(sK0,sK1,sK3,sK4) = k8_setfam_1(sK1,k4_relset_2(k1_zfmisc_1(sK0),sK1,k6_relset_2(sK1,sK0,sK4),k3_pua2mss1(sK3))),
inference(resolve,[status(thm)],[c_326,c_85]) ).
cnf(c_59799,negated_conjecture,
k7_relset_2(sK0,sK1,sK3,sK4) = k8_setfam_1(sK1,k4_relset_2(k1_zfmisc_1(sK0),sK1,k5_relset_2(sK0,sK4),k3_pua2mss1(sK3))),
inference(paramod,[status(thm)],[c_186,c_59798]) ).
cnf(c_5846,negated_conjecture,
k7_relset_2(sK0,sK1,sK3,sK4) = k8_setfam_1(sK1,k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(sK3))),
inference(paramod,[status(thm)],[c_1028,c_59799]) ).
cnf(c_6052,negated_conjecture,
k7_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) != k8_setfam_1(sK1,k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(sK3))),
inference(paramod,[status(thm)],[c_5846,c_1311]) ).
cnf(c_59800,plain,
k7_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) = k8_setfam_1(sK1,k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(k2_xboole_0(sK2,sK3)))),
inference(resolve,[status(thm)],[c_1038,c_1283]) ).
cnf(c_59801,plain,
k7_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) = k8_setfam_1(sK1,k9_relat_1(k5_relset_2(sK0,sK4),k2_xboole_0(k3_pua2mss1(sK2),k3_pua2mss1(sK3)))),
inference(paramod,[status(thm)],[c_94,c_59800]) ).
cnf(c_59802,plain,
k7_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) = k8_setfam_1(sK1,k2_xboole_0(k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(sK2)),k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(sK3)))),
inference(paramod,[status(thm)],[c_458,c_59801]) ).
cnf(c_59803,plain,
k7_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) = k8_setfam_1(sK1,k2_xboole_0(k1_xboole_0,k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(sK3)))),
inference(paramod,[status(thm)],[c_1039,c_59802]) ).
cnf(c_59804,plain,
k7_relset_2(sK0,sK1,k2_xboole_0(sK2,sK3),sK4) = k8_setfam_1(sK1,k9_relat_1(k5_relset_2(sK0,sK4),k3_pua2mss1(sK3))),
inference(paramod,[status(thm)],[c_352,c_59803]) ).
cnf(c_59795,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_6052,c_59804]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU427+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Sat Sep 26 09:42:04 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/0.30 % Process 317070 was started by sandbox on n012,
% 0.03/0.30 % Sat Sep 26 09:42:04 2026
% 0.03/0.30 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.03/0.30
% 0.03/0.30 % From the command line: assign(max_seconds, 300).
% 29.74/4.73
% 29.74/4.73 % given #500 (W,wt=18): 3507 r2_hidden(k7_relset_2(A,B,A,k1_xboole_0),k1_zfmisc_1(B)). [resolve(3409,a,95,a),unit_del(a,124)].
% 29.74/4.73
% 29.74/4.73 % given #1000 (F,wt=26): 12723 -r2_hidden(k2_zfmisc_1(k1_zfmisc_1(A),k1_zfmisc_1(B)),f2(k1_zfmisc_1(A),k1_zfmisc_1(B))). [ur(159,b,889,a)].
% 29.74/4.73
% 29.74/4.73 % given #1500 (W,wt=23): 24063 v1_xboole_0(k7_relset_2(c4,k1_xboole_0,k2_xboole_0(c6,c7),k1_xboole_0)). [resolve(9073,a,526,b)].
% 29.74/4.73
% 29.74/4.73 % given #2000 (F,wt=25): 47511 -r2_hidden(k1_zfmisc_1(k2_zfmisc_1(c4,c5)),k2_xboole_0(c8,f4(c4,c5))). [resolve(21687,a,137,b)].
% 29.74/4.73
% 29.74/4.73 % SZS status Theorem for theBenchmark
% 29.74/4.73
% 29.74/4.73 % Proof 1 at 3.33 (+ 1.06) seconds.
% 29.74/4.73 % Length of proof is 73.
% 29.74/4.73 % Level of proof is 9.
% 29.74/4.73 % Maximum clause weight is 48.000.
% 29.74/4.73 % Given clauses 2230.
% 29.74/4.73
% 29.74/4.73 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------