%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:22 AM UTC 2026 % Result : Theorem 76.96s 77.20s % Output : Proof 77.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0. % 0.00/0.05 % Command : duper %s % 0.11/0.38 % Computer : n007.cluster.edu % 0.11/0.38 % Model : x86_64 x86_64 % 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.38 % Memory : 8046.5625MB % 0.11/0.38 % OS : Linux 6.8.0-71-generic % 0.11/0.38 % CPULimit : 300 % 0.11/0.38 % WCLimit : 300 % 0.11/0.38 % DateTime : Mon Sep 7 13:48:56 UTC 2026 % 0.11/0.39 % CPUTime : % 76.96/77.20 SZS status Theorem for theBenchmark.p % 76.96/77.20 SZS output start Proof for theBenchmark.p % 76.96/77.20 Clause #11 (by assumption #[]): Eq (ssSingleRole (singleRoleEntry ssZBANF_WRK_INF_ED (authObj ssS_TCODE ssTCD ssME51N))) True % 76.96/77.20 Clause #12 (by assumption #[]): Eq (ssSingleRole (singleRoleEntry ssZBANF_WRK_INF_ED (authObj ssM_BANF_WRK ssACTVT np__1))) True % 76.96/77.20 Clause #15 (by assumption #[]): Eq (ssSingleRole (singleRoleEntry ssZBANF_WRK_INF_ED (authObj ssM_BANF_WRK ssWERKS ssINF))) True % 76.96/77.20 Clause #16 (by assumption #[]): Eq (ssSingleRole (singleRoleEntry ssZBANF_WRK_INF_ED (authObj ssM_BANF_BSA ssACTVT ssSTAR))) True % 76.96/77.20 Clause #17 (by assumption #[]): Eq (ssSingleRole (singleRoleEntry ssZBANF_WRK_INF_ED (authObj ssM_BANF_BSA ssBSART ssSTAR))) True % 76.96/77.20 Clause #18 (by assumption #[]): Eq (ssSingleRole (singleRoleEntry ssZBANF_WRK_INF_ED (authObj ssM_BANF_EKG ssACTVT ssSTAR))) True % 76.96/77.20 Clause #19 (by assumption #[]): Eq (ssSingleRole (singleRoleEntry ssZBANF_WRK_INF_ED (authObj ssM_BANF_EKG ssEKGRP ssI26))) True % 76.96/77.20 Clause #113 (by assumption #[]): Eq (ssHolds ssMUELLER ssZBANF_WRK_INF_ED) True % 76.96/77.20 Clause #117 (by assumption #[]): Eq (ssStandardPurchase ssNB) True % 76.96/77.20 Clause #136 (by assumption #[]): Eq (∀ (U V W X : Iota), ssUserProfile (userProfileEntry U (authObj V W X)) → ssAccess U (authObj V W X)) True % 76.96/77.20 Clause #137 (by assumption #[]): Eq (∀ (U V W X : Iota), ssUserProfile (userProfileEntry U (authObj V W ssSTAR)) → ssAccess U (authObj V W X)) True % 76.96/77.20 Clause #140 (by assumption #[]): Eq % 76.96/77.20 (∀ (U V W X Y Z X1 : Iota), % 76.96/77.20 Or % 76.96/77.20 (Or (And (ssProfile (profileEntry V (authObj Y Z X1))) (ssHolds U V)) % 76.96/77.20 (And (ssSingleRole (singleRoleEntry W (authObj Y Z X1))) (ssHolds U W))) % 76.96/77.20 (And (And (ssCompositeRole (compositeRoleEntry X W)) (ssSingleRole (singleRoleEntry W (authObj Y Z X1)))) % 76.96/77.20 (ssHolds U X)) → % 76.96/77.20 ssUserProfile (userProfileEntry U (authObj Y Z X1))) % 76.96/77.20 True % 76.96/77.20 Clause #141 (by assumption #[]): Eq % 76.96/77.20 (∀ (U V W X : Iota), % 76.96/77.20 And % 76.96/77.20 (And % 76.96/77.20 (And % 76.96/77.20 (And % 76.96/77.20 (And % 76.96/77.20 (And (ssAccess U (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess U (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.20 (ssAccess U (authObj ssM_BANF_WRK ssWERKS V))) % 76.96/77.20 (ssAccess U (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.20 (ssAccess U (authObj ssM_BANF_BSA ssBSART W))) % 76.96/77.20 (ssAccess U (authObj ssM_BANF_EKG ssACTVT np__1))) % 76.96/77.20 (ssAccess U (authObj ssM_BANF_EKG ssEKGRP X)) → % 76.96/77.20 ssAccess U ssME51N) % 76.96/77.20 True % 76.96/77.20 Clause #148 (by assumption #[]): Eq % 76.96/77.20 (∀ (U V W X Y Z X1 X2 X3 X4 : Iota), % 76.96/77.20 And % 76.96/77.20 (And % 76.96/77.20 (And (And (And (ssRequisition W Z X1 V X X2 Y X3 X4) (ssStandardPurchase W)) (ssAccess U ssME51N)) % 76.96/77.20 (ssAccess U (authObj ssM_BANF_WRK ssWERKS V))) % 76.96/77.20 (ssAccess U (authObj ssM_BANF_BSA ssBSART W))) % 76.96/77.20 (ssAccess U (authObj ssM_BANF_EKG ssEKGRP X)) → % 76.96/77.20 ssRequisitionCreated U W Z X1 V X X2 Y X3 X4) % 76.96/77.20 True % 76.96/77.20 Clause #154 (by assumption #[]): Eq % 76.96/77.20 (Not % 76.96/77.20 (Exists fun U => % 76.96/77.20 Exists fun V => % 76.96/77.20 Exists fun W => % 76.96/77.20 Exists fun X => % 76.96/77.20 Exists fun Y => % 76.96/77.20 Exists fun Z => % 76.96/77.20 Exists fun X1 => % 76.96/77.20 Exists fun X2 => % 76.96/77.20 Exists fun X3 => % 76.96/77.20 Exists fun X4 => % 76.96/77.20 ssRequisition Z X1 X2 V W X Y X3 X4 → % 76.96/77.20 And % 76.96/77.20 (And (ssRequisitionCreated U Z X1 X2 V W X Y X3 X4) % 76.96/77.20 (ssRequisitionReleased U Z X1 X2 V W X Y X3 X4)) % 76.96/77.20 (ssOrderCreated U Z X1 X2 V W X Y X3 X4))) % 76.96/77.20 True % 76.96/77.20 Clause #157 (by assumption #[]): Eq % 76.96/77.20 (Not % 76.96/77.20 (Exists fun U => % 76.96/77.20 Exists fun V => % 76.96/77.20 Exists fun W => % 76.96/77.20 Exists fun X => % 76.96/77.20 Exists fun Y => % 76.96/77.20 Exists fun Z => % 76.96/77.20 Exists fun X1 => % 76.96/77.20 Exists fun X2 => % 76.96/77.20 Exists fun X3 => % 76.96/77.20 ssRequisition Y Z X1 U ssINF W X X2 X3 → ssRequisitionCreated ssMUELLER Y Z X1 ssINF V W X X2 X3)) % 76.96/77.20 True % 76.96/77.20 Clause #187 (by clausification #[141]): ∀ (a : Iota), % 76.96/77.20 Eq % 76.96/77.20 (∀ (V W X : Iota), % 76.96/77.20 And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_WRK ssWERKS V))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssBSART W))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssEKGRP X)) → % 76.96/77.23 ssAccess a ssME51N) % 76.96/77.23 True % 76.96/77.23 Clause #188 (by clausification #[187]): ∀ (a a_1 : Iota), % 76.96/77.23 Eq % 76.96/77.23 (∀ (W X : Iota), % 76.96/77.23 And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssBSART W))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssEKGRP X)) → % 76.96/77.23 ssAccess a ssME51N) % 76.96/77.23 True % 76.96/77.23 Clause #189 (by clausification #[188]): ∀ (a a_1 a_2 : Iota), % 76.96/77.23 Eq % 76.96/77.23 (∀ (X : Iota), % 76.96/77.23 And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssBSART a_2))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssEKGRP X)) → % 76.96/77.23 ssAccess a ssME51N) % 76.96/77.23 True % 76.96/77.23 Clause #190 (by clausification #[189]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.23 Eq % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssBSART a_2))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_3)) → % 76.96/77.23 ssAccess a ssME51N) % 76.96/77.23 True % 76.96/77.23 Clause #191 (by clausification #[190]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.23 Or % 76.96/77.23 (Eq % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssBSART a_2))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_3))) % 76.96/77.23 False) % 76.96/77.23 (Eq (ssAccess a ssME51N) True) % 76.96/77.23 Clause #192 (by clausification #[191]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.23 Or (Eq (ssAccess a ssME51N) True) % 76.96/77.23 (Or % 76.96/77.23 (Eq % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_BSA ssBSART a_2))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1))) % 76.96/77.23 False) % 76.96/77.23 (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_3)) False)) % 76.96/77.23 Clause #193 (by clausification #[192]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.23 Or (Eq (ssAccess a ssME51N) True) % 76.96/77.23 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_1)) False) % 76.96/77.23 (Or % 76.96/77.23 (Eq % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And % 76.96/77.23 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.23 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_2))) % 76.96/77.28 (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.28 (ssAccess a (authObj ssM_BANF_BSA ssBSART a_3))) % 76.96/77.28 False) % 76.96/77.28 (Eq (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1)) False))) % 76.96/77.28 Clause #194 (by clausification #[193]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.28 Or (Eq (ssAccess a ssME51N) True) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_1)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 76.96/77.28 (Or % 76.96/77.28 (Eq % 76.96/77.28 (And % 76.96/77.28 (And % 76.96/77.28 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.28 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_2))) % 76.96/77.28 (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1))) % 76.96/77.28 False) % 76.96/77.28 (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_3)) False)))) % 76.96/77.28 Clause #195 (by clausification #[194]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.28 Or (Eq (ssAccess a ssME51N) True) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_1)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_2)) False) % 76.96/77.28 (Or % 76.96/77.28 (Eq % 76.96/77.28 (And % 76.96/77.28 (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.28 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_3))) % 76.96/77.28 False) % 76.96/77.28 (Eq (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1)) False))))) % 76.96/77.28 Clause #196 (by clausification #[195]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.28 Or (Eq (ssAccess a ssME51N) True) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_1)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_2)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1)) False) % 76.96/77.28 (Or % 76.96/77.28 (Eq (And (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1))) % 76.96/77.28 False) % 76.96/77.28 (Eq (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_3)) False)))))) % 76.96/77.28 Clause #197 (by clausification #[196]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.28 Or (Eq (ssAccess a ssME51N) True) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_1)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_2)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssACTVT np__1)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_3)) False) % 76.96/77.28 (Or (Eq (ssAccess a (authObj ssS_TCODE ssTCD ssME51N)) False) % 76.96/77.28 (Eq (ssAccess a (authObj ssM_BANF_WRK ssACTVT np__1)) False))))))) % 76.96/77.28 Clause #302 (by clausification #[137]): ∀ (a : Iota), % 76.96/77.28 Eq (∀ (V W X : Iota), ssUserProfile (userProfileEntry a (authObj V W ssSTAR)) → ssAccess a (authObj V W X)) True % 76.96/77.28 Clause #303 (by clausification #[302]): ∀ (a a_1 : Iota), % 76.96/77.28 Eq (∀ (W X : Iota), ssUserProfile (userProfileEntry a (authObj a_1 W ssSTAR)) → ssAccess a (authObj a_1 W X)) True % 76.96/77.28 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 : Iota), % 76.96/77.28 Eq (∀ (X : Iota), ssUserProfile (userProfileEntry a (authObj a_1 a_2 ssSTAR)) → ssAccess a (authObj a_1 a_2 X)) True % 76.96/77.28 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.28 Eq (ssUserProfile (userProfileEntry a (authObj a_1 a_2 ssSTAR)) → ssAccess a (authObj a_1 a_2 a_3)) True % 76.96/77.28 Clause #306 (by clausification #[305]): ∀ (a a_1 a_2 a_3 : Iota), % 76.96/77.28 Or (Eq (ssUserProfile (userProfileEntry a (authObj a_1 a_2 ssSTAR))) False) % 76.96/77.28 (Eq (ssAccess a (authObj a_1 a_2 a_3)) True) % 76.96/77.28 Clause #307 (by clausification #[136]): ∀ (a : Iota), % 76.96/77.28 Eq (∀ (V W X : Iota), ssUserProfile (userProfileEntry a (authObj V W X)) → ssAccess a (authObj V W X)) True % 76.96/77.28 Clause #308 (by clausification #[307]): ∀ (a a_1 : Iota), % 76.96/77.28 Eq (∀ (W X : Iota), ssUserProfile (userProfileEntry a (authObj a_1 W X)) → ssAccess a (authObj a_1 W X)) True % 76.96/77.28 Clause #309 (by clausification #[308]): ∀ (a a_1 a_2 : Iota), % 77.06/77.32 Eq (∀ (X : Iota), ssUserProfile (userProfileEntry a (authObj a_1 a_2 X)) → ssAccess a (authObj a_1 a_2 X)) True % 77.06/77.32 Clause #310 (by clausification #[309]): ∀ (a a_1 a_2 a_3 : Iota), % 77.06/77.32 Eq (ssUserProfile (userProfileEntry a (authObj a_1 a_2 a_3)) → ssAccess a (authObj a_1 a_2 a_3)) True % 77.06/77.32 Clause #311 (by clausification #[310]): ∀ (a a_1 a_2 a_3 : Iota), % 77.06/77.32 Or (Eq (ssUserProfile (userProfileEntry a (authObj a_1 a_2 a_3))) False) (Eq (ssAccess a (authObj a_1 a_2 a_3)) True) % 77.06/77.32 Clause #326 (by clausification #[140]): ∀ (a : Iota), % 77.06/77.32 Eq % 77.06/77.32 (∀ (V W X Y Z X1 : Iota), % 77.06/77.32 Or % 77.06/77.32 (Or (And (ssProfile (profileEntry V (authObj Y Z X1))) (ssHolds a V)) % 77.06/77.32 (And (ssSingleRole (singleRoleEntry W (authObj Y Z X1))) (ssHolds a W))) % 77.06/77.32 (And (And (ssCompositeRole (compositeRoleEntry X W)) (ssSingleRole (singleRoleEntry W (authObj Y Z X1)))) % 77.06/77.32 (ssHolds a X)) → % 77.06/77.32 ssUserProfile (userProfileEntry a (authObj Y Z X1))) % 77.06/77.32 True % 77.06/77.32 Clause #327 (by clausification #[326]): ∀ (a a_1 : Iota), % 77.06/77.32 Eq % 77.06/77.32 (∀ (W X Y Z X1 : Iota), % 77.06/77.32 Or % 77.06/77.32 (Or (And (ssProfile (profileEntry a (authObj Y Z X1))) (ssHolds a_1 a)) % 77.06/77.32 (And (ssSingleRole (singleRoleEntry W (authObj Y Z X1))) (ssHolds a_1 W))) % 77.06/77.32 (And (And (ssCompositeRole (compositeRoleEntry X W)) (ssSingleRole (singleRoleEntry W (authObj Y Z X1)))) % 77.06/77.32 (ssHolds a_1 X)) → % 77.06/77.32 ssUserProfile (userProfileEntry a_1 (authObj Y Z X1))) % 77.06/77.32 True % 77.06/77.32 Clause #328 (by clausification #[327]): ∀ (a a_1 a_2 : Iota), % 77.06/77.32 Eq % 77.06/77.32 (∀ (X Y Z X1 : Iota), % 77.06/77.32 Or % 77.06/77.32 (Or (And (ssProfile (profileEntry a (authObj Y Z X1))) (ssHolds a_1 a)) % 77.06/77.32 (And (ssSingleRole (singleRoleEntry a_2 (authObj Y Z X1))) (ssHolds a_1 a_2))) % 77.06/77.32 (And (And (ssCompositeRole (compositeRoleEntry X a_2)) (ssSingleRole (singleRoleEntry a_2 (authObj Y Z X1)))) % 77.06/77.32 (ssHolds a_1 X)) → % 77.06/77.32 ssUserProfile (userProfileEntry a_1 (authObj Y Z X1))) % 77.06/77.32 True % 77.06/77.32 Clause #329 (by clausification #[328]): ∀ (a a_1 a_2 a_3 : Iota), % 77.06/77.32 Eq % 77.06/77.32 (∀ (Y Z X1 : Iota), % 77.06/77.32 Or % 77.06/77.32 (Or (And (ssProfile (profileEntry a (authObj Y Z X1))) (ssHolds a_1 a)) % 77.06/77.32 (And (ssSingleRole (singleRoleEntry a_2 (authObj Y Z X1))) (ssHolds a_1 a_2))) % 77.06/77.32 (And % 77.06/77.32 (And (ssCompositeRole (compositeRoleEntry a_3 a_2)) (ssSingleRole (singleRoleEntry a_2 (authObj Y Z X1)))) % 77.06/77.32 (ssHolds a_1 a_3)) → % 77.06/77.32 ssUserProfile (userProfileEntry a_1 (authObj Y Z X1))) % 77.06/77.32 True % 77.06/77.32 Clause #330 (by clausification #[329]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 77.06/77.32 Eq % 77.06/77.32 (∀ (Z X1 : Iota), % 77.06/77.32 Or % 77.06/77.32 (Or (And (ssProfile (profileEntry a (authObj a_1 Z X1))) (ssHolds a_2 a)) % 77.06/77.32 (And (ssSingleRole (singleRoleEntry a_3 (authObj a_1 Z X1))) (ssHolds a_2 a_3))) % 77.06/77.32 (And % 77.06/77.32 (And (ssCompositeRole (compositeRoleEntry a_4 a_3)) (ssSingleRole (singleRoleEntry a_3 (authObj a_1 Z X1)))) % 77.06/77.32 (ssHolds a_2 a_4)) → % 77.06/77.32 ssUserProfile (userProfileEntry a_2 (authObj a_1 Z X1))) % 77.06/77.32 True % 77.06/77.32 Clause #331 (by clausification #[330]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 77.06/77.32 Eq % 77.06/77.32 (∀ (X1 : Iota), % 77.06/77.32 Or % 77.06/77.32 (Or (And (ssProfile (profileEntry a (authObj a_1 a_2 X1))) (ssHolds a_3 a)) % 77.06/77.32 (And (ssSingleRole (singleRoleEntry a_4 (authObj a_1 a_2 X1))) (ssHolds a_3 a_4))) % 77.06/77.32 (And % 77.06/77.32 (And (ssCompositeRole (compositeRoleEntry a_5 a_4)) % 77.06/77.32 (ssSingleRole (singleRoleEntry a_4 (authObj a_1 a_2 X1)))) % 77.06/77.32 (ssHolds a_3 a_5)) → % 77.06/77.32 ssUserProfile (userProfileEntry a_3 (authObj a_1 a_2 X1))) % 77.06/77.32 True % 77.06/77.32 Clause #332 (by clausification #[331]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.06/77.32 Eq % 77.06/77.32 (Or % 77.06/77.32 (Or (And (ssProfile (profileEntry a (authObj a_1 a_2 a_3))) (ssHolds a_4 a)) % 77.06/77.32 (And (ssSingleRole (singleRoleEntry a_5 (authObj a_1 a_2 a_3))) (ssHolds a_4 a_5))) % 77.06/77.32 (And % 77.06/77.32 (And (ssCompositeRole (compositeRoleEntry a_6 a_5)) % 77.06/77.32 (ssSingleRole (singleRoleEntry a_5 (authObj a_1 a_2 a_3)))) % 77.06/77.32 (ssHolds a_4 a_6)) → % 77.06/77.32 ssUserProfile (userProfileEntry a_4 (authObj a_1 a_2 a_3))) % 77.06/77.37 True % 77.06/77.37 Clause #333 (by clausification #[332]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.06/77.37 Or % 77.06/77.37 (Eq % 77.06/77.37 (Or % 77.06/77.37 (Or (And (ssProfile (profileEntry a (authObj a_1 a_2 a_3))) (ssHolds a_4 a)) % 77.06/77.37 (And (ssSingleRole (singleRoleEntry a_5 (authObj a_1 a_2 a_3))) (ssHolds a_4 a_5))) % 77.06/77.37 (And % 77.06/77.37 (And (ssCompositeRole (compositeRoleEntry a_6 a_5)) % 77.06/77.37 (ssSingleRole (singleRoleEntry a_5 (authObj a_1 a_2 a_3)))) % 77.06/77.37 (ssHolds a_4 a_6))) % 77.06/77.37 False) % 77.06/77.37 (Eq (ssUserProfile (userProfileEntry a_4 (authObj a_1 a_2 a_3))) True) % 77.06/77.37 Clause #335 (by clausification #[333]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 77.06/77.37 Or (Eq (ssUserProfile (userProfileEntry a (authObj a_1 a_2 a_3))) True) % 77.06/77.37 (Eq % 77.06/77.37 (Or (And (ssProfile (profileEntry a_4 (authObj a_1 a_2 a_3))) (ssHolds a a_4)) % 77.06/77.37 (And (ssSingleRole (singleRoleEntry a_5 (authObj a_1 a_2 a_3))) (ssHolds a a_5))) % 77.06/77.37 False) % 77.06/77.37 Clause #415 (by clausification #[148]): ∀ (a : Iota), % 77.06/77.37 Eq % 77.06/77.37 (∀ (V W X Y Z X1 X2 X3 X4 : Iota), % 77.06/77.37 And % 77.06/77.37 (And % 77.06/77.37 (And (And (And (ssRequisition W Z X1 V X X2 Y X3 X4) (ssStandardPurchase W)) (ssAccess a ssME51N)) % 77.06/77.37 (ssAccess a (authObj ssM_BANF_WRK ssWERKS V))) % 77.06/77.37 (ssAccess a (authObj ssM_BANF_BSA ssBSART W))) % 77.06/77.37 (ssAccess a (authObj ssM_BANF_EKG ssEKGRP X)) → % 77.06/77.37 ssRequisitionCreated a W Z X1 V X X2 Y X3 X4) % 77.06/77.37 True % 77.06/77.37 Clause #416 (by clausification #[415]): ∀ (a a_1 : Iota), % 77.06/77.37 Eq % 77.06/77.37 (∀ (W X Y Z X1 X2 X3 X4 : Iota), % 77.06/77.37 And % 77.06/77.37 (And % 77.06/77.37 (And (And (And (ssRequisition W Z X1 a X X2 Y X3 X4) (ssStandardPurchase W)) (ssAccess a_1 ssME51N)) % 77.06/77.37 (ssAccess a_1 (authObj ssM_BANF_WRK ssWERKS a))) % 77.06/77.37 (ssAccess a_1 (authObj ssM_BANF_BSA ssBSART W))) % 77.06/77.37 (ssAccess a_1 (authObj ssM_BANF_EKG ssEKGRP X)) → % 77.06/77.37 ssRequisitionCreated a_1 W Z X1 a X X2 Y X3 X4) % 77.06/77.37 True % 77.06/77.37 Clause #417 (by clausification #[416]): ∀ (a a_1 a_2 : Iota), % 77.06/77.37 Eq % 77.06/77.37 (∀ (X Y Z X1 X2 X3 X4 : Iota), % 77.06/77.37 And % 77.06/77.37 (And % 77.06/77.37 (And (And (And (ssRequisition a Z X1 a_1 X X2 Y X3 X4) (ssStandardPurchase a)) (ssAccess a_2 ssME51N)) % 77.06/77.37 (ssAccess a_2 (authObj ssM_BANF_WRK ssWERKS a_1))) % 77.06/77.37 (ssAccess a_2 (authObj ssM_BANF_BSA ssBSART a))) % 77.06/77.37 (ssAccess a_2 (authObj ssM_BANF_EKG ssEKGRP X)) → % 77.06/77.37 ssRequisitionCreated a_2 a Z X1 a_1 X X2 Y X3 X4) % 77.06/77.37 True % 77.06/77.37 Clause #418 (by clausification #[417]): ∀ (a a_1 a_2 a_3 : Iota), % 77.06/77.37 Eq % 77.06/77.37 (∀ (Y Z X1 X2 X3 X4 : Iota), % 77.06/77.37 And % 77.06/77.37 (And % 77.06/77.37 (And (And (And (ssRequisition a Z X1 a_1 a_2 X2 Y X3 X4) (ssStandardPurchase a)) (ssAccess a_3 ssME51N)) % 77.06/77.37 (ssAccess a_3 (authObj ssM_BANF_WRK ssWERKS a_1))) % 77.06/77.37 (ssAccess a_3 (authObj ssM_BANF_BSA ssBSART a))) % 77.06/77.37 (ssAccess a_3 (authObj ssM_BANF_EKG ssEKGRP a_2)) → % 77.06/77.37 ssRequisitionCreated a_3 a Z X1 a_1 a_2 X2 Y X3 X4) % 77.06/77.37 True % 77.06/77.37 Clause #419 (by clausification #[418]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 77.06/77.37 Eq % 77.06/77.37 (∀ (Z X1 X2 X3 X4 : Iota), % 77.06/77.37 And % 77.06/77.37 (And % 77.06/77.37 (And (And (And (ssRequisition a Z X1 a_1 a_2 X2 a_3 X3 X4) (ssStandardPurchase a)) (ssAccess a_4 ssME51N)) % 77.06/77.37 (ssAccess a_4 (authObj ssM_BANF_WRK ssWERKS a_1))) % 77.06/77.37 (ssAccess a_4 (authObj ssM_BANF_BSA ssBSART a))) % 77.06/77.37 (ssAccess a_4 (authObj ssM_BANF_EKG ssEKGRP a_2)) → % 77.06/77.37 ssRequisitionCreated a_4 a Z X1 a_1 a_2 X2 a_3 X3 X4) % 77.06/77.37 True % 77.06/77.37 Clause #420 (by clausification #[419]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 77.06/77.37 Eq % 77.06/77.37 (∀ (X1 X2 X3 X4 : Iota), % 77.06/77.37 And % 77.06/77.37 (And % 77.06/77.37 (And (And (And (ssRequisition a a_1 X1 a_2 a_3 X2 a_4 X3 X4) (ssStandardPurchase a)) (ssAccess a_5 ssME51N)) % 77.06/77.37 (ssAccess a_5 (authObj ssM_BANF_WRK ssWERKS a_2))) % 77.06/77.37 (ssAccess a_5 (authObj ssM_BANF_BSA ssBSART a))) % 77.06/77.37 (ssAccess a_5 (authObj ssM_BANF_EKG ssEKGRP a_3)) → % 77.06/77.37 ssRequisitionCreated a_5 a a_1 X1 a_2 a_3 X2 a_4 X3 X4) % 77.06/77.37 True % 77.06/77.37 Clause #421 (by clausification #[420]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.06/77.37 Eq % 77.06/77.37 (∀ (X2 X3 X4 : Iota), % 77.06/77.37 And % 77.06/77.37 (And % 77.06/77.37 (And % 77.16/77.41 (And (And (ssRequisition a a_1 a_2 a_3 a_4 X2 a_5 X3 X4) (ssStandardPurchase a)) (ssAccess a_6 ssME51N)) % 77.16/77.41 (ssAccess a_6 (authObj ssM_BANF_WRK ssWERKS a_3))) % 77.16/77.41 (ssAccess a_6 (authObj ssM_BANF_BSA ssBSART a))) % 77.16/77.41 (ssAccess a_6 (authObj ssM_BANF_EKG ssEKGRP a_4)) → % 77.16/77.41 ssRequisitionCreated a_6 a a_1 a_2 a_3 a_4 X2 a_5 X3 X4) % 77.16/77.41 True % 77.16/77.41 Clause #422 (by clausification #[421]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 77.16/77.41 Eq % 77.16/77.41 (∀ (X3 X4 : Iota), % 77.16/77.41 And % 77.16/77.41 (And % 77.16/77.41 (And % 77.16/77.41 (And (And (ssRequisition a a_1 a_2 a_3 a_4 a_5 a_6 X3 X4) (ssStandardPurchase a)) (ssAccess a_7 ssME51N)) % 77.16/77.41 (ssAccess a_7 (authObj ssM_BANF_WRK ssWERKS a_3))) % 77.16/77.41 (ssAccess a_7 (authObj ssM_BANF_BSA ssBSART a))) % 77.16/77.41 (ssAccess a_7 (authObj ssM_BANF_EKG ssEKGRP a_4)) → % 77.16/77.41 ssRequisitionCreated a_7 a a_1 a_2 a_3 a_4 a_5 a_6 X3 X4) % 77.16/77.41 True % 77.16/77.41 Clause #423 (by clausification #[422]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 77.16/77.41 Eq % 77.16/77.41 (∀ (X4 : Iota), % 77.16/77.41 And % 77.16/77.41 (And % 77.16/77.41 (And % 77.16/77.41 (And (And (ssRequisition a a_1 a_2 a_3 a_4 a_5 a_6 a_7 X4) (ssStandardPurchase a)) (ssAccess a_8 ssME51N)) % 77.16/77.41 (ssAccess a_8 (authObj ssM_BANF_WRK ssWERKS a_3))) % 77.16/77.41 (ssAccess a_8 (authObj ssM_BANF_BSA ssBSART a))) % 77.16/77.41 (ssAccess a_8 (authObj ssM_BANF_EKG ssEKGRP a_4)) → % 77.16/77.41 ssRequisitionCreated a_8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 X4) % 77.16/77.41 True % 77.16/77.41 Clause #424 (by clausification #[423]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.41 Eq % 77.16/77.41 (And % 77.16/77.41 (And % 77.16/77.41 (And % 77.16/77.41 (And (And (ssRequisition a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (ssStandardPurchase a)) (ssAccess a_9 ssME51N)) % 77.16/77.41 (ssAccess a_9 (authObj ssM_BANF_WRK ssWERKS a_3))) % 77.16/77.41 (ssAccess a_9 (authObj ssM_BANF_BSA ssBSART a))) % 77.16/77.41 (ssAccess a_9 (authObj ssM_BANF_EKG ssEKGRP a_4)) → % 77.16/77.41 ssRequisitionCreated a_9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 77.16/77.41 True % 77.16/77.41 Clause #425 (by clausification #[424]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.41 Or % 77.16/77.41 (Eq % 77.16/77.41 (And % 77.16/77.41 (And % 77.16/77.41 (And % 77.16/77.41 (And (And (ssRequisition a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (ssStandardPurchase a)) (ssAccess a_9 ssME51N)) % 77.16/77.41 (ssAccess a_9 (authObj ssM_BANF_WRK ssWERKS a_3))) % 77.16/77.41 (ssAccess a_9 (authObj ssM_BANF_BSA ssBSART a))) % 77.16/77.41 (ssAccess a_9 (authObj ssM_BANF_EKG ssEKGRP a_4))) % 77.16/77.41 False) % 77.16/77.41 (Eq (ssRequisitionCreated a_9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) True) % 77.16/77.41 Clause #426 (by clausification #[425]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.41 Or (Eq (ssRequisitionCreated a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) True) % 77.16/77.41 (Or % 77.16/77.41 (Eq % 77.16/77.41 (And % 77.16/77.41 (And % 77.16/77.41 (And (And (ssRequisition a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (ssStandardPurchase a_1)) % 77.16/77.41 (ssAccess a ssME51N)) % 77.16/77.41 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_4))) % 77.16/77.41 (ssAccess a (authObj ssM_BANF_BSA ssBSART a_1))) % 77.16/77.41 False) % 77.16/77.41 (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_5)) False)) % 77.16/77.41 Clause #427 (by clausification #[426]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.41 Or (Eq (ssRequisitionCreated a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) True) % 77.16/77.41 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_5)) False) % 77.16/77.41 (Or % 77.16/77.41 (Eq % 77.16/77.41 (And % 77.16/77.41 (And (And (ssRequisition a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (ssStandardPurchase a_1)) % 77.16/77.41 (ssAccess a ssME51N)) % 77.16/77.41 (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_4))) % 77.16/77.41 False) % 77.16/77.41 (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_1)) False))) % 77.16/77.41 Clause #428 (by clausification #[427]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.41 Or (Eq (ssRequisitionCreated a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) True) % 77.16/77.41 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_5)) False) % 77.16/77.41 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_1)) False) % 77.16/77.41 (Or % 77.16/77.41 (Eq % 77.16/77.41 (And (And (ssRequisition a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (ssStandardPurchase a_1)) % 77.16/77.41 (ssAccess a ssME51N)) % 77.16/77.45 False) % 77.16/77.45 (Eq (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_4)) False)))) % 77.16/77.45 Clause #429 (by clausification #[428]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.45 Or (Eq (ssRequisitionCreated a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) True) % 77.16/77.45 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_5)) False) % 77.16/77.45 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_1)) False) % 77.16/77.45 (Or (Eq (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_4)) False) % 77.16/77.45 (Or (Eq (And (ssRequisition a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (ssStandardPurchase a_1)) False) % 77.16/77.45 (Eq (ssAccess a ssME51N) False))))) % 77.16/77.45 Clause #430 (by clausification #[429]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.45 Or (Eq (ssRequisitionCreated a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) True) % 77.16/77.45 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_5)) False) % 77.16/77.45 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_1)) False) % 77.16/77.45 (Or (Eq (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_4)) False) % 77.16/77.45 (Or (Eq (ssAccess a ssME51N) False) % 77.16/77.45 (Or (Eq (ssRequisition a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) False) (Eq (ssStandardPurchase a_1) False)))))) % 77.16/77.45 Clause #609 (by clausification #[154]): Eq % 77.16/77.45 (Exists fun U => % 77.16/77.45 Exists fun V => % 77.16/77.45 Exists fun W => % 77.16/77.45 Exists fun X => % 77.16/77.45 Exists fun Y => % 77.16/77.45 Exists fun Z => % 77.16/77.45 Exists fun X1 => % 77.16/77.45 Exists fun X2 => % 77.16/77.45 Exists fun X3 => % 77.16/77.45 Exists fun X4 => % 77.16/77.45 ssRequisition Z X1 X2 V W X Y X3 X4 → % 77.16/77.45 And % 77.16/77.45 (And (ssRequisitionCreated U Z X1 X2 V W X Y X3 X4) % 77.16/77.45 (ssRequisitionReleased U Z X1 X2 V W X Y X3 X4)) % 77.16/77.45 (ssOrderCreated U Z X1 X2 V W X Y X3 X4)) % 77.16/77.45 False % 77.16/77.45 Clause #610 (by clausification #[609]): ∀ (a : Iota), % 77.16/77.45 Eq % 77.16/77.45 (Exists fun V => % 77.16/77.45 Exists fun W => % 77.16/77.45 Exists fun X => % 77.16/77.45 Exists fun Y => % 77.16/77.45 Exists fun Z => % 77.16/77.45 Exists fun X1 => % 77.16/77.45 Exists fun X2 => % 77.16/77.45 Exists fun X3 => % 77.16/77.45 Exists fun X4 => % 77.16/77.45 ssRequisition Z X1 X2 V W X Y X3 X4 → % 77.16/77.45 And % 77.16/77.45 (And (ssRequisitionCreated a Z X1 X2 V W X Y X3 X4) % 77.16/77.45 (ssRequisitionReleased a Z X1 X2 V W X Y X3 X4)) % 77.16/77.45 (ssOrderCreated a Z X1 X2 V W X Y X3 X4)) % 77.16/77.45 False % 77.16/77.45 Clause #611 (by clausification #[610]): ∀ (a a_1 : Iota), % 77.16/77.45 Eq % 77.16/77.45 (Exists fun W => % 77.16/77.45 Exists fun X => % 77.16/77.45 Exists fun Y => % 77.16/77.45 Exists fun Z => % 77.16/77.45 Exists fun X1 => % 77.16/77.45 Exists fun X2 => % 77.16/77.45 Exists fun X3 => % 77.16/77.45 Exists fun X4 => % 77.16/77.45 ssRequisition Z X1 X2 a W X Y X3 X4 → % 77.16/77.45 And % 77.16/77.45 (And (ssRequisitionCreated a_1 Z X1 X2 a W X Y X3 X4) % 77.16/77.45 (ssRequisitionReleased a_1 Z X1 X2 a W X Y X3 X4)) % 77.16/77.45 (ssOrderCreated a_1 Z X1 X2 a W X Y X3 X4)) % 77.16/77.45 False % 77.16/77.45 Clause #612 (by clausification #[611]): ∀ (a a_1 a_2 : Iota), % 77.16/77.45 Eq % 77.16/77.45 (Exists fun X => % 77.16/77.45 Exists fun Y => % 77.16/77.45 Exists fun Z => % 77.16/77.45 Exists fun X1 => % 77.16/77.45 Exists fun X2 => % 77.16/77.45 Exists fun X3 => % 77.16/77.45 Exists fun X4 => % 77.16/77.45 ssRequisition Z X1 X2 a a_1 X Y X3 X4 → % 77.16/77.45 And % 77.16/77.45 (And (ssRequisitionCreated a_2 Z X1 X2 a a_1 X Y X3 X4) % 77.16/77.45 (ssRequisitionReleased a_2 Z X1 X2 a a_1 X Y X3 X4)) % 77.16/77.45 (ssOrderCreated a_2 Z X1 X2 a a_1 X Y X3 X4)) % 77.16/77.45 False % 77.16/77.45 Clause #613 (by clausification #[612]): ∀ (a a_1 a_2 a_3 : Iota), % 77.16/77.45 Eq % 77.16/77.45 (Exists fun Y => % 77.16/77.45 Exists fun Z => % 77.16/77.45 Exists fun X1 => % 77.16/77.45 Exists fun X2 => % 77.16/77.45 Exists fun X3 => % 77.16/77.45 Exists fun X4 => % 77.16/77.45 ssRequisition Z X1 X2 a a_1 a_2 Y X3 X4 → % 77.16/77.45 And % 77.16/77.45 (And (ssRequisitionCreated a_3 Z X1 X2 a a_1 a_2 Y X3 X4) % 77.16/77.45 (ssRequisitionReleased a_3 Z X1 X2 a a_1 a_2 Y X3 X4)) % 77.16/77.45 (ssOrderCreated a_3 Z X1 X2 a a_1 a_2 Y X3 X4)) % 77.16/77.50 False % 77.16/77.50 Clause #614 (by clausification #[613]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 77.16/77.50 Eq % 77.16/77.50 (Exists fun Z => % 77.16/77.50 Exists fun X1 => % 77.16/77.50 Exists fun X2 => % 77.16/77.50 Exists fun X3 => % 77.16/77.50 Exists fun X4 => % 77.16/77.50 ssRequisition Z X1 X2 a a_1 a_2 a_3 X3 X4 → % 77.16/77.50 And % 77.16/77.50 (And (ssRequisitionCreated a_4 Z X1 X2 a a_1 a_2 a_3 X3 X4) % 77.16/77.50 (ssRequisitionReleased a_4 Z X1 X2 a a_1 a_2 a_3 X3 X4)) % 77.16/77.50 (ssOrderCreated a_4 Z X1 X2 a a_1 a_2 a_3 X3 X4)) % 77.16/77.50 False % 77.16/77.50 Clause #615 (by clausification #[614]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 77.16/77.50 Eq % 77.16/77.50 (Exists fun X1 => % 77.16/77.50 Exists fun X2 => % 77.16/77.50 Exists fun X3 => % 77.16/77.50 Exists fun X4 => % 77.16/77.50 ssRequisition a X1 X2 a_1 a_2 a_3 a_4 X3 X4 → % 77.16/77.50 And % 77.16/77.50 (And (ssRequisitionCreated a_5 a X1 X2 a_1 a_2 a_3 a_4 X3 X4) % 77.16/77.50 (ssRequisitionReleased a_5 a X1 X2 a_1 a_2 a_3 a_4 X3 X4)) % 77.16/77.50 (ssOrderCreated a_5 a X1 X2 a_1 a_2 a_3 a_4 X3 X4)) % 77.16/77.50 False % 77.16/77.50 Clause #616 (by clausification #[615]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.16/77.50 Eq % 77.16/77.50 (Exists fun X2 => % 77.16/77.50 Exists fun X3 => % 77.16/77.50 Exists fun X4 => % 77.16/77.50 ssRequisition a a_1 X2 a_2 a_3 a_4 a_5 X3 X4 → % 77.16/77.50 And % 77.16/77.50 (And (ssRequisitionCreated a_6 a a_1 X2 a_2 a_3 a_4 a_5 X3 X4) % 77.16/77.50 (ssRequisitionReleased a_6 a a_1 X2 a_2 a_3 a_4 a_5 X3 X4)) % 77.16/77.50 (ssOrderCreated a_6 a a_1 X2 a_2 a_3 a_4 a_5 X3 X4)) % 77.16/77.50 False % 77.16/77.50 Clause #617 (by clausification #[616]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 77.16/77.50 Eq % 77.16/77.50 (Exists fun X3 => % 77.16/77.50 Exists fun X4 => % 77.16/77.50 ssRequisition a a_1 a_2 a_3 a_4 a_5 a_6 X3 X4 → % 77.16/77.50 And % 77.16/77.50 (And (ssRequisitionCreated a_7 a a_1 a_2 a_3 a_4 a_5 a_6 X3 X4) % 77.16/77.50 (ssRequisitionReleased a_7 a a_1 a_2 a_3 a_4 a_5 a_6 X3 X4)) % 77.16/77.50 (ssOrderCreated a_7 a a_1 a_2 a_3 a_4 a_5 a_6 X3 X4)) % 77.16/77.50 False % 77.16/77.50 Clause #618 (by clausification #[617]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 77.16/77.50 Eq % 77.16/77.50 (Exists fun X4 => % 77.16/77.50 ssRequisition a a_1 a_2 a_3 a_4 a_5 a_6 a_7 X4 → % 77.16/77.50 And % 77.16/77.50 (And (ssRequisitionCreated a_8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 X4) % 77.16/77.50 (ssRequisitionReleased a_8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 X4)) % 77.16/77.50 (ssOrderCreated a_8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 X4)) % 77.16/77.50 False % 77.16/77.50 Clause #619 (by clausification #[618]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.50 Eq % 77.16/77.50 (ssRequisition a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 → % 77.16/77.50 And % 77.16/77.50 (And (ssRequisitionCreated a_9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 77.16/77.50 (ssRequisitionReleased a_9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 77.16/77.50 (ssOrderCreated a_9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 77.16/77.50 False % 77.16/77.50 Clause #620 (by clausification #[619]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), Eq (ssRequisition a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) True % 77.16/77.50 Clause #622 (by backward demodulation #[620, 430]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.16/77.50 Or (Eq (ssRequisitionCreated a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) True) % 77.16/77.50 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_5)) False) % 77.16/77.50 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_1)) False) % 77.16/77.50 (Or (Eq (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_4)) False) % 77.16/77.50 (Or (Eq (ssAccess a ssME51N) False) (Or (Eq True False) (Eq (ssStandardPurchase a_1) False)))))) % 77.16/77.50 Clause #669 (by clausification #[157]): Eq % 77.16/77.50 (Exists fun U => % 77.16/77.50 Exists fun V => % 77.16/77.50 Exists fun W => % 77.16/77.50 Exists fun X => % 77.16/77.50 Exists fun Y => % 77.16/77.50 Exists fun Z => % 77.16/77.50 Exists fun X1 => % 77.16/77.50 Exists fun X2 => % 77.16/77.50 Exists fun X3 => % 77.16/77.50 ssRequisition Y Z X1 U ssINF W X X2 X3 → ssRequisitionCreated ssMUELLER Y Z X1 ssINF V W X X2 X3) % 77.16/77.50 False % 77.16/77.50 Clause #670 (by clausification #[669]): ∀ (a : Iota), % 77.16/77.50 Eq % 77.16/77.50 (Exists fun V => % 77.16/77.50 Exists fun W => % 77.16/77.50 Exists fun X => % 77.16/77.50 Exists fun Y => % 77.16/77.50 Exists fun Z => % 77.16/77.50 Exists fun X1 => % 77.16/77.50 Exists fun X2 => % 77.16/77.50 Exists fun X3 => % 77.16/77.50 ssRequisition Y Z X1 a ssINF W X X2 X3 → ssRequisitionCreated ssMUELLER Y Z X1 ssINF V W X X2 X3) % 77.26/77.54 False % 77.26/77.54 Clause #671 (by clausification #[670]): ∀ (a a_1 : Iota), % 77.26/77.54 Eq % 77.26/77.54 (Exists fun W => % 77.26/77.54 Exists fun X => % 77.26/77.54 Exists fun Y => % 77.26/77.54 Exists fun Z => % 77.26/77.54 Exists fun X1 => % 77.26/77.54 Exists fun X2 => % 77.26/77.54 Exists fun X3 => % 77.26/77.54 ssRequisition Y Z X1 a ssINF W X X2 X3 → ssRequisitionCreated ssMUELLER Y Z X1 ssINF a_1 W X X2 X3) % 77.26/77.54 False % 77.26/77.54 Clause #672 (by clausification #[671]): ∀ (a a_1 a_2 : Iota), % 77.26/77.54 Eq % 77.26/77.54 (Exists fun X => % 77.26/77.54 Exists fun Y => % 77.26/77.54 Exists fun Z => % 77.26/77.54 Exists fun X1 => % 77.26/77.54 Exists fun X2 => % 77.26/77.54 Exists fun X3 => % 77.26/77.54 ssRequisition Y Z X1 a ssINF a_1 X X2 X3 → ssRequisitionCreated ssMUELLER Y Z X1 ssINF a_2 a_1 X X2 X3) % 77.26/77.54 False % 77.26/77.54 Clause #673 (by clausification #[672]): ∀ (a a_1 a_2 a_3 : Iota), % 77.26/77.54 Eq % 77.26/77.54 (Exists fun Y => % 77.26/77.54 Exists fun Z => % 77.26/77.54 Exists fun X1 => % 77.26/77.54 Exists fun X2 => % 77.26/77.54 Exists fun X3 => % 77.26/77.54 ssRequisition Y Z X1 a ssINF a_1 a_2 X2 X3 → % 77.26/77.54 ssRequisitionCreated ssMUELLER Y Z X1 ssINF a_3 a_1 a_2 X2 X3) % 77.26/77.54 False % 77.26/77.54 Clause #674 (by clausification #[673]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 77.26/77.54 Eq % 77.26/77.54 (Exists fun Z => % 77.26/77.54 Exists fun X1 => % 77.26/77.54 Exists fun X2 => % 77.26/77.54 Exists fun X3 => % 77.26/77.54 ssRequisition a Z X1 a_1 ssINF a_2 a_3 X2 X3 → % 77.26/77.54 ssRequisitionCreated ssMUELLER a Z X1 ssINF a_4 a_2 a_3 X2 X3) % 77.26/77.54 False % 77.26/77.54 Clause #675 (by clausification #[674]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 77.26/77.54 Eq % 77.26/77.54 (Exists fun X1 => % 77.26/77.54 Exists fun X2 => % 77.26/77.54 Exists fun X3 => % 77.26/77.54 ssRequisition a a_1 X1 a_2 ssINF a_3 a_4 X2 X3 → % 77.26/77.54 ssRequisitionCreated ssMUELLER a a_1 X1 ssINF a_5 a_3 a_4 X2 X3) % 77.26/77.54 False % 77.26/77.54 Clause #676 (by clausification #[675]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.26/77.54 Eq % 77.26/77.54 (Exists fun X2 => % 77.26/77.54 Exists fun X3 => % 77.26/77.54 ssRequisition a a_1 a_2 a_3 ssINF a_4 a_5 X2 X3 → % 77.26/77.54 ssRequisitionCreated ssMUELLER a a_1 a_2 ssINF a_6 a_4 a_5 X2 X3) % 77.26/77.54 False % 77.26/77.54 Clause #677 (by clausification #[676]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 77.26/77.54 Eq % 77.26/77.54 (Exists fun X3 => % 77.26/77.54 ssRequisition a a_1 a_2 a_3 ssINF a_4 a_5 a_6 X3 → % 77.26/77.54 ssRequisitionCreated ssMUELLER a a_1 a_2 ssINF a_7 a_4 a_5 a_6 X3) % 77.26/77.54 False % 77.26/77.54 Clause #678 (by clausification #[677]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 77.26/77.54 Eq % 77.26/77.54 (ssRequisition a a_1 a_2 a_3 ssINF a_4 a_5 a_6 a_7 → % 77.26/77.54 ssRequisitionCreated ssMUELLER a a_1 a_2 ssINF a_8 a_4 a_5 a_6 a_7) % 77.26/77.54 False % 77.26/77.54 Clause #680 (by clausification #[678]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 ssINF a_3 a_4 a_5 a_6 a_7) False % 77.26/77.54 Clause #693 (by clausification #[335]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 77.26/77.54 Or (Eq (ssUserProfile (userProfileEntry a (authObj a_1 a_2 a_3))) True) % 77.26/77.54 (Eq (And (ssSingleRole (singleRoleEntry a_4 (authObj a_1 a_2 a_3))) (ssHolds a a_4)) False) % 77.26/77.54 Clause #695 (by clausification #[693]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 77.26/77.54 Or (Eq (ssUserProfile (userProfileEntry a (authObj a_1 a_2 a_3))) True) % 77.26/77.54 (Or (Eq (ssSingleRole (singleRoleEntry a_4 (authObj a_1 a_2 a_3))) False) (Eq (ssHolds a a_4) False)) % 77.26/77.54 Clause #747 (by superposition #[695, 11]): ∀ (a : Iota), % 77.26/77.54 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssS_TCODE ssTCD ssME51N))) True) % 77.26/77.54 (Or (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) (Eq False True)) % 77.26/77.54 Clause #753 (by superposition #[695, 12]): ∀ (a : Iota), % 77.26/77.54 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_WRK ssACTVT np__1))) True) % 77.26/77.54 (Or (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) (Eq False True)) % 77.26/77.54 Clause #770 (by superposition #[695, 19]): ∀ (a : Iota), % 77.26/77.54 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_EKG ssEKGRP ssI26))) True) % 77.26/77.54 (Or (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) (Eq False True)) % 77.26/77.54 Clause #771 (by superposition #[695, 15]): ∀ (a : Iota), % 77.26/77.54 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_WRK ssWERKS ssINF))) True) % 77.26/77.54 (Or (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) (Eq False True)) % 77.26/77.59 Clause #772 (by superposition #[695, 18]): ∀ (a : Iota), % 77.26/77.59 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_EKG ssACTVT ssSTAR))) True) % 77.26/77.59 (Or (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) (Eq False True)) % 77.26/77.59 Clause #773 (by superposition #[695, 17]): ∀ (a : Iota), % 77.26/77.59 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_BSA ssBSART ssSTAR))) True) % 77.26/77.59 (Or (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) (Eq False True)) % 77.26/77.59 Clause #774 (by superposition #[695, 16]): ∀ (a : Iota), % 77.26/77.59 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_BSA ssACTVT ssSTAR))) True) % 77.26/77.59 (Or (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) (Eq False True)) % 77.26/77.59 Clause #817 (by clausification #[774]): ∀ (a : Iota), % 77.26/77.59 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_BSA ssACTVT ssSTAR))) True) % 77.26/77.59 (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) % 77.26/77.59 Clause #818 (by superposition #[817, 113]): Or (Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_BSA ssACTVT ssSTAR))) True) (Eq False True) % 77.26/77.59 Clause #819 (by clausification #[818]): Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_BSA ssACTVT ssSTAR))) True % 77.26/77.59 Clause #820 (by superposition #[819, 306]): ∀ (a : Iota), Or (Eq True False) (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssACTVT a)) True) % 77.26/77.59 Clause #823 (by clausification #[820]): ∀ (a : Iota), Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssACTVT a)) True % 77.26/77.59 Clause #825 (by clausification #[773]): ∀ (a : Iota), % 77.26/77.59 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_BSA ssBSART ssSTAR))) True) % 77.26/77.59 (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) % 77.26/77.59 Clause #826 (by superposition #[825, 113]): Or (Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_BSA ssBSART ssSTAR))) True) (Eq False True) % 77.26/77.59 Clause #827 (by clausification #[826]): Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_BSA ssBSART ssSTAR))) True % 77.26/77.59 Clause #828 (by superposition #[827, 306]): ∀ (a : Iota), Or (Eq True False) (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) True) % 77.26/77.59 Clause #831 (by clausification #[828]): ∀ (a : Iota), Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) True % 77.26/77.59 Clause #832 (by clausification #[772]): ∀ (a : Iota), % 77.26/77.59 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_EKG ssACTVT ssSTAR))) True) % 77.26/77.59 (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) % 77.26/77.59 Clause #833 (by superposition #[832, 113]): Or (Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_EKG ssACTVT ssSTAR))) True) (Eq False True) % 77.26/77.59 Clause #844 (by clausification #[833]): Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_EKG ssACTVT ssSTAR))) True % 77.26/77.59 Clause #845 (by superposition #[844, 306]): ∀ (a : Iota), Or (Eq True False) (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT a)) True) % 77.26/77.59 Clause #848 (by clausification #[845]): ∀ (a : Iota), Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT a)) True % 77.26/77.59 Clause #850 (by clausification #[771]): ∀ (a : Iota), % 77.26/77.59 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_WRK ssWERKS ssINF))) True) % 77.26/77.59 (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) % 77.26/77.59 Clause #851 (by superposition #[850, 113]): Or (Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_WRK ssWERKS ssINF))) True) (Eq False True) % 77.26/77.59 Clause #852 (by clausification #[851]): Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_WRK ssWERKS ssINF))) True % 77.26/77.59 Clause #853 (by superposition #[852, 311]): Or (Eq True False) (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS ssINF)) True) % 77.26/77.59 Clause #864 (by clausification #[853]): Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS ssINF)) True % 77.26/77.59 Clause #867 (by clausification #[770]): ∀ (a : Iota), % 77.26/77.59 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_EKG ssEKGRP ssI26))) True) % 77.26/77.59 (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) % 77.26/77.59 Clause #868 (by superposition #[867, 113]): Or (Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_EKG ssEKGRP ssI26))) True) (Eq False True) % 77.26/77.59 Clause #869 (by clausification #[868]): Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_EKG ssEKGRP ssI26))) True % 77.26/77.59 Clause #870 (by superposition #[869, 311]): Or (Eq True False) (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssEKGRP ssI26)) True) % 77.36/77.63 Clause #879 (by clausification #[870]): Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssEKGRP ssI26)) True % 77.36/77.63 Clause #882 (by superposition #[879, 197]): ∀ (a a_1 : Iota), % 77.36/77.63 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.63 (Or (Eq True False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssACTVT np__1)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssS_TCODE ssTCD ssME51N)) False) % 77.36/77.63 (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1)) False))))))) % 77.36/77.63 Clause #907 (by clausification #[747]): ∀ (a : Iota), % 77.36/77.63 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssS_TCODE ssTCD ssME51N))) True) % 77.36/77.63 (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) % 77.36/77.63 Clause #908 (by superposition #[907, 113]): Or (Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssS_TCODE ssTCD ssME51N))) True) (Eq False True) % 77.36/77.63 Clause #909 (by clausification #[908]): Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssS_TCODE ssTCD ssME51N))) True % 77.36/77.63 Clause #910 (by superposition #[909, 311]): Or (Eq True False) (Eq (ssAccess ssMUELLER (authObj ssS_TCODE ssTCD ssME51N)) True) % 77.36/77.63 Clause #911 (by clausification #[910]): Eq (ssAccess ssMUELLER (authObj ssS_TCODE ssTCD ssME51N)) True % 77.36/77.63 Clause #957 (by clausification #[753]): ∀ (a : Iota), % 77.36/77.63 Or (Eq (ssUserProfile (userProfileEntry a (authObj ssM_BANF_WRK ssACTVT np__1))) True) % 77.36/77.63 (Eq (ssHolds a ssZBANF_WRK_INF_ED) False) % 77.36/77.63 Clause #958 (by superposition #[957, 113]): Or (Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1))) True) (Eq False True) % 77.36/77.63 Clause #959 (by clausification #[958]): Eq (ssUserProfile (userProfileEntry ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1))) True % 77.36/77.63 Clause #960 (by superposition #[959, 311]): Or (Eq True False) (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1)) True) % 77.36/77.63 Clause #961 (by clausification #[960]): Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1)) True % 77.36/77.63 Clause #981 (by clausification #[622]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 77.36/77.63 Or (Eq (ssRequisitionCreated a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) True) % 77.36/77.63 (Or (Eq (ssAccess a (authObj ssM_BANF_EKG ssEKGRP a_5)) False) % 77.36/77.63 (Or (Eq (ssAccess a (authObj ssM_BANF_BSA ssBSART a_1)) False) % 77.36/77.63 (Or (Eq (ssAccess a (authObj ssM_BANF_WRK ssWERKS a_4)) False) % 77.36/77.63 (Or (Eq (ssAccess a ssME51N) False) (Eq (ssStandardPurchase a_1) False))))) % 77.36/77.63 Clause #984 (by superposition #[981, 879]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 77.36/77.63 Or (Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 a_3 ssI26 a_4 a_5 a_6 a_7) True) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_3)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER ssME51N) False) (Or (Eq (ssStandardPurchase a) False) (Eq False True))))) % 77.36/77.63 Clause #1246 (by clausification #[882]): ∀ (a a_1 : Iota), % 77.36/77.63 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssACTVT np__1)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssS_TCODE ssTCD ssME51N)) False) % 77.36/77.63 (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1)) False)))))) % 77.36/77.63 Clause #1247 (by forward demodulation #[1246, 823]): ∀ (a a_1 : Iota), % 77.36/77.63 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.63 (Or (Eq True False) % 77.36/77.63 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssS_TCODE ssTCD ssME51N)) False) % 77.36/77.68 (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1)) False)))))) % 77.36/77.68 Clause #1248 (by clausification #[1247]): ∀ (a a_1 : Iota), % 77.36/77.68 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssS_TCODE ssTCD ssME51N)) False) % 77.36/77.68 (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1)) False))))) % 77.36/77.68 Clause #1249 (by forward demodulation #[1248, 911]): ∀ (a a_1 : Iota), % 77.36/77.68 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False) % 77.36/77.68 (Or (Eq True False) (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1)) False))))) % 77.36/77.68 Clause #1250 (by clausification #[1249]): ∀ (a a_1 : Iota), % 77.36/77.68 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False) % 77.36/77.68 (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssACTVT np__1)) False)))) % 77.36/77.68 Clause #1251 (by forward demodulation #[1250, 961]): ∀ (a a_1 : Iota), % 77.36/77.68 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False) (Eq True False)))) % 77.36/77.68 Clause #1252 (by clausification #[1251]): ∀ (a a_1 : Iota), % 77.36/77.68 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_EKG ssACTVT np__1)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.68 (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False))) % 77.36/77.68 Clause #1253 (by superposition #[1252, 848]): ∀ (a a_1 : Iota), % 77.36/77.68 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False) (Eq False True))) % 77.36/77.68 Clause #1370 (by clausification #[984]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 77.36/77.68 Or (Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 a_3 ssI26 a_4 a_5 a_6 a_7) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_3)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER ssME51N) False) (Eq (ssStandardPurchase a) False)))) % 77.36/77.68 Clause #1371 (by forward demodulation #[1370, 831]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 77.36/77.68 Or (Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 a_3 ssI26 a_4 a_5 a_6 a_7) True) % 77.36/77.68 (Or (Eq True False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_3)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER ssME51N) False) (Eq (ssStandardPurchase a) False)))) % 77.36/77.68 Clause #1372 (by clausification #[1371]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 77.36/77.68 Or (Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 a_3 ssI26 a_4 a_5 a_6 a_7) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_3)) False) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER ssME51N) False) (Eq (ssStandardPurchase a) False))) % 77.36/77.68 Clause #1373 (by superposition #[1372, 864]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.36/77.68 Or (Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 ssINF ssI26 a_3 a_4 a_5 a_6) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER ssME51N) False) (Or (Eq (ssStandardPurchase a) False) (Eq False True))) % 77.36/77.68 Clause #1450 (by clausification #[1253]): ∀ (a a_1 : Iota), % 77.36/77.68 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.36/77.68 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_BSA ssBSART a)) False) % 77.46/77.71 (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a_1)) False)) % 77.46/77.71 Clause #1451 (by superposition #[1450, 831]): ∀ (a : Iota), % 77.46/77.71 Or (Eq (ssAccess ssMUELLER ssME51N) True) % 77.46/77.71 (Or (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a)) False) (Eq False True)) % 77.46/77.71 Clause #1452 (by clausification #[1451]): ∀ (a : Iota), Or (Eq (ssAccess ssMUELLER ssME51N) True) (Eq (ssAccess ssMUELLER (authObj ssM_BANF_WRK ssWERKS a)) False) % 77.46/77.71 Clause #1453 (by superposition #[1452, 864]): Or (Eq (ssAccess ssMUELLER ssME51N) True) (Eq False True) % 77.46/77.71 Clause #1458 (by clausification #[1453]): Eq (ssAccess ssMUELLER ssME51N) True % 77.46/77.71 Clause #1478 (by clausification #[1373]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.46/77.71 Or (Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 ssINF ssI26 a_3 a_4 a_5 a_6) True) % 77.46/77.71 (Or (Eq (ssAccess ssMUELLER ssME51N) False) (Eq (ssStandardPurchase a) False)) % 77.46/77.71 Clause #1479 (by forward demodulation #[1478, 1458]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.46/77.71 Or (Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 ssINF ssI26 a_3 a_4 a_5 a_6) True) % 77.46/77.71 (Or (Eq True False) (Eq (ssStandardPurchase a) False)) % 77.46/77.71 Clause #1480 (by clausification #[1479]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 77.46/77.71 Or (Eq (ssRequisitionCreated ssMUELLER a a_1 a_2 ssINF ssI26 a_3 a_4 a_5 a_6) True) (Eq (ssStandardPurchase a) False) % 77.46/77.71 Clause #1481 (by superposition #[1480, 117]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 77.46/77.71 Or (Eq (ssRequisitionCreated ssMUELLER ssNB a a_1 ssINF ssI26 a_2 a_3 a_4 a_5) True) (Eq False True) % 77.46/77.71 Clause #1506 (by clausification #[1481]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (ssRequisitionCreated ssMUELLER ssNB a a_1 ssINF ssI26 a_2 a_3 a_4 a_5) True % 77.46/77.71 Clause #1508 (by superposition #[1506, 680]): Eq True False % 77.46/77.71 Clause #1514 (by clausification #[1508]): False % 77.46/77.71 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------