%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SEU430+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Tue Jul 19 12:41:19 EDT 2022
% Result : Theorem 0.19s 0.55s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 15
% Syntax : Number of formulae : 122 ( 31 unt; 0 def)
% Number of atoms : 303 ( 124 equ)
% Maximal formula atoms : 20 ( 2 avg)
% Number of connectives : 313 ( 132 ~; 116 |; 38 &)
% ( 16 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 158 ( 6 sgn 78 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t30_relset_2,conjecture,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> ( k5_setfam_1(A,B) = k1_xboole_0
<=> ! [C] :
( r2_hidden(C,B)
=> C = k1_xboole_0 ) ) ) ).
fof(d1_xboole_0,axiom,
! [A] :
( A = k1_xboole_0
<=> ! [B] : ~ r2_hidden(B,A) ) ).
fof(d4_tarski,axiom,
! [A,B] :
( B = k3_tarski(A)
<=> ! [C] :
( r2_hidden(C,B)
<=> ? [D] :
( r2_hidden(C,D)
& r2_hidden(D,A) ) ) ) ).
fof(fc12_relat_1,axiom,
( v1_xboole_0(k1_xboole_0)
& v1_relat_1(k1_xboole_0)
& v3_relat_1(k1_xboole_0) ) ).
fof(redefinition_k5_setfam_1,axiom,
! [A,B] :
( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
=> k5_setfam_1(A,B) = k3_tarski(B) ) ).
fof(t7_boole,axiom,
! [A,B] :
~ ( r2_hidden(A,B)
& v1_xboole_0(B) ) ).
fof(subgoal_0,plain,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
& k5_setfam_1(A,B) = k1_xboole_0 )
=> ! [C] :
( r2_hidden(C,B)
=> C = k1_xboole_0 ) ),
inference(strip,[],[t30_relset_2]) ).
fof(subgoal_1,plain,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
& ! [C] :
( r2_hidden(C,B)
=> C = k1_xboole_0 ) )
=> k5_setfam_1(A,B) = k1_xboole_0 ),
inference(strip,[],[t30_relset_2]) ).
fof(negate_0_0,plain,
~ ! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
& k5_setfam_1(A,B) = k1_xboole_0 )
=> ! [C] :
( r2_hidden(C,B)
=> C = k1_xboole_0 ) ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [A] :
( A != k1_xboole_0
<=> ? [B] : r2_hidden(B,A) ),
inference(canonicalize,[],[d1_xboole_0]) ).
fof(normalize_0_1,plain,
! [A] :
( A != k1_xboole_0
<=> ? [B] : r2_hidden(B,A) ),
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [A,B] :
( ( A != k1_xboole_0
| ~ r2_hidden(B,A) )
& ( A = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(A),A) ) ),
inference(clausify,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
! [A] :
( A = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(A),A) ),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
? [A,B] :
( k5_setfam_1(A,B) = k1_xboole_0
& m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
& ? [C] :
( C != k1_xboole_0
& r2_hidden(C,B) ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_5,plain,
( k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4) = k1_xboole_0
& m1_subset_1(skolemFOFtoCNF_B_4,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_3)))
& ? [C] :
( C != k1_xboole_0
& r2_hidden(C,skolemFOFtoCNF_B_4) ) ),
inference(skolemize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
? [C] :
( C != k1_xboole_0
& r2_hidden(C,skolemFOFtoCNF_B_4) ),
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
( skolemFOFtoCNF_C_1 != k1_xboole_0
& r2_hidden(skolemFOFtoCNF_C_1,skolemFOFtoCNF_B_4) ),
inference(skolemize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
r2_hidden(skolemFOFtoCNF_C_1,skolemFOFtoCNF_B_4),
inference(conjunct,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [A,B] :
( B != k3_tarski(A)
<=> ? [C] :
( ~ r2_hidden(C,B)
<=> ? [D] :
( r2_hidden(C,D)
& r2_hidden(D,A) ) ) ),
inference(canonicalize,[],[d4_tarski]) ).
fof(normalize_0_10,plain,
! [A,B] :
( B != k3_tarski(A)
<=> ? [C] :
( ~ r2_hidden(C,B)
<=> ? [D] :
( r2_hidden(C,D)
& r2_hidden(D,A) ) ) ),
inference(specialize,[],[normalize_0_9]) ).
fof(normalize_0_11,plain,
! [A,B,C,D] :
( ( B != k3_tarski(A)
| ~ r2_hidden(C,B)
| r2_hidden(C,skolemFOFtoCNF_D_1(A,C)) )
& ( B != k3_tarski(A)
| ~ r2_hidden(C,B)
| r2_hidden(skolemFOFtoCNF_D_1(A,C),A) )
& ( B = k3_tarski(A)
| r2_hidden(skolemFOFtoCNF_C(A,B),B)
| r2_hidden(skolemFOFtoCNF_C(A,B),skolemFOFtoCNF_D(A,B)) )
& ( B = k3_tarski(A)
| r2_hidden(skolemFOFtoCNF_C(A,B),B)
| r2_hidden(skolemFOFtoCNF_D(A,B),A) )
& ( B != k3_tarski(A)
| ~ r2_hidden(C,D)
| ~ r2_hidden(D,A)
| r2_hidden(C,B) )
& ( ~ r2_hidden(D,A)
| ~ r2_hidden(skolemFOFtoCNF_C(A,B),B)
| ~ r2_hidden(skolemFOFtoCNF_C(A,B),D)
| B = k3_tarski(A) ) ),
inference(clausify,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [A,B,C,D] :
( B != k3_tarski(A)
| ~ r2_hidden(C,D)
| ~ r2_hidden(D,A)
| r2_hidden(C,B) ),
inference(conjunct,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
m1_subset_1(skolemFOFtoCNF_B_4,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_3))),
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_14,plain,
! [A,B] :
( ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
| k5_setfam_1(A,B) = k3_tarski(B) ),
inference(canonicalize,[],[redefinition_k5_setfam_1]) ).
fof(normalize_0_15,plain,
! [A,B] :
( ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
| k5_setfam_1(A,B) = k3_tarski(B) ),
inference(specialize,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4) = k1_xboole_0,
inference(conjunct,[],[normalize_0_5]) ).
fof(normalize_0_17,plain,
! [A,B] :
( A != k1_xboole_0
| ~ r2_hidden(B,A) ),
inference(conjunct,[],[normalize_0_2]) ).
fof(normalize_0_18,plain,
skolemFOFtoCNF_C_1 != k1_xboole_0,
inference(conjunct,[],[normalize_0_7]) ).
cnf(refute_0_0,plain,
( A = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(A),A) ),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_1,plain,
( skolemFOFtoCNF_C_1 = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(skolemFOFtoCNF_C_1),skolemFOFtoCNF_C_1) ),
inference(subst,[],[refute_0_0:[bind(A,$fot(skolemFOFtoCNF_C_1))]]) ).
cnf(refute_0_2,plain,
r2_hidden(skolemFOFtoCNF_C_1,skolemFOFtoCNF_B_4),
inference(canonicalize,[],[normalize_0_8]) ).
cnf(refute_0_3,plain,
( B != k3_tarski(A)
| ~ r2_hidden(C,D)
| ~ r2_hidden(D,A)
| r2_hidden(C,B) ),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_4,plain,
( k3_tarski(A) != k3_tarski(A)
| ~ r2_hidden(C,D)
| ~ r2_hidden(D,A)
| r2_hidden(C,k3_tarski(A)) ),
inference(subst,[],[refute_0_3:[bind(B,$fot(k3_tarski(A)))]]) ).
cnf(refute_0_5,plain,
k3_tarski(A) = k3_tarski(A),
introduced(tautology,[refl,[$fot(k3_tarski(A))]]) ).
cnf(refute_0_6,plain,
( ~ r2_hidden(C,D)
| ~ r2_hidden(D,A)
| r2_hidden(C,k3_tarski(A)) ),
inference(resolve,[$cnf( $equal(k3_tarski(A),k3_tarski(A)) )],[refute_0_5,refute_0_4]) ).
cnf(refute_0_7,plain,
( ~ r2_hidden(X_286,skolemFOFtoCNF_C_1)
| ~ r2_hidden(skolemFOFtoCNF_C_1,skolemFOFtoCNF_B_4)
| r2_hidden(X_286,k3_tarski(skolemFOFtoCNF_B_4)) ),
inference(subst,[],[refute_0_6:[bind(A,$fot(skolemFOFtoCNF_B_4)),bind(C,$fot(X_286)),bind(D,$fot(skolemFOFtoCNF_C_1))]]) ).
cnf(refute_0_8,plain,
( ~ r2_hidden(X_286,skolemFOFtoCNF_C_1)
| r2_hidden(X_286,k3_tarski(skolemFOFtoCNF_B_4)) ),
inference(resolve,[$cnf( r2_hidden(skolemFOFtoCNF_C_1,skolemFOFtoCNF_B_4) )],[refute_0_2,refute_0_7]) ).
cnf(refute_0_9,plain,
m1_subset_1(skolemFOFtoCNF_B_4,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_3))),
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_10,plain,
( ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
| k5_setfam_1(A,B) = k3_tarski(B) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_11,plain,
( ~ m1_subset_1(skolemFOFtoCNF_B_4,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_3)))
| k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4) = k3_tarski(skolemFOFtoCNF_B_4) ),
inference(subst,[],[refute_0_10:[bind(A,$fot(skolemFOFtoCNF_A_3)),bind(B,$fot(skolemFOFtoCNF_B_4))]]) ).
cnf(refute_0_12,plain,
k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4) = k3_tarski(skolemFOFtoCNF_B_4),
inference(resolve,[$cnf( m1_subset_1(skolemFOFtoCNF_B_4,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_3))) )],[refute_0_9,refute_0_11]) ).
cnf(refute_0_13,plain,
k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4) = k1_xboole_0,
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_14,plain,
( k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4) != k1_xboole_0
| k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4) != k3_tarski(skolemFOFtoCNF_B_4)
| k1_xboole_0 = k3_tarski(skolemFOFtoCNF_B_4) ),
introduced(tautology,[equality,[$cnf( $equal(k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4),k3_tarski(skolemFOFtoCNF_B_4)) ),[0],$fot(k1_xboole_0)]]) ).
cnf(refute_0_15,plain,
( k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4) != k3_tarski(skolemFOFtoCNF_B_4)
| k1_xboole_0 = k3_tarski(skolemFOFtoCNF_B_4) ),
inference(resolve,[$cnf( $equal(k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4),k1_xboole_0) )],[refute_0_13,refute_0_14]) ).
cnf(refute_0_16,plain,
k1_xboole_0 = k3_tarski(skolemFOFtoCNF_B_4),
inference(resolve,[$cnf( $equal(k5_setfam_1(skolemFOFtoCNF_A_3,skolemFOFtoCNF_B_4),k3_tarski(skolemFOFtoCNF_B_4)) )],[refute_0_12,refute_0_15]) ).
cnf(refute_0_17,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_0_18,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_0_19,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_0_17,refute_0_18]) ).
cnf(refute_0_20,plain,
( k1_xboole_0 != k3_tarski(skolemFOFtoCNF_B_4)
| k3_tarski(skolemFOFtoCNF_B_4) = k1_xboole_0 ),
inference(subst,[],[refute_0_19:[bind(X,$fot(k1_xboole_0)),bind(Y,$fot(k3_tarski(skolemFOFtoCNF_B_4)))]]) ).
cnf(refute_0_21,plain,
k3_tarski(skolemFOFtoCNF_B_4) = k1_xboole_0,
inference(resolve,[$cnf( $equal(k1_xboole_0,k3_tarski(skolemFOFtoCNF_B_4)) )],[refute_0_16,refute_0_20]) ).
cnf(refute_0_22,plain,
( k3_tarski(skolemFOFtoCNF_B_4) != k1_xboole_0
| ~ r2_hidden(X_286,k3_tarski(skolemFOFtoCNF_B_4))
| r2_hidden(X_286,k1_xboole_0) ),
introduced(tautology,[equality,[$cnf( r2_hidden(X_286,k3_tarski(skolemFOFtoCNF_B_4)) ),[1],$fot(k1_xboole_0)]]) ).
cnf(refute_0_23,plain,
( ~ r2_hidden(X_286,k3_tarski(skolemFOFtoCNF_B_4))
| r2_hidden(X_286,k1_xboole_0) ),
inference(resolve,[$cnf( $equal(k3_tarski(skolemFOFtoCNF_B_4),k1_xboole_0) )],[refute_0_21,refute_0_22]) ).
cnf(refute_0_24,plain,
( ~ r2_hidden(X_286,skolemFOFtoCNF_C_1)
| r2_hidden(X_286,k1_xboole_0) ),
inference(resolve,[$cnf( r2_hidden(X_286,k3_tarski(skolemFOFtoCNF_B_4)) )],[refute_0_8,refute_0_23]) ).
cnf(refute_0_25,plain,
( A != k1_xboole_0
| ~ r2_hidden(B,A) ),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_26,plain,
( k1_xboole_0 != k1_xboole_0
| ~ r2_hidden(B,k1_xboole_0) ),
inference(subst,[],[refute_0_25:[bind(A,$fot(k1_xboole_0))]]) ).
cnf(refute_0_27,plain,
k1_xboole_0 = k1_xboole_0,
introduced(tautology,[refl,[$fot(k1_xboole_0)]]) ).
cnf(refute_0_28,plain,
~ r2_hidden(B,k1_xboole_0),
inference(resolve,[$cnf( $equal(k1_xboole_0,k1_xboole_0) )],[refute_0_27,refute_0_26]) ).
cnf(refute_0_29,plain,
~ r2_hidden(X_286,k1_xboole_0),
inference(subst,[],[refute_0_28:[bind(B,$fot(X_286))]]) ).
cnf(refute_0_30,plain,
~ r2_hidden(X_286,skolemFOFtoCNF_C_1),
inference(resolve,[$cnf( r2_hidden(X_286,k1_xboole_0) )],[refute_0_24,refute_0_29]) ).
cnf(refute_0_31,plain,
~ r2_hidden(skolemFOFtoCNF_B(skolemFOFtoCNF_C_1),skolemFOFtoCNF_C_1),
inference(subst,[],[refute_0_30:[bind(X_286,$fot(skolemFOFtoCNF_B(skolemFOFtoCNF_C_1)))]]) ).
cnf(refute_0_32,plain,
skolemFOFtoCNF_C_1 = k1_xboole_0,
inference(resolve,[$cnf( r2_hidden(skolemFOFtoCNF_B(skolemFOFtoCNF_C_1),skolemFOFtoCNF_C_1) )],[refute_0_1,refute_0_31]) ).
cnf(refute_0_33,plain,
skolemFOFtoCNF_C_1 != k1_xboole_0,
inference(canonicalize,[],[normalize_0_18]) ).
cnf(refute_0_34,plain,
$false,
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C_1,k1_xboole_0) )],[refute_0_32,refute_0_33]) ).
fof(negate_1_0,plain,
~ ! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
& ! [C] :
( r2_hidden(C,B)
=> C = k1_xboole_0 ) )
=> k5_setfam_1(A,B) = k1_xboole_0 ),
inference(negate,[],[subgoal_1]) ).
fof(normalize_1_0,plain,
? [A,B] :
( k5_setfam_1(A,B) != k1_xboole_0
& m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
& ! [C] :
( ~ r2_hidden(C,B)
| C = k1_xboole_0 ) ),
inference(canonicalize,[],[negate_1_0]) ).
fof(normalize_1_1,plain,
( k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) != k1_xboole_0
& m1_subset_1(skolemFOFtoCNF_B_5,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_4)))
& ! [C] :
( ~ r2_hidden(C,skolemFOFtoCNF_B_5)
| C = k1_xboole_0 ) ),
inference(skolemize,[],[normalize_1_0]) ).
fof(normalize_1_2,plain,
m1_subset_1(skolemFOFtoCNF_B_5,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_4))),
inference(conjunct,[],[normalize_1_1]) ).
fof(normalize_1_3,plain,
! [A,B] :
( ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
| k5_setfam_1(A,B) = k3_tarski(B) ),
inference(canonicalize,[],[redefinition_k5_setfam_1]) ).
fof(normalize_1_4,plain,
! [A,B] :
( ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
| k5_setfam_1(A,B) = k3_tarski(B) ),
inference(specialize,[],[normalize_1_3]) ).
fof(normalize_1_5,plain,
! [A,B] :
( ~ r2_hidden(A,B)
| ~ v1_xboole_0(B) ),
inference(canonicalize,[],[t7_boole]) ).
fof(normalize_1_6,plain,
! [A,B] :
( ~ r2_hidden(A,B)
| ~ v1_xboole_0(B) ),
inference(specialize,[],[normalize_1_5]) ).
fof(normalize_1_7,plain,
! [A] :
( A != k1_xboole_0
<=> ? [B] : r2_hidden(B,A) ),
inference(canonicalize,[],[d1_xboole_0]) ).
fof(normalize_1_8,plain,
! [A] :
( A != k1_xboole_0
<=> ? [B] : r2_hidden(B,A) ),
inference(specialize,[],[normalize_1_7]) ).
fof(normalize_1_9,plain,
! [A,B] :
( ( A != k1_xboole_0
| ~ r2_hidden(B,A) )
& ( A = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(A),A) ) ),
inference(clausify,[],[normalize_1_8]) ).
fof(normalize_1_10,plain,
! [A] :
( A = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(A),A) ),
inference(conjunct,[],[normalize_1_9]) ).
fof(normalize_1_11,plain,
! [A,B] :
( B != k3_tarski(A)
<=> ? [C] :
( ~ r2_hidden(C,B)
<=> ? [D] :
( r2_hidden(C,D)
& r2_hidden(D,A) ) ) ),
inference(canonicalize,[],[d4_tarski]) ).
fof(normalize_1_12,plain,
! [A,B] :
( B != k3_tarski(A)
<=> ? [C] :
( ~ r2_hidden(C,B)
<=> ? [D] :
( r2_hidden(C,D)
& r2_hidden(D,A) ) ) ),
inference(specialize,[],[normalize_1_11]) ).
fof(normalize_1_13,plain,
! [A,B,C,D] :
( ( B != k3_tarski(A)
| ~ r2_hidden(C,B)
| r2_hidden(C,skolemFOFtoCNF_D_1(A,C)) )
& ( B != k3_tarski(A)
| ~ r2_hidden(C,B)
| r2_hidden(skolemFOFtoCNF_D_1(A,C),A) )
& ( B = k3_tarski(A)
| r2_hidden(skolemFOFtoCNF_C(A,B),B)
| r2_hidden(skolemFOFtoCNF_C(A,B),skolemFOFtoCNF_D(A,B)) )
& ( B = k3_tarski(A)
| r2_hidden(skolemFOFtoCNF_C(A,B),B)
| r2_hidden(skolemFOFtoCNF_D(A,B),A) )
& ( B != k3_tarski(A)
| ~ r2_hidden(C,D)
| ~ r2_hidden(D,A)
| r2_hidden(C,B) )
& ( ~ r2_hidden(D,A)
| ~ r2_hidden(skolemFOFtoCNF_C(A,B),B)
| ~ r2_hidden(skolemFOFtoCNF_C(A,B),D)
| B = k3_tarski(A) ) ),
inference(clausify,[],[normalize_1_12]) ).
fof(normalize_1_14,plain,
! [A,B,C] :
( B != k3_tarski(A)
| ~ r2_hidden(C,B)
| r2_hidden(C,skolemFOFtoCNF_D_1(A,C)) ),
inference(conjunct,[],[normalize_1_13]) ).
fof(normalize_1_15,plain,
! [C] :
( ~ r2_hidden(C,skolemFOFtoCNF_B_5)
| C = k1_xboole_0 ),
inference(conjunct,[],[normalize_1_1]) ).
fof(normalize_1_16,plain,
! [C] :
( ~ r2_hidden(C,skolemFOFtoCNF_B_5)
| C = k1_xboole_0 ),
inference(specialize,[],[normalize_1_15]) ).
fof(normalize_1_17,plain,
! [A,B,C] :
( B != k3_tarski(A)
| ~ r2_hidden(C,B)
| r2_hidden(skolemFOFtoCNF_D_1(A,C),A) ),
inference(conjunct,[],[normalize_1_13]) ).
fof(normalize_1_18,plain,
( v1_relat_1(k1_xboole_0)
& v1_xboole_0(k1_xboole_0)
& v3_relat_1(k1_xboole_0) ),
inference(canonicalize,[],[fc12_relat_1]) ).
fof(normalize_1_19,plain,
v1_xboole_0(k1_xboole_0),
inference(conjunct,[],[normalize_1_18]) ).
fof(normalize_1_20,plain,
k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) != k1_xboole_0,
inference(conjunct,[],[normalize_1_1]) ).
cnf(refute_1_0,plain,
m1_subset_1(skolemFOFtoCNF_B_5,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_4))),
inference(canonicalize,[],[normalize_1_2]) ).
cnf(refute_1_1,plain,
( ~ m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A)))
| k5_setfam_1(A,B) = k3_tarski(B) ),
inference(canonicalize,[],[normalize_1_4]) ).
cnf(refute_1_2,plain,
( ~ m1_subset_1(skolemFOFtoCNF_B_5,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_4)))
| k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) = k3_tarski(skolemFOFtoCNF_B_5) ),
inference(subst,[],[refute_1_1:[bind(A,$fot(skolemFOFtoCNF_A_4)),bind(B,$fot(skolemFOFtoCNF_B_5))]]) ).
cnf(refute_1_3,plain,
k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) = k3_tarski(skolemFOFtoCNF_B_5),
inference(resolve,[$cnf( m1_subset_1(skolemFOFtoCNF_B_5,k1_zfmisc_1(k1_zfmisc_1(skolemFOFtoCNF_A_4))) )],[refute_1_0,refute_1_2]) ).
cnf(refute_1_4,plain,
( ~ r2_hidden(A,B)
| ~ v1_xboole_0(B) ),
inference(canonicalize,[],[normalize_1_6]) ).
cnf(refute_1_5,plain,
( ~ r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_346)),skolemFOFtoCNF_D_1(X_346,skolemFOFtoCNF_B(k3_tarski(X_346))))
| ~ v1_xboole_0(skolemFOFtoCNF_D_1(X_346,skolemFOFtoCNF_B(k3_tarski(X_346)))) ),
inference(subst,[],[refute_1_4:[bind(A,$fot(skolemFOFtoCNF_B(k3_tarski(X_346)))),bind(B,$fot(skolemFOFtoCNF_D_1(X_346,skolemFOFtoCNF_B(k3_tarski(X_346)))))]]) ).
cnf(refute_1_6,plain,
( A = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(A),A) ),
inference(canonicalize,[],[normalize_1_10]) ).
cnf(refute_1_7,plain,
( k3_tarski(X_344) = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_344)),k3_tarski(X_344)) ),
inference(subst,[],[refute_1_6:[bind(A,$fot(k3_tarski(X_344)))]]) ).
cnf(refute_1_8,plain,
( B != k3_tarski(A)
| ~ r2_hidden(C,B)
| r2_hidden(C,skolemFOFtoCNF_D_1(A,C)) ),
inference(canonicalize,[],[normalize_1_14]) ).
cnf(refute_1_9,plain,
( k3_tarski(A) != k3_tarski(A)
| ~ r2_hidden(C,k3_tarski(A))
| r2_hidden(C,skolemFOFtoCNF_D_1(A,C)) ),
inference(subst,[],[refute_1_8:[bind(B,$fot(k3_tarski(A)))]]) ).
cnf(refute_1_10,plain,
k3_tarski(A) = k3_tarski(A),
introduced(tautology,[refl,[$fot(k3_tarski(A))]]) ).
cnf(refute_1_11,plain,
( ~ r2_hidden(C,k3_tarski(A))
| r2_hidden(C,skolemFOFtoCNF_D_1(A,C)) ),
inference(resolve,[$cnf( $equal(k3_tarski(A),k3_tarski(A)) )],[refute_1_10,refute_1_9]) ).
cnf(refute_1_12,plain,
( ~ r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_344)),k3_tarski(X_344))
| r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_344)),skolemFOFtoCNF_D_1(X_344,skolemFOFtoCNF_B(k3_tarski(X_344)))) ),
inference(subst,[],[refute_1_11:[bind(A,$fot(X_344)),bind(C,$fot(skolemFOFtoCNF_B(k3_tarski(X_344))))]]) ).
cnf(refute_1_13,plain,
( k3_tarski(X_344) = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_344)),skolemFOFtoCNF_D_1(X_344,skolemFOFtoCNF_B(k3_tarski(X_344)))) ),
inference(resolve,[$cnf( r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_344)),k3_tarski(X_344)) )],[refute_1_7,refute_1_12]) ).
cnf(refute_1_14,plain,
( k3_tarski(X_346) = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_346)),skolemFOFtoCNF_D_1(X_346,skolemFOFtoCNF_B(k3_tarski(X_346)))) ),
inference(subst,[],[refute_1_13:[bind(X_344,$fot(X_346))]]) ).
cnf(refute_1_15,plain,
( ~ v1_xboole_0(skolemFOFtoCNF_D_1(X_346,skolemFOFtoCNF_B(k3_tarski(X_346))))
| k3_tarski(X_346) = k1_xboole_0 ),
inference(resolve,[$cnf( r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_346)),skolemFOFtoCNF_D_1(X_346,skolemFOFtoCNF_B(k3_tarski(X_346)))) )],[refute_1_14,refute_1_5]) ).
cnf(refute_1_16,plain,
( ~ v1_xboole_0(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5))))
| k3_tarski(skolemFOFtoCNF_B_5) = k1_xboole_0 ),
inference(subst,[],[refute_1_15:[bind(X_346,$fot(skolemFOFtoCNF_B_5))]]) ).
cnf(refute_1_17,plain,
( ~ r2_hidden(C,skolemFOFtoCNF_B_5)
| C = k1_xboole_0 ),
inference(canonicalize,[],[normalize_1_16]) ).
cnf(refute_1_18,plain,
( ~ r2_hidden(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5))),skolemFOFtoCNF_B_5)
| skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5))) = k1_xboole_0 ),
inference(subst,[],[refute_1_17:[bind(C,$fot(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5)))))]]) ).
cnf(refute_1_19,plain,
( k3_tarski(X_349) = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_349)),k3_tarski(X_349)) ),
inference(subst,[],[refute_1_6:[bind(A,$fot(k3_tarski(X_349)))]]) ).
cnf(refute_1_20,plain,
( B != k3_tarski(A)
| ~ r2_hidden(C,B)
| r2_hidden(skolemFOFtoCNF_D_1(A,C),A) ),
inference(canonicalize,[],[normalize_1_17]) ).
cnf(refute_1_21,plain,
( k3_tarski(A) != k3_tarski(A)
| ~ r2_hidden(C,k3_tarski(A))
| r2_hidden(skolemFOFtoCNF_D_1(A,C),A) ),
inference(subst,[],[refute_1_20:[bind(B,$fot(k3_tarski(A)))]]) ).
cnf(refute_1_22,plain,
( ~ r2_hidden(C,k3_tarski(A))
| r2_hidden(skolemFOFtoCNF_D_1(A,C),A) ),
inference(resolve,[$cnf( $equal(k3_tarski(A),k3_tarski(A)) )],[refute_1_10,refute_1_21]) ).
cnf(refute_1_23,plain,
( ~ r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_349)),k3_tarski(X_349))
| r2_hidden(skolemFOFtoCNF_D_1(X_349,skolemFOFtoCNF_B(k3_tarski(X_349))),X_349) ),
inference(subst,[],[refute_1_22:[bind(A,$fot(X_349)),bind(C,$fot(skolemFOFtoCNF_B(k3_tarski(X_349))))]]) ).
cnf(refute_1_24,plain,
( k3_tarski(X_349) = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_D_1(X_349,skolemFOFtoCNF_B(k3_tarski(X_349))),X_349) ),
inference(resolve,[$cnf( r2_hidden(skolemFOFtoCNF_B(k3_tarski(X_349)),k3_tarski(X_349)) )],[refute_1_19,refute_1_23]) ).
cnf(refute_1_25,plain,
( k3_tarski(skolemFOFtoCNF_B_5) = k1_xboole_0
| r2_hidden(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5))),skolemFOFtoCNF_B_5) ),
inference(subst,[],[refute_1_24:[bind(X_349,$fot(skolemFOFtoCNF_B_5))]]) ).
cnf(refute_1_26,plain,
( k3_tarski(skolemFOFtoCNF_B_5) = k1_xboole_0
| skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5))) = k1_xboole_0 ),
inference(resolve,[$cnf( r2_hidden(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5))),skolemFOFtoCNF_B_5) )],[refute_1_25,refute_1_18]) ).
cnf(refute_1_27,plain,
( skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5))) != k1_xboole_0
| ~ v1_xboole_0(k1_xboole_0)
| v1_xboole_0(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5)))) ),
introduced(tautology,[equality,[$cnf( ~ v1_xboole_0(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5)))) ),[0],$fot(k1_xboole_0)]]) ).
cnf(refute_1_28,plain,
( ~ v1_xboole_0(k1_xboole_0)
| k3_tarski(skolemFOFtoCNF_B_5) = k1_xboole_0
| v1_xboole_0(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5)))) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5))),k1_xboole_0) )],[refute_1_26,refute_1_27]) ).
cnf(refute_1_29,plain,
( ~ v1_xboole_0(k1_xboole_0)
| k3_tarski(skolemFOFtoCNF_B_5) = k1_xboole_0 ),
inference(resolve,[$cnf( v1_xboole_0(skolemFOFtoCNF_D_1(skolemFOFtoCNF_B_5,skolemFOFtoCNF_B(k3_tarski(skolemFOFtoCNF_B_5)))) )],[refute_1_28,refute_1_16]) ).
cnf(refute_1_30,plain,
v1_xboole_0(k1_xboole_0),
inference(canonicalize,[],[normalize_1_19]) ).
cnf(refute_1_31,plain,
k3_tarski(skolemFOFtoCNF_B_5) = k1_xboole_0,
inference(resolve,[$cnf( v1_xboole_0(k1_xboole_0) )],[refute_1_30,refute_1_29]) ).
cnf(refute_1_32,plain,
( k3_tarski(skolemFOFtoCNF_B_5) != k1_xboole_0
| k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) != k3_tarski(skolemFOFtoCNF_B_5)
| k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) = k1_xboole_0 ),
introduced(tautology,[equality,[$cnf( $equal(k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5),k3_tarski(skolemFOFtoCNF_B_5)) ),[1],$fot(k1_xboole_0)]]) ).
cnf(refute_1_33,plain,
( k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) != k3_tarski(skolemFOFtoCNF_B_5)
| k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) = k1_xboole_0 ),
inference(resolve,[$cnf( $equal(k3_tarski(skolemFOFtoCNF_B_5),k1_xboole_0) )],[refute_1_31,refute_1_32]) ).
cnf(refute_1_34,plain,
k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) = k1_xboole_0,
inference(resolve,[$cnf( $equal(k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5),k3_tarski(skolemFOFtoCNF_B_5)) )],[refute_1_3,refute_1_33]) ).
cnf(refute_1_35,plain,
k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5) != k1_xboole_0,
inference(canonicalize,[],[normalize_1_20]) ).
cnf(refute_1_36,plain,
$false,
inference(resolve,[$cnf( $equal(k5_setfam_1(skolemFOFtoCNF_A_4,skolemFOFtoCNF_B_5),k1_xboole_0) )],[refute_1_34,refute_1_35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU430+1 : TPTP v8.1.0. Released v3.4.0.
% 0.12/0.13 % Command : metis --show proof --show saturation %s
% 0.13/0.34 % Computer : n007.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 20 12:35:30 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.55 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.55
% 0.19/0.55 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.19/0.56
%------------------------------------------------------------------------------