%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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 : Unsatisfiable 10.76s 11.08s % Output : Proof 11.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.02 % Command : duper %s % 0.04/0.30 % Computer : n012.cluster.edu % 0.04/0.30 % Model : x86_64 x86_64 % 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.04/0.30 % Memory : 8046.5625MB % 0.04/0.30 % OS : Linux 6.8.0-71-generic % 0.04/0.31 % CPULimit : 300 % 0.04/0.31 % WCLimit : 300 % 0.04/0.31 % DateTime : Mon Sep 7 14:07:56 UTC 2026 % 0.04/0.31 % CPUTime : % 10.76/11.08 SZS status Theorem for theBenchmark.p % 10.76/11.08 SZS output start Proof for theBenchmark.p % 10.76/11.08 Clause #0 (by assumption #[]): Eq % 10.76/11.08 (∀ (Rho A T : Iota), % 10.76/11.08 odrl_rel Rho → % 10.76/11.08 Iff % 10.76/11.08 (Exists fun L => % 10.76/11.08 And (And (And (permission L) (part_of L Rho)) (cnt L A T)) % 10.76/11.08 (∀ (L2 : Iota), And (And (permission L2) (part_of L2 Rho)) (cnt L2 A T) → Eq L2 L)) % 10.76/11.08 (Exists fun N => % 10.76/11.08 And (And (And (no_right N) (part_of N Rho)) (cnt N A T)) % 10.76/11.08 (∀ (M : Iota), And (And (no_right M) (part_of M Rho)) (cnt M A T) → Eq M N))) % 10.76/11.08 True % 10.76/11.08 Clause #5 (by assumption #[]): Eq (odrl_rel rho1) True % 10.76/11.08 Clause #6 (by assumption #[]): Eq (permission l) True % 10.76/11.08 Clause #7 (by assumption #[]): Eq (no_right n1) True % 10.76/11.08 Clause #8 (by assumption #[]): Eq (no_right n2) True % 10.76/11.08 Clause #9 (by assumption #[]): Eq (part_of l rho1) True % 10.76/11.08 Clause #10 (by assumption #[]): Eq (part_of n1 rho1) True % 10.76/11.08 Clause #11 (by assumption #[]): Eq (part_of n2 rho1) True % 10.76/11.08 Clause #12 (by assumption #[]): Eq (cnt l some_action some_target) True % 10.76/11.08 Clause #13 (by assumption #[]): Eq (cnt n1 some_action some_target) True % 10.76/11.08 Clause #14 (by assumption #[]): Eq (cnt n2 some_action some_target) True % 10.76/11.08 Clause #17 (by assumption #[]): Eq (Ne n1 n2) True % 10.76/11.08 Clause #18 (by assumption #[]): Eq (∀ (L2 : Iota), And (And (permission L2) (part_of L2 rho1)) (cnt L2 some_action some_target) → Eq L2 l) True % 10.76/11.08 Clause #19 (by clausification #[0]): ∀ (a : Iota), % 10.76/11.08 Eq % 10.76/11.08 (∀ (A T : Iota), % 10.76/11.08 odrl_rel a → % 10.76/11.08 Iff % 10.76/11.08 (Exists fun L => % 10.76/11.08 And (And (And (permission L) (part_of L a)) (cnt L A T)) % 10.76/11.08 (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 A T) → Eq L2 L)) % 10.76/11.08 (Exists fun N => % 10.76/11.08 And (And (And (no_right N) (part_of N a)) (cnt N A T)) % 10.76/11.08 (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M A T) → Eq M N))) % 10.76/11.08 True % 10.76/11.08 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), % 10.76/11.08 Eq % 10.76/11.08 (∀ (T : Iota), % 10.76/11.08 odrl_rel a → % 10.76/11.08 Iff % 10.76/11.08 (Exists fun L => % 10.76/11.08 And (And (And (permission L) (part_of L a)) (cnt L a_1 T)) % 10.76/11.08 (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_1 T) → Eq L2 L)) % 10.76/11.08 (Exists fun N => % 10.76/11.08 And (And (And (no_right N) (part_of N a)) (cnt N a_1 T)) % 10.76/11.08 (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_1 T) → Eq M N))) % 10.76/11.08 True % 10.76/11.08 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 : Iota), % 10.76/11.08 Eq % 10.76/11.08 (odrl_rel a → % 10.76/11.08 Iff % 10.76/11.08 (Exists fun L => % 10.76/11.08 And (And (And (permission L) (part_of L a)) (cnt L a_1 a_2)) % 10.76/11.08 (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_1 a_2) → Eq L2 L)) % 10.76/11.08 (Exists fun N => % 10.76/11.08 And (And (And (no_right N) (part_of N a)) (cnt N a_1 a_2)) % 10.76/11.08 (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_1 a_2) → Eq M N))) % 10.76/11.08 True % 10.76/11.08 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 : Iota), % 10.76/11.08 Or (Eq (odrl_rel a) False) % 10.76/11.08 (Eq % 10.76/11.08 (Iff % 10.76/11.08 (Exists fun L => % 10.76/11.08 And (And (And (permission L) (part_of L a)) (cnt L a_1 a_2)) % 10.76/11.08 (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_1 a_2) → Eq L2 L)) % 10.76/11.08 (Exists fun N => % 10.76/11.08 And (And (And (no_right N) (part_of N a)) (cnt N a_1 a_2)) % 10.76/11.08 (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_1 a_2) → Eq M N))) % 10.76/11.08 True) % 10.76/11.08 Clause #24 (by clausification #[22]): ∀ (a a_1 a_2 : Iota), % 10.76/11.08 Or (Eq (odrl_rel a) False) % 10.76/11.08 (Or % 10.76/11.08 (Eq % 10.76/11.08 (Exists fun L => % 10.76/11.08 And (And (And (permission L) (part_of L a)) (cnt L a_1 a_2)) % 10.76/11.08 (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_1 a_2) → Eq L2 L)) % 10.76/11.08 False) % 10.76/11.08 (Eq % 10.76/11.08 (Exists fun N => % 10.76/11.08 And (And (And (no_right N) (part_of N a)) (cnt N a_1 a_2)) % 10.76/11.08 (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_1 a_2) → Eq M N)) % 10.76/11.08 True)) % 10.76/11.08 Clause #44 (by clausification #[17]): Ne n1 n2 % 10.76/11.08 Clause #45 (by clausification #[18]): ∀ (a : Iota), Eq (And (And (permission a) (part_of a rho1)) (cnt a some_action some_target) → Eq a l) True % 10.76/11.11 Clause #46 (by clausification #[45]): ∀ (a : Iota), % 10.76/11.11 Or (Eq (And (And (permission a) (part_of a rho1)) (cnt a some_action some_target)) False) (Eq (Eq a l) True) % 10.76/11.11 Clause #47 (by clausification #[46]): ∀ (a : Iota), % 10.76/11.11 Or (Eq (Eq a l) True) (Or (Eq (And (permission a) (part_of a rho1)) False) (Eq (cnt a some_action some_target) False)) % 10.76/11.11 Clause #48 (by clausification #[47]): ∀ (a : Iota), % 10.76/11.11 Or (Eq (And (permission a) (part_of a rho1)) False) (Or (Eq (cnt a some_action some_target) False) (Eq a l)) % 10.76/11.11 Clause #49 (by clausification #[48]): ∀ (a : Iota), % 10.76/11.11 Or (Eq (cnt a some_action some_target) False) (Or (Eq a l) (Or (Eq (permission a) False) (Eq (part_of a rho1) False))) % 10.76/11.11 Clause #56 (by clausification #[24]): ∀ (a a_1 a_2 a_3 : Iota), % 10.76/11.11 Or (Eq (odrl_rel a) False) % 10.76/11.11 (Or % 10.76/11.11 (Eq % 10.76/11.11 (Exists fun N => % 10.76/11.11 And (And (And (no_right N) (part_of N a)) (cnt N a_1 a_2)) % 10.76/11.11 (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_1 a_2) → Eq M N)) % 10.76/11.11 True) % 10.76/11.11 (Eq % 10.76/11.11 (And (And (And (permission a_3) (part_of a_3 a)) (cnt a_3 a_1 a_2)) % 10.76/11.11 (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_1 a_2) → Eq L2 a_3)) % 10.76/11.11 False)) % 10.76/11.11 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.76/11.11 Or (Eq (odrl_rel a) False) % 10.76/11.11 (Or % 10.76/11.11 (Eq % 10.76/11.11 (And (And (And (permission a_1) (part_of a_1 a)) (cnt a_1 a_2 a_3)) % 10.76/11.11 (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_2 a_3) → Eq L2 a_1)) % 10.76/11.11 False) % 10.76/11.11 (Eq % 10.76/11.11 (And % 10.76/11.11 (And (And (no_right (skS.0 2 a a_2 a_3 a_4)) (part_of (skS.0 2 a a_2 a_3 a_4) a)) % 10.76/11.11 (cnt (skS.0 2 a a_2 a_3 a_4) a_2 a_3)) % 10.76/11.11 (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_2 a_3) → Eq M (skS.0 2 a a_2 a_3 a_4))) % 10.76/11.11 True)) % 10.76/11.11 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.76/11.11 Or (Eq (odrl_rel a) False) % 10.76/11.11 (Or % 10.76/11.11 (Eq % 10.76/11.11 (And % 10.76/11.11 (And (And (no_right (skS.0 2 a a_1 a_2 a_3)) (part_of (skS.0 2 a a_1 a_2 a_3) a)) % 10.76/11.11 (cnt (skS.0 2 a a_1 a_2 a_3) a_1 a_2)) % 10.76/11.11 (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_1 a_2) → Eq M (skS.0 2 a a_1 a_2 a_3))) % 10.76/11.11 True) % 10.76/11.11 (Or (Eq (And (And (permission a_4) (part_of a_4 a)) (cnt a_4 a_1 a_2)) False) % 10.76/11.11 (Eq (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_1 a_2) → Eq L2 a_4) False))) % 10.76/11.11 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.76/11.11 Or (Eq (odrl_rel a) False) % 10.76/11.11 (Or (Eq (And (And (permission a_1) (part_of a_1 a)) (cnt a_1 a_2 a_3)) False) % 10.76/11.11 (Or (Eq (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_2 a_3) → Eq L2 a_1) False) % 10.76/11.11 (Eq (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_2 a_3) → Eq M (skS.0 2 a a_2 a_3 a_4)) True))) % 10.76/11.11 Clause #61 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.76/11.11 Or (Eq (odrl_rel a) False) % 10.76/11.11 (Or (Eq (∀ (L2 : Iota), And (And (permission L2) (part_of L2 a)) (cnt L2 a_1 a_2) → Eq L2 a_3) False) % 10.76/11.11 (Or (Eq (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_1 a_2) → Eq M (skS.0 2 a a_1 a_2 a_4)) True) % 10.76/11.11 (Or (Eq (And (permission a_3) (part_of a_3 a)) False) (Eq (cnt a_3 a_1 a_2) False)))) % 10.76/11.11 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.76/11.11 Or (Eq (odrl_rel a) False) % 10.76/11.11 (Or (Eq (∀ (M : Iota), And (And (no_right M) (part_of M a)) (cnt M a_1 a_2) → Eq M (skS.0 2 a a_1 a_2 a_3)) True) % 10.76/11.11 (Or (Eq (And (permission a_4) (part_of a_4 a)) False) % 10.76/11.11 (Or (Eq (cnt a_4 a_1 a_2) False) % 10.76/11.11 (Eq % 10.76/11.11 (Not % 10.76/11.11 (And (And (permission (skS.0 3 a a_1 a_2 a_4 a_5)) (part_of (skS.0 3 a a_1 a_2 a_4 a_5) a)) % 10.76/11.11 (cnt (skS.0 3 a a_1 a_2 a_4 a_5) a_1 a_2) → % 10.76/11.11 Eq (skS.0 3 a a_1 a_2 a_4 a_5) a_4)) % 10.76/11.11 True)))) % 10.76/11.11 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.76/11.11 Or (Eq (odrl_rel a) False) % 10.76/11.11 (Or (Eq (And (permission a_1) (part_of a_1 a)) False) % 10.76/11.11 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.76/11.11 (Or % 10.76/11.11 (Eq % 10.86/11.13 (Not % 10.86/11.13 (And (And (permission (skS.0 3 a a_2 a_3 a_1 a_4)) (part_of (skS.0 3 a a_2 a_3 a_1 a_4) a)) % 10.86/11.13 (cnt (skS.0 3 a a_2 a_3 a_1 a_4) a_2 a_3) → % 10.86/11.13 Eq (skS.0 3 a a_2 a_3 a_1 a_4) a_1)) % 10.86/11.13 True) % 10.86/11.13 (Eq (And (And (no_right a_5) (part_of a_5 a)) (cnt a_5 a_2 a_3) → Eq a_5 (skS.0 2 a a_2 a_3 a_6)) True)))) % 10.86/11.13 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.13 Or (Eq (odrl_rel a) False) % 10.86/11.13 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.13 (Or % 10.86/11.13 (Eq % 10.86/11.13 (Not % 10.86/11.13 (And (And (permission (skS.0 3 a a_2 a_3 a_1 a_4)) (part_of (skS.0 3 a a_2 a_3 a_1 a_4) a)) % 10.86/11.13 (cnt (skS.0 3 a a_2 a_3 a_1 a_4) a_2 a_3) → % 10.86/11.13 Eq (skS.0 3 a a_2 a_3 a_1 a_4) a_1)) % 10.86/11.13 True) % 10.86/11.13 (Or (Eq (And (And (no_right a_5) (part_of a_5 a)) (cnt a_5 a_2 a_3) → Eq a_5 (skS.0 2 a a_2 a_3 a_6)) True) % 10.86/11.13 (Or (Eq (permission a_1) False) (Eq (part_of a_1 a) False))))) % 10.86/11.13 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.13 Or (Eq (odrl_rel a) False) % 10.86/11.13 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.13 (Or (Eq (And (And (no_right a_4) (part_of a_4 a)) (cnt a_4 a_2 a_3) → Eq a_4 (skS.0 2 a a_2 a_3 a_5)) True) % 10.86/11.13 (Or (Eq (permission a_1) False) % 10.86/11.13 (Or (Eq (part_of a_1 a) False) % 10.86/11.13 (Eq % 10.86/11.13 (And (And (permission (skS.0 3 a a_2 a_3 a_1 a_6)) (part_of (skS.0 3 a a_2 a_3 a_1 a_6) a)) % 10.86/11.13 (cnt (skS.0 3 a a_2 a_3 a_1 a_6) a_2 a_3) → % 10.86/11.13 Eq (skS.0 3 a a_2 a_3 a_1 a_6) a_1) % 10.86/11.13 False))))) % 10.86/11.13 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.13 Or (Eq (odrl_rel a) False) % 10.86/11.13 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.13 (Or (Eq (permission a_1) False) % 10.86/11.13 (Or (Eq (part_of a_1 a) False) % 10.86/11.13 (Or % 10.86/11.13 (Eq % 10.86/11.13 (And (And (permission (skS.0 3 a a_2 a_3 a_1 a_4)) (part_of (skS.0 3 a a_2 a_3 a_1 a_4) a)) % 10.86/11.13 (cnt (skS.0 3 a a_2 a_3 a_1 a_4) a_2 a_3) → % 10.86/11.13 Eq (skS.0 3 a a_2 a_3 a_1 a_4) a_1) % 10.86/11.13 False) % 10.86/11.13 (Or (Eq (And (And (no_right a_5) (part_of a_5 a)) (cnt a_5 a_2 a_3)) False) % 10.86/11.13 (Eq (Eq a_5 (skS.0 2 a a_2 a_3 a_6)) True)))))) % 10.86/11.13 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.13 Or (Eq (odrl_rel a) False) % 10.86/11.13 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.13 (Or (Eq (permission a_1) False) % 10.86/11.13 (Or (Eq (part_of a_1 a) False) % 10.86/11.13 (Or (Eq (And (And (no_right a_4) (part_of a_4 a)) (cnt a_4 a_2 a_3)) False) % 10.86/11.13 (Or (Eq (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) True) % 10.86/11.13 (Eq % 10.86/11.13 (And (And (permission (skS.0 3 a a_2 a_3 a_1 a_6)) (part_of (skS.0 3 a a_2 a_3 a_1 a_6) a)) % 10.86/11.13 (cnt (skS.0 3 a a_2 a_3 a_1 a_6) a_2 a_3)) % 10.86/11.13 True)))))) % 10.86/11.13 Clause #68 (by clausification #[66]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.13 Or (Eq (odrl_rel a) False) % 10.86/11.13 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.13 (Or (Eq (permission a_1) False) % 10.86/11.13 (Or (Eq (part_of a_1 a) False) % 10.86/11.13 (Or (Eq (And (And (no_right a_4) (part_of a_4 a)) (cnt a_4 a_2 a_3)) False) % 10.86/11.13 (Or (Eq (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) True) (Eq (Eq (skS.0 3 a a_2 a_3 a_1 a_6) a_1) False)))))) % 10.86/11.13 Clause #69 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.13 Or (Eq (odrl_rel a) False) % 10.86/11.13 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.13 (Or (Eq (permission a_1) False) % 10.86/11.13 (Or (Eq (part_of a_1 a) False) % 10.86/11.13 (Or (Eq (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) True) % 10.86/11.13 (Or % 10.86/11.13 (Eq % 10.86/11.13 (And (And (permission (skS.0 3 a a_2 a_3 a_1 a_6)) (part_of (skS.0 3 a a_2 a_3 a_1 a_6) a)) % 10.86/11.13 (cnt (skS.0 3 a a_2 a_3 a_1 a_6) a_2 a_3)) % 10.86/11.13 True) % 10.86/11.13 (Or (Eq (And (no_right a_4) (part_of a_4 a)) False) (Eq (cnt a_4 a_2 a_3) False))))))) % 10.86/11.13 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.13 Or (Eq (odrl_rel a) False) % 10.86/11.13 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.13 (Or (Eq (permission a_1) False) % 10.86/11.13 (Or (Eq (part_of a_1 a) False) % 10.86/11.13 (Or % 10.86/11.13 (Eq % 10.86/11.13 (And (And (permission (skS.0 3 a a_2 a_3 a_1 a_4)) (part_of (skS.0 3 a a_2 a_3 a_1 a_4) a)) % 10.86/11.16 (cnt (skS.0 3 a a_2 a_3 a_1 a_4) a_2 a_3)) % 10.86/11.16 True) % 10.86/11.16 (Or (Eq (And (no_right a_5) (part_of a_5 a)) False) % 10.86/11.16 (Or (Eq (cnt a_5 a_2 a_3) False) (Eq a_5 (skS.0 2 a a_2 a_3 a_6)))))))) % 10.86/11.16 Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.16 Or (Eq (odrl_rel a) False) % 10.86/11.16 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.16 (Or (Eq (permission a_1) False) % 10.86/11.16 (Or (Eq (part_of a_1 a) False) % 10.86/11.16 (Or (Eq (And (no_right a_4) (part_of a_4 a)) False) % 10.86/11.16 (Or (Eq (cnt a_4 a_2 a_3) False) % 10.86/11.16 (Or (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) (Eq (cnt (skS.0 3 a a_2 a_3 a_1 a_6) a_2 a_3) True))))))) % 10.86/11.16 Clause #72 (by clausification #[70]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.16 Or (Eq (odrl_rel a) False) % 10.86/11.16 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.16 (Or (Eq (permission a_1) False) % 10.86/11.16 (Or (Eq (part_of a_1 a) False) % 10.86/11.16 (Or (Eq (And (no_right a_4) (part_of a_4 a)) False) % 10.86/11.16 (Or (Eq (cnt a_4 a_2 a_3) False) % 10.86/11.16 (Or (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) % 10.86/11.16 (Eq (And (permission (skS.0 3 a a_2 a_3 a_1 a_6)) (part_of (skS.0 3 a a_2 a_3 a_1 a_6) a)) True))))))) % 10.86/11.16 Clause #73 (by clausification #[71]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.16 Or (Eq (odrl_rel a) False) % 10.86/11.16 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.16 (Or (Eq (permission a_1) False) % 10.86/11.16 (Or (Eq (part_of a_1 a) False) % 10.86/11.16 (Or (Eq (cnt a_4 a_2 a_3) False) % 10.86/11.16 (Or (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) % 10.86/11.16 (Or (Eq (cnt (skS.0 3 a a_2 a_3 a_1 a_6) a_2 a_3) True) % 10.86/11.16 (Or (Eq (no_right a_4) False) (Eq (part_of a_4 a) False)))))))) % 10.86/11.16 Clause #74 (by superposition #[73, 5]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.86/11.16 Or (Eq (cnt a a_1 a_2) False) % 10.86/11.16 (Or (Eq (permission a) False) % 10.86/11.16 (Or (Eq (part_of a rho1) False) % 10.86/11.16 (Or (Eq (cnt a_3 a_1 a_2) False) % 10.86/11.16 (Or (Eq a_3 (skS.0 2 rho1 a_1 a_2 a_4)) % 10.86/11.16 (Or (Eq (cnt (skS.0 3 rho1 a_1 a_2 a a_5) a_1 a_2) True) % 10.86/11.16 (Or (Eq (no_right a_3) False) (Or (Eq (part_of a_3 rho1) False) (Eq False True)))))))) % 10.86/11.16 Clause #273 (by clausification #[68]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.16 Or (Eq (odrl_rel a) False) % 10.86/11.16 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.16 (Or (Eq (permission a_1) False) % 10.86/11.16 (Or (Eq (part_of a_1 a) False) % 10.86/11.16 (Or (Eq (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) True) % 10.86/11.16 (Or (Eq (Eq (skS.0 3 a a_2 a_3 a_1 a_6) a_1) False) % 10.86/11.16 (Or (Eq (And (no_right a_4) (part_of a_4 a)) False) (Eq (cnt a_4 a_2 a_3) False))))))) % 10.86/11.16 Clause #274 (by clausification #[273]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.16 Or (Eq (odrl_rel a) False) % 10.86/11.16 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.16 (Or (Eq (permission a_1) False) % 10.86/11.16 (Or (Eq (part_of a_1 a) False) % 10.86/11.16 (Or (Eq (Eq (skS.0 3 a a_2 a_3 a_1 a_4) a_1) False) % 10.86/11.16 (Or (Eq (And (no_right a_5) (part_of a_5 a)) False) % 10.86/11.16 (Or (Eq (cnt a_5 a_2 a_3) False) (Eq a_5 (skS.0 2 a a_2 a_3 a_6)))))))) % 10.86/11.16 Clause #275 (by clausification #[274]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.16 Or (Eq (odrl_rel a) False) % 10.86/11.16 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.16 (Or (Eq (permission a_1) False) % 10.86/11.16 (Or (Eq (part_of a_1 a) False) % 10.86/11.16 (Or (Eq (And (no_right a_4) (part_of a_4 a)) False) % 10.86/11.16 (Or (Eq (cnt a_4 a_2 a_3) False) % 10.86/11.16 (Or (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) (Ne (skS.0 3 a a_2 a_3 a_1 a_6) a_1))))))) % 10.86/11.16 Clause #276 (by clausification #[275]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.16 Or (Eq (odrl_rel a) False) % 10.86/11.16 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.16 (Or (Eq (permission a_1) False) % 10.86/11.16 (Or (Eq (part_of a_1 a) False) % 10.86/11.16 (Or (Eq (cnt a_4 a_2 a_3) False) % 10.86/11.16 (Or (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) % 10.86/11.16 (Or (Ne (skS.0 3 a a_2 a_3 a_1 a_6) a_1) (Or (Eq (no_right a_4) False) (Eq (part_of a_4 a) False)))))))) % 10.86/11.16 Clause #277 (by superposition #[276, 5]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.86/11.16 Or (Eq (cnt a a_1 a_2) False) % 10.86/11.16 (Or (Eq (permission a) False) % 10.86/11.16 (Or (Eq (part_of a rho1) False) % 10.86/11.16 (Or (Eq (cnt a_3 a_1 a_2) False) % 10.86/11.18 (Or (Eq a_3 (skS.0 2 rho1 a_1 a_2 a_4)) % 10.86/11.18 (Or (Ne (skS.0 3 rho1 a_1 a_2 a a_5) a) % 10.86/11.18 (Or (Eq (no_right a_3) False) (Or (Eq (part_of a_3 rho1) False) (Eq False True)))))))) % 10.86/11.18 Clause #315 (by clausification #[72]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.18 Or (Eq (odrl_rel a) False) % 10.86/11.18 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.18 (Or (Eq (permission a_1) False) % 10.86/11.18 (Or (Eq (part_of a_1 a) False) % 10.86/11.18 (Or (Eq (cnt a_4 a_2 a_3) False) % 10.86/11.18 (Or (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) % 10.86/11.18 (Or (Eq (And (permission (skS.0 3 a a_2 a_3 a_1 a_6)) (part_of (skS.0 3 a a_2 a_3 a_1 a_6) a)) True) % 10.86/11.18 (Or (Eq (no_right a_4) False) (Eq (part_of a_4 a) False)))))))) % 10.86/11.18 Clause #316 (by clausification #[315]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.18 Or (Eq (odrl_rel a) False) % 10.86/11.18 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.18 (Or (Eq (permission a_1) False) % 10.86/11.18 (Or (Eq (part_of a_1 a) False) % 10.86/11.18 (Or (Eq (cnt a_4 a_2 a_3) False) % 10.86/11.18 (Or (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) % 10.86/11.18 (Or (Eq (no_right a_4) False) % 10.86/11.18 (Or (Eq (part_of a_4 a) False) (Eq (part_of (skS.0 3 a a_2 a_3 a_1 a_6) a) True)))))))) % 10.86/11.18 Clause #317 (by clausification #[315]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.86/11.18 Or (Eq (odrl_rel a) False) % 10.86/11.18 (Or (Eq (cnt a_1 a_2 a_3) False) % 10.86/11.18 (Or (Eq (permission a_1) False) % 10.86/11.18 (Or (Eq (part_of a_1 a) False) % 10.86/11.18 (Or (Eq (cnt a_4 a_2 a_3) False) % 10.86/11.18 (Or (Eq a_4 (skS.0 2 a a_2 a_3 a_5)) % 10.86/11.18 (Or (Eq (no_right a_4) False) % 10.86/11.18 (Or (Eq (part_of a_4 a) False) (Eq (permission (skS.0 3 a a_2 a_3 a_1 a_6)) True)))))))) % 10.86/11.18 Clause #318 (by superposition #[316, 5]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.86/11.18 Or (Eq (cnt a a_1 a_2) False) % 10.86/11.18 (Or (Eq (permission a) False) % 10.86/11.18 (Or (Eq (part_of a rho1) False) % 10.86/11.18 (Or (Eq (cnt a_3 a_1 a_2) False) % 10.86/11.18 (Or (Eq a_3 (skS.0 2 rho1 a_1 a_2 a_4)) % 10.86/11.18 (Or (Eq (no_right a_3) False) % 10.86/11.18 (Or (Eq (part_of a_3 rho1) False) % 10.86/11.18 (Or (Eq (part_of (skS.0 3 rho1 a_1 a_2 a a_5) rho1) True) (Eq False True)))))))) % 10.86/11.18 Clause #364 (by clausification #[74]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.86/11.18 Or (Eq (cnt a a_1 a_2) False) % 10.86/11.18 (Or (Eq (permission a) False) % 10.86/11.18 (Or (Eq (part_of a rho1) False) % 10.86/11.18 (Or (Eq (cnt a_3 a_1 a_2) False) % 10.86/11.18 (Or (Eq a_3 (skS.0 2 rho1 a_1 a_2 a_4)) % 10.86/11.18 (Or (Eq (cnt (skS.0 3 rho1 a_1 a_2 a a_5) a_1 a_2) True) % 10.86/11.18 (Or (Eq (no_right a_3) False) (Eq (part_of a_3 rho1) False))))))) % 10.86/11.18 Clause #367 (by superposition #[364, 12]): ∀ (a a_1 a_2 : Iota), % 10.86/11.18 Or (Eq (permission l) False) % 10.86/11.18 (Or (Eq (part_of l rho1) False) % 10.86/11.18 (Or (Eq (cnt a some_action some_target) False) % 10.86/11.18 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.86/11.18 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_2) some_action some_target) True) % 10.86/11.18 (Or (Eq (no_right a) False) (Or (Eq (part_of a rho1) False) (Eq False True))))))) % 10.86/11.18 Clause #574 (by clausification #[367]): ∀ (a a_1 a_2 : Iota), % 10.86/11.18 Or (Eq (permission l) False) % 10.86/11.18 (Or (Eq (part_of l rho1) False) % 10.86/11.18 (Or (Eq (cnt a some_action some_target) False) % 10.86/11.18 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.86/11.18 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_2) some_action some_target) True) % 10.86/11.18 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False)))))) % 10.86/11.18 Clause #575 (by forward demodulation #[574, 6]): ∀ (a a_1 a_2 : Iota), % 10.86/11.18 Or (Eq True False) % 10.86/11.18 (Or (Eq (part_of l rho1) False) % 10.86/11.18 (Or (Eq (cnt a some_action some_target) False) % 10.86/11.18 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.86/11.18 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_2) some_action some_target) True) % 10.86/11.18 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False)))))) % 10.86/11.18 Clause #576 (by clausification #[575]): ∀ (a a_1 a_2 : Iota), % 10.86/11.18 Or (Eq (part_of l rho1) False) % 10.86/11.18 (Or (Eq (cnt a some_action some_target) False) % 10.86/11.18 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.86/11.18 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_2) some_action some_target) True) % 10.95/11.20 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False))))) % 10.95/11.20 Clause #577 (by forward demodulation #[576, 9]): ∀ (a a_1 a_2 : Iota), % 10.95/11.20 Or (Eq True False) % 10.95/11.20 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.20 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_2) some_action some_target) True) % 10.95/11.20 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False))))) % 10.95/11.20 Clause #578 (by clausification #[577]): ∀ (a a_1 a_2 : Iota), % 10.95/11.20 Or (Eq (cnt a some_action some_target) False) % 10.95/11.20 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_2) some_action some_target) True) % 10.95/11.20 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False)))) % 10.95/11.20 Clause #579 (by superposition #[578, 14]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 (Or (Eq (no_right n2) False) (Or (Eq (part_of n2 rho1) False) (Eq False True)))) % 10.95/11.20 Clause #580 (by superposition #[578, 13]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 (Or (Eq (no_right n1) False) (Or (Eq (part_of n1 rho1) False) (Eq False True)))) % 10.95/11.20 Clause #600 (by clausification #[580]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 (Or (Eq (no_right n1) False) (Eq (part_of n1 rho1) False))) % 10.95/11.20 Clause #601 (by forward demodulation #[600, 7]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 (Or (Eq True False) (Eq (part_of n1 rho1) False))) % 10.95/11.20 Clause #602 (by clausification #[601]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 (Eq (part_of n1 rho1) False)) % 10.95/11.20 Clause #603 (by forward demodulation #[602, 10]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) (Eq True False)) % 10.95/11.20 Clause #604 (by clausification #[603]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 Clause #624 (by clausification #[579]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 (Or (Eq (no_right n2) False) (Eq (part_of n2 rho1) False))) % 10.95/11.20 Clause #625 (by forward demodulation #[624, 8]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 (Or (Eq True False) (Eq (part_of n2 rho1) False))) % 10.95/11.20 Clause #626 (by clausification #[625]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 (Eq (part_of n2 rho1) False)) % 10.95/11.20 Clause #627 (by forward demodulation #[626, 11]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) (Eq True False)) % 10.95/11.20 Clause #628 (by clausification #[627]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.20 (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.20 Clause #630 (by superposition #[628, 604]): ∀ (a a_1 : Iota), % 10.95/11.20 Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a) some_action some_target) True) % 10.95/11.20 (Or (Eq n1 n2) (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True)) % 10.95/11.23 Clause #646 (by forward contextual literal cutting #[630, 44]): ∀ (a a_1 : Iota), % 10.95/11.23 Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a) some_action some_target) True) % 10.95/11.23 (Eq (cnt (skS.0 3 rho1 some_action some_target l a_1) some_action some_target) True) % 10.95/11.23 Clause #662 (by equality factoring #[646]): ∀ (a : Iota), Or (Ne True True) (Eq (cnt (skS.0 3 rho1 some_action some_target l a) some_action some_target) True) % 10.95/11.23 Clause #663 (by clausification #[662]): ∀ (a : Iota), % 10.95/11.23 Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a) some_action some_target) True) % 10.95/11.23 (Or (Eq True False) (Eq True False)) % 10.95/11.23 Clause #665 (by clausification #[663]): ∀ (a : Iota), Or (Eq (cnt (skS.0 3 rho1 some_action some_target l a) some_action some_target) True) (Eq True False) % 10.95/11.23 Clause #666 (by clausification #[665]): ∀ (a : Iota), Eq (cnt (skS.0 3 rho1 some_action some_target l a) some_action some_target) True % 10.95/11.23 Clause #667 (by superposition #[666, 49]): ∀ (a : Iota), % 10.95/11.23 Or (Eq True False) % 10.95/11.23 (Or (Eq (skS.0 3 rho1 some_action some_target l a) l) % 10.95/11.23 (Or (Eq (permission (skS.0 3 rho1 some_action some_target l a)) False) % 10.95/11.23 (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) False))) % 10.95/11.23 Clause #683 (by clausification #[667]): ∀ (a : Iota), % 10.95/11.23 Or (Eq (skS.0 3 rho1 some_action some_target l a) l) % 10.95/11.23 (Or (Eq (permission (skS.0 3 rho1 some_action some_target l a)) False) % 10.95/11.23 (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) False)) % 10.95/11.23 Clause #860 (by clausification #[277]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.95/11.23 Or (Eq (cnt a a_1 a_2) False) % 10.95/11.23 (Or (Eq (permission a) False) % 10.95/11.23 (Or (Eq (part_of a rho1) False) % 10.95/11.23 (Or (Eq (cnt a_3 a_1 a_2) False) % 10.95/11.23 (Or (Eq a_3 (skS.0 2 rho1 a_1 a_2 a_4)) % 10.95/11.23 (Or (Ne (skS.0 3 rho1 a_1 a_2 a a_5) a) (Or (Eq (no_right a_3) False) (Eq (part_of a_3 rho1) False))))))) % 10.95/11.23 Clause #863 (by superposition #[860, 12]): ∀ (a a_1 a_2 : Iota), % 10.95/11.23 Or (Eq (permission l) False) % 10.95/11.23 (Or (Eq (part_of l rho1) False) % 10.95/11.23 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.23 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.23 (Or (Ne (skS.0 3 rho1 some_action some_target l a_2) l) % 10.95/11.23 (Or (Eq (no_right a) False) (Or (Eq (part_of a rho1) False) (Eq False True))))))) % 10.95/11.23 Clause #881 (by clausification #[863]): ∀ (a a_1 a_2 : Iota), % 10.95/11.23 Or (Eq (permission l) False) % 10.95/11.23 (Or (Eq (part_of l rho1) False) % 10.95/11.23 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.23 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.23 (Or (Ne (skS.0 3 rho1 some_action some_target l a_2) l) % 10.95/11.23 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False)))))) % 10.95/11.23 Clause #882 (by forward demodulation #[881, 6]): ∀ (a a_1 a_2 : Iota), % 10.95/11.23 Or (Eq True False) % 10.95/11.23 (Or (Eq (part_of l rho1) False) % 10.95/11.23 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.23 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.23 (Or (Ne (skS.0 3 rho1 some_action some_target l a_2) l) % 10.95/11.23 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False)))))) % 10.95/11.23 Clause #883 (by clausification #[882]): ∀ (a a_1 a_2 : Iota), % 10.95/11.23 Or (Eq (part_of l rho1) False) % 10.95/11.23 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.23 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.23 (Or (Ne (skS.0 3 rho1 some_action some_target l a_2) l) % 10.95/11.23 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False))))) % 10.95/11.23 Clause #884 (by forward demodulation #[883, 9]): ∀ (a a_1 a_2 : Iota), % 10.95/11.23 Or (Eq True False) % 10.95/11.23 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.23 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.23 (Or (Ne (skS.0 3 rho1 some_action some_target l a_2) l) % 10.95/11.23 (Or (Eq (no_right a) False) (Eq (part_of a rho1) False))))) % 10.95/11.23 Clause #885 (by clausification #[884]): ∀ (a a_1 a_2 : Iota), % 10.95/11.23 Or (Eq (cnt a some_action some_target) False) % 10.95/11.23 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.23 (Or (Ne (skS.0 3 rho1 some_action some_target l a_2) l) (Or (Eq (no_right a) False) (Eq (part_of a rho1) False)))) % 10.95/11.23 Clause #886 (by superposition #[885, 14]): ∀ (a a_1 : Iota), % 10.95/11.23 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) % 10.95/11.25 (Or (Eq (no_right n2) False) (Or (Eq (part_of n2 rho1) False) (Eq False True)))) % 10.95/11.25 Clause #887 (by superposition #[885, 13]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) % 10.95/11.25 (Or (Eq (no_right n1) False) (Or (Eq (part_of n1 rho1) False) (Eq False True)))) % 10.95/11.25 Clause #910 (by clausification #[887]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) (Or (Eq (no_right n1) False) (Eq (part_of n1 rho1) False))) % 10.95/11.25 Clause #911 (by forward demodulation #[910, 7]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) (Or (Eq True False) (Eq (part_of n1 rho1) False))) % 10.95/11.25 Clause #912 (by clausification #[911]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) (Eq (part_of n1 rho1) False)) % 10.95/11.25 Clause #913 (by forward demodulation #[912, 10]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) (Eq True False)) % 10.95/11.25 Clause #914 (by clausification #[913]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) (Ne (skS.0 3 rho1 some_action some_target l a_1) l) % 10.95/11.25 Clause #915 (by clausification #[886]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) (Or (Eq (no_right n2) False) (Eq (part_of n2 rho1) False))) % 10.95/11.25 Clause #916 (by forward demodulation #[915, 8]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) (Or (Eq True False) (Eq (part_of n2 rho1) False))) % 10.95/11.25 Clause #917 (by clausification #[916]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) (Eq (part_of n2 rho1) False)) % 10.95/11.25 Clause #918 (by forward demodulation #[917, 11]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.25 (Or (Ne (skS.0 3 rho1 some_action some_target l a_1) l) (Eq True False)) % 10.95/11.25 Clause #919 (by clausification #[918]): ∀ (a a_1 : Iota), % 10.95/11.25 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) (Ne (skS.0 3 rho1 some_action some_target l a_1) l) % 10.95/11.25 Clause #926 (by clausification #[318]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.95/11.25 Or (Eq (cnt a a_1 a_2) False) % 10.95/11.25 (Or (Eq (permission a) False) % 10.95/11.25 (Or (Eq (part_of a rho1) False) % 10.95/11.25 (Or (Eq (cnt a_3 a_1 a_2) False) % 10.95/11.25 (Or (Eq a_3 (skS.0 2 rho1 a_1 a_2 a_4)) % 10.95/11.25 (Or (Eq (no_right a_3) False) % 10.95/11.25 (Or (Eq (part_of a_3 rho1) False) (Eq (part_of (skS.0 3 rho1 a_1 a_2 a a_5) rho1) True))))))) % 10.95/11.25 Clause #929 (by superposition #[926, 12]): ∀ (a a_1 a_2 : Iota), % 10.95/11.25 Or (Eq (permission l) False) % 10.95/11.25 (Or (Eq (part_of l rho1) False) % 10.95/11.25 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.25 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.25 (Or (Eq (no_right a) False) % 10.95/11.25 (Or (Eq (part_of a rho1) False) % 10.95/11.25 (Or (Eq (part_of (skS.0 3 rho1 some_action some_target l a_2) rho1) True) (Eq False True))))))) % 10.95/11.25 Clause #949 (by clausification #[929]): ∀ (a a_1 a_2 : Iota), % 10.95/11.25 Or (Eq (permission l) False) % 10.95/11.25 (Or (Eq (part_of l rho1) False) % 10.95/11.25 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.25 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.25 (Or (Eq (no_right a) False) % 10.95/11.25 (Or (Eq (part_of a rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_2) rho1) True)))))) % 10.95/11.25 Clause #950 (by forward demodulation #[949, 6]): ∀ (a a_1 a_2 : Iota), % 10.95/11.25 Or (Eq True False) % 10.95/11.25 (Or (Eq (part_of l rho1) False) % 10.95/11.25 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.25 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.25 (Or (Eq (no_right a) False) % 10.95/11.25 (Or (Eq (part_of a rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_2) rho1) True)))))) % 10.95/11.27 Clause #951 (by clausification #[950]): ∀ (a a_1 a_2 : Iota), % 10.95/11.27 Or (Eq (part_of l rho1) False) % 10.95/11.27 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.27 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.27 (Or (Eq (no_right a) False) % 10.95/11.27 (Or (Eq (part_of a rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_2) rho1) True))))) % 10.95/11.27 Clause #952 (by forward demodulation #[951, 9]): ∀ (a a_1 a_2 : Iota), % 10.95/11.27 Or (Eq True False) % 10.95/11.27 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.27 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.27 (Or (Eq (no_right a) False) % 10.95/11.27 (Or (Eq (part_of a rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_2) rho1) True))))) % 10.95/11.27 Clause #953 (by clausification #[952]): ∀ (a a_1 a_2 : Iota), % 10.95/11.27 Or (Eq (cnt a some_action some_target) False) % 10.95/11.27 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.27 (Or (Eq (no_right a) False) % 10.95/11.27 (Or (Eq (part_of a rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_2) rho1) True)))) % 10.95/11.27 Clause #954 (by superposition #[953, 14]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq (no_right n2) False) % 10.95/11.27 (Or (Eq (part_of n2 rho1) False) % 10.95/11.27 (Or (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True) (Eq False True)))) % 10.95/11.27 Clause #955 (by superposition #[953, 13]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq (no_right n1) False) % 10.95/11.27 (Or (Eq (part_of n1 rho1) False) % 10.95/11.27 (Or (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True) (Eq False True)))) % 10.95/11.27 Clause #977 (by clausification #[955]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq (no_right n1) False) % 10.95/11.27 (Or (Eq (part_of n1 rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True))) % 10.95/11.27 Clause #978 (by forward demodulation #[977, 7]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq True False) % 10.95/11.27 (Or (Eq (part_of n1 rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True))) % 10.95/11.27 Clause #979 (by clausification #[978]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq (part_of n1 rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True)) % 10.95/11.27 Clause #980 (by forward demodulation #[979, 10]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq True False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True)) % 10.95/11.27 Clause #981 (by clausification #[980]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True) % 10.95/11.27 Clause #983 (by clausification #[954]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq (no_right n2) False) % 10.95/11.27 (Or (Eq (part_of n2 rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True))) % 10.95/11.27 Clause #984 (by forward demodulation #[983, 8]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq True False) % 10.95/11.27 (Or (Eq (part_of n2 rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True))) % 10.95/11.27 Clause #985 (by clausification #[984]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq (part_of n2 rho1) False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True)) % 10.95/11.27 Clause #986 (by forward demodulation #[985, 11]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Or (Eq True False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True)) % 10.95/11.27 Clause #987 (by clausification #[986]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 10.95/11.27 (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True) % 10.95/11.27 Clause #989 (by superposition #[987, 981]): ∀ (a a_1 : Iota), % 10.95/11.27 Or (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) True) % 10.95/11.29 (Or (Eq n1 n2) (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True)) % 10.95/11.29 Clause #990 (by forward contextual literal cutting #[989, 44]): ∀ (a a_1 : Iota), % 10.95/11.29 Or (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) True) % 10.95/11.29 (Eq (part_of (skS.0 3 rho1 some_action some_target l a_1) rho1) True) % 10.95/11.29 Clause #991 (by equality factoring #[990]): ∀ (a : Iota), Or (Ne True True) (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) True) % 10.95/11.29 Clause #995 (by clausification #[991]): ∀ (a : Iota), % 10.95/11.29 Or (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) True) (Or (Eq True False) (Eq True False)) % 10.95/11.29 Clause #997 (by clausification #[995]): ∀ (a : Iota), Or (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) True) (Eq True False) % 10.95/11.29 Clause #998 (by clausification #[997]): ∀ (a : Iota), Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) True % 10.95/11.29 Clause #1440 (by superposition #[317, 5]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.95/11.29 Or (Eq (cnt a a_1 a_2) False) % 10.95/11.29 (Or (Eq (permission a) False) % 10.95/11.29 (Or (Eq (part_of a rho1) False) % 10.95/11.29 (Or (Eq (cnt a_3 a_1 a_2) False) % 10.95/11.29 (Or (Eq a_3 (skS.0 2 rho1 a_1 a_2 a_4)) % 10.95/11.29 (Or (Eq (no_right a_3) False) % 10.95/11.29 (Or (Eq (part_of a_3 rho1) False) % 10.95/11.29 (Or (Eq (permission (skS.0 3 rho1 a_1 a_2 a a_5)) True) (Eq False True)))))))) % 10.95/11.29 Clause #1441 (by clausification #[1440]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.95/11.29 Or (Eq (cnt a a_1 a_2) False) % 10.95/11.29 (Or (Eq (permission a) False) % 10.95/11.29 (Or (Eq (part_of a rho1) False) % 10.95/11.29 (Or (Eq (cnt a_3 a_1 a_2) False) % 10.95/11.29 (Or (Eq a_3 (skS.0 2 rho1 a_1 a_2 a_4)) % 10.95/11.29 (Or (Eq (no_right a_3) False) % 10.95/11.29 (Or (Eq (part_of a_3 rho1) False) (Eq (permission (skS.0 3 rho1 a_1 a_2 a a_5)) True))))))) % 10.95/11.29 Clause #1444 (by superposition #[1441, 12]): ∀ (a a_1 a_2 : Iota), % 10.95/11.29 Or (Eq (permission l) False) % 10.95/11.29 (Or (Eq (part_of l rho1) False) % 10.95/11.29 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.29 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.29 (Or (Eq (no_right a) False) % 10.95/11.29 (Or (Eq (part_of a rho1) False) % 10.95/11.29 (Or (Eq (permission (skS.0 3 rho1 some_action some_target l a_2)) True) (Eq False True))))))) % 10.95/11.29 Clause #1464 (by clausification #[1444]): ∀ (a a_1 a_2 : Iota), % 10.95/11.29 Or (Eq (permission l) False) % 10.95/11.29 (Or (Eq (part_of l rho1) False) % 10.95/11.29 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.29 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.29 (Or (Eq (no_right a) False) % 10.95/11.29 (Or (Eq (part_of a rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_2)) True)))))) % 10.95/11.29 Clause #1465 (by forward demodulation #[1464, 6]): ∀ (a a_1 a_2 : Iota), % 10.95/11.29 Or (Eq True False) % 10.95/11.29 (Or (Eq (part_of l rho1) False) % 10.95/11.29 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.29 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.29 (Or (Eq (no_right a) False) % 10.95/11.29 (Or (Eq (part_of a rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_2)) True)))))) % 10.95/11.29 Clause #1466 (by clausification #[1465]): ∀ (a a_1 a_2 : Iota), % 10.95/11.29 Or (Eq (part_of l rho1) False) % 10.95/11.29 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.29 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.29 (Or (Eq (no_right a) False) % 10.95/11.29 (Or (Eq (part_of a rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_2)) True))))) % 10.95/11.29 Clause #1467 (by forward demodulation #[1466, 9]): ∀ (a a_1 a_2 : Iota), % 10.95/11.29 Or (Eq True False) % 10.95/11.29 (Or (Eq (cnt a some_action some_target) False) % 10.95/11.29 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.29 (Or (Eq (no_right a) False) % 10.95/11.29 (Or (Eq (part_of a rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_2)) True))))) % 10.95/11.29 Clause #1468 (by clausification #[1467]): ∀ (a a_1 a_2 : Iota), % 10.95/11.29 Or (Eq (cnt a some_action some_target) False) % 10.95/11.29 (Or (Eq a (skS.0 2 rho1 some_action some_target a_1)) % 10.95/11.29 (Or (Eq (no_right a) False) % 10.95/11.29 (Or (Eq (part_of a rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_2)) True)))) % 11.05/11.32 Clause #1469 (by superposition #[1468, 14]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq (no_right n2) False) % 11.05/11.32 (Or (Eq (part_of n2 rho1) False) % 11.05/11.32 (Or (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True) (Eq False True)))) % 11.05/11.32 Clause #1470 (by superposition #[1468, 13]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq (no_right n1) False) % 11.05/11.32 (Or (Eq (part_of n1 rho1) False) % 11.05/11.32 (Or (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True) (Eq False True)))) % 11.05/11.32 Clause #1492 (by clausification #[1470]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq (no_right n1) False) % 11.05/11.32 (Or (Eq (part_of n1 rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True))) % 11.05/11.32 Clause #1493 (by forward demodulation #[1492, 7]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq True False) % 11.05/11.32 (Or (Eq (part_of n1 rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True))) % 11.05/11.32 Clause #1494 (by clausification #[1493]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq (part_of n1 rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True)) % 11.05/11.32 Clause #1495 (by forward demodulation #[1494, 10]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq True False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True)) % 11.05/11.32 Clause #1496 (by clausification #[1495]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n1 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True) % 11.05/11.32 Clause #1499 (by clausification #[1469]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq (no_right n2) False) % 11.05/11.32 (Or (Eq (part_of n2 rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True))) % 11.05/11.32 Clause #1500 (by forward demodulation #[1499, 8]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq True False) % 11.05/11.32 (Or (Eq (part_of n2 rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True))) % 11.05/11.32 Clause #1501 (by clausification #[1500]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq (part_of n2 rho1) False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True)) % 11.05/11.32 Clause #1502 (by forward demodulation #[1501, 11]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Or (Eq True False) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True)) % 11.05/11.32 Clause #1503 (by clausification #[1502]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq n2 (skS.0 2 rho1 some_action some_target a)) % 11.05/11.32 (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True) % 11.05/11.32 Clause #1505 (by superposition #[1503, 1496]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq (permission (skS.0 3 rho1 some_action some_target l a)) True) % 11.05/11.32 (Or (Eq n1 n2) (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True)) % 11.05/11.32 Clause #1507 (by forward contextual literal cutting #[1505, 44]): ∀ (a a_1 : Iota), % 11.05/11.32 Or (Eq (permission (skS.0 3 rho1 some_action some_target l a)) True) % 11.05/11.32 (Eq (permission (skS.0 3 rho1 some_action some_target l a_1)) True) % 11.05/11.32 Clause #1509 (by equality factoring #[1507]): ∀ (a : Iota), Or (Ne True True) (Eq (permission (skS.0 3 rho1 some_action some_target l a)) True) % 11.05/11.32 Clause #1517 (by clausification #[1509]): ∀ (a : Iota), Or (Eq (permission (skS.0 3 rho1 some_action some_target l a)) True) (Or (Eq True False) (Eq True False)) % 11.05/11.32 Clause #1519 (by clausification #[1517]): ∀ (a : Iota), Or (Eq (permission (skS.0 3 rho1 some_action some_target l a)) True) (Eq True False) % 11.05/11.32 Clause #1520 (by clausification #[1519]): ∀ (a : Iota), Eq (permission (skS.0 3 rho1 some_action some_target l a)) True % 11.05/11.32 Clause #1521 (by backward demodulation #[1520, 683]): ∀ (a : Iota), % 11.05/11.32 Or (Eq (skS.0 3 rho1 some_action some_target l a) l) % 11.05/11.32 (Or (Eq True False) (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) False)) % 11.05/11.33 Clause #1522 (by clausification #[1521]): ∀ (a : Iota), % 11.05/11.33 Or (Eq (skS.0 3 rho1 some_action some_target l a) l) % 11.05/11.33 (Eq (part_of (skS.0 3 rho1 some_action some_target l a) rho1) False) % 11.05/11.33 Clause #1523 (by superposition #[1522, 998]): ∀ (a : Iota), Or (Eq (skS.0 3 rho1 some_action some_target l a) l) (Eq False True) % 11.05/11.33 Clause #1524 (by clausification #[1523]): ∀ (a : Iota), Eq (skS.0 3 rho1 some_action some_target l a) l % 11.05/11.33 Clause #1530 (by backward contextual literal cutting #[1524, 914]): ∀ (a : Iota), Eq n1 (skS.0 2 rho1 some_action some_target a) % 11.05/11.33 Clause #1531 (by backward contextual literal cutting #[1524, 919]): ∀ (a : Iota), Eq n2 (skS.0 2 rho1 some_action some_target a) % 11.05/11.33 Clause #1548 (by superposition #[1530, 1531]): Eq n1 n2 % 11.05/11.33 Clause #1549 (by forward contextual literal cutting #[1548, 44]): False % 11.05/11.33 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------