%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.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 31.96s 32.22s % Output : Proof 33.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.05 % Command : duper %s % 0.13/0.38 % Computer : n009.cluster.edu % 0.13/0.38 % Model : x86_64 x86_64 % 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.38 % Memory : 8046.5625MB % 0.13/0.38 % OS : Linux 6.8.0-71-generic % 0.13/0.39 % CPULimit : 300 % 0.13/0.39 % WCLimit : 300 % 0.13/0.39 % DateTime : Mon Sep 7 14:05:52 UTC 2026 % 0.13/0.39 % CPUTime : % 31.96/32.22 SZS status Theorem for theBenchmark.p % 31.96/32.22 SZS output start Proof for theBenchmark.p % 31.96/32.22 Clause #0 (by assumption #[]): Eq (agent portal) True % 31.96/32.22 Clause #2 (by assumption #[]): Eq (action modify_act) True % 31.96/32.22 Clause #3 (by assumption #[]): Eq (target theater_ds) True % 31.96/32.22 Clause #4 (by assumption #[]): Eq (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F portal)) (act F modify_act)) (activates E F))) % 31.96/32.22 True % 31.96/32.22 Clause #5 (by assumption #[]): Eq % 31.96/32.22 (∀ (X A T : Iota), % 31.96/32.22 And (And (And (agent X) (action A)) (target T)) % 31.96/32.22 (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F X)) (act F A)) (activates E F))) → % 31.96/32.22 Exists fun L => And (And (permission L) (bearer L X)) (cnt L A T)) % 31.96/32.22 True % 31.96/32.22 Clause #6 (by assumption #[]): Eq (Not (Exists fun L => And (And (permission L) (bearer L portal)) (cnt L modify_act theater_ds))) True % 31.96/32.22 Clause #7 (by clausification #[6]): Eq (Exists fun L => And (And (permission L) (bearer L portal)) (cnt L modify_act theater_ds)) False % 31.96/32.22 Clause #8 (by clausification #[7]): ∀ (a : Iota), Eq (And (And (permission a) (bearer a portal)) (cnt a modify_act theater_ds)) False % 31.96/32.22 Clause #9 (by clausification #[8]): ∀ (a : Iota), Or (Eq (And (permission a) (bearer a portal)) False) (Eq (cnt a modify_act theater_ds) False) % 31.96/32.22 Clause #10 (by clausification #[9]): ∀ (a : Iota), Or (Eq (cnt a modify_act theater_ds) False) (Or (Eq (permission a) False) (Eq (bearer a portal) False)) % 31.96/32.22 Clause #11 (by clausification #[4]): Eq (Exists fun F => Exists fun E => And (And (And (proh F) (aee F portal)) (act F modify_act)) (activates E F)) False % 31.96/32.22 Clause #12 (by clausification #[11]): ∀ (a : Iota), Eq (Exists fun E => And (And (And (proh a) (aee a portal)) (act a modify_act)) (activates E a)) False % 31.96/32.22 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), Eq (And (And (And (proh a) (aee a portal)) (act a modify_act)) (activates a_1 a)) False % 31.96/32.22 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), Or (Eq (And (And (proh a) (aee a portal)) (act a modify_act)) False) (Eq (activates a_1 a) False) % 31.96/32.22 Clause #15 (by clausification #[14]): ∀ (a a_1 : Iota), % 31.96/32.22 Or (Eq (activates a a_1) False) (Or (Eq (And (proh a_1) (aee a_1 portal)) False) (Eq (act a_1 modify_act) False)) % 31.96/32.22 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), % 31.96/32.22 Or (Eq (activates a a_1) False) % 31.96/32.22 (Or (Eq (act a_1 modify_act) False) (Or (Eq (proh a_1) False) (Eq (aee a_1 portal) False))) % 31.96/32.22 Clause #17 (by clausification #[5]): ∀ (a : Iota), % 31.96/32.22 Eq % 31.96/32.22 (∀ (A T : Iota), % 31.96/32.22 And (And (And (agent a) (action A)) (target T)) % 31.96/32.22 (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F A)) (activates E F))) → % 31.96/32.22 Exists fun L => And (And (permission L) (bearer L a)) (cnt L A T)) % 31.96/32.22 True % 31.96/32.22 Clause #18 (by clausification #[17]): ∀ (a a_1 : Iota), % 31.96/32.22 Eq % 31.96/32.22 (∀ (T : Iota), % 31.96/32.22 And (And (And (agent a) (action a_1)) (target T)) % 31.96/32.22 (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F))) → % 31.96/32.22 Exists fun L => And (And (permission L) (bearer L a)) (cnt L a_1 T)) % 31.96/32.22 True % 31.96/32.22 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 : Iota), % 31.96/32.22 Eq % 31.96/32.22 (And (And (And (agent a) (action a_1)) (target a_2)) % 31.96/32.22 (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F))) → % 31.96/32.22 Exists fun L => And (And (permission L) (bearer L a)) (cnt L a_1 a_2)) % 31.96/32.22 True % 31.96/32.22 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 : Iota), % 31.96/32.22 Or % 31.96/32.22 (Eq % 31.96/32.22 (And (And (And (agent a) (action a_1)) (target a_2)) % 31.96/32.22 (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F)))) % 31.96/32.22 False) % 31.96/32.22 (Eq (Exists fun L => And (And (permission L) (bearer L a)) (cnt L a_1 a_2)) True) % 31.96/32.22 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 : Iota), % 31.96/32.22 Or (Eq (Exists fun L => And (And (permission L) (bearer L a)) (cnt L a_1 a_2)) True) % 31.96/32.22 (Or (Eq (And (And (agent a) (action a_1)) (target a_2)) False) % 31.96/32.22 (Eq (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F))) False)) % 31.96/32.22 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 : Iota), % 31.96/32.27 Or (Eq (And (And (agent a) (action a_1)) (target a_2)) False) % 31.96/32.27 (Or % 31.96/32.27 (Eq (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F))) False) % 31.96/32.27 (Eq % 31.96/32.27 (And (And (permission (skS.0 0 a a_1 a_2 a_3)) (bearer (skS.0 0 a a_1 a_2 a_3) a)) % 31.96/32.27 (cnt (skS.0 0 a a_1 a_2 a_3) a_1 a_2)) % 31.96/32.27 True)) % 31.96/32.27 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 : Iota), % 31.96/32.27 Or (Eq (Not (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F))) False) % 31.96/32.27 (Or % 31.96/32.27 (Eq % 31.96/32.27 (And (And (permission (skS.0 0 a a_1 a_2 a_3)) (bearer (skS.0 0 a a_1 a_2 a_3) a)) % 31.96/32.27 (cnt (skS.0 0 a a_1 a_2 a_3) a_1 a_2)) % 31.96/32.27 True) % 31.96/32.27 (Or (Eq (And (agent a) (action a_1)) False) (Eq (target a_2) False))) % 31.96/32.27 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 a_3 : Iota), % 31.96/32.27 Or % 31.96/32.27 (Eq % 31.96/32.27 (And (And (permission (skS.0 0 a a_1 a_2 a_3)) (bearer (skS.0 0 a a_1 a_2 a_3) a)) % 31.96/32.27 (cnt (skS.0 0 a a_1 a_2 a_3) a_1 a_2)) % 31.96/32.27 True) % 31.96/32.27 (Or (Eq (And (agent a) (action a_1)) False) % 31.96/32.27 (Or (Eq (target a_2) False) % 31.96/32.27 (Eq (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F)) True))) % 31.96/32.27 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 a_3 : Iota), % 31.96/32.27 Or (Eq (And (agent a) (action a_1)) False) % 31.96/32.27 (Or (Eq (target a_2) False) % 31.96/32.27 (Or (Eq (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F)) True) % 31.96/32.27 (Eq (cnt (skS.0 0 a a_1 a_2 a_3) a_1 a_2) True))) % 31.96/32.27 Clause #26 (by clausification #[24]): ∀ (a a_1 a_2 a_3 : Iota), % 31.96/32.27 Or (Eq (And (agent a) (action a_1)) False) % 31.96/32.27 (Or (Eq (target a_2) False) % 31.96/32.27 (Or (Eq (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a)) (act F a_1)) (activates E F)) True) % 31.96/32.27 (Eq (And (permission (skS.0 0 a a_1 a_2 a_3)) (bearer (skS.0 0 a a_1 a_2 a_3) a)) True))) % 31.96/32.27 Clause #27 (by clausification #[25]): ∀ (a a_1 a_2 a_3 : Iota), % 31.96/32.27 Or (Eq (target a) False) % 31.96/32.27 (Or (Eq (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a_1)) (act F a_2)) (activates E F)) True) % 31.96/32.27 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) (Or (Eq (agent a_1) False) (Eq (action a_2) False)))) % 31.96/32.27 Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.96/32.27 Or (Eq (target a) False) % 31.96/32.27 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) % 31.96/32.27 (Or (Eq (agent a_1) False) % 31.96/32.27 (Or (Eq (action a_2) False) % 31.96/32.27 (Eq % 31.96/32.27 (Exists fun E => % 31.96/32.27 And % 31.96/32.27 (And (And (proh (skS.0 1 a_1 a_2 a_4)) (aee (skS.0 1 a_1 a_2 a_4) a_1)) (act (skS.0 1 a_1 a_2 a_4) a_2)) % 31.96/32.27 (activates E (skS.0 1 a_1 a_2 a_4))) % 31.96/32.27 True)))) % 31.96/32.27 Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 31.96/32.27 Or (Eq (target a) False) % 31.96/32.27 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) % 31.96/32.27 (Or (Eq (agent a_1) False) % 31.96/32.27 (Or (Eq (action a_2) False) % 31.96/32.27 (Eq % 31.96/32.27 (And % 31.96/32.27 (And (And (proh (skS.0 1 a_1 a_2 a_4)) (aee (skS.0 1 a_1 a_2 a_4) a_1)) (act (skS.0 1 a_1 a_2 a_4) a_2)) % 31.96/32.27 (activates (skS.0 2 a_1 a_2 a_4 a_5) (skS.0 1 a_1 a_2 a_4))) % 31.96/32.27 True)))) % 31.96/32.27 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 31.96/32.27 Or (Eq (target a) False) % 31.96/32.27 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) % 31.96/32.27 (Or (Eq (agent a_1) False) % 31.96/32.27 (Or (Eq (action a_2) False) (Eq (activates (skS.0 2 a_1 a_2 a_4 a_5) (skS.0 1 a_1 a_2 a_4)) True)))) % 31.96/32.27 Clause #31 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.96/32.27 Or (Eq (target a) False) % 31.96/32.27 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) % 31.96/32.27 (Or (Eq (agent a_1) False) % 31.96/32.27 (Or (Eq (action a_2) False) % 31.96/32.27 (Eq (And (And (proh (skS.0 1 a_1 a_2 a_4)) (aee (skS.0 1 a_1 a_2 a_4) a_1)) (act (skS.0 1 a_1 a_2 a_4) a_2)) % 31.96/32.27 True)))) % 31.96/32.27 Clause #32 (by superposition #[30, 3]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 31.96/32.27 Or (Eq (cnt (skS.0 0 a a_1 theater_ds a_2) a_1 theater_ds) True) % 31.96/32.27 (Or (Eq (agent a) False) % 31.96/32.27 (Or (Eq (action a_1) False) % 31.96/32.27 (Or (Eq (activates (skS.0 2 a a_1 a_3 a_4) (skS.0 1 a a_1 a_3)) True) (Eq False True)))) % 32.06/32.33 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.33 Or (Eq (cnt (skS.0 0 a a_1 theater_ds a_2) a_1 theater_ds) True) % 32.06/32.33 (Or (Eq (agent a) False) % 32.06/32.33 (Or (Eq (action a_1) False) (Eq (activates (skS.0 2 a a_1 a_3 a_4) (skS.0 1 a a_1 a_3)) True))) % 32.06/32.33 Clause #35 (by superposition #[33, 0]): ∀ (a a_1 a_2 a_3 : Iota), % 32.06/32.33 Or (Eq (cnt (skS.0 0 portal a theater_ds a_1) a theater_ds) True) % 32.06/32.33 (Or (Eq (action a) False) % 32.06/32.33 (Or (Eq (activates (skS.0 2 portal a a_2 a_3) (skS.0 1 portal a a_2)) True) (Eq False True))) % 32.06/32.33 Clause #36 (by clausification #[35]): ∀ (a a_1 a_2 a_3 : Iota), % 32.06/32.33 Or (Eq (cnt (skS.0 0 portal a theater_ds a_1) a theater_ds) True) % 32.06/32.33 (Or (Eq (action a) False) (Eq (activates (skS.0 2 portal a a_2 a_3) (skS.0 1 portal a a_2)) True)) % 32.06/32.33 Clause #37 (by superposition #[36, 2]): ∀ (a a_1 a_2 : Iota), % 32.06/32.33 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.06/32.33 (Or (Eq (activates (skS.0 2 portal modify_act a_1 a_2) (skS.0 1 portal modify_act a_1)) True) (Eq False True)) % 32.06/32.33 Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 : Iota), % 32.06/32.33 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.06/32.33 (Eq (activates (skS.0 2 portal modify_act a_1 a_2) (skS.0 1 portal modify_act a_1)) True) % 32.06/32.33 Clause #39 (by superposition #[38, 10]): ∀ (a a_1 a_2 : Iota), % 32.06/32.33 Or (Eq (activates (skS.0 2 portal modify_act a a_1) (skS.0 1 portal modify_act a)) True) % 32.06/32.33 (Or (Eq True False) % 32.06/32.33 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_2)) False) % 32.06/32.33 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.06/32.33 Clause #40 (by superposition #[38, 16]): ∀ (a a_1 : Iota), % 32.06/32.33 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.06/32.33 (Or (Eq True False) % 32.06/32.33 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) False) % 32.06/32.33 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) False) (Eq (aee (skS.0 1 portal modify_act a_1) portal) False)))) % 32.06/32.33 Clause #43 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : Iota), % 32.06/32.33 Or (Eq (target a) False) % 32.06/32.33 (Or (Eq (Exists fun F => Exists fun E => And (And (And (proh F) (aee F a_1)) (act F a_2)) (activates E F)) True) % 32.06/32.33 (Or (Eq (And (permission (skS.0 0 a_1 a_2 a a_3)) (bearer (skS.0 0 a_1 a_2 a a_3) a_1)) True) % 32.06/32.33 (Or (Eq (agent a_1) False) (Eq (action a_2) False)))) % 32.06/32.33 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.33 Or (Eq (target a) False) % 32.06/32.33 (Or (Eq (And (permission (skS.0 0 a_1 a_2 a a_3)) (bearer (skS.0 0 a_1 a_2 a a_3) a_1)) True) % 32.06/32.33 (Or (Eq (agent a_1) False) % 32.06/32.33 (Or (Eq (action a_2) False) % 32.06/32.33 (Eq % 32.06/32.33 (Exists fun E => % 32.06/32.33 And % 32.06/32.33 (And (And (proh (skS.0 3 a_1 a_2 a_4)) (aee (skS.0 3 a_1 a_2 a_4) a_1)) (act (skS.0 3 a_1 a_2 a_4) a_2)) % 32.06/32.33 (activates E (skS.0 3 a_1 a_2 a_4))) % 32.06/32.33 True)))) % 32.06/32.33 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.33 Or (Eq (target a) False) % 32.06/32.33 (Or (Eq (agent a_1) False) % 32.06/32.33 (Or (Eq (action a_2) False) % 32.06/32.33 (Or % 32.06/32.33 (Eq % 32.06/32.33 (Exists fun E => % 32.06/32.33 And % 32.06/32.33 (And (And (proh (skS.0 3 a_1 a_2 a_3)) (aee (skS.0 3 a_1 a_2 a_3) a_1)) (act (skS.0 3 a_1 a_2 a_3) a_2)) % 32.06/32.33 (activates E (skS.0 3 a_1 a_2 a_3))) % 32.06/32.33 True) % 32.06/32.33 (Eq (bearer (skS.0 0 a_1 a_2 a a_4) a_1) True)))) % 32.06/32.33 Clause #46 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.33 Or (Eq (target a) False) % 32.06/32.33 (Or (Eq (agent a_1) False) % 32.06/32.33 (Or (Eq (action a_2) False) % 32.06/32.33 (Or % 32.06/32.33 (Eq % 32.06/32.33 (Exists fun E => % 32.06/32.33 And % 32.06/32.33 (And (And (proh (skS.0 3 a_1 a_2 a_3)) (aee (skS.0 3 a_1 a_2 a_3) a_1)) (act (skS.0 3 a_1 a_2 a_3) a_2)) % 32.06/32.33 (activates E (skS.0 3 a_1 a_2 a_3))) % 32.06/32.33 True) % 32.06/32.33 (Eq (permission (skS.0 0 a_1 a_2 a a_4)) True)))) % 32.06/32.33 Clause #47 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 32.06/32.33 Or (Eq (target a) False) % 32.06/32.33 (Or (Eq (agent a_1) False) % 32.06/32.33 (Or (Eq (action a_2) False) % 32.06/32.33 (Or (Eq (bearer (skS.0 0 a_1 a_2 a a_3) a_1) True) % 32.06/32.39 (Eq % 32.06/32.39 (And % 32.06/32.39 (And (And (proh (skS.0 3 a_1 a_2 a_4)) (aee (skS.0 3 a_1 a_2 a_4) a_1)) (act (skS.0 3 a_1 a_2 a_4) a_2)) % 32.06/32.39 (activates (skS.0 4 a_1 a_2 a_4 a_5) (skS.0 3 a_1 a_2 a_4))) % 32.06/32.39 True)))) % 32.06/32.39 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 32.06/32.39 Or (Eq (target a) False) % 32.06/32.39 (Or (Eq (agent a_1) False) % 32.06/32.39 (Or (Eq (action a_2) False) % 32.06/32.39 (Or (Eq (bearer (skS.0 0 a_1 a_2 a a_3) a_1) True) % 32.06/32.39 (Eq (activates (skS.0 4 a_1 a_2 a_4 a_5) (skS.0 3 a_1 a_2 a_4)) True)))) % 32.06/32.39 Clause #49 (by clausification #[47]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.39 Or (Eq (target a) False) % 32.06/32.39 (Or (Eq (agent a_1) False) % 32.06/32.39 (Or (Eq (action a_2) False) % 32.06/32.39 (Or (Eq (bearer (skS.0 0 a_1 a_2 a a_3) a_1) True) % 32.06/32.39 (Eq (And (And (proh (skS.0 3 a_1 a_2 a_4)) (aee (skS.0 3 a_1 a_2 a_4) a_1)) (act (skS.0 3 a_1 a_2 a_4) a_2)) % 32.06/32.39 True)))) % 32.06/32.39 Clause #50 (by superposition #[48, 3]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.39 Or (Eq (agent a) False) % 32.06/32.39 (Or (Eq (action a_1) False) % 32.06/32.39 (Or (Eq (bearer (skS.0 0 a a_1 theater_ds a_2) a) True) % 32.06/32.39 (Or (Eq (activates (skS.0 4 a a_1 a_3 a_4) (skS.0 3 a a_1 a_3)) True) (Eq False True)))) % 32.06/32.39 Clause #54 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.39 Or (Eq (agent a) False) % 32.06/32.39 (Or (Eq (action a_1) False) % 32.06/32.39 (Or (Eq (bearer (skS.0 0 a a_1 theater_ds a_2) a) True) % 32.06/32.39 (Eq (activates (skS.0 4 a a_1 a_3 a_4) (skS.0 3 a a_1 a_3)) True))) % 32.06/32.39 Clause #56 (by superposition #[54, 0]): ∀ (a a_1 a_2 a_3 : Iota), % 32.06/32.39 Or (Eq (action a) False) % 32.06/32.39 (Or (Eq (bearer (skS.0 0 portal a theater_ds a_1) portal) True) % 32.06/32.39 (Or (Eq (activates (skS.0 4 portal a a_2 a_3) (skS.0 3 portal a a_2)) True) (Eq False True))) % 32.06/32.39 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 : Iota), % 32.06/32.39 Or (Eq (action a) False) % 32.06/32.39 (Or (Eq (bearer (skS.0 0 portal a theater_ds a_1) portal) True) % 32.06/32.39 (Eq (activates (skS.0 4 portal a a_2 a_3) (skS.0 3 portal a a_2)) True)) % 32.06/32.39 Clause #58 (by superposition #[57, 2]): ∀ (a a_1 a_2 : Iota), % 32.06/32.39 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.06/32.39 (Or (Eq (activates (skS.0 4 portal modify_act a_1 a_2) (skS.0 3 portal modify_act a_1)) True) (Eq False True)) % 32.06/32.39 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 : Iota), % 32.06/32.39 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.06/32.39 (Eq (activates (skS.0 4 portal modify_act a_1 a_2) (skS.0 3 portal modify_act a_1)) True) % 32.06/32.39 Clause #60 (by superposition #[59, 16]): ∀ (a a_1 : Iota), % 32.06/32.39 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.06/32.39 (Or (Eq True False) % 32.06/32.39 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 32.06/32.39 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) False) (Eq (aee (skS.0 3 portal modify_act a_1) portal) False)))) % 32.06/32.39 Clause #63 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.39 Or (Eq (target a) False) % 32.06/32.39 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) % 32.06/32.39 (Or (Eq (agent a_1) False) (Or (Eq (action a_2) False) (Eq (act (skS.0 1 a_1 a_2 a_4) a_2) True)))) % 32.06/32.39 Clause #64 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.06/32.39 Or (Eq (target a) False) % 32.06/32.39 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) % 32.06/32.39 (Or (Eq (agent a_1) False) % 32.06/32.39 (Or (Eq (action a_2) False) (Eq (And (proh (skS.0 1 a_1 a_2 a_4)) (aee (skS.0 1 a_1 a_2 a_4) a_1)) True)))) % 32.06/32.39 Clause #65 (by superposition #[63, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.06/32.39 Or (Eq (cnt (skS.0 0 a a_1 theater_ds a_2) a_1 theater_ds) True) % 32.06/32.39 (Or (Eq (agent a) False) (Or (Eq (action a_1) False) (Or (Eq (act (skS.0 1 a a_1 a_3) a_1) True) (Eq False True)))) % 32.06/32.39 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 a_3 : Iota), % 32.06/32.39 Or (Eq (cnt (skS.0 0 a a_1 theater_ds a_2) a_1 theater_ds) True) % 32.06/32.39 (Or (Eq (agent a) False) (Or (Eq (action a_1) False) (Eq (act (skS.0 1 a a_1 a_3) a_1) True))) % 32.06/32.39 Clause #68 (by superposition #[66, 0]): ∀ (a a_1 a_2 : Iota), % 32.06/32.39 Or (Eq (cnt (skS.0 0 portal a theater_ds a_1) a theater_ds) True) % 32.06/32.39 (Or (Eq (action a) False) (Or (Eq (act (skS.0 1 portal a a_2) a) True) (Eq False True))) % 32.16/32.45 Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 portal a theater_ds a_1) a theater_ds) True) % 32.16/32.45 (Or (Eq (action a) False) (Eq (act (skS.0 1 portal a a_2) a) True)) % 32.16/32.45 Clause #70 (by superposition #[69, 2]): ∀ (a a_1 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.16/32.45 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) (Eq False True)) % 32.16/32.45 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.16/32.45 (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.16/32.45 Clause #72 (by superposition #[71, 10]): ∀ (a a_1 : Iota), % 32.16/32.45 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.16/32.45 (Or (Eq True False) % 32.16/32.45 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_1)) False) % 32.16/32.45 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_1) portal) False))) % 32.16/32.45 Clause #77 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 32.16/32.45 Or (Eq (activates (skS.0 2 portal modify_act a a_1) (skS.0 1 portal modify_act a)) True) % 32.16/32.45 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_2)) False) % 32.16/32.45 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.16/32.45 Clause #80 (by clausification #[72]): ∀ (a a_1 : Iota), % 32.16/32.45 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.16/32.45 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_1)) False) % 32.16/32.45 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_1) portal) False)) % 32.16/32.45 Clause #82 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.16/32.45 Or (Eq (target a) False) % 32.16/32.45 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) % 32.16/32.45 (Or (Eq (agent a_1) False) (Or (Eq (action a_2) False) (Eq (aee (skS.0 1 a_1 a_2 a_4) a_1) True)))) % 32.16/32.45 Clause #83 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.16/32.45 Or (Eq (target a) False) % 32.16/32.45 (Or (Eq (cnt (skS.0 0 a_1 a_2 a a_3) a_2 a) True) % 32.16/32.45 (Or (Eq (agent a_1) False) (Or (Eq (action a_2) False) (Eq (proh (skS.0 1 a_1 a_2 a_4)) True)))) % 32.16/32.45 Clause #84 (by superposition #[82, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 a a_1 theater_ds a_2) a_1 theater_ds) True) % 32.16/32.45 (Or (Eq (agent a) False) (Or (Eq (action a_1) False) (Or (Eq (aee (skS.0 1 a a_1 a_3) a) True) (Eq False True)))) % 32.16/32.45 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 a a_1 theater_ds a_2) a_1 theater_ds) True) % 32.16/32.45 (Or (Eq (agent a) False) (Or (Eq (action a_1) False) (Eq (aee (skS.0 1 a a_1 a_3) a) True))) % 32.16/32.45 Clause #87 (by superposition #[85, 0]): ∀ (a a_1 a_2 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 portal a theater_ds a_1) a theater_ds) True) % 32.16/32.45 (Or (Eq (action a) False) (Or (Eq (aee (skS.0 1 portal a a_2) portal) True) (Eq False True))) % 32.16/32.45 Clause #88 (by clausification #[40]): ∀ (a a_1 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.16/32.45 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) False) % 32.16/32.45 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) False) (Eq (aee (skS.0 1 portal modify_act a_1) portal) False))) % 32.16/32.45 Clause #90 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 portal a theater_ds a_1) a theater_ds) True) % 32.16/32.45 (Or (Eq (action a) False) (Eq (aee (skS.0 1 portal a a_2) portal) True)) % 32.16/32.45 Clause #91 (by superposition #[90, 2]): ∀ (a a_1 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.16/32.45 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq False True)) % 32.16/32.45 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.16/32.45 (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.16/32.45 Clause #93 (by superposition #[92, 10]): ∀ (a a_1 : Iota), % 32.16/32.45 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.16/32.45 (Or (Eq True False) % 32.16/32.45 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_1)) False) % 32.16/32.45 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_1) portal) False))) % 32.16/32.45 Clause #98 (by superposition #[83, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.16/32.45 Or (Eq (cnt (skS.0 0 a a_1 theater_ds a_2) a_1 theater_ds) True) % 32.26/32.51 (Or (Eq (agent a) False) (Or (Eq (action a_1) False) (Or (Eq (proh (skS.0 1 a a_1 a_3)) True) (Eq False True)))) % 32.26/32.51 Clause #99 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 32.26/32.51 Or (Eq (target a) False) % 32.26/32.51 (Or (Eq (agent a_1) False) % 32.26/32.51 (Or (Eq (action a_2) False) % 32.26/32.51 (Or (Eq (permission (skS.0 0 a_1 a_2 a a_3)) True) % 32.26/32.51 (Eq % 32.26/32.51 (And % 32.26/32.51 (And (And (proh (skS.0 3 a_1 a_2 a_4)) (aee (skS.0 3 a_1 a_2 a_4) a_1)) (act (skS.0 3 a_1 a_2 a_4) a_2)) % 32.26/32.51 (activates (skS.0 5 a_1 a_2 a_4 a_5) (skS.0 3 a_1 a_2 a_4))) % 32.26/32.51 True)))) % 32.26/32.51 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 32.26/32.51 Or (Eq (target a) False) % 32.26/32.51 (Or (Eq (agent a_1) False) % 32.26/32.51 (Or (Eq (action a_2) False) % 32.26/32.51 (Or (Eq (permission (skS.0 0 a_1 a_2 a a_3)) True) % 32.26/32.51 (Eq (activates (skS.0 5 a_1 a_2 a_4 a_5) (skS.0 3 a_1 a_2 a_4)) True)))) % 32.26/32.51 Clause #101 (by clausification #[99]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.26/32.51 Or (Eq (target a) False) % 32.26/32.51 (Or (Eq (agent a_1) False) % 32.26/32.51 (Or (Eq (action a_2) False) % 32.26/32.51 (Or (Eq (permission (skS.0 0 a_1 a_2 a a_3)) True) % 32.26/32.51 (Eq (And (And (proh (skS.0 3 a_1 a_2 a_4)) (aee (skS.0 3 a_1 a_2 a_4) a_1)) (act (skS.0 3 a_1 a_2 a_4) a_2)) % 32.26/32.51 True)))) % 32.26/32.51 Clause #102 (by superposition #[100, 3]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.26/32.51 Or (Eq (agent a) False) % 32.26/32.51 (Or (Eq (action a_1) False) % 32.26/32.51 (Or (Eq (permission (skS.0 0 a a_1 theater_ds a_2)) True) % 32.26/32.51 (Or (Eq (activates (skS.0 5 a a_1 a_3 a_4) (skS.0 3 a a_1 a_3)) True) (Eq False True)))) % 32.26/32.51 Clause #103 (by clausification #[98]): ∀ (a a_1 a_2 a_3 : Iota), % 32.26/32.51 Or (Eq (cnt (skS.0 0 a a_1 theater_ds a_2) a_1 theater_ds) True) % 32.26/32.51 (Or (Eq (agent a) False) (Or (Eq (action a_1) False) (Eq (proh (skS.0 1 a a_1 a_3)) True))) % 32.26/32.51 Clause #105 (by superposition #[103, 0]): ∀ (a a_1 a_2 : Iota), % 32.26/32.51 Or (Eq (cnt (skS.0 0 portal a theater_ds a_1) a theater_ds) True) % 32.26/32.51 (Or (Eq (action a) False) (Or (Eq (proh (skS.0 1 portal a a_2)) True) (Eq False True))) % 32.26/32.51 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 32.26/32.51 Or (Eq (cnt (skS.0 0 portal a theater_ds a_1) a theater_ds) True) % 32.26/32.51 (Or (Eq (action a) False) (Eq (proh (skS.0 1 portal a a_2)) True)) % 32.26/32.51 Clause #107 (by superposition #[106, 2]): ∀ (a a_1 : Iota), % 32.26/32.51 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.26/32.51 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq False True)) % 32.26/32.51 Clause #108 (by clausification #[107]): ∀ (a a_1 : Iota), % 32.26/32.51 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.26/32.51 (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.26/32.51 Clause #109 (by superposition #[108, 10]): ∀ (a a_1 : Iota), % 32.26/32.51 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.26/32.51 (Or (Eq True False) % 32.26/32.51 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_1)) False) % 32.26/32.51 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_1) portal) False))) % 32.26/32.51 Clause #114 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.26/32.51 Or (Eq (target a) False) % 32.26/32.51 (Or (Eq (agent a_1) False) % 32.26/32.51 (Or (Eq (action a_2) False) % 32.26/32.51 (Or (Eq (bearer (skS.0 0 a_1 a_2 a a_3) a_1) True) (Eq (act (skS.0 3 a_1 a_2 a_4) a_2) True)))) % 32.26/32.51 Clause #115 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.26/32.51 Or (Eq (target a) False) % 32.26/32.51 (Or (Eq (agent a_1) False) % 32.26/32.51 (Or (Eq (action a_2) False) % 32.26/32.51 (Or (Eq (bearer (skS.0 0 a_1 a_2 a a_3) a_1) True) % 32.26/32.51 (Eq (And (proh (skS.0 3 a_1 a_2 a_4)) (aee (skS.0 3 a_1 a_2 a_4) a_1)) True)))) % 32.26/32.51 Clause #116 (by superposition #[114, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.26/32.51 Or (Eq (agent a) False) % 32.26/32.51 (Or (Eq (action a_1) False) % 32.26/32.51 (Or (Eq (bearer (skS.0 0 a a_1 theater_ds a_2) a) True) % 32.26/32.51 (Or (Eq (act (skS.0 3 a a_1 a_3) a_1) True) (Eq False True)))) % 32.26/32.51 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 a_3 : Iota), % 32.26/32.51 Or (Eq (agent a) False) % 32.26/32.51 (Or (Eq (action a_1) False) % 32.26/32.51 (Or (Eq (bearer (skS.0 0 a a_1 theater_ds a_2) a) True) (Eq (act (skS.0 3 a a_1 a_3) a_1) True))) % 32.26/32.51 Clause #119 (by superposition #[117, 0]): ∀ (a a_1 a_2 : Iota), % 32.26/32.57 Or (Eq (action a) False) % 32.26/32.57 (Or (Eq (bearer (skS.0 0 portal a theater_ds a_1) portal) True) % 32.26/32.57 (Or (Eq (act (skS.0 3 portal a a_2) a) True) (Eq False True))) % 32.26/32.57 Clause #120 (by clausification #[119]): ∀ (a a_1 a_2 : Iota), % 32.26/32.57 Or (Eq (action a) False) % 32.26/32.57 (Or (Eq (bearer (skS.0 0 portal a theater_ds a_1) portal) True) (Eq (act (skS.0 3 portal a a_2) a) True)) % 32.26/32.57 Clause #121 (by superposition #[120, 2]): ∀ (a a_1 : Iota), % 32.26/32.57 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.26/32.57 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) (Eq False True)) % 32.26/32.57 Clause #122 (by clausification #[121]): ∀ (a a_1 : Iota), % 32.26/32.57 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.26/32.57 (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) % 32.26/32.57 Clause #128 (by clausification #[109]): ∀ (a a_1 : Iota), % 32.26/32.57 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.26/32.57 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_1)) False) % 32.26/32.57 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_1) portal) False)) % 32.26/32.57 Clause #129 (by clausification #[93]): ∀ (a a_1 : Iota), % 32.26/32.57 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.26/32.57 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_1)) False) % 32.26/32.57 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_1) portal) False)) % 32.26/32.57 Clause #131 (by clausification #[102]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.26/32.57 Or (Eq (agent a) False) % 32.26/32.57 (Or (Eq (action a_1) False) % 32.26/32.57 (Or (Eq (permission (skS.0 0 a a_1 theater_ds a_2)) True) % 32.26/32.57 (Eq (activates (skS.0 5 a a_1 a_3 a_4) (skS.0 3 a a_1 a_3)) True))) % 32.26/32.57 Clause #133 (by superposition #[131, 0]): ∀ (a a_1 a_2 a_3 : Iota), % 32.26/32.57 Or (Eq (action a) False) % 32.26/32.57 (Or (Eq (permission (skS.0 0 portal a theater_ds a_1)) True) % 32.26/32.57 (Or (Eq (activates (skS.0 5 portal a a_2 a_3) (skS.0 3 portal a a_2)) True) (Eq False True))) % 32.26/32.57 Clause #136 (by clausification #[133]): ∀ (a a_1 a_2 a_3 : Iota), % 32.26/32.57 Or (Eq (action a) False) % 32.26/32.57 (Or (Eq (permission (skS.0 0 portal a theater_ds a_1)) True) % 32.26/32.57 (Eq (activates (skS.0 5 portal a a_2 a_3) (skS.0 3 portal a a_2)) True)) % 32.26/32.57 Clause #137 (by superposition #[136, 2]): ∀ (a a_1 a_2 : Iota), % 32.26/32.57 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.26/32.57 (Or (Eq (activates (skS.0 5 portal modify_act a_1 a_2) (skS.0 3 portal modify_act a_1)) True) (Eq False True)) % 32.26/32.57 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 32.26/32.57 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.26/32.57 (Eq (activates (skS.0 5 portal modify_act a_1 a_2) (skS.0 3 portal modify_act a_1)) True) % 32.26/32.57 Clause #143 (by superposition #[138, 16]): ∀ (a a_1 : Iota), % 32.26/32.57 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.26/32.57 (Or (Eq True False) % 32.26/32.57 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 32.26/32.57 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) False) (Eq (aee (skS.0 3 portal modify_act a_1) portal) False)))) % 32.26/32.57 Clause #152 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.26/32.57 Or (Eq (target a) False) % 32.26/32.57 (Or (Eq (agent a_1) False) % 32.26/32.57 (Or (Eq (action a_2) False) % 32.26/32.57 (Or (Eq (bearer (skS.0 0 a_1 a_2 a a_3) a_1) True) (Eq (aee (skS.0 3 a_1 a_2 a_4) a_1) True)))) % 32.26/32.57 Clause #153 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.26/32.57 Or (Eq (target a) False) % 32.26/32.57 (Or (Eq (agent a_1) False) % 32.26/32.57 (Or (Eq (action a_2) False) % 32.26/32.57 (Or (Eq (bearer (skS.0 0 a_1 a_2 a a_3) a_1) True) (Eq (proh (skS.0 3 a_1 a_2 a_4)) True)))) % 32.26/32.57 Clause #154 (by superposition #[152, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.26/32.57 Or (Eq (agent a) False) % 32.26/32.57 (Or (Eq (action a_1) False) % 32.26/32.57 (Or (Eq (bearer (skS.0 0 a a_1 theater_ds a_2) a) True) % 32.26/32.57 (Or (Eq (aee (skS.0 3 a a_1 a_3) a) True) (Eq False True)))) % 32.26/32.57 Clause #155 (by clausification #[60]): ∀ (a a_1 : Iota), % 32.26/32.57 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.26/32.57 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 32.26/32.57 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) False) (Eq (aee (skS.0 3 portal modify_act a_1) portal) False))) % 32.26/32.57 Clause #157 (by clausification #[154]): ∀ (a a_1 a_2 a_3 : Iota), % 32.26/32.57 Or (Eq (agent a) False) % 32.36/32.63 (Or (Eq (action a_1) False) % 32.36/32.63 (Or (Eq (bearer (skS.0 0 a a_1 theater_ds a_2) a) True) (Eq (aee (skS.0 3 a a_1 a_3) a) True))) % 32.36/32.63 Clause #159 (by superposition #[157, 0]): ∀ (a a_1 a_2 : Iota), % 32.36/32.63 Or (Eq (action a) False) % 32.36/32.63 (Or (Eq (bearer (skS.0 0 portal a theater_ds a_1) portal) True) % 32.36/32.63 (Or (Eq (aee (skS.0 3 portal a a_2) portal) True) (Eq False True))) % 32.36/32.63 Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), % 32.36/32.63 Or (Eq (action a) False) % 32.36/32.63 (Or (Eq (bearer (skS.0 0 portal a theater_ds a_1) portal) True) (Eq (aee (skS.0 3 portal a a_2) portal) True)) % 32.36/32.63 Clause #161 (by superposition #[160, 2]): ∀ (a a_1 : Iota), % 32.36/32.63 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.36/32.63 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) (Eq False True)) % 32.36/32.63 Clause #162 (by clausification #[161]): ∀ (a a_1 : Iota), % 32.36/32.63 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.36/32.63 (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) % 32.36/32.63 Clause #168 (by superposition #[153, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.36/32.63 Or (Eq (agent a) False) % 32.36/32.63 (Or (Eq (action a_1) False) % 32.36/32.63 (Or (Eq (bearer (skS.0 0 a a_1 theater_ds a_2) a) True) % 32.36/32.63 (Or (Eq (proh (skS.0 3 a a_1 a_3)) True) (Eq False True)))) % 32.36/32.63 Clause #169 (by clausification #[168]): ∀ (a a_1 a_2 a_3 : Iota), % 32.36/32.63 Or (Eq (agent a) False) % 32.36/32.63 (Or (Eq (action a_1) False) % 32.36/32.63 (Or (Eq (bearer (skS.0 0 a a_1 theater_ds a_2) a) True) (Eq (proh (skS.0 3 a a_1 a_3)) True))) % 32.36/32.63 Clause #171 (by superposition #[169, 0]): ∀ (a a_1 a_2 : Iota), % 32.36/32.63 Or (Eq (action a) False) % 32.36/32.63 (Or (Eq (bearer (skS.0 0 portal a theater_ds a_1) portal) True) % 32.36/32.63 (Or (Eq (proh (skS.0 3 portal a a_2)) True) (Eq False True))) % 32.36/32.63 Clause #172 (by clausification #[171]): ∀ (a a_1 a_2 : Iota), % 32.36/32.63 Or (Eq (action a) False) % 32.36/32.63 (Or (Eq (bearer (skS.0 0 portal a theater_ds a_1) portal) True) (Eq (proh (skS.0 3 portal a a_2)) True)) % 32.36/32.63 Clause #173 (by superposition #[172, 2]): ∀ (a a_1 : Iota), % 32.36/32.63 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.36/32.63 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Eq False True)) % 32.36/32.63 Clause #174 (by clausification #[173]): ∀ (a a_1 : Iota), % 32.36/32.63 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.36/32.63 Clause #195 (by clausification #[101]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.36/32.63 Or (Eq (target a) False) % 32.36/32.63 (Or (Eq (agent a_1) False) % 32.36/32.63 (Or (Eq (action a_2) False) % 32.36/32.63 (Or (Eq (permission (skS.0 0 a_1 a_2 a a_3)) True) (Eq (act (skS.0 3 a_1 a_2 a_4) a_2) True)))) % 32.36/32.63 Clause #196 (by clausification #[101]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.36/32.63 Or (Eq (target a) False) % 32.36/32.63 (Or (Eq (agent a_1) False) % 32.36/32.63 (Or (Eq (action a_2) False) % 32.36/32.63 (Or (Eq (permission (skS.0 0 a_1 a_2 a a_3)) True) % 32.36/32.63 (Eq (And (proh (skS.0 3 a_1 a_2 a_4)) (aee (skS.0 3 a_1 a_2 a_4) a_1)) True)))) % 32.36/32.63 Clause #197 (by superposition #[195, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.36/32.63 Or (Eq (agent a) False) % 32.36/32.63 (Or (Eq (action a_1) False) % 32.36/32.63 (Or (Eq (permission (skS.0 0 a a_1 theater_ds a_2)) True) % 32.36/32.63 (Or (Eq (act (skS.0 3 a a_1 a_3) a_1) True) (Eq False True)))) % 32.36/32.63 Clause #198 (by clausification #[197]): ∀ (a a_1 a_2 a_3 : Iota), % 32.36/32.63 Or (Eq (agent a) False) % 32.36/32.63 (Or (Eq (action a_1) False) % 32.36/32.63 (Or (Eq (permission (skS.0 0 a a_1 theater_ds a_2)) True) (Eq (act (skS.0 3 a a_1 a_3) a_1) True))) % 32.36/32.63 Clause #200 (by superposition #[198, 0]): ∀ (a a_1 a_2 : Iota), % 32.36/32.63 Or (Eq (action a) False) % 32.36/32.63 (Or (Eq (permission (skS.0 0 portal a theater_ds a_1)) True) % 32.36/32.63 (Or (Eq (act (skS.0 3 portal a a_2) a) True) (Eq False True))) % 32.36/32.63 Clause #201 (by clausification #[200]): ∀ (a a_1 a_2 : Iota), % 32.36/32.63 Or (Eq (action a) False) % 32.36/32.63 (Or (Eq (permission (skS.0 0 portal a theater_ds a_1)) True) (Eq (act (skS.0 3 portal a a_2) a) True)) % 32.36/32.63 Clause #202 (by superposition #[201, 2]): ∀ (a a_1 : Iota), % 32.36/32.63 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.36/32.63 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) (Eq False True)) % 32.36/32.63 Clause #203 (by clausification #[202]): ∀ (a a_1 : Iota), % 32.36/32.63 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.36/32.68 (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) % 32.36/32.68 Clause #205 (by superposition #[203, 80]): ∀ (a a_1 a_2 : Iota), % 32.36/32.68 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.68 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.36/32.68 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.36/32.68 Clause #206 (by superposition #[203, 128]): ∀ (a a_1 a_2 : Iota), % 32.36/32.68 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.68 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.36/32.68 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.36/32.68 Clause #207 (by superposition #[203, 129]): ∀ (a a_1 a_2 : Iota), % 32.36/32.68 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.68 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.36/32.68 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.36/32.68 Clause #220 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 32.36/32.68 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.68 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.36/32.68 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.36/32.68 Clause #222 (by superposition #[220, 122]): ∀ (a a_1 a_2 : Iota), % 32.36/32.68 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.68 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.36/32.68 (Or (Eq False True) (Eq (act (skS.0 3 portal modify_act a_2) modify_act) True))) % 32.36/32.68 Clause #231 (by clausification #[222]): ∀ (a a_1 a_2 : Iota), % 32.36/32.68 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.68 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq (act (skS.0 3 portal modify_act a_2) modify_act) True)) % 32.36/32.68 Clause #235 (by equality factoring #[231]): ∀ (a a_1 : Iota), % 32.36/32.68 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.36/32.68 (Or (Ne True True) (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True)) % 32.36/32.68 Clause #241 (by clausification #[235]): ∀ (a a_1 : Iota), % 32.36/32.68 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.36/32.69 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) (Or (Eq True False) (Eq True False))) % 32.36/32.69 Clause #243 (by clausification #[241]): ∀ (a a_1 : Iota), % 32.36/32.69 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.36/32.69 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) (Eq True False)) % 32.36/32.69 Clause #244 (by clausification #[243]): ∀ (a a_1 : Iota), % 32.36/32.69 Or (Eq (proh (skS.0 1 portal modify_act a)) True) (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) % 32.36/32.69 Clause #247 (by clausification #[207]): ∀ (a a_1 a_2 : Iota), % 32.36/32.69 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.69 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.36/32.69 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.36/32.69 Clause #249 (by superposition #[247, 122]): ∀ (a a_1 a_2 : Iota), % 32.36/32.69 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.69 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.36/32.69 (Or (Eq False True) (Eq (act (skS.0 3 portal modify_act a_2) modify_act) True))) % 32.36/32.69 Clause #261 (by clausification #[249]): ∀ (a a_1 a_2 : Iota), % 32.36/32.69 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.36/32.69 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.36/32.69 (Eq (act (skS.0 3 portal modify_act a_2) modify_act) True)) % 32.36/32.69 Clause #264 (by equality factoring #[261]): ∀ (a a_1 : Iota), % 32.36/32.69 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.36/32.69 (Or (Ne True True) (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True)) % 32.36/32.69 Clause #265 (by clausification #[264]): ∀ (a a_1 : Iota), % 32.36/32.69 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.36/32.69 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) (Or (Eq True False) (Eq True False))) % 32.36/32.69 Clause #267 (by clausification #[265]): ∀ (a a_1 : Iota), % 32.36/32.69 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.36/32.69 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) (Eq True False)) % 32.36/32.69 Clause #268 (by clausification #[267]): ∀ (a a_1 : Iota), % 32.36/32.69 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) % 32.46/32.74 Clause #277 (by clausification #[205]): ∀ (a a_1 a_2 : Iota), % 32.46/32.74 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.46/32.74 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.46/32.74 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.46/32.74 Clause #279 (by superposition #[277, 122]): ∀ (a a_1 a_2 : Iota), % 32.46/32.74 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.46/32.74 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.46/32.74 (Or (Eq False True) (Eq (act (skS.0 3 portal modify_act a_2) modify_act) True))) % 32.46/32.74 Clause #288 (by clausification #[279]): ∀ (a a_1 a_2 : Iota), % 32.46/32.74 Or (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 32.46/32.74 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.46/32.74 (Eq (act (skS.0 3 portal modify_act a_2) modify_act) True)) % 32.46/32.74 Clause #292 (by equality factoring #[288]): ∀ (a a_1 : Iota), % 32.46/32.74 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.46/32.74 (Or (Ne True True) (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True)) % 32.46/32.74 Clause #293 (by clausification #[292]): ∀ (a a_1 : Iota), % 32.46/32.74 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.46/32.74 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) (Or (Eq True False) (Eq True False))) % 32.46/32.74 Clause #295 (by clausification #[293]): ∀ (a a_1 : Iota), % 32.46/32.74 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.46/32.74 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) (Eq True False)) % 32.46/32.74 Clause #296 (by clausification #[295]): ∀ (a a_1 : Iota), % 32.46/32.74 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) (Eq (act (skS.0 3 portal modify_act a_1) modify_act) True) % 32.46/32.74 Clause #299 (by clausification #[143]): ∀ (a a_1 : Iota), % 32.46/32.74 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.46/32.74 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 32.46/32.74 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) False) (Eq (aee (skS.0 3 portal modify_act a_1) portal) False))) % 32.46/32.74 Clause #305 (by clausification #[196]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.46/32.74 Or (Eq (target a) False) % 32.46/32.74 (Or (Eq (agent a_1) False) % 32.46/32.74 (Or (Eq (action a_2) False) % 32.46/32.74 (Or (Eq (permission (skS.0 0 a_1 a_2 a a_3)) True) (Eq (aee (skS.0 3 a_1 a_2 a_4) a_1) True)))) % 32.46/32.74 Clause #306 (by clausification #[196]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 32.46/32.74 Or (Eq (target a) False) % 32.46/32.74 (Or (Eq (agent a_1) False) % 32.46/32.74 (Or (Eq (action a_2) False) % 32.46/32.74 (Or (Eq (permission (skS.0 0 a_1 a_2 a a_3)) True) (Eq (proh (skS.0 3 a_1 a_2 a_4)) True)))) % 32.46/32.74 Clause #307 (by superposition #[305, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.46/32.74 Or (Eq (agent a) False) % 32.46/32.74 (Or (Eq (action a_1) False) % 32.46/32.74 (Or (Eq (permission (skS.0 0 a a_1 theater_ds a_2)) True) % 32.46/32.74 (Or (Eq (aee (skS.0 3 a a_1 a_3) a) True) (Eq False True)))) % 32.46/32.74 Clause #308 (by clausification #[307]): ∀ (a a_1 a_2 a_3 : Iota), % 32.46/32.74 Or (Eq (agent a) False) % 32.46/32.74 (Or (Eq (action a_1) False) % 32.46/32.74 (Or (Eq (permission (skS.0 0 a a_1 theater_ds a_2)) True) (Eq (aee (skS.0 3 a a_1 a_3) a) True))) % 32.46/32.74 Clause #310 (by superposition #[308, 0]): ∀ (a a_1 a_2 : Iota), % 32.46/32.74 Or (Eq (action a) False) % 32.46/32.74 (Or (Eq (permission (skS.0 0 portal a theater_ds a_1)) True) % 32.46/32.74 (Or (Eq (aee (skS.0 3 portal a a_2) portal) True) (Eq False True))) % 32.46/32.74 Clause #311 (by clausification #[310]): ∀ (a a_1 a_2 : Iota), % 32.46/32.74 Or (Eq (action a) False) % 32.46/32.74 (Or (Eq (permission (skS.0 0 portal a theater_ds a_1)) True) (Eq (aee (skS.0 3 portal a a_2) portal) True)) % 32.46/32.74 Clause #312 (by superposition #[311, 2]): ∀ (a a_1 : Iota), % 32.46/32.74 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.46/32.74 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) (Eq False True)) % 32.46/32.74 Clause #313 (by clausification #[312]): ∀ (a a_1 : Iota), % 32.46/32.74 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.46/32.74 (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) % 32.46/32.74 Clause #315 (by superposition #[313, 80]): ∀ (a a_1 a_2 : Iota), % 32.46/32.74 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.46/32.74 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.46/32.74 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.56/32.80 Clause #316 (by superposition #[313, 128]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.56/32.80 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.56/32.80 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.56/32.80 Clause #317 (by superposition #[313, 129]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.56/32.80 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.56/32.80 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.56/32.80 Clause #326 (by superposition #[306, 3]): ∀ (a a_1 a_2 a_3 : Iota), % 32.56/32.80 Or (Eq (agent a) False) % 32.56/32.80 (Or (Eq (action a_1) False) % 32.56/32.80 (Or (Eq (permission (skS.0 0 a a_1 theater_ds a_2)) True) % 32.56/32.80 (Or (Eq (proh (skS.0 3 a a_1 a_3)) True) (Eq False True)))) % 32.56/32.80 Clause #327 (by clausification #[326]): ∀ (a a_1 a_2 a_3 : Iota), % 32.56/32.80 Or (Eq (agent a) False) % 32.56/32.80 (Or (Eq (action a_1) False) % 32.56/32.80 (Or (Eq (permission (skS.0 0 a a_1 theater_ds a_2)) True) (Eq (proh (skS.0 3 a a_1 a_3)) True))) % 32.56/32.80 Clause #329 (by superposition #[327, 0]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (action a) False) % 32.56/32.80 (Or (Eq (permission (skS.0 0 portal a theater_ds a_1)) True) % 32.56/32.80 (Or (Eq (proh (skS.0 3 portal a a_2)) True) (Eq False True))) % 32.56/32.80 Clause #330 (by clausification #[329]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (action a) False) % 32.56/32.80 (Or (Eq (permission (skS.0 0 portal a theater_ds a_1)) True) (Eq (proh (skS.0 3 portal a a_2)) True)) % 32.56/32.80 Clause #331 (by superposition #[330, 2]): ∀ (a a_1 : Iota), % 32.56/32.80 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.56/32.80 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Eq False True)) % 32.56/32.80 Clause #333 (by clausification #[331]): ∀ (a a_1 : Iota), % 32.56/32.80 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.56/32.80 Clause #334 (by superposition #[333, 77]): ∀ (a a_1 a_2 a_3 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.80 (Or (Eq (activates (skS.0 2 portal modify_act a_1 a_2) (skS.0 1 portal modify_act a_1)) True) % 32.56/32.80 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_3) portal) False))) % 32.56/32.80 Clause #335 (by superposition #[333, 80]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.80 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.56/32.80 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.56/32.80 Clause #336 (by superposition #[333, 128]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.80 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.56/32.80 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.56/32.80 Clause #337 (by superposition #[333, 129]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.80 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.56/32.80 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.56/32.80 Clause #346 (by clausification #[336]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.80 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.56/32.80 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.56/32.80 Clause #350 (by superposition #[346, 174]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.80 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.56/32.80 (Or (Eq False True) (Eq (proh (skS.0 3 portal modify_act a_2)) True))) % 32.56/32.80 Clause #352 (by clausification #[350]): ∀ (a a_1 a_2 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.80 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq (proh (skS.0 3 portal modify_act a_2)) True)) % 32.56/32.80 Clause #354 (by equality factoring #[352]): ∀ (a a_1 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 1 portal modify_act a)) True) (Or (Ne True True) (Eq (proh (skS.0 3 portal modify_act a_1)) True)) % 32.56/32.80 Clause #355 (by clausification #[354]): ∀ (a a_1 : Iota), % 32.56/32.80 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.56/32.86 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Or (Eq True False) (Eq True False))) % 32.56/32.86 Clause #357 (by clausification #[355]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.56/32.86 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Eq True False)) % 32.56/32.86 Clause #358 (by clausification #[357]): ∀ (a a_1 : Iota), Or (Eq (proh (skS.0 1 portal modify_act a)) True) (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.56/32.86 Clause #363 (by clausification #[335]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.86 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.56/32.86 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.56/32.86 Clause #367 (by superposition #[363, 174]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.86 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.56/32.86 (Or (Eq False True) (Eq (proh (skS.0 3 portal modify_act a_2)) True))) % 32.56/32.86 Clause #368 (by clausification #[367]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.86 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) (Eq (proh (skS.0 3 portal modify_act a_2)) True)) % 32.56/32.86 Clause #370 (by equality factoring #[368]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.56/32.86 (Or (Ne True True) (Eq (proh (skS.0 3 portal modify_act a_1)) True)) % 32.56/32.86 Clause #371 (by clausification #[370]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.56/32.86 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Or (Eq True False) (Eq True False))) % 32.56/32.86 Clause #373 (by clausification #[371]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.56/32.86 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Eq True False)) % 32.56/32.86 Clause #374 (by clausification #[373]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.56/32.86 Clause #381 (by clausification #[337]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.86 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.56/32.86 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.56/32.86 Clause #385 (by superposition #[381, 174]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.86 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.56/32.86 (Or (Eq False True) (Eq (proh (skS.0 3 portal modify_act a_2)) True))) % 32.56/32.86 Clause #386 (by clausification #[385]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.56/32.86 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq (proh (skS.0 3 portal modify_act a_2)) True)) % 32.56/32.86 Clause #387 (by equality factoring #[386]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.56/32.86 (Or (Ne True True) (Eq (proh (skS.0 3 portal modify_act a_1)) True)) % 32.56/32.86 Clause #388 (by clausification #[387]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.56/32.86 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Or (Eq True False) (Eq True False))) % 32.56/32.86 Clause #390 (by clausification #[388]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.56/32.86 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Eq True False)) % 32.56/32.86 Clause #391 (by clausification #[390]): ∀ (a a_1 : Iota), % 32.56/32.86 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.56/32.86 Clause #400 (by clausification #[316]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.56/32.86 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.56/32.86 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.56/32.86 Clause #403 (by superposition #[400, 162]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.56/32.86 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.56/32.86 (Or (Eq False True) (Eq (aee (skS.0 3 portal modify_act a_2) portal) True))) % 32.56/32.86 Clause #406 (by clausification #[403]): ∀ (a a_1 a_2 : Iota), % 32.56/32.86 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq (aee (skS.0 3 portal modify_act a_2) portal) True)) % 32.66/32.92 Clause #408 (by equality factoring #[406]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.66/32.92 (Or (Ne True True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True)) % 32.66/32.92 Clause #412 (by clausification #[408]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.66/32.92 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) (Or (Eq True False) (Eq True False))) % 32.66/32.92 Clause #414 (by clausification #[412]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.66/32.92 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) (Eq True False)) % 32.66/32.92 Clause #415 (by clausification #[414]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (proh (skS.0 1 portal modify_act a)) True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) % 32.66/32.92 Clause #425 (by clausification #[317]): ∀ (a a_1 a_2 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.66/32.92 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.66/32.92 Clause #428 (by superposition #[425, 162]): ∀ (a a_1 a_2 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.66/32.92 (Or (Eq False True) (Eq (aee (skS.0 3 portal modify_act a_2) portal) True))) % 32.66/32.92 Clause #431 (by clausification #[428]): ∀ (a a_1 a_2 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq (aee (skS.0 3 portal modify_act a_2) portal) True)) % 32.66/32.92 Clause #433 (by equality factoring #[431]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.66/32.92 (Or (Ne True True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True)) % 32.66/32.92 Clause #434 (by clausification #[433]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) (Or (Eq True False) (Eq True False))) % 32.66/32.92 Clause #436 (by clausification #[434]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) (Eq True False)) % 32.66/32.92 Clause #437 (by clausification #[436]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) % 32.66/32.92 Clause #445 (by clausification #[315]): ∀ (a a_1 a_2 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.66/32.92 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.66/32.92 Clause #448 (by superposition #[445, 162]): ∀ (a a_1 a_2 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.66/32.92 (Or (Eq False True) (Eq (aee (skS.0 3 portal modify_act a_2) portal) True))) % 32.66/32.92 Clause #452 (by clausification #[448]): ∀ (a a_1 a_2 : Iota), % 32.66/32.92 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 32.66/32.92 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.66/32.92 (Eq (aee (skS.0 3 portal modify_act a_2) portal) True)) % 32.66/32.92 Clause #454 (by equality factoring #[452]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.66/32.92 (Or (Ne True True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True)) % 32.66/32.92 Clause #455 (by clausification #[454]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.66/32.92 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) (Or (Eq True False) (Eq True False))) % 32.66/32.92 Clause #457 (by clausification #[455]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.66/32.92 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) (Eq True False)) % 32.66/32.92 Clause #458 (by clausification #[457]): ∀ (a a_1 : Iota), % 32.66/32.92 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) % 32.66/32.98 Clause #489 (by clausification #[334]): ∀ (a a_1 a_2 a_3 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (activates (skS.0 2 portal modify_act a_1 a_2) (skS.0 1 portal modify_act a_1)) True) % 32.66/32.98 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_3) portal) False)) % 32.66/32.98 Clause #493 (by superposition #[489, 174]): ∀ (a a_1 a_2 a_3 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (activates (skS.0 2 portal modify_act a_1 a_2) (skS.0 1 portal modify_act a_1)) True) % 32.66/32.98 (Or (Eq False True) (Eq (proh (skS.0 3 portal modify_act a_3)) True))) % 32.66/32.98 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (activates (skS.0 2 portal modify_act a_1 a_2) (skS.0 1 portal modify_act a_1)) True) % 32.66/32.98 (Eq (proh (skS.0 3 portal modify_act a_3)) True)) % 32.66/32.98 Clause #498 (by equality factoring #[494]): ∀ (a a_1 a_2 : Iota), % 32.66/32.98 Or (Eq (activates (skS.0 2 portal modify_act a a_1) (skS.0 1 portal modify_act a)) True) % 32.66/32.98 (Or (Ne True True) (Eq (proh (skS.0 3 portal modify_act a_2)) True)) % 32.66/32.98 Clause #499 (by clausification #[498]): ∀ (a a_1 a_2 : Iota), % 32.66/32.98 Or (Eq (activates (skS.0 2 portal modify_act a a_1) (skS.0 1 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (proh (skS.0 3 portal modify_act a_2)) True) (Or (Eq True False) (Eq True False))) % 32.66/32.98 Clause #501 (by clausification #[499]): ∀ (a a_1 a_2 : Iota), % 32.66/32.98 Or (Eq (activates (skS.0 2 portal modify_act a a_1) (skS.0 1 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (proh (skS.0 3 portal modify_act a_2)) True) (Eq True False)) % 32.66/32.98 Clause #502 (by clausification #[501]): ∀ (a a_1 a_2 : Iota), % 32.66/32.98 Or (Eq (activates (skS.0 2 portal modify_act a a_1) (skS.0 1 portal modify_act a)) True) % 32.66/32.98 (Eq (proh (skS.0 3 portal modify_act a_2)) True) % 32.66/32.98 Clause #503 (by superposition #[502, 16]): ∀ (a a_1 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq True False) % 32.66/32.98 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) False) % 32.66/32.98 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) False) (Eq (aee (skS.0 1 portal modify_act a_1) portal) False)))) % 32.66/32.98 Clause #512 (by clausification #[503]): ∀ (a a_1 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) False) % 32.66/32.98 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) False) (Eq (aee (skS.0 1 portal modify_act a_1) portal) False))) % 32.66/32.98 Clause #515 (by superposition #[512, 374]): ∀ (a a_1 a_2 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) False) % 32.66/32.98 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) False) % 32.66/32.98 (Or (Eq False True) (Eq (proh (skS.0 3 portal modify_act a_2)) True)))) % 32.66/32.98 Clause #517 (by clausification #[515]): ∀ (a a_1 a_2 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) False) % 32.66/32.98 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) False) (Eq (proh (skS.0 3 portal modify_act a_2)) True))) % 32.66/32.98 Clause #520 (by superposition #[517, 358]): ∀ (a a_1 a_2 a_3 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) False) % 32.66/32.98 (Or (Eq (proh (skS.0 3 portal modify_act a_2)) True) % 32.66/32.98 (Or (Eq False True) (Eq (proh (skS.0 3 portal modify_act a_3)) True)))) % 32.66/32.98 Clause #523 (by clausification #[520]): ∀ (a a_1 a_2 a_3 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) False) % 32.66/32.98 (Or (Eq (proh (skS.0 3 portal modify_act a_2)) True) (Eq (proh (skS.0 3 portal modify_act a_3)) True))) % 32.66/32.98 Clause #526 (by superposition #[523, 391]): ∀ (a a_1 a_2 a_3 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.66/32.98 (Or (Eq (proh (skS.0 3 portal modify_act a_2)) True) % 32.66/32.98 (Or (Eq False True) (Eq (proh (skS.0 3 portal modify_act a_3)) True)))) % 32.66/32.98 Clause #528 (by clausification #[526]): ∀ (a a_1 a_2 a_3 : Iota), % 32.66/32.98 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.66/32.98 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_2)) True) (Eq (proh (skS.0 3 portal modify_act a_3)) True))) % 32.80/33.04 Clause #530 (by equality factoring #[528]): ∀ (a a_1 a_2 : Iota), % 32.80/33.04 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.80/33.04 (Or (Ne True True) (Eq (proh (skS.0 3 portal modify_act a_2)) True))) % 32.80/33.04 Clause #542 (by clausification #[530]): ∀ (a a_1 a_2 : Iota), % 32.80/33.04 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_2)) True) (Or (Eq True False) (Eq True False)))) % 32.80/33.04 Clause #544 (by clausification #[542]): ∀ (a a_1 a_2 : Iota), % 32.80/33.04 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_2)) True) (Eq True False))) % 32.80/33.04 Clause #545 (by clausification #[544]): ∀ (a a_1 a_2 : Iota), % 32.80/33.04 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Eq (proh (skS.0 3 portal modify_act a_2)) True)) % 32.80/33.04 Clause #548 (by equality factoring #[545]): ∀ (a a_1 : Iota), % 32.80/33.04 Or (Eq (proh (skS.0 3 portal modify_act a)) True) (Or (Ne True True) (Eq (proh (skS.0 3 portal modify_act a_1)) True)) % 32.80/33.04 Clause #549 (by clausification #[548]): ∀ (a a_1 : Iota), % 32.80/33.04 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Or (Eq True False) (Eq True False))) % 32.80/33.04 Clause #551 (by clausification #[549]): ∀ (a a_1 : Iota), % 32.80/33.04 Or (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.80/33.04 (Or (Eq (proh (skS.0 3 portal modify_act a_1)) True) (Eq True False)) % 32.80/33.04 Clause #552 (by clausification #[551]): ∀ (a a_1 : Iota), Or (Eq (proh (skS.0 3 portal modify_act a)) True) (Eq (proh (skS.0 3 portal modify_act a_1)) True) % 32.80/33.04 Clause #555 (by equality factoring #[552]): ∀ (a : Iota), Or (Ne True True) (Eq (proh (skS.0 3 portal modify_act a)) True) % 32.80/33.04 Clause #556 (by clausification #[555]): ∀ (a : Iota), Or (Eq (proh (skS.0 3 portal modify_act a)) True) (Or (Eq True False) (Eq True False)) % 32.80/33.04 Clause #558 (by clausification #[556]): ∀ (a : Iota), Or (Eq (proh (skS.0 3 portal modify_act a)) True) (Eq True False) % 32.80/33.04 Clause #559 (by clausification #[558]): ∀ (a : Iota), Eq (proh (skS.0 3 portal modify_act a)) True % 32.80/33.04 Clause #560 (by backward demodulation #[559, 155]): ∀ (a a_1 : Iota), % 32.80/33.04 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.80/33.04 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 32.80/33.04 (Or (Eq True False) (Eq (aee (skS.0 3 portal modify_act a_1) portal) False))) % 32.80/33.04 Clause #561 (by backward demodulation #[559, 299]): ∀ (a a_1 : Iota), % 32.80/33.04 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.04 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 32.80/33.04 (Or (Eq True False) (Eq (aee (skS.0 3 portal modify_act a_1) portal) False))) % 32.80/33.04 Clause #568 (by clausification #[561]): ∀ (a a_1 : Iota), % 32.80/33.04 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.04 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 32.80/33.04 (Eq (aee (skS.0 3 portal modify_act a_1) portal) False)) % 32.80/33.04 Clause #570 (by superposition #[568, 203]): ∀ (a a_1 a_2 : Iota), % 32.80/33.04 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.04 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.80/33.04 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a_2)) True) (Eq False True))) % 32.80/33.04 Clause #571 (by superposition #[568, 244]): ∀ (a a_1 a_2 : Iota), % 32.80/33.04 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.04 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.80/33.04 (Or (Eq (proh (skS.0 1 portal modify_act a_2)) True) (Eq False True))) % 32.80/33.04 Clause #572 (by superposition #[568, 268]): ∀ (a a_1 a_2 : Iota), % 32.80/33.04 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.04 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.80/33.04 (Or (Eq (aee (skS.0 1 portal modify_act a_2) portal) True) (Eq False True))) % 32.80/33.09 Clause #573 (by superposition #[568, 296]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.80/33.09 (Or (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True) (Eq False True))) % 32.80/33.09 Clause #574 (by clausification #[571]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) (Eq (proh (skS.0 1 portal modify_act a_2)) True)) % 32.80/33.09 Clause #577 (by superposition #[574, 415]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.80/33.09 (Or (Eq (proh (skS.0 1 portal modify_act a_2)) True) (Eq False True))) % 32.80/33.09 Clause #580 (by clausification #[577]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq (proh (skS.0 1 portal modify_act a_2)) True)) % 32.80/33.09 Clause #586 (by equality factoring #[580]): ∀ (a a_1 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Ne True True) (Eq (proh (skS.0 1 portal modify_act a_1)) True)) % 32.80/33.09 Clause #587 (by clausification #[586]): ∀ (a a_1 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Or (Eq True False) (Eq True False))) % 32.80/33.09 Clause #589 (by clausification #[587]): ∀ (a a_1 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq True False)) % 32.80/33.09 Clause #590 (by clausification #[589]): ∀ (a a_1 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.80/33.09 Clause #593 (by superposition #[590, 128]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.80/33.09 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.80/33.09 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.80/33.09 Clause #605 (by clausification #[593]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.80/33.09 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.80/33.09 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.80/33.09 Clause #623 (by clausification #[573]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.80/33.09 (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True)) % 32.80/33.09 Clause #628 (by superposition #[623, 458]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.80/33.09 (Or (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True) (Eq False True))) % 32.80/33.09 Clause #630 (by clausification #[628]): ∀ (a a_1 a_2 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.80/33.09 (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True)) % 32.80/33.09 Clause #636 (by equality factoring #[630]): ∀ (a a_1 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Ne True True) (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True)) % 32.80/33.09 Clause #637 (by clausification #[636]): ∀ (a a_1 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) (Or (Eq True False) (Eq True False))) % 32.80/33.09 Clause #639 (by clausification #[637]): ∀ (a a_1 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) (Eq True False)) % 32.80/33.09 Clause #640 (by clausification #[639]): ∀ (a a_1 : Iota), % 32.80/33.09 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.80/33.09 (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.80/33.09 Clause #642 (by superposition #[640, 80]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.90/33.16 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.90/33.16 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.90/33.16 Clause #649 (by clausification #[572]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.90/33.16 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) (Eq (aee (skS.0 1 portal modify_act a_2) portal) True)) % 32.90/33.16 Clause #653 (by superposition #[649, 437]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.90/33.16 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.90/33.16 (Or (Eq (aee (skS.0 1 portal modify_act a_2) portal) True) (Eq False True))) % 32.90/33.16 Clause #660 (by clausification #[653]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.90/33.16 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq (aee (skS.0 1 portal modify_act a_2) portal) True)) % 32.90/33.16 Clause #668 (by equality factoring #[660]): ∀ (a a_1 : Iota), % 32.90/33.16 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.90/33.16 (Or (Ne True True) (Eq (aee (skS.0 1 portal modify_act a_1) portal) True)) % 32.90/33.16 Clause #669 (by clausification #[668]): ∀ (a a_1 : Iota), % 32.90/33.16 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.90/33.16 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Or (Eq True False) (Eq True False))) % 32.90/33.16 Clause #671 (by clausification #[669]): ∀ (a a_1 : Iota), % 32.90/33.16 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.90/33.16 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq True False)) % 32.90/33.16 Clause #672 (by clausification #[671]): ∀ (a a_1 : Iota), % 32.90/33.16 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.90/33.16 (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.90/33.16 Clause #676 (by superposition #[672, 129]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 32.90/33.16 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.90/33.16 (Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False))) % 32.90/33.16 Clause #688 (by clausification #[560]): ∀ (a a_1 : Iota), % 32.90/33.16 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.90/33.16 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 32.90/33.16 (Eq (aee (skS.0 3 portal modify_act a_1) portal) False)) % 32.90/33.16 Clause #691 (by superposition #[688, 244]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.90/33.16 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.90/33.16 (Or (Eq (proh (skS.0 1 portal modify_act a_2)) True) (Eq False True))) % 32.90/33.16 Clause #692 (by superposition #[688, 268]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.90/33.16 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.90/33.16 (Or (Eq (aee (skS.0 1 portal modify_act a_2) portal) True) (Eq False True))) % 32.90/33.16 Clause #693 (by superposition #[688, 296]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.90/33.16 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.90/33.16 (Or (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True) (Eq False True))) % 32.90/33.16 Clause #694 (by clausification #[691]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.90/33.16 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) (Eq (proh (skS.0 1 portal modify_act a_2)) True)) % 32.90/33.16 Clause #697 (by superposition #[694, 415]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.90/33.16 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.90/33.16 (Or (Eq (proh (skS.0 1 portal modify_act a_2)) True) (Eq False True))) % 32.90/33.16 Clause #700 (by clausification #[697]): ∀ (a a_1 a_2 : Iota), % 32.90/33.16 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.90/33.16 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq (proh (skS.0 1 portal modify_act a_2)) True)) % 32.90/33.16 Clause #710 (by equality factoring #[700]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.21 (Or (Ne True True) (Eq (proh (skS.0 1 portal modify_act a_1)) True)) % 32.96/33.21 Clause #714 (by clausification #[710]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.21 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Or (Eq True False) (Eq True False))) % 32.96/33.21 Clause #716 (by clausification #[714]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.21 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq True False)) % 32.96/33.21 Clause #717 (by clausification #[716]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.96/33.21 Clause #723 (by superposition #[717, 605]): ∀ (a a_1 a_2 : Iota), % 32.96/33.21 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.96/33.21 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.96/33.21 (Or (Eq (proh (skS.0 1 portal modify_act a_2)) True) (Eq True False))) % 32.96/33.21 Clause #727 (by clausification #[723]): ∀ (a a_1 a_2 : Iota), % 32.96/33.21 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.96/33.21 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq (proh (skS.0 1 portal modify_act a_2)) True)) % 32.96/33.21 Clause #729 (by equality factoring #[727]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (proh (skS.0 1 portal modify_act a)) True) (Or (Ne True True) (Eq (proh (skS.0 1 portal modify_act a_1)) True)) % 32.96/33.21 Clause #730 (by clausification #[729]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.96/33.21 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Or (Eq True False) (Eq True False))) % 32.96/33.21 Clause #732 (by clausification #[730]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.96/33.21 (Or (Eq (proh (skS.0 1 portal modify_act a_1)) True) (Eq True False)) % 32.96/33.21 Clause #733 (by clausification #[732]): ∀ (a a_1 : Iota), Or (Eq (proh (skS.0 1 portal modify_act a)) True) (Eq (proh (skS.0 1 portal modify_act a_1)) True) % 32.96/33.21 Clause #735 (by equality factoring #[733]): ∀ (a : Iota), Or (Ne True True) (Eq (proh (skS.0 1 portal modify_act a)) True) % 32.96/33.21 Clause #736 (by clausification #[735]): ∀ (a : Iota), Or (Eq (proh (skS.0 1 portal modify_act a)) True) (Or (Eq True False) (Eq True False)) % 32.96/33.21 Clause #738 (by clausification #[736]): ∀ (a : Iota), Or (Eq (proh (skS.0 1 portal modify_act a)) True) (Eq True False) % 32.96/33.21 Clause #739 (by clausification #[738]): ∀ (a : Iota), Eq (proh (skS.0 1 portal modify_act a)) True % 32.96/33.21 Clause #740 (by backward demodulation #[739, 88]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 32.96/33.21 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) False) % 32.96/33.21 (Or (Eq True False) (Eq (aee (skS.0 1 portal modify_act a_1) portal) False))) % 32.96/33.21 Clause #754 (by clausification #[692]): ∀ (a a_1 a_2 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.21 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) (Eq (aee (skS.0 1 portal modify_act a_2) portal) True)) % 32.96/33.21 Clause #757 (by superposition #[754, 437]): ∀ (a a_1 a_2 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.21 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.96/33.21 (Or (Eq (aee (skS.0 1 portal modify_act a_2) portal) True) (Eq False True))) % 32.96/33.21 Clause #768 (by clausification #[757]): ∀ (a a_1 a_2 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.21 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq (aee (skS.0 1 portal modify_act a_2) portal) True)) % 32.96/33.21 Clause #777 (by equality factoring #[768]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.21 (Or (Ne True True) (Eq (aee (skS.0 1 portal modify_act a_1) portal) True)) % 32.96/33.21 Clause #778 (by clausification #[777]): ∀ (a a_1 : Iota), % 32.96/33.21 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.21 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Or (Eq True False) (Eq True False))) % 32.96/33.21 Clause #780 (by clausification #[778]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq True False)) % 32.96/33.27 Clause #781 (by clausification #[780]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 32.96/33.27 Clause #796 (by clausification #[570]): ∀ (a a_1 a_2 : Iota), % 32.96/33.27 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 32.96/33.27 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.96/33.27 (Eq (permission (skS.0 0 portal modify_act theater_ds a_2)) True)) % 32.96/33.27 Clause #809 (by clausification #[693]): ∀ (a a_1 a_2 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Or (Eq (aee (skS.0 3 portal modify_act a_1) portal) False) % 32.96/33.27 (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True)) % 32.96/33.27 Clause #813 (by superposition #[809, 458]): ∀ (a a_1 a_2 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True) (Eq False True))) % 32.96/33.27 Clause #814 (by clausification #[813]): ∀ (a a_1 a_2 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.96/33.27 (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True)) % 32.96/33.27 Clause #819 (by equality factoring #[814]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Or (Ne True True) (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True)) % 32.96/33.27 Clause #820 (by clausification #[819]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) (Or (Eq True False) (Eq True False))) % 32.96/33.27 Clause #822 (by clausification #[820]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) (Eq True False)) % 32.96/33.27 Clause #823 (by clausification #[822]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 32.96/33.27 (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.96/33.27 Clause #834 (by clausification #[642]): ∀ (a a_1 a_2 : Iota), % 32.96/33.27 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.96/33.27 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 32.96/33.27 Clause #839 (by superposition #[834, 823]): ∀ (a a_1 a_2 : Iota), % 32.96/33.27 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.96/33.27 (Or (Eq False True) (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True))) % 32.96/33.27 Clause #840 (by clausification #[839]): ∀ (a a_1 a_2 : Iota), % 32.96/33.27 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.96/33.27 (Eq (act (skS.0 1 portal modify_act a_2) modify_act) True)) % 32.96/33.27 Clause #841 (by equality factoring #[840]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.96/33.27 (Or (Ne True True) (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True)) % 32.96/33.27 Clause #847 (by clausification #[841]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) (Or (Eq True False) (Eq True False))) % 32.96/33.27 Clause #849 (by clausification #[847]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.96/33.27 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) (Eq True False)) % 32.96/33.27 Clause #850 (by clausification #[849]): ∀ (a a_1 : Iota), % 32.96/33.27 Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) (Eq (act (skS.0 1 portal modify_act a_1) modify_act) True) % 32.96/33.27 Clause #851 (by equality factoring #[850]): ∀ (a : Iota), Or (Ne True True) (Eq (act (skS.0 1 portal modify_act a) modify_act) True) % 32.96/33.27 Clause #852 (by clausification #[851]): ∀ (a : Iota), Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) (Or (Eq True False) (Eq True False)) % 33.06/33.32 Clause #854 (by clausification #[852]): ∀ (a : Iota), Or (Eq (act (skS.0 1 portal modify_act a) modify_act) True) (Eq True False) % 33.06/33.32 Clause #855 (by clausification #[854]): ∀ (a : Iota), Eq (act (skS.0 1 portal modify_act a) modify_act) True % 33.06/33.32 Clause #865 (by clausification #[676]): ∀ (a a_1 a_2 : Iota), % 33.06/33.32 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 33.06/33.32 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 33.06/33.32 (Eq (bearer (skS.0 0 portal modify_act theater_ds a_2) portal) False)) % 33.06/33.32 Clause #869 (by superposition #[865, 781]): ∀ (a a_1 a_2 : Iota), % 33.06/33.32 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 33.06/33.32 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 33.06/33.32 (Or (Eq False True) (Eq (aee (skS.0 1 portal modify_act a_2) portal) True))) % 33.06/33.32 Clause #870 (by clausification #[869]): ∀ (a a_1 a_2 : Iota), % 33.06/33.32 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 33.06/33.32 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq (aee (skS.0 1 portal modify_act a_2) portal) True)) % 33.06/33.32 Clause #876 (by equality factoring #[870]): ∀ (a a_1 : Iota), % 33.06/33.32 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 33.06/33.32 (Or (Ne True True) (Eq (aee (skS.0 1 portal modify_act a_1) portal) True)) % 33.06/33.32 Clause #878 (by clausification #[876]): ∀ (a a_1 : Iota), % 33.06/33.32 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 33.06/33.32 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Or (Eq True False) (Eq True False))) % 33.06/33.32 Clause #880 (by clausification #[878]): ∀ (a a_1 : Iota), % 33.06/33.32 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 33.06/33.32 (Or (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) (Eq True False)) % 33.06/33.32 Clause #881 (by clausification #[880]): ∀ (a a_1 : Iota), % 33.06/33.32 Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) (Eq (aee (skS.0 1 portal modify_act a_1) portal) True) % 33.06/33.32 Clause #887 (by equality factoring #[881]): ∀ (a : Iota), Or (Ne True True) (Eq (aee (skS.0 1 portal modify_act a) portal) True) % 33.06/33.32 Clause #888 (by clausification #[887]): ∀ (a : Iota), Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) (Or (Eq True False) (Eq True False)) % 33.06/33.32 Clause #890 (by clausification #[888]): ∀ (a : Iota), Or (Eq (aee (skS.0 1 portal modify_act a) portal) True) (Eq True False) % 33.06/33.32 Clause #891 (by clausification #[890]): ∀ (a : Iota), Eq (aee (skS.0 1 portal modify_act a) portal) True % 33.06/33.32 Clause #911 (by clausification #[740]): ∀ (a a_1 : Iota), % 33.06/33.32 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 33.06/33.32 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) False) % 33.06/33.32 (Eq (aee (skS.0 1 portal modify_act a_1) portal) False)) % 33.06/33.32 Clause #912 (by forward demodulation #[911, 891]): ∀ (a a_1 : Iota), % 33.06/33.32 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 33.06/33.32 (Or (Eq (act (skS.0 1 portal modify_act a_1) modify_act) False) (Eq True False)) % 33.06/33.32 Clause #913 (by clausification #[912]): ∀ (a a_1 : Iota), % 33.06/33.32 Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) % 33.06/33.32 (Eq (act (skS.0 1 portal modify_act a_1) modify_act) False) % 33.06/33.32 Clause #914 (by superposition #[913, 855]): ∀ (a : Iota), Or (Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True) (Eq False True) % 33.06/33.32 Clause #915 (by clausification #[914]): ∀ (a : Iota), Eq (cnt (skS.0 0 portal modify_act theater_ds a) modify_act theater_ds) True % 33.06/33.32 Clause #916 (by superposition #[915, 10]): ∀ (a : Iota), % 33.06/33.32 Or (Eq True False) % 33.06/33.32 (Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) False) % 33.06/33.32 (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) False)) % 33.06/33.32 Clause #920 (by clausification #[916]): ∀ (a : Iota), % 33.06/33.32 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) False) % 33.06/33.32 (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) False) % 33.06/33.32 Clause #923 (by superposition #[920, 313]): ∀ (a a_1 : Iota), % 33.06/33.32 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) False) % 33.06/33.32 (Or (Eq False True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True)) % 33.06/33.37 Clause #924 (by clausification #[923]): ∀ (a a_1 : Iota), % 33.06/33.37 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) False) % 33.06/33.37 (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) % 33.06/33.37 Clause #927 (by superposition #[924, 162]): ∀ (a a_1 : Iota), % 33.06/33.37 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 33.06/33.37 (Or (Eq False True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True)) % 33.06/33.37 Clause #928 (by clausification #[927]): ∀ (a a_1 : Iota), % 33.06/33.37 Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) (Eq (aee (skS.0 3 portal modify_act a_1) portal) True) % 33.06/33.37 Clause #931 (by equality factoring #[928]): ∀ (a : Iota), Or (Ne True True) (Eq (aee (skS.0 3 portal modify_act a) portal) True) % 33.06/33.37 Clause #932 (by clausification #[931]): ∀ (a : Iota), Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) (Or (Eq True False) (Eq True False)) % 33.06/33.37 Clause #934 (by clausification #[932]): ∀ (a : Iota), Or (Eq (aee (skS.0 3 portal modify_act a) portal) True) (Eq True False) % 33.06/33.37 Clause #935 (by clausification #[934]): ∀ (a : Iota), Eq (aee (skS.0 3 portal modify_act a) portal) True % 33.06/33.37 Clause #937 (by backward demodulation #[935, 688]): ∀ (a a_1 : Iota), % 33.06/33.37 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 33.06/33.37 (Or (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) (Eq True False)) % 33.06/33.37 Clause #939 (by superposition #[935, 796]): ∀ (a a_1 : Iota), % 33.06/33.37 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 33.06/33.37 (Or (Eq True False) (Eq (permission (skS.0 0 portal modify_act theater_ds a_1)) True)) % 33.06/33.37 Clause #948 (by clausification #[937]): ∀ (a a_1 : Iota), % 33.06/33.37 Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) % 33.06/33.37 (Eq (act (skS.0 3 portal modify_act a_1) modify_act) False) % 33.06/33.37 Clause #952 (by clausification #[939]): ∀ (a a_1 : Iota), % 33.06/33.37 Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 33.06/33.37 (Eq (permission (skS.0 0 portal modify_act theater_ds a_1)) True) % 33.06/33.37 Clause #954 (by equality factoring #[952]): ∀ (a : Iota), Or (Ne True True) (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) % 33.06/33.37 Clause #955 (by clausification #[954]): ∀ (a : Iota), Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) (Or (Eq True False) (Eq True False)) % 33.06/33.37 Clause #957 (by clausification #[955]): ∀ (a : Iota), Or (Eq (permission (skS.0 0 portal modify_act theater_ds a)) True) (Eq True False) % 33.06/33.37 Clause #958 (by clausification #[957]): ∀ (a : Iota), Eq (permission (skS.0 0 portal modify_act theater_ds a)) True % 33.06/33.37 Clause #959 (by backward demodulation #[958, 920]): ∀ (a : Iota), Or (Eq True False) (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) False) % 33.06/33.37 Clause #961 (by clausification #[959]): ∀ (a : Iota), Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) False % 33.06/33.37 Clause #963 (by superposition #[961, 122]): ∀ (a : Iota), Or (Eq False True) (Eq (act (skS.0 3 portal modify_act a) modify_act) True) % 33.06/33.37 Clause #964 (by clausification #[963]): ∀ (a : Iota), Eq (act (skS.0 3 portal modify_act a) modify_act) True % 33.06/33.37 Clause #965 (by superposition #[964, 948]): ∀ (a : Iota), Or (Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True) (Eq True False) % 33.06/33.37 Clause #966 (by clausification #[965]): ∀ (a : Iota), Eq (bearer (skS.0 0 portal modify_act theater_ds a) portal) True % 33.06/33.37 Clause #967 (by superposition #[966, 961]): Eq True False % 33.06/33.37 Clause #968 (by clausification #[967]): False % 33.06/33.37 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------