%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:06:26 AM UTC 2026 % Result : Theorem 11.25s 11.53s % Output : Proof 11.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.04 % Command : duper %s % 0.10/0.36 % Computer : n026.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 14:12:12 UTC 2026 % 0.10/0.36 % CPUTime : % 11.25/11.53 SZS status Theorem for theBenchmark.p % 11.25/11.53 SZS output start Proof for theBenchmark.p % 11.25/11.53 Clause #0 (by assumption #[]): Eq % 11.25/11.53 (∀ (P X Y A T E : Iota), % 11.25/11.53 And (And (And (And (And (And (perm P) (strong P)) (aee P X)) (aer P Y)) (act P A)) (tgt P T)) (activates E P) → % 11.25/11.53 Exists fun RhoI => % 11.25/11.53 Exists fun Im => % 11.25/11.53 Exists fun Db => % 11.25/11.53 And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And (And (And (And (founds_imm E RhoI P) (immunity Im)) (bearer Im X)) (cnt Im A T)) % 11.25/11.53 (part_of Im RhoI)) % 11.25/11.53 (disability Db)) % 11.25/11.53 (bearer Db Y)) % 11.25/11.53 (cnt Db A T)) % 11.25/11.53 (part_of Db RhoI)) % 11.25/11.53 True % 11.25/11.53 Clause #7 (by assumption #[]): Eq (perm p1) True % 11.25/11.53 Clause #8 (by assumption #[]): Eq (strong p1) True % 11.25/11.53 Clause #9 (by assumption #[]): Eq (aee p1 bibliothek) True % 11.25/11.53 Clause #10 (by assumption #[]): Eq (aer p1 museen) True % 11.25/11.53 Clause #11 (by assumption #[]): Eq (act p1 read) True % 11.25/11.53 Clause #12 (by assumption #[]): Eq (tgt p1 museum_api) True % 11.25/11.53 Clause #13 (by assumption #[]): Eq (activates e1 p1) True % 11.25/11.53 Clause #14 (by assumption #[]): Eq % 11.25/11.53 (Not % 11.25/11.53 (Exists fun RhoI => % 11.25/11.53 Exists fun Db => % 11.25/11.53 And (And (And (And (founds_imm e1 RhoI p1) (disability Db)) (bearer Db museen)) (cnt Db read museum_api)) % 11.25/11.53 (part_of Db RhoI))) % 11.25/11.53 True % 11.25/11.53 Clause #15 (by clausification #[0]): ∀ (a : Iota), % 11.25/11.53 Eq % 11.25/11.53 (∀ (X Y A T E : Iota), % 11.25/11.53 And (And (And (And (And (And (perm a) (strong a)) (aee a X)) (aer a Y)) (act a A)) (tgt a T)) (activates E a) → % 11.25/11.53 Exists fun RhoI => % 11.25/11.53 Exists fun Im => % 11.25/11.53 Exists fun Db => % 11.25/11.53 And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And (And (And (And (founds_imm E RhoI a) (immunity Im)) (bearer Im X)) (cnt Im A T)) % 11.25/11.53 (part_of Im RhoI)) % 11.25/11.53 (disability Db)) % 11.25/11.53 (bearer Db Y)) % 11.25/11.53 (cnt Db A T)) % 11.25/11.53 (part_of Db RhoI)) % 11.25/11.53 True % 11.25/11.53 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), % 11.25/11.53 Eq % 11.25/11.53 (∀ (Y A T E : Iota), % 11.25/11.53 And (And (And (And (And (And (perm a) (strong a)) (aee a a_1)) (aer a Y)) (act a A)) (tgt a T)) (activates E a) → % 11.25/11.53 Exists fun RhoI => % 11.25/11.53 Exists fun Im => % 11.25/11.53 Exists fun Db => % 11.25/11.53 And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And (And (And (And (founds_imm E RhoI a) (immunity Im)) (bearer Im a_1)) (cnt Im A T)) % 11.25/11.53 (part_of Im RhoI)) % 11.25/11.53 (disability Db)) % 11.25/11.53 (bearer Db Y)) % 11.25/11.53 (cnt Db A T)) % 11.25/11.53 (part_of Db RhoI)) % 11.25/11.53 True % 11.25/11.53 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 : Iota), % 11.25/11.53 Eq % 11.25/11.53 (∀ (A T E : Iota), % 11.25/11.53 And (And (And (And (And (And (perm a) (strong a)) (aee a a_1)) (aer a a_2)) (act a A)) (tgt a T)) % 11.25/11.53 (activates E a) → % 11.25/11.53 Exists fun RhoI => % 11.25/11.53 Exists fun Im => % 11.25/11.53 Exists fun Db => % 11.25/11.53 And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And (And (And (And (founds_imm E RhoI a) (immunity Im)) (bearer Im a_1)) (cnt Im A T)) % 11.25/11.53 (part_of Im RhoI)) % 11.25/11.53 (disability Db)) % 11.25/11.53 (bearer Db a_2)) % 11.25/11.53 (cnt Db A T)) % 11.25/11.53 (part_of Db RhoI)) % 11.25/11.53 True % 11.25/11.53 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 a_3 : Iota), % 11.25/11.53 Eq % 11.25/11.53 (∀ (T E : Iota), % 11.25/11.53 And (And (And (And (And (And (perm a) (strong a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a T)) % 11.25/11.53 (activates E a) → % 11.25/11.53 Exists fun RhoI => % 11.25/11.53 Exists fun Im => % 11.25/11.53 Exists fun Db => % 11.25/11.53 And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And % 11.25/11.53 (And (And (And (And (founds_imm E RhoI a) (immunity Im)) (bearer Im a_1)) (cnt Im a_3 T)) % 11.25/11.53 (part_of Im RhoI)) % 11.25/11.53 (disability Db)) % 11.25/11.53 (bearer Db a_2)) % 11.25/11.53 (cnt Db a_3 T)) % 11.25/11.53 (part_of Db RhoI)) % 11.25/11.53 True % 11.25/11.58 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.25/11.58 Eq % 11.25/11.58 (∀ (E : Iota), % 11.25/11.58 And (And (And (And (And (And (perm a) (strong a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a a_4)) % 11.25/11.58 (activates E a) → % 11.25/11.58 Exists fun RhoI => % 11.25/11.58 Exists fun Im => % 11.25/11.58 Exists fun Db => % 11.25/11.58 And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And (And (And (And (founds_imm E RhoI a) (immunity Im)) (bearer Im a_1)) (cnt Im a_3 a_4)) % 11.25/11.58 (part_of Im RhoI)) % 11.25/11.58 (disability Db)) % 11.25/11.58 (bearer Db a_2)) % 11.25/11.58 (cnt Db a_3 a_4)) % 11.25/11.58 (part_of Db RhoI)) % 11.25/11.58 True % 11.25/11.58 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.25/11.58 Eq % 11.25/11.58 (And (And (And (And (And (And (perm a) (strong a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a a_4)) % 11.25/11.58 (activates a_5 a) → % 11.25/11.58 Exists fun RhoI => % 11.25/11.58 Exists fun Im => % 11.25/11.58 Exists fun Db => % 11.25/11.58 And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And (And (And (And (founds_imm a_5 RhoI a) (immunity Im)) (bearer Im a_1)) (cnt Im a_3 a_4)) % 11.25/11.58 (part_of Im RhoI)) % 11.25/11.58 (disability Db)) % 11.25/11.58 (bearer Db a_2)) % 11.25/11.58 (cnt Db a_3 a_4)) % 11.25/11.58 (part_of Db RhoI)) % 11.25/11.58 True % 11.25/11.58 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.25/11.58 Or % 11.25/11.58 (Eq % 11.25/11.58 (And (And (And (And (And (And (perm a) (strong a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a a_4)) % 11.25/11.58 (activates a_5 a)) % 11.25/11.58 False) % 11.25/11.58 (Eq % 11.25/11.58 (Exists fun RhoI => % 11.25/11.58 Exists fun Im => % 11.25/11.58 Exists fun Db => % 11.25/11.58 And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And (And (And (And (founds_imm a_5 RhoI a) (immunity Im)) (bearer Im a_1)) (cnt Im a_3 a_4)) % 11.25/11.58 (part_of Im RhoI)) % 11.25/11.58 (disability Db)) % 11.25/11.58 (bearer Db a_2)) % 11.25/11.58 (cnt Db a_3 a_4)) % 11.25/11.58 (part_of Db RhoI)) % 11.25/11.58 True) % 11.25/11.58 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.25/11.58 Or % 11.25/11.58 (Eq % 11.25/11.58 (Exists fun RhoI => % 11.25/11.58 Exists fun Im => % 11.25/11.58 Exists fun Db => % 11.25/11.58 And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And (And (And (And (founds_imm a RhoI a_1) (immunity Im)) (bearer Im a_2)) (cnt Im a_3 a_4)) % 11.25/11.58 (part_of Im RhoI)) % 11.25/11.58 (disability Db)) % 11.25/11.58 (bearer Db a_5)) % 11.25/11.58 (cnt Db a_3 a_4)) % 11.25/11.58 (part_of Db RhoI)) % 11.25/11.58 True) % 11.25/11.58 (Or % 11.25/11.58 (Eq (And (And (And (And (And (perm a_1) (strong a_1)) (aee a_1 a_2)) (aer a_1 a_5)) (act a_1 a_3)) (tgt a_1 a_4)) % 11.25/11.58 False) % 11.25/11.58 (Eq (activates a a_1) False)) % 11.25/11.58 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.25/11.58 Or (Eq (And (And (And (And (And (perm a) (strong a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a a_4)) False) % 11.25/11.58 (Or (Eq (activates a_5 a) False) % 11.25/11.58 (Eq % 11.25/11.58 (Exists fun Im => % 11.25/11.58 Exists fun Db => % 11.25/11.58 And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And (And (founds_imm a_5 (skS.0 0 a_5 a a_1 a_3 a_4 a_2 a_6) a) (immunity Im)) (bearer Im a_1)) % 11.25/11.58 (cnt Im a_3 a_4)) % 11.25/11.58 (part_of Im (skS.0 0 a_5 a a_1 a_3 a_4 a_2 a_6))) % 11.25/11.58 (disability Db)) % 11.25/11.58 (bearer Db a_2)) % 11.25/11.58 (cnt Db a_3 a_4)) % 11.25/11.58 (part_of Db (skS.0 0 a_5 a a_1 a_3 a_4 a_2 a_6))) % 11.25/11.58 True)) % 11.25/11.58 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.25/11.58 Or (Eq (activates a a_1) False) % 11.25/11.58 (Or % 11.25/11.58 (Eq % 11.25/11.58 (Exists fun Im => % 11.25/11.58 Exists fun Db => % 11.25/11.58 And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And % 11.25/11.58 (And (And (founds_imm a (skS.0 0 a a_1 a_2 a_3 a_4 a_5 a_6) a_1) (immunity Im)) (bearer Im a_2)) % 11.35/11.63 (cnt Im a_3 a_4)) % 11.35/11.63 (part_of Im (skS.0 0 a a_1 a_2 a_3 a_4 a_5 a_6))) % 11.35/11.63 (disability Db)) % 11.35/11.63 (bearer Db a_5)) % 11.35/11.63 (cnt Db a_3 a_4)) % 11.35/11.63 (part_of Db (skS.0 0 a a_1 a_2 a_3 a_4 a_5 a_6))) % 11.35/11.63 True) % 11.35/11.63 (Or (Eq (And (And (And (And (perm a_1) (strong a_1)) (aee a_1 a_2)) (aer a_1 a_5)) (act a_1 a_3)) False) % 11.35/11.63 (Eq (tgt a_1 a_4) False))) % 11.35/11.63 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.35/11.63 Or (Eq (activates a a_1) False) % 11.35/11.63 (Or (Eq (And (And (And (And (perm a_1) (strong a_1)) (aee a_1 a_2)) (aer a_1 a_3)) (act a_1 a_4)) False) % 11.35/11.63 (Or (Eq (tgt a_1 a_5) False) % 11.35/11.63 (Eq % 11.35/11.63 (Exists fun Db => % 11.35/11.63 And % 11.35/11.63 (And % 11.35/11.63 (And % 11.35/11.63 (And % 11.35/11.63 (And % 11.35/11.63 (And % 11.35/11.63 (And % 11.35/11.63 (And (founds_imm a (skS.0 0 a a_1 a_2 a_4 a_5 a_3 a_6) a_1) % 11.35/11.63 (immunity (skS.0 1 a a_1 a_2 a_4 a_5 a_3 a_6 a_7))) % 11.35/11.64 (bearer (skS.0 1 a a_1 a_2 a_4 a_5 a_3 a_6 a_7) a_2)) % 11.35/11.64 (cnt (skS.0 1 a a_1 a_2 a_4 a_5 a_3 a_6 a_7) a_4 a_5)) % 11.35/11.64 (part_of (skS.0 1 a a_1 a_2 a_4 a_5 a_3 a_6 a_7) (skS.0 0 a a_1 a_2 a_4 a_5 a_3 a_6))) % 11.35/11.64 (disability Db)) % 11.35/11.64 (bearer Db a_3)) % 11.35/11.64 (cnt Db a_4 a_5)) % 11.35/11.64 (part_of Db (skS.0 0 a a_1 a_2 a_4 a_5 a_3 a_6))) % 11.35/11.64 True))) % 11.35/11.64 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.35/11.64 Or (Eq (activates a a_1) False) % 11.35/11.64 (Or (Eq (tgt a_1 a_2) False) % 11.35/11.64 (Or % 11.35/11.64 (Eq % 11.35/11.64 (Exists fun Db => % 11.35/11.64 And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And (founds_imm a (skS.0 0 a a_1 a_3 a_4 a_2 a_5 a_6) a_1) % 11.35/11.64 (immunity (skS.0 1 a a_1 a_3 a_4 a_2 a_5 a_6 a_7))) % 11.35/11.64 (bearer (skS.0 1 a a_1 a_3 a_4 a_2 a_5 a_6 a_7) a_3)) % 11.35/11.64 (cnt (skS.0 1 a a_1 a_3 a_4 a_2 a_5 a_6 a_7) a_4 a_2)) % 11.35/11.64 (part_of (skS.0 1 a a_1 a_3 a_4 a_2 a_5 a_6 a_7) (skS.0 0 a a_1 a_3 a_4 a_2 a_5 a_6))) % 11.35/11.64 (disability Db)) % 11.35/11.64 (bearer Db a_5)) % 11.35/11.64 (cnt Db a_4 a_2)) % 11.35/11.64 (part_of Db (skS.0 0 a a_1 a_3 a_4 a_2 a_5 a_6))) % 11.35/11.64 True) % 11.35/11.64 (Or (Eq (And (And (And (perm a_1) (strong a_1)) (aee a_1 a_3)) (aer a_1 a_5)) False) (Eq (act a_1 a_4) False)))) % 11.35/11.64 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.35/11.64 Or (Eq (activates a a_1) False) % 11.35/11.64 (Or (Eq (tgt a_1 a_2) False) % 11.35/11.64 (Or (Eq (And (And (And (perm a_1) (strong a_1)) (aee a_1 a_3)) (aer a_1 a_4)) False) % 11.35/11.64 (Or (Eq (act a_1 a_5) False) % 11.35/11.64 (Eq % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And % 11.35/11.64 (And (founds_imm a (skS.0 0 a a_1 a_3 a_5 a_2 a_4 a_6) a_1) % 11.35/11.64 (immunity (skS.0 1 a a_1 a_3 a_5 a_2 a_4 a_6 a_7))) % 11.35/11.64 (bearer (skS.0 1 a a_1 a_3 a_5 a_2 a_4 a_6 a_7) a_3)) % 11.35/11.64 (cnt (skS.0 1 a a_1 a_3 a_5 a_2 a_4 a_6 a_7) a_5 a_2)) % 11.35/11.64 (part_of (skS.0 1 a a_1 a_3 a_5 a_2 a_4 a_6 a_7) (skS.0 0 a a_1 a_3 a_5 a_2 a_4 a_6))) % 11.35/11.64 (disability (skS.0 2 a a_1 a_3 a_5 a_2 a_4 a_6 a_7 a_8))) % 11.35/11.64 (bearer (skS.0 2 a a_1 a_3 a_5 a_2 a_4 a_6 a_7 a_8) a_4)) % 11.35/11.64 (cnt (skS.0 2 a a_1 a_3 a_5 a_2 a_4 a_6 a_7 a_8) a_5 a_2)) % 11.35/11.64 (part_of (skS.0 2 a a_1 a_3 a_5 a_2 a_4 a_6 a_7 a_8) (skS.0 0 a a_1 a_3 a_5 a_2 a_4 a_6))) % 11.35/11.64 True)))) % 11.35/11.64 Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.35/11.64 Or (Eq (activates a a_1) False) % 11.35/11.64 (Or (Eq (tgt a_1 a_2) False) % 11.35/11.64 (Or (Eq (act a_1 a_3) False) % 11.35/11.64 (Or % 11.35/11.64 (Eq % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And (founds_imm a (skS.0 0 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 11.35/11.68 (immunity (skS.0 1 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 11.35/11.68 (bearer (skS.0 1 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 11.35/11.68 (cnt (skS.0 1 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_3 a_2)) % 11.35/11.68 (part_of (skS.0 1 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 0 a a_1 a_4 a_3 a_2 a_5 a_6))) % 11.35/11.68 (disability (skS.0 2 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8))) % 11.35/11.68 (bearer (skS.0 2 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_5)) % 11.35/11.68 (cnt (skS.0 2 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_3 a_2)) % 11.35/11.68 (part_of (skS.0 2 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (skS.0 0 a a_1 a_4 a_3 a_2 a_5 a_6))) % 11.35/11.68 True) % 11.35/11.68 (Or (Eq (And (And (perm a_1) (strong a_1)) (aee a_1 a_4)) False) (Eq (aer a_1 a_5) False))))) % 11.35/11.68 Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.35/11.68 Or (Eq (activates a a_1) False) % 11.35/11.68 (Or (Eq (tgt a_1 a_2) False) % 11.35/11.68 (Or (Eq (act a_1 a_3) False) % 11.35/11.68 (Or (Eq (And (And (perm a_1) (strong a_1)) (aee a_1 a_4)) False) % 11.35/11.68 (Or (Eq (aer a_1 a_5) False) % 11.35/11.68 (Eq (part_of (skS.0 2 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (skS.0 0 a a_1 a_4 a_3 a_2 a_5 a_6)) True))))) % 11.35/11.68 Clause #30 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.35/11.68 Or (Eq (activates a a_1) False) % 11.35/11.68 (Or (Eq (tgt a_1 a_2) False) % 11.35/11.68 (Or (Eq (act a_1 a_3) False) % 11.35/11.68 (Or (Eq (And (And (perm a_1) (strong a_1)) (aee a_1 a_4)) False) % 11.35/11.68 (Or (Eq (aer a_1 a_5) False) % 11.35/11.68 (Eq % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And % 11.35/11.68 (And (founds_imm a (skS.0 0 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 11.35/11.68 (immunity (skS.0 1 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 11.35/11.68 (bearer (skS.0 1 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 11.35/11.68 (cnt (skS.0 1 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_3 a_2)) % 11.35/11.68 (part_of (skS.0 1 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 0 a a_1 a_4 a_3 a_2 a_5 a_6))) % 11.35/11.68 (disability (skS.0 2 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8))) % 11.35/11.68 (bearer (skS.0 2 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_5)) % 11.35/11.68 (cnt (skS.0 2 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_3 a_2)) % 11.35/11.68 True))))) % 11.35/11.68 Clause #31 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.35/11.68 Or (Eq (activates a a_1) False) % 11.35/11.68 (Or (Eq (tgt a_1 a_2) False) % 11.35/11.68 (Or (Eq (act a_1 a_3) False) % 11.35/11.68 (Or (Eq (aer a_1 a_4) False) % 11.35/11.68 (Or (Eq (part_of (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6)) True) % 11.35/11.68 (Or (Eq (And (perm a_1) (strong a_1)) False) (Eq (aee a_1 a_5) False)))))) % 11.35/11.68 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.35/11.68 Or (Eq (activates a a_1) False) % 11.35/11.68 (Or (Eq (tgt a_1 a_2) False) % 11.35/11.68 (Or (Eq (act a_1 a_3) False) % 11.35/11.68 (Or (Eq (aer a_1 a_4) False) % 11.35/11.68 (Or (Eq (part_of (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6)) True) % 11.35/11.68 (Or (Eq (aee a_1 a_5) False) (Or (Eq (perm a_1) False) (Eq (strong a_1) False))))))) % 11.35/11.68 Clause #33 (by superposition #[13, 32]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.35/11.68 Or (Eq (tgt p1 a) False) % 11.35/11.68 (Or (Eq (act p1 a_1) False) % 11.35/11.68 (Or (Eq (aer p1 a_2) False) % 11.35/11.68 (Or (Eq (part_of (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4)) True) % 11.35/11.68 (Or (Eq (aee p1 a_3) False) (Or (Eq (perm p1) False) (Or (Eq (strong p1) False) (Eq False True))))))) % 11.35/11.68 Clause #34 (by clausification #[14]): Eq % 11.35/11.68 (Exists fun RhoI => % 11.35/11.68 Exists fun Db => % 11.35/11.68 And (And (And (And (founds_imm e1 RhoI p1) (disability Db)) (bearer Db museen)) (cnt Db read museum_api)) % 11.35/11.68 (part_of Db RhoI)) % 11.45/11.75 False % 11.45/11.75 Clause #35 (by clausification #[34]): ∀ (a : Iota), % 11.45/11.75 Eq % 11.45/11.75 (Exists fun Db => % 11.45/11.75 And (And (And (And (founds_imm e1 a p1) (disability Db)) (bearer Db museen)) (cnt Db read museum_api)) % 11.45/11.75 (part_of Db a)) % 11.45/11.75 False % 11.45/11.75 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 11.45/11.75 Eq % 11.45/11.75 (And (And (And (And (founds_imm e1 a p1) (disability a_1)) (bearer a_1 museen)) (cnt a_1 read museum_api)) % 11.45/11.75 (part_of a_1 a)) % 11.45/11.75 False % 11.45/11.75 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 11.45/11.75 Or (Eq (And (And (And (founds_imm e1 a p1) (disability a_1)) (bearer a_1 museen)) (cnt a_1 read museum_api)) False) % 11.45/11.75 (Eq (part_of a_1 a) False) % 11.45/11.75 Clause #38 (by clausification #[37]): ∀ (a a_1 : Iota), % 11.45/11.75 Or (Eq (part_of a a_1) False) % 11.45/11.75 (Or (Eq (And (And (founds_imm e1 a_1 p1) (disability a)) (bearer a museen)) False) % 11.45/11.75 (Eq (cnt a read museum_api) False)) % 11.45/11.75 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), % 11.45/11.75 Or (Eq (part_of a a_1) False) % 11.45/11.75 (Or (Eq (cnt a read museum_api) False) % 11.45/11.75 (Or (Eq (And (founds_imm e1 a_1 p1) (disability a)) False) (Eq (bearer a museen) False))) % 11.45/11.75 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), % 11.45/11.75 Or (Eq (part_of a a_1) False) % 11.45/11.75 (Or (Eq (cnt a read museum_api) False) % 11.45/11.75 (Or (Eq (bearer a museen) False) (Or (Eq (founds_imm e1 a_1 p1) False) (Eq (disability a) False)))) % 11.45/11.75 Clause #41 (by clausification #[33]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.75 Or (Eq (tgt p1 a) False) % 11.45/11.75 (Or (Eq (act p1 a_1) False) % 11.45/11.75 (Or (Eq (aer p1 a_2) False) % 11.45/11.75 (Or (Eq (part_of (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4)) True) % 11.45/11.75 (Or (Eq (aee p1 a_3) False) (Or (Eq (perm p1) False) (Eq (strong p1) False)))))) % 11.45/11.75 Clause #42 (by forward demodulation #[41, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.75 Or (Eq (tgt p1 a) False) % 11.45/11.75 (Or (Eq (act p1 a_1) False) % 11.45/11.75 (Or (Eq (aer p1 a_2) False) % 11.45/11.75 (Or (Eq (part_of (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4)) True) % 11.45/11.75 (Or (Eq (aee p1 a_3) False) (Or (Eq True False) (Eq (strong p1) False)))))) % 11.45/11.75 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.75 Or (Eq (tgt p1 a) False) % 11.45/11.75 (Or (Eq (act p1 a_1) False) % 11.45/11.75 (Or (Eq (aer p1 a_2) False) % 11.45/11.75 (Or (Eq (part_of (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4)) True) % 11.45/11.75 (Or (Eq (aee p1 a_3) False) (Eq (strong p1) False))))) % 11.45/11.75 Clause #44 (by forward demodulation #[43, 8]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.75 Or (Eq (tgt p1 a) False) % 11.45/11.75 (Or (Eq (act p1 a_1) False) % 11.45/11.75 (Or (Eq (aer p1 a_2) False) % 11.45/11.75 (Or (Eq (part_of (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4)) True) % 11.45/11.75 (Or (Eq (aee p1 a_3) False) (Eq True False))))) % 11.45/11.75 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.75 Or (Eq (tgt p1 a) False) % 11.45/11.75 (Or (Eq (act p1 a_1) False) % 11.45/11.75 (Or (Eq (aer p1 a_2) False) % 11.45/11.75 (Or (Eq (part_of (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4)) True) % 11.45/11.75 (Eq (aee p1 a_3) False)))) % 11.45/11.75 Clause #46 (by superposition #[45, 12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.45/11.75 Or (Eq (act p1 a) False) % 11.45/11.75 (Or (Eq (aer p1 a_1) False) % 11.45/11.75 (Or (Eq (part_of (skS.0 2 e1 p1 a_2 a museum_api a_1 a_3 a_4 a_5) (skS.0 0 e1 p1 a_2 a museum_api a_1 a_3)) True) % 11.45/11.75 (Or (Eq (aee p1 a_2) False) (Eq False True)))) % 11.45/11.75 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.45/11.75 Or (Eq (act p1 a) False) % 11.45/11.75 (Or (Eq (aer p1 a_1) False) % 11.45/11.75 (Or (Eq (part_of (skS.0 2 e1 p1 a_2 a museum_api a_1 a_3 a_4 a_5) (skS.0 0 e1 p1 a_2 a museum_api a_1 a_3)) True) % 11.45/11.75 (Eq (aee p1 a_2) False))) % 11.45/11.75 Clause #48 (by superposition #[47, 11]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.45/11.75 Or (Eq (aer p1 a) False) % 11.45/11.75 (Or (Eq (part_of (skS.0 2 e1 p1 a_1 read museum_api a a_2 a_3 a_4) (skS.0 0 e1 p1 a_1 read museum_api a a_2)) True) % 11.45/11.75 (Or (Eq (aee p1 a_1) False) (Eq False True))) % 11.45/11.75 Clause #49 (by clausification #[30]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.45/11.75 Or (Eq (activates a a_1) False) % 11.45/11.75 (Or (Eq (tgt a_1 a_2) False) % 11.45/11.79 (Or (Eq (act a_1 a_3) False) % 11.45/11.79 (Or (Eq (aer a_1 a_4) False) % 11.45/11.79 (Or % 11.45/11.79 (Eq % 11.45/11.79 (And % 11.45/11.79 (And % 11.45/11.79 (And % 11.45/11.79 (And % 11.45/11.79 (And % 11.45/11.79 (And % 11.45/11.79 (And (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 11.45/11.79 (immunity (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 11.45/11.79 (bearer (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_5)) % 11.45/11.79 (cnt (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_3 a_2)) % 11.45/11.79 (part_of (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6))) % 11.45/11.79 (disability (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8))) % 11.45/11.79 (bearer (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) a_4)) % 11.45/11.79 (cnt (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) a_3 a_2)) % 11.45/11.79 True) % 11.45/11.79 (Or (Eq (And (perm a_1) (strong a_1)) False) (Eq (aee a_1 a_5) False)))))) % 11.45/11.80 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.45/11.80 Or (Eq (activates a a_1) False) % 11.45/11.80 (Or (Eq (tgt a_1 a_2) False) % 11.45/11.80 (Or (Eq (act a_1 a_3) False) % 11.45/11.80 (Or (Eq (aer a_1 a_4) False) % 11.45/11.80 (Or (Eq (And (perm a_1) (strong a_1)) False) % 11.45/11.80 (Or (Eq (aee a_1 a_5) False) (Eq (cnt (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) a_3 a_2) True)))))) % 11.45/11.80 Clause #51 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.45/11.80 Or (Eq (activates a a_1) False) % 11.45/11.80 (Or (Eq (tgt a_1 a_2) False) % 11.45/11.80 (Or (Eq (act a_1 a_3) False) % 11.45/11.80 (Or (Eq (aer a_1 a_4) False) % 11.45/11.80 (Or (Eq (And (perm a_1) (strong a_1)) False) % 11.45/11.80 (Or (Eq (aee a_1 a_5) False) % 11.45/11.80 (Eq % 11.45/11.80 (And % 11.45/11.80 (And % 11.45/11.80 (And % 11.45/11.80 (And % 11.45/11.80 (And % 11.45/11.80 (And (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 11.45/11.80 (immunity (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 11.45/11.80 (bearer (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_5)) % 11.45/11.80 (cnt (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_3 a_2)) % 11.45/11.80 (part_of (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6))) % 11.45/11.80 (disability (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8))) % 11.45/11.80 (bearer (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) a_4)) % 11.45/11.80 True)))))) % 11.45/11.80 Clause #52 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.45/11.80 Or (Eq (activates a a_1) False) % 11.45/11.80 (Or (Eq (tgt a_1 a_2) False) % 11.45/11.80 (Or (Eq (act a_1 a_3) False) % 11.45/11.80 (Or (Eq (aer a_1 a_4) False) % 11.45/11.80 (Or (Eq (aee a_1 a_5) False) % 11.45/11.80 (Or (Eq (cnt (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) a_3 a_2) True) % 11.45/11.80 (Or (Eq (perm a_1) False) (Eq (strong a_1) False))))))) % 11.45/11.80 Clause #53 (by superposition #[52, 13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.80 Or (Eq (tgt p1 a) False) % 11.45/11.80 (Or (Eq (act p1 a_1) False) % 11.45/11.80 (Or (Eq (aer p1 a_2) False) % 11.45/11.80 (Or (Eq (aee p1 a_3) False) % 11.45/11.80 (Or (Eq (cnt (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_1 a) True) % 11.45/11.80 (Or (Eq (perm p1) False) (Or (Eq (strong p1) False) (Eq False True))))))) % 11.45/11.80 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.80 Or (Eq (tgt p1 a) False) % 11.45/11.80 (Or (Eq (act p1 a_1) False) % 11.45/11.80 (Or (Eq (aer p1 a_2) False) % 11.45/11.80 (Or (Eq (aee p1 a_3) False) % 11.45/11.80 (Or (Eq (cnt (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_1 a) True) % 11.45/11.80 (Or (Eq (perm p1) False) (Eq (strong p1) False)))))) % 11.45/11.80 Clause #55 (by forward demodulation #[54, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.80 Or (Eq (tgt p1 a) False) % 11.45/11.80 (Or (Eq (act p1 a_1) False) % 11.45/11.80 (Or (Eq (aer p1 a_2) False) % 11.45/11.80 (Or (Eq (aee p1 a_3) False) % 11.45/11.80 (Or (Eq (cnt (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_1 a) True) % 11.45/11.80 (Or (Eq True False) (Eq (strong p1) False)))))) % 11.45/11.80 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.80 Or (Eq (tgt p1 a) False) % 11.55/11.85 (Or (Eq (act p1 a_1) False) % 11.55/11.85 (Or (Eq (aer p1 a_2) False) % 11.55/11.85 (Or (Eq (aee p1 a_3) False) % 11.55/11.85 (Or (Eq (cnt (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_1 a) True) (Eq (strong p1) False))))) % 11.55/11.85 Clause #57 (by forward demodulation #[56, 8]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.55/11.85 Or (Eq (tgt p1 a) False) % 11.55/11.85 (Or (Eq (act p1 a_1) False) % 11.55/11.85 (Or (Eq (aer p1 a_2) False) % 11.55/11.85 (Or (Eq (aee p1 a_3) False) % 11.55/11.85 (Or (Eq (cnt (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_1 a) True) (Eq True False))))) % 11.55/11.85 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.55/11.85 Or (Eq (tgt p1 a) False) % 11.55/11.85 (Or (Eq (act p1 a_1) False) % 11.55/11.85 (Or (Eq (aer p1 a_2) False) % 11.55/11.85 (Or (Eq (aee p1 a_3) False) (Eq (cnt (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_1 a) True)))) % 11.55/11.85 Clause #59 (by superposition #[58, 12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.55/11.85 Or (Eq (act p1 a) False) % 11.55/11.85 (Or (Eq (aer p1 a_1) False) % 11.55/11.85 (Or (Eq (aee p1 a_2) False) % 11.55/11.85 (Or (Eq (cnt (skS.0 2 e1 p1 a_2 a museum_api a_1 a_3 a_4 a_5) a museum_api) True) (Eq False True)))) % 11.55/11.85 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.55/11.85 Or (Eq (act p1 a) False) % 11.55/11.85 (Or (Eq (aer p1 a_1) False) % 11.55/11.85 (Or (Eq (aee p1 a_2) False) (Eq (cnt (skS.0 2 e1 p1 a_2 a museum_api a_1 a_3 a_4 a_5) a museum_api) True))) % 11.55/11.85 Clause #61 (by superposition #[60, 11]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.55/11.85 Or (Eq (aer p1 a) False) % 11.55/11.85 (Or (Eq (aee p1 a_1) False) % 11.55/11.85 (Or (Eq (cnt (skS.0 2 e1 p1 a_1 read museum_api a a_2 a_3 a_4) read museum_api) True) (Eq False True))) % 11.55/11.85 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.55/11.85 Or (Eq (aer p1 a) False) % 11.55/11.85 (Or (Eq (aee p1 a_1) False) (Eq (cnt (skS.0 2 e1 p1 a_1 read museum_api a a_2 a_3 a_4) read museum_api) True)) % 11.55/11.85 Clause #63 (by superposition #[62, 10]): ∀ (a a_1 a_2 a_3 : Iota), % 11.55/11.85 Or (Eq (aee p1 a) False) % 11.55/11.85 (Or (Eq (cnt (skS.0 2 e1 p1 a read museum_api museen a_1 a_2 a_3) read museum_api) True) (Eq False True)) % 11.55/11.85 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 : Iota), % 11.55/11.85 Or (Eq (aee p1 a) False) (Eq (cnt (skS.0 2 e1 p1 a read museum_api museen a_1 a_2 a_3) read museum_api) True) % 11.55/11.85 Clause #65 (by superposition #[64, 9]): ∀ (a a_1 a_2 : Iota), % 11.55/11.85 Or (Eq (cnt (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) read museum_api) True) (Eq False True) % 11.55/11.85 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 : Iota), Eq (cnt (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) read museum_api) True % 11.55/11.85 Clause #67 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.55/11.85 Or (Eq (aer p1 a) False) % 11.55/11.85 (Or (Eq (part_of (skS.0 2 e1 p1 a_1 read museum_api a a_2 a_3 a_4) (skS.0 0 e1 p1 a_1 read museum_api a a_2)) True) % 11.55/11.85 (Eq (aee p1 a_1) False)) % 11.55/11.85 Clause #68 (by superposition #[67, 10]): ∀ (a a_1 a_2 a_3 : Iota), % 11.55/11.85 Or % 11.55/11.85 (Eq (part_of (skS.0 2 e1 p1 a read museum_api museen a_1 a_2 a_3) (skS.0 0 e1 p1 a read museum_api museen a_1)) % 11.55/11.85 True) % 11.55/11.85 (Or (Eq (aee p1 a) False) (Eq False True)) % 11.55/11.85 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 a_3 : Iota), % 11.55/11.85 Or % 11.55/11.85 (Eq (part_of (skS.0 2 e1 p1 a read museum_api museen a_1 a_2 a_3) (skS.0 0 e1 p1 a read museum_api museen a_1)) % 11.55/11.85 True) % 11.55/11.85 (Eq (aee p1 a) False) % 11.55/11.85 Clause #70 (by superposition #[69, 9]): ∀ (a a_1 a_2 : Iota), % 11.55/11.85 Or % 11.55/11.85 (Eq % 11.55/11.85 (part_of (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) % 11.55/11.85 (skS.0 0 e1 p1 bibliothek read museum_api museen a)) % 11.55/11.85 True) % 11.55/11.85 (Eq False True) % 11.55/11.85 Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 : Iota), % 11.55/11.85 Eq % 11.55/11.85 (part_of (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) % 11.55/11.85 (skS.0 0 e1 p1 bibliothek read museum_api museen a)) % 11.55/11.85 True % 11.55/11.85 Clause #72 (by superposition #[71, 40]): ∀ (a a_1 a_2 : Iota), % 11.55/11.85 Or (Eq True False) % 11.55/11.85 (Or (Eq (cnt (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) read museum_api) False) % 11.55/11.85 (Or (Eq (bearer (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) museen) False) % 11.55/11.85 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) False) % 11.55/11.85 (Eq (disability (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2)) False)))) % 11.65/11.90 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 11.65/11.90 Or (Eq (cnt (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) read museum_api) False) % 11.65/11.90 (Or (Eq (bearer (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) museen) False) % 11.65/11.90 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) False) % 11.65/11.90 (Eq (disability (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2)) False))) % 11.65/11.90 Clause #74 (by superposition #[73, 66]): ∀ (a a_1 a_2 : Iota), % 11.65/11.90 Or (Eq (bearer (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) museen) False) % 11.65/11.90 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) False) % 11.65/11.90 (Or (Eq (disability (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2)) False) (Eq False True))) % 11.65/11.90 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 : Iota), % 11.65/11.90 Or (Eq (bearer (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) museen) False) % 11.65/11.90 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) False) % 11.65/11.90 (Eq (disability (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2)) False)) % 11.65/11.90 Clause #76 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.65/11.90 Or (Eq (activates a a_1) False) % 11.65/11.90 (Or (Eq (tgt a_1 a_2) False) % 11.65/11.90 (Or (Eq (act a_1 a_3) False) % 11.65/11.90 (Or (Eq (aer a_1 a_4) False) % 11.65/11.90 (Or (Eq (aee a_1 a_5) False) % 11.65/11.90 (Or % 11.65/11.90 (Eq % 11.65/11.90 (And % 11.65/11.90 (And % 11.65/11.90 (And % 11.65/11.90 (And % 11.65/11.90 (And % 11.65/11.90 (And (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 11.65/11.90 (immunity (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 11.65/11.90 (bearer (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_5)) % 11.65/11.90 (cnt (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_3 a_2)) % 11.65/11.90 (part_of (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6))) % 11.65/11.90 (disability (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8))) % 11.65/11.90 (bearer (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) a_4)) % 11.65/11.90 True) % 11.65/11.90 (Or (Eq (perm a_1) False) (Eq (strong a_1) False))))))) % 11.65/11.90 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.65/11.90 Or (Eq (activates a a_1) False) % 11.65/11.90 (Or (Eq (tgt a_1 a_2) False) % 11.65/11.90 (Or (Eq (act a_1 a_3) False) % 11.65/11.90 (Or (Eq (aer a_1 a_4) False) % 11.65/11.90 (Or (Eq (aee a_1 a_5) False) % 11.65/11.90 (Or (Eq (perm a_1) False) % 11.65/11.90 (Or (Eq (strong a_1) False) (Eq (bearer (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) a_4) True))))))) % 11.65/11.90 Clause #78 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.65/11.90 Or (Eq (activates a a_1) False) % 11.65/11.90 (Or (Eq (tgt a_1 a_2) False) % 11.65/11.90 (Or (Eq (act a_1 a_3) False) % 11.65/11.90 (Or (Eq (aer a_1 a_4) False) % 11.65/11.90 (Or (Eq (aee a_1 a_5) False) % 11.65/11.90 (Or (Eq (perm a_1) False) % 11.65/11.90 (Or (Eq (strong a_1) False) % 11.65/11.90 (Eq % 11.65/11.90 (And % 11.65/11.90 (And % 11.65/11.90 (And % 11.65/11.90 (And % 11.65/11.90 (And (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 11.65/11.90 (immunity (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 11.65/11.90 (bearer (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_5)) % 11.65/11.90 (cnt (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_3 a_2)) % 11.65/11.90 (part_of (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6))) % 11.65/11.90 (disability (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8))) % 11.65/11.90 True))))))) % 11.65/11.90 Clause #79 (by superposition #[77, 13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/11.90 Or (Eq (tgt p1 a) False) % 11.65/11.90 (Or (Eq (act p1 a_1) False) % 11.65/11.90 (Or (Eq (aer p1 a_2) False) % 11.65/11.90 (Or (Eq (aee p1 a_3) False) % 11.65/11.90 (Or (Eq (perm p1) False) % 11.65/11.90 (Or (Eq (strong p1) False) % 11.65/11.90 (Or (Eq (bearer (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_2) True) (Eq False True))))))) % 11.65/11.96 Clause #80 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.65/11.96 Or (Eq (activates a a_1) False) % 11.65/11.96 (Or (Eq (tgt a_1 a_2) False) % 11.65/11.96 (Or (Eq (act a_1 a_3) False) % 11.65/11.96 (Or (Eq (aer a_1 a_4) False) % 11.65/11.96 (Or (Eq (aee a_1 a_5) False) % 11.65/11.96 (Or (Eq (perm a_1) False) % 11.65/11.96 (Or (Eq (strong a_1) False) (Eq (disability (skS.0 2 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8)) True))))))) % 11.65/11.96 Clause #81 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.65/11.96 Or (Eq (activates a a_1) False) % 11.65/11.96 (Or (Eq (tgt a_1 a_2) False) % 11.65/11.96 (Or (Eq (act a_1 a_3) False) % 11.65/11.96 (Or (Eq (aer a_1 a_4) False) % 11.65/11.96 (Or (Eq (aee a_1 a_5) False) % 11.65/11.96 (Or (Eq (perm a_1) False) % 11.65/11.96 (Or (Eq (strong a_1) False) % 11.65/11.96 (Eq % 11.65/11.96 (And % 11.65/11.96 (And % 11.65/11.96 (And % 11.65/11.96 (And (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 11.65/11.96 (immunity (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 11.65/11.96 (bearer (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_5)) % 11.65/11.96 (cnt (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_3 a_2)) % 11.65/11.96 (part_of (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6))) % 11.65/11.96 True))))))) % 11.65/11.96 Clause #82 (by superposition #[80, 13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/11.96 Or (Eq (tgt p1 a) False) % 11.65/11.96 (Or (Eq (act p1 a_1) False) % 11.65/11.96 (Or (Eq (aer p1 a_2) False) % 11.65/11.96 (Or (Eq (aee p1 a_3) False) % 11.65/11.96 (Or (Eq (perm p1) False) % 11.65/11.96 (Or (Eq (strong p1) False) % 11.65/11.96 (Or (Eq (disability (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6)) True) (Eq False True))))))) % 11.65/11.96 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/11.96 Or (Eq (tgt p1 a) False) % 11.65/11.96 (Or (Eq (act p1 a_1) False) % 11.65/11.96 (Or (Eq (aer p1 a_2) False) % 11.65/11.96 (Or (Eq (aee p1 a_3) False) % 11.65/11.96 (Or (Eq (perm p1) False) % 11.65/11.96 (Or (Eq (strong p1) False) (Eq (disability (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6)) True)))))) % 11.65/11.96 Clause #84 (by forward demodulation #[83, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/11.96 Or (Eq (tgt p1 a) False) % 11.65/11.96 (Or (Eq (act p1 a_1) False) % 11.65/11.96 (Or (Eq (aer p1 a_2) False) % 11.65/11.96 (Or (Eq (aee p1 a_3) False) % 11.65/11.96 (Or (Eq True False) % 11.65/11.96 (Or (Eq (strong p1) False) (Eq (disability (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6)) True)))))) % 11.65/11.96 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/11.96 Or (Eq (tgt p1 a) False) % 11.65/11.96 (Or (Eq (act p1 a_1) False) % 11.65/11.96 (Or (Eq (aer p1 a_2) False) % 11.65/11.96 (Or (Eq (aee p1 a_3) False) % 11.65/11.96 (Or (Eq (strong p1) False) (Eq (disability (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6)) True))))) % 11.65/11.96 Clause #86 (by forward demodulation #[85, 8]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/11.96 Or (Eq (tgt p1 a) False) % 11.65/11.96 (Or (Eq (act p1 a_1) False) % 11.65/11.96 (Or (Eq (aer p1 a_2) False) % 11.65/11.96 (Or (Eq (aee p1 a_3) False) % 11.65/11.96 (Or (Eq True False) (Eq (disability (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6)) True))))) % 11.65/11.96 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/11.96 Or (Eq (tgt p1 a) False) % 11.65/11.96 (Or (Eq (act p1 a_1) False) % 11.65/11.96 (Or (Eq (aer p1 a_2) False) % 11.65/11.96 (Or (Eq (aee p1 a_3) False) (Eq (disability (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6)) True)))) % 11.65/11.96 Clause #88 (by superposition #[87, 12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.65/11.96 Or (Eq (act p1 a) False) % 11.65/11.96 (Or (Eq (aer p1 a_1) False) % 11.65/11.96 (Or (Eq (aee p1 a_2) False) % 11.65/11.96 (Or (Eq (disability (skS.0 2 e1 p1 a_2 a museum_api a_1 a_3 a_4 a_5)) True) (Eq False True)))) % 11.65/11.96 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.65/11.96 Or (Eq (act p1 a) False) % 11.65/11.96 (Or (Eq (aer p1 a_1) False) % 11.65/11.96 (Or (Eq (aee p1 a_2) False) (Eq (disability (skS.0 2 e1 p1 a_2 a museum_api a_1 a_3 a_4 a_5)) True))) % 11.65/11.96 Clause #90 (by superposition #[89, 11]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.65/11.96 Or (Eq (aer p1 a) False) % 11.65/11.96 (Or (Eq (aee p1 a_1) False) % 11.65/11.96 (Or (Eq (disability (skS.0 2 e1 p1 a_1 read museum_api a a_2 a_3 a_4)) True) (Eq False True))) % 11.65/11.96 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.65/12.02 Or (Eq (aer p1 a) False) % 11.65/12.02 (Or (Eq (aee p1 a_1) False) (Eq (disability (skS.0 2 e1 p1 a_1 read museum_api a a_2 a_3 a_4)) True)) % 11.65/12.02 Clause #92 (by superposition #[91, 10]): ∀ (a a_1 a_2 a_3 : Iota), % 11.65/12.02 Or (Eq (aee p1 a) False) % 11.65/12.02 (Or (Eq (disability (skS.0 2 e1 p1 a read museum_api museen a_1 a_2 a_3)) True) (Eq False True)) % 11.65/12.02 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 a_3 : Iota), % 11.65/12.02 Or (Eq (aee p1 a) False) (Eq (disability (skS.0 2 e1 p1 a read museum_api museen a_1 a_2 a_3)) True) % 11.65/12.02 Clause #94 (by superposition #[93, 9]): ∀ (a a_1 a_2 : Iota), % 11.65/12.02 Or (Eq (disability (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2)) True) (Eq False True) % 11.65/12.02 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 : Iota), Eq (disability (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2)) True % 11.65/12.02 Clause #96 (by backward demodulation #[95, 75]): ∀ (a a_1 a_2 : Iota), % 11.65/12.02 Or (Eq (bearer (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) museen) False) % 11.65/12.02 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) False) (Eq True False)) % 11.65/12.02 Clause #97 (by clausification #[79]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/12.02 Or (Eq (tgt p1 a) False) % 11.65/12.02 (Or (Eq (act p1 a_1) False) % 11.65/12.02 (Or (Eq (aer p1 a_2) False) % 11.65/12.02 (Or (Eq (aee p1 a_3) False) % 11.65/12.02 (Or (Eq (perm p1) False) % 11.65/12.02 (Or (Eq (strong p1) False) (Eq (bearer (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_2) True)))))) % 11.65/12.02 Clause #98 (by forward demodulation #[97, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/12.02 Or (Eq (tgt p1 a) False) % 11.65/12.02 (Or (Eq (act p1 a_1) False) % 11.65/12.02 (Or (Eq (aer p1 a_2) False) % 11.65/12.02 (Or (Eq (aee p1 a_3) False) % 11.65/12.02 (Or (Eq True False) % 11.65/12.02 (Or (Eq (strong p1) False) (Eq (bearer (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_2) True)))))) % 11.65/12.02 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/12.02 Or (Eq (tgt p1 a) False) % 11.65/12.02 (Or (Eq (act p1 a_1) False) % 11.65/12.02 (Or (Eq (aer p1 a_2) False) % 11.65/12.02 (Or (Eq (aee p1 a_3) False) % 11.65/12.02 (Or (Eq (strong p1) False) (Eq (bearer (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_2) True))))) % 11.65/12.02 Clause #100 (by forward demodulation #[99, 8]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/12.02 Or (Eq (tgt p1 a) False) % 11.65/12.02 (Or (Eq (act p1 a_1) False) % 11.65/12.02 (Or (Eq (aer p1 a_2) False) % 11.65/12.02 (Or (Eq (aee p1 a_3) False) % 11.65/12.02 (Or (Eq True False) (Eq (bearer (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_2) True))))) % 11.65/12.02 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.65/12.02 Or (Eq (tgt p1 a) False) % 11.65/12.02 (Or (Eq (act p1 a_1) False) % 11.65/12.02 (Or (Eq (aer p1 a_2) False) % 11.65/12.02 (Or (Eq (aee p1 a_3) False) (Eq (bearer (skS.0 2 e1 p1 a_3 a_1 a a_2 a_4 a_5 a_6) a_2) True)))) % 11.65/12.02 Clause #102 (by superposition #[101, 12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.65/12.02 Or (Eq (act p1 a) False) % 11.65/12.02 (Or (Eq (aer p1 a_1) False) % 11.65/12.02 (Or (Eq (aee p1 a_2) False) % 11.65/12.02 (Or (Eq (bearer (skS.0 2 e1 p1 a_2 a museum_api a_1 a_3 a_4 a_5) a_1) True) (Eq False True)))) % 11.65/12.02 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.65/12.02 Or (Eq (act p1 a) False) % 11.65/12.02 (Or (Eq (aer p1 a_1) False) % 11.65/12.02 (Or (Eq (aee p1 a_2) False) (Eq (bearer (skS.0 2 e1 p1 a_2 a museum_api a_1 a_3 a_4 a_5) a_1) True))) % 11.65/12.02 Clause #104 (by superposition #[103, 11]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.65/12.02 Or (Eq (aer p1 a) False) % 11.65/12.02 (Or (Eq (aee p1 a_1) False) % 11.65/12.02 (Or (Eq (bearer (skS.0 2 e1 p1 a_1 read museum_api a a_2 a_3 a_4) a) True) (Eq False True))) % 11.65/12.02 Clause #105 (by clausification #[104]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.65/12.02 Or (Eq (aer p1 a) False) % 11.65/12.02 (Or (Eq (aee p1 a_1) False) (Eq (bearer (skS.0 2 e1 p1 a_1 read museum_api a a_2 a_3 a_4) a) True)) % 11.65/12.02 Clause #106 (by superposition #[105, 10]): ∀ (a a_1 a_2 a_3 : Iota), % 11.65/12.02 Or (Eq (aee p1 a) False) % 11.65/12.02 (Or (Eq (bearer (skS.0 2 e1 p1 a read museum_api museen a_1 a_2 a_3) museen) True) (Eq False True)) % 11.65/12.02 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 a_3 : Iota), % 11.65/12.02 Or (Eq (aee p1 a) False) (Eq (bearer (skS.0 2 e1 p1 a read museum_api museen a_1 a_2 a_3) museen) True) % 11.65/12.02 Clause #108 (by superposition #[107, 9]): ∀ (a a_1 a_2 : Iota), % 11.78/12.08 Or (Eq (bearer (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) museen) True) (Eq False True) % 11.78/12.08 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 : Iota), Eq (bearer (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) museen) True % 11.78/12.08 Clause #110 (by clausification #[96]): ∀ (a a_1 a_2 : Iota), % 11.78/12.08 Or (Eq (bearer (skS.0 2 e1 p1 bibliothek read museum_api museen a a_1 a_2) museen) False) % 11.78/12.08 (Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) False) % 11.78/12.08 Clause #111 (by superposition #[110, 109]): ∀ (a : Iota), Or (Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) False) (Eq False True) % 11.78/12.08 Clause #113 (by clausification #[81]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.78/12.08 Or (Eq (activates a a_1) False) % 11.78/12.08 (Or (Eq (tgt a_1 a_2) False) % 11.78/12.08 (Or (Eq (act a_1 a_3) False) % 11.78/12.08 (Or (Eq (aer a_1 a_4) False) % 11.78/12.08 (Or (Eq (aee a_1 a_5) False) % 11.78/12.08 (Or (Eq (perm a_1) False) % 11.78/12.08 (Or (Eq (strong a_1) False) % 11.78/12.08 (Eq % 11.78/12.08 (And % 11.78/12.08 (And % 11.78/12.08 (And (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 11.78/12.08 (immunity (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 11.78/12.08 (bearer (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_5)) % 11.78/12.08 (cnt (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_3 a_2)) % 11.78/12.08 True))))))) % 11.78/12.08 Clause #115 (by clausification #[111]): ∀ (a : Iota), Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) False % 11.78/12.08 Clause #128 (by clausification #[113]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.78/12.08 Or (Eq (activates a a_1) False) % 11.78/12.08 (Or (Eq (tgt a_1 a_2) False) % 11.78/12.08 (Or (Eq (act a_1 a_3) False) % 11.78/12.08 (Or (Eq (aer a_1 a_4) False) % 11.78/12.08 (Or (Eq (aee a_1 a_5) False) % 11.78/12.08 (Or (Eq (perm a_1) False) % 11.78/12.08 (Or (Eq (strong a_1) False) % 11.78/12.08 (Eq % 11.78/12.08 (And % 11.78/12.08 (And (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 11.78/12.08 (immunity (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 11.78/12.08 (bearer (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_5)) % 11.78/12.08 True))))))) % 11.78/12.08 Clause #145 (by clausification #[128]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.78/12.08 Or (Eq (activates a a_1) False) % 11.78/12.08 (Or (Eq (tgt a_1 a_2) False) % 11.78/12.08 (Or (Eq (act a_1 a_3) False) % 11.78/12.08 (Or (Eq (aer a_1 a_4) False) % 11.78/12.08 (Or (Eq (aee a_1 a_5) False) % 11.78/12.08 (Or (Eq (perm a_1) False) % 11.78/12.08 (Or (Eq (strong a_1) False) % 11.78/12.08 (Eq % 11.78/12.08 (And (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 11.78/12.08 (immunity (skS.0 1 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 11.78/12.08 True))))))) % 11.78/12.08 Clause #166 (by clausification #[145]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.78/12.08 Or (Eq (activates a a_1) False) % 11.78/12.08 (Or (Eq (tgt a_1 a_2) False) % 11.78/12.08 (Or (Eq (act a_1 a_3) False) % 11.78/12.08 (Or (Eq (aer a_1 a_4) False) % 11.78/12.08 (Or (Eq (aee a_1 a_5) False) % 11.78/12.08 (Or (Eq (perm a_1) False) % 11.78/12.08 (Or (Eq (strong a_1) False) (Eq (founds_imm a (skS.0 0 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) True))))))) % 11.78/12.08 Clause #176 (by superposition #[166, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.78/12.08 Or (Eq (tgt p1 a) False) % 11.78/12.08 (Or (Eq (act p1 a_1) False) % 11.78/12.08 (Or (Eq (aer p1 a_2) False) % 11.78/12.08 (Or (Eq (aee p1 a_3) False) % 11.78/12.08 (Or (Eq (perm p1) False) % 11.78/12.08 (Or (Eq (strong p1) False) % 11.78/12.08 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4) p1) True) (Eq False True))))))) % 11.78/12.08 Clause #182 (by clausification #[176]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.78/12.08 Or (Eq (tgt p1 a) False) % 11.78/12.08 (Or (Eq (act p1 a_1) False) % 11.78/12.08 (Or (Eq (aer p1 a_2) False) % 11.78/12.08 (Or (Eq (aee p1 a_3) False) % 11.78/12.08 (Or (Eq (perm p1) False) % 11.78/12.08 (Or (Eq (strong p1) False) (Eq (founds_imm e1 (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4) p1) True)))))) % 11.78/12.08 Clause #183 (by forward demodulation #[182, 7]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.78/12.08 Or (Eq (tgt p1 a) False) % 11.78/12.08 (Or (Eq (act p1 a_1) False) % 11.78/12.08 (Or (Eq (aer p1 a_2) False) % 11.78/12.08 (Or (Eq (aee p1 a_3) False) % 11.78/12.11 (Or (Eq True False) % 11.78/12.11 (Or (Eq (strong p1) False) (Eq (founds_imm e1 (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4) p1) True)))))) % 11.78/12.11 Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.78/12.11 Or (Eq (tgt p1 a) False) % 11.78/12.11 (Or (Eq (act p1 a_1) False) % 11.78/12.11 (Or (Eq (aer p1 a_2) False) % 11.78/12.11 (Or (Eq (aee p1 a_3) False) % 11.78/12.11 (Or (Eq (strong p1) False) (Eq (founds_imm e1 (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4) p1) True))))) % 11.78/12.11 Clause #185 (by forward demodulation #[184, 8]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.78/12.11 Or (Eq (tgt p1 a) False) % 11.78/12.11 (Or (Eq (act p1 a_1) False) % 11.78/12.11 (Or (Eq (aer p1 a_2) False) % 11.78/12.11 (Or (Eq (aee p1 a_3) False) % 11.78/12.11 (Or (Eq True False) (Eq (founds_imm e1 (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4) p1) True))))) % 11.78/12.11 Clause #186 (by clausification #[185]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.78/12.11 Or (Eq (tgt p1 a) False) % 11.78/12.11 (Or (Eq (act p1 a_1) False) % 11.78/12.11 (Or (Eq (aer p1 a_2) False) % 11.78/12.11 (Or (Eq (aee p1 a_3) False) (Eq (founds_imm e1 (skS.0 0 e1 p1 a_3 a_1 a a_2 a_4) p1) True)))) % 11.78/12.11 Clause #187 (by superposition #[186, 12]): ∀ (a a_1 a_2 a_3 : Iota), % 11.78/12.11 Or (Eq (act p1 a) False) % 11.78/12.11 (Or (Eq (aer p1 a_1) False) % 11.78/12.11 (Or (Eq (aee p1 a_2) False) % 11.78/12.11 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 a_2 a museum_api a_1 a_3) p1) True) (Eq False True)))) % 11.78/12.11 Clause #188 (by clausification #[187]): ∀ (a a_1 a_2 a_3 : Iota), % 11.78/12.11 Or (Eq (act p1 a) False) % 11.78/12.11 (Or (Eq (aer p1 a_1) False) % 11.78/12.11 (Or (Eq (aee p1 a_2) False) (Eq (founds_imm e1 (skS.0 0 e1 p1 a_2 a museum_api a_1 a_3) p1) True))) % 11.78/12.11 Clause #189 (by superposition #[188, 11]): ∀ (a a_1 a_2 : Iota), % 11.78/12.11 Or (Eq (aer p1 a) False) % 11.78/12.11 (Or (Eq (aee p1 a_1) False) % 11.78/12.11 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 a_1 read museum_api a a_2) p1) True) (Eq False True))) % 11.78/12.11 Clause #190 (by clausification #[189]): ∀ (a a_1 a_2 : Iota), % 11.78/12.11 Or (Eq (aer p1 a) False) % 11.78/12.11 (Or (Eq (aee p1 a_1) False) (Eq (founds_imm e1 (skS.0 0 e1 p1 a_1 read museum_api a a_2) p1) True)) % 11.78/12.11 Clause #191 (by superposition #[190, 10]): ∀ (a a_1 : Iota), % 11.78/12.11 Or (Eq (aee p1 a) False) % 11.78/12.11 (Or (Eq (founds_imm e1 (skS.0 0 e1 p1 a read museum_api museen a_1) p1) True) (Eq False True)) % 11.78/12.11 Clause #192 (by clausification #[191]): ∀ (a a_1 : Iota), Or (Eq (aee p1 a) False) (Eq (founds_imm e1 (skS.0 0 e1 p1 a read museum_api museen a_1) p1) True) % 11.78/12.11 Clause #193 (by superposition #[192, 9]): ∀ (a : Iota), Or (Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) True) (Eq False True) % 11.78/12.11 Clause #194 (by clausification #[193]): ∀ (a : Iota), Eq (founds_imm e1 (skS.0 0 e1 p1 bibliothek read museum_api museen a) p1) True % 11.78/12.11 Clause #195 (by superposition #[194, 115]): Eq True False % 11.78/12.11 Clause #196 (by clausification #[195]): False % 11.78/12.11 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------