%------------------------------------------------------------------------------ % File : lazyCoP---0.1 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop % Computer : n003.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:13:22 AM UTC 2026 % Result : Theorem 3.50s 0.89s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0. % 0.00/0.04 % Command : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop % 0.08/0.34 % Computer : n003.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Mon Sep 7 13:51:54 UTC 2026 % 0.08/0.35 % CPUTime : % 3.50/0.89 % SZS status Theorem % 3.50/0.89 % SZS output begin IncompleteProof % 3.50/0.89 cnf(c0, axiom, % 3.50/0.89 ~ssRequisitionCreated(ssMUELLER,X0,X1,X2,ssINF,X3,X4,X5,X6,X7)). % 3.50/0.89 cnf(c1, plain, % 3.50/0.89 ~ssRequisitionCreated(ssMUELLER,X0,X1,X2,ssINF,X3,X4,X5,X6,X7), % 3.50/0.89 inference(start, [], [c0])). % 3.50/0.89 % 3.50/0.89 cnf(c2, axiom, % 3.50/0.89 ssRequisitionCreated(X8,X9,X10,X11,X12,X13,X14,X15,X16,X17) | ~ssAccess(X8,authObj(ssM_BANF_EKG,ssEKGRP,X13)) | ~ssAccess(X8,authObj(ssM_BANF_BSA,ssBSART,X9)) | ~ssAccess(X8,authObj(ssM_BANF_WRK,ssWERKS,X12)) | ~ssAccess(X8,ssME51N) | ~ssStandardPurchase(X9) | ~ssRequisition(X9,X10,X11,X12,X13,X14,X15,X16,X17)). % 3.50/0.89 cnf(a0, assumption, % 3.50/0.89 ssMUELLER = X8). % 3.50/0.89 cnf(a1, assumption, % 3.50/0.89 X0 = X9). % 3.50/0.89 cnf(a2, assumption, % 3.50/0.89 X1 = X10). % 3.50/0.89 cnf(a3, assumption, % 3.50/0.89 X2 = X11). % 3.50/0.89 cnf(a4, assumption, % 3.50/0.89 ssINF = X12). % 3.50/0.89 cnf(a5, assumption, % 3.50/0.89 X3 = X13). % 3.50/0.89 cnf(a6, assumption, % 3.50/0.89 X4 = X14). % 3.50/0.89 cnf(a7, assumption, % 3.50/0.89 X5 = X15). % 3.50/0.89 cnf(a8, assumption, % 3.50/0.89 X6 = X16). % 3.50/0.89 cnf(a9, assumption, % 3.50/0.89 X7 = X17). % 3.50/0.89 cnf(c3, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9])], [c1, c2])). % 3.50/0.89 cnf(c4, plain, % 3.50/0.89 ~ssAccess(X8,authObj(ssM_BANF_EKG,ssEKGRP,X13)) | ~ssAccess(X8,authObj(ssM_BANF_BSA,ssBSART,X9)) | ~ssAccess(X8,authObj(ssM_BANF_WRK,ssWERKS,X12)) | ~ssAccess(X8,ssME51N) | ~ssStandardPurchase(X9) | ~ssRequisition(X9,X10,X11,X12,X13,X14,X15,X16,X17), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9])], [c1, c2])). % 3.50/0.89 % 3.50/0.89 cnf(c5, axiom, % 3.50/0.89 ssAccess(X18,authObj(X19,X20,X21)) | ~ssUserProfile(userProfileEntry(X18,authObj(X19,X20,X21)))). % 3.50/0.89 cnf(a10, assumption, % 3.50/0.89 X8 = X18). % 3.50/0.89 cnf(a11, assumption, % 3.50/0.89 authObj(ssM_BANF_EKG,ssEKGRP,X13) = authObj(X19,X20,X21)). % 3.50/0.89 cnf(c6, plain, % 3.50/0.89 ~ssAccess(X8,authObj(ssM_BANF_BSA,ssBSART,X9)) | ~ssAccess(X8,authObj(ssM_BANF_WRK,ssWERKS,X12)) | ~ssAccess(X8,ssME51N) | ~ssStandardPurchase(X9) | ~ssRequisition(X9,X10,X11,X12,X13,X14,X15,X16,X17), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a10, a11])], [c4, c5])). % 3.50/0.89 cnf(c7, plain, % 3.50/0.89 ~ssUserProfile(userProfileEntry(X18,authObj(X19,X20,X21))), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a10, a11])], [c4, c5])). % 3.50/0.89 % 3.50/0.89 cnf(c8, axiom, % 3.50/0.89 ssUserProfile(userProfileEntry(X22,authObj(X23,X24,X25))) | sP0(X26,X22,X25,X24,X23,X27,X28)). % 3.50/0.89 cnf(a12, assumption, % 3.50/0.89 userProfileEntry(X18,authObj(X19,X20,X21)) = userProfileEntry(X22,authObj(X23,X24,X25))). % 3.50/0.89 cnf(c9, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a12])], [c7, c8])). % 3.50/0.89 cnf(c10, plain, % 3.50/0.89 sP0(X26,X22,X25,X24,X23,X27,X28), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a12])], [c7, c8])). % 3.50/0.89 % 3.50/0.89 cnf(c11, axiom, % 3.50/0.89 ~ssHolds(X29,X30) | ~ssSingleRole(singleRoleEntry(X30,authObj(X31,X32,X33))) | ~sP0(X34,X29,X33,X32,X31,X30,X35)). % 3.50/0.89 cnf(a13, assumption, % 3.50/0.89 X26 = X34). % 3.50/0.89 cnf(a14, assumption, % 3.50/0.89 X22 = X29). % 3.50/0.89 cnf(a15, assumption, % 3.50/0.89 X25 = X33). % 3.50/0.89 cnf(a16, assumption, % 3.50/0.89 X24 = X32). % 3.50/0.89 cnf(a17, assumption, % 3.50/0.89 X23 = X31). % 3.50/0.89 cnf(a18, assumption, % 3.50/0.89 X27 = X30). % 3.50/0.89 cnf(a19, assumption, % 3.50/0.89 X28 = X35). % 3.50/0.89 cnf(c12, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a13, a14, a15, a16, a17, a18, a19])], [c10, c11])). % 3.50/0.89 cnf(c13, plain, % 3.50/0.89 ~ssHolds(X29,X30) | ~ssSingleRole(singleRoleEntry(X30,authObj(X31,X32,X33))), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a13, a14, a15, a16, a17, a18, a19])], [c10, c11])). % 3.50/0.89 % 3.50/0.89 cnf(c14, axiom, % 3.50/0.89 ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)). % 3.50/0.89 cnf(a20, assumption, % 3.50/0.89 X29 = ssMUELLER). % 3.50/0.89 cnf(a21, assumption, % 3.50/0.89 X30 = ssZBANF_WRK_INF_ED). % 3.50/0.89 cnf(c15, plain, % 3.50/0.89 ~ssSingleRole(singleRoleEntry(X30,authObj(X31,X32,X33))), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a20, a21])], [c13, c14])). % 3.50/0.89 cnf(c16, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a20, a21])], [c13, c14])). % 3.50/0.89 % 3.50/0.89 cnf(c17, axiom, % 3.50/0.89 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))). % 3.50/0.89 cnf(a22, assumption, % 3.50/0.89 singleRoleEntry(X30,authObj(X31,X32,X33)) = singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))). % 3.50/0.89 cnf(c18, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a22])], [c15, c17])). % 3.50/0.89 cnf(c19, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a22])], [c15, c17])). % 3.50/0.89 % 3.50/0.89 cnf(c20, axiom, % 3.50/0.89 ssAccess(X36,authObj(X37,X38,X39)) | ~ssUserProfile(userProfileEntry(X36,authObj(X37,X38,ssSTAR)))). % 3.50/0.89 cnf(a23, assumption, % 3.50/0.89 X8 = X36). % 3.50/0.89 cnf(a24, assumption, % 3.50/0.89 authObj(ssM_BANF_BSA,ssBSART,X9) = authObj(X37,X38,X39)). % 3.50/0.89 cnf(c21, plain, % 3.50/0.89 ~ssAccess(X8,authObj(ssM_BANF_WRK,ssWERKS,X12)) | ~ssAccess(X8,ssME51N) | ~ssStandardPurchase(X9) | ~ssRequisition(X9,X10,X11,X12,X13,X14,X15,X16,X17), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a23, a24])], [c6, c20])). % 3.50/0.89 cnf(c22, plain, % 3.50/0.89 ~ssUserProfile(userProfileEntry(X36,authObj(X37,X38,ssSTAR))), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a23, a24])], [c6, c20])). % 3.50/0.89 % 3.50/0.89 cnf(c23, axiom, % 3.50/0.89 ssUserProfile(userProfileEntry(X40,authObj(X41,X42,X43))) | sP0(X44,X40,X43,X42,X41,X45,X46)). % 3.50/0.89 cnf(a25, assumption, % 3.50/0.89 userProfileEntry(X36,authObj(X37,X38,ssSTAR)) = userProfileEntry(X40,authObj(X41,X42,X43))). % 3.50/0.89 cnf(c24, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a25])], [c22, c23])). % 3.50/0.89 cnf(c25, plain, % 3.50/0.89 sP0(X44,X40,X43,X42,X41,X45,X46), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a25])], [c22, c23])). % 3.50/0.89 % 3.50/0.89 cnf(c26, axiom, % 3.50/0.89 ~ssHolds(X47,X48) | ~ssSingleRole(singleRoleEntry(X48,authObj(X49,X50,X51))) | ~sP0(X52,X47,X51,X50,X49,X48,X53)). % 3.50/0.89 cnf(a26, assumption, % 3.50/0.89 X44 = X52). % 3.50/0.89 cnf(a27, assumption, % 3.50/0.89 X40 = X47). % 3.50/0.89 cnf(a28, assumption, % 3.50/0.89 X43 = X51). % 3.50/0.89 cnf(a29, assumption, % 3.50/0.89 X42 = X50). % 3.50/0.89 cnf(a30, assumption, % 3.50/0.89 X41 = X49). % 3.50/0.89 cnf(a31, assumption, % 3.50/0.89 X45 = X48). % 3.50/0.89 cnf(a32, assumption, % 3.50/0.89 X46 = X53). % 3.50/0.89 cnf(c27, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a26, a27, a28, a29, a30, a31, a32])], [c25, c26])). % 3.50/0.89 cnf(c28, plain, % 3.50/0.89 ~ssHolds(X47,X48) | ~ssSingleRole(singleRoleEntry(X48,authObj(X49,X50,X51))), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a26, a27, a28, a29, a30, a31, a32])], [c25, c26])). % 3.50/0.89 % 3.50/0.89 cnf(c29, plain, % 3.50/0.89 ssHolds(X29,X30)). % 3.50/0.89 cnf(a33, assumption, % 3.50/0.89 X47 = X29). % 3.50/0.89 cnf(a34, assumption, % 3.50/0.89 X48 = X30). % 3.50/0.89 cnf(c30, plain, % 3.50/0.89 ~ssSingleRole(singleRoleEntry(X48,authObj(X49,X50,X51))), % 3.50/0.89 inference(predicate_reduction, [assumptions([a33, a34])], [c28, c29])). % 3.50/0.89 % 3.50/0.89 cnf(c31, axiom, % 3.50/0.89 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))). % 3.50/0.89 cnf(a35, assumption, % 3.50/0.89 singleRoleEntry(X48,authObj(X49,X50,X51)) = singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))). % 3.50/0.89 cnf(c32, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a35])], [c30, c31])). % 3.50/0.89 cnf(c33, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a35])], [c30, c31])). % 3.50/0.89 % 3.50/0.89 cnf(c34, axiom, % 3.50/0.89 ssAccess(X54,authObj(X55,X56,X57)) | ~ssUserProfile(userProfileEntry(X54,authObj(X55,X56,X57)))). % 3.50/0.89 cnf(a36, assumption, % 3.50/0.89 X8 = X54). % 3.50/0.89 cnf(a37, assumption, % 3.50/0.89 authObj(ssM_BANF_WRK,ssWERKS,X12) = authObj(X55,X56,X57)). % 3.50/0.89 cnf(c35, plain, % 3.50/0.89 ~ssAccess(X8,ssME51N) | ~ssStandardPurchase(X9) | ~ssRequisition(X9,X10,X11,X12,X13,X14,X15,X16,X17), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a36, a37])], [c21, c34])). % 3.50/0.89 cnf(c36, plain, % 3.50/0.89 ~ssUserProfile(userProfileEntry(X54,authObj(X55,X56,X57))), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a36, a37])], [c21, c34])). % 3.50/0.89 % 3.50/0.89 cnf(c37, axiom, % 3.50/0.89 ssUserProfile(userProfileEntry(X58,authObj(X59,X60,X61))) | sP0(X62,X58,X61,X60,X59,X63,X64)). % 3.50/0.89 cnf(a38, assumption, % 3.50/0.89 userProfileEntry(X54,authObj(X55,X56,X57)) = userProfileEntry(X58,authObj(X59,X60,X61))). % 3.50/0.89 cnf(c38, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a38])], [c36, c37])). % 3.50/0.89 cnf(c39, plain, % 3.50/0.89 sP0(X62,X58,X61,X60,X59,X63,X64), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a38])], [c36, c37])). % 3.50/0.89 % 3.50/0.89 cnf(c40, axiom, % 3.50/0.89 ~ssHolds(X65,X66) | ~ssSingleRole(singleRoleEntry(X66,authObj(X67,X68,X69))) | ~sP0(X70,X65,X69,X68,X67,X66,X71)). % 3.50/0.89 cnf(a39, assumption, % 3.50/0.89 X62 = X70). % 3.50/0.89 cnf(a40, assumption, % 3.50/0.89 X58 = X65). % 3.50/0.89 cnf(a41, assumption, % 3.50/0.89 X61 = X69). % 3.50/0.89 cnf(a42, assumption, % 3.50/0.89 X60 = X68). % 3.50/0.89 cnf(a43, assumption, % 3.50/0.89 X59 = X67). % 3.50/0.89 cnf(a44, assumption, % 3.50/0.89 X63 = X66). % 3.50/0.89 cnf(a45, assumption, % 3.50/0.89 X64 = X71). % 3.50/0.89 cnf(c41, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a39, a40, a41, a42, a43, a44, a45])], [c39, c40])). % 3.50/0.89 cnf(c42, plain, % 3.50/0.89 ~ssHolds(X65,X66) | ~ssSingleRole(singleRoleEntry(X66,authObj(X67,X68,X69))), % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a39, a40, a41, a42, a43, a44, a45])], [c39, c40])). % 3.50/0.89 % 3.50/0.89 cnf(c43, plain, % 3.50/0.89 ssHolds(X29,X30)). % 3.50/0.89 cnf(a46, assumption, % 3.50/0.89 X65 = X29). % 3.50/0.89 cnf(a47, assumption, % 3.50/0.89 X66 = X30). % 3.50/0.89 cnf(c44, plain, % 3.50/0.89 ~ssSingleRole(singleRoleEntry(X66,authObj(X67,X68,X69))), % 3.50/0.89 inference(predicate_reduction, [assumptions([a46, a47])], [c42, c43])). % 3.50/0.89 % 3.50/0.89 cnf(c45, axiom, % 3.50/0.89 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))). % 3.50/0.89 cnf(a48, assumption, % 3.50/0.89 singleRoleEntry(X66,authObj(X67,X68,X69)) = singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))). % 3.50/0.89 cnf(c46, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a48])], [c44, c45])). % 3.50/0.89 cnf(c47, plain, % 3.50/0.89 $false, % 3.50/0.89 inference(strict_predicate_extension, [assumptions([a48])], [c44, c45])). % 3.50/0.89 % 3.50/0.89 cnf(c48, axiom, % 3.50/0.89 ssAccess(X72,ssME51N) | ~ssAccess(X72,authObj(ssM_BANF_EKG,ssEKGRP,X73)) | ~ssAccess(X72,authObj(ssM_BANF_EKG,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssM_BANF_BSA,ssBSART,X74)) | ~ssAccess(X72,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssWERKS,X75)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssS_TCODE,ssTCD,ssME51N))). % 3.50/0.90 cnf(a49, assumption, % 3.50/0.90 X8 = X72). % 3.50/0.90 cnf(a50, assumption, % 3.50/0.90 ssME51N = ssME51N). % 3.50/0.90 cnf(c49, plain, % 3.50/0.90 ~ssStandardPurchase(X9) | ~ssRequisition(X9,X10,X11,X12,X13,X14,X15,X16,X17), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a49, a50])], [c35, c48])). % 3.50/0.90 cnf(c50, plain, % 3.50/0.90 ~ssAccess(X72,authObj(ssM_BANF_EKG,ssEKGRP,X73)) | ~ssAccess(X72,authObj(ssM_BANF_EKG,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssM_BANF_BSA,ssBSART,X74)) | ~ssAccess(X72,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssWERKS,X75)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssS_TCODE,ssTCD,ssME51N)), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a49, a50])], [c35, c48])). % 3.50/0.90 % 3.50/0.90 cnf(c51, plain, % 3.50/0.90 ssAccess(X8,authObj(ssM_BANF_EKG,ssEKGRP,X13))). % 3.50/0.90 cnf(a51, assumption, % 3.50/0.90 X72 = X8). % 3.50/0.90 cnf(a52, assumption, % 3.50/0.90 authObj(ssM_BANF_EKG,ssEKGRP,X73) = authObj(ssM_BANF_EKG,ssEKGRP,X13)). % 3.50/0.90 cnf(c52, plain, % 3.50/0.90 ~ssAccess(X72,authObj(ssM_BANF_EKG,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssM_BANF_BSA,ssBSART,X74)) | ~ssAccess(X72,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssWERKS,X75)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssS_TCODE,ssTCD,ssME51N)), % 3.50/0.90 inference(predicate_reduction, [assumptions([a51, a52])], [c50, c51])). % 3.50/0.90 % 3.50/0.90 cnf(c53, axiom, % 3.50/0.90 ssAccess(X76,authObj(X77,X78,X79)) | ~ssUserProfile(userProfileEntry(X76,authObj(X77,X78,ssSTAR)))). % 3.50/0.90 cnf(a53, assumption, % 3.50/0.90 X72 = X76). % 3.50/0.90 cnf(a54, assumption, % 3.50/0.90 authObj(ssM_BANF_EKG,ssACTVT,np__1) = authObj(X77,X78,X79)). % 3.50/0.90 cnf(c54, plain, % 3.50/0.90 ~ssAccess(X72,authObj(ssM_BANF_BSA,ssBSART,X74)) | ~ssAccess(X72,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssWERKS,X75)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssS_TCODE,ssTCD,ssME51N)), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a53, a54])], [c52, c53])). % 3.50/0.90 cnf(c55, plain, % 3.50/0.90 ~ssUserProfile(userProfileEntry(X76,authObj(X77,X78,ssSTAR))), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a53, a54])], [c52, c53])). % 3.50/0.90 % 3.50/0.90 cnf(c56, axiom, % 3.50/0.90 ssUserProfile(userProfileEntry(X80,authObj(X81,X82,X83))) | sP0(X84,X80,X83,X82,X81,X85,X86)). % 3.50/0.90 cnf(a55, assumption, % 3.50/0.90 userProfileEntry(X76,authObj(X77,X78,ssSTAR)) = userProfileEntry(X80,authObj(X81,X82,X83))). % 3.50/0.90 cnf(c57, plain, % 3.50/0.90 $false, % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a55])], [c55, c56])). % 3.50/0.90 cnf(c58, plain, % 3.50/0.90 sP0(X84,X80,X83,X82,X81,X85,X86), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a55])], [c55, c56])). % 3.50/0.90 % 3.50/0.90 cnf(c59, axiom, % 3.50/0.90 ~ssHolds(X87,X88) | ~ssSingleRole(singleRoleEntry(X88,authObj(X89,X90,X91))) | ~sP0(X92,X87,X91,X90,X89,X88,X93)). % 3.50/0.90 cnf(a56, assumption, % 3.50/0.90 X84 = X92). % 3.50/0.90 cnf(a57, assumption, % 3.50/0.90 X80 = X87). % 3.50/0.90 cnf(a58, assumption, % 3.50/0.90 X83 = X91). % 3.50/0.90 cnf(a59, assumption, % 3.50/0.90 X82 = X90). % 3.50/0.90 cnf(a60, assumption, % 3.50/0.90 X81 = X89). % 3.50/0.90 cnf(a61, assumption, % 3.50/0.90 X85 = X88). % 3.50/0.90 cnf(a62, assumption, % 3.50/0.90 X86 = X93). % 3.50/0.90 cnf(c60, plain, % 3.50/0.90 $false, % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a56, a57, a58, a59, a60, a61, a62])], [c58, c59])). % 3.50/0.90 cnf(c61, plain, % 3.50/0.90 ~ssHolds(X87,X88) | ~ssSingleRole(singleRoleEntry(X88,authObj(X89,X90,X91))), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a56, a57, a58, a59, a60, a61, a62])], [c58, c59])). % 3.50/0.90 % 3.50/0.90 cnf(c62, plain, % 3.50/0.90 ssHolds(X29,X30)). % 3.50/0.90 cnf(a63, assumption, % 3.50/0.90 X87 = X29). % 3.50/0.90 cnf(a64, assumption, % 3.50/0.90 X88 = X30). % 3.50/0.90 cnf(c63, plain, % 3.50/0.90 ~ssSingleRole(singleRoleEntry(X88,authObj(X89,X90,X91))), % 3.50/0.90 inference(predicate_reduction, [assumptions([a63, a64])], [c61, c62])). % 3.50/0.90 % 3.50/0.90 cnf(c64, axiom, % 3.50/0.90 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))). % 3.50/0.90 cnf(a65, assumption, % 3.50/0.90 singleRoleEntry(X88,authObj(X89,X90,X91)) = singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))). % 3.50/0.90 cnf(c65, plain, % 3.50/0.90 $false, % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a65])], [c63, c64])). % 3.50/0.90 cnf(c66, plain, % 3.50/0.90 $false, % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a65])], [c63, c64])). % 3.50/0.90 % 3.50/0.90 cnf(c67, plain, % 3.50/0.90 ssAccess(X8,authObj(ssM_BANF_BSA,ssBSART,X9))). % 3.50/0.90 cnf(a66, assumption, % 3.50/0.90 X72 = X8). % 3.50/0.90 cnf(a67, assumption, % 3.50/0.90 authObj(ssM_BANF_BSA,ssBSART,X74) = authObj(ssM_BANF_BSA,ssBSART,X9)). % 3.50/0.90 cnf(c68, plain, % 3.50/0.90 ~ssAccess(X72,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssWERKS,X75)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssS_TCODE,ssTCD,ssME51N)), % 3.50/0.90 inference(predicate_reduction, [assumptions([a66, a67])], [c54, c67])). % 3.50/0.90 % 3.50/0.90 cnf(c69, axiom, % 3.50/0.90 ssAccess(X94,authObj(X95,X96,X97)) | ~ssUserProfile(userProfileEntry(X94,authObj(X95,X96,ssSTAR)))). % 3.50/0.90 cnf(a68, assumption, % 3.50/0.90 X72 = X94). % 3.50/0.90 cnf(a69, assumption, % 3.50/0.90 authObj(ssM_BANF_BSA,ssACTVT,np__1) = authObj(X95,X96,X97)). % 3.50/0.90 cnf(c70, plain, % 3.50/0.90 ~ssAccess(X72,authObj(ssM_BANF_WRK,ssWERKS,X75)) | ~ssAccess(X72,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssS_TCODE,ssTCD,ssME51N)), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a68, a69])], [c68, c69])). % 3.50/0.90 cnf(c71, plain, % 3.50/0.90 ~ssUserProfile(userProfileEntry(X94,authObj(X95,X96,ssSTAR))), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a68, a69])], [c68, c69])). % 3.50/0.90 % 3.50/0.90 cnf(c72, axiom, % 3.50/0.90 ssUserProfile(userProfileEntry(X98,authObj(X99,X100,X101))) | sP0(X102,X98,X101,X100,X99,X103,X104)). % 3.50/0.90 cnf(a70, assumption, % 3.50/0.90 userProfileEntry(X94,authObj(X95,X96,ssSTAR)) = userProfileEntry(X98,authObj(X99,X100,X101))). % 3.50/0.90 cnf(c73, plain, % 3.50/0.90 $false, % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a70])], [c71, c72])). % 3.50/0.90 cnf(c74, plain, % 3.50/0.90 sP0(X102,X98,X101,X100,X99,X103,X104), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a70])], [c71, c72])). % 3.50/0.90 % 3.50/0.90 cnf(c75, axiom, % 3.50/0.90 ~ssHolds(X105,X106) | ~ssSingleRole(singleRoleEntry(X106,authObj(X107,X108,X109))) | ~sP0(X110,X105,X109,X108,X107,X106,X111)). % 3.50/0.90 cnf(a71, assumption, % 3.50/0.90 X102 = X110). % 3.50/0.90 cnf(a72, assumption, % 3.50/0.90 X98 = X105). % 3.50/0.90 cnf(a73, assumption, % 3.50/0.90 X101 = X109). % 3.50/0.90 cnf(a74, assumption, % 3.50/0.90 X100 = X108). % 3.50/0.90 cnf(a75, assumption, % 3.50/0.90 X99 = X107). % 3.50/0.90 cnf(a76, assumption, % 3.50/0.90 X103 = X106). % 3.50/0.90 cnf(a77, assumption, % 3.50/0.90 X104 = X111). % 3.50/0.90 cnf(c76, plain, % 3.50/0.90 $false, % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a71, a72, a73, a74, a75, a76, a77])], [c74, c75])). % 3.50/0.90 cnf(c77, plain, % 3.50/0.90 ~ssHolds(X105,X106) | ~ssSingleRole(singleRoleEntry(X106,authObj(X107,X108,X109))), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a71, a72, a73, a74, a75, a76, a77])], [c74, c75])). % 3.50/0.90 % 3.50/0.90 cnf(c78, plain, % 3.50/0.90 ssHolds(X29,X30)). % 3.50/0.90 cnf(a78, assumption, % 3.50/0.90 X105 = X29). % 3.50/0.90 cnf(a79, assumption, % 3.50/0.90 X106 = X30). % 3.50/0.90 cnf(c79, plain, % 3.50/0.90 ~ssSingleRole(singleRoleEntry(X106,authObj(X107,X108,X109))), % 3.50/0.90 inference(predicate_reduction, [assumptions([a78, a79])], [c77, c78])). % 3.50/0.90 % 3.50/0.90 cnf(c80, axiom, % 3.50/0.90 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))). % 3.50/0.90 cnf(a80, assumption, % 3.50/0.90 singleRoleEntry(X106,authObj(X107,X108,X109)) = singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))). % 3.50/0.90 cnf(c81, plain, % 3.50/0.90 $false, % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a80])], [c79, c80])). % 3.50/0.90 cnf(c82, plain, % 3.50/0.90 $false, % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a80])], [c79, c80])). % 3.50/0.90 % 3.50/0.90 cnf(c83, plain, % 3.50/0.90 ssAccess(X8,authObj(ssM_BANF_WRK,ssWERKS,X12))). % 3.50/0.90 cnf(a81, assumption, % 3.50/0.90 X72 = X8). % 3.50/0.90 cnf(a82, assumption, % 3.50/0.90 authObj(ssM_BANF_WRK,ssWERKS,X75) = authObj(ssM_BANF_WRK,ssWERKS,X12)). % 3.50/0.90 cnf(c84, plain, % 3.50/0.90 ~ssAccess(X72,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X72,authObj(ssS_TCODE,ssTCD,ssME51N)), % 3.50/0.90 inference(predicate_reduction, [assumptions([a81, a82])], [c70, c83])). % 3.50/0.90 % 3.50/0.90 cnf(c85, axiom, % 3.50/0.90 ssAccess(X112,authObj(X113,X114,X115)) | ~ssUserProfile(userProfileEntry(X112,authObj(X113,X114,X115)))). % 3.50/0.90 cnf(a83, assumption, % 3.50/0.90 X72 = X112). % 3.50/0.90 cnf(a84, assumption, % 3.50/0.90 authObj(ssM_BANF_WRK,ssACTVT,np__1) = authObj(X113,X114,X115)). % 3.50/0.90 cnf(c86, plain, % 3.50/0.90 ~ssAccess(X72,authObj(ssS_TCODE,ssTCD,ssME51N)), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a83, a84])], [c84, c85])). % 3.50/0.90 cnf(c87, plain, % 3.50/0.90 ~ssUserProfile(userProfileEntry(X112,authObj(X113,X114,X115))), % 3.50/0.90 inference(strict_predicate_extension, [assumptions([a83, a84])], [c84, c85])). % 3.50/0.90 % 3.50/0.90 cnf(c88, axiom, % 3.50/0.90 ssUserProfile(userProfileEntry(X116,authObj(X117,X118,X119))) | sP0(X120,X116,X119,X118,X117,X121,X122)). % 4.26/0.90 cnf(a85, assumption, % 4.26/0.90 userProfileEntry(X112,authObj(X113,X114,X115)) = userProfileEntry(X116,authObj(X117,X118,X119))). % 4.26/0.90 cnf(c89, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a85])], [c87, c88])). % 4.26/0.90 cnf(c90, plain, % 4.26/0.90 sP0(X120,X116,X119,X118,X117,X121,X122), % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a85])], [c87, c88])). % 4.26/0.90 % 4.26/0.90 cnf(c91, axiom, % 4.26/0.90 ~ssHolds(X123,X124) | ~ssSingleRole(singleRoleEntry(X124,authObj(X125,X126,X127))) | ~sP0(X128,X123,X127,X126,X125,X124,X129)). % 4.26/0.90 cnf(a86, assumption, % 4.26/0.90 X120 = X128). % 4.26/0.90 cnf(a87, assumption, % 4.26/0.90 X116 = X123). % 4.26/0.90 cnf(a88, assumption, % 4.26/0.90 X119 = X127). % 4.26/0.90 cnf(a89, assumption, % 4.26/0.90 X118 = X126). % 4.26/0.90 cnf(a90, assumption, % 4.26/0.90 X117 = X125). % 4.26/0.90 cnf(a91, assumption, % 4.26/0.90 X121 = X124). % 4.26/0.90 cnf(a92, assumption, % 4.26/0.90 X122 = X129). % 4.26/0.90 cnf(c92, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a86, a87, a88, a89, a90, a91, a92])], [c90, c91])). % 4.26/0.90 cnf(c93, plain, % 4.26/0.90 ~ssHolds(X123,X124) | ~ssSingleRole(singleRoleEntry(X124,authObj(X125,X126,X127))), % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a86, a87, a88, a89, a90, a91, a92])], [c90, c91])). % 4.26/0.90 % 4.26/0.90 cnf(c94, plain, % 4.26/0.90 ssHolds(X29,X30)). % 4.26/0.90 cnf(a93, assumption, % 4.26/0.90 X123 = X29). % 4.26/0.90 cnf(a94, assumption, % 4.26/0.90 X124 = X30). % 4.26/0.90 cnf(c95, plain, % 4.26/0.90 ~ssSingleRole(singleRoleEntry(X124,authObj(X125,X126,X127))), % 4.26/0.90 inference(predicate_reduction, [assumptions([a93, a94])], [c93, c94])). % 4.26/0.90 % 4.26/0.90 cnf(c96, axiom, % 4.26/0.90 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1)))). % 4.26/0.90 cnf(a95, assumption, % 4.26/0.90 singleRoleEntry(X124,authObj(X125,X126,X127)) = singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))). % 4.26/0.90 cnf(c97, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a95])], [c95, c96])). % 4.26/0.90 cnf(c98, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a95])], [c95, c96])). % 4.26/0.90 % 4.26/0.90 cnf(c99, axiom, % 4.26/0.90 ssAccess(X130,authObj(X131,X132,X133)) | ~ssUserProfile(userProfileEntry(X130,authObj(X131,X132,X133)))). % 4.26/0.90 cnf(a96, assumption, % 4.26/0.90 X72 = X130). % 4.26/0.90 cnf(a97, assumption, % 4.26/0.90 authObj(ssS_TCODE,ssTCD,ssME51N) = authObj(X131,X132,X133)). % 4.26/0.90 cnf(c100, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a96, a97])], [c86, c99])). % 4.26/0.90 cnf(c101, plain, % 4.26/0.90 ~ssUserProfile(userProfileEntry(X130,authObj(X131,X132,X133))), % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a96, a97])], [c86, c99])). % 4.26/0.90 % 4.26/0.90 cnf(c102, axiom, % 4.26/0.90 ssUserProfile(userProfileEntry(X134,authObj(X135,X136,X137))) | sP0(X138,X134,X137,X136,X135,X139,X140)). % 4.26/0.90 cnf(a98, assumption, % 4.26/0.90 userProfileEntry(X130,authObj(X131,X132,X133)) = userProfileEntry(X134,authObj(X135,X136,X137))). % 4.26/0.90 cnf(c103, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a98])], [c101, c102])). % 4.26/0.90 cnf(c104, plain, % 4.26/0.90 sP0(X138,X134,X137,X136,X135,X139,X140), % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a98])], [c101, c102])). % 4.26/0.90 % 4.26/0.90 cnf(c105, axiom, % 4.26/0.90 ~ssHolds(X141,X142) | ~ssSingleRole(singleRoleEntry(X142,authObj(X143,X144,X145))) | ~sP0(X146,X141,X145,X144,X143,X142,X147)). % 4.26/0.90 cnf(a99, assumption, % 4.26/0.90 X138 = X146). % 4.26/0.90 cnf(a100, assumption, % 4.26/0.90 X134 = X141). % 4.26/0.90 cnf(a101, assumption, % 4.26/0.90 X137 = X145). % 4.26/0.90 cnf(a102, assumption, % 4.26/0.90 X136 = X144). % 4.26/0.90 cnf(a103, assumption, % 4.26/0.90 X135 = X143). % 4.26/0.90 cnf(a104, assumption, % 4.26/0.90 X139 = X142). % 4.26/0.90 cnf(a105, assumption, % 4.26/0.90 X140 = X147). % 4.26/0.90 cnf(c106, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a99, a100, a101, a102, a103, a104, a105])], [c104, c105])). % 4.26/0.90 cnf(c107, plain, % 4.26/0.90 ~ssHolds(X141,X142) | ~ssSingleRole(singleRoleEntry(X142,authObj(X143,X144,X145))), % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a99, a100, a101, a102, a103, a104, a105])], [c104, c105])). % 4.26/0.90 % 4.26/0.90 cnf(c108, plain, % 4.26/0.90 ssHolds(X29,X30)). % 4.26/0.90 cnf(a106, assumption, % 4.26/0.90 X141 = X29). % 4.26/0.90 cnf(a107, assumption, % 4.26/0.90 X142 = X30). % 4.26/0.90 cnf(c109, plain, % 4.26/0.90 ~ssSingleRole(singleRoleEntry(X142,authObj(X143,X144,X145))), % 4.26/0.90 inference(predicate_reduction, [assumptions([a106, a107])], [c107, c108])). % 4.26/0.90 % 4.26/0.90 cnf(c110, axiom, % 4.26/0.90 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N)))). % 4.26/0.90 cnf(a108, assumption, % 4.26/0.90 singleRoleEntry(X142,authObj(X143,X144,X145)) = singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))). % 4.26/0.90 cnf(c111, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a108])], [c109, c110])). % 4.26/0.90 cnf(c112, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a108])], [c109, c110])). % 4.26/0.90 % 4.26/0.90 cnf(c113, axiom, % 4.26/0.90 ssStandardPurchase(ssNB)). % 4.26/0.90 cnf(a109, assumption, % 4.26/0.90 X9 = ssNB). % 4.26/0.90 cnf(c114, plain, % 4.26/0.90 ~ssRequisition(X9,X10,X11,X12,X13,X14,X15,X16,X17), % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a109])], [c49, c113])). % 4.26/0.90 cnf(c115, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a109])], [c49, c113])). % 4.26/0.90 % 4.26/0.90 cnf(c116, axiom, % 4.26/0.90 ssRequisition(X148,X149,X150,X151,X152,X153,X154,X155,X156)). % 4.26/0.90 cnf(a110, assumption, % 4.26/0.90 X9 = X148). % 4.26/0.90 cnf(a111, assumption, % 4.26/0.90 X10 = X149). % 4.26/0.90 cnf(a112, assumption, % 4.26/0.90 X11 = X150). % 4.26/0.90 cnf(a113, assumption, % 4.26/0.90 X12 = X151). % 4.26/0.90 cnf(a114, assumption, % 4.26/0.90 X13 = X152). % 4.26/0.90 cnf(a115, assumption, % 4.26/0.90 X14 = X153). % 4.26/0.90 cnf(a116, assumption, % 4.26/0.90 X15 = X154). % 4.26/0.90 cnf(a117, assumption, % 4.26/0.90 X16 = X155). % 4.26/0.90 cnf(a118, assumption, % 4.26/0.90 X17 = X156). % 4.26/0.90 cnf(c117, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a110, a111, a112, a113, a114, a115, a116, a117, a118])], [c114, c116])). % 4.26/0.90 cnf(c118, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(strict_predicate_extension, [assumptions([a110, a111, a112, a113, a114, a115, a116, a117, a118])], [c114, c116])). % 4.26/0.90 % 4.26/0.90 cnf(c119, plain, % 4.26/0.90 $false, % 4.26/0.90 inference(constraint_solving, [ % 4.26/0.90 bind(X0, ssNB), % 4.26/0.90 bind(X1, X10), % 4.26/0.90 bind(X2, X11), % 4.26/0.90 bind(X3, ssI26), % 4.26/0.90 bind(X4, X14), % 4.26/0.90 bind(X5, X15), % 4.26/0.90 bind(X6, X16), % 4.26/0.90 bind(X7, X17), % 4.26/0.90 bind(X8, ssMUELLER), % 4.26/0.90 bind(X9, ssNB), % 4.26/0.90 bind(X10, X10), % 4.26/0.90 bind(X11, X11), % 4.26/0.90 bind(X12, ssINF), % 4.26/0.90 bind(X13, ssI26), % 4.26/0.90 bind(X14, X14), % 4.26/0.90 bind(X15, X15), % 4.26/0.90 bind(X16, X16), % 4.26/0.90 bind(X17, X17), % 4.26/0.90 bind(X18, ssMUELLER), % 4.26/0.90 bind(X19, ssM_BANF_EKG), % 4.26/0.90 bind(X20, ssEKGRP), % 4.26/0.90 bind(X21, ssI26), % 4.26/0.90 bind(X22, ssMUELLER), % 4.26/0.90 bind(X23, ssM_BANF_EKG), % 4.26/0.90 bind(X24, ssEKGRP), % 4.26/0.90 bind(X25, ssI26), % 4.26/0.90 bind(X26, X34), % 4.26/0.90 bind(X27, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X28, X35), % 4.26/0.90 bind(X29, ssMUELLER), % 4.26/0.90 bind(X30, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X31, ssM_BANF_EKG), % 4.26/0.90 bind(X32, ssEKGRP), % 4.26/0.90 bind(X33, ssI26), % 4.26/0.90 bind(X34, X34), % 4.26/0.90 bind(X35, X35), % 4.26/0.90 bind(X36, ssMUELLER), % 4.26/0.90 bind(X37, ssM_BANF_BSA), % 4.26/0.90 bind(X38, ssBSART), % 4.26/0.90 bind(X39, ssNB), % 4.26/0.90 bind(X40, ssMUELLER), % 4.26/0.90 bind(X41, ssM_BANF_BSA), % 4.26/0.90 bind(X42, ssBSART), % 4.26/0.90 bind(X43, ssSTAR), % 4.26/0.90 bind(X44, X52), % 4.26/0.90 bind(X45, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X46, X53), % 4.26/0.90 bind(X47, ssMUELLER), % 4.26/0.90 bind(X48, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X49, ssM_BANF_BSA), % 4.26/0.90 bind(X50, ssBSART), % 4.26/0.90 bind(X51, ssSTAR), % 4.26/0.90 bind(X52, X52), % 4.26/0.90 bind(X53, X53), % 4.26/0.90 bind(X54, ssMUELLER), % 4.26/0.90 bind(X55, ssM_BANF_WRK), % 4.26/0.90 bind(X56, ssWERKS), % 4.26/0.90 bind(X57, ssINF), % 4.26/0.90 bind(X58, ssMUELLER), % 4.26/0.90 bind(X59, ssM_BANF_WRK), % 4.26/0.90 bind(X60, ssWERKS), % 4.26/0.90 bind(X61, ssINF), % 4.26/0.90 bind(X62, X70), % 4.26/0.90 bind(X63, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X64, X71), % 4.26/0.90 bind(X65, ssMUELLER), % 4.26/0.90 bind(X66, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X67, ssM_BANF_WRK), % 4.26/0.90 bind(X68, ssWERKS), % 4.26/0.90 bind(X69, ssINF), % 4.26/0.90 bind(X70, X70), % 4.26/0.90 bind(X71, X71), % 4.26/0.90 bind(X72, ssMUELLER), % 4.26/0.90 bind(X73, ssI26), % 4.26/0.90 bind(X74, ssNB), % 4.26/0.90 bind(X75, ssINF), % 4.26/0.90 bind(X76, ssMUELLER), % 4.26/0.90 bind(X77, ssM_BANF_EKG), % 4.26/0.90 bind(X78, ssACTVT), % 4.26/0.90 bind(X79, np__1), % 4.26/0.90 bind(X80, ssMUELLER), % 4.26/0.90 bind(X81, ssM_BANF_EKG), % 4.26/0.90 bind(X82, ssACTVT), % 4.26/0.90 bind(X83, ssSTAR), % 4.26/0.90 bind(X84, X92), % 4.26/0.90 bind(X85, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X86, X93), % 4.26/0.90 bind(X87, ssMUELLER), % 4.26/0.90 bind(X88, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X89, ssM_BANF_EKG), % 4.26/0.90 bind(X90, ssACTVT), % 4.26/0.90 bind(X91, ssSTAR), % 4.26/0.90 bind(X92, X92), % 4.26/0.90 bind(X93, X93), % 4.26/0.90 bind(X94, ssMUELLER), % 4.26/0.90 bind(X95, ssM_BANF_BSA), % 4.26/0.90 bind(X96, ssACTVT), % 4.26/0.90 bind(X97, np__1), % 4.26/0.90 bind(X98, ssMUELLER), % 4.26/0.90 bind(X99, ssM_BANF_BSA), % 4.26/0.90 bind(X100, ssACTVT), % 4.26/0.90 bind(X101, ssSTAR), % 4.26/0.90 bind(X102, X110), % 4.26/0.90 bind(X103, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X104, X111), % 4.26/0.90 bind(X105, ssMUELLER), % 4.26/0.90 bind(X106, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X107, ssM_BANF_BSA), % 4.26/0.90 bind(X108, ssACTVT), % 4.26/0.90 bind(X109, ssSTAR), % 4.26/0.90 bind(X110, X110), % 4.26/0.90 bind(X111, X111), % 4.26/0.90 bind(X112, ssMUELLER), % 4.26/0.90 bind(X113, ssM_BANF_WRK), % 4.26/0.90 bind(X114, ssACTVT), % 4.26/0.90 bind(X115, np__1), % 4.26/0.90 bind(X116, ssMUELLER), % 4.26/0.90 bind(X117, ssM_BANF_WRK), % 4.26/0.90 bind(X118, ssACTVT), % 4.26/0.90 bind(X119, np__1), % 4.26/0.90 bind(X120, X128), % 4.26/0.90 bind(X121, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X122, X129), % 4.26/0.90 bind(X123, ssMUELLER), % 4.26/0.90 bind(X124, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X125, ssM_BANF_WRK), % 4.26/0.90 bind(X126, ssACTVT), % 4.26/0.90 bind(X127, np__1), % 4.26/0.90 bind(X128, X128), % 4.26/0.90 bind(X129, X129), % 4.26/0.90 bind(X130, ssMUELLER), % 4.26/0.90 bind(X131, ssS_TCODE), % 4.26/0.90 bind(X132, ssTCD), % 4.26/0.90 bind(X133, ssME51N), % 4.26/0.90 bind(X134, ssMUELLER), % 4.26/0.90 bind(X135, ssS_TCODE), % 4.26/0.90 bind(X136, ssTCD), % 4.26/0.90 bind(X137, ssME51N), % 4.26/0.90 bind(X138, X146), % 4.26/0.90 bind(X139, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X140, X147), % 4.26/0.90 bind(X141, ssMUELLER), % 4.26/0.90 bind(X142, ssZBANF_WRK_INF_ED), % 4.26/0.90 bind(X143, ssS_TCODE), % 4.26/0.90 bind(X144, ssTCD), % 4.26/0.90 bind(X145, ssME51N), % 4.26/0.90 bind(X146, X146), % 4.26/0.90 bind(X147, X147), % 4.26/0.90 bind(X148, ssNB), % 4.26/0.90 bind(X149, X10), % 4.26/0.90 bind(X150, X11), % 4.26/0.90 bind(X151, ssINF), % 4.26/0.90 bind(X152, ssI26), % 4.26/0.90 bind(X153, X14), % 4.26/0.90 bind(X154, X15), % 4.26/0.90 bind(X155, X16), % 4.26/0.90 bind(X156, X17) % 4.26/0.90 ], % 4.26/0.90 [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58, a59, a60, a61, a62, a63, a64, a65, a66, a67, a68, a69, a70, a71, a72, a73, a74, a75, a76, a77, a78, a79, a80, a81, a82, a83, a84, a85, a86, a87, a88, a89, a90, a91, a92, a93, a94, a95, a96, a97, a98, a99, a100, a101, a102, a103, a104, a105, a106, a107, a108, a109, a110, a111, a112, a113, a114, a115, a116, a117, a118])). % 4.26/0.90 % 4.26/0.90 % SZS output end IncompleteProof %------------------------------------------------------------------------------