%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SEU448+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 : n003.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:24 AM UTC 2026
% Result : Theorem 36.97s 10.83s
% Output : CNFRefutation 36.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 15
% Syntax : Number of formulae : 97 ( 30 unt; 0 def)
% Number of atoms : 214 ( 16 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 189 ( 72 ~; 80 |; 8 &)
% ( 6 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-4 aty)
% Number of variables : 128 ( 7 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_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_k3_subset_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> m1_subset_1(k3_subset_1(A,B),k1_zfmisc_1(A)) ),
file('theBenchmark.p',dt_k3_subset_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_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_k3_subset_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> k3_subset_1(A,k3_subset_1(A,B)) = B ),
file('theBenchmark.p',involutiveness_k3_subset_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_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(symmetry_r1_xboole_0,axiom,
! [A,B] :
( r1_xboole_0(A,B)
=> r1_xboole_0(B,A) ),
file('theBenchmark.p',symmetry_r1_xboole_0) ).
fof(t43_subset_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(A))
=> ( r1_xboole_0(B,C)
<=> r1_tarski(B,k3_subset_1(A,C)) ) ) ),
file('theBenchmark.p',t43_subset_1) ).
fof(t44_subset_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(A))
=> ! [C] :
( m1_subset_1(C,k1_zfmisc_1(A))
=> ( r1_xboole_0(B,k3_subset_1(A,C))
<=> r1_tarski(B,C) ) ) ),
file('theBenchmark.p',t44_subset_1) ).
fof(t46_relset_2,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(A))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(B))
=> ! [E] :
( m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> ( r1_xboole_0(C,k9_relat_1(k4_relat_1(E),D))
<=> r1_xboole_0(D,k9_relat_1(E,C)) ) ) ) ),
file('theBenchmark.p',t46_relset_2) ).
fof(t62_relset_2,conjecture,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(A))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(B))
=> ! [E] :
( m2_relset_1(E,A,B)
=> ( r1_tarski(k10_relset_1(A,B,E,k3_subset_1(A,C)),k3_subset_1(B,D))
<=> r1_tarski(k10_relset_1(B,A,k6_relset_1(A,B,E),D),C) ) ) ) ),
file('theBenchmark.p',t62_relset_2) ).
fof(t62_relset_2_neg,negated_conjecture,
~ ! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(A))
=> ! [D] :
( m1_subset_1(D,k1_zfmisc_1(B))
=> ! [E] :
( m2_relset_1(E,A,B)
=> ( r1_tarski(k10_relset_1(A,B,E,k3_subset_1(A,C)),k3_subset_1(B,D))
<=> r1_tarski(k10_relset_1(B,A,k6_relset_1(A,B,E),D),C) ) ) ) ),
inference(assume_negation,[status(cth)],[t62_relset_2]) ).
cnf(c_49,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_50,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_52,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
fof(nnf_48,plain,
? [A,B,C] :
( ? [D] :
( ? [E] :
( ( ~ r1_tarski(k10_relset_1(B,A,k6_relset_1(A,B,E),D),C)
| ~ r1_tarski(k10_relset_1(A,B,E,k3_subset_1(A,C)),k3_subset_1(B,D)) )
& ( r1_tarski(k10_relset_1(B,A,k6_relset_1(A,B,E),D),C)
| r1_tarski(k10_relset_1(A,B,E,k3_subset_1(A,C)),k3_subset_1(B,D)) )
& m2_relset_1(E,A,B) )
& m1_subset_1(D,k1_zfmisc_1(B)) )
& m1_subset_1(C,k1_zfmisc_1(A)) ),
inference(fof_nnf,[status(thm)],[t62_relset_2_neg]) ).
fof(sk_t62_relset_2_neg,plain,
( ( ~ r1_tarski(k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),sK4),sK3)
| ~ r1_tarski(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4)) )
& ( r1_tarski(k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),sK4),sK3)
| r1_tarski(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4)) )
& m2_relset_1(sK0,sK1,sK2)
& m1_subset_1(sK4,k1_zfmisc_1(sK2))
& m1_subset_1(sK3,k1_zfmisc_1(sK1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK1,sK4,sK2,sK0]),skolemize(A,sK1),skolemize(B,sK2),skolemize(C,sK3),skolemize(D,sK4),skolemize(E,sK0)],[nnf_48]) ).
cnf(c_54,negated_conjecture,
m2_relset_1(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t62_relset_2_neg]) ).
cnf(c_57,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_58,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_59,plain,
( m1_subset_1(k3_subset_1(B,A),k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[dt_k3_subset_1]) ).
cnf(c_70,plain,
( k3_subset_1(B,k3_subset_1(B,A)) = A
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[involutiveness_k3_subset_1]) ).
cnf(c_71,plain,
( k4_relat_1(k4_relat_1(A)) = A
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[involutiveness_k4_relat_1]) ).
cnf(c_82,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_83,plain,
( k10_relset_1(B,C,A,D) = k9_relat_1(A,D)
| ~ m1_relset_1(A,B,C) ),
inference(copy,[status(thm)],[c_82]) ).
cnf(c_84,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_85,plain,
( k6_relset_1(B,C,A) = k4_relat_1(A)
| ~ m1_relset_1(A,B,C) ),
inference(copy,[status(thm)],[c_84]) ).
cnf(c_87,plain,
( r1_xboole_0(B,A)
| ~ r1_xboole_0(A,B) ),
inference(clausify,[status(thm)],[symmetry_r1_xboole_0]) ).
cnf(c_93,plain,
( ~ r1_tarski(A,k3_subset_1(B,C))
| r1_xboole_0(A,C)
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t43_subset_1]) ).
cnf(c_94,plain,
( r1_tarski(A,C)
| ~ r1_xboole_0(A,k3_subset_1(B,C))
| ~ m1_subset_1(C,k1_zfmisc_1(B))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t44_subset_1]) ).
cnf(c_97,plain,
( ~ r1_xboole_0(C,k9_relat_1(E,A))
| r1_xboole_0(A,k9_relat_1(k4_relat_1(E),C))
| ~ m1_subset_1(E,k1_zfmisc_1(k2_zfmisc_1(B,D)))
| ~ m1_subset_1(C,k1_zfmisc_1(D))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t46_relset_2]) ).
cnf(c_103,negated_conjecture,
m1_subset_1(sK3,k1_zfmisc_1(sK1)),
inference(split_conjunct,[status(thm)],[sk_t62_relset_2_neg]) ).
cnf(c_104,negated_conjecture,
m1_subset_1(sK4,k1_zfmisc_1(sK2)),
inference(split_conjunct,[status(thm)],[sk_t62_relset_2_neg]) ).
cnf(c_105,negated_conjecture,
( r1_tarski(k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),sK4),sK3)
| r1_tarski(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4)) ),
inference(split_conjunct,[status(thm)],[sk_t62_relset_2_neg]) ).
cnf(c_106,negated_conjecture,
( ~ r1_tarski(k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),sK4),sK3)
| ~ r1_tarski(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4)) ),
inference(split_conjunct,[status(thm)],[sk_t62_relset_2_neg]) ).
cnf(c_107,plain,
( ~ m1_relset_1(C,A,B)
| m1_subset_1(k6_relset_1(A,B,C),k1_zfmisc_1(k2_zfmisc_1(B,A))) ),
inference(resolve,[status(thm)],[c_49,c_50]) ).
cnf(c_110,plain,
( ~ m1_relset_1(C,A,B)
| m1_relset_1(k6_relset_1(A,B,C),B,A) ),
inference(resolve,[status(thm)],[c_52,c_50]) ).
cnf(c_112,negated_conjecture,
m1_relset_1(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_54,c_52]) ).
cnf(c_113,negated_conjecture,
m1_subset_1(sK0,k1_zfmisc_1(k2_zfmisc_1(sK1,sK2))),
inference(resolve,[status(thm)],[c_54,c_49]) ).
cnf(c_185,plain,
k3_subset_1(sK1,k3_subset_1(sK1,sK3)) = sK3,
inference(resolve,[status(thm)],[c_103,c_70]) ).
cnf(c_186,plain,
m1_subset_1(k3_subset_1(sK1,sK3),k1_zfmisc_1(sK1)),
inference(resolve,[status(thm)],[c_103,c_59]) ).
cnf(c_190,plain,
k3_subset_1(sK2,k3_subset_1(sK2,sK4)) = sK4,
inference(resolve,[status(thm)],[c_104,c_70]) ).
cnf(c_191,plain,
m1_subset_1(k3_subset_1(sK2,sK4),k1_zfmisc_1(sK2)),
inference(resolve,[status(thm)],[c_104,c_59]) ).
cnf(c_12988,negated_conjecture,
( r1_xboole_0(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),sK4)
| ~ m1_subset_1(sK4,k1_zfmisc_1(sK2))
| ~ m1_subset_1(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),k1_zfmisc_1(sK2))
| r1_tarski(k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),sK4),sK3) ),
inference(resolve,[status(thm)],[c_105,c_93]) ).
cnf(c_194,negated_conjecture,
( r1_xboole_0(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),sK4)
| ~ m1_subset_1(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),k1_zfmisc_1(sK2))
| r1_tarski(k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),sK4),sK3) ),
inference(resolve,[status(thm)],[c_104,c_12988]) ).
cnf(c_214,plain,
k6_relset_1(sK1,sK2,sK0) = k4_relat_1(sK0),
inference(resolve,[status(thm)],[c_112,c_85]) ).
cnf(c_215,plain,
k10_relset_1(sK1,sK2,sK0,A) = k9_relat_1(sK0,A),
inference(resolve,[status(thm)],[c_112,c_83]) ).
cnf(c_12989,negated_conjecture,
m1_subset_1(k10_relset_1(sK1,sK2,sK0,A),k1_zfmisc_1(sK2)),
inference(resolve,[status(thm)],[c_112,c_58]) ).
cnf(c_217,negated_conjecture,
m1_subset_1(k9_relat_1(sK0,A),k1_zfmisc_1(sK2)),
inference(paramod,[status(thm)],[c_215,c_12989]) ).
cnf(c_12990,negated_conjecture,
m1_relset_1(k6_relset_1(sK1,sK2,sK0),sK2,sK1),
inference(resolve,[status(thm)],[c_110,c_112]) ).
cnf(c_218,negated_conjecture,
m1_relset_1(k4_relat_1(sK0),sK2,sK1),
inference(paramod,[status(thm)],[c_214,c_12990]) ).
cnf(c_12991,negated_conjecture,
m1_subset_1(k6_relset_1(sK1,sK2,sK0),k1_zfmisc_1(k2_zfmisc_1(sK2,sK1))),
inference(resolve,[status(thm)],[c_107,c_112]) ).
cnf(c_219,negated_conjecture,
m1_subset_1(k4_relat_1(sK0),k1_zfmisc_1(k2_zfmisc_1(sK2,sK1))),
inference(paramod,[status(thm)],[c_214,c_12991]) ).
cnf(c_12992,negated_conjecture,
( r1_xboole_0(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),sK4)
| ~ m1_subset_1(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),k1_zfmisc_1(sK2))
| r1_tarski(k10_relset_1(sK2,sK1,k4_relat_1(sK0),sK4),sK3) ),
inference(paramod,[status(thm)],[c_214,c_194]) ).
cnf(c_12993,negated_conjecture,
( r1_xboole_0(k10_relset_1(sK1,sK2,sK0,k3_subset_1(sK1,sK3)),sK4)
| ~ m1_subset_1(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),k1_zfmisc_1(sK2))
| r1_tarski(k10_relset_1(sK2,sK1,k4_relat_1(sK0),sK4),sK3) ),
inference(paramod,[status(thm)],[c_215,c_12992]) ).
cnf(c_12994,negated_conjecture,
( r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4)
| ~ m1_subset_1(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),k1_zfmisc_1(sK2))
| r1_tarski(k10_relset_1(sK2,sK1,k4_relat_1(sK0),sK4),sK3) ),
inference(paramod,[status(thm)],[c_215,c_12993]) ).
cnf(c_221,negated_conjecture,
( r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4)
| r1_tarski(k10_relset_1(sK2,sK1,k4_relat_1(sK0),sK4),sK3) ),
inference(resolve,[status(thm)],[c_217,c_12994]) ).
cnf(c_12995,negated_conjecture,
( ~ r1_tarski(k10_relset_1(sK2,sK1,k6_relset_1(sK1,sK2,sK0),sK4),sK3)
| ~ r1_tarski(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4)) ),
inference(paramod,[status(thm)],[c_215,c_106]) ).
cnf(c_223,negated_conjecture,
( ~ r1_tarski(k10_relset_1(sK2,sK1,k4_relat_1(sK0),sK4),sK3)
| ~ r1_tarski(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4)) ),
inference(paramod,[status(thm)],[c_214,c_12995]) ).
cnf(c_229,plain,
v1_relat_1(sK0),
inference(resolve,[status(thm)],[c_113,c_57]) ).
cnf(c_256,plain,
k4_relat_1(k4_relat_1(sK0)) = sK0,
inference(resolve,[status(thm)],[c_229,c_71]) ).
cnf(c_496,plain,
k10_relset_1(sK2,sK1,k4_relat_1(sK0),A) = k9_relat_1(k4_relat_1(sK0),A),
inference(resolve,[status(thm)],[c_218,c_83]) ).
cnf(c_12996,plain,
m1_subset_1(k10_relset_1(sK2,sK1,k4_relat_1(sK0),A),k1_zfmisc_1(sK1)),
inference(resolve,[status(thm)],[c_218,c_58]) ).
cnf(c_498,plain,
m1_subset_1(k9_relat_1(k4_relat_1(sK0),A),k1_zfmisc_1(sK1)),
inference(paramod,[status(thm)],[c_496,c_12996]) ).
cnf(c_500,negated_conjecture,
( ~ r1_tarski(k9_relat_1(k4_relat_1(sK0),sK4),sK3)
| ~ r1_tarski(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4)) ),
inference(paramod,[status(thm)],[c_496,c_223]) ).
cnf(c_502,negated_conjecture,
( r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4)
| r1_tarski(k9_relat_1(k4_relat_1(sK0),sK4),sK3) ),
inference(paramod,[status(thm)],[c_496,c_221]) ).
cnf(c_12997,plain,
( ~ r1_tarski(A,sK3)
| r1_xboole_0(A,k3_subset_1(sK1,sK3))
| ~ m1_subset_1(k3_subset_1(sK1,sK3),k1_zfmisc_1(sK1))
| ~ m1_subset_1(A,k1_zfmisc_1(sK1)) ),
inference(paramod,[status(thm)],[c_185,c_93]) ).
cnf(c_2127,plain,
( ~ r1_tarski(A,sK3)
| r1_xboole_0(A,k3_subset_1(sK1,sK3))
| ~ m1_subset_1(A,k1_zfmisc_1(sK1)) ),
inference(resolve,[status(thm)],[c_186,c_12997]) ).
cnf(c_12998,plain,
( r1_tarski(A,k3_subset_1(sK2,sK4))
| ~ r1_xboole_0(A,sK4)
| ~ m1_subset_1(k3_subset_1(sK2,sK4),k1_zfmisc_1(sK2))
| ~ m1_subset_1(A,k1_zfmisc_1(sK2)) ),
inference(paramod,[status(thm)],[c_190,c_94]) ).
cnf(c_2145,plain,
( r1_tarski(A,k3_subset_1(sK2,sK4))
| ~ r1_xboole_0(A,sK4)
| ~ m1_subset_1(A,k1_zfmisc_1(sK2)) ),
inference(resolve,[status(thm)],[c_191,c_12998]) ).
cnf(c_12999,plain,
( r1_xboole_0(k9_relat_1(k4_relat_1(sK0),sK4),k3_subset_1(sK1,sK3))
| ~ m1_subset_1(k9_relat_1(k4_relat_1(sK0),sK4),k1_zfmisc_1(sK1))
| r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4) ),
inference(resolve,[status(thm)],[c_502,c_2127]) ).
cnf(c_7094,plain,
( r1_xboole_0(k9_relat_1(k4_relat_1(sK0),sK4),k3_subset_1(sK1,sK3))
| r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4) ),
inference(resolve,[status(thm)],[c_498,c_12999]) ).
cnf(c_12398,plain,
( r1_xboole_0(k3_subset_1(sK1,sK3),k9_relat_1(k4_relat_1(sK0),sK4))
| r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4) ),
inference(resolve,[status(thm)],[c_7094,c_87]) ).
cnf(c_13000,negated_conjecture,
( ~ r1_xboole_0(A,k9_relat_1(C,sK4))
| r1_xboole_0(sK4,k9_relat_1(k4_relat_1(C),A))
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(sK2,B)))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(resolve,[status(thm)],[c_97,c_104]) ).
cnf(c_13001,negated_conjecture,
( ~ r1_xboole_0(k3_subset_1(sK1,sK3),k9_relat_1(A,sK4))
| r1_xboole_0(sK4,k9_relat_1(k4_relat_1(A),k3_subset_1(sK1,sK3)))
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(sK2,sK1))) ),
inference(resolve,[status(thm)],[c_13000,c_186]) ).
cnf(c_13002,negated_conjecture,
( ~ r1_xboole_0(k3_subset_1(sK1,sK3),k9_relat_1(k4_relat_1(sK0),sK4))
| r1_xboole_0(sK4,k9_relat_1(k4_relat_1(k4_relat_1(sK0)),k3_subset_1(sK1,sK3))) ),
inference(resolve,[status(thm)],[c_13001,c_219]) ).
cnf(c_13003,negated_conjecture,
( r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4)
| r1_xboole_0(sK4,k9_relat_1(k4_relat_1(k4_relat_1(sK0)),k3_subset_1(sK1,sK3))) ),
inference(resolve,[status(thm)],[c_13002,c_12398]) ).
cnf(c_12643,negated_conjecture,
( r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4)
| r1_xboole_0(sK4,k9_relat_1(sK0,k3_subset_1(sK1,sK3))) ),
inference(paramod,[status(thm)],[c_256,c_13003]) ).
cnf(c_13004,plain,
( r1_xboole_0(sK4,k9_relat_1(sK0,k3_subset_1(sK1,sK3)))
| r1_xboole_0(sK4,k9_relat_1(sK0,k3_subset_1(sK1,sK3))) ),
inference(resolve,[status(thm)],[c_12643,c_87]) ).
cnf(c_12648,plain,
r1_xboole_0(sK4,k9_relat_1(sK0,k3_subset_1(sK1,sK3))),
inference(copy,[status(thm)],[c_13004]) ).
cnf(c_12973,plain,
r1_xboole_0(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),sK4),
inference(resolve,[status(thm)],[c_12648,c_87]) ).
cnf(c_13005,plain,
( ~ r1_xboole_0(A,k9_relat_1(C,k3_subset_1(sK1,sK3)))
| r1_xboole_0(k3_subset_1(sK1,sK3),k9_relat_1(k4_relat_1(C),A))
| ~ m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(sK1,B)))
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(resolve,[status(thm)],[c_97,c_186]) ).
cnf(c_13006,negated_conjecture,
( ~ r1_xboole_0(sK4,k9_relat_1(A,k3_subset_1(sK1,sK3)))
| r1_xboole_0(k3_subset_1(sK1,sK3),k9_relat_1(k4_relat_1(A),sK4))
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(sK1,sK2))) ),
inference(resolve,[status(thm)],[c_13005,c_104]) ).
cnf(c_13007,negated_conjecture,
( ~ r1_xboole_0(sK4,k9_relat_1(sK0,k3_subset_1(sK1,sK3)))
| r1_xboole_0(k3_subset_1(sK1,sK3),k9_relat_1(k4_relat_1(sK0),sK4)) ),
inference(resolve,[status(thm)],[c_13006,c_113]) ).
cnf(c_12974,negated_conjecture,
r1_xboole_0(k3_subset_1(sK1,sK3),k9_relat_1(k4_relat_1(sK0),sK4)),
inference(resolve,[status(thm)],[c_13007,c_12648]) ).
cnf(c_13008,plain,
( r1_tarski(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4))
| ~ m1_subset_1(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),k1_zfmisc_1(sK2)) ),
inference(resolve,[status(thm)],[c_12973,c_2145]) ).
cnf(c_12976,plain,
r1_tarski(k9_relat_1(sK0,k3_subset_1(sK1,sK3)),k3_subset_1(sK2,sK4)),
inference(resolve,[status(thm)],[c_217,c_13008]) ).
cnf(c_12979,negated_conjecture,
~ r1_tarski(k9_relat_1(k4_relat_1(sK0),sK4),sK3),
inference(resolve,[status(thm)],[c_12976,c_500]) ).
cnf(c_12984,plain,
r1_xboole_0(k9_relat_1(k4_relat_1(sK0),sK4),k3_subset_1(sK1,sK3)),
inference(resolve,[status(thm)],[c_12974,c_87]) ).
cnf(c_13009,plain,
( r1_tarski(k9_relat_1(k4_relat_1(sK0),sK4),sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(sK1))
| ~ m1_subset_1(k9_relat_1(k4_relat_1(sK0),sK4),k1_zfmisc_1(sK1)) ),
inference(resolve,[status(thm)],[c_12984,c_94]) ).
cnf(c_13010,plain,
( r1_tarski(k9_relat_1(k4_relat_1(sK0),sK4),sK3)
| ~ m1_subset_1(sK3,k1_zfmisc_1(sK1)) ),
inference(resolve,[status(thm)],[c_498,c_13009]) ).
cnf(c_13011,negated_conjecture,
r1_tarski(k9_relat_1(k4_relat_1(sK0),sK4),sK3),
inference(resolve,[status(thm)],[c_103,c_13010]) ).
cnf(c_12987,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_12979,c_13011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU448+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/5.45 % Computer : n003.cluster.edu
% 0.19/5.45 % Model : x86_64 x86_64
% 0.19/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.45 % Memory : 8046.5625MB
% 0.19/5.45 % OS : Linux 6.8.0-71-generic
% 0.19/5.45 % CPULimit : 300
% 0.19/5.45 % WCLimit : 300
% 0.19/5.45 % DateTime : Sat Sep 26 10:01:29 UTC 2026
% 0.19/5.45 % CPUTime :
% 0.19/5.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/5.45 % Process 2649576 was started by sandbox on n003,
% 0.19/5.45 % Sat Sep 26 10:01:29 2026
% 0.19/5.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/5.47
% 0.19/5.47 % From the command line: assign(max_seconds, 300).
% 36.97/10.83
% 36.97/10.83 % given #500 (T,wt=24): 755 r1_xboole_0(k3_subset_1(A,f4(A)),f4(A)) | v1_xboole_0(A). [hyper(93,a,136,b,b,75,b,d,86,a),merge(c)].
% 36.97/10.83
% 36.97/10.83 % SZS status Theorem for theBenchmark
% 36.97/10.83
% 36.97/10.83 % Proof 1 at 4.39 (+ 0.89) seconds.
% 36.97/10.83 % Length of proof is 70.
% 36.97/10.83 % Level of proof is 14.
% 36.97/10.83 % Maximum clause weight is 44.000.
% 36.97/10.83 % Given clauses 986.
% 36.97/10.83
% 36.97/10.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------