%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : ITP021_1 : TPTP v8.1.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n032.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 23.22s 13.08s % Output : Refutation 23.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : ITP021_1 : TPTP v8.1.0. Bugfixed v7.5.0. % 0.00/0.11 % Command : spasst-tptp-script %s %d % 0.11/0.30 % Computer : n032.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 600 % 0.11/0.31 % DateTime : Fri Jun 3 00:46:01 EDT 2022 % 0.11/0.31 % CPUTime : % 0.16/0.41 % Using EUF theory % 23.22/13.08 % 23.22/13.08 % 23.22/13.08 % SZS status Theorem for /tmp/SPASST_23070_n032.cluster.edu % 23.22/13.08 % 23.22/13.08 SPASS V 2.2.22 in combination with yices. % 23.22/13.08 SPASS beiseite: Proof found by SPASS. % 23.22/13.08 Problem: /tmp/SPASST_23070_n032.cluster.edu % 23.22/13.08 SPASS derived 34303 clauses, backtracked 16724 clauses and kept 25908 clauses. % 23.22/13.08 SPASS backtracked 42 times (0 times due to theory inconsistency). % 23.22/13.08 SPASS allocated 54996 KBytes. % 23.22/13.08 SPASS spent 0:00:11.72 on the problem. % 23.22/13.08 0:00:00.01 for the input. % 23.22/13.08 0:00:00.02 for the FLOTTER CNF translation. % 23.22/13.08 0:00:00.17 for inferences. % 23.22/13.08 0:00:00.56 for the backtracking. % 23.22/13.08 0:00:09.50 for the reduction. % 23.22/13.08 0:00:00.72 for interacting with the SMT procedure. % 23.22/13.08 % 23.22/13.08 % 23.22/13.08 % SZS output start CNFRefutation for /tmp/SPASST_23070_n032.cluster.edu % 23.22/13.08 % 23.22/13.08 % Here is a proof with depth 13, length 790 : % 23.22/13.08 2[0:Inp] || -> p(mono_2Ec_2Ebool_2ET_2E0)*. % 23.22/13.08 4[0:Inp] || -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__max_2E0)*. % 23.22/13.08 5[0:Inp] || -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__le_2E0)*. % 23.22/13.08 7[0:Inp] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0)*. % 23.22/13.08 8[0:Inp] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)*. % 23.22/13.08 26[0:Inp] || -> u(combin_i_2E0)*. % 23.22/13.08 27[0:Inp] || -> d(tyop_2Emin_2Ebool)*. % 23.22/13.08 28[0:Inp] || -> d(tyop_2Eextreal_2Eextreal)*. % 23.22/13.08 41[0:Inp] || -> mono_2Etyop_2Eextreal_2Eextreal(skc17)*. % 23.22/13.08 42(e)[0:Inp] || -> mono_2Etyop_2Eextreal_2Eextreal(skc16)*. % 23.22/13.08 43[0:Inp] || -> mono_2Etyop_2Eextreal_2Eextreal(skc15)*. % 23.22/13.08 44[0:Inp] || p(mono_2Ec_2Ebool_2EF_2E0)* -> . % 23.22/13.08 46[0:Inp] || -> u(skf5(U,V))*. % 23.22/13.08 70[0:Inp] || du(U) -> mono_2Etyop_2Emin_2Ebool(j_mono_2Etyop_2Emin_2Ebool(U))*. % 23.22/13.08 78[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U) -> u(i_mono_2Etyop_2Eextreal_2Eextreal(U))*. % 23.22/13.08 79[0:Inp] || mono_2Etyop_2Emin_2Ebool(U) -> u(i_mono_2Etyop_2Emin_2Ebool(U))*. % 23.22/13.08 80[0:Inp] || mono_2Etyop_2Emin_2Ebool(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E1(U))*. % 23.22/13.08 97[0:Inp] || mono_2Etyop_2Emin_2Ebool(U) -> p(U)* equal(mono_2Ec_2Ebool_2EF_2E0,U). % 23.22/13.08 108[0:Inp] || mono_2Etyop_2Emin_2Ebool(U) p(U)* -> equal(mono_2Ec_2Ebool_2ET_2E0,U). % 23.22/13.08 109[0:Inp] || mono_2Etyop_2Emin_2Ebool(U) equal(mono_2Ec_2Ebool_2ET_2E0,U) -> p(U)*. % 23.22/13.08 113[0:Inp] || mono_2Etyop_2Emin_2Ebool(U)* -> equal(U,mono_2Ec_2Ebool_2ET_2E0) equal(U,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 127[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(U))),U)**. % 23.22/13.08 128[0:Inp] || mono_2Etyop_2Emin_2Ebool(U) -> equal(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(U))),U)**. % 23.22/13.08 129[0:Inp] || mono_2Etyop_2Emin_2Ebool(U) p(U) p(mono_2Ec_2Ebool_2E_7E_2E1(U))* -> . % 23.22/13.08 130[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(U,V))*. % 23.22/13.08 131[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))*. % 23.22/13.08 135[0:Inp] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,V))*. % 23.22/13.08 136[0:Inp] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,V))*. % 23.22/13.08 137[0:Inp] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,V))*. % 23.22/13.08 138[0:Inp] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,V))*. % 23.22/13.08 151[0:Inp] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))*. % 23.22/13.08 152(e)[0:Inp] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))*. % 23.22/13.08 175[0:Inp] || mono_2Etyop_2Emin_2Ebool(U)+ mono_2Etyop_2Emin_2Ebool(V) -> p(U)* p(V)* equal(U,V)*. % 23.22/13.08 176[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U)+ mono_2Etyop_2Eextreal_2Eextreal(V) -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(V,U))*. % 23.22/13.08 185[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,U),V),mono_2Ec_2Eextreal_2Eextreal__max_2E2(U,V))**. % 23.22/13.08 186[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,U),V),mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))**. % 23.22/13.08 194[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V),V,U),mono_2Ec_2Eextreal_2Eextreal__max_2E2(U,V))**. % 23.22/13.08 203(e)[0:Inp] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))* -> . % 23.22/13.08 218[0:Inp] || d(U) u(V) -> equal(s(U,app_2E2(s(tyop_2Emin_2Efun(U,U),combin_i_2E0),s(U,V))),s(U,V))**. % 23.22/13.08 220[0:Inp] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) mono_2Etyop_2Eextreal_2Eextreal(W) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))*+ p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(V,W))* -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,W))*. % 23.22/13.08 233[0:Inp] || d(U) u(V) u(W) -> equal(s(U,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0)),s(U,V),s(U,W))),s(U,V))**. % 23.22/13.08 234[0:Inp] || d(U) u(V) u(W) -> equal(s(U,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)),s(U,V),s(U,W))),s(U,W))**. % 23.22/13.08 238[0:Inp] || d(U) u(V) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(U,tyop_2Emin_2Ebool),V))))) -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U,tyop_2Emin_2Ebool),V),s(U,skf5(V,U))))))*. % 23.22/13.08 245[0:Inp] || mono_2Etyop_2Emin_2Ebool(U) mono_2Etyop_2Eextreal_2Eextreal(V) mono_2Etyop_2Eextreal_2Eextreal(W) -> equal(s(tyop_2Eextreal_2Eextreal,c_2Ebool_2ECOND_2E3(s(tyop_2Emin_2Ebool,i_mono_2Etyop_2Emin_2Ebool(U)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(V)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(W)))),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(U,V,W))))**. % 23.22/13.08 247[0:Inp] || d(U) u(V) u(W) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(U,tyop_2Emin_2Ebool),W),s(U,V)))))* -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(U,tyop_2Emin_2Ebool),W))))). % 23.22/13.08 267[0:Res:43.0,186.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,U),skc15),mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))**. % 23.22/13.08 268[0:Res:43.0,176.0] || mono_2Etyop_2Eextreal_2Eextreal(U)+ -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,U))*. % 23.22/13.08 270[0:Res:43.0,127.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15))),skc15)**. % 23.22/13.08 272[0:Res:43.0,131.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))*. % 23.22/13.08 273[0:Res:43.0,135.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc15))*. % 23.22/13.08 274[0:Res:43.0,136.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc15))*. % 23.22/13.08 275[0:Res:43.0,137.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc15))*. % 23.22/13.08 276[0:Res:43.0,138.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc15))*. % 23.22/13.08 281[0:Res:43.0,194.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,U),U,skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,U))**. % 23.22/13.08 282[0:Res:43.0,185.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc15),U),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,U))**. % 23.22/13.08 283[0:Res:43.0,186.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15),U),mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,U))**. % 23.22/13.08 287[0:Res:43.0,131.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,U))*. % 23.22/13.08 299(e)[0:Res:42.0,176.0] || mono_2Etyop_2Eextreal_2Eextreal(U)+ -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc16))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,U))*. % 23.22/13.08 301(e)[0:Res:42.0,127.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16))),skc16)**. % 23.22/13.08 303(e)[0:Res:42.0,131.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc16))*. % 23.22/13.08 304(e)[0:Res:42.0,135.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc16))*. % 23.22/13.08 305(e)[0:Res:42.0,136.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc16))*. % 23.22/13.08 307(e)[0:Res:42.0,138.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc16))*. % 23.22/13.08 312(e)[0:Res:42.0,194.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,U),U,skc16),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,U))**. % 23.22/13.08 313(e)[0:Res:42.0,185.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),U),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,U))**. % 23.22/13.08 314(e)[0:Res:42.0,186.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc16),U),mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,U))**. % 23.22/13.08 317(e)[0:Res:42.0,130.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,U))*. % 23.22/13.08 318(e)[0:Res:42.0,131.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,U))*. % 23.22/13.08 325(e)[0:Res:41.0,220.0] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(V,skc17))* -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17))*. % 23.22/13.08 327(e)[0:Res:41.0,194.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17),skc17,U),mono_2Ec_2Eextreal_2Eextreal__max_2E2(U,skc17))**. % 23.22/13.08 328(e)[0:Res:41.0,185.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,U),skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(U,skc17))**. % 23.22/13.08 329(e)[0:Res:41.0,186.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,U),skc17),mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17))**. % 23.22/13.08 330(e)[0:Res:41.0,176.0] || mono_2Etyop_2Eextreal_2Eextreal(U)+ -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,U))*. % 23.22/13.08 332[0:Res:41.0,127.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17))),skc17)**. % 23.22/13.08 334(e)[0:Res:41.0,131.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17))*. % 23.22/13.08 336(e)[0:Res:41.0,136.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) -> mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc17))*. % 23.22/13.08 337(e)[0:Res:41.0,137.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc17))*. % 23.22/13.08 338(e)[0:Res:41.0,138.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(U,skc17))*. % 23.22/13.08 343(e)[0:Res:41.0,194.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,U),U,skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,U))**. % 23.22/13.08 344(e)[0:Res:41.0,185.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),U),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,U))**. % 23.22/13.08 349(e)[0:Res:41.0,131.1] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,U))*. % 23.22/13.08 363(e)[0:Res:43.0,325.0] || mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17))* -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17))*. % 23.22/13.08 372[0:Res:43.0,343.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),skc15,skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15))**. % 23.22/13.08 373[0:Res:43.0,327.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),skc17,skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17))**. % 23.22/13.08 374[0:Res:43.0,312.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc15),skc15,skc16),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15))**. % 23.22/13.08 376[0:Res:43.0,281.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15),skc15,skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15))**. % 23.22/13.08 379[0:Res:43.0,344.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15))**. % 23.22/13.08 380[0:Res:43.0,329.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15),skc17),mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17))**. % 23.22/13.08 381[0:Res:43.0,328.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc15),skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17))**. % 23.22/13.08 383[0:Res:43.0,313.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15))**. % 23.22/13.08 386[0:Res:43.0,283.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15),skc15),mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15))**. % 23.22/13.08 387[0:Res:43.0,282.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc15),skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15))**. % 23.22/13.08 392(e)[0:Res:43.0,330.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15))*. % 23.22/13.08 398[0:Res:43.0,268.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15))*. % 23.22/13.08 399[0:Res:43.0,349.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15))*. % 23.22/13.08 401[0:Res:43.0,334.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17))*. % 23.22/13.08 403[0:Res:43.0,318.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc15))*. % 23.22/13.08 404[0:Res:43.0,317.0] || -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15))*. % 23.22/13.08 407[0:Res:43.0,287.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15))*. % 23.22/13.08 432(e)[0:Res:42.0,325.0] || mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc16)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17))* -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17))*. % 23.22/13.08 442(e)[0:Res:42.0,327.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),skc17,skc16),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17))**. % 23.22/13.08 443[0:Res:42.0,312.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16),skc16,skc16),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16))**. % 23.22/13.08 449(e)[0:Res:42.0,329.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc16),skc17),mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17))**. % 23.22/13.08 450(e)[0:Res:42.0,328.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17))**. % 23.22/13.08 451[0:Res:42.0,314.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc16),skc16),mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16))**. % 23.22/13.08 452(e)[0:Res:42.0,313.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc16),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16))**. % 23.22/13.08 461(e)[0:Res:42.0,330.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc16))*. % 23.22/13.08 464[0:Res:42.0,299.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16))*. % 23.22/13.08 470(e)[0:Res:42.0,334.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17))*. % 23.22/13.08 472[0:Res:42.0,318.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16))*. % 23.22/13.08 510[0:Res:41.0,343.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17),skc17,skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17))**. % 23.22/13.08 517(e)[0:Res:41.0,344.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17))**. % 23.22/13.08 530[0:Res:41.0,330.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17))*. % 23.22/13.08 537[0:Res:41.0,349.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17))*. % 23.22/13.08 558[0:Obv:398.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15))*. % 23.22/13.08 559[0:Obv:464.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16))*. % 23.22/13.08 560[0:Obv:530.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17))*. % 23.22/13.08 568[1:Spt:392.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17))*. % 23.22/13.08 569(e)[1:MRR:203.1,568.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))* -> . % 23.22/13.08 570[1:MRR:363.2,568.0] || mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15)) -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17))*. % 23.22/13.08 575[2:Spt:461.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17))*. % 23.22/13.08 576[2:MRR:432.2,575.0] || mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc16)) -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17))*. % 23.22/13.08 578(e)[2:MRR:569.0,575.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))* -> . % 23.22/13.08 579(e)[2:Res:97.1,578.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 591[0:SpR:379.0,276.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17))* -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15)). % 23.22/13.08 595[0:SpR:380.0,337.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15))* -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17)). % 23.22/13.08 601[0:SpR:381.0,338.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc15))* -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17)). % 23.22/13.08 606(e)[0:Res:399.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 607[0:Res:403.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 609(e)[0:Res:401.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 611(e)[0:Res:407.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 614(e)[0:Res:537.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 616(e)[0:Res:470.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 617(e)[0:Res:472.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 620(e)[0:Res:334.1,113.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 621[0:Res:70.1,113.0] || du(U) -> equal(j_mono_2Etyop_2Emin_2Ebool(U),mono_2Ec_2Ebool_2ET_2E0)** equal(j_mono_2Etyop_2Emin_2Ebool(U),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 622[0:Res:80.1,113.0] || mono_2Etyop_2Emin_2Ebool(U) -> equal(mono_2Ec_2Ebool_2E_7E_2E1(U),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Ebool_2E_7E_2E1(U),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 626[3:Spt:609.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 630[3:Rew:626.0,373.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17))**. % 23.22/13.08 633[3:Rew:626.0,595.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15))* -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 728[3:Res:273.1,633.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__le_2E0)* -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 729[3:MRR:728.0,5.0] || -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)*. % 23.22/13.08 763[0:Res:109.2,44.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)* equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0) -> . % 23.22/13.08 766[0:MRR:763.0,8.0] || equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)** -> . % 23.22/13.08 808[0:SpR:383.0,276.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16))* -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15)). % 23.22/13.08 824[0:SpR:450.0,338.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16))* -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17)). % 23.22/13.08 829[0:SpR:387.0,276.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc15))* -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15)). % 23.22/13.08 834[0:SpR:452.0,307.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16))* -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16)). % 23.22/13.08 839[0:SpR:517.0,338.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17))* -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17)). % 23.22/13.08 850[0:Res:336.1,591.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__max_2E0) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15))*. % 23.22/13.08 851[0:MRR:850.0,4.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15))*. % 23.22/13.08 852(e)[0:Res:851.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 882[0:Res:274.1,601.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__max_2E0) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17))*. % 23.22/13.08 883[0:MRR:882.0,4.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17))*. % 23.22/13.08 884[0:Res:883.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 903[0:Res:97.1,129.2] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2E_7E_2E1(U))* mono_2Etyop_2Emin_2Ebool(U) p(U) -> equal(mono_2Ec_2Ebool_2E_7E_2E1(U),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 904[0:Rew:622.1,903.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0) mono_2Etyop_2Emin_2Ebool(U) p(U) -> equal(mono_2Ec_2Ebool_2E_7E_2E1(U),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 905[0:MRR:904.0,7.0] || mono_2Etyop_2Emin_2Ebool(U) p(U) -> equal(mono_2Ec_2Ebool_2E_7E_2E1(U),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 912[0:Res:305.1,808.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__max_2E0) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15))*. % 23.22/13.08 913[0:MRR:912.0,4.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15))*. % 23.22/13.08 914(e)[0:Res:913.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 915[4:Spt:914.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 923[4:Rew:915.0,579.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17)) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 924(e)[4:Rew:915.0,923.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 1032[0:Res:305.1,824.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__max_2E0) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17))*. % 23.22/13.08 1034(e)[0:MRR:1032.0,4.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17))*. % 23.22/13.08 1035(e)[0:Res:1034.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 1061[0:Res:274.1,829.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__max_2E0) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15))*. % 23.22/13.08 1063[0:MRR:1061.0,4.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15))*. % 23.22/13.08 1064[0:Res:1063.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 1090[0:Res:305.1,834.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__max_2E0) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16))*. % 23.22/13.08 1092(e)[0:MRR:1090.0,4.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16))*. % 23.22/13.08 1093(e)[0:Res:1092.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 1119[0:Res:336.1,839.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__max_2E0) -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17))*. % 23.22/13.08 1121(e)[0:MRR:1119.0,4.0] || -> mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17))*. % 23.22/13.08 1122(e)[0:Res:1121.0,113.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 1163(e)[4:Res:334.1,924.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 1164[4:MRR:1163.0,729.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 1213[0:Res:131.2,113.0] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 1265(e)[3:Res:729.0,268.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,mono_2Ec_2Ebool_2ET_2E0))*. % 23.22/13.08 1278[5:Spt:1265.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15))*. % 23.22/13.08 1280[5:Res:1278.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 1292[5:Res:272.1,1280.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 1294[5:MRR:1292.0,729.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 1324(e)[3:Res:729.0,299.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc16)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,mono_2Ec_2Ebool_2ET_2E0))*. % 23.22/13.08 1697[0:SpR:314.1,137.2] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc16))* mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,U))*. % 23.22/13.08 1714[0:Obv:1697.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc16))*+ mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,U))*. % 23.22/13.08 1736[0:Res:304.1,1714.0] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__le_2E0) mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,U))*. % 23.22/13.08 1738(e)[0:MRR:1736.0,5.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,U))*. % 23.22/13.08 1802[0:Res:80.1,175.0] || mono_2Etyop_2Emin_2Ebool(U)+ mono_2Etyop_2Emin_2Ebool(V) -> p(mono_2Ec_2Ebool_2E_7E_2E1(U))* p(V)* equal(mono_2Ec_2Ebool_2E_7E_2E1(U),V)*. % 23.22/13.08 1910[0:SpR:267.1,275.1] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,U))* -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15)). % 23.22/13.08 1989(e)[4:SpR:1164.0,570.2] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15))* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 1992[1:Res:570.2,108.1] || mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))* mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17)) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 1993[5:Rew:1294.0,1989.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) p(mono_2Ec_2Ebool_2ET_2E0)* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 1994(e)[5:MRR:1993.0,1993.1,1993.2,729.0,2.0,44.0] || -> . % 23.22/13.08 1995[1:Rew:620.2,1992.2] || mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))* mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 1996[1:MRR:1995.2,8.0] || mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 1999[5:Spt:1994.0,1265.0,1278.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15))* -> . % 23.22/13.08 2000[5:Spt:1994.0,1265.1] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,mono_2Ec_2Ebool_2ET_2E0))*. % 23.22/13.08 2016[4:Rew:915.0,374.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc15),skc15,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2057[5:Res:97.1,1999.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 2265[0:Res:559.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 2266[0:Rew:617.1,2265.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2267(e)[0:MRR:2266.0,8.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2270(e)[0:Rew:2267.0,451.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc16),skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2274[2:Res:575.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 2275[2:Rew:616.1,2274.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2276(e)[2:MRR:2275.0,8.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2283[0:Res:560.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 2284[0:Rew:614.1,2283.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2285[0:MRR:2284.0,8.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2300[0:Res:558.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 2301[0:Rew:611.1,2300.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2302[0:MRR:2301.0,8.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2305[0:Rew:2302.0,386.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15),skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2360[0:SpR:2267.0,1738.1] || mono_2Etyop_2Eextreal_2Eextreal(skc16)* -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 2508[3:Res:729.0,176.0] || mono_2Etyop_2Eextreal_2Eextreal(U)+ -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,U))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,mono_2Ec_2Ebool_2ET_2E0))*. % 23.22/13.08 2667[6:Spt:1324.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc16))*. % 23.22/13.08 2669[6:Res:2667.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc16))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc16),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 2692[5:Res:272.1,2057.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 2694[5:MRR:2692.0,729.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 2709[6:Res:303.1,2669.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2711[6:MRR:2709.0,729.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 2801[0:SpR:186.2,137.2] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,U))* mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))*. % 23.22/13.08 2824[0:Obv:2801.1] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eext(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,U))*+ mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))*. % 23.22/13.08 2949(e)[4:SpR:1164.0,576.2] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc16))* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 2953[6:Rew:2711.0,2949.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) p(mono_2Ec_2Ebool_2ET_2E0)* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 2954(e)[6:MRR:2953.0,2953.1,2953.2,729.0,2.0,44.0] || -> . % 23.22/13.08 2959[6:Spt:2954.0,1324.0,2667.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc16))* -> . % 23.22/13.08 2960[6:Spt:2954.0,1324.1] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,mono_2Ec_2Ebool_2ET_2E0))*. % 23.22/13.08 2962[0:Rew:2302.0,376.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15))**. % 23.22/13.08 2963(e)[0:Rew:2267.0,443.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc16,skc16),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16))**. % 23.22/13.08 2964(e)[0:Rew:2285.0,510.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17))**. % 23.22/13.08 3862[0:Res:135.2,1910.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__le_2E0) mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))*. % 23.22/13.08 3865[0:Obv:3862.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__le_2E0) mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))*. % 23.22/13.08 3866[0:MRR:3865.0,5.0] || mono_2Etyop_2Eextreal_2Eextreal(U) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,skc15))*. % 23.22/13.08 3870[5:SpR:2694.0,3866.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 3878[5:MRR:3870.0,729.0] || -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)*. % 23.22/13.08 3879(e)[5:Res:3878.0,2508.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2ET_2E0)). % 23.22/13.08 3881[5:Res:3878.0,176.0] || mono_2Etyop_2Eextreal_2Eextreal(U)+ -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,U))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,mono_2Ec_2Ebool_2EF_2E0))*. % 23.22/13.08 3882(e)[5:Res:3878.0,330.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17)) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,mono_2Ec_2Ebool_2EF_2E0))*. % 23.22/13.08 3890[7:Spt:3879.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0))*. % 23.22/13.08 3892[7:Res:3890.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 3898[8:Spt:3882.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17))*. % 23.22/13.08 3900[8:Res:3898.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 3918[7:Res:131.2,3892.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 3919[7:MRR:3918.0,3918.1,729.0,3878.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 3942[8:Res:334.1,3900.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 3944[8:MRR:3942.0,3878.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 4070[5:Res:3878.0,3881.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0))* p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0))*. % 23.22/13.08 4076[5:Obv:4070.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0))*. % 23.22/13.08 4078[5:Res:4076.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 4080[5:Res:131.2,4078.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 4081[5:Obv:4080.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 4082[5:MRR:4081.0,3878.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 4107[7:SpL:3919.0,220.3] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Ebool_2ET_2E0) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,U)) -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,U))*. % 23.22/13.08 4136[7:MRR:4107.0,4107.1,4107.3,729.0,3878.0,2.0] || mono_2Etyop_2Eextreal_2Eextreal(U) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,U)) -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,U))*. % 23.22/13.08 4849(e)[7:SpR:1164.0,4136.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17))* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 4850[7:SpR:2694.0,4136.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15))* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 4857[8:Rew:3944.0,4849.1] || mono_2Etyop_2Eextreal_2Eextreal(skc17) p(mono_2Ec_2Ebool_2ET_2E0)* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 4858(e)[8:MRR:4857.0,4857.1,4857.2,41.0,2.0,44.0] || -> . % 23.22/13.08 4864[8:Spt:4858.0,3882.0,3898.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17))* -> . % 23.22/13.08 4865[8:Spt:4858.0,3882.1] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,mono_2Ec_2Ebool_2EF_2E0))*. % 23.22/13.08 4866[7:MRR:4850.0,4850.2,43.0,44.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15))* -> . % 23.22/13.08 5400[7:Res:97.1,4866.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 5741[0:SpR:218.2,238.3] || d(tyop_2Emin_2Ebool) u(skf5(combin_i_2E0,tyop_2Emin_2Ebool)) d(tyop_2Emin_2Ebool) u(combin_i_2E0) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))))* -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,skf5(combin_i_2E0,tyop_2Emin_2Ebool)))). % 23.22/13.08 5747[0:Obv:5741.0] || u(skf5(combin_i_2E0,tyop_2Emin_2Ebool)) d(tyop_2Emin_2Ebool) u(combin_i_2E0) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))))* -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,skf5(combin_i_2E0,tyop_2Emin_2Ebool)))). % 23.22/13.08 5748(e)[0:MRR:5747.0,5747.1,5747.2,46.0,27.0,26.0] || p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))))* -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,skf5(combin_i_2E0,tyop_2Emin_2Ebool)))). % 23.22/13.08 5841[0:SpR:245.3,233.3] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0) mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) d(tyop_2Eextreal_2Eextreal) u(i_mono_2Etyop_2Eextreal_2Eextreal(U)) u(i_mono_2Etyop_2Eextreal_2Eextreal(V)) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,U,V))),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(U)))**. % 23.22/13.08 5842[0:SpR:245.3,234.3] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) d(tyop_2Eextreal_2Eextreal) u(i_mono_2Etyop_2Eextreal_2Eextreal(U)) u(i_mono_2Etyop_2Eextreal_2Eextreal(V)) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0,U,V))),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(V)))**. % 23.22/13.08 5850[0:MRR:5842.0,5842.3,5842.4,5842.5,8.0,28.0,78.1,78.1] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0,U,V))),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(V)))**. % 23.22/13.08 5851[0:MRR:5841.0,5841.3,5841.4,5841.5,7.0,28.0,78.1,78.1] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,U,V))),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(U)))**. % 23.22/13.08 5960[7:Res:272.1,5400.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 5962[7:MRR:5960.0,3878.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 6001[0:SpL:218.2,247.3] || d(tyop_2Emin_2Ebool) u(U) d(tyop_2Emin_2Ebool) u(U) u(combin_i_2E0) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,U)))* -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))))*. % 23.22/13.08 6009[0:Obv:6001.1] || d(tyop_2Emin_2Ebool) u(U) u(combin_i_2E0) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,U)))* -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))))*. % 23.22/13.08 6010(e)[0:MRR:6009.0,6009.2,27.0,26.0] || u(U) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,U)))* -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))))*. % 23.22/13.08 8763[1:SpL:2302.0,1996.1] || mono_2Etyop_2Eextreal_2Eextreal(skc15) p(mono_2Ec_2Ebool_2ET_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 9506[0:Res:135.2,2824.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__le_2E0) mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))*. % 23.22/13.08 9511[0:Obv:9506.1] || mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin(mono_2Ec_2Eextreal_2Eextreal__le_2E0) mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))*. % 23.22/13.08 9512[0:MRR:9511.0,5.0] || mono_2Etyop_2Eextreal_2Eextreal(U) mono_2Etyop_2Eextreal_2Eextreal(V) -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(U,V))*. % 23.22/13.08 9983(e)[0:Res:7.0,1802.0] || mono_2Etyop_2Emin_2Ebool(U) -> p(mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0))* p(U)* equal(mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0),U)*. % 23.22/13.08 10042[9:Spt:9983.1] || -> p(mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0))*. % 23.22/13.08 10043[9:SpR:905.2,10042.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0) p(mono_2Ec_2Ebool_2ET_2E0)* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 10049(e)[9:MRR:10043.0,10043.1,10043.2,7.0,2.0,44.0] || -> . % 23.22/13.08 10051[9:Spt:10049.0,9983.1,10042.0] || p(mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0))* -> . % 23.22/13.08 10052[9:Spt:10049.0,9983.0,9983.2,9983.3] || mono_2Etyop_2Emin_2Ebool(U)+ -> p(U)* equal(mono_2Ec_2Ebool_2E_7E_2E1(mono_2Ec_2Ebool_2ET_2E0),U)*. % 23.22/13.08 12899[0:SpL:621.1,5748.0] || du(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))) p(mono_2Ec_2Ebool_2ET_2E0) -> equal(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))),mono_2Ec_2Ebool_2EF_2E0)** p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,skf5(combin_i_2E0,tyop_2Emin_2Ebool)))). % 23.22/13.08 12903(e)[0:MRR:12899.1,2.0] || du(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))) -> equal(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))),mono_2Ec_2Ebool_2EF_2E0)** p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,skf5(combin_i_2E0,tyop_2Emin_2Ebool)))). % 23.22/13.08 12904[10:Spt:12903.1] || -> equal(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 12906[10:Rew:12904.0,6010.2] || u(U) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,U)))* -> p(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 12907[10:MRR:12906.2,44.0] || u(U) p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,U)))* -> . % 23.22/13.08 12928[10:SpL:128.1,12907.1] || mono_2Etyop_2Emin_2Ebool(U) u(i_mono_2Etyop_2Emin_2Ebool(U))* p(U) -> . % 23.22/13.08 12938[10:MRR:12928.1,79.1] || mono_2Etyop_2Emin_2Ebool(U) p(U)* -> . % 23.22/13.08 13050[10:Res:2.0,12938.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0)* -> . % 23.22/13.08 13087(e)[10:MRR:13050.0,7.0] || -> . % 23.22/13.08 13088[10:Spt:13087.0,12903.1,12904.0] || equal(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0)))),mono_2Ec_2Ebool_2EF_2E0)** -> . % 23.22/13.08 13089[10:Spt:13087.0,12903.0,12903.2] || du(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),combin_i_2E0))))* -> p(j_mono_2Etyop_2Emin_2Ebool(s(tyop_2Emin_2Ebool,skf5(combin_i_2E0,tyop_2Emin_2Ebool)))). % 23.22/13.08 13183[11:Spt:1064.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 13188[11:Rew:13183.0,2962.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 17294[11:SpR:13188.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 17356[11:Obv:17294.0] || mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 18873[11:MRR:17356.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 18874[11:Rew:18873.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc15)**. % 23.22/13.08 19570[11:SpR:18874.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 19573(e)[11:MRR:19570.0,729.0] || -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 19588[11:Rew:19573.0,626.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 19877[11:Rew:1164.0,19588.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 19878(e)[11:MRR:19877.0,766.0] || -> . % 23.22/13.08 20061[11:Spt:19878.0,1064.0,13183.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 20062[11:Spt:19878.0,1064.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 20068[11:Rew:20062.0,2962.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 20667[11:SpR:20068.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 20670[11:Obv:20667.0] || mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 20671[11:MRR:20670.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 20672[11:Rew:20671.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc15)**. % 23.22/13.08 20737[11:SpR:20672.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 20740(e)[11:MRR:20737.0,3878.0] || -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 20756[11:Rew:20740.0,5962.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 21125[11:Rew:4082.0,20756.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 21126(e)[11:MRR:21125.0,766.0] || -> . % 23.22/13.08 21871[7:Spt:21126.0,3879.0,3890.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0))* -> . % 23.22/13.08 21872[7:Spt:21126.0,3879.1] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2ET_2E0))*. % 23.22/13.08 21966[8:Spt:607.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 21968[8:Rew:21966.0,2016.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 22391[8:SpR:21968.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 22393[8:MRR:22391.0,22391.1,43.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 22394[8:Rew:22393.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc15)**. % 23.22/13.08 22957[8:SpR:22394.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 22960(e)[8:MRR:22957.0,729.0] || -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 22970[8:Rew:22960.0,626.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 23258[8:Rew:1164.0,22970.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 23259(e)[8:MRR:23258.0,766.0] || -> . % 23.22/13.08 23439[8:Spt:23259.0,607.0,21966.0] || equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 23440[8:Spt:23259.0,607.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 23445[8:Rew:23440.0,2016.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0,skc15,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 23904[8:SpR:23445.0,5850.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 23906[8:MRR:23904.0,23904.1,43.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 23907[8:Rew:23906.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc16)**. % 23.22/13.08 24717[8:SpR:23907.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc16,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 24720(e)[8:MRR:24717.0,729.0] || -> equal(skc16,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 24734[8:Rew:24720.0,2276.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25087[8:Rew:1164.0,24734.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 25088(e)[8:MRR:25087.0,766.0] || -> . % 23.22/13.08 25334[4:Spt:25088.0,914.0,915.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 25335[4:Spt:25088.0,914.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 25339[4:Rew:25335.0,404.0] || -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)*. % 23.22/13.08 25341[4:Rew:25335.0,578.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17))* -> . % 23.22/13.08 25342(e)[4:Rew:25335.0,383.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 25383[4:SpL:1213.2,25341.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) mono_2Etyop_2Eextreal_2Eextreal(skc17) p(mono_2Ec_2Ebool_2ET_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 25387[4:MRR:25383.1,25383.2,41.0,2.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 25388[4:MRR:25387.0,25339.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 25399[5:Spt:852.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25404[5:Rew:25399.0,379.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25425[6:Spt:884.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25430[6:Rew:25425.0,630.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25548[7:Spt:1093.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25553[7:Rew:25548.0,2963.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25795[6:SpR:25430.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 25797[6:MRR:25795.0,25795.1,41.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 25798[6:Rew:25797.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc17)**. % 23.22/13.08 25817[6:SpR:25798.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc17,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 25820[6:MRR:25817.0,729.0] || -> equal(skc17,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25837[6:Rew:25820.0,2276.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25839[6:Rew:25820.0,25388.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 25842[6:Rew:25820.0,25798.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 25955(e)[6:Rew:25820.0,25404.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 26395[7:SpR:25553.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc16) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 26398[7:Obv:26395.0] || mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 26399[7:MRR:26398.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 26400[7:Rew:26399.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc16)**. % 23.22/13.08 26412(e)[7:Rew:25842.0,26400.0] || -> equal(skc16,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 26552[7:Rew:26412.0,25342.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 26672[7:Rew:25955.0,26552.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 26673(e)[7:MRR:26672.0,766.0] || -> . % 23.22/13.08 26837[7:Spt:26673.0,1093.0,25548.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 26838[7:Spt:26673.0,1093.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 26860[7:Rew:26838.0,2963.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc16,skc16),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 27266[7:SpR:26860.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc16) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 27269[7:Obv:27266.0] || mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 27270[7:MRR:27269.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 27271[7:Rew:27270.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc16)**. % 23.22/13.08 28543[7:SpR:27271.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc16,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 28546(e)[7:MRR:28543.0,25339.0] || -> equal(skc16,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 28559[7:Rew:28546.0,25837.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 28815[7:Rew:25839.0,28559.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 28816(e)[7:MRR:28815.0,766.0] || -> . % 23.22/13.08 28971[6:Spt:28816.0,884.0,25425.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 28972[6:Spt:28816.0,884.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 28978[6:Rew:28972.0,630.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 29397[6:SpR:28978.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 29399[6:MRR:29397.0,29397.1,41.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 29400[6:Rew:29399.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc17)**. % 23.22/13.08 29414[6:SpR:29400.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 29417(e)[6:MRR:29414.0,25339.0] || -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 29426(e)[6:Rew:29417.0,25388.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 29430[6:Rew:29417.0,2285.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 29706[6:Rew:29426.0,29430.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 29707(e)[6:MRR:29706.0,766.0] || -> . % 23.22/13.08 29876[5:Spt:29707.0,852.0,25399.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 29877[5:Spt:29707.0,852.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 29884[5:Rew:29877.0,372.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 29924[6:Spt:1122.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 29929[6:Rew:29924.0,2964.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 29960[7:Spt:606.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 29967[7:Rew:29960.0,29884.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 30303[6:SpR:29929.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 30306[6:Obv:30303.0] || mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 30307[6:MRR:30306.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 30308[6:Rew:30307.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc17)**. % 23.22/13.08 30321[7:SpR:29967.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 30323[7:MRR:30321.0,30321.1,43.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 30324[7:Rew:30323.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc15)**. % 23.22/13.08 30338[6:SpR:30308.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc17,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 30341[6:MRR:30338.0,729.0] || -> equal(skc17,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 30352[6:Rew:30341.0,626.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 30354[6:Rew:30341.0,25388.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 30357[6:Rew:30341.0,30308.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 30832[7:SpR:30324.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 30835(e)[7:MRR:30832.0,25339.0] || -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 31066[7:Rew:30835.0,30352.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 31109[7:Rew:30354.0,31066.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 31110(e)[7:MRR:31109.0,766.0] || -> . % 23.22/13.08 31269[7:Spt:31110.0,606.0,29960.0] || equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 31270[7:Spt:31110.0,606.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 31285[7:Rew:30341.0,31270.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 31292[6:Rew:30341.0,29884.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),skc15,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 31293[7:Rew:31285.0,31292.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0,skc15,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 31743[7:SpR:31293.0,5850.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 31745(e)[7:MRR:31743.0,31743.1,43.0,729.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 31746[7:Rew:31745.0,30357.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 31763[7:SpR:31746.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 31766(e)[7:MRR:31763.0,31763.1,25339.0,766.0] || -> . % 23.22/13.08 31768[6:Spt:31766.0,1122.0,29924.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 31769[6:Spt:31766.0,1122.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 31775[6:Rew:31769.0,2964.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 32183[6:SpR:31775.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 32186[6:Obv:32183.0] || mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 32187[6:MRR:32186.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 32188[6:Rew:32187.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc17)**. % 23.22/13.08 32202[6:SpR:32188.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 32205(e)[6:MRR:32202.0,25339.0] || -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 32214(e)[6:Rew:32205.0,25388.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 32217[6:Rew:32205.0,2285.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 32494[6:Rew:32214.0,32217.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 32495(e)[6:MRR:32494.0,766.0] || -> . % 23.22/13.08 32664[3:Spt:32495.0,609.0,626.0] || equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 32665(e)[3:Spt:32495.0,609.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 32668[0:MRR:2360.0,42.0] || -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)*. % 23.22/13.08 32683[3:Rew:32665.0,8763.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) p(mono_2Ec_2Ebool_2ET_2E0)* -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 32684(e)[3:MRR:32683.0,32683.1,32683.2,43.0,2.0,766.0] || -> . % 23.22/13.08 32697[2:Spt:32684.0,461.0,575.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17))* -> . % 23.22/13.08 32698[2:Spt:32684.0,461.1] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc16))*. % 23.22/13.08 32702[2:MRR:152.0,32697.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))*. % 23.22/13.08 32703(e)[1:MRR:8763.0,8763.1,43.0,2.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 32706(e)[1:Rew:32703.0,380.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15),skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 32710(e)[1:Rew:32703.0,373.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc15),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17))**. % 23.22/13.08 32756[2:Res:97.1,32697.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 32757[2:Rew:616.0,32756.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 32758[2:MRR:32757.0,7.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc16,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 32761[2:Rew:32758.0,449.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc16),skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 32763[2:Rew:32758.0,442.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0,skc17,skc16),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17))**. % 23.22/13.08 32803[3:Spt:1035.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 32808[3:Rew:32803.0,450.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 32814[3:Rew:32803.0,32763.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0,skc17,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 32827[2:Res:32702.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 32829[4:Spt:914.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 32837[4:Rew:32829.0,32827.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17)) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 32838[4:Rew:32829.0,32837.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 33088[2:SpR:32758.0,9512.2] || mono_2Etyop_2Eextreal_2Eextreal(skc16) mono_2Etyop_2Eextreal_2Eextreal(skc17)* -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 33094[2:MRR:33088.0,33088.1,42.0,41.0] || -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)*. % 23.22/13.08 33166[3:SpR:32814.0,5850.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 33168[3:MRR:33166.0,33166.1,41.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 33169[3:Rew:33168.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc16)**. % 23.22/13.08 33183[3:SpR:33169.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc16,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 33186[3:MRR:33183.0,32668.0] || -> equal(skc16,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 33203[3:Rew:33186.0,32758.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 33206[3:Rew:33186.0,33169.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 33210[3:Rew:33186.0,32761.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2ET_2E0),skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 33212(e)[3:Rew:33186.0,2270.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 33298[3:Rew:33186.0,32808.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 33452[4:Rew:33203.0,32838.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 33456[4:Rew:33203.0,33452.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)* -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 33457(e)[4:MRR:33456.0,33456.1,8.0,766.0] || -> . % 23.22/13.08 33611[4:Spt:33457.0,914.0,32829.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 33612[4:Spt:33457.0,914.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 33631[4:Rew:33186.0,33612.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 33646[4:Rew:33631.0,383.0,33186.0,383.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 33648(e)[3:Rew:33186.0,607.1,33186.0,607.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 33654[4:Rew:33631.0,374.0,33186.0,374.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),skc15,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 33742[5:Spt:1122.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 33747[5:Rew:33742.0,2964.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 34059[5:SpR:33747.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 34062[5:Obv:34059.0] || mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 34063[5:MRR:34062.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 34064[5:Rew:34063.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc17)**. % 23.22/13.08 34076(e)[5:Rew:33206.0,34064.0] || -> equal(skc17,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 34290[5:Rew:34076.0,33210.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 34340[5:Rew:33212.0,34290.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 34341(e)[5:MRR:34340.0,766.0] || -> . % 23.22/13.08 34504[5:Spt:34341.0,1122.0,33742.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 34505[5:Spt:34341.0,1122.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 34511[5:Rew:34505.0,2964.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 34512[5:Rew:34505.0,517.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 34621[6:Spt:884.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 34626[6:Rew:34621.0,32710.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 34883[5:SpR:34511.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 34886[5:Obv:34883.0] || mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 34887[5:MRR:34886.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 34888[5:Rew:34887.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc17)**. % 23.22/13.08 34904[6:SpR:34626.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 34906[6:Rew:34887.0,34904.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 34907(e)[6:MRR:34906.0,34906.1,41.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 34908[6:Rew:34907.0,33206.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 34920(e)[6:Rew:34888.0,34908.0] || -> equal(skc17,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 34940[6:Rew:34920.0,33210.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 35196[6:Rew:33212.0,34940.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 35197(e)[6:MRR:35196.0,766.0] || -> . % 23.22/13.08 35355[6:Spt:35197.0,884.0,34621.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 35356[6:Spt:35197.0,884.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 35402[7:Spt:852.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 35407[7:Rew:35402.0,379.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 35458[8:Spt:33648.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 35460[8:Rew:35458.0,33654.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 35705[5:SpR:34888.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 35708[5:MRR:35705.0,33094.0] || -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 35724[5:Rew:35708.0,34888.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 35730(e)[7:Rew:35708.0,35407.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2EF_2E0),skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 35732(e)[5:Rew:35708.0,34512.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 35828[5:Rew:35708.0,32706.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 35829(e)[5:Rew:35708.0,33210.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 35830(e)[5:Rew:35708.0,33298.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 36223[8:SpR:35460.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 36225[8:MRR:36223.0,36223.1,43.0,32668.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 36226[8:Rew:36225.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc15)**. % 23.22/13.08 36238(e)[8:Rew:35724.0,36226.0] || -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 36460[8:Rew:36238.0,35730.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 36515[8:Rew:35732.0,36460.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 36516(e)[8:MRR:36515.0,766.0] || -> . % 23.22/13.08 36690[8:Spt:36516.0,33648.0,35458.0] || equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 36691[8:Spt:36516.0,33648.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 36703[8:Rew:36691.0,33654.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0,skc15,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 37004[8:SpR:36703.0,5850.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 37006(e)[8:MRR:37004.0,37004.1,43.0,32668.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 37007[8:Rew:37006.0,33206.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 37019[8:Rew:35724.0,37007.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 37020(e)[8:MRR:37019.0,766.0] || -> . % 23.22/13.08 37032[7:Spt:37020.0,852.0,35402.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 37033[7:Spt:37020.0,852.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 37179[8:Spt:1064.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 37184[8:Rew:37179.0,2962.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 37318[8:SpR:37184.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 37321[8:Obv:37318.0] || mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 37322[8:MRR:37321.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 37323[8:Rew:37322.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc15)**. % 23.22/13.08 37335(e)[8:Rew:33206.0,37323.0] || -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 37430[8:Rew:37335.0,35828.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 37610[8:Rew:35829.0,37430.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 37611(e)[8:MRR:37610.0,766.0] || -> . % 23.22/13.08 37820[8:Spt:37611.0,1064.0,37179.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 37821[8:Spt:37611.0,1064.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 37827[8:Rew:37821.0,2962.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 38099[8:SpR:37827.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 38102[8:Obv:38099.0] || mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 38103[8:MRR:38102.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 38104[8:Rew:38103.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc15)**. % 23.22/13.08 38116(e)[8:Rew:35724.0,38104.0] || -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 38157[8:Rew:38116.0,33646.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 38379[8:Rew:35830.0,38157.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 38380(e)[8:MRR:38379.0,766.0] || -> . % 23.22/13.08 38550[3:Spt:38380.0,1035.0,32803.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 38551[3:Spt:38380.0,1035.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 38557[3:Rew:38551.0,32763.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0,skc17,skc16),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 38558[3:Rew:38551.0,450.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 38603[4:Spt:914.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 38610[4:Rew:38603.0,383.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 38618[5:Spt:1064.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 38623[5:Rew:38618.0,2962.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 38642[6:Spt:884.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 38647[6:Rew:38642.0,32710.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 38978[3:SpR:38557.0,5850.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 38980[3:MRR:38978.0,38978.1,41.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 38981[3:Rew:38980.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc16)**. % 23.22/13.08 39000[5:SpR:38623.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 39003[5:Obv:39000.0] || mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 39004[5:MRR:39003.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 39005[5:Rew:39004.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc15)**. % 23.22/13.08 39018[6:SpR:38647.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 39020[6:MRR:39018.0,39018.1,41.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 39021[6:Rew:39020.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc17)**. % 23.22/13.08 39033(e)[6:Rew:39005.0,39021.0] || -> equal(skc17,skc15)**. % 23.22/13.08 39201[6:Rew:39033.0,38558.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 39296[6:Rew:38610.0,39201.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 39297(e)[6:MRR:39296.0,766.0] || -> . % 23.22/13.08 39461[6:Spt:39297.0,884.0,38642.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 39462[6:Spt:39297.0,884.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 39468[6:Rew:39462.0,32710.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 39723[3:SpR:38981.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc16,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 39726[3:MRR:39723.0,33094.0] || -> equal(skc16,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 39734[3:Rew:39726.0,32758.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 39737[3:Rew:39726.0,38981.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 39830(e)[3:Rew:39726.0,32761.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2EF_2E0),skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 39832(e)[3:Rew:39726.0,2270.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 40232[5:SpR:39005.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 40235[5:MRR:40232.0,32668.0] || -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 40422[6:Rew:40235.0,39468.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 41186[6:SpR:40422.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 41188[6:MRR:41186.0,41186.1,41.0,32668.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 41189[6:Rew:41188.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc17)**. % 23.22/13.08 41201(e)[6:Rew:39737.0,41189.0] || -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 41383[6:Rew:41201.0,39830.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 41470[6:Rew:39832.0,41383.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 41471(e)[6:MRR:41470.0,766.0] || -> . % 23.22/13.08 41643[5:Spt:41471.0,1064.0,38618.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 41644[5:Spt:41471.0,1064.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc15,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 41657[5:Rew:41644.0,2962.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 42090[5:SpR:41657.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 42093[5:Obv:42090.0] || mono_2Etyop_2Eextreal_2Eextreal(skc15) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 42094[5:MRR:42093.0,43.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 42095[5:Rew:42094.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc15)**. % 23.22/13.08 42107(e)[5:Rew:39737.0,42095.0] || -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 42137[5:Rew:42107.0,32706.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2EF_2E0),skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 42377[5:Rew:39830.0,42137.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 42378(e)[5:MRR:42377.0,766.0] || -> . % 23.22/13.08 42558[4:Spt:42378.0,914.0,38603.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 42559[4:Spt:42378.0,914.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 42564(e)[4:Rew:39726.0,42559.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 42582[3:Rew:39726.0,32827.1,39726.0,32827.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15),skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2EF_2E0,skc15),skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 42583[4:Rew:42564.0,42582.1,42564.0,42582.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 42584[4:Rew:39734.0,42583.1,39734.0,42583.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)* -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 42585(e)[4:MRR:42584.0,42584.1,8.0,766.0] || -> . % 23.22/13.08 42586[1:Spt:42585.0,392.0,568.0] || p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17))* -> . % 23.22/13.08 42587[1:Spt:42585.0,392.1] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15))*. % 23.22/13.08 42591[1:MRR:151.0,42586.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))*. % 23.22/13.08 42596[1:Res:42587.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 42597[1:Rew:606.1,42596.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 42598[1:MRR:42597.0,8.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 42605[1:Rew:42598.0,372.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc17),mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15))**. % 23.22/13.08 42638[1:Res:97.1,42586.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 42639[1:Rew:609.0,42638.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2ET_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 42640[1:MRR:42639.0,7.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 42646[1:Rew:42640.0,380.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15),skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 42652[2:Spt:852.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 42657[2:Rew:42652.0,379.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 42666[2:Rew:42652.0,42605.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 42708[1:Res:42591.0,108.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 42730[3:Spt:1122.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 42735[3:Rew:42730.0,2964.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 42948[1:SpR:42640.0,9512.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc17)* -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 42953[1:MRR:42948.0,42948.1,43.0,41.0] || -> mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)*. % 23.22/13.08 43069[2:SpR:42666.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 43071[2:MRR:43069.0,43069.1,43.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 43072[2:Rew:43071.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc15)**. % 23.22/13.08 43088[3:SpR:42735.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 43091[3:Obv:43088.0] || mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 43092[3:MRR:43091.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 43093[3:Rew:43092.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc17)**. % 23.22/13.08 43105(e)[3:Rew:43072.0,43093.0] || -> equal(skc17,skc15)**. % 23.22/13.08 43350[3:Rew:43105.0,42646.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,skc15),skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 43361[3:Rew:2305.0,43350.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 43362(e)[3:MRR:43361.0,766.0] || -> . % 23.22/13.08 43526[3:Spt:43362.0,1122.0,42730.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 43527[3:Spt:43362.0,1122.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 43533[3:Rew:43527.0,2964.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 43665[4:Spt:914.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 43671[4:Rew:43665.0,42708.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17)) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 43674[4:Rew:43665.0,43671.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17))* -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 43904[3:SpR:43533.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 43907[3:Obv:43904.0] || mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 43908[3:MRR:43907.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 43909[3:Rew:43908.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc17)**. % 23.22/13.08 43923[2:SpR:43072.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 43926[2:MRR:43923.0,32668.0] || -> equal(skc15,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 43937[2:Rew:43926.0,42640.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 43940[2:Rew:43926.0,43072.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 44148[2:Rew:43926.0,42657.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 44196[4:Rew:43937.0,43674.0] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0) -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2ET_2E0,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 44200[4:Rew:43937.0,44196.1] || mono_2Etyop_2Emin_2Ebool(mono_2Ec_2Ebool_2EF_2E0)* -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 44201(e)[4:MRR:44200.0,44200.1,8.0,766.0] || -> . % 23.22/13.08 44363[4:Spt:44201.0,914.0,43665.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 44364[4:Spt:44201.0,914.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 44383[4:Rew:43926.0,44364.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 44391[2:Rew:43926.0,2962.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0))**. % 23.22/13.08 44394[2:Rew:43926.0,387.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0))**. % 23.22/13.08 44398(e)[4:Rew:44383.0,383.0,43926.0,383.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 44400(e)[2:Rew:43926.0,1064.1,43926.0,1064.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)** equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 44489[5:Spt:44400.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 44495(e)[5:Rew:44489.0,44394.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 44533[6:Spt:1093.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 44538[6:Rew:44533.0,2963.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 44711[3:SpR:43909.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 44714[3:MRR:44711.0,42953.0] || -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 44726[3:Rew:44714.0,43909.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 44730(e)[3:Rew:44714.0,44148.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 45279[6:SpR:44538.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc16) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 45282[6:Obv:45279.0] || mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 45283[6:MRR:45282.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 45284[6:Rew:45283.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc16)**. % 23.22/13.08 45296(e)[6:Rew:43940.0,45284.0] || -> equal(skc16,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 45414[6:Rew:45296.0,44398.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 45555[6:Rew:44495.0,45414.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 45556(e)[6:MRR:45555.0,766.0] || -> . % 23.22/13.08 45718[6:Spt:45556.0,1093.0,44533.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 45719[6:Spt:45556.0,1093.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 45739[6:Rew:45719.0,2963.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc16,skc16),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46080[6:SpR:45739.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc16) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 46083[6:Obv:46080.0] || mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 46084[6:MRR:46083.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 46085[6:Rew:46084.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc16)**. % 23.22/13.08 46097(e)[6:Rew:44726.0,46085.0] || -> equal(skc16,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46111[6:Rew:46097.0,44398.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46362[6:Rew:44730.0,46111.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46363(e)[6:MRR:46362.0,766.0] || -> . % 23.22/13.08 46531[5:Spt:46363.0,44400.0,44489.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 46532[5:Spt:46363.0,44400.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46538[5:Rew:46532.0,44391.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46856[5:SpR:46538.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 46859[5:Obv:46856.0] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 46860(e)[5:MRR:46859.0,32668.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 46861[5:Rew:46860.0,43940.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 46873[5:Rew:44726.0,46861.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46874(e)[5:MRR:46873.0,766.0] || -> . % 23.22/13.08 46886[2:Spt:46874.0,852.0,42652.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 46887[2:Spt:46874.0,852.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46893[2:Rew:46887.0,42605.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc15,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46894[2:Rew:46887.0,379.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 46939[3:Spt:914.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 46946[3:Rew:46939.0,383.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),skc15),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 46954[4:Spt:1093.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 46959[4:Rew:46954.0,2963.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 46978[5:Spt:1122.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 46983[5:Rew:46978.0,2964.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 47306[2:SpR:46893.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc15) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 47308[2:MRR:47306.0,47306.1,43.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc15)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 47309[2:Rew:47308.0,270.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc15)**. % 23.22/13.08 47322[4:SpR:46959.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc16) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 47325[4:Obv:47322.0] || mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 47326[4:MRR:47325.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 47327[4:Rew:47326.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc16)**. % 23.22/13.08 47341[2:SpR:47309.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)* -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0). % 23.22/13.08 47344[2:MRR:47341.0,42953.0] || -> equal(skc15,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 47351[2:Rew:47344.0,42640.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 47358[2:Rew:47344.0,47309.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 47375(e)[2:Rew:47344.0,42646.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2EF_2E0),skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 47380(e)[2:Rew:47344.0,2305.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 47513(e)[2:Rew:47344.0,46894.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc17),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 47605[3:Rew:47344.0,46946.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,skc16),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 47824[4:SpR:47327.0,127.1] || mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)* -> equal(skc16,mono_2Ec_2Ebool_2ET_2E0). % 23.22/13.08 47827[4:MRR:47824.0,32668.0] || -> equal(skc16,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 47840[4:Rew:47827.0,47327.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 47940(e)[4:Rew:47827.0,47605.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 48361[5:SpR:46983.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 48364[5:Obv:48361.0] || mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 48365[5:MRR:48364.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0)))**. % 23.22/13.08 48366[5:Rew:48365.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0))),skc17)**. % 23.22/13.08 48378(e)[5:Rew:47840.0,48366.0] || -> equal(skc17,mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 48497[5:Rew:48378.0,47513.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2ET_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 48635[5:Rew:47940.0,48497.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 48636(e)[5:MRR:48635.0,766.0] || -> . % 23.22/13.08 48801[5:Spt:48636.0,1122.0,46978.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 48802[5:Spt:48636.0,1122.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc17,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 48837[5:Rew:48802.0,2964.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc17,skc17),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 48841(e)[2:Rew:47344.0,387.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0))**. % 23.22/13.08 49247[5:SpR:48837.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc17) mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 49250[5:Obv:49247.0] || mono_2Etyop_2Eextreal_2Eextreal(skc17) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 49251[5:MRR:49250.0,41.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc17)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 49252[5:Rew:49251.0,332.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc17)**. % 23.22/13.08 49264(e)[5:Rew:47358.0,49252.0] || -> equal(skc17,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 49293[5:Rew:49264.0,47375.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__le_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 49525[5:Rew:47380.0,49293.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 49526(e)[5:MRR:49525.0,766.0] || -> . % 23.22/13.08 49698[4:Spt:49526.0,1093.0,46954.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 49699[4:Spt:49526.0,1093.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc16),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 49711[4:Rew:49699.0,2963.0] || -> equal(mono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2ET_2E0,skc16,skc16),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 50133[4:SpR:49711.0,5851.2] || mono_2Etyop_2Eextreal_2Eextreal(skc16) mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 50136[4:Obv:50133.0] || mono_2Etyop_2Eextreal_2Eextreal(skc16) -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 50137[4:MRR:50136.0,42.0] || -> equal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(skc16)),s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0)))**. % 23.22/13.08 50138[4:Rew:50137.0,301.0] || -> equal(j_mono_2Etyop_2Eextreal_2Eextreal(s(tyop_2Eextreal_2Eextreal,i_mono_2Etyop_2Eextreal_2Eextreal(mono_2Ec_2Ebool_2EF_2E0))),skc16)**. % 23.22/13.08 50150(e)[4:Rew:47358.0,50138.0] || -> equal(skc16,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 50151(e)[4:Rew:50150.0,49699.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(mono_2Ec_2Ebool_2EF_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 50164(e)[4:Rew:50150.0,47605.0] || -> equal(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_(mono_2Ec_2Eextreal_2Eextreal__max_2E0,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2ET_2E0)**. % 23.22/13.08 50637[4:Rew:50164.0,48841.0,50151.0,48841.0] || -> equal(mono_2Ec_2Ebool_2ET_2E0,mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 50638(e)[4:MRR:50637.0,766.0] || -> . % 23.22/13.08 50735[3:Spt:50638.0,914.0,46939.0] || equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2ET_2E0)** -> . % 23.22/13.08 50736[3:Spt:50638.0,914.1] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,skc15),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 50741(e)[3:Rew:47344.0,50736.0] || -> equal(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,mono_2Ec_2Ebool_2EF_2E0),mono_2Ec_2Ebool_2EF_2E0)**. % 23.22/13.08 50746[2:Rew:47344.0,42591.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Eextreal_2Eextreal__max_2E2(skc16,mono_2Ec_2Ebool_2EF_2E0),skc17))*. % 23.22/13.08 50747[3:Rew:50741.0,50746.0] || -> p(mono_2Ec_2Eextreal_2Eextreal__le_2E2(mono_2Ec_2Ebool_2EF_2E0,skc17))*. % 23.22/13.08 50748[3:Rew:47351.0,50747.0] || -> p(mono_2Ec_2Ebool_2EF_2E0)*. % 23.22/13.08 50749(e)[3:MRR:50748.0,44.0] || -> . % 23.22/13.08 % 23.22/13.08 % SZS output end CNFRefutation for /tmp/SPASST_23070_n032.cluster.edu % 23.22/13.08 % 23.22/13.08 Formulae used in the proof : fof_reserved_2Eho_2Etruth fof_mono_2Ec_2Eextreal_2Eextreal__max_2E0 fof_mono_2Ec_2Eextreal_2Eextreal__le_2E0 fof_mono_2Ec_2Ebool_2ET_2E0 fof_mono_2Ec_2Ebool_2EF_2E0 fof_combin_i_2E0 fof_tyop_2Emin_2Ebool fof_tyop_2Eextreal_2Eextreal fof_thm_2Eextreal_2Emax__le fof_reserved_2Eho_2Enotfalse fof_reserved_2Equant_2E_3F fof_c_2Ebool_2E_7E_2E0 fof_j_mono_2Etyop_2Emin_2Ebool fof_i_mono_2Etyop_2Eextreal_2Eextreal fof_i_mono_2Etyop_2Emin_2Ebool fof_mono_2Ec_2Ebool_2E_7E_2E1 fof_thm_2Ebool_2EEQ__CLAUSES fof_reserved_2Eho_2Ebool__cases__ax fof_ji_2Emono_2Etyop_2Eextreal_2Eextreal fof_ji_2Emono_2Etyop_2Emin_2Ebool fof_reserved_2Elogic_2E_7E fof_mono_2Ec_2Eextreal_2Eextreal__max_2E2 fof_mono_2Ec_2Eextreal_2Eextreal__le_2E2 fof_mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Eextreal_2Eextreal_29 fof_mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_2Emin_2Efun_28tyop_2Eextreal_2Eextreal_2Ctyop_2Emin_2Ebool_29 fof_mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_2Eextreal_2Eextreal fof_mono_2Eapp_2E2_2Emono_2Etyop_2Eextreal_2Eextreal_20mono_2Etyop_2Emin_2Ebool fof_reserved_2Eho_2Eboolext fof_thm_2Eextreal_2Ele__total fof_arityeq2_2Ec_2Eextreal_2Eextreal__max_2E2 fof_arityeq2_2Ec_2Eextreal_2Eextreal__le_2E2 fof_thm_2Eextreal_2Eextreal__max__def fof_reserved_2Eho_2Ei__thm fof_thm_2Eextreal_2Ele__trans fof_thm_2Ebool_2ECOND__CLAUSES fof_monoeq_2Emono_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Eextreal_2Eextreal % 31.01/16.98 % 31.01/16.98 SPASS+T ended %------------------------------------------------------------------------------