%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SEU326+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n017.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:40:20 EDT 2022
% Result : Theorem 0.82s 1.03s
% Output : CNFRefutation 0.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 13
% Syntax : Number of formulae : 72 ( 26 unt; 0 def)
% Number of atoms : 148 ( 89 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 146 ( 70 ~; 43 |; 24 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 76 ( 7 sgn 41 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k7_setfam_1,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> element(complements_of_subsets(A,B),powerset(powerset(A))) ) ).
fof(involutiveness_k7_setfam_1,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> complements_of_subsets(A,complements_of_subsets(A,B)) = B ) ).
fof(rc2_subset_1,axiom,
! [A] :
? [B] :
( element(B,powerset(A))
& empty(B) ) ).
fof(t10_tops_2,conjecture,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ( ~ ( B != empty_set
& complements_of_subsets(A,B) = empty_set )
& ~ ( complements_of_subsets(A,B) != empty_set
& B = empty_set ) ) ) ).
fof(t46_setfam_1,axiom,
! [A,B] :
( element(B,powerset(powerset(A)))
=> ~ ( B != empty_set
& complements_of_subsets(A,B) = empty_set ) ) ).
fof(t6_boole,axiom,
! [A] :
( empty(A)
=> A = empty_set ) ).
fof(subgoal_0,plain,
! [A,B] :
( ( element(B,powerset(powerset(A)))
& B != empty_set )
=> complements_of_subsets(A,B) != empty_set ),
inference(strip,[],[t10_tops_2]) ).
fof(subgoal_1,plain,
! [A,B] :
( ( element(B,powerset(powerset(A)))
& ~ ( B != empty_set
& complements_of_subsets(A,B) = empty_set )
& complements_of_subsets(A,B) != empty_set )
=> B != empty_set ),
inference(strip,[],[t10_tops_2]) ).
fof(negate_0_0,plain,
~ ! [A,B] :
( ( element(B,powerset(powerset(A)))
& B != empty_set )
=> complements_of_subsets(A,B) != empty_set ),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
? [A,B] :
( B != empty_set
& complements_of_subsets(A,B) = empty_set
& element(B,powerset(powerset(A))) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,plain,
! [A,B] :
( complements_of_subsets(A,B) != empty_set
| ~ element(B,powerset(powerset(A)))
| B = empty_set ),
inference(canonicalize,[],[t46_setfam_1]) ).
fof(normalize_0_2,plain,
! [A,B] :
( complements_of_subsets(A,B) != empty_set
| ~ element(B,powerset(powerset(A)))
| B = empty_set ),
inference(specialize,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
$false,
inference(simplify,[],[normalize_0_0,normalize_0_2]) ).
cnf(refute_0_0,plain,
$false,
inference(canonicalize,[],[normalize_0_3]) ).
fof(negate_1_0,plain,
~ ! [A,B] :
( ( element(B,powerset(powerset(A)))
& ~ ( B != empty_set
& complements_of_subsets(A,B) = empty_set )
& complements_of_subsets(A,B) != empty_set )
=> B != empty_set ),
inference(negate,[],[subgoal_1]) ).
fof(normalize_1_0,plain,
? [A,B] :
( complements_of_subsets(A,B) != empty_set
& B = empty_set
& element(B,powerset(powerset(A)))
& ( complements_of_subsets(A,B) != empty_set
| B = empty_set ) ),
inference(canonicalize,[],[negate_1_0]) ).
fof(normalize_1_1,plain,
( complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) != empty_set
& skolemFOFtoCNF_B_3 = empty_set
& element(skolemFOFtoCNF_B_3,powerset(powerset(skolemFOFtoCNF_A_1)))
& ( complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) != empty_set
| skolemFOFtoCNF_B_3 = empty_set ) ),
inference(skolemize,[],[normalize_1_0]) ).
fof(normalize_1_2,plain,
complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) != empty_set,
inference(conjunct,[],[normalize_1_1]) ).
fof(normalize_1_3,plain,
skolemFOFtoCNF_B_3 = empty_set,
inference(conjunct,[],[normalize_1_1]) ).
fof(normalize_1_4,plain,
! [A] :
? [B] :
( element(B,powerset(A))
& empty(B) ),
inference(canonicalize,[],[rc2_subset_1]) ).
fof(normalize_1_5,plain,
! [A] :
? [B] :
( element(B,powerset(A))
& empty(B) ),
inference(specialize,[],[normalize_1_4]) ).
fof(normalize_1_6,plain,
! [A] :
( element(skolemFOFtoCNF_B_2(A),powerset(A))
& empty(skolemFOFtoCNF_B_2(A)) ),
inference(skolemize,[],[normalize_1_5]) ).
fof(normalize_1_7,plain,
! [A] : element(skolemFOFtoCNF_B_2(A),powerset(A)),
inference(conjunct,[],[normalize_1_6]) ).
fof(normalize_1_8,plain,
! [A] : empty(skolemFOFtoCNF_B_2(A)),
inference(conjunct,[],[normalize_1_6]) ).
fof(normalize_1_9,plain,
! [A] :
( ~ empty(A)
| A = empty_set ),
inference(canonicalize,[],[t6_boole]) ).
fof(normalize_1_10,plain,
! [A] :
( ~ empty(A)
| A = empty_set ),
inference(specialize,[],[normalize_1_9]) ).
fof(normalize_1_11,plain,
! [A,B] :
( ~ element(B,powerset(powerset(A)))
| element(complements_of_subsets(A,B),powerset(powerset(A))) ),
inference(canonicalize,[],[dt_k7_setfam_1]) ).
fof(normalize_1_12,plain,
! [A,B] :
( ~ element(B,powerset(powerset(A)))
| element(complements_of_subsets(A,B),powerset(powerset(A))) ),
inference(specialize,[],[normalize_1_11]) ).
fof(normalize_1_13,plain,
! [A,B] :
( complements_of_subsets(A,B) != empty_set
| ~ element(B,powerset(powerset(A)))
| B = empty_set ),
inference(canonicalize,[],[t46_setfam_1]) ).
fof(normalize_1_14,plain,
! [A,B] :
( complements_of_subsets(A,B) != empty_set
| ~ element(B,powerset(powerset(A)))
| B = empty_set ),
inference(specialize,[],[normalize_1_13]) ).
fof(normalize_1_15,plain,
! [A,B] :
( ~ element(B,powerset(powerset(A)))
| complements_of_subsets(A,complements_of_subsets(A,B)) = B ),
inference(canonicalize,[],[involutiveness_k7_setfam_1]) ).
fof(normalize_1_16,plain,
! [A,B] :
( ~ element(B,powerset(powerset(A)))
| complements_of_subsets(A,complements_of_subsets(A,B)) = B ),
inference(specialize,[],[normalize_1_15]) ).
cnf(refute_1_0,plain,
complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) != empty_set,
inference(canonicalize,[],[normalize_1_2]) ).
cnf(refute_1_1,plain,
skolemFOFtoCNF_B_3 = empty_set,
inference(canonicalize,[],[normalize_1_3]) ).
cnf(refute_1_2,plain,
complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) = complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3),
introduced(tautology,[refl,[$fot(complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3))]]) ).
cnf(refute_1_3,plain,
( complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) != complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3)
| skolemFOFtoCNF_B_3 != empty_set
| complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) = complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) ),
introduced(tautology,[equality,[$cnf( $equal(complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3),complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3)) ),[1,1],$fot(empty_set)]]) ).
cnf(refute_1_4,plain,
( skolemFOFtoCNF_B_3 != empty_set
| complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) = complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) ),
inference(resolve,[$cnf( $equal(complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3),complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3)) )],[refute_1_2,refute_1_3]) ).
cnf(refute_1_5,plain,
complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) = complements_of_subsets(skolemFOFtoCNF_A_1,empty_set),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_B_3,empty_set) )],[refute_1_1,refute_1_4]) ).
cnf(refute_1_6,plain,
( complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) != empty_set
| complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) != complements_of_subsets(skolemFOFtoCNF_A_1,empty_set)
| complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) = empty_set ),
introduced(tautology,[equality,[$cnf( $equal(complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3),complements_of_subsets(skolemFOFtoCNF_A_1,empty_set)) ),[1],$fot(empty_set)]]) ).
cnf(refute_1_7,plain,
( complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) != empty_set
| complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3) = empty_set ),
inference(resolve,[$cnf( $equal(complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3),complements_of_subsets(skolemFOFtoCNF_A_1,empty_set)) )],[refute_1_5,refute_1_6]) ).
cnf(refute_1_8,plain,
complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) != empty_set,
inference(resolve,[$cnf( $equal(complements_of_subsets(skolemFOFtoCNF_A_1,skolemFOFtoCNF_B_3),empty_set) )],[refute_1_7,refute_1_0]) ).
cnf(refute_1_9,plain,
element(skolemFOFtoCNF_B_2(A),powerset(A)),
inference(canonicalize,[],[normalize_1_7]) ).
cnf(refute_1_10,plain,
empty(skolemFOFtoCNF_B_2(A)),
inference(canonicalize,[],[normalize_1_8]) ).
cnf(refute_1_11,plain,
( ~ empty(A)
| A = empty_set ),
inference(canonicalize,[],[normalize_1_10]) ).
cnf(refute_1_12,plain,
( ~ empty(skolemFOFtoCNF_B_2(A))
| skolemFOFtoCNF_B_2(A) = empty_set ),
inference(subst,[],[refute_1_11:[bind(A,$fot(skolemFOFtoCNF_B_2(A)))]]) ).
cnf(refute_1_13,plain,
skolemFOFtoCNF_B_2(A) = empty_set,
inference(resolve,[$cnf( empty(skolemFOFtoCNF_B_2(A)) )],[refute_1_10,refute_1_12]) ).
cnf(refute_1_14,plain,
( skolemFOFtoCNF_B_2(A) != empty_set
| ~ element(skolemFOFtoCNF_B_2(A),powerset(A))
| element(empty_set,powerset(A)) ),
introduced(tautology,[equality,[$cnf( element(skolemFOFtoCNF_B_2(A),powerset(A)) ),[0],$fot(empty_set)]]) ).
cnf(refute_1_15,plain,
( ~ element(skolemFOFtoCNF_B_2(A),powerset(A))
| element(empty_set,powerset(A)) ),
inference(resolve,[$cnf( $equal(skolemFOFtoCNF_B_2(A),empty_set) )],[refute_1_13,refute_1_14]) ).
cnf(refute_1_16,plain,
element(empty_set,powerset(A)),
inference(resolve,[$cnf( element(skolemFOFtoCNF_B_2(A),powerset(A)) )],[refute_1_9,refute_1_15]) ).
cnf(refute_1_17,plain,
element(empty_set,powerset(powerset(X_197))),
inference(subst,[],[refute_1_16:[bind(A,$fot(powerset(X_197)))]]) ).
cnf(refute_1_18,plain,
( ~ element(B,powerset(powerset(A)))
| element(complements_of_subsets(A,B),powerset(powerset(A))) ),
inference(canonicalize,[],[normalize_1_12]) ).
cnf(refute_1_19,plain,
( ~ element(empty_set,powerset(powerset(X_197)))
| element(complements_of_subsets(X_197,empty_set),powerset(powerset(X_197))) ),
inference(subst,[],[refute_1_18:[bind(A,$fot(X_197)),bind(B,$fot(empty_set))]]) ).
cnf(refute_1_20,plain,
element(complements_of_subsets(X_197,empty_set),powerset(powerset(X_197))),
inference(resolve,[$cnf( element(empty_set,powerset(powerset(X_197))) )],[refute_1_17,refute_1_19]) ).
cnf(refute_1_21,plain,
element(complements_of_subsets(X_412,empty_set),powerset(powerset(X_412))),
inference(subst,[],[refute_1_20:[bind(X_197,$fot(X_412))]]) ).
cnf(refute_1_22,plain,
( complements_of_subsets(A,B) != empty_set
| ~ element(B,powerset(powerset(A)))
| B = empty_set ),
inference(canonicalize,[],[normalize_1_14]) ).
cnf(refute_1_23,plain,
( complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)) != empty_set
| ~ element(complements_of_subsets(X_412,empty_set),powerset(powerset(X_412)))
| complements_of_subsets(X_412,empty_set) = empty_set ),
inference(subst,[],[refute_1_22:[bind(A,$fot(X_412)),bind(B,$fot(complements_of_subsets(X_412,empty_set)))]]) ).
cnf(refute_1_24,plain,
( complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)) != empty_set
| complements_of_subsets(X_412,empty_set) = empty_set ),
inference(resolve,[$cnf( element(complements_of_subsets(X_412,empty_set),powerset(powerset(X_412))) )],[refute_1_21,refute_1_23]) ).
cnf(refute_1_25,plain,
element(empty_set,powerset(powerset(X_313))),
inference(subst,[],[refute_1_16:[bind(A,$fot(powerset(X_313)))]]) ).
cnf(refute_1_26,plain,
( ~ element(B,powerset(powerset(A)))
| complements_of_subsets(A,complements_of_subsets(A,B)) = B ),
inference(canonicalize,[],[normalize_1_16]) ).
cnf(refute_1_27,plain,
( ~ element(empty_set,powerset(powerset(X_313)))
| complements_of_subsets(X_313,complements_of_subsets(X_313,empty_set)) = empty_set ),
inference(subst,[],[refute_1_26:[bind(A,$fot(X_313)),bind(B,$fot(empty_set))]]) ).
cnf(refute_1_28,plain,
complements_of_subsets(X_313,complements_of_subsets(X_313,empty_set)) = empty_set,
inference(resolve,[$cnf( element(empty_set,powerset(powerset(X_313))) )],[refute_1_25,refute_1_27]) ).
cnf(refute_1_29,plain,
complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)) = empty_set,
inference(subst,[],[refute_1_28:[bind(X_313,$fot(X_412))]]) ).
cnf(refute_1_30,plain,
( complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)) != empty_set
| empty_set != empty_set
| complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)) = empty_set ),
introduced(tautology,[equality,[$cnf( ~ $equal(complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)),empty_set) ),[0],$fot(empty_set)]]) ).
cnf(refute_1_31,plain,
( empty_set != empty_set
| complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)) = empty_set ),
inference(resolve,[$cnf( $equal(complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)),empty_set) )],[refute_1_29,refute_1_30]) ).
cnf(refute_1_32,plain,
( empty_set != empty_set
| complements_of_subsets(X_412,empty_set) = empty_set ),
inference(resolve,[$cnf( $equal(complements_of_subsets(X_412,complements_of_subsets(X_412,empty_set)),empty_set) )],[refute_1_31,refute_1_24]) ).
cnf(refute_1_33,plain,
empty_set = empty_set,
introduced(tautology,[refl,[$fot(empty_set)]]) ).
cnf(refute_1_34,plain,
complements_of_subsets(X_412,empty_set) = empty_set,
inference(resolve,[$cnf( $equal(empty_set,empty_set) )],[refute_1_33,refute_1_32]) ).
cnf(refute_1_35,plain,
complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) = empty_set,
inference(subst,[],[refute_1_34:[bind(X_412,$fot(skolemFOFtoCNF_A_1))]]) ).
cnf(refute_1_36,plain,
( complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) != empty_set
| empty_set != empty_set
| complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) = empty_set ),
introduced(tautology,[equality,[$cnf( ~ $equal(complements_of_subsets(skolemFOFtoCNF_A_1,empty_set),empty_set) ),[0],$fot(empty_set)]]) ).
cnf(refute_1_37,plain,
( empty_set != empty_set
| complements_of_subsets(skolemFOFtoCNF_A_1,empty_set) = empty_set ),
inference(resolve,[$cnf( $equal(complements_of_subsets(skolemFOFtoCNF_A_1,empty_set),empty_set) )],[refute_1_35,refute_1_36]) ).
cnf(refute_1_38,plain,
empty_set != empty_set,
inference(resolve,[$cnf( $equal(complements_of_subsets(skolemFOFtoCNF_A_1,empty_set),empty_set) )],[refute_1_37,refute_1_8]) ).
cnf(refute_1_39,plain,
$false,
inference(resolve,[$cnf( $equal(empty_set,empty_set) )],[refute_1_33,refute_1_38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SEU326+1 : TPTP v8.1.0. Released v3.3.0.
% 0.11/0.12 % Command : metis --show proof --show saturation %s
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun Jun 19 18:31:28 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.82/1.03 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.82/1.03
% 0.82/1.03 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.82/1.04
%------------------------------------------------------------------------------