%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWV238+1 : TPTP v9.0.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n013.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 : 300s % DateTime : Wed Apr 9 09:29:50 PM UTC 2025 % Result : CounterSatisfiable 30.60s 18.85s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.09 % Problem : SWV238+1 : TPTP v9.0.0. Released v3.2.0. % 0.03/0.10 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.09/0.30 % Computer : n013.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Wed Apr 9 02:51:47 EDT 2025 % 0.09/0.30 % CPUTime : % 30.60/18.85 % 30.60/18.85 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.60/18.85 % 30.60/18.85 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.60/18.86 %$ p > enc > #nlpp > i > zcmk > wk > w > tmk > tc > t2 > t1 > pp > lp > kk > k > a % 30.60/18.86 % 30.60/18.86 %Foreground sorts: % 30.60/18.86 % 30.60/18.86 % 30.60/18.86 %Background operators: % 30.60/18.86 % 30.60/18.86 % 30.60/18.86 %Foreground operators: % 30.60/18.86 tff(zcmk, type, zcmk: $i). % 30.60/18.86 tff(enc, type, enc: ($i * $i) > $i). % 30.60/18.86 tff(a, type, a: $i). % 30.60/18.86 tff(i, type, i: $i > $i). % 30.60/18.86 tff(pp, type, pp: $i). % 30.60/18.86 tff(w, type, w: $i). % 30.60/18.86 tff(k, type, k: $i). % 30.60/18.86 tff(p, type, p: $i > $o). % 30.60/18.86 tff(tmk, type, tmk: $i). % 30.60/18.86 tff(t2, type, t2: $i). % 30.60/18.86 tff(tc, type, tc: $i). % 30.60/18.86 tff(kk, type, kk: $i). % 30.60/18.86 tff(wk, type, wk: $i). % 30.60/18.86 tff(t1, type, t1: $i). % 30.60/18.86 tff(lp, type, lp: $i). % 30.60/18.86 % 30.60/18.86 %Saturated clause set: % 30.60/18.86 tff(c_64921, plain, (![V_1158, V_1159, V_2, V_1160]: (p(enc(enc(i(enc(i(zcmk), V_1158)), V_1159), V_2)) | ~p(V_1158) | ~p(V_1159) | ~p(V_1160) | ~p(enc(enc(i(zcmk), V_1160), V_2))))). % 30.60/18.87 tff(c_58329, plain, (![V_1065, V_4, V_1063, U_1064]: (p(enc(enc(i(enc(i(zcmk), V_1065)), V_4), enc(i(enc(i(zcmk), V_1063)), U_1064))) | ~p(V_1065) | ~p(V_4) | ~p(V_1063) | ~p(U_1064)))). % 30.60/18.87 tff(c_63948, plain, (![U_13, V_914, U_915, V_916]: (p(enc(enc(i(tmk), U_13), enc(i(enc(i(enc(i(zcmk), V_914)), U_915)), V_916))) | ~p(U_13) | ~p(V_916) | ~p(V_914) | ~p(U_915)))). % 30.60/18.87 tff(c_64198, plain, (![U_5, U_1147, V_1148, V_1149]: (p(enc(enc(U_5, U_1147), enc(i(enc(i(zcmk), V_1148)), V_1149))) | ~p(V_1148) | ~p(V_1149) | ~p(enc(zcmk, i(U_5))) | ~p(U_1147)))). % 30.60/18.87 tff(c_57049, plain, (![V_1050, U_1051, V_1053, V_4]: (p(enc(enc(i(V_1050), U_1051), enc(i(enc(i(zcmk), V_1053)), V_4))) | ~p(V_1053) | ~p(V_4) | ~p(enc(zcmk, V_1050)) | ~p(U_1051)))). % 30.60/18.87 tff(c_60702, plain, (![V_1094, V_1095, U_5, U_1097]: (p(enc(enc(i(enc(i(zcmk), V_1094)), V_1095), enc(U_5, U_1097))) | ~p(V_1094) | ~p(V_1095) | ~p(enc(zcmk, i(U_5))) | ~p(U_1097)))). % 30.60/18.87 tff(c_61677, plain, (![U_1110, V_1111, V_1112, V_4]: (p(enc(enc(U_1110, V_1111), V_1112)) | ~p(enc(zcmk, i(U_1110))) | ~p(V_1111) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_1112))))). % 30.60/18.87 tff(c_62135, plain, (![V_1118, U_1119, U_1120, V_4]: (p(enc(V_1118, enc(U_1119, U_1120))) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_1118)) | ~p(enc(zcmk, i(U_1119))) | ~p(U_1120)))). % 30.60/18.87 tff(c_61181, plain, (![V_1102, V_1103, V_1104, V_4]: (p(enc(enc(i(V_1102), V_1103), V_1104)) | ~p(enc(zcmk, V_1102)) | ~p(V_1103) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_1104))))). % 30.60/18.87 tff(c_61459, plain, (![U_1106, V_1107, U_5, U_1109]: (p(enc(enc(U_1106, V_1107), enc(U_5, U_1109))) | ~p(enc(zcmk, i(U_1106))) | ~p(V_1107) | ~p(enc(zcmk, i(U_5))) | ~p(U_1109)))). % 30.60/18.87 tff(c_61933, plain, (![V_2, U_1116, U_1117, U_1]: (p(enc(V_2, enc(U_1116, U_1117))) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2)) | ~p(enc(zcmk, i(U_1116))) | ~p(U_1117)))). % 30.60/18.87 tff(c_61000, plain, (![V_1098, V_1099, U_5, U_1101]: (p(enc(enc(i(V_1098), V_1099), enc(U_5, U_1101))) | ~p(enc(zcmk, V_1098)) | ~p(V_1099) | ~p(enc(zcmk, i(U_5))) | ~p(U_1101)))). % 30.60/18.87 tff(c_61445, plain, (![U_1106, V_1107, V_2, U_1]: (p(enc(enc(U_1106, V_1107), V_2)) | ~p(enc(zcmk, i(U_1106))) | ~p(V_1107) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.60/18.87 tff(c_60997, plain, (![U_5, V_1099, V_1100, U_1101]: (p(enc(enc(U_5, V_1099), enc(i(V_1100), U_1101))) | ~p(enc(zcmk, i(U_5))) | ~p(V_1099) | ~p(enc(zcmk, V_1100)) | ~p(U_1101)))). % 30.60/18.87 tff(c_60982, plain, (![V_1098, V_1099, V_2, U_1]: (p(enc(enc(i(V_1098), V_1099), V_2)) | ~p(enc(zcmk, V_1098)) | ~p(V_1099) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.60/18.87 tff(c_60676, plain, (![V_2, V_1095, V_1096, U_1097]: (p(enc(enc(i(V_2), V_1095), enc(i(V_1096), U_1097))) | ~p(enc(zcmk, V_2)) | ~p(V_1095) | ~p(enc(zcmk, V_1096)) | ~p(U_1097)))). % 30.60/18.87 tff(c_41536, plain, (![V_877, V_4, V_875, U_876]: (p(enc(enc(i(enc(i(zcmk), V_877)), V_4), enc(i(V_875), U_876))) | ~p(V_877) | ~p(V_4) | ~p(enc(zcmk, V_875)) | ~p(U_876)))). % 30.60/18.87 tff(c_58910, plain, (![U_1070, U_1, V_2, V_1073]: (p(enc(enc(i(tmk), U_1070), enc(U_1, V_2))) | ~p(V_2) | ~p(U_1070) | ~p(V_1073) | ~p(enc(enc(i(zcmk), V_1073), i(U_1)))))). % 30.60/18.87 tff(c_58912, plain, (![U_1070, U_3, V_4, V_1073]: (p(enc(enc(i(tmk), U_1070), enc(i(U_3), V_4))) | ~p(V_4) | ~p(U_1070) | ~p(V_1073) | ~p(enc(enc(i(zcmk), V_1073), U_3))))). % 30.60/18.87 tff(c_60148, plain, (![U_1078, U_5, U_1080, V_1081]: (p(enc(enc(i(tmk), U_1078), enc(i(enc(U_5, U_1080)), V_1081))) | ~p(V_1081) | ~p(U_1078) | ~p(enc(zcmk, i(U_5))) | ~p(U_1080)))). % 30.71/18.88 tff(c_41816, plain, (![U_878, V_880, U_881, V_4]: (p(enc(enc(i(tmk), U_878), enc(i(enc(i(V_880), U_881)), V_4))) | ~p(V_4) | ~p(U_878) | ~p(enc(zcmk, V_880)) | ~p(U_881)))). % 30.71/18.88 tff(c_40924, plain, (![V_866, V_868, U_869, V_4]: (p(enc(V_866, enc(i(enc(i(enc(i(zcmk), V_868)), U_869)), V_4))) | ~p(V_4) | ~p(enc(tmk, V_866)) | ~p(V_868) | ~p(U_869)))). % 30.71/18.88 tff(c_58541, plain, (![U_1066, V_1067, V_2, V_1068]: (p(enc(enc(i(tmk), U_1066), V_1067)) | ~p(enc(V_2, V_1067)) | ~p(U_1066) | ~p(V_1068) | ~p(enc(enc(i(zcmk), V_1068), V_2))))). % 30.71/18.88 tff(c_23315, plain, (![U_589, V_590, V_8, U_7]: (p(enc(enc(i(tmk), U_589), V_590)) | ~p(enc(enc(i(enc(i(zcmk), V_8)), U_7), V_590)) | ~p(U_589) | ~p(V_8) | ~p(U_7)))). % 30.71/18.88 tff(c_26821, plain, (![V_665, V_8, U_7, V_667]: (p(enc(V_665, enc(i(enc(i(zcmk), V_8)), U_7))) | ~p(V_667) | ~p(enc(enc(i(zcmk), V_667), V_665)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.88 tff(c_57797, plain, (![V_1054, V_2, V_1055, U_1056]: (p(enc(V_1054, V_2)) | ~p(enc(wk, V_1054)) | ~p(enc(enc(i(enc(i(zcmk), V_1055)), U_1056), V_2)) | ~p(V_1055) | ~p(U_1056)))). % 30.71/18.88 tff(c_45517, plain, (![V_2, V_914, U_915, V_916]: (p(enc(V_2, enc(i(enc(i(enc(i(zcmk), V_914)), U_915)), V_916))) | ~p(enc(wk, V_2)) | ~p(V_916) | ~p(V_914) | ~p(U_915)))). % 30.71/18.88 tff(c_38808, plain, (![W_822, U_1, V_2, V_825]: (p(enc(enc(i(wk), W_822), enc(U_1, V_2))) | ~p(W_822) | ~p(V_2) | ~p(V_825) | ~p(enc(enc(i(zcmk), V_825), i(U_1)))))). % 30.71/18.88 tff(c_24382, plain, (![V_8, U_7, V_602, U_603]: (p(enc(enc(i(enc(i(zcmk), V_8)), U_7), V_602)) | ~p(enc(zcmk, U_603)) | ~p(enc(U_603, V_602)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.88 tff(c_45579, plain, (![W_913, V_4, V_916, V_914]: (p(enc(enc(i(wk), W_913), enc(i(V_4), V_916))) | ~p(W_913) | ~p(V_916) | ~p(V_914) | ~p(enc(enc(i(zcmk), V_914), V_4))))). % 30.71/18.88 tff(c_41259, plain, (![V_870, U_3, V_4, V_873]: (p(enc(V_870, enc(i(U_3), V_4))) | ~p(V_4) | ~p(enc(tmk, V_870)) | ~p(V_873) | ~p(enc(enc(i(zcmk), V_873), U_3))))). % 30.71/18.88 tff(c_42197, plain, (![U_882, U_1, V_2, U_885]: (p(enc(enc(i(tmk), U_882), enc(U_1, V_2))) | ~p(V_2) | ~p(U_882) | ~p(enc(zcmk, U_885)) | ~p(enc(U_885, i(U_1)))))). % 30.71/18.88 tff(c_42199, plain, (![U_882, U_3, V_4, U_885]: (p(enc(enc(i(tmk), U_882), enc(i(U_3), V_4))) | ~p(V_4) | ~p(U_882) | ~p(enc(zcmk, U_885)) | ~p(enc(U_885, U_3))))). % 30.71/18.88 tff(c_41257, plain, (![V_870, U_1, V_2, V_873]: (p(enc(V_870, enc(U_1, V_2))) | ~p(V_2) | ~p(enc(tmk, V_870)) | ~p(V_873) | ~p(enc(enc(i(zcmk), V_873), i(U_1)))))). % 30.71/18.88 tff(c_52149, plain, (![V_986, V_987, V_988, V_4]: (p(enc(V_986, enc(i(V_987), V_988))) | ~p(enc(wk, V_986)) | ~p(V_988) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_987))))). % 30.71/18.88 tff(c_54268, plain, (![V_1006, U_5, U_1008, V_1009]: (p(enc(V_1006, enc(i(enc(U_5, U_1008)), V_1009))) | ~p(V_1009) | ~p(enc(tmk, V_1006)) | ~p(enc(zcmk, i(U_5))) | ~p(U_1008)))). % 30.71/18.88 tff(c_41818, plain, (![U_878, V_879, U_5, U_881]: (p(enc(enc(i(tmk), U_878), V_879)) | ~p(enc(enc(U_5, U_881), V_879)) | ~p(U_878) | ~p(enc(zcmk, i(U_5))) | ~p(U_881)))). % 30.71/18.88 tff(c_38011, plain, (![V_814, V_816, U_817, V_4]: (p(enc(V_814, enc(i(enc(i(V_816), U_817)), V_4))) | ~p(V_4) | ~p(enc(tmk, V_814)) | ~p(enc(zcmk, V_816)) | ~p(U_817)))). % 30.71/18.88 tff(c_40298, plain, (![W_850, U_852, U_853, V_4]: (p(enc(enc(i(wk), W_850), enc(i(enc(U_852, U_853)), V_4))) | ~p(W_850) | ~p(V_4) | ~p(enc(zcmk, i(U_852))) | ~p(U_853)))). % 30.71/18.88 tff(c_53001, plain, (![V_994, V_2, U_995, U_996]: (p(enc(V_994, V_2)) | ~p(enc(wk, V_994)) | ~p(enc(enc(U_995, U_996), V_2)) | ~p(enc(zcmk, i(U_995))) | ~p(U_996)))). % 30.71/18.88 tff(c_48584, plain, (![V_946, U_5, U_948, V_949]: (p(enc(V_946, enc(i(enc(U_5, U_948)), V_949))) | ~p(enc(wk, V_946)) | ~p(V_949) | ~p(enc(zcmk, i(U_5))) | ~p(U_948)))). % 30.71/18.88 tff(c_48565, plain, (![V_946, V_2, V_947, U_948]: (p(enc(V_946, V_2)) | ~p(enc(wk, V_946)) | ~p(enc(enc(i(V_947), U_948), V_2)) | ~p(enc(zcmk, V_947)) | ~p(U_948)))). % 30.71/18.88 tff(c_48819, plain, (![V_946, V_4, V_949, V_947]: (p(enc(V_946, enc(i(V_4), V_949))) | ~p(enc(wk, V_946)) | ~p(V_949) | ~p(enc(zcmk, V_947)) | ~p(enc(V_947, V_4))))). % 30.71/18.88 tff(c_51848, plain, (![U_1, V_2, V_982]: (p(enc(w, enc(U_1, V_2))) | ~p(V_2) | ~p(V_982) | ~p(enc(enc(i(zcmk), V_982), i(U_1)))))). % 30.71/18.88 tff(c_51484, plain, (![V_977, V_2, V_978]: (p(enc(w, V_977)) | ~p(enc(V_2, V_977)) | ~p(V_978) | ~p(enc(enc(i(zcmk), V_978), V_2))))). % 30.71/18.88 tff(c_51247, plain, (![V_2, V_974, V_975]: (p(enc(w, V_2)) | ~p(enc(enc(i(enc(i(zcmk), V_974)), V_975), V_2)) | ~p(V_974) | ~p(V_975)))). % 30.71/18.88 tff(c_51131, plain, (![V_973, V_4, V_972]: (p(enc(w, enc(i(enc(i(enc(i(zcmk), V_973)), V_4)), V_972))) | ~p(V_972) | ~p(V_973) | ~p(V_4)))). % 30.71/18.89 tff(c_49315, plain, (![V_953, V_954, V_4]: (p(enc(w, enc(i(V_953), V_954))) | ~p(V_954) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_953))))). % 30.71/18.89 tff(c_49208, plain, (![U_5, U_951, V_952]: (p(enc(w, enc(i(enc(U_5, U_951)), V_952))) | ~p(V_952) | ~p(enc(zcmk, i(U_5))) | ~p(U_951)))). % 30.71/18.89 tff(c_50088, plain, (![U_1, V_2, U_961]: (p(enc(w, enc(U_1, V_2))) | ~p(V_2) | ~p(enc(zcmk, U_961)) | ~p(enc(U_961, i(U_1)))))). % 30.71/18.89 tff(c_49682, plain, (![V_956, U_5, U_958]: (p(enc(w, V_956)) | ~p(enc(enc(U_5, U_958), V_956)) | ~p(enc(zcmk, i(U_5))) | ~p(U_958)))). % 30.71/18.89 tff(c_49671, plain, (![V_956, V_2, U_1]: (p(enc(w, V_956)) | ~p(enc(V_2, V_956)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.89 tff(c_49197, plain, (![V_2, V_950, U_951]: (p(enc(w, V_2)) | ~p(enc(enc(i(V_950), U_951), V_2)) | ~p(enc(zcmk, V_950)) | ~p(U_951)))). % 30.71/18.89 tff(c_49193, plain, (![V_2, V_952, U_1]: (p(enc(w, enc(i(V_2), V_952))) | ~p(V_952) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.89 tff(c_49130, plain, (![V_887, U_888, V_889]: (p(enc(w, enc(i(enc(i(V_887), U_888)), V_889))) | ~p(V_889) | ~p(enc(zcmk, V_887)) | ~p(U_888)))). % 30.71/18.89 tff(c_42402, plain, (![V_2, V_887, U_888, V_889]: (p(enc(V_2, enc(i(enc(i(V_887), U_888)), V_889))) | ~p(enc(wk, V_2)) | ~p(V_889) | ~p(enc(zcmk, V_887)) | ~p(U_888)))). % 30.71/18.89 tff(c_47834, plain, (![V_936, U_22]: (~p(V_936) | ~p(enc(enc(i(zcmk), V_936), i(enc(i(tc), U_22)))) | ~p(U_22)))). % 30.71/18.89 tff(c_47794, plain, (![V_930, V_4]: (~p(V_930) | ~p(enc(enc(i(zcmk), V_930), i(V_4))) | ~p(enc(tc, V_4))))). % 30.71/18.89 tff(c_47696, plain, (![V_927, U_25]: (~p(V_927) | ~p(enc(enc(i(zcmk), V_927), enc(i(tc), U_25))) | ~p(U_25)))). % 30.71/18.89 tff(c_47656, plain, (![V_936, U_37]: (~p(V_936) | ~p(enc(enc(i(zcmk), V_936), i(U_37))) | ~p(U_37)))). % 30.71/18.89 tff(c_47619, plain, (![V_936]: (~p(V_936) | ~p(enc(enc(i(zcmk), V_936), i(k)))))). % 30.71/18.89 tff(c_46156, plain, (![U_5, V_926, V_927]: (~p(enc(U_5, V_926)) | ~p(V_926) | ~p(V_927) | ~p(enc(enc(i(zcmk), V_927), i(U_5)))))). % 30.71/18.89 tff(c_46021, plain, (![V_2, V_922, U_923]: (~p(V_2) | ~p(enc(enc(i(enc(i(zcmk), V_922)), U_923), V_2)) | ~p(V_922) | ~p(U_923)))). % 30.71/18.89 tff(c_46151, plain, (![V_2, U_1, V_927]: (~p(V_2) | ~p(enc(U_1, V_2)) | ~p(V_927) | ~p(enc(enc(i(zcmk), V_927), U_1))))). % 30.71/18.89 tff(c_46017, plain, (![V_2, V_924, V_922]: (~p(enc(i(V_2), V_924)) | ~p(V_924) | ~p(V_922) | ~p(enc(enc(i(zcmk), V_922), V_2))))). % 30.71/18.89 tff(c_45900, plain, (![V_914, U_915, V_916]: (~p(enc(i(enc(i(enc(i(zcmk), V_914)), U_915)), V_916)) | ~p(V_916) | ~p(V_914) | ~p(U_915)))). % 30.71/18.89 tff(c_45749, plain, (![U_898, U_25]: (~p(enc(zcmk, U_898)) | ~p(enc(U_898, i(enc(i(tc), U_25)))) | ~p(U_25)))). % 30.71/18.89 tff(c_42594, plain, (![U_5, U_891, V_892]: (~p(enc(i(enc(U_5, U_891)), V_892)) | ~p(V_892) | ~p(enc(zcmk, i(U_5))) | ~p(U_891)))). % 30.71/18.89 tff(c_32857, plain, (![W_734, V_736, U_737, V_4]: (p(enc(enc(i(wk), W_734), enc(i(enc(i(enc(i(zcmk), V_736)), U_737)), V_4))) | ~p(W_734) | ~p(V_4) | ~p(V_736) | ~p(U_737)))). % 30.71/18.89 tff(c_45123, plain, (![U_895, U_25]: (~p(enc(zcmk, U_895)) | ~p(enc(U_895, enc(i(tc), U_25))) | ~p(U_25)))). % 30.71/18.89 tff(c_44978, plain, (![U_904, U_37]: (~p(enc(zcmk, U_904)) | ~p(enc(U_904, i(U_37))) | ~p(U_37)))). % 30.71/18.89 tff(c_43505, plain, (![V_899, U_5, U_901]: (~p(V_899) | ~p(enc(enc(U_5, U_901), V_899)) | ~p(enc(zcmk, i(U_5))) | ~p(U_901)))). % 30.71/18.89 tff(c_44352, plain, (![U_904]: (~p(enc(zcmk, U_904)) | ~p(enc(U_904, i(k)))))). % 30.71/18.89 tff(c_42719, plain, (![U_5, V_894, U_895]: (~p(enc(U_5, V_894)) | ~p(V_894) | ~p(enc(zcmk, U_895)) | ~p(enc(U_895, i(U_5)))))). % 30.71/18.89 tff(c_42583, plain, (![V_2, V_890, U_891]: (~p(V_2) | ~p(enc(enc(i(V_890), U_891), V_2)) | ~p(enc(zcmk, V_890)) | ~p(U_891)))). % 30.71/18.89 tff(c_42714, plain, (![V_2, U_1, U_895]: (~p(V_2) | ~p(enc(U_1, V_2)) | ~p(enc(zcmk, U_895)) | ~p(enc(U_895, U_1))))). % 30.71/18.89 tff(c_42579, plain, (![V_2, V_892, U_1]: (~p(enc(i(V_2), V_892)) | ~p(V_892) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.89 tff(c_42458, plain, (![V_887, U_888, V_889]: (~p(enc(i(enc(i(V_887), U_888)), V_889)) | ~p(V_889) | ~p(enc(zcmk, V_887)) | ~p(U_888)))). % 30.71/18.89 tff(c_32384, plain, (![W_721, V_723, U_724, V_4]: (p(enc(enc(i(wk), W_721), enc(i(enc(i(V_723), U_724)), V_4))) | ~p(W_721) | ~p(V_4) | ~p(enc(zcmk, V_723)) | ~p(U_724)))). % 30.71/18.89 tff(c_41810, plain, (![U_878, V_879, V_2, U_1]: (p(enc(enc(i(tmk), U_878), V_879)) | ~p(enc(V_2, V_879)) | ~p(U_878) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.89 tff(c_23312, plain, (![U_589, V_590, V_2, U_71]: (p(enc(enc(i(tmk), U_589), V_590)) | ~p(enc(enc(i(V_2), U_71), V_590)) | ~p(U_589) | ~p(enc(zcmk, V_2)) | ~p(U_71)))). % 30.71/18.89 tff(c_39356, plain, (![V_830, V_831, U_832, V_4]: (p(enc(V_830, enc(i(V_831), U_832))) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_830)) | ~p(enc(zcmk, V_831)) | ~p(U_832)))). % 30.71/18.89 tff(c_40915, plain, (![V_866, V_867, V_2, V_868]: (p(enc(V_866, V_867)) | ~p(enc(V_2, V_867)) | ~p(enc(tmk, V_866)) | ~p(V_868) | ~p(enc(enc(i(zcmk), V_868), V_2))))). % 30.71/18.89 tff(c_16598, plain, (![V_491, V_492, V_8, U_7]: (p(enc(V_491, V_492)) | ~p(enc(enc(i(enc(i(zcmk), V_8)), U_7), V_492)) | ~p(enc(tmk, V_491)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.89 tff(c_22909, plain, (![V_577, V_8, U_7, U_579]: (p(enc(V_577, enc(i(enc(i(zcmk), V_8)), U_7))) | ~p(enc(zcmk, U_579)) | ~p(enc(U_579, V_577)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.89 tff(c_37496, plain, (![W_808, U_3, V_4, U_811]: (p(enc(enc(i(wk), W_808), enc(i(U_3), V_4))) | ~p(W_808) | ~p(V_4) | ~p(enc(zcmk, U_811)) | ~p(enc(U_811, U_3))))). % 30.71/18.89 tff(c_37494, plain, (![W_808, U_1, V_2, U_811]: (p(enc(enc(i(wk), W_808), enc(U_1, V_2))) | ~p(W_808) | ~p(V_2) | ~p(enc(zcmk, U_811)) | ~p(enc(U_811, i(U_1)))))). % 30.71/18.89 tff(c_32386, plain, (![W_721, V_722, U_5, U_724]: (p(enc(enc(i(wk), W_721), V_722)) | ~p(W_721) | ~p(enc(enc(U_5, U_724), V_722)) | ~p(enc(zcmk, i(U_5))) | ~p(U_724)))). % 30.71/18.89 tff(c_38394, plain, (![V_818, U_3, V_4, U_821]: (p(enc(V_818, enc(i(U_3), V_4))) | ~p(V_4) | ~p(enc(tmk, V_818)) | ~p(enc(zcmk, U_821)) | ~p(enc(U_821, U_3))))). % 30.71/18.89 tff(c_38392, plain, (![V_818, U_1, V_2, U_821]: (p(enc(V_818, enc(U_1, V_2))) | ~p(V_2) | ~p(enc(tmk, V_818)) | ~p(enc(zcmk, U_821)) | ~p(enc(U_821, i(U_1)))))). % 30.71/18.89 tff(c_38013, plain, (![V_814, V_815, U_5, U_817]: (p(enc(V_814, V_815)) | ~p(enc(enc(U_5, U_817), V_815)) | ~p(enc(tmk, V_814)) | ~p(enc(zcmk, i(U_5))) | ~p(U_817)))). % 30.71/18.89 tff(c_22906, plain, (![V_577, V_2, U_71, U_579]: (p(enc(V_577, enc(i(V_2), U_71))) | ~p(enc(zcmk, U_579)) | ~p(enc(U_579, V_577)) | ~p(enc(zcmk, V_2)) | ~p(U_71)))). % 30.71/18.89 tff(c_39034, plain, (![V_4, U_827]: (~p(V_4) | ~p(enc(enc(i(zcmk), V_4), U_827)) | ~p(U_827)))). % 30.71/18.90 tff(c_38958, plain, (![U_821, U_37]: (~p(enc(zcmk, U_821)) | ~p(enc(U_821, U_37)) | ~p(U_37)))). % 30.71/18.90 tff(c_32911, plain, (![W_734, V_735, V_4, V_736]: (p(enc(enc(i(wk), W_734), V_735)) | ~p(W_734) | ~p(enc(V_4, V_735)) | ~p(V_736) | ~p(enc(enc(i(zcmk), V_736), V_4))))). % 30.71/18.90 tff(c_38005, plain, (![V_814, V_815, V_2, U_1]: (p(enc(V_814, V_815)) | ~p(enc(V_2, V_815)) | ~p(enc(tmk, V_814)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.90 tff(c_16595, plain, (![V_491, V_492, V_2, U_71]: (p(enc(V_491, V_492)) | ~p(enc(enc(i(V_2), U_71), V_492)) | ~p(enc(tmk, V_491)) | ~p(enc(zcmk, V_2)) | ~p(U_71)))). % 30.71/18.90 tff(c_37720, plain, (![V_4]: (~p(V_4) | ~p(enc(enc(i(zcmk), V_4), wk))))). % 30.71/18.90 tff(c_37644, plain, (![U_811]: (~p(enc(zcmk, U_811)) | ~p(enc(U_811, wk))))). % 30.71/18.90 tff(c_32378, plain, (![W_721, V_722, V_2, U_1]: (p(enc(enc(i(wk), W_721), V_722)) | ~p(W_721) | ~p(enc(V_2, V_722)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.90 tff(c_36913, plain, (![V_802, V_2, V_803]: (p(enc(V_802, V_2)) | ~p(enc(wk, V_802)) | ~p(V_803) | ~p(enc(enc(i(zcmk), V_803), V_2))))). % 30.71/18.90 tff(c_36327, plain, (![V_2, V_800, V_801]: (p(enc(V_2, enc(i(enc(i(zcmk), V_800)), V_801))) | ~p(enc(wk, V_2)) | ~p(V_800) | ~p(V_801)))). % 30.71/18.90 tff(c_36241, plain, (![W_796, V_798, V_4]: (p(enc(enc(i(wk), W_796), enc(i(enc(i(zcmk), V_798)), V_4))) | ~p(W_796) | ~p(V_798) | ~p(V_4)))). % 30.71/18.90 tff(c_36002, plain, (![W_787, V_788, V_4]: (p(enc(enc(i(wk), W_787), V_788)) | ~p(W_787) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_788))))). % 30.71/18.90 tff(c_34925, plain, (![W_778, U_5, V_780]: (p(enc(enc(i(wk), W_778), enc(U_5, V_780))) | ~p(W_778) | ~p(enc(zcmk, i(U_5))) | ~p(V_780)))). % 30.71/18.90 tff(c_35608, plain, (![V_781, U_5, V_783]: (p(enc(V_781, enc(U_5, V_783))) | ~p(enc(wk, V_781)) | ~p(enc(zcmk, i(U_5))) | ~p(V_783)))). % 30.71/18.90 tff(c_34910, plain, (![W_778, V_2, U_1]: (p(enc(enc(i(wk), W_778), V_2)) | ~p(W_778) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.90 tff(c_35594, plain, (![V_781, V_2, U_1]: (p(enc(V_781, V_2)) | ~p(enc(wk, V_781)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.90 tff(c_34907, plain, (![V_2, V_779, V_780]: (p(enc(V_2, enc(i(V_779), V_780))) | ~p(enc(wk, V_2)) | ~p(enc(zcmk, V_779)) | ~p(V_780)))). % 30.71/18.90 tff(c_34861, plain, (![W_371, V_773, V_774]: (p(enc(enc(i(wk), W_371), enc(i(V_773), V_774))) | ~p(W_371) | ~p(enc(zcmk, V_773)) | ~p(V_774)))). % 30.71/18.90 tff(c_34475, plain, (![V_772, U_5, V_774]: (p(enc(enc(i(tmk), V_772), enc(U_5, V_774))) | ~p(V_772) | ~p(enc(zcmk, i(U_5))) | ~p(V_774)))). % 30.71/18.90 tff(c_34374, plain, (![V_769, V_2, V_771]: (p(enc(enc(i(tmk), V_769), enc(i(V_2), V_771))) | ~p(V_769) | ~p(enc(zcmk, V_2)) | ~p(V_771)))). % 30.71/18.90 tff(c_30258, plain, (![V_693, V_695, V_4]: (p(enc(enc(i(tmk), V_693), enc(i(enc(i(zcmk), V_695)), V_4))) | ~p(V_693) | ~p(V_695) | ~p(V_4)))). % 30.71/18.90 tff(c_34089, plain, (![U_5, V_764, V_765]: (p(enc(enc(U_5, V_764), enc(i(tmk), V_765))) | ~p(V_765) | ~p(enc(zcmk, i(U_5))) | ~p(V_764)))). % 30.71/18.90 tff(c_33916, plain, (![V_2, V_761, V_762]: (p(enc(enc(i(V_2), V_761), enc(i(tmk), V_762))) | ~p(V_762) | ~p(enc(zcmk, V_2)) | ~p(V_761)))). % 30.71/18.90 tff(c_26923, plain, (![V_670, V_4, V_669]: (p(enc(enc(i(enc(i(zcmk), V_670)), V_4), enc(i(tmk), V_669))) | ~p(V_669) | ~p(V_670) | ~p(V_4)))). % 30.71/18.90 tff(c_33640, plain, (![U_5, V_755, V_756]: (p(enc(enc(U_5, V_755), enc(i(tc), V_756))) | ~p(V_756) | ~p(enc(zcmk, i(U_5))) | ~p(V_755)))). % 30.71/18.90 tff(c_33463, plain, (![V_2, V_752, V_753]: (p(enc(enc(i(V_2), V_752), enc(i(tc), V_753))) | ~p(V_753) | ~p(enc(zcmk, V_2)) | ~p(V_752)))). % 30.71/18.90 tff(c_27242, plain, (![V_676, V_4, V_675]: (p(enc(enc(i(enc(i(zcmk), V_676)), V_4), enc(i(tc), V_675))) | ~p(V_675) | ~p(V_676) | ~p(V_4)))). % 30.71/18.90 tff(c_33290, plain, (![V_745, U_5, V_747]: (p(V_745) | ~p(enc(tc, enc(U_5, V_745))) | ~p(V_747) | ~p(enc(enc(i(zcmk), V_747), i(U_5)))))). % 30.71/18.90 tff(c_32944, plain, (![V_738, V_2, V_739]: (p(V_738) | ~p(enc(tc, enc(i(V_2), V_738))) | ~p(V_739) | ~p(enc(enc(i(zcmk), V_739), V_2))))). % 30.71/18.90 tff(c_33005, plain, (![V_2, V_741]: (~p(enc(zcmk, V_2)) | ~p(V_741) | ~p(enc(enc(i(zcmk), V_741), V_2))))). % 30.71/18.90 tff(c_32912, plain, (![V_639, U_640]: (~p(enc(zcmk, enc(i(enc(i(zcmk), V_639)), U_640))) | ~p(V_639) | ~p(U_640)))). % 30.71/18.90 tff(c_25577, plain, (![V_4, V_639, U_640]: (p(V_4) | ~p(enc(tc, enc(i(enc(i(enc(i(zcmk), V_639)), U_640)), V_4))) | ~p(V_639) | ~p(U_640)))). % 30.71/18.90 tff(c_10280, plain, (![W_385, V_386, V_8, U_7]: (p(enc(enc(i(wk), W_385), V_386)) | ~p(W_385) | ~p(enc(enc(i(enc(i(zcmk), V_8)), U_7), V_386)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.90 tff(c_32620, plain, (![U_728, U_5, V_730]: (p(enc(enc(i(tmk), U_728), enc(U_5, V_730))) | ~p(enc(wk, i(U_5))) | ~p(V_730) | ~p(U_728)))). % 30.71/18.90 tff(c_32519, plain, (![U_725, V_2, V_727]: (p(enc(enc(i(tmk), U_725), enc(i(V_2), V_727))) | ~p(enc(wk, V_2)) | ~p(V_727) | ~p(U_725)))). % 30.71/18.90 tff(c_26124, plain, (![U_654, V_656, V_4]: (p(enc(enc(i(tmk), U_654), enc(i(enc(i(wk), V_656)), V_4))) | ~p(V_656) | ~p(V_4) | ~p(U_654)))). % 30.71/18.90 tff(c_10277, plain, (![W_385, V_386, V_2, U_71]: (p(enc(enc(i(wk), W_385), V_386)) | ~p(W_385) | ~p(enc(enc(i(V_2), U_71), V_386)) | ~p(enc(zcmk, V_2)) | ~p(U_71)))). % 30.71/18.90 tff(c_32039, plain, (![V_715, U_5, V_717]: (p(V_715) | ~p(enc(tmk, enc(U_5, V_715))) | ~p(V_717) | ~p(enc(enc(i(zcmk), V_717), i(U_5)))))). % 30.71/18.90 tff(c_31932, plain, (![V_712, V_2, V_713]: (p(V_712) | ~p(enc(tmk, enc(i(V_2), V_712))) | ~p(V_713) | ~p(enc(enc(i(zcmk), V_713), V_2))))). % 30.71/18.90 tff(c_26724, plain, (![V_4, V_662, U_663]: (p(V_4) | ~p(enc(tmk, enc(i(enc(i(enc(i(zcmk), V_662)), U_663)), V_4))) | ~p(V_662) | ~p(U_663)))). % 30.71/18.90 tff(c_31792, plain, (![U_706, U_5, V_708]: (p(enc(enc(i(tmk), U_706), enc(U_5, V_708))) | ~p(enc(tmk, i(U_5))) | ~p(V_708) | ~p(U_706)))). % 30.71/18.90 tff(c_31690, plain, (![U_703, V_2, V_705]: (p(enc(enc(i(tmk), U_703), enc(i(V_2), V_705))) | ~p(enc(tmk, V_2)) | ~p(V_705) | ~p(U_703)))). % 30.71/18.90 tff(c_26614, plain, (![U_659, V_661, V_4]: (p(enc(enc(i(tmk), U_659), enc(i(enc(i(tmk), V_661)), V_4))) | ~p(V_661) | ~p(V_4) | ~p(U_659)))). % 30.71/18.90 tff(c_30941, plain, (![V_2, V_700]: (p(enc(V_2, enc(i(pp), V_700))) | ~p(enc(wk, V_2)) | ~p(V_700)))). % 30.71/18.90 tff(c_30905, plain, (![W_371, V_698]: (p(enc(enc(i(wk), W_371), enc(i(pp), V_698))) | ~p(W_371) | ~p(V_698)))). % 30.71/18.90 tff(c_30584, plain, (![U_659, V_4]: (p(enc(enc(i(tmk), U_659), enc(i(pp), V_4))) | ~p(U_659) | ~p(V_4)))). % 30.71/18.90 tff(c_28766, plain, (![V_4, V_684, V_685]: (p(enc(enc(i(tmk), V_4), V_684)) | ~p(V_4) | ~p(V_685) | ~p(enc(enc(i(zcmk), V_685), V_684))))). % 30.71/18.90 tff(c_29422, plain, (![V_2, V_690]: (p(enc(V_2, enc(i(w), V_690))) | ~p(enc(wk, V_2)) | ~p(V_690)))). % 30.71/18.90 tff(c_29386, plain, (![W_371, V_688]: (p(enc(enc(i(wk), W_371), enc(i(w), V_688))) | ~p(W_371) | ~p(V_688)))). % 30.71/18.90 tff(c_29068, plain, (![U_671, V_4]: (p(enc(enc(i(tmk), U_671), enc(i(w), V_4))) | ~p(U_671) | ~p(V_4)))). % 30.71/18.90 tff(c_28508, plain, (![V_680, V_2, V_681]: (p(enc(V_680, V_2)) | ~p(enc(tmk, V_680)) | ~p(V_681) | ~p(enc(enc(i(zcmk), V_681), V_2))))). % 30.71/18.90 tff(c_16923, plain, (![V_497, V_8, U_7]: (p(enc(V_497, enc(i(enc(i(zcmk), V_8)), U_7))) | ~p(enc(tmk, V_497)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.90 tff(c_10021, plain, (![V_380, V_98, U_99]: (p(enc(V_380, enc(i(enc(i(tmk), V_98)), U_99))) | ~p(enc(tmk, V_380)) | ~p(V_98) | ~p(U_99)))). % 30.71/18.90 tff(c_25650, plain, (![V_642, V_4, V_644]: (p(enc(V_642, enc(i(tc), V_4))) | ~p(V_4) | ~p(V_644) | ~p(enc(enc(i(zcmk), V_644), V_642))))). % 30.71/18.90 tff(c_22990, plain, (![U_580, V_581, U_13]: (p(enc(enc(i(tmk), U_580), V_581)) | ~p(enc(enc(i(tmk), U_13), V_581)) | ~p(U_580) | ~p(U_13)))). % 30.71/18.90 tff(c_26800, plain, (![V_665, V_4, V_667]: (p(enc(V_665, enc(i(tmk), V_4))) | ~p(V_4) | ~p(V_667) | ~p(enc(enc(i(zcmk), V_667), V_665))))). % 30.71/18.90 tff(c_26712, plain, (![V_2, V_664, V_662]: (p(enc(V_2, V_664)) | ~p(enc(tmk, V_664)) | ~p(V_662) | ~p(enc(enc(i(zcmk), V_662), V_2))))). % 30.71/18.90 tff(c_1612, plain, (![V_8, U_7, V_121]: (p(enc(enc(i(enc(i(zcmk), V_8)), U_7), V_121)) | ~p(enc(tmk, V_121)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.91 tff(c_26426, plain, (![U_654, U_34]: (p(enc(enc(i(tmk), U_654), enc(i(lp), U_34))) | ~p(U_654) | ~p(U_34)))). % 30.71/18.91 tff(c_9505, plain, (![U_13, V_357, V_358]: (p(enc(enc(i(tmk), U_13), V_357)) | ~p(V_358) | ~p(enc(enc(i(wk), V_358), V_357)) | ~p(U_13)))). % 30.71/18.91 tff(c_9809, plain, (![W_371, V_372, U_13]: (p(enc(enc(i(wk), W_371), V_372)) | ~p(W_371) | ~p(enc(enc(i(tmk), U_13), V_372)) | ~p(U_13)))). % 30.71/18.91 tff(c_25067, plain, (![V_621, U_5, U_623]: (p(V_621) | ~p(enc(tmk, enc(i(enc(U_5, U_623)), V_621))) | ~p(enc(zcmk, i(U_5))) | ~p(U_623)))). % 30.71/18.91 tff(c_25331, plain, (![V_630, U_5, U_632]: (p(V_630) | ~p(enc(tc, enc(i(enc(U_5, U_632)), V_630))) | ~p(enc(zcmk, i(U_5))) | ~p(U_632)))). % 30.71/18.91 tff(c_25565, plain, (![V_2, V_641, V_639]: (p(enc(V_2, V_641)) | ~p(enc(tc, V_641)) | ~p(V_639) | ~p(enc(enc(i(zcmk), V_639), V_2))))). % 30.71/18.91 tff(c_1279, plain, (![V_8, U_7, V_107]: (p(enc(enc(i(enc(i(zcmk), V_8)), U_7), V_107)) | ~p(enc(tc, V_107)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.91 tff(c_25407, plain, (![V_633, U_5, U_635]: (p(V_633) | ~p(enc(tc, enc(U_5, V_633))) | ~p(enc(zcmk, U_635)) | ~p(enc(U_635, i(U_5)))))). % 30.71/18.91 tff(c_25316, plain, (![V_630, V_2, U_1]: (p(V_630) | ~p(enc(tc, enc(i(V_2), V_630))) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.91 tff(c_22387, plain, (![V_4, V_565, U_566]: (p(V_4) | ~p(enc(tc, enc(i(enc(i(V_565), U_566)), V_4))) | ~p(enc(zcmk, V_565)) | ~p(U_566)))). % 30.71/18.91 tff(c_25149, plain, (![V_624, U_5, U_626]: (p(V_624) | ~p(enc(tmk, enc(U_5, V_624))) | ~p(enc(zcmk, U_626)) | ~p(enc(U_626, i(U_5)))))). % 30.71/18.91 tff(c_25052, plain, (![V_621, V_2, U_1]: (p(V_621) | ~p(enc(tmk, enc(i(V_2), V_621))) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.91 tff(c_22794, plain, (![V_4, V_574, U_575]: (p(V_4) | ~p(enc(tmk, enc(i(enc(i(V_574), U_575)), V_4))) | ~p(enc(zcmk, V_574)) | ~p(U_575)))). % 30.71/18.91 tff(c_24642, plain, (![V_4, U_616]: (~p(V_4) | ~p(enc(zcmk, U_616)) | ~p(enc(U_616, enc(i(zcmk), V_4)))))). % 30.71/18.91 tff(c_24565, plain, (![U_5, U_614]: (~p(enc(zcmk, enc(U_5, U_614))) | ~p(enc(zcmk, i(U_5))) | ~p(U_614)))). % 30.71/18.91 tff(c_24554, plain, (![V_2, U_1]: (~p(enc(zcmk, V_2)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.91 tff(c_24479, plain, (![V_565, U_566]: (~p(enc(zcmk, enc(i(V_565), U_566))) | ~p(enc(zcmk, V_565)) | ~p(U_566)))). % 30.71/18.91 tff(c_24361, plain, (![V_4, V_602, U_603]: (p(enc(enc(i(tmk), V_4), V_602)) | ~p(V_4) | ~p(enc(zcmk, U_603)) | ~p(enc(U_603, V_602))))). % 30.71/18.91 tff(c_22086, plain, (![V_562, U_5, V_564]: (p(enc(V_562, enc(U_5, V_564))) | ~p(enc(wk, i(U_5))) | ~p(V_564) | ~p(enc(tmk, V_562))))). % 30.71/18.91 tff(c_24120, plain, (![V_598, U_5, U_600]: (p(enc(V_598, enc(U_5, U_600))) | ~p(enc(tmk, V_598)) | ~p(enc(zcmk, i(U_5))) | ~p(U_600)))). % 30.71/18.91 tff(c_24106, plain, (![V_598, V_2, U_1]: (p(enc(V_598, V_2)) | ~p(enc(tmk, V_598)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.91 tff(c_16936, plain, (![V_497, V_133, U_134]: (p(enc(V_497, enc(i(V_133), U_134))) | ~p(enc(tmk, V_497)) | ~p(enc(zcmk, V_133)) | ~p(U_134)))). % 30.71/18.91 tff(c_16667, plain, (![V_494, V_495, U_13]: (p(enc(V_494, V_495)) | ~p(enc(enc(i(tmk), U_13), V_495)) | ~p(enc(tmk, V_494)) | ~p(U_13)))). % 30.71/18.91 tff(c_22481, plain, (![V_568, V_4, U_570]: (p(enc(V_568, enc(i(tc), V_4))) | ~p(V_4) | ~p(enc(zcmk, U_570)) | ~p(enc(U_570, V_568))))). % 30.71/18.91 tff(c_16474, plain, (![U_13, V_487, U_488]: (p(enc(enc(i(tmk), U_13), V_487)) | ~p(enc(tmk, U_488)) | ~p(enc(U_488, V_487)) | ~p(U_13)))). % 30.71/18.91 tff(c_22889, plain, (![V_577, V_4, U_579]: (p(enc(V_577, enc(i(tmk), V_4))) | ~p(V_4) | ~p(enc(zcmk, U_579)) | ~p(enc(U_579, V_577))))). % 30.71/18.91 tff(c_22797, plain, (![U_5, U_575, V_576]: (p(enc(enc(U_5, U_575), V_576)) | ~p(enc(tmk, V_576)) | ~p(enc(zcmk, i(U_5))) | ~p(U_575)))). % 30.71/18.91 tff(c_8545, plain, (![U_13, V_336, U_337]: (p(enc(enc(i(tmk), U_13), V_336)) | ~p(enc(wk, U_337)) | ~p(enc(U_337, V_336)) | ~p(U_13)))). % 30.71/18.91 tff(c_22786, plain, (![V_2, V_576, U_1]: (p(enc(V_2, V_576)) | ~p(enc(tmk, V_576)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.91 tff(c_1833, plain, (![V_133, U_134, V_2]: (p(enc(enc(i(V_133), U_134), V_2)) | ~p(enc(tmk, V_2)) | ~p(enc(zcmk, V_133)) | ~p(U_134)))). % 30.71/18.91 tff(c_22390, plain, (![U_5, U_566, V_567]: (p(enc(enc(U_5, U_566), V_567)) | ~p(enc(tc, V_567)) | ~p(enc(zcmk, i(U_5))) | ~p(U_566)))). % 30.71/18.91 tff(c_22379, plain, (![V_2, V_567, U_1]: (p(enc(V_2, V_567)) | ~p(enc(tc, V_567)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.91 tff(c_1837, plain, (![V_133, U_134, V_2]: (p(enc(enc(i(V_133), U_134), V_2)) | ~p(enc(tc, V_2)) | ~p(enc(zcmk, V_133)) | ~p(U_134)))). % 30.71/18.91 tff(c_21376, plain, (![V_559, V_2, V_561]: (p(enc(V_559, enc(i(V_2), V_561))) | ~p(enc(wk, V_2)) | ~p(V_561) | ~p(enc(tmk, V_559))))). % 30.71/18.91 tff(c_17542, plain, (![V_513, V_515, V_4]: (p(enc(V_513, enc(i(enc(i(wk), V_515)), V_4))) | ~p(V_515) | ~p(V_4) | ~p(enc(tmk, V_513))))). % 30.71/18.91 tff(c_16856, plain, (![V_497, U_3, V_4]: (p(enc(V_497, enc(i(U_3), V_4))) | ~p(V_4) | ~p(enc(tmk, V_497)) | ~p(enc(tmk, U_3))))). % 30.71/18.91 tff(c_16854, plain, (![V_497, U_1, V_2]: (p(enc(V_497, enc(U_1, V_2))) | ~p(V_2) | ~p(enc(tmk, V_497)) | ~p(enc(tmk, i(U_1)))))). % 30.71/18.91 tff(c_3226, plain, (![W_192, U_5, U_194]: (p(enc(enc(i(wk), W_192), enc(U_5, U_194))) | ~p(W_192) | ~p(enc(tmk, i(U_5))) | ~p(U_194)))). % 30.71/18.91 tff(c_19987, plain, (![U_22]: (~p(enc(wk, i(enc(i(tc), U_22)))) | ~p(U_22)))). % 30.71/18.91 tff(c_18024, plain, (![U_349, V_4]: (~p(enc(i(enc(i(tmk), U_349)), V_4)) | ~p(V_4) | ~p(U_349)))). % 30.71/18.91 tff(c_18053, plain, (![V_89, U_90]: (~p(enc(i(enc(i(wk), V_89)), U_90)) | ~p(V_89) | ~p(U_90)))). % 30.71/18.91 tff(c_18223, plain, (![V_522, V_4]: (~p(V_522) | ~p(V_4) | ~p(enc(enc(i(wk), V_4), V_522))))). % 30.71/18.91 tff(c_18240, plain, (![V_522, U_13]: (~p(V_522) | ~p(enc(enc(i(tmk), U_13), V_522)) | ~p(U_13)))). % 30.71/18.91 tff(c_19358, plain, (![U_25]: (~p(enc(wk, enc(i(tc), U_25))) | ~p(U_25)))). % 30.71/18.91 tff(c_19349, plain, (![U_37]: (~p(enc(tmk, i(U_37))) | ~p(U_37)))). % 30.71/18.91 tff(c_18033, plain, (![U_1, V_2]: (~p(enc(U_1, V_2)) | ~p(V_2) | ~p(enc(tmk, i(U_1)))))). % 30.71/18.91 tff(c_4944, plain, (![W_241, U_5, U_243]: (p(enc(enc(i(wk), W_241), enc(U_5, U_243))) | ~p(W_241) | ~p(enc(wk, i(U_5))) | ~p(U_243)))). % 30.71/18.91 tff(c_18032, plain, (![U_3, V_4]: (~p(enc(i(U_3), V_4)) | ~p(V_4) | ~p(enc(tmk, U_3))))). % 30.71/18.91 tff(c_18239, plain, (![V_522, V_2]: (~p(V_522) | ~p(enc(V_2, V_522)) | ~p(enc(tmk, V_2))))). % 30.71/18.91 tff(c_18543, plain, (![U_37]: (~p(enc(wk, i(U_37))) | ~p(U_37)))). % 30.71/18.91 tff(c_18151, plain, (![U_5, U_521]: (~p(enc(U_5, U_521)) | ~p(enc(wk, i(U_5))) | ~p(U_521)))). % 30.71/18.91 tff(c_18144, plain, (![V_2, U_1]: (~p(V_2) | ~p(enc(wk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.91 tff(c_18049, plain, (![V_242, U_243]: (~p(enc(i(V_242), U_243)) | ~p(enc(wk, V_242)) | ~p(U_243)))). % 30.71/18.91 tff(c_17878, plain, (![V_2]: (~p(V_2) | ~p(enc(w, V_2))))). % 30.71/18.91 tff(c_17684, plain, (![V_4]: (~p(enc(i(w), V_4)) | ~p(V_4)))). % 30.71/18.91 tff(c_17681, plain, (![V_4]: (~p(enc(i(pp), V_4)) | ~p(V_4)))). % 30.71/18.91 tff(c_17434, plain, (![V_392]: (~p(V_392) | ~p(enc(pp, V_392))))). % 30.71/18.91 tff(c_16650, plain, (![V_494, V_495, V_4]: (p(enc(V_494, V_495)) | ~p(V_4) | ~p(enc(enc(i(wk), V_4), V_495)) | ~p(enc(tmk, V_494))))). % 30.71/18.91 tff(c_17425, plain, (~p(enc(wk, i(lp))))). % 30.71/18.91 tff(c_17416, plain, (~p(enc(wk, lp)))). % 30.71/18.91 tff(c_17411, plain, (~p(enc(tmk, i(lp))))). % 30.71/18.91 tff(c_17406, plain, (~p(enc(tmk, lp)))). % 30.71/18.91 tff(c_16260, plain, (![V_483, U_5, U_485]: (p(enc(V_483, enc(U_5, U_485))) | ~p(enc(wk, V_483)) | ~p(enc(tmk, i(U_5))) | ~p(U_485)))). % 30.71/18.91 tff(c_17296, plain, (![V_2]: (~p(V_2) | ~p(enc(lp, V_2))))). % 30.71/18.92 tff(c_17223, plain, (![U_141]: (~p(enc(i(lp), U_141)) | ~p(U_141)))). % 30.71/18.92 tff(c_6434, plain, (![V_292, U_5, U_294]: (p(enc(V_292, enc(U_5, U_294))) | ~p(enc(wk, V_292)) | ~p(enc(wk, i(U_5))) | ~p(U_294)))). % 30.71/18.92 tff(c_17203, plain, (~p(enc(wk, i(tc))))). % 30.71/18.92 tff(c_17198, plain, (~p(enc(tmk, i(tc))))). % 30.71/18.92 tff(c_17095, plain, (![V_2]: (~p(V_2) | ~p(enc(tc, V_2))))). % 30.71/18.92 tff(c_17022, plain, (![U_317]: (~p(enc(i(tc), U_317)) | ~p(U_317)))). % 30.71/18.92 tff(c_17012, plain, (![U_5]: (~p(enc(zcmk, i(U_5))) | ~p(enc(tmk, U_5))))). % 30.71/18.92 tff(c_17005, plain, (![V_133]: (~p(enc(zcmk, V_133)) | ~p(enc(tmk, i(V_133)))))). % 30.71/18.92 tff(c_16990, plain, (![U_25]: (~p(enc(tmk, i(enc(i(tc), U_25)))) | ~p(U_25)))). % 30.71/18.92 tff(c_16666, plain, (![V_494, V_495, V_2]: (p(enc(V_494, V_495)) | ~p(enc(V_2, V_495)) | ~p(enc(tmk, V_494)) | ~p(enc(tmk, V_2))))). % 30.71/18.92 tff(c_8544, plain, (![V_2, V_336, U_337]: (p(enc(V_2, V_336)) | ~p(enc(wk, U_337)) | ~p(enc(U_337, V_336)) | ~p(enc(tmk, V_2))))). % 30.71/18.92 tff(c_16517, plain, (![V_177]: (~p(enc(tc, i(enc(i(zcmk), V_177)))) | ~p(V_177)))). % 30.71/18.92 tff(c_16477, plain, (![U_22]: (~p(enc(tmk, enc(i(tc), U_22))) | ~p(U_22)))). % 30.71/18.92 tff(c_16246, plain, (![V_483, V_2, U_1]: (p(enc(V_483, V_2)) | ~p(enc(wk, V_483)) | ~p(enc(tmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.92 tff(c_3231, plain, (![V_4, V_193, U_194]: (p(enc(V_4, enc(i(V_193), U_194))) | ~p(enc(wk, V_4)) | ~p(enc(tmk, V_193)) | ~p(U_194)))). % 30.71/18.92 tff(c_15666, plain, (![V_2, V_479]: (~p(enc(tc, i(V_2))) | ~p(V_479) | ~p(enc(enc(i(zcmk), V_479), V_2))))). % 30.71/18.92 tff(c_15648, plain, (![V_477, U_478]: (~p(enc(tc, i(enc(i(enc(i(zcmk), V_477)), U_478)))) | ~p(V_477) | ~p(U_478)))). % 30.71/18.92 tff(c_10222, plain, (![V_8, U_7]: (p(enc(enc(i(enc(i(zcmk), V_8)), U_7), pp)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.92 tff(c_10164, plain, (![V_8, U_7]: (p(enc(enc(i(enc(i(zcmk), V_8)), U_7), k)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.92 tff(c_10086, plain, (![V_8, U_7]: (p(enc(enc(i(enc(i(zcmk), V_8)), U_7), t1)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.92 tff(c_12558, plain, (![V_4, U_412]: (p(V_4) | ~p(enc(pp, enc(i(enc(i(tmk), U_412)), V_4))) | ~p(U_412)))). % 30.71/18.92 tff(c_8741, plain, (![V_8, U_7]: (p(enc(w, enc(i(enc(i(zcmk), V_8)), U_7))) | ~p(V_8) | ~p(U_7)))). % 30.71/18.92 tff(c_9319, plain, (![U_349, V_4]: (p(enc(w, enc(i(enc(i(tmk), U_349)), V_4))) | ~p(V_4) | ~p(U_349)))). % 30.71/18.92 tff(c_15244, plain, (![V_463, V_464]: (p(V_463) | ~p(enc(tmk, V_464)) | ~p(enc(pp, enc(i(V_464), V_463)))))). % 30.71/18.92 tff(c_15099, plain, (![V_461, V_2]: (p(V_461) | ~p(enc(w, enc(i(V_2), V_461))) | ~p(enc(tmk, V_2))))). % 30.71/18.92 tff(c_12510, plain, (![V_4, U_410]: (p(V_4) | ~p(enc(w, enc(i(enc(i(tmk), U_410)), V_4))) | ~p(U_410)))). % 30.71/18.92 tff(c_14897, plain, (![V_457, U_458]: (p(V_457) | ~p(enc(w, enc(U_458, V_457))) | ~p(enc(tmk, i(U_458)))))). % 30.71/18.92 tff(c_14842, plain, (![V_455, U_5]: (p(V_455) | ~p(enc(wk, i(U_5))) | ~p(enc(w, enc(U_5, V_455)))))). % 30.71/18.92 tff(c_14704, plain, (![V_453, V_2]: (p(V_453) | ~p(enc(wk, V_2)) | ~p(enc(w, enc(i(V_2), V_453)))))). % 30.71/18.92 tff(c_9848, plain, (![V_4, W_374]: (p(V_4) | ~p(W_374) | ~p(enc(w, enc(i(enc(i(wk), W_374)), V_4)))))). % 30.71/18.92 tff(c_14560, plain, (![V_449, U_450]: (p(V_449) | ~p(enc(pp, enc(U_450, V_449))) | ~p(enc(tmk, i(U_450)))))). % 30.71/18.92 tff(c_14521, plain, (![V_447, U_5]: (p(V_447) | ~p(enc(wk, i(U_5))) | ~p(enc(pp, enc(U_5, V_447)))))). % 30.71/18.92 tff(c_14424, plain, (![V_445, V_2]: (p(V_445) | ~p(enc(wk, V_2)) | ~p(enc(pp, enc(i(V_2), V_445)))))). % 30.71/18.92 tff(c_10433, plain, (![V_4, W_391]: (p(V_4) | ~p(W_391) | ~p(enc(pp, enc(i(enc(i(wk), W_391)), V_4)))))). % 30.71/18.92 tff(c_13766, plain, (![V_431, V_4]: (p(enc(V_431, k)) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_431))))). % 30.71/18.92 tff(c_13925, plain, (![V_435, V_4]: (p(enc(V_435, pp)) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_435))))). % 30.71/18.92 tff(c_13691, plain, (![U_5, U_430]: (p(enc(enc(U_5, U_430), k)) | ~p(enc(zcmk, i(U_5))) | ~p(U_430)))). % 30.71/18.92 tff(c_13851, plain, (![U_5, U_434]: (p(enc(enc(U_5, U_434), pp)) | ~p(enc(zcmk, i(U_5))) | ~p(U_434)))). % 30.71/18.92 tff(c_13844, plain, (![V_2, U_1]: (p(enc(V_2, pp)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.92 tff(c_10219, plain, (![V_2, U_71]: (p(enc(enc(i(V_2), U_71), pp)) | ~p(enc(zcmk, V_2)) | ~p(U_71)))). % 30.71/18.92 tff(c_13684, plain, (![V_2, U_1]: (p(enc(V_2, k)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.92 tff(c_10161, plain, (![V_2, U_71]: (p(enc(enc(i(V_2), U_71), k)) | ~p(enc(zcmk, V_2)) | ~p(U_71)))). % 30.71/18.92 tff(c_13112, plain, (![V_418, V_4]: (p(enc(V_418, t1)) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_418))))). % 30.71/18.92 tff(c_13042, plain, (![U_5, U_417]: (p(enc(enc(U_5, U_417), t1)) | ~p(enc(zcmk, i(U_5))) | ~p(U_417)))). % 30.71/18.92 tff(c_13321, plain, (![V_415]: (p(enc(w, enc(i(pp), V_415))) | ~p(V_415)))). % 30.71/18.92 tff(c_4066, plain, (![V_218, V_4, V_219]: (p(enc(V_218, V_4)) | ~p(enc(wk, V_218)) | ~p(V_219) | ~p(enc(enc(i(tmk), V_219), V_4))))). % 30.71/18.92 tff(c_13035, plain, (![V_2, U_1]: (p(enc(V_2, t1)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.92 tff(c_10083, plain, (![V_2, U_71]: (p(enc(enc(i(V_2), U_71), t1)) | ~p(enc(zcmk, V_2)) | ~p(U_71)))). % 30.71/18.92 tff(c_12445, plain, (![V_408, V_4]: (p(enc(V_408, enc(i(pp), V_4))) | ~p(V_4) | ~p(enc(tmk, V_408))))). % 30.71/18.92 tff(c_11457, plain, (![U_13, V_401]: (p(enc(enc(i(tmk), U_13), V_401)) | ~p(enc(pp, V_401)) | ~p(U_13)))). % 30.71/18.92 tff(c_9913, plain, (![U_13, V_377]: (p(enc(enc(i(tmk), U_13), V_377)) | ~p(enc(w, V_377)) | ~p(U_13)))). % 30.71/18.92 tff(c_11456, plain, (![V_2, V_401]: (p(enc(V_2, V_401)) | ~p(enc(pp, V_401)) | ~p(enc(tmk, V_2))))). % 30.71/18.92 tff(c_12310, plain, (![V_2]: (p(enc(V_2, k)) | ~p(enc(wk, V_2))))). % 30.71/18.92 tff(c_11877, plain, (![W_97]: (p(enc(enc(i(wk), W_97), k)) | ~p(W_97)))). % 30.71/18.92 tff(c_9991, plain, (![V_380, V_4]: (p(enc(V_380, enc(i(w), V_4))) | ~p(V_4) | ~p(enc(tmk, V_380))))). % 30.71/18.92 tff(c_11640, plain, (![V_2]: (p(enc(V_2, pp)) | ~p(enc(wk, V_2))))). % 30.71/18.92 tff(c_11619, plain, (![W_97]: (p(enc(enc(i(wk), W_97), pp)) | ~p(W_97)))). % 30.71/18.92 tff(c_10425, plain, (![V_2, V_392]: (p(enc(V_2, V_392)) | ~p(enc(wk, V_2)) | ~p(enc(pp, V_392))))). % 30.71/18.92 tff(c_11327, plain, (![V_2]: (p(enc(V_2, t1)) | ~p(enc(wk, V_2))))). % 30.71/18.92 tff(c_11306, plain, (![W_97]: (p(enc(enc(i(wk), W_97), t1)) | ~p(W_97)))). % 30.71/18.92 tff(c_10624, plain, (![V_4]: (p(V_4) | ~p(enc(pp, enc(i(w), V_4)))))). % 30.71/18.92 tff(c_10598, plain, (![V_392]: (p(enc(w, V_392)) | ~p(enc(pp, V_392))))). % 30.71/18.92 tff(c_10282, plain, (![W_385, V_386]: (p(enc(enc(i(wk), W_385), V_386)) | ~p(W_385) | ~p(enc(pp, V_386))))). % 30.71/18.92 tff(c_10150, plain, (![V_4]: (p(enc(enc(i(tmk), V_4), k)) | ~p(V_4)))). % 30.71/18.92 tff(c_10208, plain, (![V_4]: (p(enc(enc(i(tmk), V_4), pp)) | ~p(V_4)))). % 30.71/18.92 tff(c_10072, plain, (![V_4]: (p(enc(enc(i(tmk), V_4), t1)) | ~p(V_4)))). % 30.71/18.92 tff(c_3232, plain, (![W_192, V_4, V_193]: (p(enc(enc(i(wk), W_192), V_4)) | ~p(W_192) | ~p(enc(tmk, V_193)) | ~p(enc(V_193, V_4))))). % 30.71/18.92 tff(c_10003, plain, (![V_380]: (p(enc(V_380, pp)) | ~p(enc(tmk, V_380))))). % 30.71/18.92 tff(c_10002, plain, (![V_380]: (p(enc(V_380, k)) | ~p(enc(tmk, V_380))))). % 30.71/18.93 tff(c_10088, plain, (p(enc(pp, t1)))). % 30.71/18.93 tff(c_10031, plain, (![V_380]: (p(enc(V_380, t1)) | ~p(enc(tmk, V_380))))). % 30.71/18.93 tff(c_9912, plain, (![V_2, V_377]: (p(enc(V_2, V_377)) | ~p(enc(w, V_377)) | ~p(enc(tmk, V_2))))). % 30.71/18.93 tff(c_9745, plain, (![U_5, V_370]: (p(enc(w, enc(U_5, V_370))) | ~p(enc(wk, i(U_5))) | ~p(V_370)))). % 30.71/18.93 tff(c_9840, plain, (![V_2, V_375]: (p(enc(V_2, V_375)) | ~p(enc(wk, V_2)) | ~p(enc(w, V_375))))). % 30.71/18.93 tff(c_9811, plain, (![W_371, V_372]: (p(enc(enc(i(wk), W_371), V_372)) | ~p(W_371) | ~p(enc(w, V_372))))). % 30.71/18.93 tff(c_4952, plain, (![W_241, V_4, V_242]: (p(enc(enc(i(wk), W_241), V_4)) | ~p(W_241) | ~p(enc(wk, V_242)) | ~p(enc(V_242, V_4))))). % 30.71/18.93 tff(c_9696, plain, (![V_2, V_368]: (p(enc(w, enc(i(V_2), V_368))) | ~p(enc(wk, V_2)) | ~p(V_368)))). % 30.71/18.93 tff(c_9042, plain, (![V_346, V_4]: (p(enc(w, enc(i(enc(i(wk), V_346)), V_4))) | ~p(V_346) | ~p(V_4)))). % 30.71/18.93 tff(c_9581, plain, (![V_361, V_4]: (p(enc(w, V_361)) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_361))))). % 30.71/18.93 tff(c_9537, plain, (![U_5, U_360]: (p(enc(w, enc(U_5, U_360))) | ~p(enc(zcmk, i(U_5))) | ~p(U_360)))). % 30.71/18.93 tff(c_9526, plain, (![V_2, U_1]: (p(enc(w, V_2)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.93 tff(c_8758, plain, (![V_133, U_134]: (p(enc(w, enc(i(V_133), U_134))) | ~p(enc(zcmk, V_133)) | ~p(U_134)))). % 30.71/18.93 tff(c_4294, plain, (![V_223, V_2, V_224]: (p(enc(V_223, V_2)) | ~p(enc(wk, V_223)) | ~p(V_224) | ~p(enc(enc(i(wk), V_224), V_2))))). % 30.71/18.93 tff(c_8717, plain, (![U_3, V_4]: (p(enc(w, enc(i(U_3), V_4))) | ~p(V_4) | ~p(enc(tmk, U_3))))). % 30.71/18.93 tff(c_8715, plain, (![U_1, V_2]: (p(enc(w, enc(U_1, V_2))) | ~p(V_2) | ~p(enc(tmk, i(U_1)))))). % 30.71/18.93 tff(c_8602, plain, (![V_338, U_13]: (p(enc(w, V_338)) | ~p(enc(enc(i(tmk), U_13), V_338)) | ~p(U_13)))). % 30.71/18.93 tff(c_9210, plain, (![U_34]: (p(enc(w, enc(i(lp), U_34))) | ~p(U_34)))). % 30.71/18.93 tff(c_8944, plain, (~p(enc(tmk, k)))). % 30.71/18.93 tff(c_8588, plain, (![V_338, V_4]: (p(enc(w, V_338)) | ~p(V_4) | ~p(enc(enc(i(wk), V_4), V_338))))). % 30.71/18.93 tff(c_8778, plain, (![V_4]: (p(enc(w, enc(i(tc), V_4))) | ~p(V_4)))). % 30.71/18.93 tff(c_8770, plain, (![V_4]: (p(enc(w, enc(i(tmk), V_4))) | ~p(V_4)))). % 30.71/18.93 tff(c_8782, plain, (p(enc(w, k)))). % 30.71/18.93 tff(c_8773, plain, (p(enc(w, pp)))). % 30.71/18.93 tff(c_8601, plain, (![V_338, V_2]: (p(enc(w, V_338)) | ~p(enc(V_2, V_338)) | ~p(enc(tmk, V_2))))). % 30.71/18.93 tff(c_8547, plain, (![V_336, U_337]: (p(enc(w, V_336)) | ~p(enc(wk, U_337)) | ~p(enc(U_337, V_336))))). % 30.71/18.93 tff(c_6420, plain, (![V_292, V_2, U_1]: (p(enc(V_292, V_2)) | ~p(enc(wk, V_292)) | ~p(enc(wk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.93 tff(c_8471, plain, (![V_177]: (~p(enc(tc, enc(i(zcmk), V_177))) | ~p(V_177)))). % 30.71/18.93 tff(c_8133, plain, (![V_2, U_331]: (p(enc(V_2, enc(i(tmk), U_331))) | ~p(enc(wk, V_2)) | ~p(U_331)))). % 30.71/18.93 tff(c_8032, plain, (![W_199, U_16]: (p(enc(enc(i(wk), W_199), enc(i(tmk), U_16))) | ~p(W_199) | ~p(U_16)))). % 30.71/18.93 tff(c_8092, plain, (![V_326, U_5]: (p(V_326) | ~p(enc(wk, i(U_5))) | ~p(enc(tmk, enc(U_5, V_326)))))). % 30.71/18.93 tff(c_7895, plain, (![V_324, V_2]: (p(V_324) | ~p(enc(wk, V_2)) | ~p(enc(tmk, enc(i(V_2), V_324)))))). % 30.71/18.93 tff(c_6650, plain, (![V_4, W_295]: (p(V_4) | ~p(W_295) | ~p(enc(tmk, enc(i(enc(i(wk), W_295)), V_4)))))). % 30.71/18.93 tff(c_7852, plain, (![V_320, U_5]: (p(V_320) | ~p(enc(wk, i(U_5))) | ~p(enc(tc, enc(U_5, V_320)))))). % 30.71/18.93 tff(c_7780, plain, (![V_318, V_2]: (p(V_318) | ~p(enc(wk, V_2)) | ~p(enc(tc, enc(i(V_2), V_318)))))). % 30.71/18.93 tff(c_6898, plain, (![V_4, W_301]: (p(V_4) | ~p(W_301) | ~p(enc(tc, enc(i(enc(i(wk), W_301)), V_4)))))). % 30.71/18.93 tff(c_7430, plain, (![V_2, U_315]: (p(enc(V_2, enc(i(tc), U_315))) | ~p(enc(wk, V_2)) | ~p(U_315)))). % 30.71/18.93 tff(c_7411, plain, (![W_199, U_19]: (p(enc(enc(i(wk), W_199), enc(i(tc), U_19))) | ~p(W_199) | ~p(U_19)))). % 30.71/18.93 tff(c_7267, plain, (![V_4]: (~p(V_4) | ~p(enc(wk, enc(i(zcmk), V_4)))))). % 30.71/18.93 tff(c_7219, plain, (![V_2]: (~p(enc(zcmk, V_2)) | ~p(enc(wk, V_2))))). % 30.71/18.93 tff(c_7207, plain, (![W_301]: (~p(enc(zcmk, enc(i(wk), W_301))) | ~p(W_301)))). % 30.71/18.93 tff(c_6978, plain, (![V_4]: (p(V_4) | ~p(enc(tc, enc(i(w), V_4)))))). % 30.71/18.93 tff(c_6956, plain, (![V_304]: (p(enc(w, V_304)) | ~p(enc(tc, V_304))))). % 30.71/18.93 tff(c_6890, plain, (![V_2, V_302]: (p(enc(V_2, V_302)) | ~p(enc(wk, V_2)) | ~p(enc(tc, V_302))))). % 30.71/18.93 tff(c_6763, plain, (![W_199, V_2]: (p(enc(enc(i(wk), W_199), V_2)) | ~p(W_199) | ~p(enc(tc, V_2))))). % 30.71/18.93 tff(c_6834, plain, (![V_4]: (p(V_4) | ~p(enc(tmk, enc(i(w), V_4)))))). % 30.71/18.93 tff(c_6812, plain, (![V_298]: (p(enc(w, V_298)) | ~p(enc(tmk, V_298))))). % 30.71/18.93 tff(c_6642, plain, (![V_2, V_296]: (p(enc(V_2, V_296)) | ~p(enc(wk, V_2)) | ~p(enc(tmk, V_296))))). % 30.71/18.93 tff(c_6618, plain, (![W_199, V_2]: (p(enc(enc(i(wk), W_199), V_2)) | ~p(W_199) | ~p(enc(tmk, V_2))))). % 30.71/18.93 tff(c_4926, plain, (![V_2, V_242, U_243]: (p(enc(V_2, enc(i(V_242), U_243))) | ~p(enc(wk, V_2)) | ~p(enc(wk, V_242)) | ~p(U_243)))). % 30.71/18.93 tff(c_4417, plain, (![U_226, U_227]: (~p(enc(tc, i(enc(U_226, U_227)))) | ~p(enc(zcmk, i(U_226))) | ~p(U_227)))). % 30.71/18.93 tff(c_6068, plain, (![V_2, V_286]: (~p(enc(tc, V_2)) | ~p(V_286) | ~p(enc(enc(i(zcmk), V_286), V_2))))). % 30.71/18.93 tff(c_5960, plain, (![V_278, U_279]: (~p(enc(tc, enc(i(enc(i(zcmk), V_278)), U_279))) | ~p(V_278) | ~p(U_279)))). % 30.71/18.93 tff(c_5986, plain, (![U_5, U_283]: (~p(enc(tc, U_5)) | ~p(enc(zcmk, U_283)) | ~p(enc(U_283, i(U_5)))))). % 30.71/18.93 tff(c_5971, plain, (![V_2, U_1]: (~p(enc(tc, i(V_2))) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.93 tff(c_3275, plain, (![V_195, U_196]: (~p(enc(tc, i(enc(i(V_195), U_196)))) | ~p(enc(zcmk, V_195)) | ~p(U_196)))). % 30.71/18.93 tff(c_1145, plain, (![V_8, U_7]: (p(enc(enc(i(enc(i(zcmk), V_8)), U_7), t2)) | ~p(V_8) | ~p(U_7)))). % 30.71/18.93 tff(c_5855, plain, (![V_274, V_2]: (p(V_274) | ~p(enc(lp, enc(i(V_2), V_274))) | ~p(enc(tmk, V_2))))). % 30.71/18.93 tff(c_2954, plain, (![V_4, U_184]: (p(V_4) | ~p(enc(lp, enc(i(enc(i(tmk), U_184)), V_4))) | ~p(U_184)))). % 30.71/18.93 tff(c_1640, plain, (![V_8, U_7]: (p(enc(pp, enc(i(enc(i(zcmk), V_8)), U_7))) | ~p(V_8) | ~p(U_7)))). % 30.71/18.93 tff(c_5761, plain, (![V_268, U_269]: (p(V_268) | ~p(enc(lp, enc(U_269, V_268))) | ~p(enc(tmk, i(U_269)))))). % 30.71/18.93 tff(c_5741, plain, (![V_266, U_5]: (p(V_266) | ~p(enc(wk, i(U_5))) | ~p(enc(lp, enc(U_5, V_266)))))). % 30.71/18.93 tff(c_5679, plain, (![V_264, V_2]: (p(V_264) | ~p(enc(wk, V_2)) | ~p(enc(lp, enc(i(V_2), V_264)))))). % 30.71/18.93 tff(c_1034, plain, (![V_4, V_91]: (p(V_4) | ~p(V_91) | ~p(enc(lp, enc(i(enc(i(wk), V_91)), V_4)))))). % 30.71/18.93 tff(c_5586, plain, (![V_260, U_5]: (p(V_260) | ~p(enc(tmk, i(U_5))) | ~p(enc(tmk, enc(U_5, V_260)))))). % 30.71/18.93 tff(c_5517, plain, (![V_258, V_2]: (p(V_258) | ~p(enc(tmk, V_2)) | ~p(enc(tmk, enc(i(V_2), V_258)))))). % 30.71/18.93 tff(c_1583, plain, (![V_4, V_118]: (p(V_4) | ~p(V_118) | ~p(enc(tmk, enc(i(enc(i(tmk), V_118)), V_4)))))). % 30.71/18.93 tff(c_5497, plain, (~p(enc(zcmk, i(zcmk))))). % 30.71/18.93 tff(c_5492, plain, (~p(enc(zcmk, i(tc))))). % 30.71/18.93 tff(c_2661, plain, (![U_5, U_171]: (p(enc(U_5, enc(i(tmk), U_171))) | ~p(enc(zcmk, i(U_5))) | ~p(U_171)))). % 30.71/18.93 tff(c_5194, plain, (~p(enc(zcmk, w)))). % 30.71/18.93 tff(c_5177, plain, (![V_250, U_5]: (p(V_250) | ~p(enc(tmk, i(U_5))) | ~p(enc(tc, enc(U_5, V_250)))))). % 30.71/18.93 tff(c_5119, plain, (![V_248, V_2]: (p(V_248) | ~p(enc(tmk, V_2)) | ~p(enc(tc, enc(i(V_2), V_248)))))). % 30.71/18.93 tff(c_1695, plain, (![V_4, V_124]: (p(V_4) | ~p(V_124) | ~p(enc(tc, enc(i(enc(i(tmk), V_124)), V_4)))))). % 30.71/18.93 tff(c_5103, plain, (~p(enc(zcmk, wk)))). % 30.71/18.93 tff(c_5060, plain, (![V_20]: (~p(enc(zcmk, enc(i(tmk), V_20))) | ~p(V_20)))). % 30.71/18.93 tff(c_2567, plain, (![V_165, V_4]: (~p(i(enc(i(enc(i(zcmk), V_165)), V_4))) | ~p(V_165) | ~p(V_4)))). % 30.71/18.93 tff(c_4898, plain, (![V_4]: (~p(V_4) | ~p(enc(tmk, enc(i(zcmk), V_4)))))). % 30.71/18.93 tff(c_988, plain, (![W_88, V_2, U_90]: (p(enc(enc(i(wk), W_88), enc(i(V_2), U_90))) | ~p(W_88) | ~p(enc(wk, V_2)) | ~p(U_90)))). % 30.71/18.93 tff(c_4865, plain, (![V_4]: (~p(enc(zcmk, V_4)) | ~p(enc(tmk, V_4))))). % 30.71/18.93 tff(c_4774, plain, (~p(enc(zcmk, pp)))). % 30.71/18.93 tff(c_4468, plain, (![U_5, U_229]: (~p(enc(tc, enc(U_5, U_229))) | ~p(enc(zcmk, i(U_5))) | ~p(U_229)))). % 30.71/18.93 tff(c_3308, plain, (![V_197, V_4]: (p(enc(V_197, t2)) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_197))))). % 30.71/18.93 tff(c_4536, plain, (![V_4]: (~p(V_4) | ~p(enc(enc(i(zcmk), V_4), k))))). % 30.71/18.93 tff(c_4511, plain, (![U_231]: (~p(enc(zcmk, U_231)) | ~p(enc(U_231, k))))). % 30.71/18.93 tff(c_4457, plain, (![V_2, U_1]: (~p(enc(tc, V_2)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.93 tff(c_3281, plain, (![V_195, U_196]: (~p(enc(tc, enc(i(V_195), U_196))) | ~p(enc(zcmk, V_195)) | ~p(U_196)))). % 30.71/18.93 tff(c_3268, plain, (![U_5, U_196]: (p(enc(enc(U_5, U_196), t2)) | ~p(enc(zcmk, i(U_5))) | ~p(U_196)))). % 30.71/18.93 tff(c_984, plain, (![V_2, V_89, U_90]: (p(enc(V_2, enc(i(enc(i(wk), V_89)), U_90))) | ~p(enc(wk, V_2)) | ~p(V_89) | ~p(U_90)))). % 30.71/18.94 tff(c_4122, plain, (~p(enc(wk, i(wk))))). % 30.71/18.94 tff(c_3004, plain, (![V_188, V_4]: (p(enc(pp, V_188)) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_188))))). % 30.71/18.94 tff(c_4067, plain, (~p(enc(tmk, i(wk))))). % 30.71/18.94 tff(c_1120, plain, (![V_4, V_98, U_99]: (p(enc(V_4, enc(i(enc(i(tmk), V_98)), U_99))) | ~p(enc(wk, V_4)) | ~p(V_98) | ~p(U_99)))). % 30.71/18.94 tff(c_3835, plain, (~p(enc(wk, wk)))). % 30.71/18.94 tff(c_3821, plain, (![U_5]: (~p(enc(tc, U_5)) | ~p(enc(wk, i(U_5)))))). % 30.71/18.94 tff(c_3808, plain, (![V_2]: (~p(enc(tc, i(V_2))) | ~p(enc(wk, V_2))))). % 30.71/18.94 tff(c_3473, plain, (![W_202]: (~p(enc(tc, i(enc(i(wk), W_202)))) | ~p(W_202)))). % 30.71/18.94 tff(c_3796, plain, (~p(enc(tmk, wk)))). % 30.71/18.94 tff(c_3746, plain, (![V_2]: (~p(enc(tc, V_2)) | ~p(enc(wk, V_2))))). % 30.71/18.94 tff(c_3476, plain, (![W_202]: (~p(enc(tc, enc(i(wk), W_202))) | ~p(W_202)))). % 30.71/18.94 tff(c_2983, plain, (![U_5, U_187]: (p(enc(pp, enc(U_5, U_187))) | ~p(enc(zcmk, i(U_5))) | ~p(U_187)))). % 30.71/18.94 tff(c_3676, plain, (![V_2]: (~p(enc(wk, V_2)) | ~p(V_2)))). % 30.71/18.94 tff(c_3543, plain, (![W_204]: (~p(W_204) | ~p(enc(i(wk), W_204))))). % 30.71/18.94 tff(c_992, plain, (![W_88, V_2, V_89]: (p(enc(enc(i(wk), W_88), V_2)) | ~p(W_88) | ~p(V_89) | ~p(enc(enc(i(wk), V_89), V_2))))). % 30.71/18.94 tff(c_3534, plain, (![V_2]: (~p(i(V_2)) | ~p(enc(wk, V_2))))). % 30.71/18.94 tff(c_3479, plain, (![W_202]: (~p(i(enc(i(wk), W_202))) | ~p(W_202)))). % 30.71/18.94 tff(c_3513, plain, (p(enc(w, t2)))). % 30.71/18.94 tff(c_3465, plain, (![V_2]: (p(enc(V_2, t2)) | ~p(enc(wk, V_2))))). % 30.71/18.94 tff(c_3451, plain, (![W_199]: (p(enc(enc(i(wk), W_199), t2)) | ~p(W_199)))). % 30.71/18.94 tff(c_3314, plain, (~p(enc(zcmk, zcmk)))). % 30.71/18.94 tff(c_3261, plain, (![V_2, U_1]: (p(enc(V_2, t2)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.94 tff(c_3285, plain, (~p(enc(zcmk, tc)))). % 30.71/18.94 tff(c_1838, plain, (![V_133, U_134]: (p(enc(enc(i(V_133), U_134), t2)) | ~p(enc(zcmk, V_133)) | ~p(U_134)))). % 30.71/18.94 tff(c_1100, plain, (![W_97, V_2, U_99]: (p(enc(enc(i(wk), W_97), enc(i(V_2), U_99))) | ~p(W_97) | ~p(enc(tmk, V_2)) | ~p(U_99)))). % 30.71/18.94 tff(c_1129, plain, (![V_100, V_4]: (p(enc(V_100, enc(i(lp), V_4))) | ~p(V_4) | ~p(enc(tmk, V_100))))). % 30.71/18.94 tff(c_3009, plain, (~p(enc(wk, tc)))). % 30.71/18.94 tff(c_2972, plain, (![V_2, U_1]: (p(enc(pp, V_2)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.94 tff(c_1832, plain, (![V_133, U_134]: (p(enc(pp, enc(i(V_133), U_134))) | ~p(enc(zcmk, V_133)) | ~p(U_134)))). % 30.71/18.94 tff(c_1053, plain, (![U_13, V_94]: (p(enc(enc(i(tmk), U_13), V_94)) | ~p(enc(lp, V_94)) | ~p(U_13)))). % 30.71/18.94 tff(c_2736, plain, (![U_5, V_174]: (p(enc(U_5, V_174)) | ~p(enc(zcmk, i(U_5))) | ~p(enc(tmk, V_174))))). % 30.71/18.94 tff(c_2880, plain, (![V_177]: (~p(enc(i(zcmk), V_177)) | ~p(V_177)))). % 30.71/18.94 tff(c_2871, plain, (~p(enc(wk, i(zcmk))))). % 30.71/18.94 tff(c_2848, plain, (~p(enc(tmk, i(zcmk))))). % 30.71/18.94 tff(c_2825, plain, (![V_2, V_177]: (p(V_2) | ~p(V_177) | ~p(enc(tmk, enc(enc(i(zcmk), V_177), V_2)))))). % 30.71/18.94 tff(c_967, plain, (![V_86, V_4]: (p(enc(i(enc(i(zcmk), V_86)), V_4)) | ~p(V_86) | ~p(enc(tmk, V_4))))). % 30.71/18.94 tff(c_2729, plain, (![V_2, U_1]: (p(V_2) | ~p(enc(zcmk, U_1)) | ~p(enc(tmk, enc(U_1, V_2)))))). % 30.71/18.94 tff(c_2687, plain, (~p(enc(zcmk, k)))). % 30.71/18.94 tff(c_2650, plain, (![V_170, V_2]: (p(enc(i(V_170), V_2)) | ~p(enc(zcmk, V_170)) | ~p(enc(tmk, V_2))))). % 30.71/18.94 tff(c_2606, plain, (![U_5]: (~p(enc(zcmk, U_5)) | ~p(enc(tc, i(U_5)))))). % 30.71/18.94 tff(c_966, plain, (![V_4, U_87]: (p(enc(i(V_4), enc(i(tmk), U_87))) | ~p(enc(zcmk, V_4)) | ~p(U_87)))). % 30.71/18.94 tff(c_2593, plain, (![V_2]: (~p(enc(zcmk, i(V_2))) | ~p(enc(tc, V_2))))). % 30.71/18.94 tff(c_2585, plain, (![U_22]: (~p(enc(zcmk, i(enc(i(tc), U_22)))) | ~p(U_22)))). % 30.71/18.94 tff(c_2573, plain, (~p(enc(zcmk, i(pp))))). % 30.71/18.94 tff(c_1831, plain, (![U_5, U_134]: (p(enc(tmk, enc(U_5, U_134))) | ~p(enc(zcmk, i(U_5))) | ~p(U_134)))). % 30.71/18.94 tff(c_2508, plain, (![V_158, V_4]: (~p(i(V_158)) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_158))))). % 30.71/18.94 tff(c_2530, plain, (~p(enc(wk, i(tmk))))). % 30.71/18.94 tff(c_2522, plain, (![U_160, U_161]: (~p(enc(zcmk, i(U_160))) | ~p(U_161) | ~p(enc(U_160, U_161))))). % 30.71/18.94 tff(c_2490, plain, (![U_5, U_157]: (~p(i(enc(U_5, U_157))) | ~p(enc(zcmk, i(U_5))) | ~p(U_157)))). % 30.71/18.94 tff(c_2480, plain, (![V_2, U_1]: (~p(i(V_2)) | ~p(enc(zcmk, U_1)) | ~p(enc(U_1, V_2))))). % 30.71/18.94 tff(c_1836, plain, (![V_133, U_134]: (~p(i(enc(i(V_133), U_134))) | ~p(enc(zcmk, V_133)) | ~p(U_134)))). % 30.71/18.94 tff(c_2468, plain, (~p(enc(wk, i(k))))). % 30.71/18.94 tff(c_2411, plain, (~p(enc(wk, zcmk)))). % 30.71/18.94 tff(c_2364, plain, (![V_152, V_4]: (~p(enc(i(enc(i(zcmk), V_152)), V_4)) | ~p(V_152) | ~p(V_4)))). % 30.71/18.94 tff(c_2406, plain, (~p(enc(zcmk, i(w))))). % 30.71/18.94 tff(c_2370, plain, (![U_10]: (~p(enc(i(tmk), U_10)) | ~p(U_10)))). % 30.71/18.94 tff(c_2177, plain, (![V_145, V_4]: (~p(V_145) | ~p(V_4) | ~p(enc(enc(i(zcmk), V_4), V_145))))). % 30.71/18.94 tff(c_2316, plain, (![U_25]: (~p(enc(zcmk, enc(i(tc), U_25))) | ~p(U_25)))). % 30.71/18.94 tff(c_2307, plain, (~p(enc(wk, tmk)))). % 30.71/18.94 tff(c_2298, plain, (![U_37]: (~p(enc(zcmk, i(U_37))) | ~p(U_37)))). % 30.71/18.94 tff(c_2297, plain, (~p(t1))). % 30.71/18.94 tff(c_2292, plain, (~p(enc(zcmk, i(k))))). % 30.71/18.94 tff(c_2291, plain, (~p(t2))). % 30.71/18.94 tff(c_2290, plain, (~p(k))). % 30.71/18.94 tff(c_1875, plain, (![U_5, U_136]: (~p(enc(U_5, U_136)) | ~p(enc(zcmk, i(U_5))) | ~p(U_136)))). % 30.71/18.94 tff(c_2143, plain, (~p(enc(tmk, zcmk)))). % 30.71/18.94 tff(c_2116, plain, (![V_4]: (~p(enc(zcmk, V_4)) | ~p(enc(tc, V_4))))). % 30.71/18.94 tff(c_2111, plain, (~p(enc(tc, zcmk)))). % 30.71/18.94 tff(c_1948, plain, (![V_4]: (~p(enc(zcmk, V_4)) | ~p(V_4)))). % 30.71/18.94 tff(c_2081, plain, (~p(i(zcmk)))). % 30.71/18.94 tff(c_675, plain, (![V_2, U_75]: (p(enc(V_2, enc(i(lp), U_75))) | ~p(enc(wk, V_2)) | ~p(U_75)))). % 30.71/18.94 tff(c_1901, plain, (![V_4]: (~p(V_4) | ~p(i(enc(i(zcmk), V_4)))))). % 30.71/18.94 tff(c_1884, plain, (![V_135]: (~p(enc(zcmk, V_135)) | ~p(i(V_135))))). % 30.71/18.94 tff(c_1835, plain, (![V_133, U_134]: (~p(enc(i(V_133), U_134)) | ~p(enc(zcmk, V_133)) | ~p(U_134)))). % 30.71/18.94 tff(c_589, plain, (![V_2, U_71]: (p(enc(tmk, enc(i(V_2), U_71))) | ~p(enc(zcmk, V_2)) | ~p(U_71)))). % 30.71/18.94 tff(c_1783, plain, (~p(enc(tmk, i(tmk))))). % 30.71/18.94 tff(c_1782, plain, (~p(zcmk))). % 30.71/18.94 tff(c_1752, plain, (![V_129, V_2]: (p(enc(tmk, V_129)) | ~p(enc(zcmk, V_2)) | ~p(enc(V_2, V_129))))). % 30.71/18.94 tff(c_593, plain, (![V_2, V_70]: (p(enc(tmk, V_2)) | ~p(V_70) | ~p(enc(enc(i(zcmk), V_70), V_2))))). % 30.71/18.94 tff(c_1726, plain, (![U_5]: (~p(enc(tc, U_5)) | ~p(enc(tmk, i(U_5)))))). % 30.71/18.94 tff(c_1713, plain, (![V_2]: (~p(enc(tc, i(V_2))) | ~p(enc(tmk, V_2))))). % 30.71/18.94 tff(c_1705, plain, (![V_105]: (~p(enc(tc, i(enc(i(tmk), V_105)))) | ~p(V_105)))). % 30.71/18.94 tff(c_1700, plain, (~p(enc(tmk, i(k))))). % 30.71/18.94 tff(c_448, plain, (![V_64, V_2]: (p(enc(enc(i(tmk), V_64), V_2)) | ~p(V_64) | ~p(enc(tc, V_2))))). % 30.71/18.94 tff(c_1634, plain, (![V_4]: (p(enc(pp, enc(i(tmk), V_4))) | ~p(V_4)))). % 30.71/18.94 tff(c_1642, plain, (p(enc(pp, pp)))). % 30.71/18.94 tff(c_1614, plain, (![V_121]: (p(enc(pp, V_121)) | ~p(enc(tmk, V_121))))). % 30.71/18.94 tff(c_1402, plain, (![V_111, V_2]: (p(enc(V_111, V_2)) | ~p(enc(tmk, V_111)) | ~p(enc(tmk, V_2))))). % 30.71/18.94 tff(c_1588, plain, (~p(enc(tmk, tmk)))). % 30.71/18.94 tff(c_803, plain, (![V_82, V_2]: (p(enc(enc(i(tmk), V_82), V_2)) | ~p(V_82) | ~p(enc(tmk, V_2))))). % 30.71/18.94 tff(c_1522, plain, (![V_2]: (~p(enc(tc, V_2)) | ~p(enc(tmk, V_2))))). % 30.71/18.94 tff(c_1530, plain, (~p(enc(tmk, tc)))). % 30.71/18.94 tff(c_1510, plain, (![V_105]: (~p(enc(tc, enc(i(tmk), V_105))) | ~p(V_105)))). % 30.71/18.94 tff(c_1294, plain, (![V_4]: (p(enc(pp, enc(i(tc), V_4))) | ~p(V_4)))). % 30.71/18.94 tff(c_1452, plain, (![V_2]: (~p(enc(tmk, V_2)) | ~p(V_2)))). % 30.71/18.94 tff(c_799, plain, (![V_2, U_83]: (p(enc(V_2, enc(i(tmk), U_83))) | ~p(enc(tmk, V_2)) | ~p(U_83)))). % 30.71/18.94 tff(c_1315, plain, (![V_2]: (~p(i(V_2)) | ~p(enc(tmk, V_2))))). % 30.71/18.94 tff(c_1263, plain, (![V_105]: (~p(i(enc(i(tmk), V_105))) | ~p(V_105)))). % 30.71/18.94 tff(c_1300, plain, (p(enc(pp, k)))). % 30.71/18.94 tff(c_1281, plain, (![V_107]: (p(enc(pp, V_107)) | ~p(enc(tc, V_107))))). % 30.71/18.94 tff(c_1212, plain, (![V_103, V_2]: (p(enc(V_103, V_2)) | ~p(enc(tmk, V_103)) | ~p(enc(tc, V_2))))). % 30.71/18.94 tff(c_1142, plain, (![V_4]: (p(enc(enc(i(tmk), V_4), t2)) | ~p(V_4)))). % 30.71/18.94 tff(c_1168, plain, (~p(enc(tc, i(pp))))). % 30.71/18.94 tff(c_458, plain, (![V_4, U_65]: (p(enc(V_4, enc(i(tc), U_65))) | ~p(enc(tmk, V_4)) | ~p(U_65)))). % 30.71/18.94 tff(c_1163, plain, (~p(enc(tc, pp)))). % 30.71/18.94 tff(c_1158, plain, (~p(i(pp)))). % 30.71/18.94 tff(c_1147, plain, (p(enc(pp, t2)))). % 30.71/18.94 tff(c_1133, plain, (![V_100]: (p(enc(V_100, t2)) | ~p(enc(tmk, V_100))))). % 30.71/18.94 tff(c_1052, plain, (![V_2, V_94]: (p(enc(V_2, V_94)) | ~p(enc(lp, V_94)) | ~p(enc(tmk, V_2))))). % 30.71/18.94 tff(c_24, plain, (![W_30, V_29, U_28]: (p(enc(enc(i(wk), W_30), enc(i(enc(i(tmk), V_29)), U_28))) | ~p(W_30) | ~p(V_29) | ~p(U_28)))). % 30.71/18.94 tff(c_1067, plain, (![V_4]: (p(V_4) | ~p(enc(lp, enc(i(w), V_4)))))). % 30.71/18.94 tff(c_1055, plain, (![V_94]: (p(enc(w, V_94)) | ~p(enc(lp, V_94))))). % 30.71/18.94 tff(c_1026, plain, (![V_2, V_92]: (p(enc(V_2, V_92)) | ~p(enc(wk, V_2)) | ~p(enc(lp, V_92))))). % 30.71/18.95 tff(c_679, plain, (![V_74, V_2]: (p(enc(enc(i(wk), V_74), V_2)) | ~p(V_74) | ~p(enc(lp, V_2))))). % 30.71/18.95 tff(c_26, plain, (![W_33, V_32, U_31]: (p(enc(enc(i(wk), W_33), enc(i(enc(i(wk), V_32)), U_31))) | ~p(W_33) | ~p(V_32) | ~p(U_31)))). % 30.71/18.95 tff(c_968, plain, (~p(enc(tc, i(w))))). % 30.71/18.95 tff(c_918, plain, (![V_11, U_10]: (p(enc(i(enc(i(zcmk), V_11)), enc(i(tmk), U_10))) | ~p(V_11) | ~p(U_10)))). % 30.71/18.95 tff(c_924, plain, (~p(enc(tc, i(lp))))). % 30.71/18.95 tff(c_919, plain, (~p(enc(tc, i(tc))))). % 30.71/18.95 tff(c_875, plain, (~p(enc(tc, i(wk))))). % 30.71/18.95 tff(c_872, plain, (~p(enc(tc, i(tmk))))). % 30.71/18.95 tff(c_784, plain, (![V_80, U_5]: (p(V_80) | ~p(enc(U_5, V_80)) | ~p(enc(tc, i(U_5)))))). % 30.71/18.95 tff(c_729, plain, (![V_17, U_16]: (p(enc(enc(i(tmk), V_17), enc(i(tmk), U_16))) | ~p(V_17) | ~p(U_16)))). % 30.71/18.95 tff(c_745, plain, (![V_78, V_2]: (p(V_78) | ~p(enc(i(V_2), V_78)) | ~p(enc(tc, V_2))))). % 30.71/18.95 tff(c_229, plain, (![V_4, U_51]: (p(V_4) | ~p(enc(i(enc(i(tc), U_51)), V_4)) | ~p(U_51)))). % 30.71/18.95 tff(c_480, plain, (![U_5, V_67]: (p(enc(U_5, V_67)) | ~p(V_67) | ~p(enc(tc, i(U_5)))))). % 30.71/18.95 tff(c_642, plain, (![V_35, U_34]: (p(enc(enc(i(wk), V_35), enc(i(lp), U_34))) | ~p(V_35) | ~p(U_34)))). % 30.71/18.95 tff(c_345, plain, (![V_4, U_55]: (p(V_4) | ~p(enc(enc(i(tc), U_55), V_4)) | ~p(U_55)))). % 30.71/18.95 tff(c_610, plain, (~p(enc(tc, tc)))). % 30.71/18.95 tff(c_579, plain, (~p(enc(tc, w)))). % 30.71/18.95 tff(c_569, plain, (![V_8, U_7]: (p(enc(tmk, enc(i(enc(i(zcmk), V_8)), U_7))) | ~p(V_8) | ~p(U_7)))). % 30.71/18.95 tff(c_574, plain, (~p(enc(tc, lp)))). % 30.71/18.95 tff(c_538, plain, (~p(enc(tc, wk)))). % 30.71/18.95 tff(c_535, plain, (~p(enc(tc, tmk)))). % 30.71/18.95 tff(c_473, plain, (![V_2, U_1]: (p(V_2) | ~p(enc(U_1, V_2)) | ~p(enc(tc, U_1))))). % 30.71/18.95 tff(c_344, plain, (![V_4, V_56]: (p(enc(i(V_4), V_56)) | ~p(V_56) | ~p(enc(tc, V_4))))). % 30.71/18.95 tff(c_401, plain, (![V_20, U_19]: (p(enc(enc(i(tmk), V_20), enc(i(tc), U_19))) | ~p(V_20) | ~p(U_19)))). % 30.71/18.95 tff(c_420, plain, (![V_4]: (p(V_4) | ~p(enc(i(k), V_4))))). % 30.71/18.95 tff(c_412, plain, (![V_61]: (p(enc(k, V_61)) | ~p(V_61)))). % 30.71/18.95 tff(c_231, plain, (![V_4, V_52]: (p(enc(V_4, V_52)) | ~p(V_52) | ~p(enc(tc, V_4))))). % 30.71/18.95 tff(c_320, plain, (![V_4]: (p(V_4) | ~p(enc(tmk, enc(i(wk), V_4)))))). % 30.71/18.95 tff(c_157, plain, (![V_4, U_3]: (p(V_4) | ~p(enc(i(U_3), V_4)) | ~p(U_3)))). % 30.71/18.95 tff(c_294, plain, (![U_25, V_26]: (p(enc(i(enc(i(tc), U_25)), V_26)) | ~p(V_26) | ~p(U_25)))). % 30.71/18.95 tff(c_306, plain, (![V_2]: (p(enc(wk, V_2)) | ~p(enc(tmk, V_2))))). % 30.71/18.95 tff(c_277, plain, (![U_13]: (p(enc(wk, enc(i(tmk), U_13))) | ~p(U_13)))). % 30.71/18.95 tff(c_298, plain, (~p(tc))). % 30.71/18.95 tff(c_278, plain, (~p(i(tc)))). % 30.71/18.95 tff(c_261, plain, (~p(lp))). % 30.71/18.95 tff(c_257, plain, (~p(i(lp)))). % 30.71/18.95 tff(c_256, plain, (~p(w))). % 30.71/18.95 tff(c_236, plain, (~p(i(w)))). % 30.71/18.95 tff(c_235, plain, (~p(wk))). % 30.71/18.95 tff(c_213, plain, (~p(i(wk)))). % 30.71/18.95 tff(c_174, plain, (![U_22, V_23]: (p(enc(enc(i(tc), U_22), V_23)) | ~p(V_23) | ~p(U_22)))). % 30.71/18.95 tff(c_212, plain, (~p(tmk))). % 30.71/18.95 tff(c_207, plain, (~p(i(tmk)))). % 30.71/18.95 tff(c_154, plain, (![V_2, U_1]: (p(V_2) | ~p(enc(U_1, V_2)) | ~p(i(U_1))))). % 30.71/18.95 tff(c_160, plain, (~p(pp))). % 30.71/18.95 tff(c_147, plain, (![U_37, V_38]: (p(enc(U_37, V_38)) | ~p(V_38) | ~p(U_37)))). % 30.71/18.95 tff(c_2, plain, (![U_1, V_2]: (enc(i(U_1), enc(U_1, V_2))=V_2))). % 30.71/18.95 tff(c_4, plain, (![U_3, V_4]: (enc(U_3, enc(i(U_3), V_4))=V_4))). % 30.71/18.95 tff(c_69, plain, (![U_5]: (p(U_5) | ~p(i(U_5))))). % 30.71/18.95 tff(c_8, plain, (![U_6]: (p(i(U_6)) | ~p(U_6)))). % 30.71/18.95 tff(c_36, plain, (p(enc(w, t1)))). % 30.71/18.95 tff(c_40, plain, (p(enc(tc, k)))). % 30.71/18.95 tff(c_6, plain, (![U_5]: (i(i(U_5))=U_5))). % 30.71/18.95 tff(c_38, plain, (p(enc(lp, t2)))). % 30.71/18.95 tff(c_32, plain, (p(enc(tmk, pp)))). % 30.71/18.95 tff(c_34, plain, (p(enc(wk, w)))). % 30.71/18.95 tff(c_48, plain, (~p(enc(pp, a)))). % 30.71/18.95 tff(c_44, plain, (p(i(kk)))). % 30.71/18.95 tff(c_42, plain, (p(kk))). % 30.71/18.95 tff(c_46, plain, (p(a))). % 30.71/18.95 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.71/18.95 %------------------------------------------------------------------------------