↑ Up

Duper---1.0.THM-Prf.s

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

% Computer : n031.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 07:44:10 PM UTC 2025

% Result   : Theorem 186.49s 186.79s
% Output   : Proof 186.88s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem    : ALG227+1 : TPTP v9.2.0. Released v3.4.0.
% 0.03/0.13  % Command    : duper %s
% 0.13/0.34  % Computer : n031.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    : 300
% 0.13/0.34  % DateTime   : Fri Oct  3 09:49:23 EDT 2025
% 0.13/0.34  % CPUTime    : 
% 186.49/186.79  SZS status Theorem for theBenchmark.p
% 186.49/186.79  SZS output start Proof for theBenchmark.p
% 186.49/186.79  Clause #0 (by assumption #[]): Eq
% 186.49/186.79    (Not
% 186.49/186.79      (∀ (A : Iota),
% 186.49/186.79        Not (v1_xboole_0 A) →
% 186.49/186.79          ∀ (B : Iota),
% 186.49/186.79            m1_pboole B A →
% 186.49/186.79              ∀ (C : Iota), m1_subset_1 C A → Not (r2_hidden C (k1_closure3 A B)) → Eq (k1_funct_1 B C) k1_xboole_0))
% 186.49/186.79    True
% 186.49/186.79  Clause #6 (by assumption #[]): Eq
% 186.49/186.79    (∀ (A : Iota),
% 186.49/186.79      Not (v1_xboole_0 A) →
% 186.49/186.79        ∀ (B : Iota), m1_pboole B A → ∀ (C : Iota), Iff (Eq C (k1_closure3 A B)) (Eq C (a_2_0_closure3 A B)))
% 186.49/186.79    True
% 186.49/186.79  Clause #12 (by assumption #[]): Eq
% 186.49/186.79    (∀ (A B C : Iota),
% 186.49/186.79      And (Not (v1_xboole_0 B)) (m1_pboole C B) →
% 186.49/186.79        Iff (r2_hidden A (a_2_0_closure3 B C))
% 186.49/186.79          (Exists fun D => And (And (m1_subset_1 D B) (Eq A D)) (Ne (k1_funct_1 C D) k1_xboole_0)))
% 186.49/186.79    True
% 186.49/186.79  Clause #33 (by clausification #[0]): Eq
% 186.49/186.79    (∀ (A : Iota),
% 186.49/186.79      Not (v1_xboole_0 A) →
% 186.49/186.79        ∀ (B : Iota),
% 186.49/186.79          m1_pboole B A →
% 186.49/186.79            ∀ (C : Iota), m1_subset_1 C A → Not (r2_hidden C (k1_closure3 A B)) → Eq (k1_funct_1 B C) k1_xboole_0)
% 186.49/186.79    False
% 186.49/186.79  Clause #34 (by clausification #[33]): ∀ (a : Iota),
% 186.49/186.79    Eq
% 186.49/186.79      (Not
% 186.49/186.79        (Not (v1_xboole_0 (skS.0 0 a)) →
% 186.49/186.79          ∀ (B : Iota),
% 186.49/186.79            m1_pboole B (skS.0 0 a) →
% 186.49/186.79              ∀ (C : Iota),
% 186.49/186.79                m1_subset_1 C (skS.0 0 a) →
% 186.49/186.79                  Not (r2_hidden C (k1_closure3 (skS.0 0 a) B)) → Eq (k1_funct_1 B C) k1_xboole_0))
% 186.49/186.79      True
% 186.49/186.79  Clause #35 (by clausification #[34]): ∀ (a : Iota),
% 186.49/186.79    Eq
% 186.49/186.79      (Not (v1_xboole_0 (skS.0 0 a)) →
% 186.49/186.79        ∀ (B : Iota),
% 186.49/186.79          m1_pboole B (skS.0 0 a) →
% 186.49/186.79            ∀ (C : Iota),
% 186.49/186.79              m1_subset_1 C (skS.0 0 a) → Not (r2_hidden C (k1_closure3 (skS.0 0 a) B)) → Eq (k1_funct_1 B C) k1_xboole_0)
% 186.49/186.79      False
% 186.49/186.79  Clause #36 (by clausification #[35]): ∀ (a : Iota), Eq (Not (v1_xboole_0 (skS.0 0 a))) True
% 186.49/186.79  Clause #37 (by clausification #[35]): ∀ (a : Iota),
% 186.49/186.79    Eq
% 186.49/186.79      (∀ (B : Iota),
% 186.49/186.79        m1_pboole B (skS.0 0 a) →
% 186.49/186.79          ∀ (C : Iota),
% 186.49/186.79            m1_subset_1 C (skS.0 0 a) → Not (r2_hidden C (k1_closure3 (skS.0 0 a) B)) → Eq (k1_funct_1 B C) k1_xboole_0)
% 186.49/186.79      False
% 186.49/186.79  Clause #38 (by clausification #[36]): ∀ (a : Iota), Eq (v1_xboole_0 (skS.0 0 a)) False
% 186.49/186.79  Clause #95 (by clausification #[6]): ∀ (a : Iota),
% 186.49/186.79    Eq
% 186.49/186.79      (Not (v1_xboole_0 a) →
% 186.49/186.79        ∀ (B : Iota), m1_pboole B a → ∀ (C : Iota), Iff (Eq C (k1_closure3 a B)) (Eq C (a_2_0_closure3 a B)))
% 186.49/186.79      True
% 186.49/186.79  Clause #96 (by clausification #[95]): ∀ (a : Iota),
% 186.49/186.79    Or (Eq (Not (v1_xboole_0 a)) False)
% 186.49/186.79      (Eq (∀ (B : Iota), m1_pboole B a → ∀ (C : Iota), Iff (Eq C (k1_closure3 a B)) (Eq C (a_2_0_closure3 a B))) True)
% 186.49/186.79  Clause #97 (by clausification #[96]): ∀ (a : Iota),
% 186.49/186.79    Or (Eq (∀ (B : Iota), m1_pboole B a → ∀ (C : Iota), Iff (Eq C (k1_closure3 a B)) (Eq C (a_2_0_closure3 a B))) True)
% 186.49/186.79      (Eq (v1_xboole_0 a) True)
% 186.49/186.79  Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota),
% 186.49/186.79    Or (Eq (v1_xboole_0 a) True)
% 186.49/186.79      (Eq (m1_pboole a_1 a → ∀ (C : Iota), Iff (Eq C (k1_closure3 a a_1)) (Eq C (a_2_0_closure3 a a_1))) True)
% 186.49/186.79  Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota),
% 186.49/186.79    Or (Eq (v1_xboole_0 a) True)
% 186.49/186.79      (Or (Eq (m1_pboole a_1 a) False)
% 186.49/186.79        (Eq (∀ (C : Iota), Iff (Eq C (k1_closure3 a a_1)) (Eq C (a_2_0_closure3 a a_1))) True))
% 186.49/186.79  Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.79    Or (Eq (v1_xboole_0 a) True)
% 186.49/186.79      (Or (Eq (m1_pboole a_1 a) False) (Eq (Iff (Eq a_2 (k1_closure3 a a_1)) (Eq a_2 (a_2_0_closure3 a a_1))) True))
% 186.49/186.79  Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.79    Or (Eq (v1_xboole_0 a) True)
% 186.49/186.79      (Or (Eq (m1_pboole a_1 a) False)
% 186.49/186.79        (Or (Eq (Eq a_2 (k1_closure3 a a_1)) True) (Eq (Eq a_2 (a_2_0_closure3 a a_1)) False)))
% 186.49/186.79  Clause #103 (by clausification #[101]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.79    Or (Eq (v1_xboole_0 a) True)
% 186.49/186.79      (Or (Eq (m1_pboole a_1 a) False) (Or (Eq (Eq a_2 (a_2_0_closure3 a a_1)) False) (Eq a_2 (k1_closure3 a a_1))))
% 186.49/186.79  Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.79    Or (Eq (v1_xboole_0 a) True)
% 186.49/186.79      (Or (Eq (m1_pboole a_1 a) False) (Or (Eq a_2 (k1_closure3 a a_1)) (Ne a_2 (a_2_0_closure3 a a_1))))
% 186.49/186.81  Clause #105 (by destructive equality resolution #[104]): ∀ (a a_1 : Iota),
% 186.49/186.81    Or (Eq (v1_xboole_0 a) True) (Or (Eq (m1_pboole a_1 a) False) (Eq (a_2_0_closure3 a a_1) (k1_closure3 a a_1)))
% 186.49/186.81  Clause #113 (by clausification #[12]): ∀ (a : Iota),
% 186.49/186.81    Eq
% 186.49/186.81      (∀ (B C : Iota),
% 186.49/186.81        And (Not (v1_xboole_0 B)) (m1_pboole C B) →
% 186.49/186.81          Iff (r2_hidden a (a_2_0_closure3 B C))
% 186.49/186.81            (Exists fun D => And (And (m1_subset_1 D B) (Eq a D)) (Ne (k1_funct_1 C D) k1_xboole_0)))
% 186.49/186.81      True
% 186.49/186.81  Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota),
% 186.49/186.81    Eq
% 186.49/186.81      (∀ (C : Iota),
% 186.49/186.81        And (Not (v1_xboole_0 a)) (m1_pboole C a) →
% 186.49/186.81          Iff (r2_hidden a_1 (a_2_0_closure3 a C))
% 186.49/186.81            (Exists fun D => And (And (m1_subset_1 D a) (Eq a_1 D)) (Ne (k1_funct_1 C D) k1_xboole_0)))
% 186.49/186.81      True
% 186.49/186.81  Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.81    Eq
% 186.49/186.81      (And (Not (v1_xboole_0 a)) (m1_pboole a_1 a) →
% 186.49/186.81        Iff (r2_hidden a_2 (a_2_0_closure3 a a_1))
% 186.49/186.81          (Exists fun D => And (And (m1_subset_1 D a) (Eq a_2 D)) (Ne (k1_funct_1 a_1 D) k1_xboole_0)))
% 186.49/186.81      True
% 186.49/186.81  Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.81    Or (Eq (And (Not (v1_xboole_0 a)) (m1_pboole a_1 a)) False)
% 186.49/186.81      (Eq
% 186.49/186.81        (Iff (r2_hidden a_2 (a_2_0_closure3 a a_1))
% 186.49/186.81          (Exists fun D => And (And (m1_subset_1 D a) (Eq a_2 D)) (Ne (k1_funct_1 a_1 D) k1_xboole_0)))
% 186.49/186.81        True)
% 186.49/186.81  Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.81    Or
% 186.49/186.81      (Eq
% 186.49/186.81        (Iff (r2_hidden a (a_2_0_closure3 a_1 a_2))
% 186.49/186.81          (Exists fun D => And (And (m1_subset_1 D a_1) (Eq a D)) (Ne (k1_funct_1 a_2 D) k1_xboole_0)))
% 186.49/186.81        True)
% 186.49/186.81      (Or (Eq (Not (v1_xboole_0 a_1)) False) (Eq (m1_pboole a_2 a_1) False))
% 186.49/186.81  Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.81    Or (Eq (Not (v1_xboole_0 a)) False)
% 186.49/186.81      (Or (Eq (m1_pboole a_1 a) False)
% 186.49/186.81        (Or (Eq (r2_hidden a_2 (a_2_0_closure3 a a_1)) True)
% 186.49/186.81          (Eq (Exists fun D => And (And (m1_subset_1 D a) (Eq a_2 D)) (Ne (k1_funct_1 a_1 D) k1_xboole_0)) False)))
% 186.49/186.81  Clause #120 (by clausification #[118]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.81    Or (Eq (m1_pboole a a_1) False)
% 186.49/186.81      (Or (Eq (r2_hidden a_2 (a_2_0_closure3 a_1 a)) True)
% 186.49/186.81        (Or (Eq (Exists fun D => And (And (m1_subset_1 D a_1) (Eq a_2 D)) (Ne (k1_funct_1 a D) k1_xboole_0)) False)
% 186.49/186.81          (Eq (v1_xboole_0 a_1) True)))
% 186.49/186.81  Clause #121 (by clausification #[120]): ∀ (a a_1 a_2 a_3 : Iota),
% 186.49/186.81    Or (Eq (m1_pboole a a_1) False)
% 186.49/186.81      (Or (Eq (r2_hidden a_2 (a_2_0_closure3 a_1 a)) True)
% 186.49/186.81        (Or (Eq (v1_xboole_0 a_1) True)
% 186.49/186.81          (Eq (And (And (m1_subset_1 a_3 a_1) (Eq a_2 a_3)) (Ne (k1_funct_1 a a_3) k1_xboole_0)) False)))
% 186.49/186.81  Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 a_3 : Iota),
% 186.49/186.81    Or (Eq (m1_pboole a a_1) False)
% 186.49/186.81      (Or (Eq (r2_hidden a_2 (a_2_0_closure3 a_1 a)) True)
% 186.49/186.81        (Or (Eq (v1_xboole_0 a_1) True)
% 186.49/186.81          (Or (Eq (And (m1_subset_1 a_3 a_1) (Eq a_2 a_3)) False) (Eq (Ne (k1_funct_1 a a_3) k1_xboole_0) False))))
% 186.49/186.81  Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 a_3 : Iota),
% 186.49/186.81    Or (Eq (m1_pboole a a_1) False)
% 186.49/186.81      (Or (Eq (r2_hidden a_2 (a_2_0_closure3 a_1 a)) True)
% 186.49/186.81        (Or (Eq (v1_xboole_0 a_1) True)
% 186.49/186.81          (Or (Eq (Ne (k1_funct_1 a a_3) k1_xboole_0) False)
% 186.49/186.81            (Or (Eq (m1_subset_1 a_3 a_1) False) (Eq (Eq a_2 a_3) False)))))
% 186.49/186.81  Clause #124 (by clausification #[123]): ∀ (a a_1 a_2 a_3 : Iota),
% 186.49/186.81    Or (Eq (m1_pboole a a_1) False)
% 186.49/186.81      (Or (Eq (r2_hidden a_2 (a_2_0_closure3 a_1 a)) True)
% 186.49/186.81        (Or (Eq (v1_xboole_0 a_1) True)
% 186.49/186.81          (Or (Eq (m1_subset_1 a_3 a_1) False) (Or (Eq (Eq a_2 a_3) False) (Eq (k1_funct_1 a a_3) k1_xboole_0)))))
% 186.49/186.81  Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 a_3 : Iota),
% 186.49/186.81    Or (Eq (m1_pboole a a_1) False)
% 186.49/186.81      (Or (Eq (r2_hidden a_2 (a_2_0_closure3 a_1 a)) True)
% 186.49/186.81        (Or (Eq (v1_xboole_0 a_1) True)
% 186.49/186.81          (Or (Eq (m1_subset_1 a_3 a_1) False) (Or (Eq (k1_funct_1 a a_3) k1_xboole_0) (Ne a_2 a_3)))))
% 186.49/186.81  Clause #126 (by destructive equality resolution #[125]): ∀ (a a_1 a_2 : Iota),
% 186.49/186.81    Or (Eq (m1_pboole a a_1) False)
% 186.49/186.81      (Or (Eq (r2_hidden a_2 (a_2_0_closure3 a_1 a)) True)
% 186.49/186.81        (Or (Eq (v1_xboole_0 a_1) True) (Or (Eq (m1_subset_1 a_2 a_1) False) (Eq (k1_funct_1 a a_2) k1_xboole_0))))
% 186.58/186.84  Clause #141 (by clausification #[37]): ∀ (a a_1 : Iota),
% 186.58/186.84    Eq
% 186.58/186.84      (Not
% 186.58/186.84        (m1_pboole (skS.0 8 a a_1) (skS.0 0 a) →
% 186.58/186.84          ∀ (C : Iota),
% 186.58/186.84            m1_subset_1 C (skS.0 0 a) →
% 186.58/186.84              Not (r2_hidden C (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))) →
% 186.58/186.84                Eq (k1_funct_1 (skS.0 8 a a_1) C) k1_xboole_0))
% 186.58/186.84      True
% 186.58/186.84  Clause #142 (by clausification #[141]): ∀ (a a_1 : Iota),
% 186.58/186.84    Eq
% 186.58/186.84      (m1_pboole (skS.0 8 a a_1) (skS.0 0 a) →
% 186.58/186.84        ∀ (C : Iota),
% 186.58/186.84          m1_subset_1 C (skS.0 0 a) →
% 186.58/186.84            Not (r2_hidden C (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))) → Eq (k1_funct_1 (skS.0 8 a a_1) C) k1_xboole_0)
% 186.58/186.84      False
% 186.58/186.84  Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), Eq (m1_pboole (skS.0 8 a a_1) (skS.0 0 a)) True
% 186.58/186.84  Clause #144 (by clausification #[142]): ∀ (a a_1 : Iota),
% 186.58/186.84    Eq
% 186.58/186.84      (∀ (C : Iota),
% 186.58/186.84        m1_subset_1 C (skS.0 0 a) →
% 186.58/186.84          Not (r2_hidden C (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))) → Eq (k1_funct_1 (skS.0 8 a a_1) C) k1_xboole_0)
% 186.58/186.84      False
% 186.58/186.84  Clause #147 (by superposition #[143, 105]): ∀ (a a_1 : Iota),
% 186.58/186.84    Or (Eq (v1_xboole_0 (skS.0 0 a)) True)
% 186.58/186.84      (Or (Eq True False) (Eq (a_2_0_closure3 (skS.0 0 a) (skS.0 8 a a_1)) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))))
% 186.58/186.84  Clause #148 (by superposition #[143, 126]): ∀ (a a_1 a_2 : Iota),
% 186.58/186.84    Or (Eq True False)
% 186.58/186.84      (Or (Eq (r2_hidden a (a_2_0_closure3 (skS.0 0 a_1) (skS.0 8 a_1 a_2))) True)
% 186.58/186.84        (Or (Eq (v1_xboole_0 (skS.0 0 a_1)) True)
% 186.58/186.84          (Or (Eq (m1_subset_1 a (skS.0 0 a_1)) False) (Eq (k1_funct_1 (skS.0 8 a_1 a_2) a) k1_xboole_0))))
% 186.58/186.84  Clause #279 (by clausification #[144]): ∀ (a a_1 a_2 : Iota),
% 186.58/186.84    Eq
% 186.58/186.84      (Not
% 186.58/186.84        (m1_subset_1 (skS.0 12 a a_1 a_2) (skS.0 0 a) →
% 186.58/186.84          Not (r2_hidden (skS.0 12 a a_1 a_2) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))) →
% 186.58/186.84            Eq (k1_funct_1 (skS.0 8 a a_1) (skS.0 12 a a_1 a_2)) k1_xboole_0))
% 186.58/186.84      True
% 186.58/186.84  Clause #280 (by clausification #[279]): ∀ (a a_1 a_2 : Iota),
% 186.58/186.84    Eq
% 186.58/186.84      (m1_subset_1 (skS.0 12 a a_1 a_2) (skS.0 0 a) →
% 186.58/186.84        Not (r2_hidden (skS.0 12 a a_1 a_2) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))) →
% 186.58/186.84          Eq (k1_funct_1 (skS.0 8 a a_1) (skS.0 12 a a_1 a_2)) k1_xboole_0)
% 186.58/186.84      False
% 186.58/186.84  Clause #281 (by clausification #[280]): ∀ (a a_1 a_2 : Iota), Eq (m1_subset_1 (skS.0 12 a a_1 a_2) (skS.0 0 a)) True
% 186.58/186.84  Clause #282 (by clausification #[280]): ∀ (a a_1 a_2 : Iota),
% 186.58/186.84    Eq
% 186.58/186.84      (Not (r2_hidden (skS.0 12 a a_1 a_2) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))) →
% 186.58/186.84        Eq (k1_funct_1 (skS.0 8 a a_1) (skS.0 12 a a_1 a_2)) k1_xboole_0)
% 186.58/186.84      False
% 186.58/186.84  Clause #366 (by clausification #[147]): ∀ (a a_1 : Iota),
% 186.58/186.84    Or (Eq (v1_xboole_0 (skS.0 0 a)) True)
% 186.58/186.84      (Eq (a_2_0_closure3 (skS.0 0 a) (skS.0 8 a a_1)) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1)))
% 186.58/186.84  Clause #367 (by forward demodulation #[366, 38]): ∀ (a a_1 : Iota),
% 186.58/186.84    Or (Eq False True) (Eq (a_2_0_closure3 (skS.0 0 a) (skS.0 8 a a_1)) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1)))
% 186.58/186.84  Clause #368 (by clausification #[367]): ∀ (a a_1 : Iota), Eq (a_2_0_closure3 (skS.0 0 a) (skS.0 8 a a_1)) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))
% 186.58/186.84  Clause #420 (by clausification #[148]): ∀ (a a_1 a_2 : Iota),
% 186.58/186.84    Or (Eq (r2_hidden a (a_2_0_closure3 (skS.0 0 a_1) (skS.0 8 a_1 a_2))) True)
% 186.58/186.84      (Or (Eq (v1_xboole_0 (skS.0 0 a_1)) True)
% 186.58/186.84        (Or (Eq (m1_subset_1 a (skS.0 0 a_1)) False) (Eq (k1_funct_1 (skS.0 8 a_1 a_2) a) k1_xboole_0)))
% 186.58/186.84  Clause #421 (by forward demodulation #[420, 368]): ∀ (a a_1 a_2 : Iota),
% 186.58/186.84    Or (Eq (r2_hidden a (k1_closure3 (skS.0 0 a_1) (skS.0 8 a_1 a_2))) True)
% 186.58/186.84      (Or (Eq (v1_xboole_0 (skS.0 0 a_1)) True)
% 186.58/186.84        (Or (Eq (m1_subset_1 a (skS.0 0 a_1)) False) (Eq (k1_funct_1 (skS.0 8 a_1 a_2) a) k1_xboole_0)))
% 186.58/186.84  Clause #422 (by forward demodulation #[421, 38]): ∀ (a a_1 a_2 : Iota),
% 186.58/186.84    Or (Eq (r2_hidden a (k1_closure3 (skS.0 0 a_1) (skS.0 8 a_1 a_2))) True)
% 186.58/186.84      (Or (Eq False True) (Or (Eq (m1_subset_1 a (skS.0 0 a_1)) False) (Eq (k1_funct_1 (skS.0 8 a_1 a_2) a) k1_xboole_0)))
% 186.58/186.84  Clause #423 (by clausification #[422]): ∀ (a a_1 a_2 : Iota),
% 186.58/186.84    Or (Eq (r2_hidden a (k1_closure3 (skS.0 0 a_1) (skS.0 8 a_1 a_2))) True)
% 186.58/186.84      (Or (Eq (m1_subset_1 a (skS.0 0 a_1)) False) (Eq (k1_funct_1 (skS.0 8 a_1 a_2) a) k1_xboole_0))
% 186.88/187.16  Clause #424 (by superposition #[423, 281]): ∀ (a a_1 a_2 a_3 : Iota),
% 186.88/187.16    Or (Eq (r2_hidden (skS.0 12 a a_1 a_2) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_3))) True)
% 186.88/187.16      (Or (Eq (k1_funct_1 (skS.0 8 a a_3) (skS.0 12 a a_1 a_2)) k1_xboole_0) (Eq False True))
% 186.88/187.16  Clause #1003 (by clausification #[282]): ∀ (a a_1 a_2 : Iota), Eq (Not (r2_hidden (skS.0 12 a a_1 a_2) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1)))) True
% 186.88/187.16  Clause #1004 (by clausification #[282]): ∀ (a a_1 a_2 : Iota), Eq (Eq (k1_funct_1 (skS.0 8 a a_1) (skS.0 12 a a_1 a_2)) k1_xboole_0) False
% 186.88/187.16  Clause #1005 (by clausification #[1003]): ∀ (a a_1 a_2 : Iota), Eq (r2_hidden (skS.0 12 a a_1 a_2) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_1))) False
% 186.88/187.16  Clause #1014 (by clausification #[1004]): ∀ (a a_1 a_2 : Iota), Ne (k1_funct_1 (skS.0 8 a a_1) (skS.0 12 a a_1 a_2)) k1_xboole_0
% 186.88/187.16  Clause #34377 (by clausification #[424]): ∀ (a a_1 a_2 a_3 : Iota),
% 186.88/187.16    Or (Eq (r2_hidden (skS.0 12 a a_1 a_2) (k1_closure3 (skS.0 0 a) (skS.0 8 a a_3))) True)
% 186.88/187.16      (Eq (k1_funct_1 (skS.0 8 a a_3) (skS.0 12 a a_1 a_2)) k1_xboole_0)
% 186.88/187.16  Clause #34378 (by superposition #[34377, 1005]): ∀ (a a_1 a_2 : Iota), Or (Eq (k1_funct_1 (skS.0 8 a a_1) (skS.0 12 a a_1 a_2)) k1_xboole_0) (Eq True False)
% 186.88/187.16  Clause #34557 (by clausification #[34378]): ∀ (a a_1 a_2 : Iota), Eq (k1_funct_1 (skS.0 8 a a_1) (skS.0 12 a a_1 a_2)) k1_xboole_0
% 186.88/187.16  Clause #34558 (by forward contextual literal cutting #[34557, 1014]): False
% 186.88/187.16  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------