%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:25 AM UTC 2026 % Result : Theorem 20.36s 20.68s % Output : Proof 21.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.05 % Command : duper %s % 0.09/0.36 % Computer : n027.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 14:10:15 UTC 2026 % 0.09/0.36 % CPUTime : % 20.36/20.68 SZS status Theorem for theBenchmark.p % 20.36/20.68 SZS output start Proof for theBenchmark.p % 20.36/20.68 Clause #1 (by assumption #[]): Eq % 20.36/20.68 (∀ (F X Y A T E : Iota), % 20.36/20.68 And (And (And (And (And (And (proh F) (has_rem F)) (aee F X)) (aer F Y)) (act F A)) (tgt F T)) (activates E F) → % 20.36/20.68 Exists fun RhoR => % 20.36/20.68 Exists fun Pw => % 20.36/20.68 Exists fun S => % 20.36/20.68 And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And (And (And (And (founds_rem E RhoR F) (power Pw)) (bearer Pw Y)) (cnt Pw (decl A) T)) % 20.36/20.68 (part_of Pw RhoR)) % 20.36/20.68 (subjection S)) % 20.36/20.68 (bearer S X)) % 20.36/20.68 (cnt S (decl A) T)) % 20.36/20.68 (part_of S RhoR)) % 20.36/20.68 True % 20.36/20.68 Clause #6 (by assumption #[]): Eq % 20.36/20.68 (∀ (Pw A T Rho E R : Iota), % 20.36/20.68 And (And (And (power Pw) (cnt Pw (decl A) T)) (part_of Pw Rho)) (founds_rem E Rho R) → about_event Pw E) % 20.36/20.68 True % 20.36/20.68 Clause #7 (by assumption #[]): Eq % 20.36/20.68 (∀ (S A T Rho E R : Iota), % 20.36/20.68 And (And (And (subjection S) (cnt S (decl A) T)) (part_of S Rho)) (founds_rem E Rho R) → about_event S E) % 20.36/20.68 True % 20.36/20.68 Clause #14 (by assumption #[]): Eq (proh f1) True % 20.36/20.68 Clause #15 (by assumption #[]): Eq (has_rem f1) True % 20.36/20.68 Clause #16 (by assumption #[]): Eq (aee f1 marketplace) True % 20.36/20.68 Clause #17 (by assumption #[]): Eq (aer f1 philharmonie) True % 20.36/20.68 Clause #18 (by assumption #[]): Eq (act f1 distrib) True % 20.36/20.68 Clause #19 (by assumption #[]): Eq (tgt f1 concert_ds) True % 20.36/20.68 Clause #20 (by assumption #[]): Eq (activates e1 f1) True % 20.36/20.68 Clause #22 (by assumption #[]): Eq % 20.36/20.68 (Not % 20.36/20.68 (Exists fun RhoR => % 20.36/20.68 Exists fun Pw => % 20.36/20.68 Exists fun S => % 20.36/20.68 And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And (And (And (founds_rem e1 RhoR f1) (power Pw)) (bearer Pw philharmonie)) % 20.36/20.68 (cnt Pw (decl distrib) concert_ds)) % 20.36/20.68 (part_of Pw RhoR)) % 20.36/20.68 (about_event Pw e1)) % 20.36/20.68 (subjection S)) % 20.36/20.68 (bearer S marketplace)) % 20.36/20.68 (cnt S (decl distrib) concert_ds)) % 20.36/20.68 (part_of S RhoR)) % 20.36/20.68 (about_event S e1))) % 20.36/20.68 True % 20.36/20.68 Clause #40 (by clausification #[1]): ∀ (a : Iota), % 20.36/20.68 Eq % 20.36/20.68 (∀ (X Y A T E : Iota), % 20.36/20.68 And (And (And (And (And (And (proh a) (has_rem a)) (aee a X)) (aer a Y)) (act a A)) (tgt a T)) (activates E a) → % 20.36/20.68 Exists fun RhoR => % 20.36/20.68 Exists fun Pw => % 20.36/20.68 Exists fun S => % 20.36/20.68 And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And (And (And (And (founds_rem E RhoR a) (power Pw)) (bearer Pw Y)) (cnt Pw (decl A) T)) % 20.36/20.68 (part_of Pw RhoR)) % 20.36/20.68 (subjection S)) % 20.36/20.68 (bearer S X)) % 20.36/20.68 (cnt S (decl A) T)) % 20.36/20.68 (part_of S RhoR)) % 20.36/20.68 True % 20.36/20.68 Clause #41 (by clausification #[40]): ∀ (a a_1 : Iota), % 20.36/20.68 Eq % 20.36/20.68 (∀ (Y A T E : Iota), % 20.36/20.68 And (And (And (And (And (And (proh a) (has_rem a)) (aee a a_1)) (aer a Y)) (act a A)) (tgt a T)) (activates E a) → % 20.36/20.68 Exists fun RhoR => % 20.36/20.68 Exists fun Pw => % 20.36/20.68 Exists fun S => % 20.36/20.68 And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And (And (And (And (founds_rem E RhoR a) (power Pw)) (bearer Pw Y)) (cnt Pw (decl A) T)) % 20.36/20.68 (part_of Pw RhoR)) % 20.36/20.68 (subjection S)) % 20.36/20.68 (bearer S a_1)) % 20.36/20.68 (cnt S (decl A) T)) % 20.36/20.68 (part_of S RhoR)) % 20.36/20.68 True % 20.36/20.68 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), % 20.36/20.68 Eq % 20.36/20.68 (∀ (A T E : Iota), % 20.36/20.68 And (And (And (And (And (And (proh a) (has_rem a)) (aee a a_1)) (aer a a_2)) (act a A)) (tgt a T)) % 20.36/20.68 (activates E a) → % 20.36/20.68 Exists fun RhoR => % 20.36/20.68 Exists fun Pw => % 20.36/20.68 Exists fun S => % 20.36/20.68 And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And % 20.36/20.68 (And (And (And (And (founds_rem E RhoR a) (power Pw)) (bearer Pw a_2)) (cnt Pw (decl A) T)) % 20.36/20.68 (part_of Pw RhoR)) % 20.46/20.73 (subjection S)) % 20.46/20.73 (bearer S a_1)) % 20.46/20.73 (cnt S (decl A) T)) % 20.46/20.73 (part_of S RhoR)) % 20.46/20.73 True % 20.46/20.73 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 : Iota), % 20.46/20.73 Eq % 20.46/20.73 (∀ (T E : Iota), % 20.46/20.73 And (And (And (And (And (And (proh a) (has_rem a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a T)) % 20.46/20.73 (activates E a) → % 20.46/20.73 Exists fun RhoR => % 20.46/20.73 Exists fun Pw => % 20.46/20.73 Exists fun S => % 20.46/20.73 And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And (And (And (And (founds_rem E RhoR a) (power Pw)) (bearer Pw a_2)) (cnt Pw (decl a_3) T)) % 20.46/20.73 (part_of Pw RhoR)) % 20.46/20.73 (subjection S)) % 20.46/20.73 (bearer S a_1)) % 20.46/20.73 (cnt S (decl a_3) T)) % 20.46/20.73 (part_of S RhoR)) % 20.46/20.73 True % 20.46/20.73 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.46/20.73 Eq % 20.46/20.73 (∀ (E : Iota), % 20.46/20.73 And (And (And (And (And (And (proh a) (has_rem a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a a_4)) % 20.46/20.73 (activates E a) → % 20.46/20.73 Exists fun RhoR => % 20.46/20.73 Exists fun Pw => % 20.46/20.73 Exists fun S => % 20.46/20.73 And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And (And (And (And (founds_rem E RhoR a) (power Pw)) (bearer Pw a_2)) (cnt Pw (decl a_3) a_4)) % 20.46/20.73 (part_of Pw RhoR)) % 20.46/20.73 (subjection S)) % 20.46/20.73 (bearer S a_1)) % 20.46/20.73 (cnt S (decl a_3) a_4)) % 20.46/20.73 (part_of S RhoR)) % 20.46/20.73 True % 20.46/20.73 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.46/20.73 Eq % 20.46/20.73 (And (And (And (And (And (And (proh a) (has_rem a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a a_4)) % 20.46/20.73 (activates a_5 a) → % 20.46/20.73 Exists fun RhoR => % 20.46/20.73 Exists fun Pw => % 20.46/20.73 Exists fun S => % 20.46/20.73 And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And (And (And (And (founds_rem a_5 RhoR a) (power Pw)) (bearer Pw a_2)) (cnt Pw (decl a_3) a_4)) % 20.46/20.73 (part_of Pw RhoR)) % 20.46/20.73 (subjection S)) % 20.46/20.73 (bearer S a_1)) % 20.46/20.73 (cnt S (decl a_3) a_4)) % 20.46/20.73 (part_of S RhoR)) % 20.46/20.73 True % 20.46/20.73 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.46/20.73 Or % 20.46/20.73 (Eq % 20.46/20.73 (And (And (And (And (And (And (proh a) (has_rem a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a a_4)) % 20.46/20.73 (activates a_5 a)) % 20.46/20.73 False) % 20.46/20.73 (Eq % 20.46/20.73 (Exists fun RhoR => % 20.46/20.73 Exists fun Pw => % 20.46/20.73 Exists fun S => % 20.46/20.73 And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And (And (And (And (founds_rem a_5 RhoR a) (power Pw)) (bearer Pw a_2)) (cnt Pw (decl a_3) a_4)) % 20.46/20.73 (part_of Pw RhoR)) % 20.46/20.73 (subjection S)) % 20.46/20.73 (bearer S a_1)) % 20.46/20.73 (cnt S (decl a_3) a_4)) % 20.46/20.73 (part_of S RhoR)) % 20.46/20.73 True) % 20.46/20.73 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.46/20.73 Or % 20.46/20.73 (Eq % 20.46/20.73 (Exists fun RhoR => % 20.46/20.73 Exists fun Pw => % 20.46/20.73 Exists fun S => % 20.46/20.73 And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.73 (And (And (And (And (founds_rem a RhoR a_1) (power Pw)) (bearer Pw a_2)) (cnt Pw (decl a_3) a_4)) % 20.46/20.73 (part_of Pw RhoR)) % 20.46/20.73 (subjection S)) % 20.46/20.73 (bearer S a_5)) % 20.46/20.73 (cnt S (decl a_3) a_4)) % 20.46/20.73 (part_of S RhoR)) % 20.46/20.73 True) % 20.46/20.73 (Or % 20.46/20.73 (Eq (And (And (And (And (And (proh a_1) (has_rem a_1)) (aee a_1 a_5)) (aer a_1 a_2)) (act a_1 a_3)) (tgt a_1 a_4)) % 20.46/20.73 False) % 20.46/20.73 (Eq (activates a a_1) False)) % 20.46/20.73 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.46/20.73 Or (Eq (And (And (And (And (And (proh a) (has_rem a)) (aee a a_1)) (aer a a_2)) (act a a_3)) (tgt a a_4)) False) % 20.46/20.73 (Or (Eq (activates a_5 a) False) % 20.46/20.73 (Eq % 20.46/20.73 (Exists fun Pw => % 20.46/20.73 Exists fun S => % 20.46/20.73 And % 20.46/20.73 (And % 20.46/20.73 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And (And (And (founds_rem a_5 (skS.0 3 a_5 a a_2 a_3 a_4 a_1 a_6) a) (power Pw)) (bearer Pw a_2)) % 20.46/20.78 (cnt Pw (decl a_3) a_4)) % 20.46/20.78 (part_of Pw (skS.0 3 a_5 a a_2 a_3 a_4 a_1 a_6))) % 20.46/20.78 (subjection S)) % 20.46/20.78 (bearer S a_1)) % 20.46/20.78 (cnt S (decl a_3) a_4)) % 20.46/20.78 (part_of S (skS.0 3 a_5 a a_2 a_3 a_4 a_1 a_6))) % 20.46/20.78 True)) % 20.46/20.78 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.46/20.78 Or (Eq (activates a a_1) False) % 20.46/20.78 (Or % 20.46/20.78 (Eq % 20.46/20.78 (Exists fun Pw => % 20.46/20.78 Exists fun S => % 20.46/20.78 And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And (And (And (founds_rem a (skS.0 3 a a_1 a_2 a_3 a_4 a_5 a_6) a_1) (power Pw)) (bearer Pw a_2)) % 20.46/20.78 (cnt Pw (decl a_3) a_4)) % 20.46/20.78 (part_of Pw (skS.0 3 a a_1 a_2 a_3 a_4 a_5 a_6))) % 20.46/20.78 (subjection S)) % 20.46/20.78 (bearer S a_5)) % 20.46/20.78 (cnt S (decl a_3) a_4)) % 20.46/20.78 (part_of S (skS.0 3 a a_1 a_2 a_3 a_4 a_5 a_6))) % 20.46/20.78 True) % 20.46/20.78 (Or (Eq (And (And (And (And (proh a_1) (has_rem a_1)) (aee a_1 a_5)) (aer a_1 a_2)) (act a_1 a_3)) False) % 20.46/20.78 (Eq (tgt a_1 a_4) False))) % 20.46/20.78 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.46/20.78 Or (Eq (activates a a_1) False) % 20.46/20.78 (Or (Eq (And (And (And (And (proh a_1) (has_rem a_1)) (aee a_1 a_2)) (aer a_1 a_3)) (act a_1 a_4)) False) % 20.46/20.78 (Or (Eq (tgt a_1 a_5) False) % 20.46/20.78 (Eq % 20.46/20.78 (Exists fun S => % 20.46/20.78 And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And (founds_rem a (skS.0 3 a a_1 a_3 a_4 a_5 a_2 a_6) a_1) % 20.46/20.78 (power (skS.0 4 a a_1 a_3 a_4 a_5 a_2 a_6 a_7))) % 20.46/20.78 (bearer (skS.0 4 a a_1 a_3 a_4 a_5 a_2 a_6 a_7) a_3)) % 20.46/20.78 (cnt (skS.0 4 a a_1 a_3 a_4 a_5 a_2 a_6 a_7) (decl a_4) a_5)) % 20.46/20.78 (part_of (skS.0 4 a a_1 a_3 a_4 a_5 a_2 a_6 a_7) (skS.0 3 a a_1 a_3 a_4 a_5 a_2 a_6))) % 20.46/20.78 (subjection S)) % 20.46/20.78 (bearer S a_2)) % 20.46/20.78 (cnt S (decl a_4) a_5)) % 20.46/20.78 (part_of S (skS.0 3 a a_1 a_3 a_4 a_5 a_2 a_6))) % 20.46/20.78 True))) % 20.46/20.78 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.46/20.78 Or (Eq (activates a a_1) False) % 20.46/20.78 (Or (Eq (tgt a_1 a_2) False) % 20.46/20.78 (Or % 20.46/20.78 (Eq % 20.46/20.78 (Exists fun S => % 20.46/20.78 And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And (founds_rem a (skS.0 3 a a_1 a_3 a_4 a_2 a_5 a_6) a_1) % 20.46/20.78 (power (skS.0 4 a a_1 a_3 a_4 a_2 a_5 a_6 a_7))) % 20.46/20.78 (bearer (skS.0 4 a a_1 a_3 a_4 a_2 a_5 a_6 a_7) a_3)) % 20.46/20.78 (cnt (skS.0 4 a a_1 a_3 a_4 a_2 a_5 a_6 a_7) (decl a_4) a_2)) % 20.46/20.78 (part_of (skS.0 4 a a_1 a_3 a_4 a_2 a_5 a_6 a_7) (skS.0 3 a a_1 a_3 a_4 a_2 a_5 a_6))) % 20.46/20.78 (subjection S)) % 20.46/20.78 (bearer S a_5)) % 20.46/20.78 (cnt S (decl a_4) a_2)) % 20.46/20.78 (part_of S (skS.0 3 a a_1 a_3 a_4 a_2 a_5 a_6))) % 20.46/20.78 True) % 20.46/20.78 (Or (Eq (And (And (And (proh a_1) (has_rem a_1)) (aee a_1 a_5)) (aer a_1 a_3)) False) % 20.46/20.78 (Eq (act a_1 a_4) False)))) % 20.46/20.78 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.46/20.78 Or (Eq (activates a a_1) False) % 20.46/20.78 (Or (Eq (tgt a_1 a_2) False) % 20.46/20.78 (Or (Eq (And (And (And (proh a_1) (has_rem a_1)) (aee a_1 a_3)) (aer a_1 a_4)) False) % 20.46/20.78 (Or (Eq (act a_1 a_5) False) % 20.46/20.78 (Eq % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And % 20.46/20.78 (And (founds_rem a (skS.0 3 a a_1 a_4 a_5 a_2 a_3 a_6) a_1) % 20.46/20.78 (power (skS.0 4 a a_1 a_4 a_5 a_2 a_3 a_6 a_7))) % 20.56/20.83 (bearer (skS.0 4 a a_1 a_4 a_5 a_2 a_3 a_6 a_7) a_4)) % 20.56/20.83 (cnt (skS.0 4 a a_1 a_4 a_5 a_2 a_3 a_6 a_7) (decl a_5) a_2)) % 20.56/20.83 (part_of (skS.0 4 a a_1 a_4 a_5 a_2 a_3 a_6 a_7) (skS.0 3 a a_1 a_4 a_5 a_2 a_3 a_6))) % 20.56/20.83 (subjection (skS.0 5 a a_1 a_4 a_5 a_2 a_3 a_6 a_7 a_8))) % 20.56/20.83 (bearer (skS.0 5 a a_1 a_4 a_5 a_2 a_3 a_6 a_7 a_8) a_3)) % 20.56/20.83 (cnt (skS.0 5 a a_1 a_4 a_5 a_2 a_3 a_6 a_7 a_8) (decl a_5) a_2)) % 20.56/20.83 (part_of (skS.0 5 a a_1 a_4 a_5 a_2 a_3 a_6 a_7 a_8) (skS.0 3 a a_1 a_4 a_5 a_2 a_3 a_6))) % 20.56/20.83 True)))) % 20.56/20.83 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.56/20.83 Or (Eq (activates a a_1) False) % 20.56/20.83 (Or (Eq (tgt a_1 a_2) False) % 20.56/20.83 (Or (Eq (act a_1 a_3) False) % 20.56/20.83 (Or % 20.56/20.83 (Eq % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 20.56/20.83 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 20.56/20.83 (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 20.56/20.83 (cnt (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (decl a_3) a_2)) % 20.56/20.83 (part_of (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6))) % 20.56/20.83 (subjection (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8))) % 20.56/20.83 (bearer (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_5)) % 20.56/20.83 (cnt (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (decl a_3) a_2)) % 20.56/20.83 (part_of (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6))) % 20.56/20.83 True) % 20.56/20.83 (Or (Eq (And (And (proh a_1) (has_rem a_1)) (aee a_1 a_5)) False) (Eq (aer a_1 a_4) False))))) % 20.56/20.83 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.56/20.83 Or (Eq (activates a a_1) False) % 20.56/20.83 (Or (Eq (tgt a_1 a_2) False) % 20.56/20.83 (Or (Eq (act a_1 a_3) False) % 20.56/20.83 (Or (Eq (And (And (proh a_1) (has_rem a_1)) (aee a_1 a_4)) False) % 20.56/20.83 (Or (Eq (aer a_1 a_5) False) % 20.56/20.83 (Eq (part_of (skS.0 5 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) (skS.0 3 a a_1 a_5 a_3 a_2 a_4 a_6)) True))))) % 20.56/20.83 Clause #55 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.56/20.83 Or (Eq (activates a a_1) False) % 20.56/20.83 (Or (Eq (tgt a_1 a_2) False) % 20.56/20.83 (Or (Eq (act a_1 a_3) False) % 20.56/20.83 (Or (Eq (And (And (proh a_1) (has_rem a_1)) (aee a_1 a_4)) False) % 20.56/20.83 (Or (Eq (aer a_1 a_5) False) % 20.56/20.83 (Eq % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And % 20.56/20.83 (And (founds_rem a (skS.0 3 a a_1 a_5 a_3 a_2 a_4 a_6) a_1) % 20.56/20.83 (power (skS.0 4 a a_1 a_5 a_3 a_2 a_4 a_6 a_7))) % 20.56/20.83 (bearer (skS.0 4 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) a_5)) % 20.56/20.83 (cnt (skS.0 4 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) (decl a_3) a_2)) % 20.56/20.83 (part_of (skS.0 4 a a_1 a_5 a_3 a_2 a_4 a_6 a_7) (skS.0 3 a a_1 a_5 a_3 a_2 a_4 a_6))) % 20.56/20.83 (subjection (skS.0 5 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8))) % 20.56/20.83 (bearer (skS.0 5 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) a_4)) % 20.56/20.83 (cnt (skS.0 5 a a_1 a_5 a_3 a_2 a_4 a_6 a_7 a_8) (decl a_3) a_2)) % 20.56/20.83 True))))) % 20.56/20.83 Clause #56 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.56/20.83 Or (Eq (activates a a_1) False) % 20.56/20.83 (Or (Eq (tgt a_1 a_2) False) % 20.56/20.83 (Or (Eq (act a_1 a_3) False) % 20.56/20.83 (Or (Eq (aer a_1 a_4) False) % 20.56/20.83 (Or (Eq (part_of (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6)) True) % 20.56/20.83 (Or (Eq (And (proh a_1) (has_rem a_1)) False) (Eq (aee a_1 a_5) False)))))) % 20.56/20.83 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.56/20.83 Or (Eq (activates a a_1) False) % 20.56/20.88 (Or (Eq (tgt a_1 a_2) False) % 20.56/20.88 (Or (Eq (act a_1 a_3) False) % 20.56/20.88 (Or (Eq (aer a_1 a_4) False) % 20.56/20.88 (Or (Eq (part_of (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6)) True) % 20.56/20.88 (Or (Eq (aee a_1 a_5) False) (Or (Eq (proh a_1) False) (Eq (has_rem a_1) False))))))) % 20.56/20.88 Clause #59 (by superposition #[20, 57]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.56/20.88 Or (Eq (tgt f1 a) False) % 20.56/20.88 (Or (Eq (act f1 a_1) False) % 20.56/20.88 (Or (Eq (aer f1 a_2) False) % 20.56/20.88 (Or (Eq (part_of (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True) % 20.56/20.88 (Or (Eq (aee f1 a_3) False) (Or (Eq (proh f1) False) (Or (Eq (has_rem f1) False) (Eq False True))))))) % 20.56/20.88 Clause #71 (by clausification #[7]): ∀ (a : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (A T Rho E R : Iota), % 20.56/20.88 And (And (And (subjection a) (cnt a (decl A) T)) (part_of a Rho)) (founds_rem E Rho R) → about_event a E) % 20.56/20.88 True % 20.56/20.88 Clause #72 (by clausification #[71]): ∀ (a a_1 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (T Rho E R : Iota), % 20.56/20.88 And (And (And (subjection a) (cnt a (decl a_1) T)) (part_of a Rho)) (founds_rem E Rho R) → about_event a E) % 20.56/20.88 True % 20.56/20.88 Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (Rho E R : Iota), % 20.56/20.88 And (And (And (subjection a) (cnt a (decl a_1) a_2)) (part_of a Rho)) (founds_rem E Rho R) → about_event a E) % 20.56/20.88 True % 20.56/20.88 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (E R : Iota), % 20.56/20.88 And (And (And (subjection a) (cnt a (decl a_1) a_2)) (part_of a a_3)) (founds_rem E a_3 R) → about_event a E) % 20.56/20.88 True % 20.56/20.88 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (R : Iota), % 20.56/20.88 And (And (And (subjection a) (cnt a (decl a_1) a_2)) (part_of a a_3)) (founds_rem a_4 a_3 R) → about_event a a_4) % 20.56/20.88 True % 20.56/20.88 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (And (And (And (subjection a) (cnt a (decl a_1) a_2)) (part_of a a_3)) (founds_rem a_4 a_3 a_5) → about_event a a_4) % 20.56/20.88 True % 20.56/20.88 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.56/20.88 Or (Eq (And (And (And (subjection a) (cnt a (decl a_1) a_2)) (part_of a a_3)) (founds_rem a_4 a_3 a_5)) False) % 20.56/20.88 (Eq (about_event a a_4) True) % 20.56/20.88 Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.56/20.88 Or (Eq (about_event a a_1) True) % 20.56/20.88 (Or (Eq (And (And (subjection a) (cnt a (decl a_2) a_3)) (part_of a a_4)) False) % 20.56/20.88 (Eq (founds_rem a_1 a_4 a_5) False)) % 20.56/20.88 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.56/20.88 Or (Eq (about_event a a_1) True) % 20.56/20.88 (Or (Eq (founds_rem a_1 a_2 a_3) False) % 20.56/20.88 (Or (Eq (And (subjection a) (cnt a (decl a_4) a_5)) False) (Eq (part_of a a_2) False))) % 20.56/20.88 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.56/20.88 Or (Eq (about_event a a_1) True) % 20.56/20.88 (Or (Eq (founds_rem a_1 a_2 a_3) False) % 20.56/20.88 (Or (Eq (part_of a a_2) False) (Or (Eq (subjection a) False) (Eq (cnt a (decl a_4) a_5) False)))) % 20.56/20.88 Clause #81 (by clausification #[6]): ∀ (a : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (A T Rho E R : Iota), % 20.56/20.88 And (And (And (power a) (cnt a (decl A) T)) (part_of a Rho)) (founds_rem E Rho R) → about_event a E) % 20.56/20.88 True % 20.56/20.88 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (T Rho E R : Iota), % 20.56/20.88 And (And (And (power a) (cnt a (decl a_1) T)) (part_of a Rho)) (founds_rem E Rho R) → about_event a E) % 20.56/20.88 True % 20.56/20.88 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (Rho E R : Iota), % 20.56/20.88 And (And (And (power a) (cnt a (decl a_1) a_2)) (part_of a Rho)) (founds_rem E Rho R) → about_event a E) % 20.56/20.88 True % 20.56/20.88 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (E R : Iota), % 20.56/20.88 And (And (And (power a) (cnt a (decl a_1) a_2)) (part_of a a_3)) (founds_rem E a_3 R) → about_event a E) % 20.56/20.88 True % 20.56/20.88 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.56/20.88 Eq % 20.56/20.88 (∀ (R : Iota), % 20.56/20.88 And (And (And (power a) (cnt a (decl a_1) a_2)) (part_of a a_3)) (founds_rem a_4 a_3 R) → about_event a a_4) % 20.56/20.88 True % 20.56/20.88 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.66/20.92 Eq (And (And (And (power a) (cnt a (decl a_1) a_2)) (part_of a a_3)) (founds_rem a_4 a_3 a_5) → about_event a a_4) % 20.66/20.92 True % 20.66/20.92 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.66/20.92 Or (Eq (And (And (And (power a) (cnt a (decl a_1) a_2)) (part_of a a_3)) (founds_rem a_4 a_3 a_5)) False) % 20.66/20.92 (Eq (about_event a a_4) True) % 20.66/20.92 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.66/20.92 Or (Eq (about_event a a_1) True) % 20.66/20.92 (Or (Eq (And (And (power a) (cnt a (decl a_2) a_3)) (part_of a a_4)) False) (Eq (founds_rem a_1 a_4 a_5) False)) % 20.66/20.92 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.66/20.92 Or (Eq (about_event a a_1) True) % 20.66/20.92 (Or (Eq (founds_rem a_1 a_2 a_3) False) % 20.66/20.92 (Or (Eq (And (power a) (cnt a (decl a_4) a_5)) False) (Eq (part_of a a_2) False))) % 20.66/20.92 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.66/20.92 Or (Eq (about_event a a_1) True) % 20.66/20.92 (Or (Eq (founds_rem a_1 a_2 a_3) False) % 20.66/20.92 (Or (Eq (part_of a a_2) False) (Or (Eq (power a) False) (Eq (cnt a (decl a_4) a_5) False)))) % 20.66/20.92 Clause #113 (by clausification #[22]): Eq % 20.66/20.92 (Exists fun RhoR => % 20.66/20.92 Exists fun Pw => % 20.66/20.92 Exists fun S => % 20.66/20.92 And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And (And (And (founds_rem e1 RhoR f1) (power Pw)) (bearer Pw philharmonie)) % 20.66/20.92 (cnt Pw (decl distrib) concert_ds)) % 20.66/20.92 (part_of Pw RhoR)) % 20.66/20.92 (about_event Pw e1)) % 20.66/20.92 (subjection S)) % 20.66/20.92 (bearer S marketplace)) % 20.66/20.92 (cnt S (decl distrib) concert_ds)) % 20.66/20.92 (part_of S RhoR)) % 20.66/20.92 (about_event S e1)) % 20.66/20.92 False % 20.66/20.92 Clause #114 (by clausification #[113]): ∀ (a : Iota), % 20.66/20.92 Eq % 20.66/20.92 (Exists fun Pw => % 20.66/20.92 Exists fun S => % 20.66/20.92 And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And (And (And (founds_rem e1 a f1) (power Pw)) (bearer Pw philharmonie)) % 20.66/20.92 (cnt Pw (decl distrib) concert_ds)) % 20.66/20.92 (part_of Pw a)) % 20.66/20.92 (about_event Pw e1)) % 20.66/20.92 (subjection S)) % 20.66/20.92 (bearer S marketplace)) % 20.66/20.92 (cnt S (decl distrib) concert_ds)) % 20.66/20.92 (part_of S a)) % 20.66/20.92 (about_event S e1)) % 20.66/20.92 False % 20.66/20.92 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), % 20.66/20.92 Eq % 20.66/20.92 (Exists fun S => % 20.66/20.92 And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And (And (And (founds_rem e1 a f1) (power a_1)) (bearer a_1 philharmonie)) % 20.66/20.92 (cnt a_1 (decl distrib) concert_ds)) % 20.66/20.92 (part_of a_1 a)) % 20.66/20.92 (about_event a_1 e1)) % 20.66/20.92 (subjection S)) % 20.66/20.92 (bearer S marketplace)) % 20.66/20.92 (cnt S (decl distrib) concert_ds)) % 20.66/20.92 (part_of S a)) % 20.66/20.92 (about_event S e1)) % 20.66/20.92 False % 20.66/20.92 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 : Iota), % 20.66/20.92 Eq % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And (And (And (founds_rem e1 a f1) (power a_1)) (bearer a_1 philharmonie)) % 20.66/20.92 (cnt a_1 (decl distrib) concert_ds)) % 20.66/20.92 (part_of a_1 a)) % 20.66/20.92 (about_event a_1 e1)) % 20.66/20.92 (subjection a_2)) % 20.66/20.92 (bearer a_2 marketplace)) % 20.66/20.92 (cnt a_2 (decl distrib) concert_ds)) % 20.66/20.92 (part_of a_2 a)) % 20.66/20.92 (about_event a_2 e1)) % 20.66/20.92 False % 20.66/20.92 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 : Iota), % 20.66/20.92 Or % 20.66/20.92 (Eq % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And % 20.66/20.92 (And (And (And (founds_rem e1 a f1) (power a_1)) (bearer a_1 philharmonie)) % 20.66/20.92 (cnt a_1 (decl distrib) concert_ds)) % 20.66/20.92 (part_of a_1 a)) % 20.66/20.92 (about_event a_1 e1)) % 20.66/20.92 (subjection a_2)) % 20.66/20.92 (bearer a_2 marketplace)) % 20.66/20.97 (cnt a_2 (decl distrib) concert_ds)) % 20.66/20.97 (part_of a_2 a)) % 20.66/20.97 False) % 20.66/20.97 (Eq (about_event a_2 e1) False) % 20.66/20.97 Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 : Iota), % 20.66/20.97 Or (Eq (about_event a e1) False) % 20.66/20.97 (Or % 20.66/20.97 (Eq % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And (And (And (founds_rem e1 a_1 f1) (power a_2)) (bearer a_2 philharmonie)) % 20.66/20.97 (cnt a_2 (decl distrib) concert_ds)) % 20.66/20.97 (part_of a_2 a_1)) % 20.66/20.97 (about_event a_2 e1)) % 20.66/20.97 (subjection a)) % 20.66/20.97 (bearer a marketplace)) % 20.66/20.97 (cnt a (decl distrib) concert_ds)) % 20.66/20.97 False) % 20.66/20.97 (Eq (part_of a a_1) False)) % 20.66/20.97 Clause #119 (by clausification #[118]): ∀ (a a_1 a_2 : Iota), % 20.66/20.97 Or (Eq (about_event a e1) False) % 20.66/20.97 (Or (Eq (part_of a a_1) False) % 20.66/20.97 (Or % 20.66/20.97 (Eq % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And (And (And (founds_rem e1 a_1 f1) (power a_2)) (bearer a_2 philharmonie)) % 20.66/20.97 (cnt a_2 (decl distrib) concert_ds)) % 20.66/20.97 (part_of a_2 a_1)) % 20.66/20.97 (about_event a_2 e1)) % 20.66/20.97 (subjection a)) % 20.66/20.97 (bearer a marketplace)) % 20.66/20.97 False) % 20.66/20.97 (Eq (cnt a (decl distrib) concert_ds) False))) % 20.66/20.97 Clause #120 (by clausification #[119]): ∀ (a a_1 a_2 : Iota), % 20.66/20.97 Or (Eq (about_event a e1) False) % 20.66/20.97 (Or (Eq (part_of a a_1) False) % 20.66/20.97 (Or (Eq (cnt a (decl distrib) concert_ds) False) % 20.66/20.97 (Or % 20.66/20.97 (Eq % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And (And (And (founds_rem e1 a_1 f1) (power a_2)) (bearer a_2 philharmonie)) % 20.66/20.97 (cnt a_2 (decl distrib) concert_ds)) % 20.66/20.97 (part_of a_2 a_1)) % 20.66/20.97 (about_event a_2 e1)) % 20.66/20.97 (subjection a)) % 20.66/20.97 False) % 20.66/20.97 (Eq (bearer a marketplace) False)))) % 20.66/20.97 Clause #121 (by clausification #[120]): ∀ (a a_1 a_2 : Iota), % 20.66/20.97 Or (Eq (about_event a e1) False) % 20.66/20.97 (Or (Eq (part_of a a_1) False) % 20.66/20.97 (Or (Eq (cnt a (decl distrib) concert_ds) False) % 20.66/20.97 (Or (Eq (bearer a marketplace) False) % 20.66/20.97 (Or % 20.66/20.97 (Eq % 20.66/20.97 (And % 20.66/20.97 (And % 20.66/20.97 (And (And (And (founds_rem e1 a_1 f1) (power a_2)) (bearer a_2 philharmonie)) % 20.66/20.97 (cnt a_2 (decl distrib) concert_ds)) % 20.66/20.97 (part_of a_2 a_1)) % 20.66/20.97 (about_event a_2 e1)) % 20.66/20.97 False) % 20.66/20.97 (Eq (subjection a) False))))) % 20.66/20.97 Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), % 20.66/20.97 Or (Eq (about_event a e1) False) % 20.66/20.97 (Or (Eq (part_of a a_1) False) % 20.66/20.97 (Or (Eq (cnt a (decl distrib) concert_ds) False) % 20.66/20.97 (Or (Eq (bearer a marketplace) False) % 20.66/20.97 (Or (Eq (subjection a) False) % 20.66/20.97 (Or % 20.66/20.97 (Eq % 20.66/20.97 (And % 20.66/20.97 (And (And (And (founds_rem e1 a_1 f1) (power a_2)) (bearer a_2 philharmonie)) % 20.66/20.97 (cnt a_2 (decl distrib) concert_ds)) % 20.66/20.97 (part_of a_2 a_1)) % 20.66/20.97 False) % 20.66/20.97 (Eq (about_event a_2 e1) False)))))) % 20.66/20.97 Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 : Iota), % 20.66/20.97 Or (Eq (about_event a e1) False) % 20.66/20.97 (Or (Eq (part_of a a_1) False) % 20.66/20.97 (Or (Eq (cnt a (decl distrib) concert_ds) False) % 20.66/20.97 (Or (Eq (bearer a marketplace) False) % 20.66/20.97 (Or (Eq (subjection a) False) % 20.66/20.97 (Or (Eq (about_event a_2 e1) False) % 20.66/20.97 (Or % 20.66/20.97 (Eq % 20.66/20.97 (And (And (And (founds_rem e1 a_1 f1) (power a_2)) (bearer a_2 philharmonie)) % 20.66/20.97 (cnt a_2 (decl distrib) concert_ds)) % 20.66/20.97 False) % 20.66/20.97 (Eq (part_of a_2 a_1) False))))))) % 20.66/20.97 Clause #124 (by clausification #[123]): ∀ (a a_1 a_2 : Iota), % 20.66/20.97 Or (Eq (about_event a e1) False) % 20.66/20.97 (Or (Eq (part_of a a_1) False) % 20.66/20.97 (Or (Eq (cnt a (decl distrib) concert_ds) False) % 20.66/20.97 (Or (Eq (bearer a marketplace) False) % 20.66/20.97 (Or (Eq (subjection a) False) % 20.66/20.97 (Or (Eq (about_event a_2 e1) False) % 20.66/20.97 (Or (Eq (part_of a_2 a_1) False) % 20.66/20.97 (Or (Eq (And (And (founds_rem e1 a_1 f1) (power a_2)) (bearer a_2 philharmonie)) False) % 20.66/21.02 (Eq (cnt a_2 (decl distrib) concert_ds) False)))))))) % 20.66/21.02 Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 20.66/21.02 Or (Eq (about_event a e1) False) % 20.66/21.02 (Or (Eq (part_of a a_1) False) % 20.66/21.02 (Or (Eq (cnt a (decl distrib) concert_ds) False) % 20.66/21.02 (Or (Eq (bearer a marketplace) False) % 20.66/21.02 (Or (Eq (subjection a) False) % 20.66/21.02 (Or (Eq (about_event a_2 e1) False) % 20.66/21.02 (Or (Eq (part_of a_2 a_1) False) % 20.66/21.02 (Or (Eq (cnt a_2 (decl distrib) concert_ds) False) % 20.66/21.02 (Or (Eq (And (founds_rem e1 a_1 f1) (power a_2)) False) (Eq (bearer a_2 philharmonie) False))))))))) % 20.66/21.02 Clause #126 (by clausification #[125]): ∀ (a a_1 a_2 : Iota), % 20.66/21.02 Or (Eq (about_event a e1) False) % 20.66/21.02 (Or (Eq (part_of a a_1) False) % 20.66/21.02 (Or (Eq (cnt a (decl distrib) concert_ds) False) % 20.66/21.02 (Or (Eq (bearer a marketplace) False) % 20.66/21.02 (Or (Eq (subjection a) False) % 20.66/21.02 (Or (Eq (about_event a_2 e1) False) % 20.66/21.02 (Or (Eq (part_of a_2 a_1) False) % 20.66/21.02 (Or (Eq (cnt a_2 (decl distrib) concert_ds) False) % 20.66/21.02 (Or (Eq (bearer a_2 philharmonie) False) % 20.66/21.02 (Or (Eq (founds_rem e1 a_1 f1) False) (Eq (power a_2) False)))))))))) % 20.66/21.02 Clause #170 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.66/21.02 Or (Eq (activates a a_1) False) % 20.66/21.02 (Or (Eq (tgt a_1 a_2) False) % 20.66/21.02 (Or (Eq (act a_1 a_3) False) % 20.66/21.02 (Or (Eq (aer a_1 a_4) False) % 20.66/21.02 (Or % 20.66/21.02 (Eq % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 20.66/21.02 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 20.66/21.02 (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 20.66/21.02 (cnt (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (decl a_3) a_2)) % 20.66/21.02 (part_of (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6))) % 20.66/21.02 (subjection (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8))) % 20.66/21.02 (bearer (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_5)) % 20.66/21.02 (cnt (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (decl a_3) a_2)) % 20.66/21.02 True) % 20.66/21.02 (Or (Eq (And (proh a_1) (has_rem a_1)) False) (Eq (aee a_1 a_5) False)))))) % 20.66/21.02 Clause #171 (by clausification #[170]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.66/21.02 Or (Eq (activates a a_1) False) % 20.66/21.02 (Or (Eq (tgt a_1 a_2) False) % 20.66/21.02 (Or (Eq (act a_1 a_3) False) % 20.66/21.02 (Or (Eq (aer a_1 a_4) False) % 20.66/21.02 (Or (Eq (And (proh a_1) (has_rem a_1)) False) % 20.66/21.02 (Or (Eq (aee a_1 a_5) False) (Eq (cnt (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (decl a_3) a_2) True)))))) % 20.66/21.02 Clause #172 (by clausification #[170]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.66/21.02 Or (Eq (activates a a_1) False) % 20.66/21.02 (Or (Eq (tgt a_1 a_2) False) % 20.66/21.02 (Or (Eq (act a_1 a_3) False) % 20.66/21.02 (Or (Eq (aer a_1 a_4) False) % 20.66/21.02 (Or (Eq (And (proh a_1) (has_rem a_1)) False) % 20.66/21.02 (Or (Eq (aee a_1 a_5) False) % 20.66/21.02 (Eq % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And % 20.66/21.02 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 20.66/21.02 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 20.66/21.02 (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 20.66/21.02 (cnt (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (decl a_3) a_2)) % 20.66/21.02 (part_of (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6))) % 20.66/21.02 (subjection (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8))) % 20.66/21.02 (bearer (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_5)) % 20.66/21.02 True)))))) % 20.66/21.02 Clause #173 (by clausification #[171]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.66/21.02 Or (Eq (activates a a_1) False) % 20.66/21.02 (Or (Eq (tgt a_1 a_2) False) % 20.79/21.08 (Or (Eq (act a_1 a_3) False) % 20.79/21.08 (Or (Eq (aer a_1 a_4) False) % 20.79/21.08 (Or (Eq (aee a_1 a_5) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) (decl a_3) a_2) True) % 20.79/21.08 (Or (Eq (proh a_1) False) (Eq (has_rem a_1) False))))))) % 20.79/21.08 Clause #174 (by superposition #[173, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.79/21.08 Or (Eq (tgt f1 a) False) % 20.79/21.08 (Or (Eq (act f1 a_1) False) % 20.79/21.08 (Or (Eq (aer f1 a_2) False) % 20.79/21.08 (Or (Eq (aee f1 a_3) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (decl a_1) a) True) % 20.79/21.08 (Or (Eq (proh f1) False) (Or (Eq (has_rem f1) False) (Eq False True))))))) % 20.79/21.08 Clause #178 (by clausification #[174]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.79/21.08 Or (Eq (tgt f1 a) False) % 20.79/21.08 (Or (Eq (act f1 a_1) False) % 20.79/21.08 (Or (Eq (aer f1 a_2) False) % 20.79/21.08 (Or (Eq (aee f1 a_3) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (decl a_1) a) True) % 20.79/21.08 (Or (Eq (proh f1) False) (Eq (has_rem f1) False)))))) % 20.79/21.08 Clause #179 (by forward demodulation #[178, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.79/21.08 Or (Eq (tgt f1 a) False) % 20.79/21.08 (Or (Eq (act f1 a_1) False) % 20.79/21.08 (Or (Eq (aer f1 a_2) False) % 20.79/21.08 (Or (Eq (aee f1 a_3) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (decl a_1) a) True) % 20.79/21.08 (Or (Eq True False) (Eq (has_rem f1) False)))))) % 20.79/21.08 Clause #180 (by clausification #[179]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.79/21.08 Or (Eq (tgt f1 a) False) % 20.79/21.08 (Or (Eq (act f1 a_1) False) % 20.79/21.08 (Or (Eq (aer f1 a_2) False) % 20.79/21.08 (Or (Eq (aee f1 a_3) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (decl a_1) a) True) (Eq (has_rem f1) False))))) % 20.79/21.08 Clause #181 (by forward demodulation #[180, 15]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.79/21.08 Or (Eq (tgt f1 a) False) % 20.79/21.08 (Or (Eq (act f1 a_1) False) % 20.79/21.08 (Or (Eq (aer f1 a_2) False) % 20.79/21.08 (Or (Eq (aee f1 a_3) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (decl a_1) a) True) (Eq True False))))) % 20.79/21.08 Clause #182 (by clausification #[181]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.79/21.08 Or (Eq (tgt f1 a) False) % 20.79/21.08 (Or (Eq (act f1 a_1) False) % 20.79/21.08 (Or (Eq (aer f1 a_2) False) % 20.79/21.08 (Or (Eq (aee f1 a_3) False) (Eq (cnt (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (decl a_1) a) True)))) % 20.79/21.08 Clause #183 (by superposition #[182, 19]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.79/21.08 Or (Eq (act f1 a) False) % 20.79/21.08 (Or (Eq (aer f1 a_1) False) % 20.79/21.08 (Or (Eq (aee f1 a_2) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 e1 f1 a_1 a concert_ds a_2 a_3 a_4 a_5) (decl a) concert_ds) True) (Eq False True)))) % 20.79/21.08 Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.79/21.08 Or (Eq (act f1 a) False) % 20.79/21.08 (Or (Eq (aer f1 a_1) False) % 20.79/21.08 (Or (Eq (aee f1 a_2) False) (Eq (cnt (skS.0 5 e1 f1 a_1 a concert_ds a_2 a_3 a_4 a_5) (decl a) concert_ds) True))) % 20.79/21.08 Clause #185 (by superposition #[184, 18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.79/21.08 Or (Eq (aer f1 a) False) % 20.79/21.08 (Or (Eq (aee f1 a_1) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 e1 f1 a distrib concert_ds a_1 a_2 a_3 a_4) (decl distrib) concert_ds) True) % 20.79/21.08 (Eq False True))) % 20.79/21.08 Clause #186 (by clausification #[185]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.79/21.08 Or (Eq (aer f1 a) False) % 20.79/21.08 (Or (Eq (aee f1 a_1) False) % 20.79/21.08 (Eq (cnt (skS.0 5 e1 f1 a distrib concert_ds a_1 a_2 a_3 a_4) (decl distrib) concert_ds) True)) % 20.79/21.08 Clause #187 (by superposition #[186, 17]): ∀ (a a_1 a_2 a_3 : Iota), % 20.79/21.08 Or (Eq (aee f1 a) False) % 20.79/21.08 (Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds a a_1 a_2 a_3) (decl distrib) concert_ds) True) % 20.79/21.08 (Eq False True)) % 20.79/21.08 Clause #192 (by clausification #[187]): ∀ (a a_1 a_2 a_3 : Iota), % 20.79/21.08 Or (Eq (aee f1 a) False) % 20.79/21.08 (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds a a_1 a_2 a_3) (decl distrib) concert_ds) True) % 20.79/21.08 Clause #193 (by superposition #[192, 16]): ∀ (a a_1 a_2 : Iota), % 20.79/21.08 Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) True) % 20.79/21.08 (Eq False True) % 20.79/21.08 Clause #194 (by clausification #[193]): ∀ (a a_1 a_2 : Iota), % 20.79/21.08 Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) True % 20.89/21.15 Clause #201 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.89/21.15 Or (Eq (tgt f1 a) False) % 20.89/21.15 (Or (Eq (act f1 a_1) False) % 20.89/21.15 (Or (Eq (aer f1 a_2) False) % 20.89/21.15 (Or (Eq (part_of (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True) % 20.89/21.15 (Or (Eq (aee f1 a_3) False) (Or (Eq (proh f1) False) (Eq (has_rem f1) False)))))) % 20.89/21.15 Clause #202 (by forward demodulation #[201, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.89/21.15 Or (Eq (tgt f1 a) False) % 20.89/21.15 (Or (Eq (act f1 a_1) False) % 20.89/21.15 (Or (Eq (aer f1 a_2) False) % 20.89/21.15 (Or (Eq (part_of (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True) % 20.89/21.15 (Or (Eq (aee f1 a_3) False) (Or (Eq True False) (Eq (has_rem f1) False)))))) % 20.89/21.15 Clause #203 (by clausification #[202]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.89/21.15 Or (Eq (tgt f1 a) False) % 20.89/21.15 (Or (Eq (act f1 a_1) False) % 20.89/21.15 (Or (Eq (aer f1 a_2) False) % 20.89/21.15 (Or (Eq (part_of (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True) % 20.89/21.15 (Or (Eq (aee f1 a_3) False) (Eq (has_rem f1) False))))) % 20.89/21.15 Clause #204 (by forward demodulation #[203, 15]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.89/21.15 Or (Eq (tgt f1 a) False) % 20.89/21.15 (Or (Eq (act f1 a_1) False) % 20.89/21.15 (Or (Eq (aer f1 a_2) False) % 20.89/21.15 (Or (Eq (part_of (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True) % 20.89/21.15 (Or (Eq (aee f1 a_3) False) (Eq True False))))) % 20.89/21.15 Clause #205 (by clausification #[204]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.89/21.15 Or (Eq (tgt f1 a) False) % 20.89/21.15 (Or (Eq (act f1 a_1) False) % 20.89/21.15 (Or (Eq (aer f1 a_2) False) % 20.89/21.15 (Or (Eq (part_of (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True) % 20.89/21.15 (Eq (aee f1 a_3) False)))) % 20.89/21.15 Clause #206 (by superposition #[205, 19]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.89/21.15 Or (Eq (act f1 a) False) % 20.89/21.15 (Or (Eq (aer f1 a_1) False) % 20.89/21.15 (Or (Eq (part_of (skS.0 5 e1 f1 a_1 a concert_ds a_2 a_3 a_4 a_5) (skS.0 3 e1 f1 a_1 a concert_ds a_2 a_3)) True) % 20.89/21.15 (Or (Eq (aee f1 a_2) False) (Eq False True)))) % 20.89/21.15 Clause #208 (by clausification #[206]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.89/21.15 Or (Eq (act f1 a) False) % 20.89/21.15 (Or (Eq (aer f1 a_1) False) % 20.89/21.15 (Or (Eq (part_of (skS.0 5 e1 f1 a_1 a concert_ds a_2 a_3 a_4 a_5) (skS.0 3 e1 f1 a_1 a concert_ds a_2 a_3)) True) % 20.89/21.15 (Eq (aee f1 a_2) False))) % 20.89/21.15 Clause #209 (by superposition #[208, 18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.89/21.15 Or (Eq (aer f1 a) False) % 20.89/21.15 (Or % 20.89/21.15 (Eq (part_of (skS.0 5 e1 f1 a distrib concert_ds a_1 a_2 a_3 a_4) (skS.0 3 e1 f1 a distrib concert_ds a_1 a_2)) % 20.89/21.15 True) % 20.89/21.15 (Or (Eq (aee f1 a_1) False) (Eq False True))) % 20.89/21.15 Clause #210 (by clausification #[209]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.89/21.15 Or (Eq (aer f1 a) False) % 20.89/21.15 (Or % 20.89/21.15 (Eq (part_of (skS.0 5 e1 f1 a distrib concert_ds a_1 a_2 a_3 a_4) (skS.0 3 e1 f1 a distrib concert_ds a_1 a_2)) % 20.89/21.15 True) % 20.89/21.15 (Eq (aee f1 a_1) False)) % 20.89/21.15 Clause #211 (by superposition #[210, 17]): ∀ (a a_1 a_2 a_3 : Iota), % 20.89/21.15 Or % 20.89/21.15 (Eq % 20.89/21.15 (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds a a_1 a_2 a_3) % 20.89/21.15 (skS.0 3 e1 f1 philharmonie distrib concert_ds a a_1)) % 20.89/21.15 True) % 20.89/21.15 (Or (Eq (aee f1 a) False) (Eq False True)) % 20.89/21.15 Clause #212 (by clausification #[211]): ∀ (a a_1 a_2 a_3 : Iota), % 20.89/21.15 Or % 20.89/21.15 (Eq % 20.89/21.15 (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds a a_1 a_2 a_3) % 20.89/21.15 (skS.0 3 e1 f1 philharmonie distrib concert_ds a a_1)) % 20.89/21.15 True) % 20.89/21.15 (Eq (aee f1 a) False) % 20.89/21.15 Clause #213 (by superposition #[212, 16]): ∀ (a a_1 a_2 : Iota), % 20.89/21.15 Or % 20.89/21.15 (Eq % 20.89/21.15 (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) % 20.89/21.15 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a)) % 20.89/21.15 True) % 20.89/21.15 (Eq False True) % 20.89/21.15 Clause #214 (by clausification #[213]): ∀ (a a_1 a_2 : Iota), % 20.89/21.15 Eq % 20.89/21.15 (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) % 20.89/21.15 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a)) % 20.89/21.15 True % 20.89/21.15 Clause #244 (by clausification #[172]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.96/21.20 Or (Eq (activates a a_1) False) % 20.96/21.20 (Or (Eq (tgt a_1 a_2) False) % 20.96/21.20 (Or (Eq (act a_1 a_3) False) % 20.96/21.20 (Or (Eq (aer a_1 a_4) False) % 20.96/21.20 (Or (Eq (aee a_1 a_5) False) % 20.96/21.20 (Or % 20.96/21.20 (Eq % 20.96/21.20 (And % 20.96/21.20 (And % 20.96/21.20 (And % 20.96/21.20 (And % 20.96/21.20 (And % 20.96/21.20 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 20.96/21.20 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 20.96/21.20 (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 20.96/21.20 (cnt (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (decl a_3) a_2)) % 20.96/21.20 (part_of (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6))) % 20.96/21.20 (subjection (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8))) % 20.96/21.20 (bearer (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_5)) % 20.96/21.20 True) % 20.96/21.20 (Or (Eq (proh a_1) False) (Eq (has_rem a_1) False))))))) % 20.96/21.20 Clause #245 (by clausification #[244]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.96/21.20 Or (Eq (activates a a_1) False) % 20.96/21.20 (Or (Eq (tgt a_1 a_2) False) % 20.96/21.20 (Or (Eq (act a_1 a_3) False) % 20.96/21.20 (Or (Eq (aer a_1 a_4) False) % 20.96/21.20 (Or (Eq (aee a_1 a_5) False) % 20.96/21.20 (Or (Eq (proh a_1) False) % 20.96/21.20 (Or (Eq (has_rem a_1) False) (Eq (bearer (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8) a_5) True))))))) % 20.96/21.20 Clause #246 (by clausification #[244]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.96/21.20 Or (Eq (activates a a_1) False) % 20.96/21.20 (Or (Eq (tgt a_1 a_2) False) % 20.96/21.20 (Or (Eq (act a_1 a_3) False) % 20.96/21.20 (Or (Eq (aer a_1 a_4) False) % 20.96/21.20 (Or (Eq (aee a_1 a_5) False) % 20.96/21.20 (Or (Eq (proh a_1) False) % 20.96/21.20 (Or (Eq (has_rem a_1) False) % 20.96/21.20 (Eq % 20.96/21.20 (And % 20.96/21.20 (And % 20.96/21.20 (And % 20.96/21.20 (And % 20.96/21.20 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 20.96/21.20 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 20.96/21.20 (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 20.96/21.20 (cnt (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (decl a_3) a_2)) % 20.96/21.20 (part_of (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6))) % 20.96/21.20 (subjection (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8))) % 20.96/21.20 True))))))) % 20.96/21.20 Clause #247 (by superposition #[245, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.96/21.20 Or (Eq (tgt f1 a) False) % 20.96/21.20 (Or (Eq (act f1 a_1) False) % 20.96/21.20 (Or (Eq (aer f1 a_2) False) % 20.96/21.20 (Or (Eq (aee f1 a_3) False) % 20.96/21.20 (Or (Eq (proh f1) False) % 20.96/21.20 (Or (Eq (has_rem f1) False) % 20.96/21.20 (Or (Eq (bearer (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) a_3) True) (Eq False True))))))) % 20.96/21.20 Clause #248 (by clausification #[247]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.96/21.20 Or (Eq (tgt f1 a) False) % 20.96/21.20 (Or (Eq (act f1 a_1) False) % 20.96/21.20 (Or (Eq (aer f1 a_2) False) % 20.96/21.20 (Or (Eq (aee f1 a_3) False) % 20.96/21.20 (Or (Eq (proh f1) False) % 20.96/21.20 (Or (Eq (has_rem f1) False) (Eq (bearer (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) a_3) True)))))) % 20.96/21.20 Clause #249 (by forward demodulation #[248, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.96/21.20 Or (Eq (tgt f1 a) False) % 20.96/21.20 (Or (Eq (act f1 a_1) False) % 20.96/21.20 (Or (Eq (aer f1 a_2) False) % 20.96/21.20 (Or (Eq (aee f1 a_3) False) % 20.96/21.20 (Or (Eq True False) % 20.96/21.20 (Or (Eq (has_rem f1) False) (Eq (bearer (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) a_3) True)))))) % 20.96/21.20 Clause #250 (by clausification #[249]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.96/21.20 Or (Eq (tgt f1 a) False) % 20.96/21.20 (Or (Eq (act f1 a_1) False) % 20.96/21.20 (Or (Eq (aer f1 a_2) False) % 20.96/21.20 (Or (Eq (aee f1 a_3) False) % 20.96/21.20 (Or (Eq (has_rem f1) False) (Eq (bearer (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) a_3) True))))) % 20.96/21.20 Clause #251 (by forward demodulation #[250, 15]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.96/21.20 Or (Eq (tgt f1 a) False) % 20.96/21.20 (Or (Eq (act f1 a_1) False) % 20.96/21.20 (Or (Eq (aer f1 a_2) False) % 20.96/21.25 (Or (Eq (aee f1 a_3) False) % 20.96/21.25 (Or (Eq True False) (Eq (bearer (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) a_3) True))))) % 20.96/21.25 Clause #252 (by clausification #[251]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.96/21.25 Or (Eq (tgt f1 a) False) % 20.96/21.25 (Or (Eq (act f1 a_1) False) % 20.96/21.25 (Or (Eq (aer f1 a_2) False) % 20.96/21.25 (Or (Eq (aee f1 a_3) False) (Eq (bearer (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6) a_3) True)))) % 20.96/21.25 Clause #253 (by superposition #[252, 19]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.96/21.25 Or (Eq (act f1 a) False) % 20.96/21.25 (Or (Eq (aer f1 a_1) False) % 20.96/21.25 (Or (Eq (aee f1 a_2) False) % 20.96/21.25 (Or (Eq (bearer (skS.0 5 e1 f1 a_1 a concert_ds a_2 a_3 a_4 a_5) a_2) True) (Eq False True)))) % 20.96/21.25 Clause #254 (by clausification #[253]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.96/21.25 Or (Eq (act f1 a) False) % 20.96/21.25 (Or (Eq (aer f1 a_1) False) % 20.96/21.25 (Or (Eq (aee f1 a_2) False) (Eq (bearer (skS.0 5 e1 f1 a_1 a concert_ds a_2 a_3 a_4 a_5) a_2) True))) % 20.96/21.25 Clause #255 (by superposition #[254, 18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.96/21.25 Or (Eq (aer f1 a) False) % 20.96/21.25 (Or (Eq (aee f1 a_1) False) % 20.96/21.25 (Or (Eq (bearer (skS.0 5 e1 f1 a distrib concert_ds a_1 a_2 a_3 a_4) a_1) True) (Eq False True))) % 20.96/21.25 Clause #256 (by clausification #[255]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.96/21.25 Or (Eq (aer f1 a) False) % 20.96/21.25 (Or (Eq (aee f1 a_1) False) (Eq (bearer (skS.0 5 e1 f1 a distrib concert_ds a_1 a_2 a_3 a_4) a_1) True)) % 20.96/21.25 Clause #257 (by superposition #[256, 17]): ∀ (a a_1 a_2 a_3 : Iota), % 20.96/21.25 Or (Eq (aee f1 a) False) % 20.96/21.25 (Or (Eq (bearer (skS.0 5 e1 f1 philharmonie distrib concert_ds a a_1 a_2 a_3) a) True) (Eq False True)) % 20.96/21.25 Clause #258 (by clausification #[257]): ∀ (a a_1 a_2 a_3 : Iota), % 20.96/21.25 Or (Eq (aee f1 a) False) (Eq (bearer (skS.0 5 e1 f1 philharmonie distrib concert_ds a a_1 a_2 a_3) a) True) % 20.96/21.25 Clause #259 (by superposition #[258, 16]): ∀ (a a_1 a_2 : Iota), % 20.96/21.25 Or (Eq (bearer (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) marketplace) True) % 20.96/21.25 (Eq False True) % 20.96/21.25 Clause #260 (by clausification #[259]): ∀ (a a_1 a_2 : Iota), Eq (bearer (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) marketplace) True % 20.96/21.25 Clause #281 (by clausification #[246]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 20.96/21.25 Or (Eq (activates a a_1) False) % 20.96/21.25 (Or (Eq (tgt a_1 a_2) False) % 20.96/21.25 (Or (Eq (act a_1 a_3) False) % 20.96/21.25 (Or (Eq (aer a_1 a_4) False) % 20.96/21.25 (Or (Eq (aee a_1 a_5) False) % 20.96/21.25 (Or (Eq (proh a_1) False) % 20.96/21.25 (Or (Eq (has_rem a_1) False) (Eq (subjection (skS.0 5 a a_1 a_4 a_3 a_2 a_5 a_6 a_7 a_8)) True))))))) % 20.96/21.25 Clause #282 (by clausification #[246]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.96/21.25 Or (Eq (activates a a_1) False) % 20.96/21.25 (Or (Eq (tgt a_1 a_2) False) % 20.96/21.25 (Or (Eq (act a_1 a_3) False) % 20.96/21.25 (Or (Eq (aer a_1 a_4) False) % 20.96/21.25 (Or (Eq (aee a_1 a_5) False) % 20.96/21.25 (Or (Eq (proh a_1) False) % 20.96/21.25 (Or (Eq (has_rem a_1) False) % 20.96/21.25 (Eq % 20.96/21.25 (And % 20.96/21.25 (And % 20.96/21.25 (And % 20.96/21.25 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 20.96/21.25 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 20.96/21.25 (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 20.96/21.25 (cnt (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (decl a_3) a_2)) % 20.96/21.25 (part_of (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6))) % 20.96/21.25 True))))))) % 20.96/21.25 Clause #283 (by superposition #[281, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.96/21.25 Or (Eq (tgt f1 a) False) % 20.96/21.25 (Or (Eq (act f1 a_1) False) % 20.96/21.25 (Or (Eq (aer f1 a_2) False) % 20.96/21.25 (Or (Eq (aee f1 a_3) False) % 20.96/21.25 (Or (Eq (proh f1) False) % 20.96/21.25 (Or (Eq (has_rem f1) False) % 20.96/21.25 (Or (Eq (subjection (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6)) True) (Eq False True))))))) % 20.96/21.25 Clause #284 (by clausification #[283]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.96/21.25 Or (Eq (tgt f1 a) False) % 20.96/21.25 (Or (Eq (act f1 a_1) False) % 20.96/21.25 (Or (Eq (aer f1 a_2) False) % 20.96/21.25 (Or (Eq (aee f1 a_3) False) % 20.96/21.25 (Or (Eq (proh f1) False) % 20.96/21.25 (Or (Eq (has_rem f1) False) (Eq (subjection (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6)) True)))))) % 21.06/21.31 Clause #285 (by forward demodulation #[284, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 21.06/21.31 Or (Eq (tgt f1 a) False) % 21.06/21.31 (Or (Eq (act f1 a_1) False) % 21.06/21.31 (Or (Eq (aer f1 a_2) False) % 21.06/21.31 (Or (Eq (aee f1 a_3) False) % 21.06/21.31 (Or (Eq True False) % 21.06/21.31 (Or (Eq (has_rem f1) False) (Eq (subjection (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6)) True)))))) % 21.06/21.31 Clause #286 (by clausification #[285]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 21.06/21.31 Or (Eq (tgt f1 a) False) % 21.06/21.31 (Or (Eq (act f1 a_1) False) % 21.06/21.31 (Or (Eq (aer f1 a_2) False) % 21.06/21.31 (Or (Eq (aee f1 a_3) False) % 21.06/21.31 (Or (Eq (has_rem f1) False) (Eq (subjection (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6)) True))))) % 21.06/21.31 Clause #287 (by forward demodulation #[286, 15]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 21.06/21.31 Or (Eq (tgt f1 a) False) % 21.06/21.31 (Or (Eq (act f1 a_1) False) % 21.06/21.31 (Or (Eq (aer f1 a_2) False) % 21.06/21.31 (Or (Eq (aee f1 a_3) False) % 21.06/21.31 (Or (Eq True False) (Eq (subjection (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6)) True))))) % 21.06/21.31 Clause #288 (by clausification #[287]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 21.06/21.31 Or (Eq (tgt f1 a) False) % 21.06/21.31 (Or (Eq (act f1 a_1) False) % 21.06/21.31 (Or (Eq (aer f1 a_2) False) % 21.06/21.31 (Or (Eq (aee f1 a_3) False) (Eq (subjection (skS.0 5 e1 f1 a_2 a_1 a a_3 a_4 a_5 a_6)) True)))) % 21.06/21.31 Clause #289 (by superposition #[288, 19]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.06/21.31 Or (Eq (act f1 a) False) % 21.06/21.31 (Or (Eq (aer f1 a_1) False) % 21.06/21.31 (Or (Eq (aee f1 a_2) False) % 21.06/21.31 (Or (Eq (subjection (skS.0 5 e1 f1 a_1 a concert_ds a_2 a_3 a_4 a_5)) True) (Eq False True)))) % 21.06/21.31 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.06/21.31 Or (Eq (act f1 a) False) % 21.06/21.31 (Or (Eq (aer f1 a_1) False) % 21.06/21.31 (Or (Eq (aee f1 a_2) False) (Eq (subjection (skS.0 5 e1 f1 a_1 a concert_ds a_2 a_3 a_4 a_5)) True))) % 21.06/21.31 Clause #291 (by superposition #[290, 18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.06/21.31 Or (Eq (aer f1 a) False) % 21.06/21.31 (Or (Eq (aee f1 a_1) False) % 21.06/21.31 (Or (Eq (subjection (skS.0 5 e1 f1 a distrib concert_ds a_1 a_2 a_3 a_4)) True) (Eq False True))) % 21.06/21.31 Clause #292 (by clausification #[291]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.06/21.31 Or (Eq (aer f1 a) False) % 21.06/21.31 (Or (Eq (aee f1 a_1) False) (Eq (subjection (skS.0 5 e1 f1 a distrib concert_ds a_1 a_2 a_3 a_4)) True)) % 21.06/21.31 Clause #293 (by superposition #[292, 17]): ∀ (a a_1 a_2 a_3 : Iota), % 21.06/21.31 Or (Eq (aee f1 a) False) % 21.06/21.31 (Or (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds a a_1 a_2 a_3)) True) (Eq False True)) % 21.06/21.31 Clause #294 (by clausification #[293]): ∀ (a a_1 a_2 a_3 : Iota), % 21.06/21.31 Or (Eq (aee f1 a) False) (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds a a_1 a_2 a_3)) True) % 21.06/21.31 Clause #295 (by superposition #[294, 16]): ∀ (a a_1 a_2 : Iota), % 21.06/21.31 Or (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2)) True) (Eq False True) % 21.06/21.31 Clause #296 (by clausification #[295]): ∀ (a a_1 a_2 : Iota), Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2)) True % 21.06/21.31 Clause #311 (by clausification #[282]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.06/21.31 Or (Eq (activates a a_1) False) % 21.06/21.31 (Or (Eq (tgt a_1 a_2) False) % 21.06/21.31 (Or (Eq (act a_1 a_3) False) % 21.06/21.31 (Or (Eq (aer a_1 a_4) False) % 21.06/21.31 (Or (Eq (aee a_1 a_5) False) % 21.06/21.31 (Or (Eq (proh a_1) False) % 21.06/21.31 (Or (Eq (has_rem a_1) False) % 21.06/21.31 (Eq (part_of (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6)) True))))))) % 21.06/21.31 Clause #312 (by clausification #[282]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.06/21.31 Or (Eq (activates a a_1) False) % 21.06/21.31 (Or (Eq (tgt a_1 a_2) False) % 21.06/21.31 (Or (Eq (act a_1 a_3) False) % 21.06/21.31 (Or (Eq (aer a_1 a_4) False) % 21.06/21.31 (Or (Eq (aee a_1 a_5) False) % 21.06/21.31 (Or (Eq (proh a_1) False) % 21.06/21.31 (Or (Eq (has_rem a_1) False) % 21.06/21.31 (Eq % 21.06/21.31 (And % 21.06/21.31 (And % 21.06/21.31 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 21.06/21.31 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 21.06/21.31 (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 21.06/21.37 (cnt (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (decl a_3) a_2)) % 21.06/21.37 True))))))) % 21.06/21.37 Clause #313 (by superposition #[311, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.06/21.37 Or (Eq (tgt f1 a) False) % 21.06/21.37 (Or (Eq (act f1 a_1) False) % 21.06/21.37 (Or (Eq (aer f1 a_2) False) % 21.06/21.37 (Or (Eq (aee f1 a_3) False) % 21.06/21.37 (Or (Eq (proh f1) False) % 21.06/21.37 (Or (Eq (has_rem f1) False) % 21.06/21.37 (Or (Eq (part_of (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True) % 21.06/21.37 (Eq False True))))))) % 21.06/21.37 Clause #314 (by clausification #[313]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.06/21.37 Or (Eq (tgt f1 a) False) % 21.06/21.37 (Or (Eq (act f1 a_1) False) % 21.06/21.37 (Or (Eq (aer f1 a_2) False) % 21.06/21.37 (Or (Eq (aee f1 a_3) False) % 21.06/21.37 (Or (Eq (proh f1) False) % 21.06/21.37 (Or (Eq (has_rem f1) False) % 21.06/21.37 (Eq (part_of (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True)))))) % 21.06/21.37 Clause #315 (by forward demodulation #[314, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.06/21.37 Or (Eq (tgt f1 a) False) % 21.06/21.37 (Or (Eq (act f1 a_1) False) % 21.06/21.37 (Or (Eq (aer f1 a_2) False) % 21.06/21.37 (Or (Eq (aee f1 a_3) False) % 21.06/21.37 (Or (Eq True False) % 21.06/21.37 (Or (Eq (has_rem f1) False) % 21.06/21.37 (Eq (part_of (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True)))))) % 21.06/21.37 Clause #316 (by clausification #[315]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.06/21.37 Or (Eq (tgt f1 a) False) % 21.06/21.37 (Or (Eq (act f1 a_1) False) % 21.06/21.37 (Or (Eq (aer f1 a_2) False) % 21.06/21.37 (Or (Eq (aee f1 a_3) False) % 21.06/21.37 (Or (Eq (has_rem f1) False) % 21.06/21.37 (Eq (part_of (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True))))) % 21.06/21.37 Clause #317 (by forward demodulation #[316, 15]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.06/21.37 Or (Eq (tgt f1 a) False) % 21.06/21.37 (Or (Eq (act f1 a_1) False) % 21.06/21.37 (Or (Eq (aer f1 a_2) False) % 21.06/21.37 (Or (Eq (aee f1 a_3) False) % 21.06/21.37 (Or (Eq True False) % 21.06/21.37 (Eq (part_of (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True))))) % 21.06/21.37 Clause #318 (by clausification #[317]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.06/21.37 Or (Eq (tgt f1 a) False) % 21.06/21.37 (Or (Eq (act f1 a_1) False) % 21.06/21.37 (Or (Eq (aer f1 a_2) False) % 21.06/21.37 (Or (Eq (aee f1 a_3) False) % 21.06/21.37 (Eq (part_of (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4)) True)))) % 21.06/21.37 Clause #319 (by superposition #[318, 19]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.06/21.37 Or (Eq (act f1 a) False) % 21.06/21.37 (Or (Eq (aer f1 a_1) False) % 21.06/21.37 (Or (Eq (aee f1 a_2) False) % 21.06/21.37 (Or (Eq (part_of (skS.0 4 e1 f1 a_1 a concert_ds a_2 a_3 a_4) (skS.0 3 e1 f1 a_1 a concert_ds a_2 a_3)) True) % 21.06/21.37 (Eq False True)))) % 21.06/21.37 Clause #320 (by clausification #[319]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.06/21.37 Or (Eq (act f1 a) False) % 21.06/21.37 (Or (Eq (aer f1 a_1) False) % 21.06/21.37 (Or (Eq (aee f1 a_2) False) % 21.06/21.37 (Eq (part_of (skS.0 4 e1 f1 a_1 a concert_ds a_2 a_3 a_4) (skS.0 3 e1 f1 a_1 a concert_ds a_2 a_3)) True))) % 21.06/21.37 Clause #321 (by superposition #[320, 18]): ∀ (a a_1 a_2 a_3 : Iota), % 21.06/21.37 Or (Eq (aer f1 a) False) % 21.06/21.37 (Or (Eq (aee f1 a_1) False) % 21.06/21.37 (Or % 21.06/21.37 (Eq (part_of (skS.0 4 e1 f1 a distrib concert_ds a_1 a_2 a_3) (skS.0 3 e1 f1 a distrib concert_ds a_1 a_2)) % 21.06/21.37 True) % 21.06/21.37 (Eq False True))) % 21.06/21.37 Clause #322 (by clausification #[321]): ∀ (a a_1 a_2 a_3 : Iota), % 21.06/21.37 Or (Eq (aer f1 a) False) % 21.06/21.37 (Or (Eq (aee f1 a_1) False) % 21.06/21.37 (Eq (part_of (skS.0 4 e1 f1 a distrib concert_ds a_1 a_2 a_3) (skS.0 3 e1 f1 a distrib concert_ds a_1 a_2)) True)) % 21.06/21.37 Clause #323 (by superposition #[322, 17]): ∀ (a a_1 a_2 : Iota), % 21.06/21.37 Or (Eq (aee f1 a) False) % 21.06/21.37 (Or % 21.06/21.37 (Eq % 21.06/21.37 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds a a_1 a_2) % 21.06/21.37 (skS.0 3 e1 f1 philharmonie distrib concert_ds a a_1)) % 21.06/21.37 True) % 21.06/21.37 (Eq False True)) % 21.06/21.37 Clause #324 (by clausification #[323]): ∀ (a a_1 a_2 : Iota), % 21.06/21.37 Or (Eq (aee f1 a) False) % 21.06/21.37 (Eq % 21.06/21.37 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds a a_1 a_2) % 21.06/21.37 (skS.0 3 e1 f1 philharmonie distrib concert_ds a a_1)) % 21.06/21.37 True) % 21.06/21.37 Clause #325 (by superposition #[324, 16]): ∀ (a a_1 : Iota), % 21.16/21.43 Or % 21.16/21.43 (Eq % 21.16/21.43 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.16/21.43 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a)) % 21.16/21.43 True) % 21.16/21.43 (Eq False True) % 21.16/21.43 Clause #326 (by clausification #[325]): ∀ (a a_1 : Iota), % 21.16/21.43 Eq % 21.16/21.43 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.16/21.43 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a)) % 21.16/21.43 True % 21.16/21.43 Clause #341 (by clausification #[312]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.16/21.43 Or (Eq (activates a a_1) False) % 21.16/21.43 (Or (Eq (tgt a_1 a_2) False) % 21.16/21.43 (Or (Eq (act a_1 a_3) False) % 21.16/21.43 (Or (Eq (aer a_1 a_4) False) % 21.16/21.43 (Or (Eq (aee a_1 a_5) False) % 21.16/21.43 (Or (Eq (proh a_1) False) % 21.16/21.43 (Or (Eq (has_rem a_1) False) (Eq (cnt (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) (decl a_3) a_2) True))))))) % 21.16/21.43 Clause #342 (by clausification #[312]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.16/21.43 Or (Eq (activates a a_1) False) % 21.16/21.43 (Or (Eq (tgt a_1 a_2) False) % 21.16/21.44 (Or (Eq (act a_1 a_3) False) % 21.16/21.44 (Or (Eq (aer a_1 a_4) False) % 21.16/21.44 (Or (Eq (aee a_1 a_5) False) % 21.16/21.44 (Or (Eq (proh a_1) False) % 21.16/21.44 (Or (Eq (has_rem a_1) False) % 21.16/21.44 (Eq % 21.16/21.44 (And % 21.16/21.44 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 21.16/21.44 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 21.16/21.44 (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4)) % 21.16/21.44 True))))))) % 21.16/21.44 Clause #343 (by superposition #[341, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.44 Or (Eq (tgt f1 a) False) % 21.16/21.44 (Or (Eq (act f1 a_1) False) % 21.16/21.44 (Or (Eq (aer f1 a_2) False) % 21.16/21.44 (Or (Eq (aee f1 a_3) False) % 21.16/21.44 (Or (Eq (proh f1) False) % 21.16/21.44 (Or (Eq (has_rem f1) False) % 21.16/21.44 (Or (Eq (cnt (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (decl a_1) a) True) (Eq False True))))))) % 21.16/21.44 Clause #344 (by clausification #[343]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.44 Or (Eq (tgt f1 a) False) % 21.16/21.44 (Or (Eq (act f1 a_1) False) % 21.16/21.44 (Or (Eq (aer f1 a_2) False) % 21.16/21.44 (Or (Eq (aee f1 a_3) False) % 21.16/21.44 (Or (Eq (proh f1) False) % 21.16/21.44 (Or (Eq (has_rem f1) False) (Eq (cnt (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (decl a_1) a) True)))))) % 21.16/21.44 Clause #345 (by forward demodulation #[344, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.44 Or (Eq (tgt f1 a) False) % 21.16/21.44 (Or (Eq (act f1 a_1) False) % 21.16/21.44 (Or (Eq (aer f1 a_2) False) % 21.16/21.44 (Or (Eq (aee f1 a_3) False) % 21.16/21.44 (Or (Eq True False) % 21.16/21.44 (Or (Eq (has_rem f1) False) (Eq (cnt (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (decl a_1) a) True)))))) % 21.16/21.44 Clause #346 (by clausification #[345]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.44 Or (Eq (tgt f1 a) False) % 21.16/21.44 (Or (Eq (act f1 a_1) False) % 21.16/21.44 (Or (Eq (aer f1 a_2) False) % 21.16/21.44 (Or (Eq (aee f1 a_3) False) % 21.16/21.44 (Or (Eq (has_rem f1) False) (Eq (cnt (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (decl a_1) a) True))))) % 21.16/21.44 Clause #347 (by forward demodulation #[346, 15]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.44 Or (Eq (tgt f1 a) False) % 21.16/21.44 (Or (Eq (act f1 a_1) False) % 21.16/21.44 (Or (Eq (aer f1 a_2) False) % 21.16/21.44 (Or (Eq (aee f1 a_3) False) % 21.16/21.44 (Or (Eq True False) (Eq (cnt (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (decl a_1) a) True))))) % 21.16/21.44 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.44 Or (Eq (tgt f1 a) False) % 21.16/21.44 (Or (Eq (act f1 a_1) False) % 21.16/21.44 (Or (Eq (aer f1 a_2) False) % 21.16/21.44 (Or (Eq (aee f1 a_3) False) (Eq (cnt (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) (decl a_1) a) True)))) % 21.16/21.44 Clause #349 (by superposition #[348, 19]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.16/21.44 Or (Eq (act f1 a) False) % 21.16/21.44 (Or (Eq (aer f1 a_1) False) % 21.16/21.44 (Or (Eq (aee f1 a_2) False) % 21.16/21.44 (Or (Eq (cnt (skS.0 4 e1 f1 a_1 a concert_ds a_2 a_3 a_4) (decl a) concert_ds) True) (Eq False True)))) % 21.16/21.44 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.16/21.44 Or (Eq (act f1 a) False) % 21.16/21.44 (Or (Eq (aer f1 a_1) False) % 21.16/21.44 (Or (Eq (aee f1 a_2) False) (Eq (cnt (skS.0 4 e1 f1 a_1 a concert_ds a_2 a_3 a_4) (decl a) concert_ds) True))) % 21.16/21.44 Clause #351 (by superposition #[350, 18]): ∀ (a a_1 a_2 a_3 : Iota), % 21.16/21.49 Or (Eq (aer f1 a) False) % 21.16/21.49 (Or (Eq (aee f1 a_1) False) % 21.16/21.49 (Or (Eq (cnt (skS.0 4 e1 f1 a distrib concert_ds a_1 a_2 a_3) (decl distrib) concert_ds) True) (Eq False True))) % 21.16/21.49 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 : Iota), % 21.16/21.49 Or (Eq (aer f1 a) False) % 21.16/21.49 (Or (Eq (aee f1 a_1) False) % 21.16/21.49 (Eq (cnt (skS.0 4 e1 f1 a distrib concert_ds a_1 a_2 a_3) (decl distrib) concert_ds) True)) % 21.16/21.49 Clause #353 (by superposition #[352, 17]): ∀ (a a_1 a_2 : Iota), % 21.16/21.49 Or (Eq (aee f1 a) False) % 21.16/21.49 (Or (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds a a_1 a_2) (decl distrib) concert_ds) True) % 21.16/21.49 (Eq False True)) % 21.16/21.49 Clause #354 (by clausification #[353]): ∀ (a a_1 a_2 : Iota), % 21.16/21.49 Or (Eq (aee f1 a) False) % 21.16/21.49 (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds a a_1 a_2) (decl distrib) concert_ds) True) % 21.16/21.49 Clause #355 (by superposition #[354, 16]): ∀ (a a_1 : Iota), % 21.16/21.49 Or (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) (decl distrib) concert_ds) True) % 21.16/21.49 (Eq False True) % 21.16/21.49 Clause #356 (by clausification #[355]): ∀ (a a_1 : Iota), % 21.16/21.49 Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) (decl distrib) concert_ds) True % 21.16/21.49 Clause #371 (by clausification #[342]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.16/21.49 Or (Eq (activates a a_1) False) % 21.16/21.49 (Or (Eq (tgt a_1 a_2) False) % 21.16/21.49 (Or (Eq (act a_1 a_3) False) % 21.16/21.49 (Or (Eq (aer a_1 a_4) False) % 21.16/21.49 (Or (Eq (aee a_1 a_5) False) % 21.16/21.49 (Or (Eq (proh a_1) False) % 21.16/21.49 (Or (Eq (has_rem a_1) False) (Eq (bearer (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7) a_4) True))))))) % 21.16/21.49 Clause #372 (by clausification #[342]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.16/21.49 Or (Eq (activates a a_1) False) % 21.16/21.49 (Or (Eq (tgt a_1 a_2) False) % 21.16/21.49 (Or (Eq (act a_1 a_3) False) % 21.16/21.49 (Or (Eq (aer a_1 a_4) False) % 21.16/21.49 (Or (Eq (aee a_1 a_5) False) % 21.16/21.49 (Or (Eq (proh a_1) False) % 21.16/21.49 (Or (Eq (has_rem a_1) False) % 21.16/21.49 (Eq % 21.16/21.49 (And (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) % 21.16/21.49 (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7))) % 21.16/21.49 True))))))) % 21.16/21.49 Clause #373 (by superposition #[371, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.49 Or (Eq (tgt f1 a) False) % 21.16/21.49 (Or (Eq (act f1 a_1) False) % 21.16/21.49 (Or (Eq (aer f1 a_2) False) % 21.16/21.49 (Or (Eq (aee f1 a_3) False) % 21.16/21.49 (Or (Eq (proh f1) False) % 21.16/21.49 (Or (Eq (has_rem f1) False) % 21.16/21.49 (Or (Eq (bearer (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) a_2) True) (Eq False True))))))) % 21.16/21.49 Clause #374 (by clausification #[373]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.49 Or (Eq (tgt f1 a) False) % 21.16/21.49 (Or (Eq (act f1 a_1) False) % 21.16/21.49 (Or (Eq (aer f1 a_2) False) % 21.16/21.49 (Or (Eq (aee f1 a_3) False) % 21.16/21.49 (Or (Eq (proh f1) False) % 21.16/21.49 (Or (Eq (has_rem f1) False) (Eq (bearer (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) a_2) True)))))) % 21.16/21.49 Clause #375 (by forward demodulation #[374, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.49 Or (Eq (tgt f1 a) False) % 21.16/21.49 (Or (Eq (act f1 a_1) False) % 21.16/21.49 (Or (Eq (aer f1 a_2) False) % 21.16/21.49 (Or (Eq (aee f1 a_3) False) % 21.16/21.49 (Or (Eq True False) % 21.16/21.49 (Or (Eq (has_rem f1) False) (Eq (bearer (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) a_2) True)))))) % 21.16/21.49 Clause #376 (by clausification #[375]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.49 Or (Eq (tgt f1 a) False) % 21.16/21.49 (Or (Eq (act f1 a_1) False) % 21.16/21.49 (Or (Eq (aer f1 a_2) False) % 21.16/21.49 (Or (Eq (aee f1 a_3) False) % 21.16/21.49 (Or (Eq (has_rem f1) False) (Eq (bearer (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) a_2) True))))) % 21.16/21.49 Clause #377 (by forward demodulation #[376, 15]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.49 Or (Eq (tgt f1 a) False) % 21.16/21.49 (Or (Eq (act f1 a_1) False) % 21.16/21.49 (Or (Eq (aer f1 a_2) False) % 21.16/21.49 (Or (Eq (aee f1 a_3) False) (Or (Eq True False) (Eq (bearer (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) a_2) True))))) % 21.16/21.49 Clause #378 (by clausification #[377]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.16/21.49 Or (Eq (tgt f1 a) False) % 21.16/21.49 (Or (Eq (act f1 a_1) False) % 21.16/21.49 (Or (Eq (aer f1 a_2) False) % 21.16/21.49 (Or (Eq (aee f1 a_3) False) (Eq (bearer (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5) a_2) True)))) % 21.26/21.55 Clause #379 (by superposition #[378, 19]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.26/21.55 Or (Eq (act f1 a) False) % 21.26/21.55 (Or (Eq (aer f1 a_1) False) % 21.26/21.55 (Or (Eq (aee f1 a_2) False) % 21.26/21.55 (Or (Eq (bearer (skS.0 4 e1 f1 a_1 a concert_ds a_2 a_3 a_4) a_1) True) (Eq False True)))) % 21.26/21.55 Clause #380 (by clausification #[379]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.26/21.55 Or (Eq (act f1 a) False) % 21.26/21.55 (Or (Eq (aer f1 a_1) False) % 21.26/21.55 (Or (Eq (aee f1 a_2) False) (Eq (bearer (skS.0 4 e1 f1 a_1 a concert_ds a_2 a_3 a_4) a_1) True))) % 21.26/21.55 Clause #381 (by superposition #[380, 18]): ∀ (a a_1 a_2 a_3 : Iota), % 21.26/21.55 Or (Eq (aer f1 a) False) % 21.26/21.55 (Or (Eq (aee f1 a_1) False) % 21.26/21.55 (Or (Eq (bearer (skS.0 4 e1 f1 a distrib concert_ds a_1 a_2 a_3) a) True) (Eq False True))) % 21.26/21.55 Clause #382 (by clausification #[381]): ∀ (a a_1 a_2 a_3 : Iota), % 21.26/21.55 Or (Eq (aer f1 a) False) % 21.26/21.55 (Or (Eq (aee f1 a_1) False) (Eq (bearer (skS.0 4 e1 f1 a distrib concert_ds a_1 a_2 a_3) a) True)) % 21.26/21.55 Clause #383 (by superposition #[382, 17]): ∀ (a a_1 a_2 : Iota), % 21.26/21.56 Or (Eq (aee f1 a) False) % 21.26/21.56 (Or (Eq (bearer (skS.0 4 e1 f1 philharmonie distrib concert_ds a a_1 a_2) philharmonie) True) (Eq False True)) % 21.26/21.56 Clause #384 (by clausification #[383]): ∀ (a a_1 a_2 : Iota), % 21.26/21.56 Or (Eq (aee f1 a) False) (Eq (bearer (skS.0 4 e1 f1 philharmonie distrib concert_ds a a_1 a_2) philharmonie) True) % 21.26/21.56 Clause #385 (by superposition #[384, 16]): ∀ (a a_1 : Iota), % 21.26/21.56 Or (Eq (bearer (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) philharmonie) True) (Eq False True) % 21.26/21.56 Clause #386 (by clausification #[385]): ∀ (a a_1 : Iota), Eq (bearer (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) philharmonie) True % 21.26/21.56 Clause #401 (by clausification #[372]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.26/21.56 Or (Eq (activates a a_1) False) % 21.26/21.56 (Or (Eq (tgt a_1 a_2) False) % 21.26/21.56 (Or (Eq (act a_1 a_3) False) % 21.26/21.56 (Or (Eq (aer a_1 a_4) False) % 21.26/21.56 (Or (Eq (aee a_1 a_5) False) % 21.26/21.56 (Or (Eq (proh a_1) False) % 21.26/21.56 (Or (Eq (has_rem a_1) False) (Eq (power (skS.0 4 a a_1 a_4 a_3 a_2 a_5 a_6 a_7)) True))))))) % 21.26/21.56 Clause #402 (by clausification #[372]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 21.26/21.56 Or (Eq (activates a a_1) False) % 21.26/21.56 (Or (Eq (tgt a_1 a_2) False) % 21.26/21.56 (Or (Eq (act a_1 a_3) False) % 21.26/21.56 (Or (Eq (aer a_1 a_4) False) % 21.26/21.56 (Or (Eq (aee a_1 a_5) False) % 21.26/21.56 (Or (Eq (proh a_1) False) % 21.26/21.56 (Or (Eq (has_rem a_1) False) (Eq (founds_rem a (skS.0 3 a a_1 a_4 a_3 a_2 a_5 a_6) a_1) True))))))) % 21.26/21.56 Clause #403 (by superposition #[401, 20]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.26/21.56 Or (Eq (tgt f1 a) False) % 21.26/21.56 (Or (Eq (act f1 a_1) False) % 21.26/21.56 (Or (Eq (aer f1 a_2) False) % 21.26/21.56 (Or (Eq (aee f1 a_3) False) % 21.26/21.56 (Or (Eq (proh f1) False) % 21.26/21.56 (Or (Eq (has_rem f1) False) % 21.26/21.56 (Or (Eq (power (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5)) True) (Eq False True))))))) % 21.26/21.56 Clause #415 (by superposition #[402, 20]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.26/21.56 Or (Eq (tgt f1 a) False) % 21.26/21.56 (Or (Eq (act f1 a_1) False) % 21.26/21.56 (Or (Eq (aer f1 a_2) False) % 21.26/21.56 (Or (Eq (aee f1 a_3) False) % 21.26/21.56 (Or (Eq (proh f1) False) % 21.26/21.56 (Or (Eq (has_rem f1) False) % 21.26/21.56 (Or (Eq (founds_rem e1 (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4) f1) True) (Eq False True))))))) % 21.26/21.56 Clause #417 (by clausification #[415]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.26/21.56 Or (Eq (tgt f1 a) False) % 21.26/21.56 (Or (Eq (act f1 a_1) False) % 21.26/21.56 (Or (Eq (aer f1 a_2) False) % 21.26/21.56 (Or (Eq (aee f1 a_3) False) % 21.26/21.56 (Or (Eq (proh f1) False) % 21.26/21.56 (Or (Eq (has_rem f1) False) (Eq (founds_rem e1 (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4) f1) True)))))) % 21.26/21.56 Clause #418 (by forward demodulation #[417, 14]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.26/21.56 Or (Eq (tgt f1 a) False) % 21.26/21.56 (Or (Eq (act f1 a_1) False) % 21.26/21.56 (Or (Eq (aer f1 a_2) False) % 21.26/21.56 (Or (Eq (aee f1 a_3) False) % 21.26/21.56 (Or (Eq True False) % 21.26/21.56 (Or (Eq (has_rem f1) False) (Eq (founds_rem e1 (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4) f1) True)))))) % 21.26/21.56 Clause #419 (by clausification #[418]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.26/21.56 Or (Eq (tgt f1 a) False) % 21.26/21.56 (Or (Eq (act f1 a_1) False) % 21.36/21.61 (Or (Eq (aer f1 a_2) False) % 21.36/21.61 (Or (Eq (aee f1 a_3) False) % 21.36/21.61 (Or (Eq (has_rem f1) False) (Eq (founds_rem e1 (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4) f1) True))))) % 21.36/21.61 Clause #420 (by forward demodulation #[419, 15]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.36/21.61 Or (Eq (tgt f1 a) False) % 21.36/21.61 (Or (Eq (act f1 a_1) False) % 21.36/21.61 (Or (Eq (aer f1 a_2) False) % 21.36/21.61 (Or (Eq (aee f1 a_3) False) % 21.36/21.61 (Or (Eq True False) (Eq (founds_rem e1 (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4) f1) True))))) % 21.36/21.61 Clause #421 (by clausification #[420]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.36/21.61 Or (Eq (tgt f1 a) False) % 21.36/21.61 (Or (Eq (act f1 a_1) False) % 21.36/21.61 (Or (Eq (aer f1 a_2) False) % 21.36/21.61 (Or (Eq (aee f1 a_3) False) (Eq (founds_rem e1 (skS.0 3 e1 f1 a_2 a_1 a a_3 a_4) f1) True)))) % 21.36/21.61 Clause #422 (by superposition #[421, 19]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.61 Or (Eq (act f1 a) False) % 21.36/21.61 (Or (Eq (aer f1 a_1) False) % 21.36/21.61 (Or (Eq (aee f1 a_2) False) % 21.36/21.61 (Or (Eq (founds_rem e1 (skS.0 3 e1 f1 a_1 a concert_ds a_2 a_3) f1) True) (Eq False True)))) % 21.36/21.61 Clause #423 (by clausification #[422]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.62 Or (Eq (act f1 a) False) % 21.36/21.62 (Or (Eq (aer f1 a_1) False) % 21.36/21.62 (Or (Eq (aee f1 a_2) False) (Eq (founds_rem e1 (skS.0 3 e1 f1 a_1 a concert_ds a_2 a_3) f1) True))) % 21.36/21.62 Clause #424 (by superposition #[423, 18]): ∀ (a a_1 a_2 : Iota), % 21.36/21.62 Or (Eq (aer f1 a) False) % 21.36/21.62 (Or (Eq (aee f1 a_1) False) % 21.36/21.62 (Or (Eq (founds_rem e1 (skS.0 3 e1 f1 a distrib concert_ds a_1 a_2) f1) True) (Eq False True))) % 21.36/21.62 Clause #425 (by clausification #[424]): ∀ (a a_1 a_2 : Iota), % 21.36/21.62 Or (Eq (aer f1 a) False) % 21.36/21.62 (Or (Eq (aee f1 a_1) False) (Eq (founds_rem e1 (skS.0 3 e1 f1 a distrib concert_ds a_1 a_2) f1) True)) % 21.36/21.62 Clause #426 (by superposition #[425, 17]): ∀ (a a_1 : Iota), % 21.36/21.62 Or (Eq (aee f1 a) False) % 21.36/21.62 (Or (Eq (founds_rem e1 (skS.0 3 e1 f1 philharmonie distrib concert_ds a a_1) f1) True) (Eq False True)) % 21.36/21.62 Clause #427 (by clausification #[426]): ∀ (a a_1 : Iota), % 21.36/21.62 Or (Eq (aee f1 a) False) (Eq (founds_rem e1 (skS.0 3 e1 f1 philharmonie distrib concert_ds a a_1) f1) True) % 21.36/21.62 Clause #428 (by superposition #[427, 16]): ∀ (a : Iota), % 21.36/21.62 Or (Eq (founds_rem e1 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a) f1) True) (Eq False True) % 21.36/21.62 Clause #429 (by clausification #[403]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.36/21.62 Or (Eq (tgt f1 a) False) % 21.36/21.62 (Or (Eq (act f1 a_1) False) % 21.36/21.62 (Or (Eq (aer f1 a_2) False) % 21.36/21.62 (Or (Eq (aee f1 a_3) False) % 21.36/21.62 (Or (Eq (proh f1) False) % 21.36/21.62 (Or (Eq (has_rem f1) False) (Eq (power (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5)) True)))))) % 21.36/21.62 Clause #430 (by forward demodulation #[429, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.36/21.62 Or (Eq (tgt f1 a) False) % 21.36/21.62 (Or (Eq (act f1 a_1) False) % 21.36/21.62 (Or (Eq (aer f1 a_2) False) % 21.36/21.62 (Or (Eq (aee f1 a_3) False) % 21.36/21.62 (Or (Eq True False) (Or (Eq (has_rem f1) False) (Eq (power (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5)) True)))))) % 21.36/21.62 Clause #431 (by clausification #[430]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.36/21.62 Or (Eq (tgt f1 a) False) % 21.36/21.62 (Or (Eq (act f1 a_1) False) % 21.36/21.62 (Or (Eq (aer f1 a_2) False) % 21.36/21.62 (Or (Eq (aee f1 a_3) False) % 21.36/21.62 (Or (Eq (has_rem f1) False) (Eq (power (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5)) True))))) % 21.36/21.62 Clause #432 (by forward demodulation #[431, 15]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.36/21.62 Or (Eq (tgt f1 a) False) % 21.36/21.62 (Or (Eq (act f1 a_1) False) % 21.36/21.62 (Or (Eq (aer f1 a_2) False) % 21.36/21.62 (Or (Eq (aee f1 a_3) False) (Or (Eq True False) (Eq (power (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5)) True))))) % 21.36/21.62 Clause #433 (by clausification #[432]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.36/21.62 Or (Eq (tgt f1 a) False) % 21.36/21.62 (Or (Eq (act f1 a_1) False) % 21.36/21.62 (Or (Eq (aer f1 a_2) False) (Or (Eq (aee f1 a_3) False) (Eq (power (skS.0 4 e1 f1 a_2 a_1 a a_3 a_4 a_5)) True)))) % 21.36/21.62 Clause #434 (by superposition #[433, 19]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.36/21.62 Or (Eq (act f1 a) False) % 21.36/21.62 (Or (Eq (aer f1 a_1) False) % 21.36/21.62 (Or (Eq (aee f1 a_2) False) (Or (Eq (power (skS.0 4 e1 f1 a_1 a concert_ds a_2 a_3 a_4)) True) (Eq False True)))) % 21.36/21.62 Clause #435 (by clausification #[428]): ∀ (a : Iota), Eq (founds_rem e1 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a) f1) True % 21.36/21.67 Clause #436 (by superposition #[435, 80]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (about_event a e1) True) % 21.36/21.67 (Or (Eq True False) % 21.36/21.67 (Or (Eq (part_of a (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_1)) False) % 21.36/21.67 (Or (Eq (subjection a) False) (Eq (cnt a (decl a_2) a_3) False)))) % 21.36/21.67 Clause #437 (by superposition #[435, 90]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (about_event a e1) True) % 21.36/21.67 (Or (Eq True False) % 21.36/21.67 (Or (Eq (part_of a (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_1)) False) % 21.36/21.67 (Or (Eq (power a) False) (Eq (cnt a (decl a_2) a_3) False)))) % 21.36/21.67 Clause #438 (by clausification #[434]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.36/21.67 Or (Eq (act f1 a) False) % 21.36/21.67 (Or (Eq (aer f1 a_1) False) % 21.36/21.67 (Or (Eq (aee f1 a_2) False) (Eq (power (skS.0 4 e1 f1 a_1 a concert_ds a_2 a_3 a_4)) True))) % 21.36/21.67 Clause #439 (by superposition #[438, 18]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (aer f1 a) False) % 21.36/21.67 (Or (Eq (aee f1 a_1) False) (Or (Eq (power (skS.0 4 e1 f1 a distrib concert_ds a_1 a_2 a_3)) True) (Eq False True))) % 21.36/21.67 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (aer f1 a) False) % 21.36/21.67 (Or (Eq (aee f1 a_1) False) (Eq (power (skS.0 4 e1 f1 a distrib concert_ds a_1 a_2 a_3)) True)) % 21.36/21.67 Clause #441 (by superposition #[440, 17]): ∀ (a a_1 a_2 : Iota), % 21.36/21.67 Or (Eq (aee f1 a) False) % 21.36/21.67 (Or (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds a a_1 a_2)) True) (Eq False True)) % 21.36/21.67 Clause #442 (by clausification #[441]): ∀ (a a_1 a_2 : Iota), % 21.36/21.67 Or (Eq (aee f1 a) False) (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds a a_1 a_2)) True) % 21.36/21.67 Clause #443 (by superposition #[442, 16]): ∀ (a a_1 : Iota), Or (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) True) (Eq False True) % 21.36/21.67 Clause #444 (by clausification #[443]): ∀ (a a_1 : Iota), Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) True % 21.36/21.67 Clause #445 (by clausification #[436]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (about_event a e1) True) % 21.36/21.67 (Or (Eq (part_of a (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_1)) False) % 21.36/21.67 (Or (Eq (subjection a) False) (Eq (cnt a (decl a_2) a_3) False))) % 21.36/21.67 Clause #446 (by superposition #[445, 214]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.36/21.67 Or (Eq (about_event (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) e1) True) % 21.36/21.67 (Or (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2)) False) % 21.36/21.67 (Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl a_3) a_4) False) % 21.36/21.67 (Eq False True))) % 21.36/21.67 Clause #448 (by clausification #[437]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (about_event a e1) True) % 21.36/21.67 (Or (Eq (part_of a (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_1)) False) % 21.36/21.67 (Or (Eq (power a) False) (Eq (cnt a (decl a_2) a_3) False))) % 21.36/21.67 Clause #450 (by superposition #[448, 326]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (about_event (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) e1) True) % 21.36/21.67 (Or (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) False) % 21.36/21.67 (Or (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) (decl a_2) a_3) False) % 21.36/21.67 (Eq False True))) % 21.36/21.67 Clause #452 (by clausification #[450]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (about_event (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) e1) True) % 21.36/21.67 (Or (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) False) % 21.36/21.67 (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) (decl a_2) a_3) False)) % 21.36/21.67 Clause #453 (by forward demodulation #[452, 444]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (about_event (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) e1) True) % 21.36/21.67 (Or (Eq True False) % 21.36/21.67 (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) (decl a_2) a_3) False)) % 21.36/21.67 Clause #454 (by clausification #[453]): ∀ (a a_1 a_2 a_3 : Iota), % 21.36/21.67 Or (Eq (about_event (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) e1) True) % 21.46/21.72 (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) (decl a_2) a_3) False) % 21.46/21.72 Clause #455 (by superposition #[454, 356]): ∀ (a a_1 : Iota), % 21.46/21.72 Or (Eq (about_event (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) e1) True) (Eq False True) % 21.46/21.72 Clause #456 (by clausification #[455]): ∀ (a a_1 : Iota), Eq (about_event (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) e1) True % 21.46/21.72 Clause #459 (by clausification #[446]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.72 Or (Eq (about_event (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) e1) True) % 21.46/21.72 (Or (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2)) False) % 21.46/21.72 (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl a_3) a_4) False)) % 21.46/21.72 Clause #460 (by forward demodulation #[459, 296]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.72 Or (Eq (about_event (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) e1) True) % 21.46/21.72 (Or (Eq True False) % 21.46/21.72 (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl a_3) a_4) False)) % 21.46/21.72 Clause #461 (by clausification #[460]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.72 Or (Eq (about_event (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) e1) True) % 21.46/21.72 (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl a_3) a_4) False) % 21.46/21.72 Clause #462 (by superposition #[461, 194]): ∀ (a a_1 a_2 : Iota), % 21.46/21.72 Or (Eq (about_event (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) e1) True) (Eq False True) % 21.46/21.72 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 : Iota), Eq (about_event (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) e1) True % 21.46/21.72 Clause #465 (by superposition #[463, 126]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.72 Or (Eq True False) % 21.46/21.72 (Or (Eq (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) a_3) False) % 21.46/21.72 (Or % 21.46/21.72 (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.72 (Or (Eq (bearer (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) marketplace) False) % 21.46/21.72 (Or (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2)) False) % 21.46/21.72 (Or (Eq (about_event a_4 e1) False) % 21.46/21.72 (Or (Eq (part_of a_4 a_3) False) % 21.46/21.72 (Or (Eq (cnt a_4 (decl distrib) concert_ds) False) % 21.46/21.72 (Or (Eq (bearer a_4 philharmonie) False) % 21.46/21.72 (Or (Eq (founds_rem e1 a_3 f1) False) (Eq (power a_4) False)))))))))) % 21.46/21.72 Clause #470 (by clausification #[465]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.72 Or (Eq (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) a_3) False) % 21.46/21.72 (Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.72 (Or (Eq (bearer (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) marketplace) False) % 21.46/21.72 (Or (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2)) False) % 21.46/21.72 (Or (Eq (about_event a_4 e1) False) % 21.46/21.72 (Or (Eq (part_of a_4 a_3) False) % 21.46/21.72 (Or (Eq (cnt a_4 (decl distrib) concert_ds) False) % 21.46/21.72 (Or (Eq (bearer a_4 philharmonie) False) % 21.46/21.72 (Or (Eq (founds_rem e1 a_3 f1) False) (Eq (power a_4) False))))))))) % 21.46/21.72 Clause #471 (by forward demodulation #[470, 260]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.72 Or (Eq (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) a_3) False) % 21.46/21.72 (Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.72 (Or (Eq True False) % 21.46/21.72 (Or (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2)) False) % 21.46/21.72 (Or (Eq (about_event a_4 e1) False) % 21.46/21.72 (Or (Eq (part_of a_4 a_3) False) % 21.46/21.72 (Or (Eq (cnt a_4 (decl distrib) concert_ds) False) % 21.46/21.72 (Or (Eq (bearer a_4 philharmonie) False) % 21.46/21.76 (Or (Eq (founds_rem e1 a_3 f1) False) (Eq (power a_4) False))))))))) % 21.46/21.76 Clause #472 (by clausification #[471]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.76 Or (Eq (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) a_3) False) % 21.46/21.76 (Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (subjection (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2)) False) % 21.46/21.76 (Or (Eq (about_event a_4 e1) False) % 21.46/21.76 (Or (Eq (part_of a_4 a_3) False) % 21.46/21.76 (Or (Eq (cnt a_4 (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (bearer a_4 philharmonie) False) % 21.46/21.76 (Or (Eq (founds_rem e1 a_3 f1) False) (Eq (power a_4) False)))))))) % 21.46/21.76 Clause #473 (by forward demodulation #[472, 296]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.76 Or (Eq (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) a_3) False) % 21.46/21.76 (Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq True False) % 21.46/21.76 (Or (Eq (about_event a_4 e1) False) % 21.46/21.76 (Or (Eq (part_of a_4 a_3) False) % 21.46/21.76 (Or (Eq (cnt a_4 (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (bearer a_4 philharmonie) False) % 21.46/21.76 (Or (Eq (founds_rem e1 a_3 f1) False) (Eq (power a_4) False)))))))) % 21.46/21.76 Clause #474 (by clausification #[473]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.46/21.76 Or (Eq (part_of (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) a_3) False) % 21.46/21.76 (Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (about_event a_4 e1) False) % 21.46/21.76 (Or (Eq (part_of a_4 a_3) False) % 21.46/21.76 (Or (Eq (cnt a_4 (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (bearer a_4 philharmonie) False) (Or (Eq (founds_rem e1 a_3 f1) False) (Eq (power a_4) False))))))) % 21.46/21.76 Clause #475 (by superposition #[474, 214]): ∀ (a a_1 a_2 a_3 : Iota), % 21.46/21.76 Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (about_event a_3 e1) False) % 21.46/21.76 (Or (Eq (part_of a_3 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a)) False) % 21.46/21.76 (Or (Eq (cnt a_3 (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (bearer a_3 philharmonie) False) % 21.46/21.76 (Or (Eq (founds_rem e1 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a) f1) False) % 21.46/21.76 (Or (Eq (power a_3) False) (Eq False True))))))) % 21.46/21.76 Clause #481 (by clausification #[475]): ∀ (a a_1 a_2 a_3 : Iota), % 21.46/21.76 Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (about_event a_3 e1) False) % 21.46/21.76 (Or (Eq (part_of a_3 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a)) False) % 21.46/21.76 (Or (Eq (cnt a_3 (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (bearer a_3 philharmonie) False) % 21.46/21.76 (Or (Eq (founds_rem e1 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a) f1) False) % 21.46/21.76 (Eq (power a_3) False)))))) % 21.46/21.76 Clause #482 (by forward demodulation #[481, 435]): ∀ (a a_1 a_2 a_3 : Iota), % 21.46/21.76 Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (about_event a_3 e1) False) % 21.46/21.76 (Or (Eq (part_of a_3 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a)) False) % 21.46/21.76 (Or (Eq (cnt a_3 (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (bearer a_3 philharmonie) False) (Or (Eq True False) (Eq (power a_3) False)))))) % 21.46/21.76 Clause #483 (by clausification #[482]): ∀ (a a_1 a_2 a_3 : Iota), % 21.46/21.76 Or (Eq (cnt (skS.0 5 e1 f1 philharmonie distrib concert_ds marketplace a a_1 a_2) (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (about_event a_3 e1) False) % 21.46/21.76 (Or (Eq (part_of a_3 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a)) False) % 21.46/21.76 (Or (Eq (cnt a_3 (decl distrib) concert_ds) False) % 21.46/21.76 (Or (Eq (bearer a_3 philharmonie) False) (Eq (power a_3) False))))) % 21.56/21.81 Clause #484 (by superposition #[483, 194]): ∀ (a a_1 : Iota), % 21.56/21.81 Or (Eq (about_event a e1) False) % 21.56/21.81 (Or (Eq (part_of a (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_1)) False) % 21.56/21.81 (Or (Eq (cnt a (decl distrib) concert_ds) False) % 21.56/21.81 (Or (Eq (bearer a philharmonie) False) (Or (Eq (power a) False) (Eq False True))))) % 21.56/21.81 Clause #485 (by clausification #[484]): ∀ (a a_1 : Iota), % 21.56/21.81 Or (Eq (about_event a e1) False) % 21.56/21.81 (Or (Eq (part_of a (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_1)) False) % 21.56/21.81 (Or (Eq (cnt a (decl distrib) concert_ds) False) (Or (Eq (bearer a philharmonie) False) (Eq (power a) False)))) % 21.56/21.81 Clause #486 (by superposition #[485, 456]): ∀ (a a_1 a_2 : Iota), % 21.56/21.81 Or % 21.56/21.81 (Eq % 21.56/21.81 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.56/21.81 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_2)) % 21.56/21.81 False) % 21.56/21.81 (Or (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) (decl distrib) concert_ds) False) % 21.56/21.81 (Or (Eq (bearer (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) philharmonie) False) % 21.56/21.81 (Or (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) False) (Eq False True)))) % 21.56/21.81 Clause #488 (by clausification #[486]): ∀ (a a_1 a_2 : Iota), % 21.56/21.81 Or % 21.56/21.81 (Eq % 21.56/21.81 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.56/21.81 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_2)) % 21.56/21.81 False) % 21.56/21.81 (Or (Eq (cnt (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) (decl distrib) concert_ds) False) % 21.56/21.81 (Or (Eq (bearer (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) philharmonie) False) % 21.56/21.81 (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) False))) % 21.56/21.81 Clause #489 (by forward demodulation #[488, 356]): ∀ (a a_1 a_2 : Iota), % 21.56/21.81 Or % 21.56/21.81 (Eq % 21.56/21.81 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.56/21.81 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_2)) % 21.56/21.81 False) % 21.56/21.81 (Or (Eq True False) % 21.56/21.81 (Or (Eq (bearer (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) philharmonie) False) % 21.56/21.81 (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) False))) % 21.56/21.81 Clause #490 (by clausification #[489]): ∀ (a a_1 a_2 : Iota), % 21.56/21.81 Or % 21.56/21.81 (Eq % 21.56/21.81 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.56/21.81 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_2)) % 21.56/21.81 False) % 21.56/21.81 (Or (Eq (bearer (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) philharmonie) False) % 21.56/21.81 (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) False)) % 21.56/21.81 Clause #491 (by forward demodulation #[490, 386]): ∀ (a a_1 a_2 : Iota), % 21.56/21.81 Or % 21.56/21.81 (Eq % 21.56/21.81 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.56/21.81 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_2)) % 21.56/21.81 False) % 21.56/21.81 (Or (Eq True False) (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) False)) % 21.56/21.81 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 : Iota), % 21.56/21.81 Or % 21.56/21.81 (Eq % 21.56/21.81 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.56/21.81 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_2)) % 21.56/21.81 False) % 21.56/21.81 (Eq (power (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1)) False) % 21.56/21.81 Clause #493 (by forward demodulation #[492, 444]): ∀ (a a_1 a_2 : Iota), % 21.56/21.81 Or % 21.56/21.81 (Eq % 21.56/21.81 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.56/21.81 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_2)) % 21.56/21.81 False) % 21.56/21.81 (Eq True False) % 21.56/21.81 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 : Iota), % 21.56/21.81 Eq % 21.56/21.81 (part_of (skS.0 4 e1 f1 philharmonie distrib concert_ds marketplace a a_1) % 21.56/21.81 (skS.0 3 e1 f1 philharmonie distrib concert_ds marketplace a_2)) % 21.56/21.81 False % 21.56/21.81 Clause #495 (by superposition #[494, 326]): Eq False True % 21.56/21.81 Clause #496 (by clausification #[495]): False % 21.56/21.81 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------