%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n014.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:04:23 AM UTC 2026 % Result : Theorem 71.45s 71.72s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.34 % Computer : n014.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Mon Sep 7 13:51:11 UTC 2026 % 0.09/0.34 % CPUTime : % 0.14/0.44 start to proof:theBenchmark % 71.45/71.70 %------------------------------------------- % 71.45/71.70 % File :CSE---1.7 % 71.45/71.70 % Problem :theBenchmark % 71.45/71.70 % Transform :cnf % 71.45/71.70 % Format :tptp:raw % 71.45/71.70 % Command :java -jar mcs_scs.jar %d %s % 71.45/71.70 % 71.45/71.70 % Result :Theorem 71.072956s % 71.45/71.70 % Output :CNFRefutation 71.072956s % 71.45/71.70 %------------------------------------------- % 71.45/71.70 %-------------------------------------------------------------------------- % 71.45/71.70 % File : MGT067+1 : TPTP v9.3.0. Released v5.5.0. % 71.45/71.70 % Domain : Management % 71.45/71.70 % Problem : Authorization to create requisitions % 71.45/71.70 % Version : Especial. % 71.45/71.70 % English : A first-order theory representing the formalization of an % 71.45/71.70 % SAP R/3 authorization and process setup together with business % 71.45/71.70 % policies for a purchase process. % 71.45/71.70 % 71.45/71.70 % Refs : % 71.45/71.70 % Source : [TPTP] % 71.45/71.70 % Names : % 71.45/71.70 % 71.45/71.70 % Status : Theorem % 71.45/71.70 % Rating : 0.60 v9.3.0, 0.25 v9.1.0, 0.27 v9.0.0, 0.19 v8.2.0, 0.27 v8.1.0, 0.21 v7.5.0, 0.24 v7.4.0, 0.19 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.29 v6.3.0, 0.31 v6.2.0, 0.36 v6.1.0, 0.28 v6.0.0, 0.50 v5.5.0 % 71.45/71.70 % Syntax : Number of formulae : 158 ( 127 unt; 0 def) % 71.45/71.70 % Number of atoms : 330 ( 0 equ) % 71.45/71.70 % Maximal formula atoms : 20 ( 2 avg) % 71.45/71.70 % Number of connectives : 196 ( 24 ~; 8 |; 134 &) % 71.45/71.70 % ( 0 <=>; 30 =>; 0 <=; 0 <~>) % 71.45/71.70 % Maximal formula depth : 27 ( 3 avg) % 71.45/71.70 % Maximal term depth : 3 ( 1 avg) % 71.45/71.70 % Number of predicates : 15 ( 15 usr; 0 prp; 1-13 aty) % 71.45/71.70 % Number of functors : 80 ( 80 usr; 73 con; 0-3 aty) % 71.45/71.70 % Number of variables : 181 ( 160 !; 21 ?) % 71.45/71.70 % SPC : FOF_THM_RFO_NEQ % 71.45/71.70 % 71.45/71.70 % Comments : Taken from the SPASS web site % 71.45/71.70 % http://www.spass-prover.org/prototypes/index.html % 71.45/71.70 %-------------------------------------------------------------------------- % 71.45/71.70 fof(ax1,axiom, % 71.45/71.70 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssS_TCODE,ssTCD,ssME51N))) ). % 71.45/71.70 % 71.45/71.70 fof(ax2,axiom, % 71.45/71.70 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssS_TCODE,ssTCD,ssME52N))) ). % 71.45/71.70 % 71.45/71.70 fof(ax3,axiom, % 71.45/71.70 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssS_TCODE,ssTCD,ssME53N))) ). % 71.45/71.70 % 71.45/71.70 fof(ax4,axiom, % 71.45/71.70 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))) ). % 71.45/71.70 % 71.45/71.70 fof(ax5,axiom, % 71.45/71.70 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssM_BANF_WRK,ssACTVT,np__2))) ). % 71.45/71.70 % 71.45/71.70 fof(ax6,axiom, % 71.45/71.70 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssM_BANF_WRK,ssACTVT,np__3))) ). % 71.45/71.70 % 71.45/71.70 fof(ax7,axiom, % 71.45/71.70 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssM_BANF_WRK,ssWERKS,ssADSU))) ). % 71.45/71.70 % 71.45/71.70 fof(ax8,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax9,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax10,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax11,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_ADSU_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))) ). % 71.45/71.71 % 71.45/71.71 %----ZBANF_WRK_INF_ED % 71.45/71.71 %----Role to create requisitions for plant INF, purchase group I26 % 71.45/71.71 fof(ax12,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))) ). % 71.45/71.71 % 71.45/71.71 fof(ax13,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax14,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax15,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax16,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) ). % 71.45/71.71 % 71.45/71.71 fof(ax17,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax18,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax19,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax20,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))) ). % 71.45/71.71 % 71.45/71.71 %----ZRELEASE_WRK_INF_BASE % 71.45/71.71 %----Permits access to release and view requisitions, but does not specify a % 71.45/71.71 %----release group or code % 71.45/71.71 fof(ax21,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssS_TCODE,ssTCD,ssME53N))) ). % 71.45/71.71 % 71.45/71.71 fof(ax22,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssS_TCODE,ssTCD,ssME54N))) ). % 71.45/71.71 % 71.45/71.71 fof(ax23,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_BSA,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax24,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_BSA,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax25,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_BSA,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax26,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_BSA,ssBSART,ssNB))) ). % 71.45/71.71 % 71.45/71.71 fof(ax27,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_EKG,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax28,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_EKG,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax29,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_EKG,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax30,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))) ). % 71.45/71.71 % 71.45/71.71 fof(ax31,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_WRK,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax32,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_WRK,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax33,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_WRK,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax34,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_BASE,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) ). % 71.45/71.71 % 71.45/71.71 %----Extension 1 to role RELEASE_INF_BASE: % 71.45/71.71 %----Permits the release of requisitions with release group 01 (=single row % 71.45/71.71 %----release) and code W1 (=cost center release) % 71.45/71.71 fof(ax35,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_W1,authObj(ssM_EINK_FRG,ssFRGCO,ssW1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax36,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_W1,authObj(ssM_EINK_FRG,ssFRGGR,ssRGRP_01))) ). % 71.45/71.71 % 71.45/71.71 %----Extension 2 to role RELEASE_INF_BASE: % 71.45/71.71 %----Permits the release of requisitions with release group 01 (=single row % 71.45/71.71 %----release) and code W2 (=management) % 71.45/71.71 fof(ax37,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_W2,authObj(ssM_EINK_FRG,ssFRGCO,ssW2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax38,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZRELEASE_WRK_INF_W2,authObj(ssM_EINK_FRG,ssFRGGR,ssRGRP_01))) ). % 71.45/71.71 % 71.45/71.71 %----ZORDER_WRK_INF_BASE % 71.45/71.71 %----Base role to create/change/view orders % 71.45/71.71 fof(ax39,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssS_TCODE,ssTCD,ssME21N))) ). % 71.45/71.71 % 71.45/71.71 fof(ax40,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssS_TCODE,ssTCD,ssME22N))) ). % 71.45/71.71 % 71.45/71.71 fof(ax41,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssS_TCODE,ssTCD,ssME23N))) ). % 71.45/71.71 % 71.45/71.71 fof(ax42,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKO,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax43,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKO,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax44,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKO,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax45,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKO,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax46,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKO,ssACTVT,np__9))) ). % 71.45/71.71 % 71.45/71.71 fof(ax47,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKO,ssEKORG,ssINF))) ). % 71.45/71.71 % 71.45/71.71 fof(ax48,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_BSA,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax49,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_BSA,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax50,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_BSA,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax51,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_BSA,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax52,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_BSA,ssACTVT,np__9))) ). % 71.45/71.71 % 71.45/71.71 fof(ax53,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BANF_BSA,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax54,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_WRK,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax55,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_WRK,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax56,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_WRK,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax57,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_WRK,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax58,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_WRK,ssACTVT,np__9))) ). % 71.45/71.71 % 71.45/71.71 fof(ax59,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_WRK,ssWERKS,ssINF))) ). % 71.45/71.71 % 71.45/71.71 fof(ax60,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKG,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax61,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKG,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax62,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKG,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax63,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKG,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax64,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKG,ssACTVT,np__9))) ). % 71.45/71.71 % 71.45/71.71 fof(ax65,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_BASE,authObj(ssM_BEST_EKG,ssEKGRP,ssI26))) ). % 71.45/71.71 % 71.45/71.71 %----Extension 1: % 71.45/71.71 %---- -> direct order allowed: transaction code ME21NOFF, but % 71.45/71.71 %---- - limit to office material, % 71.45/71.71 %---- - limit the amount of money % 71.45/71.71 fof(ax66,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_OFFICE,authObj(ssS_TCODE,ssTCD,ssME21NOFF))) ). % 71.45/71.71 % 71.45/71.71 fof(ax67,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_OFFICE,authObj(ssM_EINK_MKL,ssMATKL,ssB0002))) ). % 71.45/71.71 % 71.45/71.71 fof(ax68,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_OFFICE,authObj(ssM_EINK_GWT,ssGSWRT,ssLESS_EQUAL_1000_EUR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax69,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_OFFICE,authObj(ssM_BEST_BSA,ssBSART,ssDIRECT))) ). % 71.45/71.71 % 71.45/71.71 fof(ax70,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_OFFICE,authObj(ssM_BANF_BSA,ssBSART,ssDIRECT))) ). % 71.45/71.71 % 71.45/71.71 %----Extension 2: % 71.45/71.71 %---- - no limits - % 71.45/71.71 fof(ax71,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_ALL,authObj(ssM_EINK_MKL,ssMATKL,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax72,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_ALL,authObj(ssM_EINK_GWT,ssGSWRT,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax73,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_ALL,authObj(ssM_BEST_BSA,ssBSART,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax74,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_INF_TYPE_ALL,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 %----ZORDER_WRK_ADSU_ED % 71.45/71.71 %----Order role for plant ADSU % 71.45/71.71 fof(ax75,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssS_TCODE,ssTCD,ssME21N))) ). % 71.45/71.71 % 71.45/71.71 fof(ax76,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKO,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax77,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKO,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax78,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKO,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax79,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKO,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax80,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKO,ssACTVT,np__9))) ). % 71.45/71.71 % 71.45/71.71 fof(ax81,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKO,ssEKORG,ssADSU))) ). % 71.45/71.71 % 71.45/71.71 fof(ax82,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_BSA,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax83,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_BSA,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax84,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_BSA,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax85,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_BSA,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax86,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_BSA,ssACTVT,np__9))) ). % 71.45/71.71 % 71.45/71.71 fof(ax87,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_BSA,ssBSART,ssNB))) ). % 71.45/71.71 % 71.45/71.71 fof(ax88,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BANF_BSA,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax89,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BANF_BSA,ssBSART,ssNB))) ). % 71.45/71.71 % 71.45/71.71 fof(ax90,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_WRK,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax91,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_WRK,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax92,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_WRK,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax93,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_WRK,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax94,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_WRK,ssACTVT,np__9))) ). % 71.45/71.71 % 71.45/71.71 fof(ax95,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_WRK,ssWERKS,ssADSU))) ). % 71.45/71.71 % 71.45/71.71 fof(ax96,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKG,ssACTVT,np__1))) ). % 71.45/71.71 % 71.45/71.71 fof(ax97,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKG,ssACTVT,np__2))) ). % 71.45/71.71 % 71.45/71.71 fof(ax98,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKG,ssACTVT,np__3))) ). % 71.45/71.71 % 71.45/71.71 fof(ax99,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKG,ssACTVT,np__8))) ). % 71.45/71.71 % 71.45/71.71 fof(ax100,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKG,ssACTVT,np__9))) ). % 71.45/71.71 % 71.45/71.71 fof(ax101,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_BEST_EKG,ssEKGRP,ssI26))) ). % 71.45/71.71 % 71.45/71.71 fof(ax102,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_EINK_MKL,ssMATKL,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 fof(ax103,axiom, % 71.45/71.71 ssSingleRole(singleRoleEntry(ssZORDER_WRK_ADSU_ED,authObj(ssM_EINK_GWT,ssGSWRT,ssSTAR))) ). % 71.45/71.71 % 71.45/71.71 %----Composite Roles % 71.45/71.71 %----Permits releasing of requisitions: plant INF, single position release, % 71.45/71.71 %----release code W1 (cost center) % 71.45/71.71 fof(ax104,axiom, % 71.45/71.71 ssCompositeRole(compositeRoleEntry(ssZRELEASE_WRK_INF_W1_MULTI,ssZRELEASE_WRK_INF_BASE)) ). % 71.45/71.71 % 71.45/71.71 fof(ax105,axiom, % 71.45/71.71 ssCompositeRole(compositeRoleEntry(ssZRELEASE_WRK_INF_W1_MULTI,ssZRELEASE_WRK_INF_W1)) ). % 71.45/71.71 % 71.45/71.71 %----Permits releasing of requisitions: plant INF, single position release, % 71.45/71.71 %----release code W2 (management) % 71.45/71.71 fof(ax106,axiom, % 71.45/71.71 ssCompositeRole(compositeRoleEntry(ssZRELEASE_WRK_INF_W2_MULTI,ssZRELEASE_WRK_INF_BASE)) ). % 71.45/71.71 % 71.45/71.71 fof(ax107,axiom, % 71.45/71.71 ssCompositeRole(compositeRoleEntry(ssZRELEASE_WRK_INF_W2_MULTI,ssZRELEASE_WRK_INF_W2)) ). % 71.45/71.71 % 71.45/71.71 %----Create arbitrary orders % 71.45/71.71 fof(ax108,axiom, % 71.45/71.71 ssCompositeRole(compositeRoleEntry(ssZORDER_WRK_INF_ALL,ssZORDER_WRK_INF_BASE)) ). % 71.45/71.71 % 71.45/71.71 fof(ax109,axiom, % 71.45/71.71 ssCompositeRole(compositeRoleEntry(ssZORDER_WRK_INF_ALL,ssZORDER_WRK_INF_TYPE_ALL)) ). % 71.45/71.71 % 71.45/71.71 %----Create orders only for office material with limited amount of money % 71.45/71.71 fof(ax110,axiom, % 71.45/71.71 ssCompositeRole(compositeRoleEntry(ssZORDER_WRK_INF_OFFICE,ssZORDER_WRK_INF_BASE)) ). % 71.45/71.71 % 71.45/71.71 fof(ax111,axiom, % 71.45/71.71 ssCompositeRole(compositeRoleEntry(ssZORDER_WRK_INF_OFFICE,ssZORDER_WRK_INF_TYPE_OFFICE)) ). % 71.45/71.71 % 71.45/71.71 %----Assign Roles to Users % 71.45/71.71 fof(ax112,axiom, % 71.45/71.71 ssHolds(ssKAISER,ssZRELEASE_WRK_INF_W1_MULTI) ). % 71.45/71.71 % 71.45/71.71 fof(ax113,axiom, % 71.45/71.71 ssHolds(ssMEIER,ssZRELEASE_WRK_INF_W2_MULTI) ). % 71.45/71.71 % 71.45/71.71 %----Create requisitions % 71.45/71.71 fof(ax114,axiom, % 71.45/71.71 ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED) ). % 71.45/71.71 % 71.45/71.71 %----Create requisitions % 71.45/71.71 fof(ax115,axiom, % 71.45/71.71 ssHolds(ssSCHMITT,ssZORDER_WRK_INF_ALL) ). % 71.45/71.71 % 71.45/71.71 %----Release requisitions with code W1 % 71.45/71.71 fof(ax116,axiom, % 71.45/71.71 ssHolds(ssLAMOTTE,ssZORDER_WRK_INF_OFFICE) ). % 71.45/71.71 % 71.45/71.71 fof(ax117,axiom, % 71.45/71.71 ssDirectPurchase(ssDIRECT) ). % 71.45/71.71 % 71.45/71.71 fof(ax118,axiom, % 71.45/71.71 ssStandardPurchase(ssNB) ). % 71.45/71.71 % 71.45/71.71 fof(ax119,axiom, % 71.45/71.71 ! [U] : % 71.45/71.71 ~ ( ssDirectPurchase(U) % 71.45/71.71 & ssStandardPurchase(U) ) ). % 71.45/71.71 % 71.45/71.71 %----Code Layer % 71.45/71.71 %----Customizing: Release Strategy % 71.45/71.71 %----Release Requirements % 71.45/71.71 fof(ax120,axiom, % 71.45/71.71 ssReleaseRequirement(ssKF,ssRGRP_01,ssW1) ). % 71.45/71.71 % 71.45/71.72 fof(ax121,axiom, % 71.45/71.72 ssReleaseRequirement(ssVF,ssRGRP_01,ssW1) ). % 71.45/71.72 % 71.45/71.72 fof(ax122,axiom, % 71.45/71.72 ssReleaseRequirement(ssVF,ssRGRP_01,ssW2) ). % 71.45/71.72 % 71.45/71.72 %----E.g. ReleaseStrategy(cost center release [KF]/management release [VF], % 71.45/71.72 %----release group 01, class(FRG_EBAN, property(...))) % 71.45/71.72 fof(ax123,axiom, % 71.45/71.72 ssReleaseStrategy(ssKF,ssRGRP_01,class(ssFRG_EBAN,property(ssFRG_CEBAN_EKGRP,ssI26))) ). % 71.45/71.72 % 71.45/71.72 fof(ax124,axiom, % 71.45/71.72 ssReleaseStrategy(ssKF,ssRGRP_01,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssINF))) ). % 71.45/71.72 % 71.45/71.72 fof(ax125,axiom, % 71.45/71.72 ssReleaseStrategy(ssKF,ssRGRP_01,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssGREATER_1000_LESS_10000_EUR))) ). % 71.45/71.72 % 71.45/71.72 fof(ax126,axiom, % 71.45/71.72 ssReleaseStrategy(ssVF,ssRGRP_01,class(ssFRG_EBAN,property(ssFRG_CEBAN_EKGRP,ssI26))) ). % 71.45/71.72 % 71.45/71.72 fof(ax127,axiom, % 71.45/71.72 ssReleaseStrategy(ssVF,ssRGRP_01,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssINF))) ). % 71.45/71.72 % 71.45/71.72 fof(ax128,axiom, % 71.45/71.72 ssReleaseStrategy(ssVF,ssRGRP_01,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssGREATER_10000_EUR))) ). % 71.45/71.72 % 71.45/71.72 fof(ax129,axiom, % 71.45/71.72 ! [U,V] : % 71.45/71.72 ( ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssINF))) % 71.45/71.72 => ( ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssADSU))) % 71.45/71.72 & ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssGRSU))) ) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax130,axiom, % 71.45/71.72 ! [U,V] : % 71.45/71.72 ( ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssGRSU))) % 71.45/71.72 => ( ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssADSU))) % 71.45/71.72 & ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssINF))) ) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax131,axiom, % 71.45/71.72 ! [U,V] : % 71.45/71.72 ( ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssADSU))) % 71.45/71.72 => ( ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssINF))) % 71.45/71.72 & ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_WERKS,ssGRSU))) ) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax132,axiom, % 71.45/71.72 ! [U,V] : % 71.45/71.72 ( ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssGREATER_1000_LESS_10000_EUR))) % 71.45/71.72 => ( ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssGREATER_10000_EUR))) % 71.45/71.72 & ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssLESS_EQUAL_1000_EUR))) ) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax133,axiom, % 71.45/71.72 ! [U,V] : % 71.45/71.72 ( ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssGREATER_10000_EUR))) % 71.45/71.72 => ( ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssGREATER_1000_LESS_10000_EUR))) % 71.45/71.72 & ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssLESS_EQUAL_1000_EUR))) ) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax134,axiom, % 71.45/71.72 ! [U,V] : % 71.45/71.72 ( ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssLESS_EQUAL_1000_EUR))) % 71.45/71.72 => ( ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssGREATER_1000_LESS_10000_EUR))) % 71.45/71.72 & ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_GSWRT,ssGREATER_10000_EUR))) ) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax135,axiom, % 71.45/71.72 ! [U,V] : % 71.45/71.72 ( ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_EKGRP,ssI26))) % 71.45/71.72 => ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_EKGRP,ssI27))) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax136,axiom, % 71.45/71.72 ! [U,V] : % 71.45/71.72 ( ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_EKGRP,ssI27))) % 71.45/71.72 => ~ ssReleaseStrategy(U,V,class(ssFRG_EBAN,property(ssFRG_CEBAN_EKGRP,ssI26))) ) ). % 71.45/71.72 % 71.45/71.72 %----Access() % 71.45/71.72 %----Check of an authorization object with its value, the user profile must % 71.45/71.72 %----have the same authorization object with an equal value or STAR % 71.45/71.72 fof(ax137,axiom, % 71.45/71.72 ! [U,V,W,X] : % 71.45/71.72 ( ssUserProfile(userProfileEntry(U,authObj(V,W,X))) % 71.45/71.72 => ssAccess(U,authObj(V,W,X)) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax138,axiom, % 71.45/71.72 ! [U,V,W,X] : % 71.45/71.72 ( ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR))) % 71.45/71.72 => ssAccess(U,authObj(V,W,X)) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax139,axiom, % 71.45/71.72 ! [U,V,W] : % 71.45/71.72 ( ( ssUserProfile(userProfileEntry(U,authObj(V,W,ssGREATER_1000_LESS_10000_EUR))) % 71.45/71.72 | ssUserProfile(userProfileEntry(U,authObj(V,W,ssGREATER_10000_EUR))) ) % 71.45/71.72 => ssAccess(U,authObj(V,W,ssLESS_EQUAL_1000_EUR)) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax140,axiom, % 71.45/71.72 ! [U,V,W] : % 71.45/71.72 ( ssUserProfile(userProfileEntry(U,authObj(V,W,ssGREATER_10000_EUR))) % 71.45/71.72 => ssAccess(U,authObj(V,W,ssGREATER_1000_LESS_10000_EUR)) ) ). % 71.45/71.72 % 71.45/71.72 %----Profile/(Single,Composite)Role -> Userprofile() % 71.45/71.72 %----A composite role contains other roles. Each authorization in a profile or % 71.45/71.72 %----single/composite role will be inserted into the user profile. % 71.45/71.72 fof(ax141,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1] : % 71.45/71.72 ( ( ( ssProfile(profileEntry(V,authObj(Y,Z,X1))) % 71.45/71.72 & ssHolds(U,V) ) % 71.45/71.72 | ( ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1))) % 71.45/71.72 & ssHolds(U,W) ) % 71.45/71.72 | ( ssCompositeRole(compositeRoleEntry(X,W)) % 71.45/71.72 & ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1))) % 71.45/71.72 & ssHolds(U,X) ) ) % 71.45/71.72 => ssUserProfile(userProfileEntry(U,authObj(Y,Z,X1))) ) ). % 71.45/71.72 % 71.45/71.72 %----Abstraction % 71.45/71.72 %----ME51N - Create Requisitions % 71.45/71.72 fof(ax142,axiom, % 71.45/71.72 ! [U,V,W,X] : % 71.45/71.72 ( ( ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME51N)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X)) ) % 71.45/71.72 => ssAccess(U,ssME51N) ) ). % 71.45/71.72 % 71.45/71.72 %----ME52N - Change Requisitions % 71.45/71.72 fof(ax143,axiom, % 71.45/71.72 ! [U,V,W,X] : % 71.45/71.72 ( ( ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME52N)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X)) ) % 71.45/71.72 => ssAccess(U,ssME52N) ) ). % 71.45/71.72 % 71.45/71.72 %----ME53N - View Requisitions % 71.45/71.72 fof(ax144,axiom, % 71.45/71.72 ! [U,V,W,X] : % 71.45/71.72 ( ( ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME53N)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__3)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__3)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__3)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X)) ) % 71.45/71.72 => ssAccess(U,ssME53N) ) ). % 71.45/71.72 % 71.45/71.72 %----ME54N - Release Requisitions % 71.45/71.72 fof(ax145,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z] : % 71.45/71.72 ( ( ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME54N)) % 71.45/71.72 & ssAccess(U,ssME53N) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X)) % 71.45/71.72 & ssAccess(U,authObj(ssM_EINK_FRG,ssFRGGR,Y)) % 71.45/71.72 & ssAccess(U,authObj(ssM_EINK_FRG,ssFRGCO,Z)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__2)) ) % 71.45/71.72 => ssAccess(U,ssME54N) ) ). % 71.45/71.72 % 71.45/71.72 %----ME21N - Create Order % 71.45/71.72 fof(ax146,axiom, % 71.45/71.72 ! [U,V,W,X,Y] : % 71.45/71.72 ( ( ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME21N)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssEKORG,Y)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssWERKS,V)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssEKGRP,X)) ) % 71.45/71.72 => ssAccess(U,ssME21N) ) ). % 71.45/71.72 % 71.45/71.72 %----ME22N - Change Order % 71.45/71.72 fof(ax147,axiom, % 71.45/71.72 ! [U,V,W,X,Y] : % 71.45/71.72 ( ( ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME22N)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssEKORG,Y)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssWERKS,V)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssACTVT,np__2)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssEKGRP,X)) ) % 71.45/71.72 => ssAccess(U,ssME22N) ) ). % 71.45/71.72 % 71.45/71.72 %----ME23N - View Order % 71.45/71.72 fof(ax148,axiom, % 71.45/71.72 ! [U,V,W,X,Y] : % 71.45/71.72 ( ( ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME23N)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssACTVT,np__3)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssEKORG,Y)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssACTVT,np__3)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssACTVT,np__3)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssWERKS,V)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssACTVT,np__3)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssACTVT,np__8)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssACTVT,np__9)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssEKGRP,X)) ) % 71.45/71.72 => ssAccess(U,ssME23N) ) ). % 71.45/71.72 % 71.45/71.72 %----Business process steps % 71.45/71.72 %----Role: Requisition, includes create/change/view requisitions % 71.45/71.72 %----If there is a requisition and an user has access to create the % 71.45/71.72 %----requisition object, then the requisition object is created by this user % 71.45/71.72 fof(ax149,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1,X2,X3,X4] : % 71.45/71.72 ( ( ssRequisition(W,Z,X1,V,X,X2,Y,X3,X4) % 71.45/71.72 & ssStandardPurchase(W) % 71.45/71.72 & ssAccess(U,ssME51N) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X)) ) % 71.45/71.72 => ssRequisitionCreated(U,W,Z,X1,V,X,X2,Y,X3,X4) ) ). % 71.45/71.72 % 71.45/71.72 %----Role: Release % 71.45/71.72 fof(ax150,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6,X7,X8,X9] : % 71.45/71.72 ( ( ssRequisitionCreated(U,X,X2,X3,W,Y,Z,X1,X4,X9) % 71.45/71.72 & ssReleaseStrategy(X5,X6,class(X8,property(ssFRG_CEBAN_EKGRP,Y))) % 71.45/71.72 & ssReleaseStrategy(X5,X6,class(X8,property(ssFRG_CEBAN_WERKS,W))) % 71.45/71.72 & ssReleaseStrategy(X5,X6,class(X8,property(ssFRG_CEBAN_GSWRT,X4))) % 71.45/71.72 & ssReleaseRequirement(X5,X6,X7) % 71.45/71.72 & ssAccess(V,authObj(ssM_EINK_FRG,ssFRGGR,X6)) % 71.45/71.72 & ssAccess(V,authObj(ssM_EINK_FRG,ssFRGCO,X7)) % 71.45/71.72 & ssAccess(V,ssME54N) % 71.45/71.72 & ssAccess(V,authObj(ssM_BANF_WRK,ssWERKS,W)) % 71.45/71.72 & ssAccess(V,authObj(ssM_BANF_BSA,ssBSART,X)) % 71.45/71.72 & ssAccess(V,authObj(ssM_BANF_EKG,ssEKGRP,Y)) ) % 71.45/71.72 => ssRequisitionReleasedStep(V,X6,X5,X7,X,X2,X3,W,Y,Z,X1,X4,X9) ) ). % 71.45/71.72 % 71.45/71.72 %----No release strategy matches % 71.45/71.72 fof(ax151,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] : % 71.45/71.72 ( ( ssRequisitionCreated(U,W,X1,X2,V,X,Y,Z,X3,X6) % 71.45/71.72 & ( ~ ssReleaseStrategy(ssKF,X4,class(X5,property(ssFRG_CEBAN_EKGRP,X))) % 71.45/71.72 | ~ ssReleaseStrategy(ssKF,X4,class(X5,property(ssFRG_CEBAN_WERKS,V))) % 71.45/71.72 | ~ ssReleaseStrategy(ssKF,X4,class(X5,property(ssFRG_CEBAN_GSWRT,X3))) ) % 71.45/71.72 & ( ~ ssReleaseStrategy(ssVF,X4,class(X5,property(ssFRG_CEBAN_EKGRP,X))) % 71.45/71.72 | ~ ssReleaseStrategy(ssVF,X4,class(X5,property(ssFRG_CEBAN_WERKS,V))) % 71.45/71.72 | ~ ssReleaseStrategy(ssVF,X4,class(X5,property(ssFRG_CEBAN_GSWRT,X3))) ) ) % 71.45/71.72 => ssRequisitionReleased(U,W,X1,X2,V,X,Y,Z,X3,X6) ) ). % 71.45/71.72 % 71.45/71.72 %----Customizing: Definition of the release codes which are necessary to % 71.45/71.72 %----release a requisition (only if the strategy matches). % 71.45/71.72 fof(ax152,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1,X2,X3,X4,X5] : % 71.45/71.72 ( ( ssRequisitionReleasedStep(V,ssRGRP_01,ssKF,ssW1,X,X2,X3,W,Y,Z,X1,X4,X5) % 71.45/71.72 | ( ssRequisitionReleasedStep(U,ssRGRP_01,ssVF,ssW1,X,X2,X3,W,Y,Z,X1,X4,X5) % 71.45/71.72 & ssRequisitionReleasedStep(V,ssRGRP_01,ssVF,ssW2,X,X2,X3,W,Y,Z,X1,X4,X5) ) ) % 71.45/71.72 => ssRequisitionReleased(V,X,X2,X3,W,Y,Z,X1,X4,X5) ) ). % 71.45/71.72 % 71.45/71.72 %----Role: Order % 71.45/71.72 %----If a requisition has been created and has already been released and the % 71.45/71.72 %----user has access to create order objects, then the order (object) will be % 71.45/71.72 %----created by the user % 71.45/71.72 fof(ax153,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1,X2,X3,X4,X5] : % 71.45/71.72 ( ( ssRequisitionReleased(U,X,X2,X3,W,Y,X1,Z,X4,X5) % 71.45/71.72 & ssAccess(V,ssME21N) % 71.45/71.72 & ssAccess(V,ssME22N) % 71.45/71.72 & ssAccess(V,ssME23N) % 71.45/71.72 & ssAccess(V,authObj(ssM_BEST_WRK,ssWERKS,W)) % 71.45/71.72 & ssAccess(V,authObj(ssM_BANF_BSA,ssBSART,X)) % 71.45/71.72 & ssAccess(V,authObj(ssM_BEST_BSA,ssBSART,X)) % 71.45/71.72 & ssAccess(V,authObj(ssM_BEST_EKG,ssEKGRP,Y)) % 71.45/71.72 & ssAccess(V,authObj(ssM_BEST_EKO,ssEKORG,X1)) % 71.45/71.72 & ssAccess(V,authObj(ssM_EINK_MKL,ssMATKL,Z)) % 71.45/71.72 & ssAccess(V,authObj(ssM_EINK_GWT,ssGSWRT,X4)) ) % 71.45/71.72 => ssOrderCreated(V,X,X2,X3,W,Y,X1,Z,X4,X5) ) ). % 71.45/71.72 % 71.45/71.72 %----Special case: direct order (e.g. office material) % 71.45/71.72 fof(ax154,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1,X2,X3,X4,X5,X6] : % 71.45/71.72 ( ( ssRequisition(Y,X3,X4,X,Z,X2,X1,X5,X6) % 71.45/71.72 & ssDirectPurchase(Y) % 71.45/71.72 & ssAccess(U,authObj(ssM_EINK_MKL,ssMATKL,X1)) % 71.45/71.72 & ssAccess(U,authObj(ssM_EINK_GWT,ssGSWRT,X5)) % 71.45/71.72 & ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME21NOFF)) % 71.45/71.72 & ssAccess(U,ssME21N) % 71.45/71.72 & ssAccess(U,ssME22N) % 71.45/71.72 & ssAccess(U,ssME23N) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_WRK,ssWERKS,X)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,Y)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_BSA,ssBSART,Y)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKG,ssEKGRP,Z)) % 71.45/71.72 & ssAccess(U,authObj(ssM_BEST_EKO,ssEKORG,X2)) ) % 71.45/71.72 => ( ssOrderCreated(U,Y,X3,X4,X,Z,X2,X1,X5,X6) % 71.45/71.72 & ~ ssRequisitionCreated(V,Y,X3,X4,X,Z,X2,X1,X5,X6) % 71.45/71.72 & ~ ssRequisitionReleased(W,Y,X3,X4,X,Z,X2,X1,X5,X6) ) ) ). % 71.45/71.72 % 71.45/71.72 %----Business Policies % 71.45/71.72 %----There exists no user, which is allowed to perform the complete purchase % 71.45/71.72 %----process: % 71.45/71.72 % - create a requisition % 71.45/71.72 % - to release a requisition % 71.45/71.72 % - to create an order % 71.45/71.72 fof(ax155,axiom, % 71.45/71.72 ~ ? [U,V,W,X,Y,Z,X1,X2,X3,X4] : % 71.45/71.72 ( ssRequisition(Z,X1,X2,V,W,X,Y,X3,X4) % 71.45/71.72 => ( ssRequisitionCreated(U,Z,X1,X2,V,W,X,Y,X3,X4) % 71.45/71.72 & ssRequisitionReleased(U,Z,X1,X2,V,W,X,Y,X3,X4) % 71.45/71.72 & ssOrderCreated(U,Z,X1,X2,V,W,X,Y,X3,X4) ) ) ). % 71.45/71.72 % 71.45/71.72 %----It is prohibited to create orders greater than 1000 EUR without a % 71.45/71.72 %----requisition % 71.45/71.72 fof(ax156,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1,X2,X3] : % 71.45/71.72 ? [X4] : % 71.45/71.72 ( ssOrderCreated(U,Z,X1,X2,V,X,Y,W,ssGREATER_1000_LESS_10000_EUR,X3) % 71.45/71.72 => ssRequisitionCreated(X4,Z,X1,X2,V,X,Y,W,ssGREATER_1000_LESS_10000_EUR,X3) ) ). % 71.45/71.72 % 71.45/71.72 fof(ax157,axiom, % 71.45/71.72 ! [U,V,W,X,Y,Z,X1,X2,X3] : % 71.45/71.72 ? [X4] : % 71.45/71.72 ( ssOrderCreated(U,Z,X1,X2,V,X,Y,W,ssGREATER_10000_EUR,X3) % 71.45/71.72 => ssRequisitionCreated(X4,Z,X1,X2,V,X,Y,W,ssGREATER_10000_EUR,X3) ) ). % 71.45/71.72 % 71.45/71.72 fof(co1,conjecture, % 71.45/71.72 ? [U,V,W,X,Y,Z,X1,X2,X3] : % 71.45/71.72 ( ssRequisition(Y,Z,X1,U,ssINF,W,X,X2,X3) % 71.45/71.72 => ssRequisitionCreated(ssMUELLER,Y,Z,X1,ssINF,V,W,X,X2,X3) ) ). % 71.45/71.72 % 71.45/71.72 %------------------------------------------------------------------------------ % 71.45/71.72 %------------------------------------------- % 71.45/71.72 % Proof found % 71.45/71.72 % SZS status Theorem for theBenchmark % 71.45/71.72 % SZS output start Proof % 71.45/71.72 %ClaNum:178(EqnAxiom:0) % 71.45/71.72 %VarNum:782(SingletonVarNum:314) % 71.45/71.72 %MaxLitNum:20 % 71.45/71.72 %MaxfuncDepth:2 % 71.45/71.72 %SharedTerms:390 % 71.45/71.72 %goalClause: 128 % 71.45/71.72 %singleGoalClaCount:1 % 71.45/71.72 [1]P1(a1) % 71.45/71.72 [2]P4(a19) % 71.45/71.72 [3]P5(a20,a60) % 71.45/71.72 [4]P5(a36,a80) % 71.45/71.72 [5]P5(a49,a61) % 71.45/71.72 [6]P5(a62,a72) % 71.45/71.72 [7]P5(a37,a74) % 71.45/71.72 [16]P6(a38,a63,a64) % 71.45/71.72 [17]P6(a65,a63,a64) % 71.45/71.72 [18]P6(a65,a63,a69) % 71.45/71.72 [8]P2(f2(a60,a76)) % 71.45/71.72 [9]P2(f2(a60,a79)) % 71.45/71.72 [10]P2(f2(a80,a76)) % 71.45/71.72 [11]P2(f2(a80,a81)) % 71.45/71.72 [12]P2(f2(a72,a75)) % 71.45/71.72 [13]P2(f2(a72,a77)) % 71.45/71.72 [14]P2(f2(a74,a75)) % 71.45/71.72 [15]P2(f2(a74,a78)) % 71.45/71.72 [19]P9(a38,a63,f3(a21,f5(a22,a29))) % 71.45/71.72 [20]P9(a38,a63,f3(a21,f5(a27,a34))) % 71.45/71.72 [21]P9(a38,a63,f3(a21,f5(a28,a30))) % 71.45/71.72 [22]P9(a65,a63,f3(a21,f5(a22,a29))) % 71.45/71.72 [23]P9(a65,a63,f3(a21,f5(a27,a34))) % 71.45/71.72 [24]P9(a65,a63,f3(a21,f5(a28,a31))) % 71.45/71.72 [25]P10(f14(a70,f4(a66,a68,a39))) % 71.45/71.72 [26]P10(f14(a70,f4(a66,a68,a46))) % 71.45/71.72 [27]P10(f14(a70,f4(a66,a68,a47))) % 71.45/71.72 [28]P10(f14(a70,f4(a50,a15,a6))) % 71.45/71.72 [29]P10(f14(a70,f4(a50,a15,a9))) % 71.45/71.72 [30]P10(f14(a70,f4(a50,a15,a10))) % 71.45/71.72 [31]P10(f14(a70,f4(a50,a71,a16))) % 71.45/71.72 [32]P10(f14(a70,f4(a51,a15,a67))) % 71.45/71.72 [33]P10(f14(a70,f4(a51,a17,a67))) % 71.45/71.72 [34]P10(f14(a70,f4(a52,a15,a67))) % 71.45/71.72 [35]P10(f14(a70,f4(a52,a23,a29))) % 71.45/71.72 [36]P10(f14(a61,f4(a66,a68,a39))) % 71.45/71.72 [37]P10(f14(a61,f4(a50,a15,a6))) % 71.45/71.72 [38]P10(f14(a61,f4(a50,a15,a9))) % 71.45/71.72 [39]P10(f14(a61,f4(a50,a15,a10))) % 71.45/71.72 [40]P10(f14(a61,f4(a50,a71,a34))) % 71.45/71.72 [41]P10(f14(a61,f4(a51,a15,a67))) % 71.45/71.72 [42]P10(f14(a61,f4(a51,a17,a67))) % 71.45/71.72 [43]P10(f14(a61,f4(a52,a15,a67))) % 71.45/71.72 [44]P10(f14(a61,f4(a52,a23,a29))) % 71.45/71.72 [45]P10(f14(a76,f4(a66,a68,a47))) % 71.45/71.72 [46]P10(f14(a76,f4(a66,a68,a48))) % 71.45/71.72 [47]P10(f14(a76,f4(a50,a15,a9))) % 71.45/71.72 [48]P10(f14(a76,f4(a50,a15,a10))) % 71.45/71.72 [49]P10(f14(a76,f4(a50,a15,a11))) % 71.45/71.72 [50]P10(f14(a76,f4(a50,a71,a34))) % 71.45/71.72 [51]P10(f14(a76,f4(a51,a15,a9))) % 71.45/71.72 [52]P10(f14(a76,f4(a51,a15,a10))) % 71.45/71.72 [53]P10(f14(a76,f4(a51,a15,a11))) % 71.45/71.72 [54]P10(f14(a76,f4(a51,a17,a19))) % 71.45/71.72 [55]P10(f14(a76,f4(a52,a15,a9))) % 71.45/71.72 [56]P10(f14(a76,f4(a52,a15,a10))) % 71.45/71.72 [57]P10(f14(a76,f4(a52,a15,a11))) % 71.45/71.72 [58]P10(f14(a76,f4(a52,a23,a29))) % 71.45/71.72 [59]P10(f14(a79,f4(a53,a24,a64))) % 71.45/71.72 [60]P10(f14(a79,f4(a53,a26,a63))) % 71.45/71.72 [61]P10(f14(a81,f4(a53,a24,a69))) % 71.45/71.72 [62]P10(f14(a81,f4(a53,a26,a63))) % 71.45/71.72 [63]P10(f14(a75,f4(a66,a68,a40))) % 71.45/71.72 [64]P10(f14(a75,f4(a66,a68,a43))) % 71.45/71.72 [65]P10(f14(a75,f4(a66,a68,a45))) % 71.45/71.72 [66]P10(f14(a75,f4(a51,a15,a6))) % 71.45/71.72 [67]P10(f14(a75,f4(a54,a15,a6))) % 71.45/71.72 [68]P10(f14(a75,f4(a54,a15,a9))) % 71.45/71.72 [69]P10(f14(a75,f4(a54,a15,a10))) % 71.45/71.72 [70]P10(f14(a75,f4(a54,a15,a11))) % 71.45/71.72 [71]P10(f14(a75,f4(a54,a15,a12))) % 71.45/71.72 [72]P10(f14(a75,f4(a54,a25,a34))) % 71.45/71.72 [73]P10(f14(a75,f4(a55,a15,a6))) % 71.45/71.72 [74]P10(f14(a75,f4(a55,a15,a9))) % 71.45/71.72 [75]P10(f14(a75,f4(a55,a15,a10))) % 71.45/71.72 [76]P10(f14(a75,f4(a55,a15,a11))) % 71.45/71.72 [77]P10(f14(a75,f4(a55,a15,a12))) % 71.45/71.72 [78]P10(f14(a75,f4(a57,a15,a6))) % 71.45/71.72 [79]P10(f14(a75,f4(a57,a15,a9))) % 71.45/71.72 [80]P10(f14(a75,f4(a57,a15,a10))) % 71.45/71.72 [81]P10(f14(a75,f4(a57,a15,a11))) % 71.45/71.72 [82]P10(f14(a75,f4(a57,a15,a12))) % 71.45/71.72 [83]P10(f14(a75,f4(a57,a71,a34))) % 71.45/71.72 [84]P10(f14(a75,f4(a56,a15,a6))) % 71.45/71.72 [85]P10(f14(a75,f4(a56,a15,a9))) % 71.45/71.72 [86]P10(f14(a75,f4(a56,a15,a10))) % 71.45/71.72 [87]P10(f14(a75,f4(a56,a15,a11))) % 71.45/71.72 [88]P10(f14(a75,f4(a56,a15,a12))) % 71.45/71.72 [89]P10(f14(a75,f4(a56,a23,a29))) % 71.45/71.72 [90]P10(f14(a78,f4(a66,a68,a44))) % 71.45/71.72 [91]P10(f14(a78,f4(a51,a17,a1))) % 71.45/71.72 [92]P10(f14(a78,f4(a55,a17,a1))) % 71.45/71.72 [93]P10(f14(a78,f4(a58,a41,a18))) % 71.45/71.72 [94]P10(f14(a78,f4(a59,a32,a42))) % 71.45/71.72 [95]P10(f14(a77,f4(a51,a17,a67))) % 71.45/71.72 [96]P10(f14(a77,f4(a55,a17,a67))) % 71.45/71.72 [97]P10(f14(a77,f4(a58,a41,a67))) % 71.45/71.72 [98]P10(f14(a77,f4(a59,a32,a67))) % 71.45/71.72 [99]P10(f14(a73,f4(a66,a68,a40))) % 71.45/71.72 [100]P10(f14(a73,f4(a51,a15,a6))) % 71.45/71.72 [101]P10(f14(a73,f4(a51,a17,a19))) % 71.45/71.72 [102]P10(f14(a73,f4(a54,a15,a6))) % 71.45/71.72 [103]P10(f14(a73,f4(a54,a15,a9))) % 71.45/71.72 [104]P10(f14(a73,f4(a54,a15,a10))) % 71.45/71.72 [105]P10(f14(a73,f4(a54,a15,a11))) % 71.45/71.72 [106]P10(f14(a73,f4(a54,a15,a12))) % 71.45/71.72 [107]P10(f14(a73,f4(a54,a25,a16))) % 71.45/71.72 [108]P10(f14(a73,f4(a55,a15,a6))) % 71.45/71.72 [109]P10(f14(a73,f4(a55,a15,a9))) % 71.45/71.72 [110]P10(f14(a73,f4(a55,a15,a10))) % 71.45/71.72 [111]P10(f14(a73,f4(a55,a15,a11))) % 71.45/71.72 [112]P10(f14(a73,f4(a55,a15,a12))) % 71.45/71.72 [113]P10(f14(a73,f4(a55,a17,a19))) % 71.45/71.72 [114]P10(f14(a73,f4(a57,a15,a6))) % 71.45/71.72 [115]P10(f14(a73,f4(a57,a15,a9))) % 71.45/71.72 [116]P10(f14(a73,f4(a57,a15,a10))) % 71.45/71.72 [117]P10(f14(a73,f4(a57,a15,a11))) % 71.45/71.72 [118]P10(f14(a73,f4(a57,a15,a12))) % 71.45/71.72 [119]P10(f14(a73,f4(a57,a71,a16))) % 71.45/71.72 [120]P10(f14(a73,f4(a56,a15,a6))) % 71.45/71.72 [121]P10(f14(a73,f4(a56,a15,a9))) % 71.45/71.72 [122]P10(f14(a73,f4(a56,a15,a10))) % 71.45/71.72 [123]P10(f14(a73,f4(a56,a15,a11))) % 71.45/71.72 [124]P10(f14(a73,f4(a56,a15,a12))) % 71.45/71.72 [125]P10(f14(a73,f4(a56,a23,a29))) % 71.45/71.72 [126]P10(f14(a73,f4(a58,a41,a67))) % 71.45/71.72 [127]P10(f14(a73,f4(a59,a32,a67))) % 71.45/71.72 [128]~P11(a49,x1281,x1282,x1283,a34,x1284,x1285,x1286,x1287,x1288) % 71.45/71.72 [129]~P4(x1291)+~P1(x1291) % 71.45/71.72 [131]~P9(x1311,x1312,f3(a21,f5(a22,a29)))+~P9(x1311,x1312,f3(a21,f5(a22,a35))) % 71.45/71.72 [133]~P9(x1331,x1332,f3(a21,f5(a27,a34)))+~P9(x1331,x1332,f3(a21,f5(a27,a16))) % 71.45/71.72 [135]~P9(x1351,x1352,f3(a21,f5(a27,a16)))+~P9(x1351,x1352,f3(a21,f5(a27,a33))) % 71.45/71.72 [137]~P9(x1371,x1372,f3(a21,f5(a27,a34)))+~P9(x1371,x1372,f3(a21,f5(a27,a33))) % 71.45/71.72 [139]~P9(x1391,x1392,f3(a21,f5(a28,a30)))+~P9(x1391,x1392,f3(a21,f5(a28,a42))) % 71.45/71.72 [141]~P9(x1411,x1412,f3(a21,f5(a28,a42)))+~P9(x1411,x1412,f3(a21,f5(a28,a31))) % 71.45/71.72 [143]~P9(x1431,x1432,f3(a21,f5(a28,a31)))+~P9(x1431,x1432,f3(a21,f5(a28,a30))) % 71.45/71.72 [144]P3(x1441,f4(x1442,x1443,a42))+~P14(f82(x1441,f4(x1442,x1443,a30))) % 71.45/71.72 [145]P3(x1451,f4(x1452,x1453,a42))+~P14(f82(x1451,f4(x1452,x1453,a31))) % 71.45/71.72 [146]P3(x1461,f4(x1462,x1463,a30))+~P14(f82(x1461,f4(x1462,x1463,a31))) % 71.45/71.72 [147]P3(x1471,f4(x1472,x1473,x1474))+~P14(f82(x1471,f4(x1472,x1473,a67))) % 71.45/71.72 [148]P3(x1481,f4(x1482,x1483,x1484))+~P14(f82(x1481,f4(x1482,x1483,x1484))) % 71.45/71.72 [173]~P8(x1731,x1736,x1737,x1738,x1732,x1734,x1735,x1733,a30,x1739)+P11(f7(x1731,x1732,x1733,x1734,x1735,x1736,x1737,x1738,x1739),x1736,x1737,x1738,x1732,x1734,x1735,x1733,a30,x1739) % 71.45/71.72 [174]~P8(x1741,x1746,x1747,x1748,x1742,x1744,x1745,x1743,a31,x1749)+P11(f8(x1741,x1742,x1743,x1744,x1745,x1746,x1747,x1748,x1749),x1746,x1747,x1748,x1742,x1744,x1745,x1743,a31,x1749) % 71.45/71.72 [177]P12(x1771,x1772,x1773,x1774,x1775,x1776,x1777,x1778,x1779,x17710)+~P13(x1771,a63,a38,a64,x1772,x1773,x1774,x1775,x1776,x1777,x1778,x1779,x17710) % 71.45/71.72 [149]~P5(x1491,x1495)+P14(f82(x1491,f4(x1492,x1493,x1494)))+~P10(f14(x1495,f4(x1492,x1493,x1494))) % 71.45/71.72 [150]~P5(x1501,x1505)+P14(f82(x1501,f4(x1502,x1503,x1504)))+~P7(f13(x1505,f4(x1502,x1503,x1504))) % 71.45/71.72 [175]~P12(x1751,x1752,x1753,x1754,x1755,x1756,x1757,x1758,x1759,x17510)+~P8(x1751,x1752,x1753,x1754,x1755,x1756,x1757,x1758,x1759,x17510)+~P11(x1751,x1752,x1753,x1754,x1755,x1756,x1757,x1758,x1759,x17510) % 71.45/71.72 [178]P12(x1781,x1782,x1783,x1784,x1785,x1786,x1787,x1788,x1789,x17810)+~P13(x1781,a63,a65,a69,x1782,x1783,x1784,x1785,x1786,x1787,x1788,x1789,x17810)+~P13(x17811,a63,a65,a64,x1782,x1783,x1784,x1785,x1786,x1787,x1788,x1789,x17810) % 71.45/71.72 [151]~P5(x1511,x1515)+~P2(f2(x1515,x1516))+P14(f82(x1511,f4(x1512,x1513,x1514)))+~P10(f14(x1516,f4(x1512,x1513,x1514))) % 71.45/71.72 [163]~P11(x1631,x1632,x1633,x1634,x1635,x1636,x1637,x1638,x1639,x16310)+P12(x1631,x1632,x1633,x1634,x1635,x1636,x1637,x1638,x1639,x16310)+P9(a65,x16311,f3(x16312,f5(a28,x1639)))+P9(a38,x16311,f3(x16312,f5(a22,x1636))) % 71.45/71.72 [164]~P11(x1641,x1642,x1643,x1644,x1645,x1646,x1647,x1648,x1649,x16410)+P12(x1641,x1642,x1643,x1644,x1645,x1646,x1647,x1648,x1649,x16410)+P9(a65,x16411,f3(x16412,f5(a22,x1646)))+P9(a38,x16411,f3(x16412,f5(a28,x1649))) % 71.45/71.72 [165]~P11(x1651,x1652,x1653,x1654,x1655,x1656,x1657,x1658,x1659,x16510)+P12(x1651,x1652,x1653,x1654,x1655,x1656,x1657,x1658,x1659,x16510)+P9(a65,x16511,f3(x16512,f5(a28,x1659)))+P9(a38,x16511,f3(x16512,f5(a27,x1655))) % 71.45/71.72 [166]~P11(x1661,x1662,x1663,x1664,x1665,x1666,x1667,x1668,x1669,x16610)+P12(x1661,x1662,x1663,x1664,x1665,x1666,x1667,x1668,x1669,x16610)+P9(a65,x16611,f3(x16612,f5(a22,x1666)))+P9(a38,x16611,f3(x16612,f5(a27,x1665))) % 71.45/71.72 [167]~P11(x1671,x1672,x1673,x1674,x1675,x1676,x1677,x1678,x1679,x16710)+P12(x1671,x1672,x1673,x1674,x1675,x1676,x1677,x1678,x1679,x16710)+P9(a65,x16711,f3(x16712,f5(a27,x1675)))+P9(a38,x16711,f3(x16712,f5(a28,x1679))) % 71.45/71.73 [168]~P11(x1681,x1682,x1683,x1684,x1685,x1686,x1687,x1688,x1689,x16810)+P12(x1681,x1682,x1683,x1684,x1685,x1686,x1687,x1688,x1689,x16810)+P9(a65,x16811,f3(x16812,f5(a27,x1685)))+P9(a38,x16811,f3(x16812,f5(a22,x1686))) % 71.45/71.73 [169]~P11(x1691,x1692,x1693,x1694,x1695,x1696,x1697,x1698,x1699,x16910)+P12(x1691,x1692,x1693,x1694,x1695,x1696,x1697,x1698,x1699,x16910)+P9(a65,x16911,f3(x16912,f5(a28,x1699)))+P9(a38,x16911,f3(x16912,f5(a28,x1699))) % 71.45/71.73 [170]~P11(x1701,x1702,x1703,x1704,x1705,x1706,x1707,x1708,x1709,x17010)+P12(x1701,x1702,x1703,x1704,x1705,x1706,x1707,x1708,x1709,x17010)+P9(a65,x17011,f3(x17012,f5(a22,x1706)))+P9(a38,x17011,f3(x17012,f5(a22,x1706))) % 71.45/71.73 [171]~P11(x1711,x1712,x1713,x1714,x1715,x1716,x1717,x1718,x1719,x17110)+P12(x1711,x1712,x1713,x1714,x1715,x1716,x1717,x1718,x1719,x17110)+P9(a65,x17111,f3(x17112,f5(a27,x1715)))+P9(a38,x17111,f3(x17112,f5(a27,x1715))) % 71.45/71.73 [159]~P4(x1592)+P11(x1591,x1592,x1593,x1594,x1595,x1596,x1597,x1598,x1599,x15910)+~P3(x1591,a39)+~P3(x1591,f4(a50,a71,x1595))+~P3(x1591,f4(a51,a17,x1592))+~P3(x1591,f4(a52,a23,x1596)) % 71.45/71.73 [152]P3(x1521,a39)+~P3(x1521,f4(a66,a68,a39))+~P3(x1521,f4(a50,a15,a6))+~P3(x1521,f4(a51,a15,a6))+~P3(x1521,f4(a50,a71,x1522))+~P3(x1521,f4(a51,a17,x1523))+~P3(x1521,f4(a52,a23,x1524))+~P3(x1521,f4(a52,a15,a6)) % 71.45/71.73 [153]P3(x1531,a46)+~P3(x1531,f4(a50,a15,a9))+~P3(x1531,f4(a66,a68,a46))+~P3(x1531,f4(a51,a15,a9))+~P3(x1531,f4(a51,a15,a11))+~P3(x1531,f4(a52,a15,a9))+~P3(x1531,f4(a50,a71,x1532))+~P3(x1531,f4(a51,a17,x1533))+~P3(x1531,f4(a52,a23,x1534)) % 71.45/71.73 [154]P3(x1541,a47)+~P3(x1541,f4(a50,a15,a10))+~P3(x1541,f4(a66,a68,a47))+~P3(x1541,f4(a51,a15,a11))+~P3(x1541,f4(a51,a15,a10))+~P3(x1541,f4(a52,a15,a10))+~P3(x1541,f4(a50,a71,x1542))+~P3(x1541,f4(a51,a17,x1543))+~P3(x1541,f4(a52,a23,x1544)) % 71.45/71.73 [155]~P3(x1551,a47)+P3(x1551,a48)+~P3(x1551,f4(a50,a15,a9))+~P3(x1551,f4(a51,a15,a11))+~P3(x1551,f4(a51,a15,a9))+~P3(x1551,f4(a52,a15,a9))+~P3(x1551,f4(a66,a68,a48))+~P3(x1551,f4(a50,a71,x1552))+~P3(x1551,f4(a51,a17,x1553))+~P3(x1551,f4(a52,a23,x1554))+~P3(x1551,f4(a53,a24,x1555))+~P3(x1551,f4(a53,a26,x1556)) % 71.45/71.73 [172]P8(x1721,x1722,x1723,x1724,x1725,x1726,x1727,x1728,x1729,x17210)+~P12(x17211,x1722,x1723,x1724,x1725,x1726,x1727,x1728,x1729,x17210)+~P3(x1721,a40)+~P3(x1721,a43)+~P3(x1721,a45)+~P3(x1721,f4(a51,a17,x1722))+~P3(x1721,f4(a54,a25,x1727))+~P3(x1721,f4(a55,a17,x1722))+~P3(x1721,f4(a57,a71,x1725))+~P3(x1721,f4(a56,a23,x1726))+~P3(x1721,f4(a58,a41,x1728))+~P3(x1721,f4(a59,a32,x1729)) % 71.45/71.73 [176]~P6(x1763,x1762,x1764)+P13(x1761,x1762,x1763,x1764,x1765,x1766,x1767,x1768,x1769,x17610,x17611,x17612,x17613)+~P11(x17615,x1765,x1766,x1767,x1768,x1769,x17610,x17611,x17612,x17613)+~P3(x1761,a48)+~P3(x1761,f4(a50,a71,x1768))+~P3(x1761,f4(a51,a17,x1765))+~P3(x1761,f4(a52,a23,x1769))+~P3(x1761,f4(a53,a24,x1764))+~P3(x1761,f4(a53,a26,x1762))+~P9(x1763,x1762,f3(x17614,f5(a27,x1768)))+~P9(x1763,x1762,f3(x17614,f5(a28,x17612)))+~P9(x1763,x1762,f3(x17614,f5(a22,x1769))) % 71.45/71.73 [160]~P1(x1602)+P8(x1601,x1602,x1603,x1604,x1605,x1606,x1607,x1608,x1609,x16010)+~P3(x1601,a40)+~P3(x1601,a43)+~P3(x1601,a45)+~P3(x1601,f4(a66,a68,a44))+~P3(x1601,f4(a51,a17,x1602))+~P3(x1601,f4(a54,a25,x1607))+~P3(x1601,f4(a55,a17,x1602))+~P3(x1601,f4(a57,a71,x1605))+~P3(x1601,f4(a56,a23,x1606))+~P3(x1601,f4(a58,a41,x1608))+~P3(x1601,f4(a59,a32,x1609)) % 71.45/71.73 [161]~P1(x1611)+~P11(x1618,x1611,x1619,x16110,x1614,x1615,x1613,x1616,x1617,x16111)+~P3(x1612,a43)+~P3(x1612,a45)+~P3(x1612,a40)+~P3(x1612,f4(a66,a68,a44))+~P3(x1612,f4(a51,a17,x1611))+~P3(x1612,f4(a55,a17,x1611))+~P3(x1612,f4(a54,a25,x1613))+~P3(x1612,f4(a57,a71,x1614))+~P3(x1612,f4(a56,a23,x1615))+~P3(x1612,f4(a58,a41,x1616))+~P3(x1612,f4(a59,a32,x1617)) % 71.45/71.73 [162]~P1(x1621)+~P12(x1628,x1621,x1629,x16210,x1624,x1625,x1623,x1626,x1627,x16211)+~P3(x1622,a43)+~P3(x1622,a45)+~P3(x1622,a40)+~P3(x1622,f4(a66,a68,a44))+~P3(x1622,f4(a51,a17,x1621))+~P3(x1622,f4(a55,a17,x1621))+~P3(x1622,f4(a54,a25,x1623))+~P3(x1622,f4(a57,a71,x1624))+~P3(x1622,f4(a56,a23,x1625))+~P3(x1622,f4(a58,a41,x1626))+~P3(x1622,f4(a59,a32,x1627)) % 71.45/71.73 [156]P3(x1561,a40)+~P3(x1561,f4(a51,a15,a6))+~P3(x1561,f4(a54,a15,a6))+~P3(x1561,f4(a56,a15,a12))+~P3(x1561,f4(a56,a15,a6))+~P3(x1561,f4(a57,a15,a12))+~P3(x1561,f4(a57,a15,a11))+~P3(x1561,f4(a57,a15,a6))+~P3(x1561,f4(a55,a15,a12))+~P3(x1561,f4(a55,a15,a6))+~P3(x1561,f4(a54,a15,a12))+~P3(x1561,f4(a66,a68,a40))+~P3(x1561,f4(a55,a17,x1562))+~P3(x1561,f4(a51,a17,x1562))+~P3(x1561,f4(a54,a25,x1563))+~P3(x1561,f4(a57,a71,x1564))+~P3(x1561,f4(a56,a23,x1565)) % 71.45/71.73 [157]P3(x1571,a45)+~P3(x1571,f4(a51,a15,a6))+~P3(x1571,f4(a56,a15,a12))+~P3(x1571,f4(a55,a15,a12))+~P3(x1571,f4(a54,a15,a12))+~P3(x1571,f4(a54,a15,a11))+~P3(x1571,f4(a56,a15,a11))+~P3(x1571,f4(a56,a15,a10))+~P3(x1571,f4(a57,a15,a10))+~P3(x1571,f4(a55,a15,a11))+~P3(x1571,f4(a55,a15,a10))+~P3(x1571,f4(a54,a15,a10))+~P3(x1571,f4(a66,a68,a45))+~P3(x1571,f4(a55,a17,x1572))+~P3(x1571,f4(a51,a17,x1572))+~P3(x1571,f4(a54,a25,x1573))+~P3(x1571,f4(a57,a71,x1574))+~P3(x1571,f4(a56,a23,x1575)) % 71.45/71.73 [158]P3(x1581,a43)+~P3(x1581,f4(a51,a15,a6))+~P3(x1581,f4(a54,a15,a12))+~P3(x1581,f4(a56,a15,a12))+~P3(x1581,f4(a55,a15,a12))+~P3(x1581,f4(a54,a15,a11))+~P3(x1581,f4(a55,a15,a11))+~P3(x1581,f4(a57,a15,a11))+~P3(x1581,f4(a57,a15,a12))+~P3(x1581,f4(a56,a15,a11))+~P3(x1581,f4(a54,a15,a9))+~P3(x1581,f4(a55,a15,a9))+~P3(x1581,f4(a57,a15,a9))+~P3(x1581,f4(a56,a15,a9))+~P3(x1581,f4(a66,a68,a43))+~P3(x1581,f4(a55,a17,x1582))+~P3(x1581,f4(a51,a17,x1582))+~P3(x1581,f4(a54,a25,x1583))+~P3(x1581,f4(a57,a71,x1584))+~P3(x1581,f4(a56,a23,x1585)) % 71.45/71.73 %EqnAxiom % 71.45/71.73 % 71.45/71.73 %------------------------------------------- % 71.45/71.74 cnf(45524,plain, % 71.45/71.74 (P14(f82(a49,f4(a66,a68,a39)))), % 71.45/71.74 inference(scs_inference,[],[2,19,20,36,24,21,5,131,133,137,139,143,129,149])). % 71.45/71.74 cnf(45536,plain, % 71.45/71.74 (P14(f82(a49,f4(a50,a15,a6)))), % 71.45/71.74 inference(scs_inference,[],[37,2,22,23,5,137,133,131,129,149])). % 71.45/71.74 cnf(45555,plain, % 71.45/71.75 (P14(f82(a49,f4(a51,a15,a67)))), % 71.45/71.75 inference(scs_inference,[],[41,2,5,129,149])). % 71.45/71.75 cnf(45561,plain, % 71.45/71.75 (P14(f82(a49,f4(a51,a17,a67)))), % 71.45/71.75 inference(scs_inference,[],[42,2,5,129,149])). % 71.45/71.75 cnf(45567,plain, % 71.45/71.75 (P14(f82(a49,f4(a52,a15,a67)))), % 71.45/71.75 inference(scs_inference,[],[43,2,5,129,149])). % 71.45/71.75 cnf(45573,plain, % 71.45/71.75 (P14(f82(a49,f4(a52,a23,a29)))), % 71.45/71.75 inference(scs_inference,[],[44,2,5,129,149])). % 71.45/71.75 cnf(45579,plain, % 71.45/71.75 (P14(f82(a49,f4(a50,a71,a34)))), % 71.45/71.75 inference(scs_inference,[],[40,2,5,129,149])). % 71.45/71.75 cnf(45932,plain, % 71.45/71.75 (P14(f82(a20,f4(a50,a15,a10)))), % 71.45/71.75 inference(scs_inference,[],[48,8,2,3,129,151])). % 71.45/71.75 cnf(45952,plain, % 71.45/71.75 (P14(f82(a36,f4(a52,a23,a29)))), % 71.45/71.75 inference(scs_inference,[],[58,10,2,4,129,151])). % 71.45/71.75 cnf(45991,plain, % 71.45/71.75 (P14(f82(a36,f4(a50,a71,a34)))), % 71.45/71.75 inference(scs_inference,[],[50,10,2,4,129,151])). % 71.45/71.75 cnf(52412,plain, % 71.45/71.75 (P3(a49,f4(a51,a17,x524121))), % 71.45/71.75 inference(scs_inference,[],[45932,45561,1,129,148,147])). % 71.45/71.75 cnf(52426,plain, % 71.45/71.75 (~P3(a49,a39)+~P3(a49,f4(a50,a71,a34))+~P3(a49,f4(a52,a23,x524261))), % 71.45/71.75 inference(scs_inference,[],[128,52412,1,2,129,159])). % 71.45/71.75 cnf(52429,plain, % 71.45/71.75 (~P3(a49,f4(a52,a23,x524291))+~P3(a49,a39)), % 71.45/71.75 inference(scs_inference,[],[45579,52426,148])). % 71.45/71.75 cnf(52434,plain, % 71.45/71.75 (P3(a49,f4(a51,a15,x524341))), % 71.45/71.75 inference(scs_inference,[],[45952,45555,1,148,129,147])). % 71.45/71.75 cnf(52457,plain, % 71.45/71.75 (P3(a49,f4(a52,a15,x524571))), % 71.45/71.75 inference(scs_inference,[],[45991,45567,1,129,148,147])). % 71.45/71.75 cnf(52510,plain, % 71.45/71.75 (~P3(a49,a39)), % 71.45/71.75 inference(scs_inference,[],[45573,52429,148])). % 71.45/71.75 cnf(53168,plain, % 71.45/71.75 (P3(a49,f4(a66,a68,a39))), % 71.45/71.75 inference(scs_inference,[],[45524,1,129,148])). % 71.45/71.75 cnf(53244,plain, % 71.45/71.75 (~P3(a49,f4(a50,a15,a6))+~P3(a49,f4(a50,a71,x532441))+~P3(a49,f4(a52,a23,x532442))), % 71.45/71.75 inference(scs_inference,[],[52510,53168,52434,52457,52412,1,129,152])). % 71.45/71.75 cnf(53249,plain, % 71.45/71.75 (~P3(a49,f4(a50,a71,x532491))+~P3(a49,f4(a52,a23,x532492))), % 71.45/71.75 inference(scs_inference,[],[45536,53244,148])). % 71.45/71.75 cnf(53324,plain, % 71.45/71.75 (~P3(a49,f4(a52,a23,x533241))), % 71.45/71.75 inference(scs_inference,[],[45579,53249,148])). % 71.45/71.75 cnf(53341,plain, % 71.45/71.75 ($false), % 71.45/71.75 inference(scs_inference,[],[53324,45573,1,129,148]), % 71.45/71.75 ['proof']). % 71.45/71.76 % SZS output end Proof % 71.45/71.76 % Total time :71.072956s %------------------------------------------------------------------------------