%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : ITP021_2 : TPTP v8.1.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 00:40:02 EDT 2022 % Result : Theorem 35.97s 20.06s % Output : Refutation 35.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ITP021_2 : TPTP v8.1.0. Bugfixed v7.5.0. % 0.03/0.12 % Command : spasst-tptp-script %s %d % 0.14/0.34 % Computer : n023.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Fri Jun 3 03:19:40 EDT 2022 % 0.14/0.34 % CPUTime : % 0.20/0.47 % Using EUF theory % 35.97/20.06 % 35.97/20.06 % 35.97/20.06 % SZS status Theorem for /tmp/SPASST_697_n023.cluster.edu % 35.97/20.06 % 35.97/20.06 SPASS V 2.2.22 in combination with yices. % 35.97/20.06 SPASS beiseite: Proof found by SPASS. % 35.97/20.06 Problem: /tmp/SPASST_697_n023.cluster.edu % 35.97/20.06 SPASS derived 60353 clauses, backtracked 11789 clauses and kept 19431 clauses. % 35.97/20.06 SPASS backtracked 49 times (0 times due to theory inconsistency). % 35.97/20.06 SPASS allocated 79578 KBytes. % 35.97/20.06 SPASS spent 0:00:18.56 on the problem. % 35.97/20.06 0:00:00.00 for the input. % 35.97/20.06 0:00:00.03 for the FLOTTER CNF translation. % 35.97/20.06 0:00:00.49 for inferences. % 35.97/20.06 0:00:01.03 for the backtracking. % 35.97/20.06 0:00:14.68 for the reduction. % 35.97/20.06 0:00:00.89 for interacting with the SMT procedure. % 35.97/20.06 % 35.97/20.06 % 35.97/20.06 % SZS output start CNFRefutation for /tmp/SPASST_697_n023.cluster.edu % 35.97/20.06 % 35.97/20.06 % Here is a proof with depth 14, length 627 : % 35.97/20.06 19[0:Inp] || -> p(c_2Ebool_2ET)*. % 35.97/20.06 20[0:Inp] || -> tp__o(fo__c_2Ebool_2EF)*. % 35.97/20.06 22[0:Inp] || -> del(ty_2Eextreal_2Eextreal)*. % 35.97/20.06 23[0:Inp] || -> tp__o(fo__c_2Ebool_2ET)*. % 35.97/20.06 26[0:Inp] || -> del(bool)*. % 35.97/20.06 28[0:Inp] || -> tp__ty_2Eextreal_2Eextreal(skc8)*. % 35.97/20.06 29[0:Inp] || -> tp__ty_2Eextreal_2Eextreal(skc7)*. % 35.97/20.06 30[0:Inp] || -> tp__ty_2Eextreal_2Eextreal(skc6)*. % 35.97/20.06 31[0:Inp] || p(c_2Ebool_2EF)* -> . % 35.97/20.06 32[0:Inp] || -> mem(c_2Ebool_2EF,bool)*. % 35.97/20.06 33[0:Inp] || -> mem(c_2Ebool_2ET,bool)*. % 35.97/20.06 34[0:Inp] || -> tp__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(U))*. % 35.97/20.06 35[0:Inp] || -> tp__o(surj__o(U))*. % 35.97/20.06 36[0:Inp] || -> equal(inj__o(fo__c_2Ebool_2EF),c_2Ebool_2EF)**. % 35.97/20.06 37[0:Inp] || -> equal(inj__o(fo__c_2Ebool_2ET),c_2Ebool_2ET)**. % 35.97/20.06 42[0:Inp] || tp__o(U) -> tp__o(fo__c_2Ebool_2E_7E(U))*. % 35.97/20.06 50[0:Inp] || -> mem(c_2Ebool_2E_2F_5C,arr(bool,arr(bool,bool)))*. % 35.97/20.06 51[0:Inp] || -> mem(c_2Ebool_2E_5C_2F,arr(bool,arr(bool,bool)))*. % 35.97/20.06 52[0:Inp] || -> mem(c_2Emin_2E_3D_3D_3E,arr(bool,arr(bool,bool)))*. % 35.97/20.06 54[0:Inp] || -> mem(c_2Eextreal_2Eextreal__le,arr(ty_2Eextreal_2Eextreal,arr(ty_2Eextreal_2Eextreal,bool)))*. % 35.97/20.06 55[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) -> mem(inj__ty_2Eextreal_2Eextreal(U),ty_2Eextreal_2Eextreal)*. % 35.97/20.06 56[0:Inp] || tp__o(U) -> mem(inj__o(U),bool)*. % 35.97/20.06 62[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(U)),U)**. % 35.97/20.06 63[0:Inp] || tp__o(U) -> equal(surj__o(inj__o(U)),U)**. % 35.97/20.06 65[0:Inp] || mem(U,ty_2Eextreal_2Eextreal) -> equal(inj__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(U)),U)**. % 35.97/20.06 66[0:Inp] || mem(U,bool) -> equal(inj__o(surj__o(U)),U)**. % 35.97/20.06 73[0:Inp] || mem(U,bool) -> p(U) p(ap(c_2Ebool_2E_7E,U))*. % 35.97/20.06 74[0:Inp] || tp__o(U) tp__o(V) -> tp__o(fo__c_2Ebool_2E_2F_5C(U,V))*. % 35.97/20.06 75[0:Inp] || tp__o(U) tp__o(V) -> tp__o(fo__c_2Ebool_2E_5C_2F(U,V))*. % 35.97/20.06 76[0:Inp] || tp__o(U) tp__o(V) -> tp__o(fo__c_2Emin_2E_3D_3D_3E(U,V))*. % 35.97/20.06 77[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) -> tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(U,V))*. % 35.97/20.06 78[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) -> tp__o(fo__c_2Eextreal_2Eextreal__le(U,V))*. % 35.97/20.06 79[0:Inp] || del(U) del(V) -> del(arr(U,V))*. % 35.97/20.06 88[0:Inp] || del(U) -> mem(c_2Emin_2E_3D(U),arr(U,arr(U,bool)))*. % 35.97/20.06 89[0:Inp] || tp__o(U) -> equal(ap(c_2Ebool_2E_7E,inj__o(U)),inj__o(fo__c_2Ebool_2E_7E(U)))**. % 35.97/20.06 102[0:Inp] || p(U) p(ap(c_2Ebool_2E_7E,U))* mem(U,bool) -> . % 35.97/20.06 110[0:Inp] || mem(U,bool)*+ mem(V,bool)* -> p(U) p(V) equal(U,V)*. % 35.97/20.06 116[0:Inp] || mem(U,bool) mem(V,bool) -> p(U) p(ap(ap(c_2Emin_2E_3D_3D_3E,U),V))*. % 35.97/20.06 120[0:Inp] || p(ap(ap(c_2Ebool_2E_2F_5C,U),V))* mem(U,bool) mem(V,bool) -> p(V). % 35.97/20.06 121[0:Inp] || p(ap(ap(c_2Ebool_2E_2F_5C,U),V))* mem(U,bool) mem(V,bool) -> p(U). % 35.97/20.06 122[0:Inp] || p(U) mem(V,bool) mem(U,bool) -> p(ap(ap(c_2Ebool_2E_5C_2F,V),U))*. % 35.97/20.06 123[0:Inp] || p(U) mem(U,bool) mem(V,bool) -> p(ap(ap(c_2Ebool_2E_5C_2F,U),V))*. % 35.97/20.06 124[0:Inp] || p(U) mem(V,bool) mem(U,bool) -> p(ap(ap(c_2Emin_2E_3D_3D_3E,V),U))*. % 35.97/20.06 125[0:Inp] || p(U) p(V) mem(U,bool)*+ mem(V,bool)* -> equal(U,V)*. % 35.97/20.06 132[0:Inp] || tp__o(U) tp__o(V) -> equal(ap(ap(c_2Ebool_2E_2F_5C,inj__o(U)),inj__o(V)),inj__o(fo__c_2Ebool_2E_2F_5C(U,V)))**. % 35.97/20.06 133[0:Inp] || tp__o(U) tp__o(V) -> equal(ap(ap(c_2Ebool_2E_5C_2F,inj__o(U)),inj__o(V)),inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))**. % 35.97/20.06 134[0:Inp] || tp__o(U) tp__o(V) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),inj__o(V)),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))**. % 35.97/20.06 135[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) -> equal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(U)),inj__ty_2Eextreal_2Eextreal(V)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(U,V)))**. % 35.97/20.06 136[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(U)),inj__ty_2Eextreal_2Eextreal(V)),inj__o(fo__c_2Eextreal_2Eextreal__le(U,V)))**. % 35.97/20.06 138[0:Inp] || p(ap(ap(c_2Ebool_2E_5C_2F,U),V))* mem(U,bool) mem(V,bool) -> p(U) p(V). % 35.97/20.06 139[0:Inp] || p(U) p(ap(ap(c_2Emin_2E_3D_3D_3E,U),V))* mem(U,bool) mem(V,bool) -> p(V). % 35.97/20.06 142[0:Inp] || -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 143[0:Inp] || -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 144[0:Inp] || del(U) del(V) mem(W,U)* mem(X,arr(U,V))*+ -> mem(ap(X,W),V)*. % 35.97/20.06 151[0:Inp] || del(U) mem(V,U) mem(W,U) -> equal(ap(ap(ap(c_2Ebool_2ECOND(U),inj__o(fo__c_2Ebool_2ET)),W),V),W)**. % 35.97/20.06 152[0:Inp] || del(U) mem(V,U) mem(W,U) -> equal(ap(ap(ap(c_2Ebool_2ECOND(U),inj__o(fo__c_2Ebool_2EF)),W),V),V)**. % 35.97/20.06 153[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(U)),inj__ty_2Eextreal_2Eextreal(V)))* p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V)),inj__ty_2Eextreal_2Eextreal(U)))*. % 35.97/20.06 160[0:Inp] || del(U) del(V) mem(W,arr(U,V))*+ mem(X,arr(U,V))* -> equal(W,X)* mem(skf2(U,Y,Z),U)*. % 35.97/20.06 161[0:Inp] || p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))* -> . % 35.97/20.06 162[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V)),inj__ty_2Eextreal_2Eextreal(U))),inj__ty_2Eextreal_2Eextreal(U)),inj__ty_2Eextreal_2Eextreal(V))),surj__ty_2Eextreal_2Eextreal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(V)),inj__ty_2Eextreal_2Eextreal(U))))**. % 35.97/20.06 165[0:Inp] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(V)),inj__ty_2Eextreal_2Eextreal(U)))* p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(W)),inj__ty_2Eextreal_2Eextreal(V)))* tp__ty_2Eextreal_2Eextreal(W) -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(W)),inj__ty_2Eextreal_2Eextreal(U)))*. % 35.97/20.06 167[0:Rew:37.0,151.3] || del(U) mem(V,U) mem(W,U) -> equal(ap(ap(ap(c_2Ebool_2ECOND(U),c_2Ebool_2ET),V),W),V)**. % 35.97/20.06 168[0:Rew:36.0,152.3] || del(U) mem(V,U) mem(W,U) -> equal(ap(ap(ap(c_2Ebool_2ECOND(U),c_2Ebool_2EF),V),W),W)**. % 35.97/20.06 169[0:Rew:136.2,153.3,136.2,153.2] || tp__ty_2Eextreal_2Eextreal(U)+ tp__ty_2Eextreal_2Eextreal(V) -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,V)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(V,U)))*. % 35.97/20.06 171[0:Rew:136.2,162.2,135.2,162.2] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Eextreal_2Eextreal__le(U,V))),inj__ty_2Eextreal_2Eextreal(V)),inj__ty_2Eextreal_2Eextreal(U))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(U,V))))**. % 35.97/20.06 172[0:Rew:136.2,165.5,136.2,165.3,136.2,165.2] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) tp__ty_2Eextreal_2Eextreal(W) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,V)))*+ p(inj__o(fo__c_2Eextreal_2Eextreal__le(V,W)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,W)))*. % 35.97/20.06 173[0:Res:30.0,172.0] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,V)))*+ p(inj__o(fo__c_2Eextreal_2Eextreal__le(V,skc6)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6)))*. % 35.97/20.06 174[0:Res:30.0,171.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6))),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(U))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(U,skc6))))**. % 35.97/20.06 175[0:Res:30.0,169.0] || tp__ty_2Eextreal_2Eextreal(U)+ -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U)))*. % 35.97/20.06 179[0:Res:30.0,78.0] || tp__ty_2Eextreal_2Eextreal(U) -> tp__o(fo__c_2Eextreal_2Eextreal__le(U,skc6))*. % 35.97/20.06 180[0:Res:30.0,62.0] || -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(skc6)),skc6)**. % 35.97/20.06 181[0:Res:30.0,55.0] || -> mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal)*. % 35.97/20.06 188[0:Res:30.0,78.1] || tp__ty_2Eextreal_2Eextreal(U) -> tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,U))*. % 35.97/20.06 197[0:Res:29.0,62.0] || -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(skc7)),skc7)**. % 35.97/20.06 198[0:Res:29.0,55.0] || -> mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal)*. % 35.97/20.06 202[0:Res:29.0,135.1] || tp__ty_2Eextreal_2Eextreal(U) -> equal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(U)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,U)))**. % 35.97/20.06 203[0:Res:29.0,136.1] || tp__ty_2Eextreal_2Eextreal(U) -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(U)),inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,U)))**. % 35.97/20.06 204[0:Res:29.0,77.1] || tp__ty_2Eextreal_2Eextreal(U) -> tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,U))*. % 35.97/20.06 205[0:Res:29.0,78.1] || tp__ty_2Eextreal_2Eextreal(U) -> tp__o(fo__c_2Eextreal_2Eextreal__le(skc7,U))*. % 35.97/20.06 207[0:Res:28.0,172.0] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,V)))*+ p(inj__o(fo__c_2Eextreal_2Eextreal__le(V,skc8)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))*. % 35.97/20.06 209[0:Res:28.0,169.0] || tp__ty_2Eextreal_2Eextreal(U)+ -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,U)))*. % 35.97/20.06 211[0:Res:28.0,136.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(U)),inj__ty_2Eextreal_2Eextreal(skc8)),inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))**. % 35.97/20.06 213[0:Res:28.0,78.0] || tp__ty_2Eextreal_2Eextreal(U) -> tp__o(fo__c_2Eextreal_2Eextreal__le(U,skc8))*. % 35.97/20.06 214[0:Res:28.0,62.0] || -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(skc8)),skc8)**. % 35.97/20.06 215[0:Res:28.0,55.0] || -> mem(inj__ty_2Eextreal_2Eextreal(skc8),ty_2Eextreal_2Eextreal)*. % 35.97/20.06 216[0:Res:28.0,172.1] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(V) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,V)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,V)))*. % 35.97/20.06 222[0:Res:28.0,78.1] || tp__ty_2Eextreal_2Eextreal(U) -> tp__o(fo__c_2Eextreal_2Eextreal__le(skc8,U))*. % 35.97/20.06 236[0:Res:30.0,216.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,skc6)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6))). % 35.97/20.06 241[0:Res:30.0,211.0] || -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc8)),inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)))**. % 35.97/20.06 244[0:Res:30.0,202.0] || -> equal(ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)))**. % 35.97/20.06 251(e)[0:Res:30.0,209.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,skc6)))*. % 35.97/20.06 253[0:Res:30.0,175.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6)))*. % 35.97/20.06 256[0:Res:30.0,213.0] || -> tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))*. % 35.97/20.06 258[0:Res:30.0,205.0] || -> tp__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc6))*. % 35.97/20.06 259[0:Res:30.0,204.0] || -> tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))*. % 35.97/20.06 262[0:Res:30.0,188.0] || -> tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6))*. % 35.97/20.06 272[0:Res:30.0,207.3] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)))*. % 35.97/20.06 273(e)[0:Res:30.0,216.3] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,U)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))) -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U))). % 35.97/20.06 276[0:Res:29.0,174.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 292[0:Res:29.0,211.0] || -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8)),inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)))**. % 35.97/20.06 302[0:Res:29.0,209.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8))) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,skc7)))*. % 35.97/20.06 307[0:Res:29.0,213.0] || -> tp__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8))*. % 35.97/20.06 317[0:Res:29.0,173.3] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,U)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc6)))*. % 35.97/20.06 326[0:Obv:253.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6)))*. % 35.97/20.06 328[0:Rew:241.0,161.0] || p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))* -> . % 35.97/20.06 329[0:Rew:241.0,143.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,ap(ap(c_2Eextreal_2Eextreal__max,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 330[0:Rew:244.0,142.1] || -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 331[0:Rew:244.0,329.1] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 332(e)[0:Rew:292.0,330.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 333(e)[0:Rew:244.0,328.2,292.0,328.1] || p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8))) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))* -> . % 35.97/20.06 346[0:SpR:37.0,63.1] || tp__o(fo__c_2Ebool_2ET) -> equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 35.97/20.06 347[0:SpR:36.0,63.1] || tp__o(fo__c_2Ebool_2EF) -> equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 348[0:MRR:346.0,23.0] || -> equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 35.97/20.06 349[0:MRR:347.0,20.0] || -> equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 372[1:Spt:251.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)))*. % 35.97/20.06 373[1:MRR:273.2,372.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,U)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U))). % 35.97/20.06 375(e)[1:MRR:333.1,372.0] || p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8))) p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))* -> . % 35.97/20.06 379[2:Spt:302.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)))*. % 35.97/20.06 382[2:MRR:375.0,379.0] || p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))* -> . % 35.97/20.06 385[0:SpR:89.1,73.2] || tp__o(U) mem(inj__o(U),bool) -> p(inj__o(U)) p(inj__o(fo__c_2Ebool_2E_7E(U)))*. % 35.97/20.06 388[0:SpR:36.0,89.1] || tp__o(fo__c_2Ebool_2EF) -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 35.97/20.06 389[0:SpR:66.1,89.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_7E(surj__o(U))),ap(c_2Ebool_2E_7E,U))**. % 35.97/20.06 391[0:MRR:388.0,20.0] || -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 35.97/20.06 392[0:MRR:385.1,56.1] || tp__o(U) -> p(inj__o(U)) p(inj__o(fo__c_2Ebool_2E_7E(U)))*. % 35.97/20.06 393[0:MRR:389.1,35.0] || mem(U,bool) -> equal(inj__o(fo__c_2Ebool_2E_7E(surj__o(U))),ap(c_2Ebool_2E_7E,U))**. % 35.97/20.06 398[0:SpR:391.0,56.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)) -> mem(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),bool)*. % 35.97/20.06 399[0:SpR:391.0,63.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)) -> equal(surj__o(ap(c_2Ebool_2E_7E,c_2Ebool_2EF)),fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF))**. % 35.97/20.06 403[0:SpR:391.0,392.2] || tp__o(fo__c_2Ebool_2EF) -> p(inj__o(fo__c_2Ebool_2EF)) p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF))*. % 35.97/20.06 405[0:Rew:36.0,403.1] || tp__o(fo__c_2Ebool_2EF) -> p(c_2Ebool_2EF) p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF))*. % 35.97/20.06 406[0:MRR:405.0,405.1,20.0,31.0] || -> p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF))*. % 35.97/20.06 424[0:SpL:89.1,102.1] || tp__o(U) p(inj__o(U)) p(inj__o(fo__c_2Ebool_2E_7E(U)))* mem(inj__o(U),bool) -> . % 35.97/20.06 427[0:MRR:424.3,56.1] || tp__o(U) p(inj__o(U)) p(inj__o(fo__c_2Ebool_2E_7E(U)))* -> . % 35.97/20.06 480[0:Res:29.0,175.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc6)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc7))). % 35.97/20.06 543(e)[0:Res:259.0,209.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8)))* p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)))). % 35.97/20.06 597[0:Res:32.0,110.0] || mem(U,bool)* -> p(c_2Ebool_2EF) p(U) equal(c_2Ebool_2EF,U). % 35.97/20.06 601[0:MRR:597.1,31.0] || mem(U,bool)* -> p(U) equal(c_2Ebool_2EF,U). % 35.97/20.06 605[0:Res:56.1,601.0] || tp__o(U) -> p(inj__o(U))* equal(inj__o(U),c_2Ebool_2EF). % 35.97/20.06 641[0:Res:605.1,427.2] || tp__o(fo__c_2Ebool_2E_7E(U)) tp__o(U) p(inj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF)**. % 35.97/20.06 647[0:MRR:641.0,42.1] || tp__o(U) p(inj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2EF)**. % 35.97/20.06 674[0:SpR:647.2,63.1] || tp__o(U) p(inj__o(U))* tp__o(fo__c_2Ebool_2E_7E(U)) -> equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2E_7E(U)). % 35.97/20.06 679[0:SpR:647.2,393.1] || tp__o(surj__o(U)) p(inj__o(surj__o(U)))* mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF). % 35.97/20.06 683[0:Rew:349.0,674.3] || tp__o(U) p(inj__o(U))* tp__o(fo__c_2Ebool_2E_7E(U)) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF). % 35.97/20.06 684[0:MRR:683.2,42.1] || tp__o(U) p(inj__o(U))* -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF). % 35.97/20.06 688[0:Rew:66.1,679.1] || tp__o(surj__o(U)) p(U) mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF)**. % 35.97/20.06 689[0:MRR:688.0,35.0] || p(U) mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF)**. % 35.97/20.06 697[0:Res:605.1,684.1] || tp__o(U) tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF). % 35.97/20.06 726[0:Obv:697.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF). % 35.97/20.06 791[0:SpR:726.1,63.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)** equal(surj__o(c_2Ebool_2EF),U)*. % 35.97/20.06 792[0:SpR:726.1,89.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) equal(inj__o(fo__c_2Ebool_2E_7E(U)),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 35.97/20.06 821[0:Obv:791.0] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)** equal(surj__o(c_2Ebool_2EF),U)*. % 35.97/20.06 822[0:Rew:349.0,821.2] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF)** equal(fo__c_2Ebool_2EF,U). % 35.97/20.06 825[0:Obv:792.0] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) equal(inj__o(fo__c_2Ebool_2E_7E(U)),ap(c_2Ebool_2E_7E,c_2Ebool_2EF))**. % 35.97/20.06 831[0:SpR:822.1,392.2] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2EF,U) p(inj__o(U))* p(inj__o(fo__c_2Ebool_2EF))*. % 35.97/20.06 848[0:Obv:831.0] || tp__o(U) -> equal(fo__c_2Ebool_2EF,U) p(inj__o(U))* p(inj__o(fo__c_2Ebool_2EF))*. % 35.97/20.06 849[0:Rew:36.0,848.3] || tp__o(U) -> equal(fo__c_2Ebool_2EF,U) p(inj__o(U))* p(c_2Ebool_2EF). % 35.97/20.06 850[0:MRR:849.3,31.0] || tp__o(U) -> equal(fo__c_2Ebool_2EF,U) p(inj__o(U))*. % 35.97/20.06 859[0:SpR:66.1,850.2] || mem(U,bool)* tp__o(surj__o(U)) -> equal(surj__o(U),fo__c_2Ebool_2EF) p(U). % 35.97/20.06 862[0:MRR:859.1,35.0] || mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2EF) p(U). % 35.97/20.06 1069[3:Spt:543.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8)))*. % 35.97/20.06 1114[0:Res:33.0,125.2] || p(c_2Ebool_2ET) p(U) mem(U,bool)* -> equal(c_2Ebool_2ET,U). % 35.97/20.06 1118[0:MRR:1114.0,19.0] || p(U) mem(U,bool)* -> equal(c_2Ebool_2ET,U). % 35.97/20.06 1122[0:Res:56.1,1118.1] || tp__o(U) p(inj__o(U))* -> equal(inj__o(U),c_2Ebool_2ET). % 35.97/20.06 1123[0:Res:398.1,1118.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)) p(ap(c_2Ebool_2E_7E,c_2Ebool_2EF))* -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2ET). % 35.97/20.06 1125[0:MRR:1123.1,406.0] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)) -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2ET)**. % 35.97/20.06 1127[0:Rew:1125.1,399.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF))* -> equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)). % 35.97/20.06 1130[0:Rew:348.0,1127.1] || tp__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF))* -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF),fo__c_2Ebool_2ET). % 35.97/20.06 1133[0:Res:42.1,1130.0] || tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF),fo__c_2Ebool_2ET)**. % 35.97/20.06 1134[0:MRR:1133.0,20.0] || -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF),fo__c_2Ebool_2ET)**. % 35.97/20.06 1135[0:Rew:1134.0,391.0] || -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),inj__o(fo__c_2Ebool_2ET))**. % 35.97/20.06 1138[0:Rew:37.0,1135.0] || -> equal(ap(c_2Ebool_2E_7E,c_2Ebool_2EF),c_2Ebool_2ET)**. % 35.97/20.06 1140[0:Rew:1138.0,825.2] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2ET)**. % 35.97/20.06 1164[0:Res:850.2,1122.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2EF,U) equal(inj__o(U),c_2Ebool_2ET)**. % 35.97/20.06 1165[0:Res:605.1,1122.1] || tp__o(U) tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(inj__o(U),c_2Ebool_2ET)**. % 35.97/20.06 1166[0:Res:326.0,1122.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6)) -> equal(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6)),c_2Ebool_2ET)**. % 35.97/20.06 1167[1:Res:372.0,1122.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)) -> equal(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)),c_2Ebool_2ET)**. % 35.97/20.06 1170[2:Res:379.0,1122.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)) -> equal(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)),c_2Ebool_2ET)**. % 35.97/20.06 1212[0:Res:392.2,1122.1] || tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> p(inj__o(U)) equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2ET)**. % 35.97/20.06 1213[0:MRR:1166.0,262.0] || -> equal(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6)),c_2Ebool_2ET)**. % 35.97/20.06 1217[1:MRR:1167.0,256.0] || -> equal(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)),c_2Ebool_2ET)**. % 35.97/20.06 1219[1:Rew:1217.0,241.0] || -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc8)),c_2Ebool_2ET)**. % 35.97/20.06 1229[2:MRR:1170.0,307.0] || -> equal(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)),c_2Ebool_2ET)**. % 35.97/20.06 1231[2:Rew:1229.0,292.0] || -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8)),c_2Ebool_2ET)**. % 35.97/20.06 1233[0:Obv:1164.0] || tp__o(U) -> equal(fo__c_2Ebool_2EF,U) equal(inj__o(U),c_2Ebool_2ET)**. % 35.97/20.06 1235[0:Obv:1165.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(inj__o(U),c_2Ebool_2ET)**. % 35.97/20.06 1238[0:Rew:1140.1,1212.1] || tp__o(U) tp__o(fo__c_2Ebool_2EF) -> p(inj__o(U)) equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2ET)**. % 35.97/20.06 1239[0:MRR:1238.1,20.0] || tp__o(U) -> p(inj__o(U)) equal(inj__o(fo__c_2Ebool_2E_7E(U)),c_2Ebool_2ET)**. % 35.97/20.06 1245[0:SpR:1213.0,63.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6))* -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,skc6),surj__o(c_2Ebool_2ET)). % 35.97/20.06 1249[0:Rew:348.0,1245.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc6))* -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,skc6),fo__c_2Ebool_2ET). % 35.97/20.06 1250[0:MRR:1249.0,262.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,skc6),fo__c_2Ebool_2ET)**. % 35.97/20.06 1264[1:SpR:1217.0,63.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))* -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,skc8),surj__o(c_2Ebool_2ET)). % 35.97/20.06 1268[1:Rew:348.0,1264.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8))* -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,skc8),fo__c_2Ebool_2ET). % 35.97/20.06 1269[1:MRR:1268.0,256.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,skc8),fo__c_2Ebool_2ET)**. % 35.97/20.06 1368(e)[2:SpL:136.2,382.0] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) tp__ty_2Eextreal_2Eextreal(skc8) p(inj__o(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8)))* -> . % 35.97/20.06 1376(e)[3:MRR:1368.0,1368.1,1368.2,259.0,28.0,1069.0] || -> . % 35.97/20.06 1379[3:Spt:1376.0,543.0,1069.0] || p(inj__o(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8)))* -> . % 35.97/20.06 1380[3:Spt:1376.0,543.1] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))*. % 35.97/20.06 1391[0:SpR:134.2,116.3] || tp__o(U) tp__o(V) mem(inj__o(U),bool) mem(inj__o(V),bool) -> p(inj__o(U)) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))*. % 35.97/20.06 1394[0:SpR:37.0,134.2] || tp__o(U) tp__o(fo__c_2Ebool_2ET) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET)))**. % 35.97/20.06 1395[0:SpR:36.0,134.2] || tp__o(U) tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))**. % 35.97/20.06 1400[0:SpR:37.0,134.2] || tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)))**. % 35.97/20.06 1403[0:SpR:66.1,134.2] || mem(U,bool) tp__o(surj__o(U)) tp__o(V) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),inj__o(V)),inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),V)))**. % 35.97/20.06 1406[0:MRR:1394.1,23.0] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET)))**. % 35.97/20.06 1407[0:MRR:1395.1,20.0] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))**. % 35.97/20.06 1408[0:MRR:1400.0,23.0] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,U)))**. % 35.97/20.06 1410[0:MRR:1403.1,35.0] || mem(U,bool) tp__o(V) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),inj__o(V)),inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),V)))**. % 35.97/20.06 1416[0:MRR:1391.2,1391.3,56.1,56.1] || tp__o(U) tp__o(V) -> p(inj__o(U)) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))*. % 35.97/20.06 1425[4:Spt:480.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc6)))*. % 35.97/20.06 1428[4:SpR:726.1,1425.0] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc6)) -> equal(fo__c_2Ebool_2E_7E(fo__c_2Eextreal_2Eextreal__le(skc7,skc6)),fo__c_2Ebool_2EF)** p(c_2Ebool_2EF). % 35.97/20.06 1429[4:MRR:1428.0,1428.2,258.0,31.0] || -> equal(fo__c_2Ebool_2E_7E(fo__c_2Eextreal_2Eextreal__le(skc7,skc6)),fo__c_2Ebool_2EF)**. % 35.97/20.06 1438[0:SpR:1233.2,63.1] || tp__o(U)* tp__o(U)* -> equal(fo__c_2Ebool_2EF,U) equal(surj__o(c_2Ebool_2ET),U)*. % 35.97/20.06 1460[0:Obv:1438.0] || tp__o(U)* -> equal(fo__c_2Ebool_2EF,U) equal(surj__o(c_2Ebool_2ET),U)*. % 35.97/20.06 1461[0:Rew:348.0,1460.2] || tp__o(U)* -> equal(fo__c_2Ebool_2EF,U) equal(fo__c_2Ebool_2ET,U). % 35.97/20.06 1473[0:SpR:133.2,123.3] || tp__o(U) tp__o(V) p(inj__o(U)) mem(inj__o(U),bool) mem(inj__o(V),bool) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))*. % 35.97/20.06 1476[0:SpR:37.0,133.2] || tp__o(U) tp__o(fo__c_2Ebool_2ET) -> equal(ap(ap(c_2Ebool_2E_5C_2F,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(U,fo__c_2Ebool_2ET)))**. % 35.97/20.06 1483[0:SpR:37.0,133.2] || tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U)))**. % 35.97/20.06 1484[0:SpR:36.0,133.2] || tp__o(fo__c_2Ebool_2EF) tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),inj__o(U)),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))**. % 35.97/20.06 1487[0:SpR:66.1,133.2] || mem(U,bool) tp__o(surj__o(U)) tp__o(V) -> equal(ap(ap(c_2Ebool_2E_5C_2F,U),inj__o(V)),inj__o(fo__c_2Ebool_2E_5C_2F(surj__o(U),V)))**. % 35.97/20.06 1490[0:MRR:1476.1,23.0] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(U,fo__c_2Ebool_2ET)))**. % 35.97/20.06 1492[0:MRR:1483.0,23.0] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U)))**. % 35.97/20.06 1493[0:MRR:1484.0,20.0] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),inj__o(U)),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))**. % 35.97/20.06 1494[0:MRR:1487.1,35.0] || mem(U,bool) tp__o(V) -> equal(ap(ap(c_2Ebool_2E_5C_2F,U),inj__o(V)),inj__o(fo__c_2Ebool_2E_5C_2F(surj__o(U),V)))**. % 35.97/20.06 1505[0:MRR:1473.3,1473.4,56.1,56.1] || tp__o(U) tp__o(V) p(inj__o(U)) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))*. % 35.97/20.06 1513[0:Res:35.0,1461.0] || -> equal(surj__o(U),fo__c_2Ebool_2EF) equal(surj__o(U),fo__c_2Ebool_2ET)**. % 35.97/20.06 1515(e)[0:Res:258.0,1461.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF) equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2ET)**. % 35.97/20.06 1516[0:Res:179.1,1461.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF) equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2ET)**. % 35.97/20.06 1517[0:Res:188.1,1461.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,U),fo__c_2Ebool_2EF) equal(fo__c_2Eextreal_2Eextreal__le(skc6,U),fo__c_2Ebool_2ET)**. % 35.97/20.06 1520[0:Res:222.1,1461.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2EF) equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2ET)**. % 35.97/20.06 1521[0:Res:205.1,1461.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,U),fo__c_2Ebool_2EF) equal(fo__c_2Eextreal_2Eextreal__le(skc7,U),fo__c_2Ebool_2ET)**. % 35.97/20.06 1523[0:Res:213.1,1461.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2EF) equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2ET)**. % 35.97/20.06 1525[0:Res:42.1,1461.0] || tp__o(U) -> equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2EF) equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET)**. % 35.97/20.06 1526(e)[0:Res:76.2,1461.0] || tp__o(U) tp__o(V) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2EF) equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2ET)**. % 35.97/20.06 1527(e)[0:Res:75.2,1461.0] || tp__o(U) tp__o(V) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2EF) equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET)**. % 35.97/20.06 1528(e)[0:Res:74.2,1461.0] || tp__o(U) tp__o(V) -> equal(fo__c_2Ebool_2E_2F_5C(U,V),fo__c_2Ebool_2EF) equal(fo__c_2Ebool_2E_2F_5C(U,V),fo__c_2Ebool_2ET)**. % 35.97/20.06 1530(e)[5:Spt:1515.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 1534[5:Rew:1530.0,1429.0] || -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 1538(e)[5:Rew:1134.0,1534.0] || -> equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)**. % 35.97/20.06 1540[5:Rew:1538.0,37.0] || -> equal(inj__o(fo__c_2Ebool_2EF),c_2Ebool_2ET)**. % 35.97/20.06 1570[5:Rew:1538.0,1526.3] || tp__o(U) tp__o(V) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2EF)** equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2EF)**. % 35.97/20.06 1573(e)[5:Rew:36.0,1540.0] || -> equal(c_2Ebool_2ET,c_2Ebool_2EF)**. % 35.97/20.06 1589[5:Rew:1573.0,1235.2] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(inj__o(U),c_2Ebool_2EF)**. % 35.97/20.06 1661(e)[5:Obv:1589.1] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)**. % 35.97/20.06 1668[5:Rew:1661.1,1416.2] || tp__o(U) tp__o(V) -> p(c_2Ebool_2EF) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))*. % 35.97/20.06 1751[5:MRR:1668.2,31.0] || tp__o(U) tp__o(V) -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,V)))*. % 35.97/20.06 1777(e)[5:Obv:1570.2] || tp__o(U) tp__o(V) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,V),fo__c_2Ebool_2EF)**. % 35.97/20.06 1779[5:Rew:1777.2,1751.2] || tp__o(U)* tp__o(V)* -> p(inj__o(fo__c_2Ebool_2EF))*. % 35.97/20.06 1781[5:Con:1779.1] || tp__o(U)* -> p(inj__o(fo__c_2Ebool_2EF))*. % 35.97/20.06 1782[5:Rew:36.0,1781.1] || tp__o(U)* -> p(c_2Ebool_2EF)*. % 35.97/20.06 1783[5:MRR:1782.1,31.0] || tp__o(U)* -> . % 35.97/20.06 1784(e)[5:UnC:1783.0,20.0] || -> . % 35.97/20.06 1857[5:Spt:1784.0,1515.0,1530.0] || equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)** -> . % 35.97/20.06 1858[5:Spt:1784.0,1515.1] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2ET)**. % 35.97/20.06 1865[5:Rew:37.0,276.0,1858.0,276.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 1955(e)[0:EqF:1513.1,1513.0] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2EF)**. % 35.97/20.06 2114(e)[0:EqF:1235.2,1235.1] || tp__o(U) equal(c_2Ebool_2ET,c_2Ebool_2EF) -> equal(inj__o(U),c_2Ebool_2EF)**. % 35.97/20.06 2117[0:SpR:1235.2,63.1] || tp__o(U) tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(surj__o(c_2Ebool_2ET),U). % 35.97/20.06 2133[0:Obv:2117.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(surj__o(c_2Ebool_2ET),U). % 35.97/20.06 2134[0:Rew:348.0,2133.2] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(fo__c_2Ebool_2ET,U). % 35.97/20.06 2148[3:SpR:2134.1,1380.0] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc8,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)))* -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 35.97/20.06 2172[3:MRR:2148.2,31.0] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc8,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)))* -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2ET). % 35.97/20.06 2235[0:SpR:2114.2,63.1] || tp__o(U)* equal(c_2Ebool_2ET,c_2Ebool_2EF) tp__o(U)* -> equal(surj__o(c_2Ebool_2EF),U)*. % 35.97/20.06 2251[0:Obv:2235.0] || equal(c_2Ebool_2ET,c_2Ebool_2EF) tp__o(U)* -> equal(surj__o(c_2Ebool_2EF),U)*. % 35.97/20.06 2252(e)[0:Rew:349.0,2251.2] || equal(c_2Ebool_2ET,c_2Ebool_2EF) tp__o(U)* -> equal(fo__c_2Ebool_2EF,U). % 35.97/20.06 2263(e)[0:Res:35.0,2252.1] || equal(c_2Ebool_2ET,c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2EF)**. % 35.97/20.06 2277[0:SpR:1239.2,63.1] || tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> p(inj__o(U))* equal(surj__o(c_2Ebool_2ET),fo__c_2Ebool_2E_7E(U)). % 35.97/20.06 2288[0:Rew:348.0,2277.3] || tp__o(U) tp__o(fo__c_2Ebool_2E_7E(U)) -> p(inj__o(U))* equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET). % 35.97/20.06 2289[0:Rew:1525.1,2288.1] || tp__o(U) tp__o(fo__c_2Ebool_2EF) -> p(inj__o(U))* equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET). % 35.97/20.06 2290[0:MRR:2289.1,20.0] || tp__o(U) -> p(inj__o(U))* equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET). % 35.97/20.06 2300[0:SpR:2134.1,2290.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2ET,U) p(c_2Ebool_2EF) equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET)**. % 35.97/20.06 2306[0:Obv:2300.0] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) p(c_2Ebool_2EF) equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET)**. % 35.97/20.06 2307[0:MRR:2306.2,31.0] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(fo__c_2Ebool_2E_7E(U),fo__c_2Ebool_2ET)**. % 35.97/20.06 2388[0:SpR:2307.2,393.1] || tp__o(surj__o(U)) mem(U,bool) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(c_2Ebool_2E_7E,U),inj__o(fo__c_2Ebool_2ET))**. % 35.97/20.06 2394[0:Rew:37.0,2388.3,1513.0,2388.0] || tp__o(fo__c_2Ebool_2EF) mem(U,bool) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2ET)**. % 35.97/20.06 2395[0:MRR:2394.0,20.0] || mem(U,bool) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2ET)**. % 35.97/20.06 2676[0:SpR:2395.2,689.2] || mem(U,bool)* p(U) mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(c_2Ebool_2ET,c_2Ebool_2EF). % 35.97/20.06 2681(e)[0:Obv:2676.0] || p(U) mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(c_2Ebool_2ET,c_2Ebool_2EF). % 35.97/20.06 2869[0:SpR:36.0,132.2] || tp__o(U) tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Ebool_2E_2F_5C,inj__o(U)),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_2F_5C(U,fo__c_2Ebool_2EF)))**. % 35.97/20.06 2878[0:SpR:36.0,132.2] || tp__o(fo__c_2Ebool_2EF) tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),inj__o(U)),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U)))**. % 35.97/20.06 2883[0:SpR:37.0,132.2] || tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)))**. % 35.97/20.06 2887[0:SpL:132.2,120.0] || tp__o(U) tp__o(V) p(inj__o(fo__c_2Ebool_2E_2F_5C(U,V)))* mem(inj__o(U),bool) mem(inj__o(V),bool) -> p(inj__o(V)). % 35.97/20.06 2889[0:MRR:2869.1,20.0] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,inj__o(U)),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_2F_5C(U,fo__c_2Ebool_2EF)))**. % 35.97/20.06 2891[0:MRR:2878.0,20.0] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),inj__o(U)),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U)))**. % 35.97/20.06 2892[0:MRR:2883.0,23.0] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)))**. % 35.97/20.06 2912[0:MRR:2887.3,2887.4,56.1,56.1] || tp__o(U) tp__o(V) p(inj__o(fo__c_2Ebool_2E_2F_5C(U,V)))* -> p(inj__o(V)). % 35.97/20.06 3116[3:Res:222.1,2172.0] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2ET)**. % 35.97/20.06 3117[3:MRR:3116.0,259.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2ET)**. % 35.97/20.06 3415[0:Res:54.0,144.3] || del(ty_2Eextreal_2Eextreal) del(arr(ty_2Eextreal_2Eextreal,bool)) mem(U,ty_2Eextreal_2Eextreal) -> mem(ap(c_2Eextreal_2Eextreal__le,U),arr(ty_2Eextreal_2Eextreal,bool))*. % 35.97/20.06 3424[0:MRR:3415.0,22.0] || del(arr(ty_2Eextreal_2Eextreal,bool)) mem(U,ty_2Eextreal_2Eextreal) -> mem(ap(c_2Eextreal_2Eextreal__le,U),arr(ty_2Eextreal_2Eextreal,bool))*. % 35.97/20.06 4802[0:Res:88.1,160.2] || del(U) del(U) del(arr(U,bool)) mem(V,arr(U,arr(U,bool)))* -> equal(c_2Emin_2E_3D(U),V) mem(skf2(U,W,X),U)*. % 35.97/20.06 4811[0:Obv:4802.0] || del(U) del(arr(U,bool)) mem(V,arr(U,arr(U,bool)))*+ -> equal(c_2Emin_2E_3D(U),V) mem(skf2(U,W,X),U)*. % 35.97/20.06 4920[0:SpR:1492.1,123.3] || tp__o(U) p(c_2Ebool_2ET) mem(c_2Ebool_2ET,bool) mem(inj__o(U),bool) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U)))*. % 35.97/20.06 4945[0:MRR:4920.1,4920.2,4920.3,19.0,33.0,56.1] || tp__o(U) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U)))*. % 35.97/20.06 4950[0:SpR:2134.1,4945.1] || tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U))* tp__o(U) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 35.97/20.06 4953[0:MRR:4950.3,31.0] || tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U))* tp__o(U) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2ET). % 35.97/20.06 4977[0:SpR:36.0,1490.1] || tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)))**. % 35.97/20.06 4988[0:MRR:4977.0,20.0] || -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)))**. % 35.97/20.06 5033[0:SpR:36.0,1408.1] || tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))**. % 35.97/20.06 5044[0:MRR:5033.0,20.0] || -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))**. % 35.97/20.06 5065[0:SpR:4988.0,122.3] || p(c_2Ebool_2ET) mem(c_2Ebool_2EF,bool) mem(c_2Ebool_2ET,bool) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)))*. % 35.97/20.06 5068[0:MRR:5065.0,5065.1,5065.2,19.0,32.0,33.0] || -> p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)))*. % 35.97/20.06 5070[0:SpR:2134.1,5068.0] || tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET))* -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 35.97/20.06 5073[0:MRR:5070.2,31.0] || tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET))* -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET). % 35.97/20.06 5091[0:SpR:1406.1,124.3] || tp__o(U) p(c_2Ebool_2ET) mem(inj__o(U),bool) mem(c_2Ebool_2ET,bool) -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET)))*. % 35.97/20.06 5114[0:MRR:5091.1,5091.2,5091.3,19.0,56.1,33.0] || tp__o(U) -> p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET)))*. % 35.97/20.06 5129[0:SpR:2134.1,5114.1] || tp__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET))* tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 35.97/20.06 5132[0:MRR:5129.3,31.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET))* tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET). % 35.97/20.06 5137[0:SpL:5044.0,139.1] || p(c_2Ebool_2ET) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))* mem(c_2Ebool_2ET,bool) mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF). % 35.97/20.06 5138[0:MRR:5137.0,5137.2,5137.3,5137.4,19.0,33.0,32.0,31.0] || p(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))* -> . % 35.97/20.06 5140[0:SpR:1493.1,122.3] || tp__o(U) p(inj__o(U)) mem(c_2Ebool_2EF,bool) mem(inj__o(U),bool) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))*. % 35.97/20.06 5142[0:SpR:36.0,1493.1] || tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 35.97/20.06 5145[0:SpR:1235.2,1493.1] || tp__o(U) tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))*. % 35.97/20.06 5151[0:SpR:66.1,1493.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U))),ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U))**. % 35.97/20.06 5153[0:MRR:5142.0,20.0] || -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 35.97/20.06 5158[0:MRR:5151.1,35.0] || mem(U,bool) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U))),ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U))**. % 35.97/20.06 5159[0:Obv:5145.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))*. % 35.97/20.06 5160[0:Rew:4988.0,5159.2] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET)),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))*. % 35.97/20.06 5163[0:MRR:5140.2,5140.3,32.0,56.1] || tp__o(U) p(inj__o(U)) -> p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))*. % 35.97/20.06 5171[0:SpL:1233.2,5138.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* p(c_2Ebool_2ET) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 35.97/20.06 5173[0:MRR:5171.1,19.0] || tp__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 35.97/20.06 5189[0:Res:75.2,5073.0] || tp__o(fo__c_2Ebool_2EF) tp__o(fo__c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 35.97/20.06 5190[0:MRR:5189.0,5189.1,20.0,23.0] || -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 35.97/20.06 5196[0:Rew:5190.0,5160.2] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)),inj__o(fo__c_2Ebool_2ET))**. % 35.97/20.06 5203[0:Rew:37.0,5196.2] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF) equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)),c_2Ebool_2ET)**. % 35.97/20.06 5290[0:SpL:5153.0,138.0] || p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))* mem(c_2Ebool_2EF,bool) mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF) p(c_2Ebool_2EF). % 35.97/20.06 5293[0:Obv:5290.3] || p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))* mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF). % 35.97/20.06 5294[0:MRR:5293.1,5293.2,32.0,31.0] || p(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))* -> . % 35.97/20.06 5298[0:SpL:1233.2,5294.0] || tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF))* p(c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 35.97/20.06 5300[0:MRR:5298.1,19.0] || tp__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF))* -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 35.97/20.06 5303[0:Res:76.2,5173.0] || tp__o(fo__c_2Ebool_2ET) tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5304[0:MRR:5303.0,5303.1,23.0,20.0] || -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5315[0:SpR:1407.1,116.3] || tp__o(U) mem(inj__o(U),bool) mem(c_2Ebool_2EF,bool) -> p(inj__o(U)) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))*. % 35.97/20.06 5327[0:SpR:66.1,1407.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)),ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF))**. % 35.97/20.06 5334[0:MRR:5327.1,35.0] || mem(U,bool) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(U),fo__c_2Ebool_2EF)),ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF))**. % 35.97/20.06 5339[0:MRR:5315.1,5315.2,56.1,32.0] || tp__o(U) -> p(inj__o(U)) p(inj__o(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2EF)))*. % 35.97/20.06 5371[0:SpR:36.0,2889.1] || tp__o(fo__c_2Ebool_2EF) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 35.97/20.06 5376[0:SpR:37.0,2889.1] || tp__o(fo__c_2Ebool_2ET) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))**. % 35.97/20.06 5383[0:MRR:5371.0,20.0] || -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 35.97/20.06 5384[0:MRR:5376.0,23.0] || -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))**. % 35.97/20.06 5480[0:Res:75.2,5300.0] || tp__o(fo__c_2Ebool_2EF) tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5481[0:Obv:5480.0] || tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5482[0:MRR:5481.0,20.0] || -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5511[0:SpL:2891.1,121.0] || tp__o(U) p(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U)))* mem(c_2Ebool_2EF,bool) mem(inj__o(U),bool) -> p(c_2Ebool_2EF). % 35.97/20.06 5518[0:MRR:5511.2,5511.3,5511.4,32.0,56.1,31.0] || tp__o(U) p(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U)))* -> . % 35.97/20.06 5535[0:SpL:1233.2,5518.1] || tp__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U))* tp__o(U) p(c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U),fo__c_2Ebool_2EF). % 35.97/20.06 5537[0:MRR:5535.2,19.0] || tp__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U))* tp__o(U) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U),fo__c_2Ebool_2EF). % 35.97/20.06 5542[0:SpL:5383.0,121.0] || p(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))* mem(c_2Ebool_2EF,bool) mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF). % 35.97/20.06 5544[0:Obv:5542.1] || p(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))* mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF). % 35.97/20.06 5545[0:MRR:5544.1,5544.2,32.0,31.0] || p(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))* -> . % 35.97/20.06 5552[0:SpR:2134.1,2892.1] || tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)))*. % 35.97/20.06 5559[0:SpR:66.1,2892.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,surj__o(U))),ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U))**. % 35.97/20.06 5562[0:Obv:5552.0] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)))*. % 35.97/20.06 5563[0:Rew:5384.0,5562.2] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)),inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)))*. % 35.97/20.06 5566[0:MRR:5559.1,35.0] || mem(U,bool) -> equal(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,surj__o(U))),ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U))**. % 35.97/20.06 5579[0:SpL:1233.2,5545.0] || tp__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF))* p(c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 35.97/20.06 5581[0:MRR:5579.1,19.0] || tp__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF))* -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 35.97/20.06 5587[0:SpL:5384.0,120.0] || p(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))* mem(c_2Ebool_2ET,bool) mem(c_2Ebool_2EF,bool) -> p(c_2Ebool_2EF). % 35.97/20.06 5588[0:MRR:5587.1,5587.2,5587.3,33.0,32.0,31.0] || p(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)))* -> . % 35.97/20.06 5592[0:SpL:1233.2,5588.0] || tp__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* p(c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 35.97/20.06 5594[0:MRR:5592.1,19.0] || tp__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF))* -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF). % 35.97/20.06 5679[0:Res:74.2,5581.0] || tp__o(fo__c_2Ebool_2EF) tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5680[0:Obv:5679.0] || tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5681[0:MRR:5680.0,20.0] || -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5682[0:Rew:5681.0,5383.0] || -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),c_2Ebool_2EF),inj__o(fo__c_2Ebool_2EF))**. % 35.97/20.06 5691[0:Rew:36.0,5682.0] || -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),c_2Ebool_2EF),c_2Ebool_2EF)**. % 35.97/20.06 5715[0:Res:74.2,5594.0] || tp__o(fo__c_2Ebool_2ET) tp__o(fo__c_2Ebool_2EF) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5716[0:MRR:5715.0,5715.1,23.0,20.0] || -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 5722[0:Rew:5716.0,5563.2] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)),inj__o(fo__c_2Ebool_2EF))**. % 35.97/20.06 5727[0:Rew:36.0,5722.2] || tp__o(U) -> equal(fo__c_2Ebool_2ET,U) equal(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)),c_2Ebool_2EF)**. % 35.97/20.06 7139[0:SpR:65.1,203.1] || mem(U,ty_2Eextreal_2Eextreal) tp__ty_2Eextreal_2Eextreal(surj__ty_2Eextreal_2Eextreal(U)) -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),U),inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,surj__ty_2Eextreal_2Eextreal(U))))**. % 35.97/20.06 7143[0:MRR:7139.1,34.0] || mem(U,ty_2Eextreal_2Eextreal) -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),U),inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,surj__ty_2Eextreal_2Eextreal(U))))**. % 35.97/20.06 8252[0:Res:75.2,4953.0] || tp__o(fo__c_2Ebool_2ET) tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2ET)**. % 35.97/20.06 8254[0:Obv:8252.1] || tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2ET)**. % 35.97/20.06 8255[0:MRR:8254.0,23.0] || tp__o(U) -> equal(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2ET,U),fo__c_2Ebool_2ET)**. % 35.97/20.06 8256[0:Rew:8255.1,1492.1] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2ET),inj__o(U)),inj__o(fo__c_2Ebool_2ET))**. % 35.97/20.06 8266[0:Rew:37.0,8256.1] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2ET),inj__o(U)),c_2Ebool_2ET)**. % 35.97/20.06 8304[0:SpR:66.1,8266.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2ET),U),c_2Ebool_2ET)**. % 35.97/20.06 8306[0:MRR:8304.1,35.0] || mem(U,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2ET),U),c_2Ebool_2ET)**. % 35.97/20.06 8601[0:Res:76.2,5132.0] || tp__o(U) tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 35.97/20.06 8603[0:Obv:8601.0] || tp__o(fo__c_2Ebool_2ET) tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 35.97/20.06 8604[0:MRR:8603.0,23.0] || tp__o(U) -> equal(fo__c_2Emin_2E_3D_3D_3E(U,fo__c_2Ebool_2ET),fo__c_2Ebool_2ET)**. % 35.97/20.06 8605[0:Rew:8604.1,1406.1] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2ET),inj__o(fo__c_2Ebool_2ET))**. % 35.97/20.06 8615[0:Rew:37.0,8605.1] || tp__o(U) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,inj__o(U)),c_2Ebool_2ET),c_2Ebool_2ET)**. % 35.97/20.06 8651[0:SpR:66.1,8615.1] || mem(U,bool) tp__o(surj__o(U)) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2ET),c_2Ebool_2ET)**. % 35.97/20.06 8653[0:MRR:8651.1,35.0] || mem(U,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2ET),c_2Ebool_2ET)**. % 35.97/20.06 9867[0:SpR:2134.1,1505.3] || tp__o(fo__c_2Ebool_2E_5C_2F(U,V))* tp__o(U) tp__o(V) p(inj__o(U)) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 35.97/20.06 9899[0:Rew:1527.2,9867.0] || tp__o(fo__c_2Ebool_2EF) tp__o(U) tp__o(V) p(inj__o(U)) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET)** p(c_2Ebool_2EF). % 35.97/20.06 9900(e)[0:MRR:9899.0,9899.5,20.0,31.0] || tp__o(U) tp__o(V) p(inj__o(U)) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET)**. % 35.97/20.06 9909[0:Res:74.2,5537.0] || tp__o(fo__c_2Ebool_2EF) tp__o(U) tp__o(U) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U),fo__c_2Ebool_2EF)**. % 35.97/20.06 9912[0:Obv:9909.1] || tp__o(fo__c_2Ebool_2EF) tp__o(U) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U),fo__c_2Ebool_2EF)**. % 35.97/20.06 9913[0:MRR:9912.0,20.0] || tp__o(U) -> equal(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2EF,U),fo__c_2Ebool_2EF)**. % 35.97/20.06 9914[0:Rew:9913.1,2891.1] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),inj__o(U)),inj__o(fo__c_2Ebool_2EF))**. % 35.97/20.06 9925[0:Rew:36.0,9914.1] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),inj__o(U)),c_2Ebool_2EF)**. % 35.97/20.06 10373[0:SpL:1233.2,2912.2] || tp__o(fo__c_2Ebool_2E_2F_5C(U,V))* tp__o(U) tp__o(V) p(c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_2F_5C(U,V),fo__c_2Ebool_2EF) p(inj__o(V)). % 35.97/20.06 10399[0:Rew:1528.3,10373.0] || tp__o(fo__c_2Ebool_2ET) tp__o(U) tp__o(V) p(c_2Ebool_2ET) -> equal(fo__c_2Ebool_2E_2F_5C(U,V),fo__c_2Ebool_2EF)** p(inj__o(V)). % 35.97/20.06 10400[0:MRR:10399.0,10399.3,23.0,19.0] || tp__o(U) tp__o(V) -> equal(fo__c_2Ebool_2E_2F_5C(U,V),fo__c_2Ebool_2EF)** p(inj__o(V)). % 35.97/20.06 10665[0:Res:3424.2,144.3] || del(arr(ty_2Eextreal_2Eextreal,bool)) mem(U,ty_2Eextreal_2Eextreal) del(ty_2Eextreal_2Eextreal) del(bool) mem(V,ty_2Eextreal_2Eextreal) -> mem(ap(ap(c_2Eextreal_2Eextreal__le,U),V),bool)*. % 35.97/20.06 10668[0:MRR:10665.0,10665.2,10665.3,79.2,22.0,26.0] || mem(U,ty_2Eextreal_2Eextreal) mem(V,ty_2Eextreal_2Eextreal) -> mem(ap(ap(c_2Eextreal_2Eextreal__le,U),V),bool)*. % 35.97/20.06 12344[0:SpR:66.1,1410.2] || mem(U,bool) mem(V,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(V),surj__o(U))),ap(ap(c_2Emin_2E_3D_3D_3E,V),U))**. % 35.97/20.06 12352(e)[0:MRR:12344.2,35.0] || mem(U,bool) mem(V,bool) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(surj__o(V),surj__o(U))),ap(ap(c_2Emin_2E_3D_3D_3E,V),U))**. % 35.97/20.06 12616[0:SpR:66.1,1494.2] || mem(U,bool) mem(V,bool) tp__o(surj__o(U)) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(surj__o(V),surj__o(U))),ap(ap(c_2Ebool_2E_5C_2F,V),U))**. % 35.97/20.06 12624(e)[0:MRR:12616.2,35.0] || mem(U,bool) mem(V,bool) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(surj__o(V),surj__o(U))),ap(ap(c_2Ebool_2E_5C_2F,V),U))**. % 35.97/20.06 13865[0:SpL:1516.2,207.2] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(skc6) p(inj__o(fo__c_2Ebool_2ET)) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)))* -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))*. % 35.97/20.06 13917(e)[0:Obv:13865.0] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(skc6) p(inj__o(fo__c_2Ebool_2ET)) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)))* -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))*. % 35.97/20.06 13918[1:Rew:37.0,13917.3,1269.0,13917.3,37.0,13917.2] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(skc6) p(c_2Ebool_2ET) p(c_2Ebool_2ET) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))*. % 35.97/20.06 13919[1:Obv:13918.2] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(skc6) p(c_2Ebool_2ET) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))*. % 35.97/20.06 13920[1:MRR:13919.1,13919.2,30.0,19.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))*. % 35.97/20.06 14405[1:SpR:2134.1,13920.2] || tp__o(fo__c_2Eextreal_2Eextreal__le(U,skc8))* tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2ET) equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF) p(c_2Ebool_2EF). % 35.97/20.06 14419[1:Rew:1523.1,14405.0] || tp__o(fo__c_2Ebool_2EF) tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2ET)** equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF) p(c_2Ebool_2EF). % 35.97/20.06 14420[1:MRR:14419.0,14419.4,20.0,31.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2ET)** equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF). % 35.97/20.06 15194[0:Res:52.0,4811.2] || del(bool) del(arr(bool,bool)) -> equal(c_2Emin_2E_3D(bool),c_2Emin_2E_3D_3D_3E) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 15195[0:Res:51.0,4811.2] || del(bool) del(arr(bool,bool)) -> equal(c_2Emin_2E_3D(bool),c_2Ebool_2E_5C_2F) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 15196[0:Res:50.0,4811.2] || del(bool) del(arr(bool,bool)) -> equal(c_2Emin_2E_3D(bool),c_2Ebool_2E_2F_5C) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 15792[1:SpL:1520.2,373.1] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Ebool_2ET)) -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U)))*. % 35.97/20.06 15818[1:Obv:15792.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Ebool_2ET)) -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U)))*. % 35.97/20.06 15819[1:Rew:37.0,15818.1] || tp__ty_2Eextreal_2Eextreal(U) p(c_2Ebool_2ET) -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U)))*. % 35.97/20.06 15820[1:MRR:15819.1,19.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U)))*. % 35.97/20.06 15837[1:SpR:2134.1,15820.2] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc6,U))* tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,U),fo__c_2Ebool_2ET) equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2EF) p(c_2Ebool_2EF). % 35.97/20.06 15850[1:Rew:1517.1,15837.0] || tp__o(fo__c_2Ebool_2EF) tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,U),fo__c_2Ebool_2ET) equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2EF)** p(c_2Ebool_2EF). % 35.97/20.06 15851[1:MRR:15850.0,15850.4,20.0,31.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,U),fo__c_2Ebool_2ET) equal(fo__c_2Eextreal_2Eextreal__le(skc8,U),fo__c_2Ebool_2EF)**. % 35.97/20.06 15861[3:SpR:15851.2,3117.0] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2ET)** equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF). % 35.97/20.06 17710[0:MRR:15194.0,26.0] || del(arr(bool,bool)) -> equal(c_2Emin_2E_3D(bool),c_2Emin_2E_3D_3D_3E) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 17711[0:Rew:17710.1,15195.2] || del(bool) del(arr(bool,bool)) -> equal(c_2Emin_2E_3D_3D_3E,c_2Ebool_2E_5C_2F) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 17712[0:MRR:17711.0,26.0] || del(arr(bool,bool)) -> equal(c_2Emin_2E_3D_3D_3E,c_2Ebool_2E_5C_2F) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 17713[0:Rew:17712.1,17710.1] || del(arr(bool,bool)) -> equal(c_2Emin_2E_3D(bool),c_2Ebool_2E_5C_2F) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 17714[0:Rew:17713.1,15196.2] || del(bool) del(arr(bool,bool)) -> equal(c_2Ebool_2E_5C_2F,c_2Ebool_2E_2F_5C) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 17715(e)[0:MRR:17714.0,26.0] || del(arr(bool,bool)) -> equal(c_2Ebool_2E_5C_2F,c_2Ebool_2E_2F_5C) mem(skf2(bool,U,V),bool)*. % 35.97/20.06 26288[0:SpR:5334.1,5339.2] || mem(U,bool) tp__o(surj__o(U)) -> p(inj__o(surj__o(U))) p(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF))*. % 35.97/20.06 26307[0:Rew:66.1,26288.2] || mem(U,bool) tp__o(surj__o(U)) -> p(U) p(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF))*. % 35.97/20.06 26308[0:Rew:862.1,26307.1] || mem(U,bool) tp__o(fo__c_2Ebool_2EF) -> p(U) p(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF))*. % 35.97/20.06 26309[0:MRR:26308.1,20.0] || mem(U,bool) -> p(U) p(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF))*. % 35.97/20.06 26403[0:SpR:5158.1,5163.2] || mem(U,bool) tp__o(surj__o(U)) p(inj__o(surj__o(U))) -> p(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U))*. % 35.97/20.06 26423[0:Rew:66.1,26403.2] || mem(U,bool) tp__o(surj__o(U)) p(U) -> p(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U))*. % 35.97/20.06 26743[0:SpR:5566.1,5727.2] || mem(U,bool) tp__o(surj__o(U)) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 35.97/20.06 26765[0:Rew:1513.0,26743.1] || mem(U,bool) tp__o(fo__c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 35.97/20.06 26766(e)[0:MRR:26765.1,20.0] || mem(U,bool) -> equal(surj__o(U),fo__c_2Ebool_2ET) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 35.97/20.06 29545[0:SpR:7143.1,10668.2] || mem(U,ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) mem(U,ty_2Eextreal_2Eextreal) -> mem(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,surj__ty_2Eextreal_2Eextreal(U))),bool)*. % 35.97/20.06 29566[0:Obv:29545.0] || mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) mem(U,ty_2Eextreal_2Eextreal) -> mem(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,surj__ty_2Eextreal_2Eextreal(U))),bool)*. % 35.97/20.06 29567[0:MRR:29566.0,198.0] || mem(U,ty_2Eextreal_2Eextreal) -> mem(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,surj__ty_2Eextreal_2Eextreal(U))),bool)*. % 35.97/20.06 29573[0:SpR:214.0,29567.1] || mem(inj__ty_2Eextreal_2Eextreal(skc8),ty_2Eextreal_2Eextreal) -> mem(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)),bool)*. % 35.97/20.06 32282[5:SpR:167.3,1865.0] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(skc6)))**. % 35.97/20.06 32284[5:Rew:180.0,32282.3] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc6)**. % 35.97/20.06 32285[5:MRR:32284.0,32284.1,32284.2,22.0,181.0,198.0] || -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc6)**. % 35.97/20.06 32357[5:SpR:32285.0,62.1] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))* -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc6). % 35.97/20.06 32363(e)[5:MRR:32357.0,259.0] || -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc6)**. % 35.97/20.06 32365[5:Rew:32363.0,382.0] || p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc8)))* -> . % 35.97/20.06 32399[5:Rew:1219.0,32365.0] || p(c_2Ebool_2ET)* -> . % 35.97/20.06 32400(e)[5:MRR:32399.0,19.0] || -> . % 35.97/20.06 32452[4:Spt:32400.0,480.0,1425.0] || p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc6)))* -> . % 35.97/20.06 32453[4:Spt:32400.0,480.1] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc7)))*. % 35.97/20.06 32515(e)[3:MRR:15861.0,259.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2ET)** equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF). % 35.97/20.06 32591[4:MRR:317.3,32452.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6)))*+ p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,U)))* -> . % 35.97/20.06 32738(e)[5:Spt:32515.1] || -> equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)**. % 35.97/20.06 32740(e)[5:Rew:32738.0,1134.0] || -> equal(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 32750[5:Rew:32738.0,1513.1] || -> equal(surj__o(U),fo__c_2Ebool_2EF)** equal(surj__o(U),fo__c_2Ebool_2EF)**. % 35.97/20.06 33058(e)[5:Obv:32750.0] || -> equal(surj__o(U),fo__c_2Ebool_2EF)**. % 35.97/20.06 33063[5:Rew:33058.0,393.1] || mem(U,bool) -> equal(inj__o(fo__c_2Ebool_2E_7E(fo__c_2Ebool_2EF)),ap(c_2Ebool_2E_7E,U))*. % 35.97/20.06 33089[5:Rew:33058.0,12624.2] || mem(U,bool) mem(V,bool) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U))),ap(ap(c_2Ebool_2E_5C_2F,V),U))*. % 35.97/20.06 33393[5:Rew:32740.0,33063.1] || mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),inj__o(fo__c_2Ebool_2EF))**. % 35.97/20.06 33394(e)[5:Rew:36.0,33393.1] || mem(U,bool) -> equal(ap(c_2Ebool_2E_7E,U),c_2Ebool_2EF)**. % 35.97/20.06 33396[5:Rew:33394.1,73.2] || mem(U,bool)* -> p(U) p(c_2Ebool_2EF). % 35.97/20.06 33407(e)[5:MRR:33396.2,31.0] || mem(U,bool)* -> p(U). % 35.97/20.06 33411[5:MRR:123.0,33407.1] || mem(U,bool) mem(V,bool) -> p(ap(ap(c_2Ebool_2E_5C_2F,U),V))*. % 35.97/20.06 33843[5:Rew:33058.0,33089.2] || mem(U,bool) mem(V,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,V),U),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 35.97/20.06 33844(e)[5:Rew:36.0,33843.2,5482.0,33843.2] || mem(U,bool) mem(V,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,V),U),c_2Ebool_2EF)**. % 35.97/20.06 33846[5:Rew:33844.2,33411.2] || mem(U,bool)* mem(V,bool)* -> p(c_2Ebool_2EF). % 35.97/20.06 33847[5:Con:33846.1] || mem(U,bool)* -> p(c_2Ebool_2EF). % 35.97/20.06 33848[5:MRR:33847.1,31.0] || mem(U,bool)* -> . % 35.97/20.06 33849(e)[5:UnC:33848.0,33.0] || -> . % 35.97/20.06 33963[5:Spt:33849.0,32515.1,32738.0] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)** -> . % 35.97/20.06 33964[5:Spt:33849.0,32515.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2ET)**. % 35.97/20.06 45904[4:SpL:1516.2,32591.1] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Ebool_2ET)) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,U)))* -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF). % 35.97/20.06 45938[4:Obv:45904.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Ebool_2ET)) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,U)))* -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF). % 35.97/20.06 45939[4:Rew:37.0,45938.1] || tp__ty_2Eextreal_2Eextreal(U) p(c_2Ebool_2ET) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,U)))* -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF). % 35.97/20.06 45940[4:MRR:45939.1,19.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,U)))* -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF). % 35.97/20.06 47336[4:SpL:1521.2,45940.1] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Ebool_2ET)) -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,U),fo__c_2Ebool_2EF)** equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 47356[4:Obv:47336.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Ebool_2ET)) -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,U),fo__c_2Ebool_2EF)** equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 47357[4:Rew:37.0,47356.1] || tp__ty_2Eextreal_2Eextreal(U) p(c_2Ebool_2ET) -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,U),fo__c_2Ebool_2EF)** equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 47358[4:MRR:47357.1,19.0] || tp__ty_2Eextreal_2Eextreal(U)+ -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,U),fo__c_2Ebool_2EF)** equal(fo__c_2Eextreal_2Eextreal__le(U,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 47365[4:Res:30.0,47358.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)** equal(fo__c_2Eextreal_2Eextreal__le(skc6,skc6),fo__c_2Ebool_2EF). % 35.97/20.06 48031[4:Rew:1250.0,47365.1] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)** equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF). % 35.97/20.06 48032[5:MRR:48031.1,33963.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 48108[5:Rew:48032.0,276.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Ebool_2EF)),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 48109[5:Rew:36.0,48108.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 49272[5:SpR:168.3,48109.0] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(skc7)))**. % 35.97/20.06 49274[5:Rew:197.0,49272.3] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc7)**. % 35.97/20.06 49275[5:MRR:49274.0,49274.1,49274.2,22.0,181.0,198.0] || -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc7)**. % 35.97/20.06 49370[5:SpR:49275.0,62.1] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))* -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc7). % 35.97/20.06 49376(e)[5:MRR:49370.0,259.0] || -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc7)**. % 35.97/20.06 49384[5:Rew:49376.0,382.0] || p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8)))* -> . % 35.97/20.06 49414[5:Rew:1231.0,49384.0] || p(c_2Ebool_2ET)* -> . % 35.97/20.06 49415(e)[5:MRR:49414.0,19.0] || -> . % 35.97/20.06 49474[2:Spt:49415.0,302.0,379.0] || p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)))* -> . % 35.97/20.06 49475[2:Spt:49415.0,302.1] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,skc7)))*. % 35.97/20.06 49477[0:MRR:29573.0,215.0] || -> mem(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)),bool)*. % 35.97/20.06 49492[2:MRR:332.0,49474.0] || -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 49499[0:MRR:26423.1,35.0] || mem(U,bool) p(U) -> p(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U))*. % 35.97/20.06 49602(e)[3:Spt:2681.3] || -> equal(c_2Ebool_2ET,c_2Ebool_2EF)**. % 35.97/20.06 49627(e)[3:Rew:49602.0,8653.1] || mem(U,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,U),c_2Ebool_2EF),c_2Ebool_2EF)**. % 35.97/20.06 50028[3:Rew:49602.0,2263.0] || equal(c_2Ebool_2EF,c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2EF)**. % 35.97/20.06 50204(e)[3:Obv:50028.0] || -> equal(surj__o(U),fo__c_2Ebool_2EF)**. % 35.97/20.06 50263[3:Rew:50204.0,12624.2] || mem(U,bool) mem(V,bool) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,surj__o(U))),ap(ap(c_2Ebool_2E_5C_2F,V),U))*. % 35.97/20.06 50456[3:Rew:49627.1,26309.2] || mem(U,bool)* -> p(U) p(c_2Ebool_2EF). % 35.97/20.06 50458(e)[3:MRR:50456.2,31.0] || mem(U,bool)* -> p(U). % 35.97/20.06 50464[3:MRR:122.0,50458.1] || mem(U,bool) mem(V,bool) -> p(ap(ap(c_2Ebool_2E_5C_2F,U),V))*. % 35.97/20.06 50997[3:Rew:50204.0,50263.2] || mem(U,bool) mem(V,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,V),U),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF)))**. % 35.97/20.06 50998(e)[3:Rew:36.0,50997.2,5482.0,50997.2] || mem(U,bool) mem(V,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,V),U),c_2Ebool_2EF)**. % 35.97/20.06 51000[3:Rew:50998.2,50464.2] || mem(U,bool)* mem(V,bool)* -> p(c_2Ebool_2EF). % 35.97/20.06 51001[3:Con:51000.1] || mem(U,bool)* -> p(c_2Ebool_2EF). % 35.97/20.06 51002[3:MRR:51001.1,31.0] || mem(U,bool)* -> . % 35.97/20.06 51003(e)[3:UnC:51002.0,32.0] || -> . % 35.97/20.06 51236[3:Spt:51003.0,2681.3,49602.0] || equal(c_2Ebool_2ET,c_2Ebool_2EF)** -> . % 35.97/20.06 51237[3:Spt:51003.0,2681.0,2681.1,2681.2] || p(U) mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2ET). % 35.97/20.06 52164[0:SpR:1955.1,66.1] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) mem(U,bool)* -> equal(inj__o(fo__c_2Ebool_2EF),U). % 35.97/20.06 52169(e)[0:Rew:36.0,52164.2] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF) mem(U,bool)* -> equal(c_2Ebool_2EF,U). % 35.97/20.06 52378(e)[0:Res:49477.0,601.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)))* equal(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)),c_2Ebool_2EF). % 35.97/20.06 52389[2:MRR:52378.0,49474.0] || -> equal(inj__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8)),c_2Ebool_2EF)**. % 35.97/20.06 52392[2:Rew:52389.0,292.0] || -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8)),c_2Ebool_2EF)**. % 35.97/20.06 52404[2:SpR:52389.0,63.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8))* -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc8),surj__o(c_2Ebool_2EF)). % 35.97/20.06 52409[2:Rew:349.0,52404.1] || tp__o(fo__c_2Eextreal_2Eextreal__le(skc7,skc8))* -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc8),fo__c_2Ebool_2EF). % 35.97/20.06 52410[2:MRR:52409.0,307.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc8),fo__c_2Ebool_2EF)**. % 35.97/20.06 53303[0:Res:33.0,52169.1] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)** -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 35.97/20.06 53319[3:MRR:53303.1,51236.0] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)** -> . % 35.97/20.06 57170[2:SpR:14420.1,52410.0] || tp__ty_2Eextreal_2Eextreal(skc7) -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)** equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF). % 35.97/20.06 63980[3:MRR:57170.0,57170.2,29.0,53319.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 64026[3:Rew:63980.0,276.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Ebool_2EF)),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 64027[3:Rew:36.0,64026.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 67475[0:SpR:10400.2,5566.1] || tp__o(fo__c_2Ebool_2ET) tp__o(surj__o(U)) mem(U,bool) -> p(inj__o(surj__o(U))) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U),inj__o(fo__c_2Ebool_2EF))**. % 35.97/20.06 67488[0:Rew:36.0,67475.4,66.1,67475.3] || tp__o(fo__c_2Ebool_2ET) tp__o(surj__o(U)) mem(U,bool) -> p(U) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 35.97/20.06 67489[0:Rew:26766.1,67488.1] || tp__o(fo__c_2Ebool_2ET) tp__o(fo__c_2Ebool_2ET) mem(U,bool) -> p(U) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 35.97/20.06 67490[0:Obv:67489.0] || tp__o(fo__c_2Ebool_2ET) mem(U,bool) -> p(U) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 35.97/20.06 67491[0:MRR:67490.0,23.0] || mem(U,bool) -> p(U) equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),U),c_2Ebool_2EF)**. % 35.97/20.06 68102[0:SpR:67491.2,2892.1] || mem(inj__o(U),bool) tp__o(U) -> p(inj__o(U)) equal(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)),c_2Ebool_2EF)**. % 35.97/20.06 68127[0:MRR:68102.0,56.1] || tp__o(U) -> p(inj__o(U)) equal(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)),c_2Ebool_2EF)**. % 35.97/20.06 73174[3:SpR:168.3,64027.0] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(skc7)))**. % 35.97/20.06 73176[3:Rew:197.0,73174.3] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc7)**. % 35.97/20.06 73177[3:MRR:73176.0,73176.1,73176.2,22.0,181.0,198.0] || -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc7)**. % 35.97/20.06 73268[3:SpR:73177.0,62.1] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))* -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc7). % 35.97/20.06 73276(e)[3:MRR:73268.0,259.0] || -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc7)**. % 35.97/20.06 73278[3:Rew:73276.0,49492.0] || -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 73303[3:Rew:52392.0,73278.0] || -> p(c_2Ebool_2EF)*. % 35.97/20.06 73304(e)[3:MRR:73303.0,31.0] || -> . % 35.97/20.06 73367[1:Spt:73304.0,251.0,372.0] || p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,skc8)))* -> . % 35.97/20.06 73368[1:Spt:73304.0,251.1] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc8,skc6)))*. % 35.97/20.06 73397[1:MRR:331.0,73367.0] || -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 73427[1:MRR:272.3,73367.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))*+ p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,U)))* -> . % 35.97/20.06 73433[1:MRR:236.2,73368.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc8)))* -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6))). % 35.97/20.06 73521(e)[2:Spt:2681.3] || -> equal(c_2Ebool_2ET,c_2Ebool_2EF)**. % 35.97/20.06 73525[2:Rew:73521.0,348.0] || -> equal(surj__o(c_2Ebool_2EF),fo__c_2Ebool_2ET)**. % 35.97/20.06 73557(e)[2:Rew:73521.0,8306.1] || mem(U,bool) -> equal(ap(ap(c_2Ebool_2E_5C_2F,c_2Ebool_2EF),U),c_2Ebool_2EF)**. % 35.97/20.06 73964[2:Rew:73521.0,2263.0] || equal(c_2Ebool_2EF,c_2Ebool_2EF) -> equal(surj__o(U),fo__c_2Ebool_2EF)**. % 35.97/20.06 73968(e)[2:Rew:349.0,73525.0] || -> equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)**. % 35.97/20.06 73979(e)[2:Rew:73968.0,5304.0] || -> equal(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,fo__c_2Ebool_2EF),fo__c_2Ebool_2EF)**. % 35.97/20.06 74146(e)[2:Obv:73964.0] || -> equal(surj__o(U),fo__c_2Ebool_2EF)**. % 35.97/20.06 74204[2:Rew:74146.0,12352.2] || mem(U,bool) mem(V,bool) -> equal(inj__o(fo__c_2Emin_2E_3D_3D_3E(fo__c_2Ebool_2EF,surj__o(U))),ap(ap(c_2Emin_2E_3D_3D_3E,V),U))*. % 35.97/20.06 74444[2:Rew:73557.1,49499.2] || mem(U,bool)* p(U) -> p(c_2Ebool_2EF). % 35.97/20.06 74445(e)[2:MRR:74444.2,31.0] || mem(U,bool)* p(U) -> . % 35.97/20.06 74448[2:MRR:116.2,74445.1] || mem(U,bool) mem(V,bool) -> p(ap(ap(c_2Emin_2E_3D_3D_3E,U),V))*. % 35.97/20.06 75023[2:Rew:73979.0,74204.2,74146.0,74204.2] || mem(U,bool) mem(V,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,V),U),inj__o(fo__c_2Ebool_2EF))**. % 35.97/20.06 75024(e)[2:Rew:36.0,75023.2] || mem(U,bool) mem(V,bool) -> equal(ap(ap(c_2Emin_2E_3D_3D_3E,V),U),c_2Ebool_2EF)**. % 35.97/20.06 75026[2:Rew:75024.2,74448.2] || mem(U,bool)* mem(V,bool)* -> p(c_2Ebool_2EF). % 35.97/20.06 75027[2:Con:75026.1] || mem(U,bool)* -> p(c_2Ebool_2EF). % 35.97/20.06 75028[2:MRR:75027.1,31.0] || mem(U,bool)* -> . % 35.97/20.06 75029(e)[2:UnC:75028.0,32.0] || -> . % 35.97/20.06 75337[2:Spt:75029.0,2681.3,73521.0] || equal(c_2Ebool_2ET,c_2Ebool_2EF)** -> . % 35.97/20.06 75338[2:Spt:75029.0,2681.0,2681.1,2681.2] || p(U) mem(U,bool)* -> equal(surj__o(U),fo__c_2Ebool_2ET). % 35.97/20.06 75339[2:MRR:53303.1,75337.0] || equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)** -> . % 35.97/20.06 75348(e)[3:Spt:17715.1] || -> equal(c_2Ebool_2E_5C_2F,c_2Ebool_2E_2F_5C)**. % 35.97/20.06 75425[3:Rew:75348.0,1493.1] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),inj__o(U)),inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)))**. % 35.97/20.06 75454[3:Rew:75348.0,8266.1] || tp__o(U) -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2ET),inj__o(U)),c_2Ebool_2ET)**. % 35.97/20.06 75476[3:Rew:75348.0,133.2] || tp__o(U) tp__o(V) -> equal(ap(ap(c_2Ebool_2E_2F_5C,inj__o(U)),inj__o(V)),inj__o(fo__c_2Ebool_2E_5C_2F(U,V)))**. % 35.97/20.06 75801(e)[3:Rew:2892.1,75454.1] || tp__o(U) -> equal(inj__o(fo__c_2Ebool_2E_2F_5C(fo__c_2Ebool_2ET,U)),c_2Ebool_2ET)**. % 35.97/20.06 75807[3:Rew:75801.1,68127.2] || tp__o(U) -> p(inj__o(U))* equal(c_2Ebool_2ET,c_2Ebool_2EF). % 35.97/20.06 75810[3:MRR:75807.2,75337.0] || tp__o(U) -> p(inj__o(U))*. % 35.97/20.06 75830(e)[3:MRR:9900.2,75810.1] || tp__o(U) tp__o(V) -> equal(fo__c_2Ebool_2E_5C_2F(U,V),fo__c_2Ebool_2ET)**. % 35.97/20.06 75947(e)[3:Rew:9925.1,75425.1] || tp__o(U) -> equal(inj__o(fo__c_2Ebool_2E_5C_2F(fo__c_2Ebool_2EF,U)),c_2Ebool_2EF)**. % 35.97/20.06 75948[3:Rew:75947.1,5203.2] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)** equal(c_2Ebool_2ET,c_2Ebool_2EF). % 35.97/20.06 75954(e)[3:MRR:75948.2,75337.0] || tp__o(U) -> equal(inj__o(U),c_2Ebool_2EF)**. % 35.97/20.06 76069[3:Rew:75954.1,75476.2,75954.1,75476.2,37.0,75476.2,75830.2,75476.2] || tp__o(U)* tp__o(V)* -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),c_2Ebool_2EF),c_2Ebool_2ET)**. % 35.97/20.06 76070[3:Con:76069.1] || tp__o(U)* -> equal(ap(ap(c_2Ebool_2E_2F_5C,c_2Ebool_2EF),c_2Ebool_2EF),c_2Ebool_2ET)**. % 35.97/20.06 76071[3:Rew:5691.0,76070.1] || tp__o(U)* -> equal(c_2Ebool_2ET,c_2Ebool_2EF). % 35.97/20.06 76072[3:MRR:76071.1,75337.0] || tp__o(U)* -> . % 35.97/20.06 76073(e)[3:UnC:76072.0,20.0] || -> . % 35.97/20.06 76115[3:Spt:76073.0,17715.1,75348.0] || equal(c_2Ebool_2E_5C_2F,c_2Ebool_2E_2F_5C)** -> . % 35.97/20.06 76116(e)[3:Spt:76073.0,17715.0,17715.2] || del(arr(bool,bool)) -> mem(skf2(bool,U,V),bool)*. % 35.97/20.06 76143[4:Spt:1515.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 76152[4:Rew:76143.0,276.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Ebool_2EF)),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 76165[4:Rew:36.0,76152.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2EF),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 76914[1:SpR:136.2,73397.0] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) tp__ty_2Eextreal_2Eextreal(skc8) -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8)))*. % 35.97/20.06 76936[1:MRR:76914.0,76914.1,259.0,28.0] || -> p(inj__o(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8)))*. % 35.97/20.06 76938[1:SpR:2134.1,76936.0] || tp__o(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8))* -> equal(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8),fo__c_2Ebool_2ET) p(c_2Ebool_2EF). % 35.97/20.06 76939[1:MRR:76938.2,31.0] || tp__o(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8))* -> equal(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8),fo__c_2Ebool_2ET). % 35.97/20.06 84085[1:Res:213.1,76939.0] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) -> equal(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8),fo__c_2Ebool_2ET)**. % 35.97/20.06 84087[1:MRR:84085.0,259.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc8),fo__c_2Ebool_2ET)**. % 35.97/20.06 84894[1:SpL:1523.2,73433.1] || tp__ty_2Eextreal_2Eextreal(U) tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Ebool_2ET)) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6)))*. % 35.97/20.06 84930[1:Obv:84894.0] || tp__ty_2Eextreal_2Eextreal(U) p(inj__o(fo__c_2Ebool_2ET)) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6)))*. % 35.97/20.06 84931[1:Rew:37.0,84930.1] || tp__ty_2Eextreal_2Eextreal(U) p(c_2Ebool_2ET) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6)))*. % 35.97/20.06 84932[1:MRR:84931.1,19.0] || tp__ty_2Eextreal_2Eextreal(U) -> equal(fo__c_2Eextreal_2Eextreal__le(U,skc8),fo__c_2Ebool_2EF) p(inj__o(fo__c_2Eextreal_2Eextreal__le(U,skc6)))*. % 35.97/20.06 85063[4:SpR:76143.0,84932.2] || tp__ty_2Eextreal_2Eextreal(skc7) -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc8),fo__c_2Ebool_2EF)** p(inj__o(fo__c_2Ebool_2EF)). % 35.97/20.06 88318[4:Rew:36.0,85063.2] || tp__ty_2Eextreal_2Eextreal(skc7) -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc8),fo__c_2Ebool_2EF)** p(c_2Ebool_2EF). % 35.97/20.06 88319[4:MRR:88318.0,88318.2,29.0,31.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc8),fo__c_2Ebool_2EF)**. % 35.97/20.06 88326[4:Rew:88319.0,292.0] || -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8)),inj__o(fo__c_2Ebool_2EF))**. % 35.97/20.06 88327[4:Rew:36.0,88326.0] || -> equal(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8)),c_2Ebool_2EF)**. % 35.97/20.06 92169[1:SpL:84087.0,73427.1] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) p(inj__o(fo__c_2Ebool_2ET)) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))* -> . % 35.97/20.06 92187[1:Rew:37.0,92169.1] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) p(c_2Ebool_2ET) p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))* -> . % 35.97/20.06 92188[1:MRR:92187.0,92187.1,259.0,19.0] || p(inj__o(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))* -> . % 35.97/20.06 92315[1:SpL:1517.2,92188.0] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) p(inj__o(fo__c_2Ebool_2ET)) -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2EF)**. % 35.97/20.06 92322[1:Rew:37.0,92315.1] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6)) p(c_2Ebool_2ET) -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2EF)**. % 35.97/20.06 92323[1:MRR:92322.0,92322.1,259.0,19.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,fo__c_2Eextreal_2Eextreal__max(skc7,skc6)),fo__c_2Ebool_2EF)**. % 35.97/20.06 96839[4:SpR:168.3,76165.0] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(skc7)))**. % 35.97/20.06 96841[4:Rew:197.0,96839.3] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc7)**. % 35.97/20.06 96842[4:MRR:96841.0,96841.1,96841.2,22.0,181.0,198.0] || -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc7)**. % 35.97/20.06 96941[4:SpR:96842.0,62.1] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))* -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc7). % 35.97/20.06 96949(e)[4:MRR:96941.0,259.0] || -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc7)**. % 35.97/20.06 96951[4:Rew:96949.0,73397.0] || -> p(ap(ap(c_2Eextreal_2Eextreal__le,inj__ty_2Eextreal_2Eextreal(skc7)),inj__ty_2Eextreal_2Eextreal(skc8)))*. % 35.97/20.06 96985[4:Rew:88327.0,96951.0] || -> p(c_2Ebool_2EF)*. % 35.97/20.06 96986(e)[4:MRR:96985.0,31.0] || -> . % 35.97/20.06 97047[4:Spt:96986.0,1515.0,76143.0] || equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2EF)** -> . % 35.97/20.06 97048[4:Spt:96986.0,1515.1] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc7,skc6),fo__c_2Ebool_2ET)**. % 35.97/20.06 97136[4:Rew:97048.0,276.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),inj__o(fo__c_2Ebool_2ET)),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 97137[4:Rew:37.0,97136.0] || -> equal(surj__ty_2Eextreal_2Eextreal(ap(ap(ap(c_2Ebool_2ECOND(ty_2Eextreal_2Eextreal),c_2Ebool_2ET),inj__ty_2Eextreal_2Eextreal(skc6)),inj__ty_2Eextreal_2Eextreal(skc7))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))))**. % 35.97/20.06 106863[4:SpR:167.3,97137.0] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(skc6)))**. % 35.97/20.06 106865[4:Rew:180.0,106863.3] || del(ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc6),ty_2Eextreal_2Eextreal) mem(inj__ty_2Eextreal_2Eextreal(skc7),ty_2Eextreal_2Eextreal) -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc6)**. % 35.97/20.06 106866[4:MRR:106865.0,106865.1,106865.2,22.0,181.0,198.0] || -> equal(surj__ty_2Eextreal_2Eextreal(inj__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))),skc6)**. % 35.97/20.06 106958[4:SpR:106866.0,62.1] || tp__ty_2Eextreal_2Eextreal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6))* -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc6). % 35.97/20.06 106966(e)[4:MRR:106958.0,259.0] || -> equal(fo__c_2Eextreal_2Eextreal__max(skc7,skc6),skc6)**. % 35.97/20.06 106968[4:Rew:106966.0,92323.0] || -> equal(fo__c_2Eextreal_2Eextreal__le(skc6,skc6),fo__c_2Ebool_2EF)**. % 35.97/20.06 106987[4:Rew:1250.0,106968.0] || -> equal(fo__c_2Ebool_2ET,fo__c_2Ebool_2EF)**. % 35.97/20.06 106988(e)[4:MRR:106987.0,75339.0] || -> . % 35.97/20.06 % 35.97/20.06 % SZS output end CNFRefutation for /tmp/SPASST_697_n023.cluster.edu % 35.97/20.06 % 35.97/20.06 Formulae used in the proof : fof_ax_true_p fof_stp_fo_c_2Ebool_2EF fof_tp_ty_2Eextreal_2Eextreal fof_stp_fo_c_2Ebool_2ET fof_bool fof_conj_thm_2Eextreal_2Emax__le fof_ax_false_p fof_mem_c_2Ebool_2EF fof_mem_c_2Ebool_2ET fof_stp_surj_ty_2Eextreal_2Eextreal fof_stp_surj_o fof_stp_eq_fo_c_2Ebool_2EF fof_stp_eq_fo_c_2Ebool_2ET fof_stp_fo_c_2Ebool_2E_7E fof_mem_c_2Ebool_2E_2F_5C fof_mem_c_2Ebool_2E_5C_2F fof_mem_c_2Emin_2E_3D_3D_3E fof_mem_c_2Eextreal_2Eextreal__le fof_stp_inj_mem_ty_2Eextreal_2Eextreal fof_stp_inj_mem_o fof_stp_inj_surj_ty_2Eextreal_2Eextreal fof_stp_inj_surj_o fof_stp_iso_mem_ty_2Eextreal_2Eextreal fof_stp_iso_mem_o fof_ax_neg_p fof_stp_fo_c_2Ebool_2E_2F_5C fof_stp_fo_c_2Ebool_2E_5C_2F fof_stp_fo_c_2Emin_2E_3D_3D_3E fof_stp_fo_c_2Eextreal_2Eextreal__max fof_stp_fo_c_2Eextreal_2Eextreal__le fof_arr fof_mem_c_2Emin_2E_3D fof_stp_eq_fo_c_2Ebool_2E_7E fof_boolext fof_ax_imp_p fof_ax_and_p fof_ax_or_p fof_stp_eq_fo_c_2Ebool_2E_2F_5C fof_stp_eq_fo_c_2Ebool_2E_5C_2F fof_stp_eq_fo_c_2Emin_2E_3D_3D_3E fof_stp_eq_fo_c_2Eextreal_2Eextreal__max fof_stp_eq_fo_c_2Eextreal_2Eextreal__le fof_ap_tp fof_conj_thm_2Ebool_2ECOND__CLAUSES fof_conj_thm_2Eextreal_2Ele__total fof_funcext fof_ax_thm_2Eextreal_2Eextreal__max__def fof_conj_thm_2Eextreal_2Ele__trans % 79.74/41.94 % 79.74/41.95 SPASS+T ended %------------------------------------------------------------------------------