%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SET889+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n027.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 03:38:08 EDT 2022
% Result : Theorem 0.59s 0.76s
% Output : CNFRefutation 0.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 23
% Syntax : Number of formulae : 114 ( 35 unt; 0 def)
% Number of atoms : 297 ( 195 equ)
% Maximal formula atoms : 20 ( 2 avg)
% Number of connectives : 298 ( 115 ~; 156 |; 12 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 5 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-3 aty)
% Number of variables : 184 ( 10 sgn 65 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_k2_tarski,axiom,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ).
fof(d1_zfmisc_1,axiom,
! [A,B] :
( B = powerset(A)
<=> ! [C] :
( in(C,B)
<=> subset(C,A) ) ) ).
fof(d2_tarski,axiom,
! [A,B,C] :
( C = unordered_pair(A,B)
<=> ! [D] :
( in(D,C)
<=> ( D = A
| D = B ) ) ) ).
fof(l4_zfmisc_1,axiom,
! [A,B] :
( subset(A,singleton(B))
<=> ( A = empty_set
| A = singleton(B) ) ) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : subset(A,A) ).
fof(t30_zfmisc_1,conjecture,
! [A] : powerset(singleton(A)) = unordered_pair(empty_set,singleton(A)) ).
fof(subgoal_0,plain,
! [A] : powerset(singleton(A)) = unordered_pair(empty_set,singleton(A)),
inference(strip,[],[t30_zfmisc_1]) ).
fof(negate_0_0,plain,
~ ! [A] : powerset(singleton(A)) = unordered_pair(empty_set,singleton(A)),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
? [A] : powerset(singleton(A)) != unordered_pair(empty_set,singleton(A)),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
powerset(singleton(skolemFOFtoCNF_A_2)) != unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2)),
inference(skolemize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [A,B] :
( B != powerset(A)
<=> ? [C] :
( ~ in(C,B)
<=> subset(C,A) ) ),
inference(canonicalize,[],[d1_zfmisc_1]) ).
fof(normalize_0_3,plain,
! [A,B] :
( B != powerset(A)
<=> ? [C] :
( ~ in(C,B)
<=> subset(C,A) ) ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [A,B,C] :
( ( B != powerset(A)
| ~ in(C,B)
| subset(C,A) )
& ( B != powerset(A)
| ~ subset(C,A)
| in(C,B) )
& ( ~ in(skolemFOFtoCNF_C(A,B),B)
| ~ subset(skolemFOFtoCNF_C(A,B),A)
| B = powerset(A) )
& ( B = powerset(A)
| in(skolemFOFtoCNF_C(A,B),B)
| subset(skolemFOFtoCNF_C(A,B),A) ) ),
inference(clausify,[],[normalize_0_3]) ).
fof(normalize_0_5,plain,
! [A,B] :
( ~ in(skolemFOFtoCNF_C(A,B),B)
| ~ subset(skolemFOFtoCNF_C(A,B),A)
| B = powerset(A) ),
inference(conjunct,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [A,B,C] :
( C != unordered_pair(A,B)
<=> ? [D] :
( ~ in(D,C)
<=> ( D = A
| D = B ) ) ),
inference(canonicalize,[],[d2_tarski]) ).
fof(normalize_0_7,plain,
! [A,B,C] :
( C != unordered_pair(A,B)
<=> ? [D] :
( ~ in(D,C)
<=> ( D = A
| D = B ) ) ),
inference(specialize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [A,B,C,D] :
( ( C != unordered_pair(A,B)
| D != A
| in(D,C) )
& ( C != unordered_pair(A,B)
| D != B
| in(D,C) )
& ( skolemFOFtoCNF_D(A,B,C) != A
| ~ in(skolemFOFtoCNF_D(A,B,C),C)
| C = unordered_pair(A,B) )
& ( skolemFOFtoCNF_D(A,B,C) != B
| ~ in(skolemFOFtoCNF_D(A,B,C),C)
| C = unordered_pair(A,B) )
& ( C != unordered_pair(A,B)
| ~ in(D,C)
| D = A
| D = B )
& ( C = unordered_pair(A,B)
| skolemFOFtoCNF_D(A,B,C) = A
| skolemFOFtoCNF_D(A,B,C) = B
| in(skolemFOFtoCNF_D(A,B,C),C) ) ),
inference(clausify,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
! [A,B,C,D] :
( C != unordered_pair(A,B)
| ~ in(D,C)
| D = A
| D = B ),
inference(conjunct,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
! [A,B] :
( ~ subset(A,singleton(B))
<=> ( A != empty_set
& A != singleton(B) ) ),
inference(canonicalize,[],[l4_zfmisc_1]) ).
fof(normalize_0_11,plain,
! [A,B] :
( ~ subset(A,singleton(B))
<=> ( A != empty_set
& A != singleton(B) ) ),
inference(specialize,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [A,B] :
( ( A != empty_set
| subset(A,singleton(B)) )
& ( A != singleton(B)
| subset(A,singleton(B)) )
& ( ~ subset(A,singleton(B))
| A = empty_set
| A = singleton(B) ) ),
inference(clausify,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [A,B] :
( ~ subset(A,singleton(B))
| A = empty_set
| A = singleton(B) ),
inference(conjunct,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [A,B] :
( B = powerset(A)
| in(skolemFOFtoCNF_C(A,B),B)
| subset(skolemFOFtoCNF_C(A,B),A) ),
inference(conjunct,[],[normalize_0_4]) ).
fof(normalize_0_15,plain,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
inference(canonicalize,[],[commutativity_k2_tarski]) ).
fof(normalize_0_16,plain,
! [A,B] : unordered_pair(A,B) = unordered_pair(B,A),
inference(specialize,[],[normalize_0_15]) ).
fof(normalize_0_17,plain,
! [A,B,C,D] :
( C != unordered_pair(A,B)
| D != B
| in(D,C) ),
inference(conjunct,[],[normalize_0_8]) ).
fof(normalize_0_18,plain,
! [A] : subset(A,A),
inference(canonicalize,[],[reflexivity_r1_tarski]) ).
fof(normalize_0_19,plain,
! [A] : subset(A,A),
inference(specialize,[],[normalize_0_18]) ).
fof(normalize_0_20,plain,
! [A,B,C,D] :
( C != unordered_pair(A,B)
| D != A
| in(D,C) ),
inference(conjunct,[],[normalize_0_8]) ).
fof(normalize_0_21,plain,
! [A,B] :
( A != empty_set
| subset(A,singleton(B)) ),
inference(conjunct,[],[normalize_0_12]) ).
cnf(refute_0_0,plain,
powerset(singleton(skolemFOFtoCNF_A_2)) != unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2)),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( ~ in(skolemFOFtoCNF_C(A,B),B)
| ~ subset(skolemFOFtoCNF_C(A,B),A)
| B = powerset(A) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_2,plain,
( ~ in(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),unordered_pair(empty_set,singleton(X_203)))
| ~ subset(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),singleton(X_203))
| unordered_pair(empty_set,singleton(X_203)) = powerset(singleton(X_203)) ),
inference(subst,[],[refute_0_1:[bind(A,$fot(singleton(X_203))),bind(B,$fot(unordered_pair(empty_set,singleton(X_203))))]]) ).
cnf(refute_0_3,plain,
( ~ in(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),unordered_pair(empty_set,singleton(X_95)))
| ~ subset(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),singleton(X_95))
| unordered_pair(empty_set,singleton(X_95)) = powerset(singleton(X_95)) ),
inference(subst,[],[refute_0_1:[bind(A,$fot(singleton(X_95))),bind(B,$fot(unordered_pair(empty_set,singleton(X_95))))]]) ).
cnf(refute_0_4,plain,
( C != unordered_pair(A,B)
| ~ in(D,C)
| D = A
| D = B ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_5,plain,
( unordered_pair(A,B) != unordered_pair(A,B)
| ~ in(D,unordered_pair(A,B))
| D = A
| D = B ),
inference(subst,[],[refute_0_4:[bind(C,$fot(unordered_pair(A,B)))]]) ).
cnf(refute_0_6,plain,
unordered_pair(A,B) = unordered_pair(A,B),
introduced(tautology,[refl,[$fot(unordered_pair(A,B))]]) ).
cnf(refute_0_7,plain,
( ~ in(D,unordered_pair(A,B))
| D = A
| D = B ),
inference(resolve,[$cnf( $equal(unordered_pair(A,B),unordered_pair(A,B)) )],[refute_0_6,refute_0_5]) ).
cnf(refute_0_8,plain,
( ~ in(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)),unordered_pair(A,B))
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)) = A
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)) = B ),
inference(subst,[],[refute_0_7:[bind(D,$fot(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B))))]]) ).
cnf(refute_0_9,plain,
( ~ subset(A,singleton(B))
| A = empty_set
| A = singleton(B) ),
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_10,plain,
( ~ subset(skolemFOFtoCNF_C(singleton(B),X_29),singleton(B))
| skolemFOFtoCNF_C(singleton(B),X_29) = empty_set
| skolemFOFtoCNF_C(singleton(B),X_29) = singleton(B) ),
inference(subst,[],[refute_0_9:[bind(A,$fot(skolemFOFtoCNF_C(singleton(B),X_29)))]]) ).
cnf(refute_0_11,plain,
( B = powerset(A)
| in(skolemFOFtoCNF_C(A,B),B)
| subset(skolemFOFtoCNF_C(A,B),A) ),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_12,plain,
( X_29 = powerset(singleton(B))
| in(skolemFOFtoCNF_C(singleton(B),X_29),X_29)
| subset(skolemFOFtoCNF_C(singleton(B),X_29),singleton(B)) ),
inference(subst,[],[refute_0_11:[bind(A,$fot(singleton(B))),bind(B,$fot(X_29))]]) ).
cnf(refute_0_13,plain,
( X_29 = powerset(singleton(B))
| skolemFOFtoCNF_C(singleton(B),X_29) = empty_set
| skolemFOFtoCNF_C(singleton(B),X_29) = singleton(B)
| in(skolemFOFtoCNF_C(singleton(B),X_29),X_29) ),
inference(resolve,[$cnf( subset(skolemFOFtoCNF_C(singleton(B),X_29),singleton(B)) )],[refute_0_12,refute_0_10]) ).
cnf(refute_0_14,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)) = empty_set
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)) = singleton(X_93)
| unordered_pair(A,B) = powerset(singleton(X_93))
| in(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)),unordered_pair(A,B)) ),
inference(subst,[],[refute_0_13:[bind(B,$fot(X_93)),bind(X_29,$fot(unordered_pair(A,B)))]]) ).
cnf(refute_0_15,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)) = A
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)) = B
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)) = empty_set
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)) = singleton(X_93)
| unordered_pair(A,B) = powerset(singleton(X_93)) ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(A,B)),unordered_pair(A,B)) )],[refute_0_14,refute_0_8]) ).
cnf(refute_0_16,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) = empty_set
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) = singleton(X_93)
| unordered_pair(singleton(X_93),empty_set) = powerset(singleton(X_93)) ),
inference(subst,[],[refute_0_15:[bind(A,$fot(singleton(X_93))),bind(B,$fot(empty_set))]]) ).
cnf(refute_0_17,plain,
unordered_pair(A,B) = unordered_pair(B,A),
inference(canonicalize,[],[normalize_0_16]) ).
cnf(refute_0_18,plain,
X = X,
introduced(tautology,[refl,[$fot(X)]]) ).
cnf(refute_0_19,plain,
( X != X
| X != Y
| Y = X ),
introduced(tautology,[equality,[$cnf( $equal(X,X) ),[0],$fot(Y)]]) ).
cnf(refute_0_20,plain,
( X != Y
| Y = X ),
inference(resolve,[$cnf( $equal(X,X) )],[refute_0_18,refute_0_19]) ).
cnf(refute_0_21,plain,
( unordered_pair(A,B) != unordered_pair(B,A)
| unordered_pair(B,A) = unordered_pair(A,B) ),
inference(subst,[],[refute_0_20:[bind(X,$fot(unordered_pair(A,B))),bind(Y,$fot(unordered_pair(B,A)))]]) ).
cnf(refute_0_22,plain,
unordered_pair(B,A) = unordered_pair(A,B),
inference(resolve,[$cnf( $equal(unordered_pair(A,B),unordered_pair(B,A)) )],[refute_0_17,refute_0_21]) ).
cnf(refute_0_23,plain,
unordered_pair(singleton(X_93),empty_set) = unordered_pair(empty_set,singleton(X_93)),
inference(subst,[],[refute_0_22:[bind(A,$fot(empty_set)),bind(B,$fot(singleton(X_93)))]]) ).
cnf(refute_0_24,plain,
skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) = skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),
introduced(tautology,[refl,[$fot(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)))]]) ).
cnf(refute_0_25,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) != skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set))
| unordered_pair(singleton(X_93),empty_set) != unordered_pair(empty_set,singleton(X_93))
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) = skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) ),
introduced(tautology,[equality,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set))) ),[1,1],$fot(unordered_pair(empty_set,singleton(X_93)))]]) ).
cnf(refute_0_26,plain,
( unordered_pair(singleton(X_93),empty_set) != unordered_pair(empty_set,singleton(X_93))
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) = skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set))) )],[refute_0_24,refute_0_25]) ).
cnf(refute_0_27,plain,
skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) = skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))),
inference(resolve,[$cnf( $equal(unordered_pair(singleton(X_93),empty_set),unordered_pair(empty_set,singleton(X_93))) )],[refute_0_23,refute_0_26]) ).
cnf(refute_0_28,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) != empty_set
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) != skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93)))
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = empty_set ),
introduced(tautology,[equality,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),empty_set) ),[0],$fot(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))))]]) ).
cnf(refute_0_29,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) != empty_set
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = empty_set ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93)))) )],[refute_0_27,refute_0_28]) ).
cnf(refute_0_30,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = empty_set
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) = singleton(X_93)
| unordered_pair(singleton(X_93),empty_set) = powerset(singleton(X_93)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),empty_set) )],[refute_0_16,refute_0_29]) ).
cnf(refute_0_31,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) != singleton(X_93)
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) != skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93)))
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = singleton(X_93) ),
introduced(tautology,[equality,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),singleton(X_93)) ),[0],$fot(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))))]]) ).
cnf(refute_0_32,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)) != singleton(X_93)
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = singleton(X_93) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93)))) )],[refute_0_27,refute_0_31]) ).
cnf(refute_0_33,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = empty_set
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = singleton(X_93)
| unordered_pair(singleton(X_93),empty_set) = powerset(singleton(X_93)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_93),unordered_pair(singleton(X_93),empty_set)),singleton(X_93)) )],[refute_0_30,refute_0_32]) ).
cnf(refute_0_34,plain,
( unordered_pair(singleton(X_93),empty_set) != powerset(singleton(X_93))
| unordered_pair(singleton(X_93),empty_set) != unordered_pair(empty_set,singleton(X_93))
| unordered_pair(empty_set,singleton(X_93)) = powerset(singleton(X_93)) ),
introduced(tautology,[equality,[$cnf( $equal(unordered_pair(singleton(X_93),empty_set),powerset(singleton(X_93))) ),[0],$fot(unordered_pair(empty_set,singleton(X_93)))]]) ).
cnf(refute_0_35,plain,
( unordered_pair(singleton(X_93),empty_set) != powerset(singleton(X_93))
| unordered_pair(empty_set,singleton(X_93)) = powerset(singleton(X_93)) ),
inference(resolve,[$cnf( $equal(unordered_pair(singleton(X_93),empty_set),unordered_pair(empty_set,singleton(X_93))) )],[refute_0_23,refute_0_34]) ).
cnf(refute_0_36,plain,
( skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = empty_set
| skolemFOFtoCNF_C(singleton(X_93),unordered_pair(empty_set,singleton(X_93))) = singleton(X_93)
| unordered_pair(empty_set,singleton(X_93)) = powerset(singleton(X_93)) ),
inference(resolve,[$cnf( $equal(unordered_pair(singleton(X_93),empty_set),powerset(singleton(X_93))) )],[refute_0_33,refute_0_35]) ).
cnf(refute_0_37,plain,
( skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))) = empty_set
| skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))) = singleton(X_95)
| unordered_pair(empty_set,singleton(X_95)) = powerset(singleton(X_95)) ),
inference(subst,[],[refute_0_36:[bind(X_93,$fot(X_95))]]) ).
cnf(refute_0_38,plain,
( skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))) != singleton(X_95)
| ~ in(singleton(X_95),unordered_pair(empty_set,singleton(X_95)))
| in(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),unordered_pair(empty_set,singleton(X_95))) ),
introduced(tautology,[equality,[$cnf( ~ in(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),unordered_pair(empty_set,singleton(X_95))) ),[0],$fot(singleton(X_95))]]) ).
cnf(refute_0_39,plain,
( ~ in(singleton(X_95),unordered_pair(empty_set,singleton(X_95)))
| skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))) = empty_set
| unordered_pair(empty_set,singleton(X_95)) = powerset(singleton(X_95))
| in(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),unordered_pair(empty_set,singleton(X_95))) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),singleton(X_95)) )],[refute_0_37,refute_0_38]) ).
cnf(refute_0_40,plain,
( ~ in(singleton(X_95),unordered_pair(empty_set,singleton(X_95)))
| ~ subset(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),singleton(X_95))
| skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))) = empty_set
| unordered_pair(empty_set,singleton(X_95)) = powerset(singleton(X_95)) ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),unordered_pair(empty_set,singleton(X_95))) )],[refute_0_39,refute_0_3]) ).
cnf(refute_0_41,plain,
( C != unordered_pair(A,B)
| D != B
| in(D,C) ),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_42,plain,
( B != B
| unordered_pair(A,B) != unordered_pair(A,B)
| in(B,unordered_pair(A,B)) ),
inference(subst,[],[refute_0_41:[bind(C,$fot(unordered_pair(A,B))),bind(D,$fot(B))]]) ).
cnf(refute_0_43,plain,
B = B,
introduced(tautology,[refl,[$fot(B)]]) ).
cnf(refute_0_44,plain,
( unordered_pair(A,B) != unordered_pair(A,B)
| in(B,unordered_pair(A,B)) ),
inference(resolve,[$cnf( $equal(B,B) )],[refute_0_43,refute_0_42]) ).
cnf(refute_0_45,plain,
in(B,unordered_pair(A,B)),
inference(resolve,[$cnf( $equal(unordered_pair(A,B),unordered_pair(A,B)) )],[refute_0_6,refute_0_44]) ).
cnf(refute_0_46,plain,
in(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),
inference(subst,[],[refute_0_45:[bind(A,$fot(empty_set)),bind(B,$fot(singleton(X_95)))]]) ).
cnf(refute_0_47,plain,
( ~ subset(skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))),singleton(X_95))
| skolemFOFtoCNF_C(singleton(X_95),unordered_pair(empty_set,singleton(X_95))) = empty_set
| unordered_pair(empty_set,singleton(X_95)) = powerset(singleton(X_95)) ),
inference(resolve,[$cnf( in(singleton(X_95),unordered_pair(empty_set,singleton(X_95))) )],[refute_0_46,refute_0_40]) ).
cnf(refute_0_48,plain,
( ~ subset(skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))),singleton(X_202))
| skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))) = empty_set
| unordered_pair(empty_set,singleton(X_202)) = powerset(singleton(X_202)) ),
inference(subst,[],[refute_0_47:[bind(X_95,$fot(X_202))]]) ).
cnf(refute_0_49,plain,
( skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))) = empty_set
| skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))) = singleton(X_202)
| unordered_pair(empty_set,singleton(X_202)) = powerset(singleton(X_202)) ),
inference(subst,[],[refute_0_36:[bind(X_93,$fot(X_202))]]) ).
cnf(refute_0_50,plain,
( skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))) != singleton(X_202)
| ~ subset(singleton(X_202),singleton(X_202))
| subset(skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))),singleton(X_202)) ),
introduced(tautology,[equality,[$cnf( ~ subset(skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))),singleton(X_202)) ),[0],$fot(singleton(X_202))]]) ).
cnf(refute_0_51,plain,
( ~ subset(singleton(X_202),singleton(X_202))
| skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))) = empty_set
| unordered_pair(empty_set,singleton(X_202)) = powerset(singleton(X_202))
| subset(skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))),singleton(X_202)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))),singleton(X_202)) )],[refute_0_49,refute_0_50]) ).
cnf(refute_0_52,plain,
( ~ subset(singleton(X_202),singleton(X_202))
| skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))) = empty_set
| unordered_pair(empty_set,singleton(X_202)) = powerset(singleton(X_202)) ),
inference(resolve,[$cnf( subset(skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))),singleton(X_202)) )],[refute_0_51,refute_0_48]) ).
cnf(refute_0_53,plain,
subset(A,A),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_54,plain,
subset(singleton(X_202),singleton(X_202)),
inference(subst,[],[refute_0_53:[bind(A,$fot(singleton(X_202)))]]) ).
cnf(refute_0_55,plain,
( skolemFOFtoCNF_C(singleton(X_202),unordered_pair(empty_set,singleton(X_202))) = empty_set
| unordered_pair(empty_set,singleton(X_202)) = powerset(singleton(X_202)) ),
inference(resolve,[$cnf( subset(singleton(X_202),singleton(X_202)) )],[refute_0_54,refute_0_52]) ).
cnf(refute_0_56,plain,
( skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))) = empty_set
| unordered_pair(empty_set,singleton(X_203)) = powerset(singleton(X_203)) ),
inference(subst,[],[refute_0_55:[bind(X_202,$fot(X_203))]]) ).
cnf(refute_0_57,plain,
( skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))) != empty_set
| ~ in(empty_set,unordered_pair(empty_set,singleton(X_203)))
| in(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),unordered_pair(empty_set,singleton(X_203))) ),
introduced(tautology,[equality,[$cnf( ~ in(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),unordered_pair(empty_set,singleton(X_203))) ),[0],$fot(empty_set)]]) ).
cnf(refute_0_58,plain,
( ~ in(empty_set,unordered_pair(empty_set,singleton(X_203)))
| unordered_pair(empty_set,singleton(X_203)) = powerset(singleton(X_203))
| in(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),unordered_pair(empty_set,singleton(X_203))) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),empty_set) )],[refute_0_56,refute_0_57]) ).
cnf(refute_0_59,plain,
( ~ in(empty_set,unordered_pair(empty_set,singleton(X_203)))
| ~ subset(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),singleton(X_203))
| unordered_pair(empty_set,singleton(X_203)) = powerset(singleton(X_203)) ),
inference(resolve,[$cnf( in(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),unordered_pair(empty_set,singleton(X_203))) )],[refute_0_58,refute_0_2]) ).
cnf(refute_0_60,plain,
( C != unordered_pair(A,B)
| D != A
| in(D,C) ),
inference(canonicalize,[],[normalize_0_20]) ).
cnf(refute_0_61,plain,
( A != A
| unordered_pair(A,B) != unordered_pair(A,B)
| in(A,unordered_pair(A,B)) ),
inference(subst,[],[refute_0_60:[bind(C,$fot(unordered_pair(A,B))),bind(D,$fot(A))]]) ).
cnf(refute_0_62,plain,
A = A,
introduced(tautology,[refl,[$fot(A)]]) ).
cnf(refute_0_63,plain,
( unordered_pair(A,B) != unordered_pair(A,B)
| in(A,unordered_pair(A,B)) ),
inference(resolve,[$cnf( $equal(A,A) )],[refute_0_62,refute_0_61]) ).
cnf(refute_0_64,plain,
in(A,unordered_pair(A,B)),
inference(resolve,[$cnf( $equal(unordered_pair(A,B),unordered_pair(A,B)) )],[refute_0_6,refute_0_63]) ).
cnf(refute_0_65,plain,
in(empty_set,unordered_pair(empty_set,singleton(X_203))),
inference(subst,[],[refute_0_64:[bind(A,$fot(empty_set)),bind(B,$fot(singleton(X_203)))]]) ).
cnf(refute_0_66,plain,
( ~ subset(skolemFOFtoCNF_C(singleton(X_203),unordered_pair(empty_set,singleton(X_203))),singleton(X_203))
| unordered_pair(empty_set,singleton(X_203)) = powerset(singleton(X_203)) ),
inference(resolve,[$cnf( in(empty_set,unordered_pair(empty_set,singleton(X_203))) )],[refute_0_65,refute_0_59]) ).
cnf(refute_0_67,plain,
( ~ subset(skolemFOFtoCNF_C(singleton(X_204),unordered_pair(empty_set,singleton(X_204))),singleton(X_204))
| unordered_pair(empty_set,singleton(X_204)) = powerset(singleton(X_204)) ),
inference(subst,[],[refute_0_66:[bind(X_203,$fot(X_204))]]) ).
cnf(refute_0_68,plain,
( skolemFOFtoCNF_C(singleton(X_204),unordered_pair(empty_set,singleton(X_204))) = empty_set
| unordered_pair(empty_set,singleton(X_204)) = powerset(singleton(X_204)) ),
inference(subst,[],[refute_0_55:[bind(X_202,$fot(X_204))]]) ).
cnf(refute_0_69,plain,
( skolemFOFtoCNF_C(singleton(X_204),unordered_pair(empty_set,singleton(X_204))) != empty_set
| ~ subset(empty_set,singleton(X_204))
| subset(skolemFOFtoCNF_C(singleton(X_204),unordered_pair(empty_set,singleton(X_204))),singleton(X_204)) ),
introduced(tautology,[equality,[$cnf( ~ subset(skolemFOFtoCNF_C(singleton(X_204),unordered_pair(empty_set,singleton(X_204))),singleton(X_204)) ),[0],$fot(empty_set)]]) ).
cnf(refute_0_70,plain,
( ~ subset(empty_set,singleton(X_204))
| unordered_pair(empty_set,singleton(X_204)) = powerset(singleton(X_204))
| subset(skolemFOFtoCNF_C(singleton(X_204),unordered_pair(empty_set,singleton(X_204))),singleton(X_204)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_C(singleton(X_204),unordered_pair(empty_set,singleton(X_204))),empty_set) )],[refute_0_68,refute_0_69]) ).
cnf(refute_0_71,plain,
( ~ subset(empty_set,singleton(X_204))
| unordered_pair(empty_set,singleton(X_204)) = powerset(singleton(X_204)) ),
inference(resolve,[$cnf( subset(skolemFOFtoCNF_C(singleton(X_204),unordered_pair(empty_set,singleton(X_204))),singleton(X_204)) )],[refute_0_70,refute_0_67]) ).
cnf(refute_0_72,plain,
( A != empty_set
| subset(A,singleton(B)) ),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_73,plain,
( empty_set != empty_set
| subset(empty_set,singleton(B)) ),
inference(subst,[],[refute_0_72:[bind(A,$fot(empty_set))]]) ).
cnf(refute_0_74,plain,
empty_set = empty_set,
introduced(tautology,[refl,[$fot(empty_set)]]) ).
cnf(refute_0_75,plain,
subset(empty_set,singleton(B)),
inference(resolve,[$cnf( $equal(empty_set,empty_set) )],[refute_0_74,refute_0_73]) ).
cnf(refute_0_76,plain,
subset(empty_set,singleton(X_204)),
inference(subst,[],[refute_0_75:[bind(B,$fot(X_204))]]) ).
cnf(refute_0_77,plain,
unordered_pair(empty_set,singleton(X_204)) = powerset(singleton(X_204)),
inference(resolve,[$cnf( subset(empty_set,singleton(X_204)) )],[refute_0_76,refute_0_71]) ).
cnf(refute_0_78,plain,
unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2)) = powerset(singleton(skolemFOFtoCNF_A_2)),
inference(subst,[],[refute_0_77:[bind(X_204,$fot(skolemFOFtoCNF_A_2))]]) ).
cnf(refute_0_79,plain,
( powerset(singleton(skolemFOFtoCNF_A_2)) != powerset(singleton(skolemFOFtoCNF_A_2))
| unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2)) != powerset(singleton(skolemFOFtoCNF_A_2))
| powerset(singleton(skolemFOFtoCNF_A_2)) = unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2)) ),
introduced(tautology,[equality,[$cnf( ~ $equal(powerset(singleton(skolemFOFtoCNF_A_2)),unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2))) ),[1],$fot(powerset(singleton(skolemFOFtoCNF_A_2)))]]) ).
cnf(refute_0_80,plain,
( powerset(singleton(skolemFOFtoCNF_A_2)) != powerset(singleton(skolemFOFtoCNF_A_2))
| powerset(singleton(skolemFOFtoCNF_A_2)) = unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2)) ),
inference(resolve,[$cnf( $equal(unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2)),powerset(singleton(skolemFOFtoCNF_A_2))) )],[refute_0_78,refute_0_79]) ).
cnf(refute_0_81,plain,
powerset(singleton(skolemFOFtoCNF_A_2)) != powerset(singleton(skolemFOFtoCNF_A_2)),
inference(resolve,[$cnf( $equal(powerset(singleton(skolemFOFtoCNF_A_2)),unordered_pair(empty_set,singleton(skolemFOFtoCNF_A_2))) )],[refute_0_80,refute_0_0]) ).
cnf(refute_0_82,plain,
powerset(singleton(skolemFOFtoCNF_A_2)) = powerset(singleton(skolemFOFtoCNF_A_2)),
introduced(tautology,[refl,[$fot(powerset(singleton(skolemFOFtoCNF_A_2)))]]) ).
cnf(refute_0_83,plain,
$false,
inference(resolve,[$cnf( $equal(powerset(singleton(skolemFOFtoCNF_A_2)),powerset(singleton(skolemFOFtoCNF_A_2))) )],[refute_0_82,refute_0_81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SET889+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% 0.12/0.14 % Command : metis --show proof --show saturation %s
% 0.14/0.35 % Computer : n027.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Sun Jul 10 04:27:32 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.14/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.59/0.76 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.59/0.76
% 0.59/0.76 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.59/0.77
%------------------------------------------------------------------------------