↑ Up

Duper---1.0.THM-Prf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Duper---1.0
% Problem  : SET663+3 : TPTP v9.2.0. Released v2.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : duper %s

% Computer : n016.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  : 300s
% DateTime : Fri Oct  3 08:00:21 PM UTC 2025

% Result   : Theorem 8.87s 9.05s
% Output   : Proof 8.94s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem    : SET663+3 : TPTP v9.2.0. Released v2.2.0.
% 0.07/0.14  % Command    : duper %s
% 0.13/0.35  % Computer : n016.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit   : 300
% 0.13/0.35  % WCLimit    : 300
% 0.13/0.35  % DateTime   : Thu Oct  2 13:47:53 EDT 2025
% 0.13/0.35  % CPUTime    : 
% 8.87/9.05  SZS status Theorem for theBenchmark.p
% 8.87/9.05  SZS output start Proof for theBenchmark.p
% 8.87/9.05  Clause #0 (by assumption #[]): Eq (∀ (B : Iota), ilf_type B set_type → subset B empty_set → Eq B empty_set) True
% 8.87/9.05  Clause #1 (by assumption #[]): Eq
% 8.87/9.05    (∀ (B : Iota),
% 8.87/9.05      ilf_type B binary_relation_type → Or (Eq (domain_of B) empty_set) (Eq (range_of B) empty_set) → Eq B empty_set)
% 8.87/9.05    True
% 8.87/9.05  Clause #2 (by assumption #[]): Eq
% 8.87/9.05    (∀ (B : Iota),
% 8.87/9.05      ilf_type B set_type →
% 8.87/9.05        ∀ (C : Iota),
% 8.87/9.05          ilf_type C set_type →
% 8.87/9.05            ∀ (D : Iota), ilf_type D (relation_type B C) → And (subset (domain_of D) B) (subset (range_of D) C))
% 8.87/9.05    True
% 8.87/9.05  Clause #6 (by assumption #[]): Eq
% 8.87/9.05    (∀ (B : Iota),
% 8.87/9.05      ilf_type B set_type →
% 8.87/9.05        ∀ (C : Iota),
% 8.87/9.05          ilf_type C set_type →
% 8.87/9.05            And (∀ (D : Iota), ilf_type D (subset_type (cross_product B C)) → ilf_type D (relation_type B C))
% 8.87/9.05              (∀ (E : Iota), ilf_type E (relation_type B C) → ilf_type E (subset_type (cross_product B C))))
% 8.87/9.05    True
% 8.87/9.05  Clause #13 (by assumption #[]): Eq
% 8.87/9.05    (∀ (B : Iota),
% 8.87/9.05      ilf_type B set_type → Iff (ilf_type B binary_relation_type) (And (relation_like B) (ilf_type B set_type)))
% 8.87/9.05    True
% 8.87/9.05  Clause #28 (by assumption #[]): Eq
% 8.87/9.05    (∀ (B : Iota),
% 8.87/9.05      ilf_type B set_type →
% 8.87/9.05        ∀ (C : Iota), ilf_type C set_type → ∀ (D : Iota), ilf_type D (subset_type (cross_product B C)) → relation_like D)
% 8.87/9.05    True
% 8.87/9.05  Clause #33 (by assumption #[]): Eq (∀ (B : Iota), ilf_type B set_type) True
% 8.87/9.05  Clause #34 (by assumption #[]): Eq
% 8.87/9.05    (Not
% 8.87/9.05      (∀ (B : Iota),
% 8.87/9.05        ilf_type B set_type →
% 8.87/9.05          ∀ (C : Iota),
% 8.87/9.05            ilf_type C set_type →
% 8.87/9.05              ∀ (D : Iota), ilf_type D (relation_type B C) → ilf_type D (relation_type empty_set C) → Eq D empty_set))
% 8.87/9.05    True
% 8.87/9.05  Clause #39 (by clausification #[33]): ∀ (a : Iota), Eq (ilf_type a set_type) True
% 8.87/9.05  Clause #44 (by clausification #[0]): ∀ (a : Iota), Eq (ilf_type a set_type → subset a empty_set → Eq a empty_set) True
% 8.87/9.05  Clause #45 (by clausification #[44]): ∀ (a : Iota), Or (Eq (ilf_type a set_type) False) (Eq (subset a empty_set → Eq a empty_set) True)
% 8.87/9.05  Clause #46 (by clausification #[45]): ∀ (a : Iota), Or (Eq (ilf_type a set_type) False) (Or (Eq (subset a empty_set) False) (Eq (Eq a empty_set) True))
% 8.87/9.05  Clause #47 (by clausification #[46]): ∀ (a : Iota), Or (Eq (ilf_type a set_type) False) (Or (Eq (subset a empty_set) False) (Eq a empty_set))
% 8.87/9.05  Clause #48 (by forward demodulation #[47, 39]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (subset a empty_set) False) (Eq a empty_set))
% 8.87/9.05  Clause #49 (by clausification #[48]): ∀ (a : Iota), Or (Eq (subset a empty_set) False) (Eq a empty_set)
% 8.87/9.05  Clause #60 (by clausification #[1]): ∀ (a : Iota),
% 8.87/9.05    Eq (ilf_type a binary_relation_type → Or (Eq (domain_of a) empty_set) (Eq (range_of a) empty_set) → Eq a empty_set)
% 8.87/9.05      True
% 8.87/9.05  Clause #61 (by clausification #[60]): ∀ (a : Iota),
% 8.87/9.05    Or (Eq (ilf_type a binary_relation_type) False)
% 8.87/9.05      (Eq (Or (Eq (domain_of a) empty_set) (Eq (range_of a) empty_set) → Eq a empty_set) True)
% 8.87/9.05  Clause #62 (by clausification #[61]): ∀ (a : Iota),
% 8.87/9.05    Or (Eq (ilf_type a binary_relation_type) False)
% 8.87/9.05      (Or (Eq (Or (Eq (domain_of a) empty_set) (Eq (range_of a) empty_set)) False) (Eq (Eq a empty_set) True))
% 8.87/9.05  Clause #64 (by clausification #[62]): ∀ (a : Iota),
% 8.87/9.05    Or (Eq (ilf_type a binary_relation_type) False)
% 8.87/9.05      (Or (Eq (Eq a empty_set) True) (Eq (Eq (domain_of a) empty_set) False))
% 8.87/9.05  Clause #73 (by clausification #[28]): ∀ (a : Iota),
% 8.87/9.05    Eq
% 8.87/9.05      (ilf_type a set_type →
% 8.87/9.05        ∀ (C : Iota), ilf_type C set_type → ∀ (D : Iota), ilf_type D (subset_type (cross_product a C)) → relation_like D)
% 8.87/9.05      True
% 8.87/9.05  Clause #74 (by clausification #[73]): ∀ (a : Iota),
% 8.87/9.05    Or (Eq (ilf_type a set_type) False)
% 8.87/9.05      (Eq
% 8.87/9.05        (∀ (C : Iota), ilf_type C set_type → ∀ (D : Iota), ilf_type D (subset_type (cross_product a C)) → relation_like D)
% 8.87/9.05        True)
% 8.87/9.05  Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota),
% 8.87/9.05    Or (Eq (ilf_type a set_type) False)
% 8.87/9.05      (Eq (ilf_type a_1 set_type → ∀ (D : Iota), ilf_type D (subset_type (cross_product a a_1)) → relation_like D) True)
% 8.87/9.07  Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.07        (Eq (∀ (D : Iota), ilf_type D (subset_type (cross_product a a_1)) → relation_like D) True))
% 8.87/9.07  Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.07        (Eq (ilf_type a_2 (subset_type (cross_product a a_1)) → relation_like a_2) True))
% 8.87/9.07  Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.07        (Or (Eq (ilf_type a_2 (subset_type (cross_product a a_1))) False) (Eq (relation_like a_2) True)))
% 8.87/9.07  Clause #79 (by forward demodulation #[78, 39]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.07    Or (Eq True False)
% 8.87/9.07      (Or (Eq (ilf_type a set_type) False)
% 8.87/9.07        (Or (Eq (ilf_type a_1 (subset_type (cross_product a_2 a))) False) (Eq (relation_like a_1) True)))
% 8.87/9.07  Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Or (Eq (ilf_type a_1 (subset_type (cross_product a_2 a))) False) (Eq (relation_like a_1) True))
% 8.87/9.07  Clause #81 (by forward demodulation #[80, 39]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.07    Or (Eq True False) (Or (Eq (ilf_type a (subset_type (cross_product a_1 a_2))) False) (Eq (relation_like a) True))
% 8.87/9.07  Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), Or (Eq (ilf_type a (subset_type (cross_product a_1 a_2))) False) (Eq (relation_like a) True)
% 8.87/9.07  Clause #87 (by clausification #[2]): ∀ (a : Iota),
% 8.87/9.07    Eq
% 8.87/9.07      (ilf_type a set_type →
% 8.87/9.07        ∀ (C : Iota),
% 8.87/9.07          ilf_type C set_type →
% 8.87/9.07            ∀ (D : Iota), ilf_type D (relation_type a C) → And (subset (domain_of D) a) (subset (range_of D) C))
% 8.87/9.07      True
% 8.87/9.07  Clause #88 (by clausification #[87]): ∀ (a : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Eq
% 8.87/9.07        (∀ (C : Iota),
% 8.87/9.07          ilf_type C set_type →
% 8.87/9.07            ∀ (D : Iota), ilf_type D (relation_type a C) → And (subset (domain_of D) a) (subset (range_of D) C))
% 8.87/9.07        True)
% 8.87/9.07  Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Eq
% 8.87/9.07        (ilf_type a_1 set_type →
% 8.87/9.07          ∀ (D : Iota), ilf_type D (relation_type a a_1) → And (subset (domain_of D) a) (subset (range_of D) a_1))
% 8.87/9.07        True)
% 8.87/9.07  Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.07        (Eq (∀ (D : Iota), ilf_type D (relation_type a a_1) → And (subset (domain_of D) a) (subset (range_of D) a_1))
% 8.87/9.07          True))
% 8.87/9.07  Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.07        (Eq (ilf_type a_2 (relation_type a a_1) → And (subset (domain_of a_2) a) (subset (range_of a_2) a_1)) True))
% 8.87/9.07  Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.07        (Or (Eq (ilf_type a_2 (relation_type a a_1)) False)
% 8.87/9.07          (Eq (And (subset (domain_of a_2) a) (subset (range_of a_2) a_1)) True)))
% 8.87/9.07  Clause #94 (by clausification #[92]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.07        (Or (Eq (ilf_type a_2 (relation_type a a_1)) False) (Eq (subset (domain_of a_2) a) True)))
% 8.87/9.07  Clause #135 (by clausification #[6]): ∀ (a : Iota),
% 8.87/9.07    Eq
% 8.87/9.07      (ilf_type a set_type →
% 8.87/9.07        ∀ (C : Iota),
% 8.87/9.07          ilf_type C set_type →
% 8.87/9.07            And (∀ (D : Iota), ilf_type D (subset_type (cross_product a C)) → ilf_type D (relation_type a C))
% 8.87/9.07              (∀ (E : Iota), ilf_type E (relation_type a C) → ilf_type E (subset_type (cross_product a C))))
% 8.87/9.07      True
% 8.87/9.07  Clause #136 (by clausification #[135]): ∀ (a : Iota),
% 8.87/9.07    Or (Eq (ilf_type a set_type) False)
% 8.87/9.07      (Eq
% 8.87/9.07        (∀ (C : Iota),
% 8.87/9.07          ilf_type C set_type →
% 8.87/9.07            And (∀ (D : Iota), ilf_type D (subset_type (cross_product a C)) → ilf_type D (relation_type a C))
% 8.87/9.07              (∀ (E : Iota), ilf_type E (relation_type a C) → ilf_type E (subset_type (cross_product a C))))
% 8.87/9.10        True)
% 8.87/9.10  Clause #137 (by clausification #[136]): ∀ (a a_1 : Iota),
% 8.87/9.10    Or (Eq (ilf_type a set_type) False)
% 8.87/9.10      (Eq
% 8.87/9.10        (ilf_type a_1 set_type →
% 8.87/9.10          And (∀ (D : Iota), ilf_type D (subset_type (cross_product a a_1)) → ilf_type D (relation_type a a_1))
% 8.87/9.10            (∀ (E : Iota), ilf_type E (relation_type a a_1) → ilf_type E (subset_type (cross_product a a_1))))
% 8.87/9.10        True)
% 8.87/9.10  Clause #138 (by clausification #[137]): ∀ (a a_1 : Iota),
% 8.87/9.10    Or (Eq (ilf_type a set_type) False)
% 8.87/9.10      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.10        (Eq
% 8.87/9.10          (And (∀ (D : Iota), ilf_type D (subset_type (cross_product a a_1)) → ilf_type D (relation_type a a_1))
% 8.87/9.10            (∀ (E : Iota), ilf_type E (relation_type a a_1) → ilf_type E (subset_type (cross_product a a_1))))
% 8.87/9.10          True))
% 8.87/9.10  Clause #139 (by clausification #[138]): ∀ (a a_1 : Iota),
% 8.87/9.10    Or (Eq (ilf_type a set_type) False)
% 8.87/9.10      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.10        (Eq (∀ (E : Iota), ilf_type E (relation_type a a_1) → ilf_type E (subset_type (cross_product a a_1))) True))
% 8.87/9.10  Clause #141 (by clausification #[139]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.10    Or (Eq (ilf_type a set_type) False)
% 8.87/9.10      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.10        (Eq (ilf_type a_2 (relation_type a a_1) → ilf_type a_2 (subset_type (cross_product a a_1))) True))
% 8.87/9.10  Clause #142 (by clausification #[141]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.10    Or (Eq (ilf_type a set_type) False)
% 8.87/9.10      (Or (Eq (ilf_type a_1 set_type) False)
% 8.87/9.10        (Or (Eq (ilf_type a_2 (relation_type a a_1)) False) (Eq (ilf_type a_2 (subset_type (cross_product a a_1))) True)))
% 8.87/9.10  Clause #143 (by forward demodulation #[142, 39]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.10    Or (Eq True False)
% 8.87/9.10      (Or (Eq (ilf_type a set_type) False)
% 8.87/9.10        (Or (Eq (ilf_type a_1 (relation_type a_2 a)) False) (Eq (ilf_type a_1 (subset_type (cross_product a_2 a))) True)))
% 8.87/9.10  Clause #144 (by clausification #[143]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.10    Or (Eq (ilf_type a set_type) False)
% 8.87/9.10      (Or (Eq (ilf_type a_1 (relation_type a_2 a)) False) (Eq (ilf_type a_1 (subset_type (cross_product a_2 a))) True))
% 8.87/9.10  Clause #145 (by forward demodulation #[144, 39]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.10    Or (Eq True False)
% 8.87/9.10      (Or (Eq (ilf_type a (relation_type a_1 a_2)) False) (Eq (ilf_type a (subset_type (cross_product a_1 a_2))) True))
% 8.87/9.10  Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 : Iota),
% 8.87/9.10    Or (Eq (ilf_type a (relation_type a_1 a_2)) False) (Eq (ilf_type a (subset_type (cross_product a_1 a_2))) True)
% 8.87/9.10  Clause #200 (by clausification #[34]): Eq
% 8.87/9.10    (∀ (B : Iota),
% 8.87/9.10      ilf_type B set_type →
% 8.87/9.10        ∀ (C : Iota),
% 8.87/9.10          ilf_type C set_type →
% 8.87/9.10            ∀ (D : Iota), ilf_type D (relation_type B C) → ilf_type D (relation_type empty_set C) → Eq D empty_set)
% 8.87/9.10    False
% 8.87/9.10  Clause #201 (by clausification #[200]): ∀ (a : Iota),
% 8.87/9.10    Eq
% 8.87/9.10      (Not
% 8.87/9.10        (ilf_type (skS.0 6 a) set_type →
% 8.87/9.10          ∀ (C : Iota),
% 8.87/9.10            ilf_type C set_type →
% 8.87/9.10              ∀ (D : Iota),
% 8.87/9.10                ilf_type D (relation_type (skS.0 6 a) C) → ilf_type D (relation_type empty_set C) → Eq D empty_set))
% 8.87/9.10      True
% 8.87/9.10  Clause #202 (by clausification #[201]): ∀ (a : Iota),
% 8.87/9.10    Eq
% 8.87/9.10      (ilf_type (skS.0 6 a) set_type →
% 8.87/9.10        ∀ (C : Iota),
% 8.87/9.10          ilf_type C set_type →
% 8.87/9.10            ∀ (D : Iota),
% 8.87/9.10              ilf_type D (relation_type (skS.0 6 a) C) → ilf_type D (relation_type empty_set C) → Eq D empty_set)
% 8.87/9.10      False
% 8.87/9.10  Clause #204 (by clausification #[202]): ∀ (a : Iota),
% 8.87/9.10    Eq
% 8.87/9.10      (∀ (C : Iota),
% 8.87/9.10        ilf_type C set_type →
% 8.87/9.10          ∀ (D : Iota),
% 8.87/9.10            ilf_type D (relation_type (skS.0 6 a) C) → ilf_type D (relation_type empty_set C) → Eq D empty_set)
% 8.87/9.10      False
% 8.87/9.10  Clause #205 (by clausification #[204]): ∀ (a a_1 : Iota),
% 8.87/9.10    Eq
% 8.87/9.10      (Not
% 8.87/9.10        (ilf_type (skS.0 7 a a_1) set_type →
% 8.87/9.10          ∀ (D : Iota),
% 8.87/9.10            ilf_type D (relation_type (skS.0 6 a) (skS.0 7 a a_1)) →
% 8.87/9.10              ilf_type D (relation_type empty_set (skS.0 7 a a_1)) → Eq D empty_set))
% 8.87/9.10      True
% 8.87/9.10  Clause #206 (by clausification #[205]): ∀ (a a_1 : Iota),
% 8.87/9.10    Eq
% 8.87/9.10      (ilf_type (skS.0 7 a a_1) set_type →
% 8.87/9.10        ∀ (D : Iota),
% 8.87/9.10          ilf_type D (relation_type (skS.0 6 a) (skS.0 7 a a_1)) →
% 8.94/9.12            ilf_type D (relation_type empty_set (skS.0 7 a a_1)) → Eq D empty_set)
% 8.94/9.12      False
% 8.94/9.12  Clause #208 (by clausification #[206]): ∀ (a a_1 : Iota),
% 8.94/9.12    Eq
% 8.94/9.12      (∀ (D : Iota),
% 8.94/9.12        ilf_type D (relation_type (skS.0 6 a) (skS.0 7 a a_1)) →
% 8.94/9.12          ilf_type D (relation_type empty_set (skS.0 7 a a_1)) → Eq D empty_set)
% 8.94/9.12      False
% 8.94/9.12  Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 : Iota),
% 8.94/9.12    Eq
% 8.94/9.12      (Not
% 8.94/9.12        (ilf_type (skS.0 8 a a_1 a_2) (relation_type (skS.0 6 a) (skS.0 7 a a_1)) →
% 8.94/9.12          ilf_type (skS.0 8 a a_1 a_2) (relation_type empty_set (skS.0 7 a a_1)) → Eq (skS.0 8 a a_1 a_2) empty_set))
% 8.94/9.12      True
% 8.94/9.12  Clause #210 (by clausification #[209]): ∀ (a a_1 a_2 : Iota),
% 8.94/9.12    Eq
% 8.94/9.12      (ilf_type (skS.0 8 a a_1 a_2) (relation_type (skS.0 6 a) (skS.0 7 a a_1)) →
% 8.94/9.12        ilf_type (skS.0 8 a a_1 a_2) (relation_type empty_set (skS.0 7 a a_1)) → Eq (skS.0 8 a a_1 a_2) empty_set)
% 8.94/9.12      False
% 8.94/9.12  Clause #211 (by clausification #[210]): ∀ (a a_1 a_2 : Iota), Eq (ilf_type (skS.0 8 a a_1 a_2) (relation_type (skS.0 6 a) (skS.0 7 a a_1))) True
% 8.94/9.12  Clause #212 (by clausification #[210]): ∀ (a a_1 a_2 : Iota),
% 8.94/9.12    Eq (ilf_type (skS.0 8 a a_1 a_2) (relation_type empty_set (skS.0 7 a a_1)) → Eq (skS.0 8 a a_1 a_2) empty_set) False
% 8.94/9.12  Clause #214 (by superposition #[211, 146]): ∀ (a a_1 a_2 : Iota),
% 8.94/9.12    Or (Eq True False) (Eq (ilf_type (skS.0 8 a a_1 a_2) (subset_type (cross_product (skS.0 6 a) (skS.0 7 a a_1)))) True)
% 8.94/9.12  Clause #215 (by clausification #[13]): ∀ (a : Iota),
% 8.94/9.12    Eq (ilf_type a set_type → Iff (ilf_type a binary_relation_type) (And (relation_like a) (ilf_type a set_type))) True
% 8.94/9.12  Clause #216 (by clausification #[215]): ∀ (a : Iota),
% 8.94/9.12    Or (Eq (ilf_type a set_type) False)
% 8.94/9.12      (Eq (Iff (ilf_type a binary_relation_type) (And (relation_like a) (ilf_type a set_type))) True)
% 8.94/9.12  Clause #217 (by clausification #[216]): ∀ (a : Iota),
% 8.94/9.12    Or (Eq (ilf_type a set_type) False)
% 8.94/9.12      (Or (Eq (ilf_type a binary_relation_type) True) (Eq (And (relation_like a) (ilf_type a set_type)) False))
% 8.94/9.12  Clause #219 (by clausification #[217]): ∀ (a : Iota),
% 8.94/9.12    Or (Eq (ilf_type a set_type) False)
% 8.94/9.12      (Or (Eq (ilf_type a binary_relation_type) True) (Or (Eq (relation_like a) False) (Eq (ilf_type a set_type) False)))
% 8.94/9.12  Clause #220 (by eliminate duplicate literals #[219]): ∀ (a : Iota),
% 8.94/9.12    Or (Eq (ilf_type a set_type) False) (Or (Eq (ilf_type a binary_relation_type) True) (Eq (relation_like a) False))
% 8.94/9.12  Clause #221 (by forward demodulation #[220, 39]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (ilf_type a binary_relation_type) True) (Eq (relation_like a) False))
% 8.94/9.12  Clause #222 (by clausification #[221]): ∀ (a : Iota), Or (Eq (ilf_type a binary_relation_type) True) (Eq (relation_like a) False)
% 8.94/9.12  Clause #308 (by clausification #[212]): ∀ (a a_1 a_2 : Iota), Eq (ilf_type (skS.0 8 a a_1 a_2) (relation_type empty_set (skS.0 7 a a_1))) True
% 8.94/9.12  Clause #309 (by clausification #[212]): ∀ (a a_1 a_2 : Iota), Eq (Eq (skS.0 8 a a_1 a_2) empty_set) False
% 8.94/9.12  Clause #313 (by clausification #[309]): ∀ (a a_1 a_2 : Iota), Ne (skS.0 8 a a_1 a_2) empty_set
% 8.94/9.12  Clause #328 (by clausification #[64]): ∀ (a : Iota),
% 8.94/9.12    Or (Eq (ilf_type a binary_relation_type) False) (Or (Eq (Eq (domain_of a) empty_set) False) (Eq a empty_set))
% 8.94/9.12  Clause #329 (by clausification #[328]): ∀ (a : Iota), Or (Eq (ilf_type a binary_relation_type) False) (Or (Eq a empty_set) (Ne (domain_of a) empty_set))
% 8.94/9.12  Clause #381 (by forward demodulation #[94, 39]): ∀ (a a_1 a_2 : Iota),
% 8.94/9.12    Or (Eq True False)
% 8.94/9.12      (Or (Eq (ilf_type a set_type) False)
% 8.94/9.12        (Or (Eq (ilf_type a_1 (relation_type a_2 a)) False) (Eq (subset (domain_of a_1) a_2) True)))
% 8.94/9.12  Clause #382 (by clausification #[381]): ∀ (a a_1 a_2 : Iota),
% 8.94/9.12    Or (Eq (ilf_type a set_type) False)
% 8.94/9.12      (Or (Eq (ilf_type a_1 (relation_type a_2 a)) False) (Eq (subset (domain_of a_1) a_2) True))
% 8.94/9.12  Clause #383 (by forward demodulation #[382, 39]): ∀ (a a_1 a_2 : Iota),
% 8.94/9.12    Or (Eq True False) (Or (Eq (ilf_type a (relation_type a_1 a_2)) False) (Eq (subset (domain_of a) a_1) True))
% 8.94/9.12  Clause #384 (by clausification #[383]): ∀ (a a_1 a_2 : Iota), Or (Eq (ilf_type a (relation_type a_1 a_2)) False) (Eq (subset (domain_of a) a_1) True)
% 8.94/9.13  Clause #387 (by superposition #[384, 308]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset (domain_of (skS.0 8 a a_1 a_2)) empty_set) True) (Eq False True)
% 8.94/9.13  Clause #392 (by clausification #[387]): ∀ (a a_1 a_2 : Iota), Eq (subset (domain_of (skS.0 8 a a_1 a_2)) empty_set) True
% 8.94/9.13  Clause #393 (by superposition #[392, 49]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (domain_of (skS.0 8 a a_1 a_2)) empty_set)
% 8.94/9.13  Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 : Iota), Eq (domain_of (skS.0 8 a a_1 a_2)) empty_set
% 8.94/9.13  Clause #496 (by clausification #[214]): ∀ (a a_1 a_2 : Iota), Eq (ilf_type (skS.0 8 a a_1 a_2) (subset_type (cross_product (skS.0 6 a) (skS.0 7 a a_1)))) True
% 8.94/9.13  Clause #497 (by superposition #[496, 82]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (relation_like (skS.0 8 a a_1 a_2)) True)
% 8.94/9.13  Clause #500 (by clausification #[497]): ∀ (a a_1 a_2 : Iota), Eq (relation_like (skS.0 8 a a_1 a_2)) True
% 8.94/9.13  Clause #501 (by superposition #[500, 222]): ∀ (a a_1 a_2 : Iota), Or (Eq (ilf_type (skS.0 8 a a_1 a_2) binary_relation_type) True) (Eq True False)
% 8.94/9.13  Clause #502 (by clausification #[501]): ∀ (a a_1 a_2 : Iota), Eq (ilf_type (skS.0 8 a a_1 a_2) binary_relation_type) True
% 8.94/9.13  Clause #504 (by superposition #[502, 329]): ∀ (a a_1 a_2 : Iota),
% 8.94/9.13    Or (Eq True False) (Or (Eq (skS.0 8 a a_1 a_2) empty_set) (Ne (domain_of (skS.0 8 a a_1 a_2)) empty_set))
% 8.94/9.13  Clause #1106 (by clausification #[504]): ∀ (a a_1 a_2 : Iota), Or (Eq (skS.0 8 a a_1 a_2) empty_set) (Ne (domain_of (skS.0 8 a a_1 a_2)) empty_set)
% 8.94/9.13  Clause #1107 (by forward demodulation #[1106, 394]): ∀ (a a_1 a_2 : Iota), Or (Eq (skS.0 8 a a_1 a_2) empty_set) (Ne empty_set empty_set)
% 8.94/9.13  Clause #1108 (by eliminate resolved literals #[1107]): ∀ (a a_1 a_2 : Iota), Eq (skS.0 8 a a_1 a_2) empty_set
% 8.94/9.13  Clause #1109 (by forward contextual literal cutting #[1108, 313]): False
% 8.94/9.13  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------