%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN720-1 : TPTP v9.0.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 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 : 300s % DateTime : Wed Apr 9 10:04:16 PM UTC 2025 % Result : Satisfiable 151.76s 133.30s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SYN720-1 : TPTP v9.0.0. Released v2.5.0. % 0.00/0.10 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.09/0.29 % Computer : n032.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Wed Apr 9 08:12:15 EDT 2025 % 0.09/0.29 % CPUTime : % 151.76/133.30 % 151.76/133.30 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 151.76/133.30 % 151.76/133.30 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 151.76/133.31 %$ r3 > q2 > q1 > p5 > p4 > p3 > p2 > p1 > n1 > m3 > m1 > m0 > k3 > s3 > r5 > q5 > q4 > q3 > q0 > p0 > n5 > n4 > n0 > m5 > m4 > l3 > l2 > l1 > k2 > s5 > s4 > s2 > s1 > s0 > r4 > r2 > r1 > r0 > n3 > n2 > m2 > l5 > l4 > l0 > k5 > k4 > k1 > k0 > #nlpp > e > d > c > b > a % 151.76/133.31 % 151.76/133.31 %Foreground sorts: % 151.76/133.31 % 151.76/133.31 % 151.76/133.31 %Background operators: % 151.76/133.31 % 151.76/133.31 % 151.76/133.31 %Foreground operators: % 151.76/133.31 tff(n5, type, n5: ($i * $i) > $o). % 151.76/133.31 tff(p2, type, p2: ($i * $i * $i) > $o). % 151.76/133.31 tff(m2, type, m2: $i > $o). % 151.76/133.31 tff(s5, type, s5: $i > $o). % 151.76/133.31 tff(s1, type, s1: $i > $o). % 151.76/133.31 tff(m5, type, m5: ($i * $i) > $o). % 151.76/133.31 tff(q4, type, q4: ($i * $i) > $o). % 151.76/133.31 tff(m4, type, m4: ($i * $i) > $o). % 151.76/133.31 tff(a, type, a: $i). % 151.76/133.31 tff(k1, type, k1: $i > $o). % 151.76/133.31 tff(l1, type, l1: ($i * $i) > $o). % 151.76/133.31 tff(s0, type, s0: $i > $o). % 151.76/133.31 tff(q2, type, q2: ($i * $i * $i) > $o). % 151.76/133.31 tff(n0, type, n0: ($i * $i) > $o). % 151.76/133.31 tff(k0, type, k0: $i > $o). % 151.76/133.31 tff(m3, type, m3: ($i * $i * $i) > $o). % 151.76/133.31 tff(r4, type, r4: $i > $o). % 151.76/133.31 tff(l0, type, l0: $i > $o). % 151.76/133.31 tff(q0, type, q0: ($i * $i) > $o). % 151.76/133.31 tff(k4, type, k4: $i > $o). % 151.76/133.31 tff(m1, type, m1: ($i * $i * $i) > $o). % 151.76/133.31 tff(b, type, b: $i). % 151.76/133.31 tff(p0, type, p0: ($i * $i) > $o). % 151.76/133.31 tff(r0, type, r0: $i > $o). % 151.76/133.31 tff(q1, type, q1: ($i * $i * $i) > $o). % 151.76/133.31 tff(s4, type, s4: $i > $o). % 151.76/133.31 tff(r3, type, r3: ($i * $i * $i) > $o). % 151.76/133.31 tff(k2, type, k2: ($i * $i) > $o). % 151.76/133.31 tff(n2, type, n2: $i > $o). % 151.76/133.31 tff(s3, type, s3: ($i * $i) > $o). % 151.76/133.31 tff(l3, type, l3: ($i * $i) > $o). % 151.76/133.31 tff(p3, type, p3: ($i * $i * $i) > $o). % 151.76/133.31 tff(p4, type, p4: ($i * $i * $i) > $o). % 151.76/133.31 tff(s2, type, s2: $i > $o). % 151.76/133.31 tff(r5, type, r5: ($i * $i) > $o). % 151.76/133.31 tff(k3, type, k3: ($i * $i * $i) > $o). % 151.76/133.31 tff(d, type, d: $i). % 151.76/133.31 tff(l2, type, l2: ($i * $i) > $o). % 151.76/133.31 tff(l4, type, l4: $i > $o). % 151.76/133.31 tff(l5, type, l5: $i > $o). % 151.76/133.31 tff(k5, type, k5: $i > $o). % 151.76/133.31 tff(p5, type, p5: ($i * $i * $i) > $o). % 151.76/133.31 tff(n4, type, n4: ($i * $i) > $o). % 151.76/133.31 tff(q3, type, q3: ($i * $i) > $o). % 151.76/133.31 tff(m0, type, m0: ($i * $i * $i) > $o). % 151.76/133.31 tff(q5, type, q5: ($i * $i) > $o). % 151.76/133.31 tff(e, type, e: $i). % 151.76/133.31 tff(n1, type, n1: ($i * $i * $i) > $o). % 151.76/133.31 tff(r1, type, r1: $i > $o). % 151.76/133.31 tff(n3, type, n3: $i > $o). % 151.76/133.31 tff(r2, type, r2: $i > $o). % 151.76/133.31 tff(p1, type, p1: ($i * $i * $i) > $o). % 151.76/133.31 tff(c, type, c: $i). % 151.76/133.31 % 151.76/133.31 %Saturated clause set: % 151.76/133.31 tff(c_617863, plain, (![B_57413, C_57414]: (q3(B_57413, B_57413) | ~s0(B_57413) | ~p0(B_57413, C_57414) | ~n0(B_57413, C_57414) | ~l1(B_57413, C_57414) | ~r0(C_57414) | ~l0(B_57413) | ~p0(C_57414, B_57413)))). % 151.76/133.31 tff(c_617762, plain, (![I_155, I_56996]: (~n0(I_155, I_56996) | q3(I_56996, I_155) | ~l1(I_155, I_56996) | ~r0(I_56996) | ~l0(I_155) | ~m0(I_56996, I_155, b) | ~m0(b, I_56996, c)))). % 151.76/133.31 tff(c_617764, plain, (![I_155, I_56998]: (~n0(I_155, I_56998) | q3(I_56998, I_155) | ~l1(I_155, I_56998) | ~r0(I_56998) | ~l0(I_155) | ~m0(I_56998, I_155, e) | ~m0(e, I_56998, d)))). % 151.76/133.32 tff(c_617766, plain, (![I_155, I_56848]: (~n0(I_155, I_56848) | q3(I_56848, I_155) | ~l1(I_155, I_56848) | ~r0(I_56848) | ~l0(I_155) | ~m0(I_56848, I_155, d) | ~m0(d, I_56848, c)))). % 151.76/133.32 tff(c_617788, plain, (![I_155, I_56359]: (~n0(I_155, I_56359) | q3(I_56359, I_155) | ~l1(I_155, I_56359) | ~r0(I_56359) | ~l0(I_155) | ~m0(I_56359, I_155, d) | ~m0(d, I_56359, d)))). % 151.76/133.32 tff(c_617795, plain, (![I_155, I_56706]: (~n0(I_155, I_56706) | q3(I_56706, I_155) | ~l1(I_155, I_56706) | ~r0(I_56706) | ~l0(I_155) | ~m0(I_56706, I_155, b) | ~m0(b, I_56706, b)))). % 151.76/133.32 tff(c_617794, plain, (![I_155, I_56345]: (~n0(I_155, I_56345) | q3(I_56345, I_155) | ~l1(I_155, I_56345) | ~r0(I_56345) | ~l0(I_155) | ~m0(I_56345, I_155, d) | ~m0(d, I_56345, e)))). % 151.76/133.32 tff(c_617864, plain, (![B_57413, C_57414]: (q3(B_57413, B_57413) | ~m0(e, C_57414, d) | ~n0(B_57413, C_57414) | ~l1(B_57413, C_57414) | ~r0(C_57414) | ~l0(B_57413) | ~p0(C_57414, B_57413)))). % 151.76/133.32 tff(c_617362, plain, (![C_57400, B_57399]: (q3(C_57400, C_57400) | ~m0(e, B_57399, d) | ~s2(B_57399) | ~n0(B_57399, C_57400) | ~l1(B_57399, C_57400) | ~l0(C_57400) | ~p0(C_57400, B_57399)))). % 151.76/133.32 tff(c_618921, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(e, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.32 tff(c_617987, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(c, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.32 tff(c_617875, plain, (![B_57413, C_57414]: (q3(B_57413, B_57413) | ~m0(e, C_57414, a) | ~n0(B_57413, C_57414) | ~l1(B_57413, C_57414) | ~r0(C_57414) | ~l0(B_57413) | ~p0(C_57414, B_57413)))). % 151.76/133.32 tff(c_617373, plain, (![C_57400, B_57399]: (q3(C_57400, C_57400) | ~m0(e, B_57399, a) | ~s2(B_57399) | ~n0(B_57399, C_57400) | ~l1(B_57399, C_57400) | ~l0(C_57400) | ~p0(C_57400, B_57399)))). % 151.76/133.32 tff(c_617280, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(d, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.32 tff(c_619952, plain, (![I_57546, E_57545]: (n4(I_57546, E_57545) | ~n1(d, I_57546, c) | ~l2(I_57546, d) | ~k1(I_57546) | ~m0(c, I_57546, a)))). % 151.76/133.32 tff(c_610412, plain, (![D_57140, E_57141, I_155]: (~k2(D_57140, E_57141) | p3(I_155, D_57140, E_57141) | ~n1(d, I_155, c) | ~l2(I_155, d) | ~k1(I_155) | ~m0(c, I_155, a)))). % 151.76/133.32 tff(c_616903, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(b, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.32 tff(c_616674, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(a, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.32 tff(c_615386, plain, (![B_57310, C_57311]: (q3(B_57310, B_57310) | ~s0(B_57310) | ~p0(B_57310, C_57311) | ~n0(B_57310, C_57311) | ~l1(B_57310, C_57311) | ~l0(C_57311) | ~p0(C_57311, B_57310)))). % 151.76/133.32 tff(c_614738, plain, (![B_57291]: (q3(B_57291, B_57291) | ~s0(B_57291) | ~p0(B_57291, c) | ~n0(B_57291, c) | ~l2(B_57291, c) | ~k1(B_57291) | ~p0(c, B_57291)))). % 151.76/133.32 tff(c_615133, plain, (![I_155, I_56996]: (~n0(I_155, I_56996) | q3(I_56996, I_155) | ~l1(I_155, I_56996) | ~l0(I_56996) | ~m0(I_56996, I_155, b) | ~m0(b, I_56996, c)))). % 151.76/133.32 tff(c_615135, plain, (![I_155, I_56998]: (~n0(I_155, I_56998) | q3(I_56998, I_155) | ~l1(I_155, I_56998) | ~l0(I_56998) | ~m0(I_56998, I_155, e) | ~m0(e, I_56998, d)))). % 151.76/133.32 tff(c_615137, plain, (![I_155, I_56848]: (~n0(I_155, I_56848) | q3(I_56848, I_155) | ~l1(I_155, I_56848) | ~l0(I_56848) | ~m0(I_56848, I_155, d) | ~m0(d, I_56848, c)))). % 151.76/133.32 tff(c_615157, plain, (![I_155, I_56359]: (~n0(I_155, I_56359) | q3(I_56359, I_155) | ~l1(I_155, I_56359) | ~l0(I_56359) | ~m0(I_56359, I_155, d) | ~m0(d, I_56359, d)))). % 151.76/133.32 tff(c_615164, plain, (![I_155, I_56706]: (~n0(I_155, I_56706) | q3(I_56706, I_155) | ~l1(I_155, I_56706) | ~l0(I_56706) | ~m0(I_56706, I_155, b) | ~m0(b, I_56706, b)))). % 151.76/133.32 tff(c_619554, plain, (![D_385, D_57518]: (q4(D_385, D_57518) | ~n1(D_57518, D_385, c) | ~p1(D_385, D_385, c) | ~l2(D_385, D_57518) | ~k1(D_385)))). % 151.76/133.32 tff(c_619750, plain, (~m0(c, a, a))). % 151.76/133.32 tff(c_619716, plain, (~p1(a, a, c))). % 151.76/133.32 tff(c_619677, plain, (~p1(e, e, c))). % 151.76/133.32 tff(c_619476, plain, (![D_57518]: (q4(b, D_57518) | ~n1(D_57518, b, c) | ~l2(b, D_57518)))). % 151.76/133.32 tff(c_619585, plain, (![A_14]: (q4(c, A_14) | ~l2(c, A_14) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.32 tff(c_619537, plain, (![D_57518]: (q4(c, D_57518) | ~n1(D_57518, c, c) | ~l2(c, D_57518)))). % 151.76/133.32 tff(c_617072, plain, (![I_57391, H_57390, I_155]: (~m0(b, I_57391, H_57390) | p1(I_57391, I_155, b) | ~m0(H_57390, b, b) | ~q0(H_57390, b) | ~s0(H_57390) | ~p0(H_57390, b)))). % 151.76/133.32 tff(c_615163, plain, (![I_155, I_56345]: (~n0(I_155, I_56345) | q3(I_56345, I_155) | ~l1(I_155, I_56345) | ~l0(I_56345) | ~m0(I_56345, I_155, d) | ~m0(d, I_56345, e)))). % 151.76/133.32 tff(c_619185, plain, (![C_57493, B_57492]: (q3(C_57493, C_57493) | ~s2(B_57492) | ~n0(B_57492, C_57493) | ~l1(B_57492, C_57493) | ~r0(C_57493) | ~l0(B_57492) | ~p0(C_57493, B_57492)))). % 151.76/133.32 tff(c_615165, plain, (![B_35]: (~n0(b, B_35) | q3(B_35, b) | ~l1(b, B_35) | ~l0(B_35) | ~m0(B_35, b, b) | ~m0(b, b, B_35)))). % 151.76/133.32 tff(c_617862, plain, (![B_57413, C_57414]: (q3(B_57413, B_57413) | ~r0(B_57413) | ~n0(B_57413, C_57414) | ~l1(B_57413, C_57414) | ~r0(C_57414) | ~l0(B_57413) | ~p0(C_57414, B_57413)))). % 151.76/133.32 tff(c_617366, plain, (![C_57400, B_57399]: (q3(C_57400, C_57400) | ~k0(B_57399) | ~s2(B_57399) | ~n0(B_57399, C_57400) | ~l1(B_57399, C_57400) | ~l0(C_57400) | ~p0(C_57400, B_57399)))). % 151.76/133.32 tff(c_612547, plain, (![A_57231]: (q3(A_57231, A_57231) | ~s0(A_57231) | ~p0(A_57231, c) | ~n0(c, A_57231) | ~l2(c, A_57231) | ~l0(A_57231) | ~k1(A_57231)))). % 151.76/133.32 tff(c_617361, plain, (![C_57400, B_57399]: (q3(C_57400, C_57400) | ~s0(C_57400) | ~s2(B_57399) | ~n0(B_57399, C_57400) | ~l1(B_57399, C_57400) | ~l0(C_57400) | ~p0(C_57400, B_57399)))). % 151.76/133.32 tff(c_617360, plain, (![C_57400, B_57399]: (q3(C_57400, C_57400) | ~r0(C_57400) | ~s2(B_57399) | ~n0(B_57399, C_57400) | ~l1(B_57399, C_57400) | ~l0(C_57400) | ~p0(C_57400, B_57399)))). % 151.76/133.33 tff(c_615387, plain, (![B_57310, C_57311]: (q3(B_57310, B_57310) | ~m0(e, C_57311, d) | ~n0(B_57310, C_57311) | ~l1(B_57310, C_57311) | ~l0(C_57311) | ~p0(C_57311, B_57310)))). % 151.76/133.33 tff(c_615394, plain, (![B_57310, C_57311]: (q3(B_57310, B_57310) | ~m0(e, C_57311, a) | ~n0(B_57310, C_57311) | ~l1(B_57310, C_57311) | ~l0(C_57311) | ~p0(C_57311, B_57310)))). % 151.76/133.33 tff(c_615125, plain, (![I_57228]: (~n0(b, I_57228) | q3(I_57228, b) | ~l1(b, I_57228) | ~m0(I_57228, b, b) | ~q0(I_57228, b) | ~l0(I_57228)))). % 151.76/133.33 tff(c_617884, plain, (![B_57413, C_57414]: (~s2(B_57413) | q3(B_57413, C_57414) | ~n0(B_57413, C_57414) | ~l1(B_57413, C_57414) | ~r0(C_57414) | ~l0(B_57413) | ~p0(C_57414, B_57413)))). % 151.76/133.33 tff(c_616776, plain, (![J_57379]: (~n1(e, J_57379, a) | p2(J_57379, e, a) | ~q0(a, J_57379) | ~s0(J_57379) | ~p0(J_57379, c) | ~k0(J_57379)))). % 151.76/133.33 tff(c_614773, plain, (![E_189, X_57295, G_57294]: (~l0(E_189) | ~k0(X_57295) | q1(E_189, G_57294, G_57294) | ~q0(G_57294, X_57295) | ~s0(X_57295) | ~p0(X_57295, c) | ~r0(G_57294)))). % 151.76/133.33 tff(c_608540, plain, (![E_56573, A_14]: (q3(E_56573, E_56573) | ~s0(E_56573) | ~p0(E_56573, A_14) | ~n0(E_56573, A_14) | ~k0(E_56573) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.33 tff(c_616773, plain, (![E_189, I_57378, J_57379]: (~l0(E_189) | q1(E_189, I_57378, I_57378) | ~q0(I_57378, J_57379) | ~s0(J_57379) | ~p0(J_57379, c) | ~k0(J_57379) | ~l0(I_57378)))). % 151.76/133.33 tff(c_615783, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(e, F_54353) | ~r0(F_54353) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.33 tff(c_618934, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(e, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.33 tff(c_613600, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(c, F_54353) | ~r0(F_54353) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.33 tff(c_618000, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(c, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.33 tff(c_617804, plain, (![I_155, I_56320]: (~n0(I_155, I_56320) | q3(I_56320, I_155) | ~l1(I_155, I_56320) | ~r0(I_56320) | ~l0(I_155) | ~m0(I_56320, I_155, a)))). % 151.76/133.33 tff(c_617379, plain, (![B_57399]: (q3(c, B_57399) | ~p0(B_57399, B_57399) | ~s2(B_57399) | ~n0(B_57399, c) | ~l1(B_57399, c) | ~p0(c, B_57399)))). % 151.76/133.33 tff(c_617294, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(d, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.33 tff(c_613425, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(d, F_54353) | ~r0(F_54353) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.33 tff(c_618810, plain, (![H_57464, H_38]: (~m1(H_57464, a, H_38) | m1(H_38, a, a) | ~q0(e, H_57464) | ~s0(H_57464) | ~p0(H_57464, c)))). % 151.76/133.33 tff(c_618811, plain, (![H_57464]: (q1(H_57464, H_57464, a) | ~q0(e, H_57464) | ~s0(H_57464) | ~p0(H_57464, c)))). % 151.76/133.33 tff(c_618712, plain, (![H_57462]: (m1(H_57462, a, a) | ~q0(e, H_57462) | ~s0(H_57462) | ~p0(H_57462, c)))). % 151.76/133.33 tff(c_613248, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(b, F_54353) | ~r0(F_54353) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.33 tff(c_616917, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(b, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.33 tff(c_617879, plain, (![C_57414]: (q3(c, C_57414) | ~p0(C_57414, C_57414) | ~n0(c, C_57414) | ~l1(c, C_57414) | ~r0(C_57414) | ~p0(C_57414, c)))). % 151.76/133.33 tff(c_612680, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~q0(a, F_54353) | ~r0(F_54353) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.33 tff(c_615399, plain, (![C_57311]: (q3(b, C_57311) | ~p0(C_57311, C_57311) | ~n0(b, C_57311) | ~l1(b, C_57311) | ~l0(C_57311) | ~p0(C_57311, b)))). % 151.76/133.33 tff(c_614047, plain, (![I_57279, I_57278, I_155]: (~m0(b, I_57279, I_57278) | p1(I_57279, I_155, b) | ~m0(I_57278, b, b) | ~q0(I_57278, b) | ~l0(I_57278)))). % 151.76/133.33 tff(c_616687, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(a, F_54353) | ~s0(F_54353) | ~p0(F_54353, c) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.33 tff(c_613853, plain, (![I_57273, G_57272, I_155]: (~m0(b, I_57273, G_57272) | p1(I_57273, I_155, b) | ~m0(G_57272, b, b) | ~q0(G_57272, b) | ~r0(G_57272)))). % 151.76/133.33 tff(c_618603, plain, (![B_57445, E_57444]: (n4(B_57445, E_57444) | ~n1(d, B_57445, c) | ~l2(B_57445, d) | ~k1(B_57445) | ~p0(c, B_57445)))). % 151.76/133.33 tff(c_610429, plain, (![D_57140, E_57141, B_132]: (~k2(D_57140, E_57141) | p3(B_132, D_57140, E_57141) | ~n1(d, B_132, c) | ~l2(B_132, d) | ~k1(B_132) | ~p0(c, B_132)))). % 151.76/133.33 tff(c_615398, plain, (![C_57311]: (q3(c, C_57311) | ~p0(C_57311, C_57311) | ~n0(c, C_57311) | ~l1(c, C_57311) | ~l0(C_57311) | ~p0(C_57311, c)))). % 151.76/133.33 tff(c_618239, plain, (![H_57423, I_57424]: (q1(H_57423, H_57423, I_57424) | ~q0(H_57423, I_57424) | ~s0(I_57424) | ~p0(I_57424, c) | ~s0(H_57423) | ~p0(H_57423, I_57424)))). % 151.76/133.33 tff(c_618548, plain, (![X_57437]: (k3(e, X_57437, e) | ~n1(e, X_57437, a) | ~k0(X_57437)))). % 151.76/133.33 tff(c_618547, plain, (![X_57437]: (r3(X_57437, e, X_57437) | ~n1(e, X_57437, a) | ~k0(X_57437)))). % 151.76/133.33 tff(c_618461, plain, (![X_56994]: (p2(X_56994, e, e) | ~n1(e, X_56994, a) | ~k0(X_56994)))). % 151.76/133.33 tff(c_615385, plain, (![B_57310, C_57311]: (q3(B_57310, B_57310) | ~r0(B_57310) | ~n0(B_57310, C_57311) | ~l1(B_57310, C_57311) | ~l0(C_57311) | ~p0(C_57311, B_57310)))). % 151.76/133.33 tff(c_614737, plain, (![B_57291]: (q3(B_57291, B_57291) | ~r0(B_57291) | ~n0(B_57291, c) | ~l2(B_57291, c) | ~k1(B_57291) | ~p0(c, B_57291)))). % 151.76/133.33 tff(c_608078, plain, (![E_56573, A_14]: (q3(E_56573, E_56573) | ~m0(e, A_14, d) | ~n0(E_56573, A_14) | ~k0(E_56573) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.33 tff(c_609254, plain, (![I_57096, I_57097, I_57095, I_155]: (~m0(I_57096, I_57097, I_57095) | p1(I_57097, I_155, I_57096) | ~m0(I_57095, I_57096, e) | ~m0(e, I_57095, d)))). % 151.76/133.33 tff(c_609139, plain, (![H_60, I_61]: (m1(H_60, I_61, I_61) | ~q0(H_60, I_61) | ~s0(I_61) | ~p0(I_61, c) | ~s0(H_60) | ~p0(H_60, I_61)))). % 151.76/133.33 tff(c_618057, plain, (~m0(b, c, c))). % 151.76/133.33 tff(c_609549, plain, (![I_57102, I_57103, I_57101, I_155]: (~m0(I_57102, I_57103, I_57101) | p1(I_57103, I_155, I_57102) | ~m0(I_57101, I_57102, b) | ~m0(b, I_57101, c)))). % 151.76/133.33 tff(c_604690, plain, (![E_56917, A_56918]: (q3(E_56917, E_56917) | ~m0(e, A_56918, a) | ~n0(E_56917, A_56918) | ~k0(E_56917) | ~l0(A_56918) | ~k1(A_56918)))). % 151.76/133.33 tff(c_609318, plain, (![H_57098, H_38]: (~m1(H_57098, a, H_38) | m1(H_38, a, a) | ~q0(c, H_57098) | ~s0(H_57098) | ~p0(H_57098, c)))). % 151.76/133.33 tff(c_617812, plain, (![B_132, C_133]: (~n0(B_132, C_133) | q3(C_133, B_132) | ~l1(B_132, C_133) | ~r0(C_133) | ~l0(B_132) | ~p0(C_133, B_132)))). % 151.76/133.33 tff(c_607041, plain, (![I_57012, X_57013]: (~n0(I_57012, X_57013) | q3(X_57013, I_57012) | ~p1(I_57012, I_57012, X_57013) | ~l1(I_57012, X_57013) | ~r0(X_57013) | ~l0(I_57012)))). % 151.76/133.33 tff(c_617591, plain, (~m0(d, c, c))). % 151.76/133.33 tff(c_608872, plain, (![I_57088, I_57089, I_57087, I_155]: (~m0(I_57088, I_57089, I_57087) | p1(I_57089, I_155, I_57088) | ~m0(I_57087, I_57088, d) | ~m0(d, I_57087, c)))). % 151.76/133.33 tff(c_617555, plain, (~m0(d, c, d))). % 151.76/133.33 tff(c_606022, plain, (![I_56968, I_56969, I_56967, I_155]: (~m0(I_56968, I_56969, I_56967) | p1(I_56969, I_155, I_56968) | ~m0(I_56967, I_56968, d) | ~m0(d, I_56967, d)))). % 151.76/133.33 tff(c_617369, plain, (![C_57400]: (q3(C_57400, C_57400) | ~n0(e, C_57400) | ~l1(e, C_57400) | ~l0(C_57400) | ~p0(C_57400, e)))). % 151.76/133.33 tff(c_617365, plain, (![C_57400]: (q3(C_57400, C_57400) | ~n0(b, C_57400) | ~l1(b, C_57400) | ~l0(C_57400) | ~p0(C_57400, b)))). % 151.76/133.33 tff(c_615403, plain, (![B_57310, C_57311]: (~s2(B_57310) | q3(B_57310, C_57311) | ~n0(B_57310, C_57311) | ~l1(B_57310, C_57311) | ~l0(C_57311) | ~p0(C_57311, B_57310)))). % 151.76/133.33 tff(c_605656, plain, (![H_56957, H_38]: (~m1(H_56957, a, H_38) | m1(H_38, a, a) | ~q0(d, H_56957) | ~s0(H_56957) | ~p0(H_56957, c)))). % 151.76/133.33 tff(c_617190, plain, (~m0(b, c, b))). % 151.76/133.34 tff(c_603956, plain, (![I_56887, I_56888, I_56886, I_155]: (~m0(I_56887, I_56888, I_56886) | p1(I_56888, I_155, I_56887) | ~m0(I_56886, I_56887, b) | ~m0(b, I_56886, b)))). % 151.76/133.34 tff(c_614752, plain, (![B_57291]: (~s2(B_57291) | q3(B_57291, c) | ~n0(B_57291, c) | ~l2(B_57291, c) | ~k1(B_57291) | ~p0(c, B_57291)))). % 151.76/133.34 tff(c_614656, plain, (![H_57288, I_54811]: (~m0(H_57288, b, b) | p1(b, I_54811, H_57288) | ~q0(H_57288, b) | ~s0(H_57288) | ~p0(H_57288, b)))). % 151.76/133.34 tff(c_616967, plain, (~m0(d, c, e))). % 151.76/133.34 tff(c_604326, plain, (![I_56904, I_56905, I_56903, I_155]: (~m0(I_56904, I_56905, I_56903) | p1(I_56905, I_155, I_56904) | ~m0(I_56903, I_56904, d) | ~m0(d, I_56903, e)))). % 151.76/133.34 tff(c_604889, plain, (![H_56923, H_38]: (~m1(H_56923, a, H_38) | m1(H_38, a, a) | ~q0(b, H_56923) | ~s0(H_56923) | ~p0(H_56923, c)))). % 151.76/133.34 tff(c_616813, plain, (~m0(b, c, a))). % 151.76/133.34 tff(c_603732, plain, (![I_56881, I_56882, I_56880, I_155]: (~m0(I_56881, I_56882, I_56880) | p1(I_56882, I_155, I_56881) | ~m0(I_56880, I_56881, b) | ~m0(b, I_56880, a)))). % 151.76/133.34 tff(c_616035, plain, (![I_57337, J_57338]: (q1(I_57337, I_57337, J_57338) | ~q0(I_57337, J_57338) | ~s0(J_57338) | ~p0(J_57338, c) | ~k0(J_57338) | ~l0(I_57337)))). % 151.76/133.34 tff(c_612546, plain, (![A_57231]: (q3(A_57231, A_57231) | ~r0(A_57231) | ~n0(c, A_57231) | ~l2(c, A_57231) | ~l0(A_57231) | ~k1(A_57231)))). % 151.76/133.34 tff(c_609535, plain, (![I_57101]: (s2(I_57101) | ~l1(b, I_57101) | ~l0(I_57101) | ~m0(I_57101, b, b) | ~m0(b, I_57101, c)))). % 151.76/133.34 tff(c_604630, plain, (![H_56914, H_38]: (~m1(H_56914, a, H_38) | m1(H_38, a, a) | ~q0(a, H_56914) | ~s0(H_56914) | ~p0(H_56914, c)))). % 151.76/133.34 tff(c_609240, plain, (![I_57095]: (s2(I_57095) | ~l1(b, I_57095) | ~l0(I_57095) | ~m0(I_57095, b, e) | ~m0(e, I_57095, d)))). % 151.76/133.34 tff(c_608832, plain, (![I_57087]: (s2(I_57087) | ~l1(b, I_57087) | ~l0(I_57087) | ~m0(I_57087, b, d) | ~m0(d, I_57087, c)))). % 151.76/133.34 tff(c_613954, plain, (![J_57277]: (~n1(e, J_57277, a) | p2(J_57277, e, a) | ~q0(a, J_57277) | ~r0(J_57277) | ~k0(J_57277)))). % 151.76/133.34 tff(c_606008, plain, (![I_56967]: (s2(I_56967) | ~l1(b, I_56967) | ~l0(I_56967) | ~m0(I_56967, b, d) | ~m0(d, I_56967, d)))). % 151.76/133.34 tff(c_615171, plain, (![I_155, I_56320]: (~n0(I_155, I_56320) | q3(I_56320, I_155) | ~l1(I_155, I_56320) | ~l0(I_56320) | ~m0(I_56320, I_155, a)))). % 151.76/133.34 tff(c_614458, plain, (![I_155]: (~n0(I_155, c) | q3(c, I_155) | ~l2(I_155, c) | ~k1(I_155) | ~m0(c, I_155, a)))). % 151.76/133.34 tff(c_616469, plain, (![X_57364]: (k3(e, X_57364, e) | ~n1(e, X_57364, a) | ~s0(X_57364)))). % 151.76/133.34 tff(c_616468, plain, (![X_57364]: (r3(X_57364, e, X_57364) | ~n1(e, X_57364, a) | ~s0(X_57364)))). % 151.76/133.34 tff(c_616381, plain, (![X_56994]: (p2(X_56994, e, e) | ~n1(e, X_56994, a) | ~s0(X_56994)))). % 151.76/133.34 tff(c_604172, plain, (![I_56706]: (s2(I_56706) | ~l1(b, I_56706) | ~l0(I_56706) | ~m0(I_56706, b, b) | ~m0(b, I_56706, b)))). % 151.76/133.34 tff(c_604312, plain, (![I_56903]: (s2(I_56903) | ~l1(b, I_56903) | ~l0(I_56903) | ~m0(I_56903, b, d) | ~m0(d, I_56903, e)))). % 151.76/133.34 tff(c_604173, plain, (![I_56311]: (s2(I_56311) | ~l1(b, I_56311) | ~l0(I_56311) | ~m0(I_56311, b, b) | ~m0(b, I_56311, a)))). % 151.76/133.34 tff(c_604177, plain, (![B_35]: (s2(B_35) | ~l1(b, B_35) | ~l0(B_35) | ~m0(B_35, b, b) | ~m0(b, b, B_35)))). % 151.76/133.34 tff(c_614851, plain, (![A_57301, E_57300]: (q3(A_57301, A_57301) | ~s2(E_57300) | ~n0(E_57300, A_57301) | ~k0(E_57300) | ~l0(A_57301) | ~k1(A_57301)))). % 151.76/133.34 tff(c_616210, plain, (![E_57351]: (~l0(E_57351) | q1(E_57351, a, a)))). % 151.76/133.34 tff(c_613951, plain, (![E_189, I_57276, J_57277]: (~l0(E_189) | q1(E_189, I_57276, I_57276) | ~q0(I_57276, J_57277) | ~r0(J_57277) | ~k0(J_57277) | ~l0(I_57276)))). % 151.76/133.34 tff(c_615434, plain, (![I_57312]: (q3(I_57312, I_57312) | ~s0(I_57312) | ~p0(I_57312, a) | ~n0(I_57312, a) | ~l1(I_57312, a)))). % 151.76/133.34 tff(c_611886, plain, (![E_56573, A_14]: (q3(E_56573, E_56573) | ~r0(E_56573) | ~n0(E_56573, A_14) | ~k0(E_56573) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.34 tff(c_608740, plain, (![H_57084, A_57085]: (p4(H_57084, A_57085, A_57085) | ~r2(H_57084) | ~k2(A_57085, H_57084) | ~r2(A_57085) | ~l2(c, A_57085) | ~s2(H_57084)))). % 151.76/133.34 tff(c_616084, plain, (![I_57101, I_57102]: (k3(I_57101, I_57101, I_57102) | ~m0(I_57101, I_57102, b) | ~m0(b, I_57101, c)))). % 151.76/133.34 tff(c_611274, plain, (![E_189, X_57178, G_57177]: (~l0(E_189) | ~k0(X_57178) | q1(E_189, G_57177, G_57177) | ~q0(G_57177, X_57178) | ~r0(X_57178) | ~r0(G_57177)))). % 151.76/133.34 tff(c_615870, plain, (![I_57095, I_57096]: (k3(I_57095, I_57095, I_57096) | ~m0(I_57095, I_57096, e) | ~m0(e, I_57095, d)))). % 151.76/133.34 tff(c_609151, plain, (![I_49, J_50]: (m1(I_49, J_50, J_50) | ~q0(I_49, J_50) | ~s0(J_50) | ~p0(J_50, c) | ~k0(J_50) | ~l0(I_49)))). % 151.76/133.34 tff(c_615797, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(e, F_54353) | ~r0(F_54353) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.34 tff(c_613614, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(c, F_54353) | ~r0(F_54353) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.34 tff(c_615848, plain, (![I_57087, I_57088]: (k3(I_57087, I_57087, I_57088) | ~m0(I_57087, I_57088, d) | ~m0(d, I_57087, c)))). % 151.76/133.34 tff(c_603123, plain, (![I_56855, B_56854, I_155]: (~m0(b, I_56855, B_56854) | p1(I_56855, I_155, b) | ~m0(B_56854, b, b) | ~m0(b, b, B_56854)))). % 151.76/133.34 tff(c_613440, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(d, F_54353) | ~r0(F_54353) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.34 tff(c_615686, plain, (![G_57322, H_38]: (~m1(G_57322, a, H_38) | m1(H_38, a, a) | ~q0(e, G_57322) | ~r0(G_57322)))). % 151.76/133.34 tff(c_615687, plain, (![G_57322]: (q1(G_57322, G_57322, a) | ~q0(e, G_57322) | ~r0(G_57322)))). % 151.76/133.34 tff(c_615607, plain, (![G_57320]: (m1(G_57320, a, a) | ~q0(e, G_57320) | ~r0(G_57320)))). % 151.76/133.34 tff(c_613262, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(b, F_54353) | ~r0(F_54353) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.34 tff(c_614028, plain, (![I_57278]: (s2(I_57278) | ~l1(b, I_57278) | ~m0(I_57278, b, b) | ~q0(I_57278, b) | ~l0(I_57278)))). % 151.76/133.34 tff(c_615588, plain, (![I_56967, I_56968]: (k3(I_56967, I_56967, I_56968) | ~m0(I_56967, I_56968, d) | ~m0(d, I_56967, d)))). % 151.76/133.34 tff(c_614967, plain, (![I_56886, I_56887]: (k3(I_56886, I_56886, I_56887) | ~m0(I_56886, I_56887, b) | ~m0(b, I_56886, b)))). % 151.76/133.34 tff(c_615433, plain, (![I_57312]: (q3(I_57312, I_57312) | ~r0(I_57312) | ~n0(I_57312, a) | ~l1(I_57312, a)))). % 151.76/133.34 tff(c_615514, plain, (~l1(c, a))). % 151.76/133.34 tff(c_615444, plain, (![I_57312]: (~s2(I_57312) | q3(I_57312, a) | ~n0(I_57312, a) | ~l1(I_57312, a)))). % 151.76/133.34 tff(c_615174, plain, (![I_155]: (~n0(I_155, a) | q3(a, I_155) | ~l1(I_155, a)))). % 151.76/133.34 tff(c_615181, plain, (![B_132, C_133]: (~n0(B_132, C_133) | q3(C_133, B_132) | ~l1(B_132, C_133) | ~l0(C_133) | ~p0(C_133, B_132)))). % 151.76/133.34 tff(c_615263, plain, (![X_57308]: (q3(X_57308, X_57308) | ~n0(d, X_57308) | ~l0(X_57308)))). % 151.76/133.34 tff(c_615229, plain, (![X_57307]: (q3(d, X_57307) | ~n0(d, X_57307) | ~l0(X_57307)))). % 151.76/133.34 tff(c_615148, plain, (![X_1]: (~n0(d, X_1) | q3(X_1, d) | ~l0(X_1)))). % 151.76/133.34 tff(c_604091, plain, (![E_56899, D_56900]: (~n0(E_56899, D_56900) | q3(D_56900, E_56899) | ~p1(E_56899, E_56899, D_56900) | ~l1(E_56899, D_56900) | ~l0(D_56900)))). % 151.76/133.34 tff(c_614953, plain, (![I_56903, I_56904]: (k3(I_56903, I_56903, I_56904) | ~m0(I_56903, I_56904, d) | ~m0(d, I_56903, e)))). % 151.76/133.34 tff(c_614850, plain, (![A_57301]: (q3(A_57301, A_57301) | ~n0(b, A_57301) | ~l0(A_57301) | ~k1(A_57301)))). % 151.76/133.34 tff(c_604701, plain, (![E_56917, A_56918]: (~s2(E_56917) | q3(E_56917, A_56918) | ~n0(E_56917, A_56918) | ~k0(E_56917) | ~l0(A_56918) | ~k1(A_56918)))). % 151.76/133.34 tff(c_612694, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~q0(a, F_54353) | ~r0(F_54353) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.34 tff(c_614706, plain, (![H_57288, I_57289]: (q1(H_57288, H_57288, I_57289) | ~q0(H_57288, I_57289) | ~r0(I_57289) | ~s0(H_57288) | ~p0(H_57288, I_57289)))). % 151.76/133.34 tff(c_613169, plain, (![G_57245, X_57246]: (q1(G_57245, G_57245, X_57246) | ~q0(G_57245, X_57246) | ~s0(X_57246) | ~p0(X_57246, c) | ~r0(G_57245)))). % 151.76/133.34 tff(c_614759, plain, (![I_56880, I_56881]: (k3(I_56880, I_56880, I_56881) | ~m0(I_56880, I_56881, b) | ~m0(b, I_56880, a)))). % 151.76/133.34 tff(c_614753, plain, (~p0(c, a))). % 151.76/133.34 tff(c_614475, plain, (![B_132]: (~n0(B_132, c) | q3(c, B_132) | ~l2(B_132, c) | ~k1(B_132) | ~p0(c, B_132)))). % 151.76/133.34 tff(c_614701, plain, (![H_57288]: (k3(b, b, H_57288) | ~q0(H_57288, b) | ~s0(H_57288) | ~p0(H_57288, b)))). % 151.76/133.35 tff(c_611100, plain, (![H_60, I_61]: (m1(H_60, I_61, I_61) | ~q0(H_60, I_61) | ~r0(I_61) | ~s0(H_60) | ~p0(H_60, I_61)))). % 151.76/133.35 tff(c_608560, plain, (![Y_56462, D_56461]: (q3(Y_56462, Y_56462) | ~s0(Y_56462) | ~p0(Y_56462, D_56461) | ~n0(Y_56462, D_56461) | ~k0(D_56461)))). % 151.76/133.35 tff(c_608557, plain, (![E_56583]: (q3(E_56583, E_56583) | ~s0(E_56583) | ~p0(E_56583, c) | ~l2(E_56583, d) | ~k1(E_56583)))). % 151.76/133.35 tff(c_610218, plain, (![E_99]: (~n0(E_99, c) | q3(c, E_99) | ~p1(E_99, E_99, c) | ~l2(E_99, c) | ~k1(E_99)))). % 151.76/133.35 tff(c_608551, plain, (![E_56573]: (q3(E_56573, E_56573) | ~s0(E_56573) | ~p0(E_56573, a) | ~n0(E_56573, a) | ~k0(E_56573)))). % 151.76/133.35 tff(c_608550, plain, (![E_56573]: (q3(E_56573, E_56573) | ~s0(E_56573) | ~p0(E_56573, c) | ~n0(E_56573, c) | ~k0(E_56573)))). % 151.76/133.35 tff(c_608547, plain, (![X_56879]: (q3(X_56879, X_56879) | ~s0(X_56879) | ~p0(X_56879, e) | ~n0(e, X_56879) | ~k1(X_56879)))). % 151.76/133.35 tff(c_614054, plain, (![I_57278]: (p1(I_57278, b, I_57278) | ~m0(I_57278, b, b) | ~q0(I_57278, b) | ~l0(I_57278)))). % 151.76/133.35 tff(c_612464, plain, (![I_57228, I_54811]: (~m0(I_57228, b, b) | p1(b, I_54811, I_57228) | ~q0(I_57228, b) | ~l0(I_57228)))). % 151.76/133.35 tff(c_612515, plain, (![I_57228, J_57229]: (q1(I_57228, I_57228, J_57229) | ~q0(I_57228, J_57229) | ~r0(J_57229) | ~k0(J_57229) | ~l0(I_57228)))). % 151.76/133.35 tff(c_604697, plain, (![A_56918]: (q3(b, A_56918) | ~p0(A_56918, A_56918) | ~n0(b, A_56918) | ~l0(A_56918) | ~k1(A_56918)))). % 151.76/133.35 tff(c_613862, plain, (![G_57272]: (p1(G_57272, b, G_57272) | ~m0(G_57272, b, b) | ~q0(G_57272, b) | ~r0(G_57272)))). % 151.76/133.35 tff(c_613122, plain, (![G_57245, I_54811]: (~m0(G_57245, b, b) | p1(b, I_54811, G_57245) | ~q0(G_57245, b) | ~r0(G_57245)))). % 151.76/133.35 tff(c_613736, plain, (![X_57268, A_57269]: (n4(X_57268, A_57269) | ~s0(A_57269) | ~p0(A_57269, X_57268)))). % 151.76/133.35 tff(c_613731, plain, (![X_57267, A_428]: (p3(X_57267, A_428, A_428) | ~s0(A_428) | ~p0(A_428, X_57267)))). % 151.76/133.35 tff(c_613671, plain, (![E_56573, A_14]: (q4(E_56573, A_14) | ~k0(E_56573) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.35 tff(c_612876, plain, (![D_385, E_57239]: (q4(D_385, E_57239) | ~n1(E_57239, D_385, D_385) | ~k0(D_385)))). % 151.76/133.35 tff(c_597744, plain, (![G_56606, H_38]: (~m1(G_56606, a, H_38) | m1(H_38, a, a) | ~q0(c, G_56606) | ~r0(G_56606)))). % 151.76/133.35 tff(c_613511, plain, (![Y_5]: (q4(Y_5, a) | ~k0(Y_5)))). % 151.76/133.35 tff(c_597573, plain, (![G_56601, H_38]: (~m1(G_56601, a, H_38) | m1(H_38, a, a) | ~q0(d, G_56601) | ~r0(G_56601)))). % 151.76/133.35 tff(c_613334, plain, (![Y_5]: (q4(Y_5, c) | ~k0(Y_5)))). % 151.76/133.35 tff(c_612911, plain, (![A_14]: (q4(b, A_14) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.35 tff(c_597681, plain, (![G_56603, H_38]: (~m1(G_56603, a, H_38) | m1(H_38, a, a) | ~q0(b, G_56603) | ~r0(G_56603)))). % 151.76/133.35 tff(c_613024, plain, (![X_4]: (q4(e, X_4) | ~k1(X_4)))). % 151.76/133.35 tff(c_613016, plain, (q4(e, a))). % 151.76/133.35 tff(c_609140, plain, (![G_48302, X_2]: (m1(G_48302, X_2, X_2) | ~q0(G_48302, X_2) | ~s0(X_2) | ~p0(X_2, c) | ~r0(G_48302)))). % 151.76/133.35 tff(c_612866, plain, (![E_57239]: (q4(e, E_57239) | ~n1(E_57239, e, e)))). % 151.76/133.35 tff(c_612983, plain, (q4(e, b))). % 151.76/133.35 tff(c_612912, plain, (q4(b, a))). % 151.76/133.35 tff(c_612830, plain, (![E_57239]: (q4(b, E_57239) | ~n1(E_57239, b, b)))). % 151.76/133.35 tff(c_596684, plain, (![G_56547, H_38]: (~m1(G_56547, a, H_38) | m1(H_38, a, a) | ~q0(a, G_56547) | ~r0(G_56547)))). % 151.76/133.35 tff(c_612598, plain, (![J_57233]: (n4(J_57233, c) | ~p0(J_57233, c) | ~k0(J_57233)))). % 151.76/133.35 tff(c_612599, plain, (~l2(c, d))). % 151.76/133.35 tff(c_612593, plain, (![J_57028]: (p3(J_57028, c, c) | ~p0(J_57028, c) | ~k0(J_57028)))). % 151.76/133.35 tff(c_611524, plain, (![A_57190]: (q3(c, A_57190) | ~n0(c, A_57190) | ~l2(c, A_57190) | ~l0(A_57190) | ~k1(A_57190)))). % 151.76/133.35 tff(c_612508, plain, (![I_57228]: (k3(b, b, I_57228) | ~q0(I_57228, b) | ~l0(I_57228)))). % 151.76/133.35 tff(c_611113, plain, (![I_49, J_50]: (m1(I_49, J_50, J_50) | ~q0(I_49, J_50) | ~r0(J_50) | ~k0(J_50) | ~l0(I_49)))). % 151.76/133.35 tff(c_611898, plain, (![E_56573]: (q3(E_56573, E_56573) | ~r0(E_56573) | ~n0(E_56573, a) | ~k0(E_56573)))). % 151.76/133.35 tff(c_611904, plain, (![E_56583]: (q3(E_56583, E_56583) | ~r0(E_56583) | ~l2(E_56583, d) | ~k1(E_56583)))). % 151.76/133.35 tff(c_611907, plain, (![Y_56462, D_56461]: (q3(Y_56462, Y_56462) | ~r0(Y_56462) | ~n0(Y_56462, D_56461) | ~k0(D_56461)))). % 151.76/133.35 tff(c_611893, plain, (![X_56879]: (q3(X_56879, X_56879) | ~r0(X_56879) | ~n0(e, X_56879) | ~k1(X_56879)))). % 151.76/133.35 tff(c_611897, plain, (![E_56573]: (q3(E_56573, E_56573) | ~r0(E_56573) | ~n0(E_56573, c) | ~k0(E_56573)))). % 151.76/133.35 tff(c_611940, plain, (![H_53257]: (q3(H_53257, H_53257) | ~r0(H_53257) | ~l1(H_53257, e)))). % 151.76/133.35 tff(c_612033, plain, (![X_57217, A_57218]: (n4(X_57217, A_57218) | ~r0(A_57218)))). % 151.76/133.35 tff(c_611988, plain, (![X_57212, A_428]: (p3(X_57212, A_428, A_428) | ~r0(A_428)))). % 151.76/133.35 tff(c_612021, plain, (![X_57215]: (n4(X_57215, b)))). % 151.76/133.35 tff(c_611979, plain, (![X_57212]: (p3(X_57212, b, b)))). % 151.76/133.35 tff(c_612002, plain, (![X_57213]: (n4(X_57213, e)))). % 151.76/133.35 tff(c_611975, plain, (![X_57212]: (p3(X_57212, e, e)))). % 151.76/133.35 tff(c_611725, plain, (![X_57195, G_57196]: (~q3(X_57195, G_57196) | q3(G_57196, G_57196) | ~r0(G_57196)))). % 151.76/133.35 tff(c_611794, plain, (![G_57202, X_57203]: (m5(G_57202, X_57203) | ~r0(G_57202)))). % 151.76/133.35 tff(c_611778, plain, (![G_57199, X_57198]: (p4(G_57199, G_57199, X_57198) | ~r0(G_57199)))). % 151.76/133.35 tff(c_611734, plain, (![G_57196, X_57195]: (k3(G_57196, X_57195, G_57196) | ~r0(G_57196)))). % 151.76/133.35 tff(c_611733, plain, (![X_57195, G_57196]: (r3(X_57195, G_57196, X_57195) | ~r0(G_57196)))). % 151.76/133.35 tff(c_611728, plain, (![X_57195]: (m3(X_57195, e, e)))). % 151.76/133.35 tff(c_611626, plain, (![X_56994, G_57194]: (p2(X_56994, G_57194, G_57194) | ~r0(G_57194)))). % 151.76/133.35 tff(c_610199, plain, (![A_14]: (~n0(c, A_14) | q3(A_14, c) | ~l2(c, A_14) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.35 tff(c_611452, plain, (![E_57188]: (n4(e, E_57188)))). % 151.76/133.35 tff(c_611443, plain, (![D_57184, E_57185]: (~k2(D_57184, E_57185) | p3(e, D_57184, E_57185)))). % 151.76/133.35 tff(c_596922, plain, (![D_435, E_436, F_56567]: (~k2(D_435, E_436) | p3(F_56567, D_435, E_436) | ~n1(d, F_56567, F_56567) | ~k0(F_56567)))). % 151.76/133.35 tff(c_609555, plain, (![I_57101, I_57102]: (p1(I_57101, I_57102, I_57101) | ~m0(I_57101, I_57102, b) | ~m0(b, I_57101, c)))). % 151.76/133.35 tff(c_611252, plain, (![G_57174, X_57175]: (q1(G_57174, G_57174, X_57175) | ~q0(G_57174, X_57175) | ~r0(X_57175) | ~r0(G_57174)))). % 151.76/133.35 tff(c_611247, plain, (![G_57174]: (k3(b, b, G_57174) | ~q0(G_57174, b) | ~r0(G_57174)))). % 151.76/133.35 tff(c_611101, plain, (![G_48302, X_2]: (m1(G_48302, X_2, X_2) | ~q0(G_48302, X_2) | ~r0(X_2) | ~r0(G_48302)))). % 151.76/133.35 tff(c_570522, plain, (![F_54353, G_48302, H_54804]: (~m1(F_54353, G_48302, H_54804) | m1(H_54804, G_48302, G_48302) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.35 tff(c_609260, plain, (![I_57095, I_57096]: (p1(I_57095, I_57096, I_57095) | ~m0(I_57095, I_57096, e) | ~m0(e, I_57095, d)))). % 151.76/133.35 tff(c_610845, plain, (~m0(e, a, d))). % 151.76/133.35 tff(c_608098, plain, (![Y_56462, D_56461]: (q3(Y_56462, Y_56462) | ~m0(e, D_56461, d) | ~n0(Y_56462, D_56461) | ~k0(D_56461)))). % 151.76/133.35 tff(c_598470, plain, (![G_48302, F_54353]: (m1(G_48302, a, a) | ~m0(a, a, F_54353) | ~q0(F_54353, G_48302) | ~r0(G_48302)))). % 151.76/133.35 tff(c_610664, plain, (![X_57159]: (p4(b, b, X_57159) | ~p0(X_57159, b)))). % 151.76/133.35 tff(c_610613, plain, (![X_57155]: (r3(X_57155, b, X_57155) | ~p0(X_57155, b)))). % 151.76/133.35 tff(c_610614, plain, (![X_57155]: (k3(b, X_57155, b) | ~p0(X_57155, b)))). % 151.76/133.35 tff(c_610562, plain, (![X_57125]: (~p0(X_57125, b) | p2(X_57125, b, b)))). % 151.76/133.35 tff(c_602210, plain, (![D_435, E_436, E_56815]: (~k2(D_435, E_436) | p3(E_56815, D_435, E_436) | ~n1(d, E_56815, c) | ~p1(E_56815, E_56815, c) | ~l2(E_56815, d) | ~k1(E_56815)))). % 151.76/133.35 tff(c_610308, plain, (~l2(c, a))). % 151.76/133.35 tff(c_610225, plain, (![X_57134]: (m5(e, X_57134) | ~p0(X_57134, e)))). % 151.76/133.35 tff(c_610158, plain, (![X_57130]: (p4(e, e, X_57130) | ~p0(X_57130, e)))). % 151.76/133.35 tff(c_602211, plain, (![E_56815, D_56814]: (~n0(E_56815, D_56814) | q3(D_56814, E_56815) | ~n1(D_56814, E_56815, c) | ~p1(E_56815, E_56815, c) | ~l2(E_56815, D_56814) | ~k1(E_56815)))). % 151.76/133.35 tff(c_610125, plain, (![X_57128]: (k3(e, X_57128, e) | ~p0(X_57128, e)))). % 151.76/133.35 tff(c_610124, plain, (![X_57128]: (r3(X_57128, e, X_57128) | ~p0(X_57128, e)))). % 151.76/133.35 tff(c_610065, plain, (![X_57125]: (~p0(X_57125, e) | p2(X_57125, e, e)))). % 151.76/133.35 tff(c_610023, plain, (~m0(e, a, a))). % 151.76/133.35 tff(c_608886, plain, (![I_57087, I_57088]: (p1(I_57087, I_57088, I_57087) | ~m0(I_57087, I_57088, d) | ~m0(d, I_57087, c)))). % 151.76/133.35 tff(c_609319, plain, (![H_57098]: (q1(H_57098, H_57098, a) | ~q0(c, H_57098) | ~s0(H_57098) | ~p0(H_57098, c)))). % 151.76/133.35 tff(c_599300, plain, (![Y_56462, D_56461]: (q3(Y_56462, Y_56462) | ~m0(e, D_56461, a) | ~n0(Y_56462, D_56461) | ~k0(D_56461)))). % 151.76/133.35 tff(c_609848, plain, (![X_57118]: (m5(e, X_57118) | ~n1(e, X_57118, a) | ~p0(X_57118, a)))). % 151.76/133.35 tff(c_609827, plain, (![X_57116]: (p4(e, e, X_57116) | ~n1(e, X_57116, a) | ~p0(X_57116, a)))). % 151.76/133.35 tff(c_609794, plain, (![X_57114]: (k3(e, X_57114, e) | ~n1(e, X_57114, a) | ~p0(X_57114, a)))). % 151.76/133.35 tff(c_609793, plain, (![X_57114]: (r3(X_57114, e, X_57114) | ~n1(e, X_57114, a) | ~p0(X_57114, a)))). % 151.76/133.35 tff(c_609704, plain, (![X_56994]: (p2(X_56994, e, e) | ~n1(e, X_56994, a) | ~p0(X_56994, a)))). % 151.76/133.35 tff(c_609623, plain, (![X_57107, A_57108]: (n4(X_57107, A_57108) | ~k0(X_57107) | ~l0(A_57108)))). % 151.76/133.35 tff(c_609618, plain, (![X_57106, A_428]: (p3(X_57106, A_428, A_428) | ~k0(X_57106) | ~l0(A_428)))). % 151.76/133.35 tff(c_609559, plain, (~m0(b, e, c))). % 151.76/133.35 tff(c_606790, plain, (![I_56996, I_56997, I_155]: (~m0(I_56996, I_56997, b) | p1(I_56997, I_155, I_56996) | ~m0(b, I_56996, c)))). % 151.76/133.35 tff(c_606028, plain, (![I_56967, I_56968]: (p1(I_56967, I_56968, I_56967) | ~m0(I_56967, I_56968, d) | ~m0(d, I_56967, d)))). % 151.76/133.36 tff(c_597801, plain, (![H_56609]: (m1(H_56609, a, a) | ~q0(c, H_56609) | ~s0(H_56609) | ~p0(H_56609, c)))). % 151.76/133.36 tff(c_606895, plain, (![I_56998, I_56999, I_155]: (~m0(I_56998, I_56999, e) | p1(I_56999, I_155, I_56998) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_597810, plain, (![F_56608, H_56609, H_38]: (~m1(F_56608, H_56609, H_38) | m1(H_38, H_56609, H_56609) | ~q0(F_56608, H_56609) | ~s0(H_56609) | ~p0(H_56609, c)))). % 151.76/133.36 tff(c_603962, plain, (![I_56886, I_56887]: (p1(I_56886, I_56887, I_56886) | ~m0(I_56886, I_56887, b) | ~m0(b, I_56886, b)))). % 151.76/133.36 tff(c_602966, plain, (![I_56848, I_56849, I_155]: (~m0(I_56848, I_56849, d) | p1(I_56849, I_155, I_56848) | ~m0(d, I_56848, c)))). % 151.76/133.36 tff(c_600482, plain, (![H_56753, A_504, G_56751]: (~r2(H_56753) | ~k2(A_504, H_56753) | r3(G_56751, A_504, H_56753) | ~r2(G_56751) | ~l2(c, G_56751) | ~s2(H_56753)))). % 151.76/133.36 tff(c_608594, plain, (![H_53257]: (q3(H_53257, H_53257) | ~s0(H_53257) | ~p0(H_53257, e) | ~l1(H_53257, e)))). % 151.76/133.36 tff(c_608657, plain, (![X_2]: (m5(b, X_2)))). % 151.76/133.36 tff(c_607428, plain, (![Y_56462, D_56461]: (q3(Y_56462, Y_56462) | ~l0(Y_56462) | ~n0(Y_56462, D_56461) | ~k0(D_56461)))). % 151.76/133.36 tff(c_608425, plain, (![X_57066, H_57067]: (~q3(X_57066, H_57067) | q3(H_57067, H_57067) | ~s0(H_57067) | ~p0(H_57067, X_57066)))). % 151.76/133.36 tff(c_608432, plain, (![H_57067, X_57066]: (k3(H_57067, X_57066, H_57067) | ~s0(H_57067) | ~p0(H_57067, X_57066)))). % 151.76/133.36 tff(c_608431, plain, (![X_57066, H_57067]: (r3(X_57066, H_57067, X_57066) | ~s0(H_57067) | ~p0(H_57067, X_57066)))). % 151.76/133.36 tff(c_608328, plain, (![X_56994, H_57065]: (p2(X_56994, H_57065, H_57065) | ~s0(H_57065) | ~p0(H_57065, X_56994)))). % 151.76/133.36 tff(c_608158, plain, (~m0(e, e, d))). % 151.76/133.36 tff(c_608150, plain, (![I_56998]: (k3(e, e, I_56998) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_606885, plain, (![I_56998]: (~q3(e, I_56998) | q3(I_56998, I_56998) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_606898, plain, (![I_56998, I_56999]: (~q3(I_56998, I_56999) | q3(I_56999, I_56999) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_607990, plain, (![I_56998]: (p3(e, I_56998, I_56998) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_598445, plain, (![H_60, F_54353]: (m1(H_60, a, a) | ~m0(a, a, F_54353) | ~q0(F_54353, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.36 tff(c_607972, plain, (![I_56996]: (k3(b, b, I_56996) | ~m0(b, I_56996, c)))). % 151.76/133.36 tff(c_606319, plain, (![X_56879]: (q3(X_56879, X_56879) | ~l0(X_56879) | ~n0(e, X_56879) | ~k1(X_56879)))). % 151.76/133.36 tff(c_607888, plain, (![A_57040]: (n4(b, A_57040) | ~l0(A_57040)))). % 151.76/133.36 tff(c_607883, plain, (![A_428]: (p3(b, A_428, A_428) | ~l0(A_428)))). % 151.76/133.36 tff(c_607740, plain, (![Y_56462]: (q3(Y_56462, Y_56462) | ~l0(Y_56462) | ~n0(Y_56462, b)))). % 151.76/133.36 tff(c_607614, plain, (![I_57031]: (~q3(b, I_57031) | q3(I_57031, I_57031) | ~l0(I_57031)))). % 151.76/133.36 tff(c_607621, plain, (![I_57031]: (k3(I_57031, b, I_57031) | ~l0(I_57031)))). % 151.76/133.36 tff(c_607620, plain, (![I_57031]: (r3(b, I_57031, b) | ~l0(I_57031)))). % 151.76/133.36 tff(c_607528, plain, (![I_56974]: (p2(b, I_56974, I_56974) | ~l0(I_56974)))). % 151.76/133.36 tff(c_607516, plain, (![J_57028]: (r3(J_57028, c, J_57028) | ~p0(J_57028, c) | ~k0(J_57028)))). % 151.76/133.36 tff(c_607519, plain, (~l1(b, c))). % 151.76/133.36 tff(c_606568, plain, (![J_56989]: (~p0(J_56989, c) | p2(J_56989, c, c) | ~k0(J_56989)))). % 151.76/133.36 tff(c_607276, plain, (![X_57019, I_57020]: (~q3(X_57019, I_57020) | q3(I_57020, I_57020) | ~k0(X_57019) | ~l0(I_57020)))). % 151.76/133.36 tff(c_607284, plain, (![I_57020, X_57019]: (k3(I_57020, X_57019, I_57020) | ~k0(X_57019) | ~l0(I_57020)))). % 151.76/133.36 tff(c_607283, plain, (![X_57019, I_57020]: (r3(X_57019, I_57020, X_57019) | ~k0(X_57019) | ~l0(I_57020)))). % 151.76/133.36 tff(c_606749, plain, (![X_56995, I_49]: (p2(X_56995, I_49, I_49) | ~k0(X_56995) | ~l0(I_49)))). % 151.76/133.36 tff(c_606901, plain, (![I_56998]: (p1(e, I_56998, e) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_606902, plain, (![I_56999, I_56998]: (k3(I_56999, I_56998, I_56999) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_601235, plain, (![I_54356, X_2]: (~p1(I_54356, I_54356, X_2) | q2(I_54356, X_2, I_54356) | ~l1(I_54356, X_2) | ~r0(X_2) | ~l0(I_54356)))). % 151.76/133.36 tff(c_606886, plain, (![I_56998]: (k3(I_56998, e, I_56998) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_606883, plain, (![I_56998, I_56999]: (n4(I_56998, I_56999) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_606699, plain, (![I_56993, X_56994, I_155]: (~m0(d, I_56993, X_56994) | p1(I_56993, I_155, d)))). % 151.76/133.36 tff(c_606903, plain, (![I_56998]: (l3(e, I_56998) | ~m0(e, I_56998, d)))). % 151.76/133.36 tff(c_606884, plain, (~m0(e, c, d))). % 151.76/133.36 tff(c_606431, plain, (![I_56983, I_155]: (~m0(e, I_56983, d) | p1(I_56983, I_155, e)))). % 151.76/133.36 tff(c_606414, plain, (![I_56982, I_155]: (~m0(b, I_56982, c) | p1(I_56982, I_155, b)))). % 151.76/133.36 tff(c_606772, plain, (~m0(c, e, a))). % 151.76/133.36 tff(c_606709, plain, (![X_56994]: (p1(X_56994, d, X_56994)))). % 151.76/133.36 tff(c_606508, plain, (![I_56986, X_1]: (p1(d, I_56986, X_1)))). % 151.76/133.36 tff(c_606337, plain, (![Y_56462]: (q3(Y_56462, Y_56462) | ~l0(Y_56462) | ~n0(Y_56462, e)))). % 151.76/133.36 tff(c_606393, plain, (![I_56981]: (p1(a, I_56981, b)))). % 151.76/133.36 tff(c_606383, plain, (![I_56981]: (p1(e, I_56981, d)))). % 151.76/133.36 tff(c_606378, plain, (![I_56981]: (p1(b, I_56981, c)))). % 151.76/133.36 tff(c_594566, plain, (![I_56385, I_56386, I_56384, I_155]: (~m0(I_56385, I_56386, I_56384) | p1(I_56386, I_155, I_56385) | ~m0(I_56384, I_56385, a)))). % 151.76/133.36 tff(c_606223, plain, (![I_56975]: (~q3(e, I_56975) | q3(I_56975, I_56975) | ~l0(I_56975)))). % 151.76/133.36 tff(c_606233, plain, (![I_56975]: (k3(I_56975, e, I_56975) | ~l0(I_56975)))). % 151.76/133.36 tff(c_606149, plain, (![I_56974]: (p2(e, I_56974, I_56974) | ~l0(I_56974)))). % 151.76/133.36 tff(c_606040, plain, (~m0(d, e, d))). % 151.76/133.36 tff(c_594253, plain, (![I_56359, I_56360, I_155]: (~m0(I_56359, I_56360, d) | p1(I_56360, I_155, I_56359) | ~m0(d, I_56359, d)))). % 151.76/133.36 tff(c_604332, plain, (![I_56903, I_56904]: (p1(I_56903, I_56904, I_56903) | ~m0(I_56903, I_56904, d) | ~m0(d, I_56903, e)))). % 151.76/133.36 tff(c_604423, plain, (![H_56909]: (q1(H_56909, H_56909, c) | ~q0(H_56909, c) | ~s0(H_56909) | ~p0(H_56909, c)))). % 151.76/133.36 tff(c_601240, plain, (![D_53281]: (~p1(c, c, D_53281) | q2(c, D_53281, c) | ~l1(c, D_53281) | ~p0(D_53281, D_53281)))). % 151.76/133.36 tff(c_604890, plain, (![H_56923]: (q1(H_56923, H_56923, a) | ~q0(b, H_56923) | ~s0(H_56923) | ~p0(H_56923, c)))). % 151.76/133.36 tff(c_605657, plain, (![H_56957]: (q1(H_56957, H_56957, a) | ~q0(d, H_56957) | ~s0(H_56957) | ~p0(H_56957, c)))). % 151.76/133.36 tff(c_597804, plain, (![H_56609]: (m1(H_56609, a, a) | ~q0(d, H_56609) | ~s0(H_56609) | ~p0(H_56609, c)))). % 151.76/133.36 tff(c_570572, plain, (![G_53298, F_53299, I_54811]: (~m0(G_53298, F_53299, G_53298) | p1(F_53299, I_54811, G_53298) | ~k0(G_53298) | ~m1(F_53299, G_53298, b)))). % 151.76/133.36 tff(c_605220, plain, (![D_55692]: (q4(D_55692, c) | ~k1(D_55692)))). % 151.76/133.36 tff(c_605196, plain, (q4(b, c))). % 151.76/133.36 tff(c_605177, plain, (q4(e, c))). % 151.76/133.36 tff(c_600483, plain, (![G_56751, A_56752]: (p4(G_56751, A_56752, A_56752) | ~r2(G_56751) | ~k2(A_56752, G_56751) | ~l2(c, G_56751) | ~s2(A_56752)))). % 151.76/133.36 tff(c_605163, plain, (q4(a, c))). % 151.76/133.36 tff(c_604986, plain, (![B_132]: (p3(e, B_132, B_132) | ~r2(B_132) | ~p0(e, B_132)))). % 151.76/133.36 tff(c_604980, plain, (![D_120]: (p3(e, D_120, D_120) | ~r2(D_120) | ~n0(d, D_120)))). % 151.76/133.36 tff(c_598085, plain, (![B_426, C_427]: (p3(e, B_426, B_426) | ~p1(B_426, C_427, e) | ~k3(B_426, C_427, B_426) | ~r2(C_427)))). % 151.76/133.36 tff(c_597800, plain, (![H_56609]: (m1(H_56609, a, a) | ~q0(b, H_56609) | ~s0(H_56609) | ~p0(H_56609, c)))). % 151.76/133.36 tff(c_597282, plain, (![D_56590, E_56591]: (n4(D_56590, E_56591) | ~r2(E_56591) | ~m2(D_56590) | ~k0(E_56591) | ~n0(d, D_56590)))). % 151.76/133.36 tff(c_603738, plain, (![I_56880, I_56881]: (p1(I_56880, I_56881, I_56880) | ~m0(I_56880, I_56881, b) | ~m0(b, I_56880, a)))). % 151.76/133.36 tff(c_603537, plain, (![E_56573, A_14]: (~n0(E_56573, A_14) | q3(A_14, E_56573) | ~k0(E_56573) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.36 tff(c_601241, plain, (![D_53281]: (~p1(b, b, D_53281) | q2(b, D_53281, b) | ~l1(b, D_53281) | ~p0(D_53281, D_53281)))). % 151.76/133.36 tff(c_604631, plain, (![H_56914]: (q1(H_56914, H_56914, a) | ~q0(a, H_56914) | ~s0(H_56914) | ~p0(H_56914, c)))). % 151.76/133.36 tff(c_597808, plain, (![H_56609]: (m1(H_56609, a, a) | ~q0(a, H_56609) | ~s0(H_56609) | ~p0(H_56609, c)))). % 151.76/133.36 tff(c_603138, plain, (![B_56854]: (p1(B_56854, b, B_56854) | ~m0(B_56854, b, b) | ~m0(b, b, B_56854)))). % 151.76/133.36 tff(c_603778, plain, (![X_56883]: (q3(X_56883, X_56883) | ~p0(e, X_56883) | ~n0(e, X_56883) | ~k1(X_56883)))). % 151.76/133.36 tff(c_603779, plain, (![X_56883]: (q3(X_56883, X_56883) | ~n0(d, X_56883) | ~n0(e, X_56883) | ~k1(X_56883)))). % 151.76/133.36 tff(c_604189, plain, (![I_56320]: (s2(I_56320) | ~l1(b, I_56320) | ~l0(I_56320) | ~m0(I_56320, b, a)))). % 151.76/133.36 tff(c_600304, plain, (![H_60]: (m1(H_60, c, c) | ~q0(H_60, c) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.36 tff(c_593017, plain, (![G_56293, X_2, I_54356]: (~l1(G_56293, X_2) | ~l0(G_56293) | n1(X_2, I_54356, I_54356) | ~r0(X_2) | ~l0(I_54356)))). % 151.76/133.36 tff(c_604336, plain, (~m0(d, e, e))). % 151.76/133.36 tff(c_593949, plain, (![I_56345, I_56346, I_155]: (~m0(I_56345, I_56346, d) | p1(I_56346, I_155, I_56345) | ~m0(d, I_56345, e)))). % 151.76/133.36 tff(c_604213, plain, (![C_133]: (s2(C_133) | ~l1(b, C_133) | ~l0(C_133) | ~p0(C_133, b)))). % 151.76/133.36 tff(c_604095, plain, (![D_56900]: (s2(D_56900) | ~p1(b, b, D_56900) | ~l1(b, D_56900) | ~l0(D_56900)))). % 151.76/133.36 tff(c_601245, plain, (![E_99, D_98]: (~p1(E_99, E_99, D_98) | q2(E_99, D_98, E_99) | ~l1(E_99, D_98) | ~l0(D_98)))). % 151.76/133.36 tff(c_603966, plain, (~m0(b, e, b))). % 151.76/133.36 tff(c_599724, plain, (![I_56706, I_56707, I_155]: (~m0(I_56706, I_56707, b) | p1(I_56707, I_155, I_56706) | ~m0(b, I_56706, b)))). % 151.76/133.36 tff(c_603603, plain, (![E_56878]: (~s2(E_56878) | q3(E_56878, c) | ~n0(E_56878, c) | ~k0(E_56878)))). % 151.76/133.36 tff(c_603580, plain, (![E_56877]: (~s2(E_56877) | q3(E_56877, a) | ~n0(E_56877, a) | ~k0(E_56877)))). % 151.76/133.36 tff(c_603777, plain, (~n0(e, c))). % 151.76/133.36 tff(c_603629, plain, (![X_56879]: (q3(e, X_56879) | ~n0(e, X_56879) | ~k1(X_56879)))). % 151.76/133.36 tff(c_603742, plain, (~m0(b, e, a))). % 151.76/133.36 tff(c_603547, plain, (![X_4]: (~n0(e, X_4) | q3(X_4, e) | ~k1(X_4)))). % 151.76/133.36 tff(c_603604, plain, (~n0(b, c))). % 151.76/133.36 tff(c_603539, plain, (![E_56573]: (~n0(E_56573, c) | q3(c, E_56573) | ~k0(E_56573)))). % 151.76/133.36 tff(c_603574, plain, (~n0(e, a))). % 151.76/133.36 tff(c_603538, plain, (![E_56573]: (~n0(E_56573, a) | q3(a, E_56573) | ~k0(E_56573)))). % 151.76/133.36 tff(c_596923, plain, (![F_56567, E_56566]: (~n0(F_56567, E_56566) | q3(E_56566, F_56567) | ~n1(E_56566, F_56567, F_56567) | ~k0(F_56567)))). % 151.76/133.37 tff(c_570574, plain, (![E_121, D_120, I_54811]: (~m0(E_121, D_120, E_121) | p1(D_120, I_54811, E_121) | ~k0(E_121) | ~n0(d, D_120)))). % 151.76/133.37 tff(c_603426, plain, (![D_56814]: (s2(D_56814) | ~n1(D_56814, b, c) | ~l2(b, D_56814)))). % 151.76/133.37 tff(c_603452, plain, (~m0(c, b, c))). % 151.76/133.37 tff(c_603439, plain, (p1(c, b, c))). % 151.76/133.37 tff(c_603291, plain, (![A_428]: (p3(e, A_428, A_428) | ~p1(A_428, e, e)))). % 151.76/133.37 tff(c_593022, plain, (![G_56293, D_53281]: (~l1(G_56293, D_53281) | ~l0(G_56293) | n1(D_53281, c, c) | ~p0(D_53281, D_53281)))). % 151.76/133.37 tff(c_603220, plain, (![I_49]: (p3(e, I_49, I_49) | ~l0(I_49)))). % 151.76/133.37 tff(c_603190, plain, (p3(e, c, c))). % 151.76/133.37 tff(c_600217, plain, (![B_35, I_56738]: (~m0(B_35, b, b) | p1(b, I_56738, B_35) | ~m0(b, b, B_35)))). % 151.76/133.37 tff(c_602981, plain, (![I_56848]: (k3(d, d, I_56848) | ~m0(d, I_56848, c)))). % 151.76/133.37 tff(c_596593, plain, (![G_56540]: (~r0(G_56540) | l3(G_56540, e) | ~n1(e, G_56540, a) | ~p0(G_56540, a)))). % 151.76/133.37 tff(c_602910, plain, (![I_56321, I_155]: (n4(I_56321, I_155) | ~m0(e, I_56321, a)))). % 151.76/133.37 tff(c_602859, plain, (![G_56843, A_56844]: (n4(G_56843, A_56844) | ~p1(G_56843, A_56844, e)))). % 151.76/133.37 tff(c_602793, plain, (![G_56841, A_428]: (p3(G_56841, A_428, A_428) | ~p1(G_56841, A_428, e)))). % 151.76/133.37 tff(c_602854, plain, (~n1(b, d, c))). % 151.76/133.37 tff(c_593023, plain, (![G_56293, D_53281]: (~l1(G_56293, D_53281) | ~l0(G_56293) | n1(D_53281, b, b) | ~p0(D_53281, D_53281)))). % 151.76/133.37 tff(c_599178, plain, (![Y_56678]: (q3(b, Y_56678) | ~p0(Y_56678, Y_56678) | ~s2(Y_56678) | ~n0(Y_56678, b)))). % 151.76/133.37 tff(c_602656, plain, (![I_56834]: (m5(e, I_56834) | ~n1(I_56834, e, e)))). % 151.76/133.37 tff(c_602649, plain, (![I_56833]: (p4(e, e, I_56833) | ~n1(I_56833, e, e)))). % 151.76/133.37 tff(c_602537, plain, (![I_56830]: (r3(I_56830, e, I_56830) | ~n1(I_56830, e, e)))). % 151.76/133.37 tff(c_602538, plain, (![I_56830]: (k3(e, I_56830, e) | ~n1(I_56830, e, e)))). % 151.76/133.37 tff(c_602483, plain, (![I_56319]: (p2(I_56319, e, e) | ~n1(I_56319, e, e)))). % 151.76/133.37 tff(c_595848, plain, (![D_56461]: (q3(b, D_56461) | ~p0(D_56461, D_56461) | ~n0(b, D_56461) | ~k0(D_56461)))). % 151.76/133.37 tff(c_602409, plain, (p4(b, b, a))). % 151.76/133.37 tff(c_602402, plain, (r3(a, b, a))). % 151.76/133.37 tff(c_602371, plain, (p2(a, b, b))). % 151.76/133.37 tff(c_602257, plain, (p2(a, b, a))). % 151.76/133.37 tff(c_597818, plain, (![H_56609]: (p2(a, H_56609, a) | ~q0(H_56609, H_56609) | ~s0(H_56609) | ~p0(H_56609, c)))). % 151.76/133.37 tff(c_595950, plain, (![D_56461]: (q3(c, D_56461) | ~p0(D_56461, D_56461) | ~n0(c, D_56461) | ~k0(D_56461)))). % 151.76/133.37 tff(c_600654, plain, (![H_56757]: (q1(H_56757, H_56757, e) | ~k0(H_56757) | ~s0(H_56757) | ~p0(H_56757, e)))). % 151.76/133.37 tff(c_595604, plain, (![D_331, E_332]: (~n1(D_331, E_332, c) | ~p1(E_332, E_332, c) | q2(E_332, D_331, E_332) | ~l2(E_332, D_331) | ~k1(E_332)))). % 151.76/133.37 tff(c_598329, plain, (![Y_56631]: (~r0(Y_56631) | l3(Y_56631, e) | ~n1(e, Y_56631, a) | ~k0(Y_56631)))). % 151.76/133.37 tff(c_602137, plain, (p2(e, b, b))). % 151.76/133.37 tff(c_602061, plain, (~p0(c, d))). % 151.76/133.37 tff(c_601718, plain, (![X_4]: (m5(e, X_4) | ~k1(X_4)))). % 151.76/133.37 tff(c_601633, plain, (![X_4]: (k3(e, X_4, e) | ~k1(X_4)))). % 151.76/133.37 tff(c_601465, plain, (~p1(c, e, e))). % 151.76/133.37 tff(c_601384, plain, (m5(e, c))). % 151.76/133.37 tff(c_601372, plain, (p4(e, e, c))). % 151.76/133.37 tff(c_601367, plain, (k3(e, c, e))). % 151.76/133.37 tff(c_601366, plain, (r3(c, e, c))). % 151.76/133.37 tff(c_601329, plain, (p2(c, e, e))). % 151.76/133.37 tff(c_601247, plain, (~l1(c, d))). % 151.76/133.37 tff(c_595608, plain, (![G_338, H_339]: (~n1(G_338, H_339, G_338) | ~p1(H_339, H_339, G_338) | q2(H_339, G_338, H_339) | ~l1(H_339, G_338)))). % 151.76/133.37 tff(c_601184, plain, (![D_385, G_56778]: (q4(D_385, G_56778) | ~l1(D_385, G_56778)))). % 151.76/133.37 tff(c_601159, plain, (![G_56778]: (q4(d, G_56778)))). % 151.76/133.37 tff(c_600945, plain, (![G_56773]: (~q3(e, G_56773) | q3(G_56773, G_56773) | ~p1(G_56773, e, e)))). % 151.76/133.37 tff(c_600956, plain, (![G_56773]: (k3(G_56773, e, G_56773) | ~p1(G_56773, e, e)))). % 151.76/133.37 tff(c_600871, plain, (![G_265]: (p2(e, G_265, G_265) | ~p1(G_265, e, e)))). % 151.76/133.37 tff(c_600791, plain, (![D_385, D_56764]: (q4(D_385, D_56764) | ~k0(D_56764)))). % 151.76/133.37 tff(c_594496, plain, (![A_428, C_56380, B_56378, D_56377]: (~q2(A_428, C_56380, B_56378) | ~k3(D_56377, D_56377, B_56378) | q4(B_56378, C_56380)))). % 151.76/133.37 tff(c_596342, plain, (![H_60]: (m1(H_60, e, e) | ~k0(H_60) | ~s0(H_60) | ~p0(H_60, e)))). % 151.76/133.37 tff(c_600558, plain, (![Y_56754]: (r3(d, Y_56754, d)))). % 151.76/133.37 tff(c_600468, plain, (![Y_41576]: (p2(d, Y_41576, Y_41576)))). % 151.76/133.37 tff(c_593454, plain, (![G_477, A_56318, H_478]: (~r2(G_477) | ~k2(A_56318, G_477) | r3(H_478, A_56318, G_477) | ~l2(c, G_477) | ~s2(H_478)))). % 151.76/133.37 tff(c_600364, plain, (![G_56747]: (q1(G_56747, G_56747, c) | ~q0(G_56747, c) | ~r0(G_56747)))). % 151.76/133.37 tff(c_600305, plain, (![G_48302]: (m1(G_48302, c, c) | ~q0(G_48302, c) | ~r0(G_48302)))). % 151.76/133.37 tff(c_570523, plain, (![F_54353, H_54804]: (~m1(F_54353, c, H_54804) | m1(H_54804, c, c) | ~q0(F_54353, c)))). % 151.76/133.37 tff(c_600257, plain, (![I_56706]: (k3(b, b, I_56706) | ~m0(b, I_56706, b)))). % 151.76/133.37 tff(c_600232, plain, (~m0(e, b, b))). % 151.76/133.37 tff(c_600231, plain, (~m0(d, b, b))). % 151.76/133.37 tff(c_570573, plain, (![F_158, G_159, I_54811]: (~m0(F_158, b, G_159) | p1(b, I_54811, F_158) | ~k0(G_159) | ~m1(F_158, G_159, b)))). % 151.76/133.37 tff(c_600148, plain, (![H_56732, X_56733]: (p4(H_56732, X_56733, X_56733) | ~m2(H_56732) | ~l2(d, X_56733)))). % 151.76/133.37 tff(c_600102, plain, (![H_315, X_56727]: (~m2(H_315) | r3(X_56727, X_56727, H_315) | ~l2(d, X_56727)))). % 151.76/133.37 tff(c_600125, plain, (![X_56729]: (p4(b, X_56729, X_56729) | ~l2(d, X_56729)))). % 151.76/133.37 tff(c_600109, plain, (![X_56727]: (r3(X_56727, X_56727, b) | ~l2(d, X_56727)))). % 151.76/133.37 tff(c_600065, plain, (![X_56724, Y_5]: (~l2(d, X_56724) | m3(X_56724, Y_5, X_56724)))). % 151.76/133.37 tff(c_599881, plain, (![A_504]: (~k2(A_504, a) | r3(a, A_504, a)))). % 151.76/133.37 tff(c_599975, plain, (![I_56716]: (k3(a, I_56716, a)))). % 151.76/133.37 tff(c_599974, plain, (![I_56716]: (r3(I_56716, a, I_56716)))). % 151.76/133.37 tff(c_599967, plain, (![I_56716]: (p3(I_56716, a, a)))). % 151.76/133.37 tff(c_599924, plain, (![I_56319]: (p2(I_56319, a, a)))). % 151.76/133.37 tff(c_599793, plain, (q3(a, a))). % 151.76/133.37 tff(c_599684, plain, (![I_56705, I_155]: (~m0(b, I_56705, b) | p1(I_56705, I_155, b)))). % 151.76/133.37 tff(c_599669, plain, (![I_56704]: (p1(b, I_56704, b)))). % 151.76/133.37 tff(c_570579, plain, (![D_120, E_121, I_54811]: (~m0(D_120, D_120, E_121) | p1(D_120, I_54811, D_120) | ~k0(E_121) | ~n0(d, D_120)))). % 151.76/133.37 tff(c_599629, plain, (~q3(e, a))). % 151.76/133.37 tff(c_599112, plain, (![C_56674]: (~r0(C_56674) | l3(C_56674, e) | ~n1(e, C_56674, a) | ~s0(C_56674)))). % 151.76/133.37 tff(c_570575, plain, (![C_133, B_132, I_54811]: (~m0(C_133, B_132, C_133) | p1(B_132, I_54811, C_133) | ~p0(C_133, B_132)))). % 151.76/133.37 tff(c_597809, plain, (![H_56609, F_56608]: (k2(H_56609, a) | ~q0(F_56608, H_56609) | ~s0(H_56609) | ~p0(H_56609, c)))). % 151.76/133.37 tff(c_599389, plain, (~m0(e, e, a))). % 151.76/133.37 tff(c_594570, plain, (![I_56386]: (~q3(e, I_56386) | q3(I_56386, I_56386) | ~m0(e, I_56386, a)))). % 151.76/133.37 tff(c_599365, plain, (~s0(a))). % 151.76/133.37 tff(c_599346, plain, (![I_56384, I_56385]: (k3(I_56384, I_56384, I_56385) | ~m0(I_56384, I_56385, a)))). % 151.76/133.37 tff(c_599340, plain, (~m0(e, b, a))). % 151.76/133.37 tff(c_594569, plain, (![I_56385, I_56386]: (~q3(I_56385, I_56386) | q3(I_56386, I_56386) | ~m0(e, I_56385, a)))). % 151.76/133.37 tff(c_599204, plain, (![I_56321]: (p3(e, I_56321, I_56321) | ~m0(e, I_56321, a)))). % 151.76/133.37 tff(c_583815, plain, (![E_189, F_55679, E_55678]: (~l0(E_189) | ~k0(F_55679) | q1(E_189, E_55678, E_55678) | ~k1(E_55678) | ~q0(F_55679, E_55678)))). % 151.76/133.37 tff(c_599174, plain, (~n0(a, e))). % 151.76/133.37 tff(c_595655, plain, (![Y_56470, D_56471]: (~s2(Y_56470) | q3(Y_56470, D_56471) | ~n0(Y_56470, D_56471) | ~k0(D_56471)))). % 151.76/133.37 tff(c_599134, plain, (![I_56359]: (k3(d, d, I_56359) | ~m0(d, I_56359, d)))). % 151.76/133.37 tff(c_570309, plain, (![B_54786, C_54787]: (n4(B_54786, C_54787) | ~r2(C_54787) | ~m2(B_54786) | ~p0(C_54787, B_54786)))). % 151.76/133.37 tff(c_599003, plain, (![C_56666]: (~n1(e, C_56666, a) | p2(C_56666, e, C_56666) | ~s0(C_56666)))). % 151.76/133.37 tff(c_599025, plain, (~m2(a))). % 151.76/133.37 tff(c_599016, plain, (![H_56668, H_56669]: (p4(H_56668, H_56669, H_56669) | ~m2(H_56668) | ~r2(H_56669)))). % 151.76/133.37 tff(c_598913, plain, (![H_56656, H_420]: (~m2(H_56656) | r3(H_420, H_420, H_56656) | ~r2(H_420)))). % 151.76/133.37 tff(c_598958, plain, (![E_55662, C_202]: (~l0(E_55662) | q1(E_55662, C_202, C_202) | ~s0(C_202)))). % 151.76/133.37 tff(c_598928, plain, (![H_56657]: (p4(H_56657, b, b) | ~m2(H_56657)))). % 151.76/133.37 tff(c_598972, plain, (![H_56660]: (p4(H_56660, d, d) | ~m2(H_56660)))). % 151.76/133.37 tff(c_598945, plain, (![H_56658]: (p4(H_56658, a, a) | ~m2(H_56658)))). % 151.76/133.37 tff(c_598906, plain, (![H_56656]: (~m2(H_56656) | r3(d, d, H_56656)))). % 151.76/133.37 tff(c_598905, plain, (![H_56656]: (~m2(H_56656) | r3(a, a, H_56656)))). % 151.76/133.37 tff(c_598904, plain, (![H_56656]: (~m2(H_56656) | r3(b, b, H_56656)))). % 151.76/133.37 tff(c_593833, plain, (![J_56340, H_56341, H_315]: (~m3(J_56340, b, H_56341) | ~m2(H_315) | r3(H_56341, H_56341, H_315)))). % 151.76/133.37 tff(c_598776, plain, (~m2(c))). % 151.76/133.37 tff(c_593302, plain, (![J_56304, H_38]: (~m1(e, J_56304, H_38) | m1(H_38, J_56304, J_56304) | ~k0(J_56304)))). % 151.76/133.37 tff(c_598715, plain, (![I_56345]: (k3(d, d, I_56345) | ~m0(d, I_56345, e)))). % 151.76/133.37 tff(c_598598, plain, (![D_120]: (p3(e, D_120, D_120) | ~m2(D_120) | ~n0(d, D_120)))). % 151.76/133.37 tff(c_598587, plain, (![F_158]: (p3(e, F_158, F_158) | ~m1(F_158, e, b)))). % 151.76/133.37 tff(c_598601, plain, (![B_132]: (p3(e, B_132, B_132) | ~m2(B_132) | ~p0(e, B_132)))). % 151.76/133.38 tff(c_598074, plain, (![A_428, A_55671]: (p3(e, A_428, A_428) | ~p1(A_428, A_55671, e) | ~m2(A_55671)))). % 151.76/133.38 tff(c_598488, plain, (![Y_5]: (m1(Y_5, d, d)))). % 151.76/133.38 tff(c_570527, plain, (![B_35, C_36, H_54804]: (~m1(B_35, C_36, H_54804) | m1(H_54804, C_36, C_36) | ~m0(C_36, C_36, B_35)))). % 151.76/133.38 tff(c_593390, plain, (![Y_56310]: (~n1(e, Y_56310, a) | p2(Y_56310, e, Y_56310) | ~k0(Y_56310)))). % 151.76/133.38 tff(c_596720, plain, (![F_56549]: (p4(b, b, F_56549) | ~p2(b, F_56549, b) | ~r0(F_56549)))). % 151.76/133.38 tff(c_598088, plain, (![A_428]: (p3(e, A_428, A_428) | ~p1(A_428, A_428, e)))). % 151.76/133.38 tff(c_598099, plain, (~m0(e, c, a))). % 151.76/133.38 tff(c_598095, plain, (~p1(c, d, e))). % 151.76/133.38 tff(c_598094, plain, (~m2(e))). % 151.76/133.38 tff(c_598077, plain, (p3(e, d, d))). % 151.76/133.38 tff(c_563963, plain, (![G_265, C_54369, H_266]: (~m3(G_265, C_54369, H_266) | p3(e, G_265, G_265) | ~p1(G_265, H_266, e)))). % 151.76/133.38 tff(c_597982, plain, (~r2(b))). % 151.76/133.38 tff(c_597977, plain, (k3(b, b, a))). % 151.76/133.38 tff(c_597897, plain, (~l2(e, d))). % 151.76/133.38 tff(c_597179, plain, (![E_56587]: (~s2(E_56587) | q3(E_56587, c) | ~l2(E_56587, d) | ~k1(E_56587)))). % 151.76/133.38 tff(c_597834, plain, (![Y_5]: (m3(b, Y_5, b)))). % 151.76/133.38 tff(c_597819, plain, (~p0(d, c))). % 151.76/133.38 tff(c_563798, plain, (![F_54353, H_60]: (~q0(F_54353, H_60) | m1(F_54353, a, H_60) | ~s0(H_60) | ~p0(H_60, c)))). % 151.76/133.38 tff(c_597745, plain, (![G_56606]: (q1(G_56606, G_56606, a) | ~q0(c, G_56606) | ~r0(G_56606)))). % 151.76/133.38 tff(c_597317, plain, (![G_48302]: (m1(G_48302, a, a) | ~q0(c, G_48302) | ~r0(G_48302)))). % 151.76/133.38 tff(c_597682, plain, (![G_56603]: (q1(G_56603, G_56603, a) | ~q0(b, G_56603) | ~r0(G_56603)))). % 151.76/133.38 tff(c_597574, plain, (![G_56601]: (q1(G_56601, G_56601, a) | ~q0(d, G_56601) | ~r0(G_56601)))). % 151.76/133.38 tff(c_597386, plain, (![G_48302]: (m1(G_48302, a, a) | ~q0(b, G_48302) | ~r0(G_48302)))). % 151.76/133.38 tff(c_597638, plain, (~l1(a, e))). % 151.76/133.38 tff(c_597628, plain, (~q3(a, e))). % 151.76/133.38 tff(c_597578, plain, (![B_81]: (~q3(B_81, e) | q3(e, B_81) | ~m1(b, B_81, e)))). % 151.76/133.38 tff(c_597232, plain, (![G_48302]: (m1(G_48302, a, a) | ~q0(d, G_48302) | ~r0(G_48302)))). % 151.76/133.38 tff(c_597430, plain, (![H_38]: (~m1(e, b, H_38) | m1(H_38, b, b)))). % 151.76/133.38 tff(c_597399, plain, (m1(e, b, b))). % 151.76/133.38 tff(c_570524, plain, (![B_53955, H_54804]: (~m1(b, B_53955, H_54804) | m1(H_54804, B_53955, B_53955) | ~k1(B_53955)))). % 151.76/133.38 tff(c_597272, plain, (![H_38]: (~m1(c, a, H_38) | m1(H_38, a, a)))). % 151.76/133.38 tff(c_570087, plain, (![D_120, E_121]: (~m2(D_120) | k3(E_121, E_121, D_120) | ~k0(E_121) | ~n0(d, D_120)))). % 151.76/133.38 tff(c_597277, plain, (~l2(b, d))). % 151.76/133.38 tff(c_597273, plain, (q1(c, c, a))). % 151.76/133.38 tff(c_597235, plain, (m1(c, a, a))). % 151.76/133.38 tff(c_570525, plain, (![B_53955, H_54804]: (~m1(d, B_53955, H_54804) | m1(H_54804, B_53955, B_53955) | ~k1(B_53955)))). % 151.76/133.38 tff(c_597133, plain, (![E_56583]: (q3(c, E_56583) | ~l2(E_56583, d) | ~k1(E_56583)))). % 151.76/133.38 tff(c_597149, plain, (![A_56584]: (s2(A_56584) | ~l0(A_56584) | ~k1(A_56584)))). % 151.76/133.38 tff(c_597005, plain, (![A_14, E_56573]: (n1(A_14, E_56573, E_56573) | ~l0(A_14) | ~k1(A_14)))). % 151.76/133.38 tff(c_548690, plain, (![D_331, E_332]: (~n0(D_331, c) | q3(c, E_332) | ~l2(E_332, D_331) | ~k1(E_332)))). % 151.76/133.38 tff(c_597117, plain, (p4(b, a, a))). % 151.76/133.38 tff(c_597059, plain, (r3(a, a, b))). % 151.76/133.38 tff(c_596977, plain, (![Y_5]: (m3(a, Y_5, a)))). % 151.76/133.38 tff(c_597011, plain, (![E_56573]: (n1(a, E_56573, E_56573)))). % 151.76/133.38 tff(c_597008, plain, (![E_56573]: (n1(c, E_56573, E_56573)))). % 151.76/133.38 tff(c_593027, plain, (![G_56293, D_98, E_99]: (~l1(G_56293, D_98) | ~l0(G_56293) | n1(D_98, E_99, E_99) | ~l0(D_98)))). % 151.76/133.38 tff(c_596929, plain, (![E_56566]: (s2(E_56566) | ~n1(E_56566, b, b)))). % 151.76/133.38 tff(c_595603, plain, (![E_320, F_321]: (~n1(E_320, F_321, F_321) | q2(F_321, E_320, F_321) | ~k0(F_321)))). % 151.76/133.38 tff(c_595668, plain, (![Y_56470]: (q3(Y_56470, Y_56470) | ~n0(d, Y_56470) | ~n0(Y_56470, e)))). % 151.76/133.38 tff(c_596863, plain, (~p0(e, b))). % 151.76/133.38 tff(c_570582, plain, (![B_132, C_133, I_54811]: (~m0(B_132, B_132, C_133) | p1(B_132, I_54811, B_132) | ~p0(C_133, B_132)))). % 151.76/133.38 tff(c_595665, plain, (![Y_56470]: (q3(Y_56470, Y_56470) | ~p0(e, Y_56470) | ~n0(Y_56470, e)))). % 151.76/133.38 tff(c_596685, plain, (![G_56547]: (q1(G_56547, G_56547, a) | ~q0(a, G_56547) | ~r0(G_56547)))). % 151.76/133.38 tff(c_596795, plain, (![X_2]: (~k1(X_2) | k2(b, X_2)))). % 151.76/133.38 tff(c_596030, plain, (![I_61, H_60]: (~k1(I_61) | k2(H_60, I_61) | ~s0(H_60) | ~p0(H_60, I_61)))). % 151.76/133.38 tff(c_596773, plain, (![H_56552]: (p4(b, H_56552, H_56552) | ~r2(H_56552)))). % 151.76/133.38 tff(c_596743, plain, (![H_420]: (r3(H_420, H_420, b) | ~r2(H_420)))). % 151.76/133.38 tff(c_596749, plain, (p4(b, d, d))). % 151.76/133.38 tff(c_596736, plain, (r3(d, d, b))). % 151.76/133.38 tff(c_596711, plain, (![J_496, H_494]: (~m3(J_496, b, H_494) | r3(H_494, H_494, b)))). % 151.76/133.38 tff(c_583867, plain, (![F_499]: (~p2(b, F_499, b) | ~r0(F_499) | r3(F_499, b, F_499)))). % 151.76/133.38 tff(c_593759, plain, (![H_48307]: (k3(b, H_48307, b) | ~s0(H_48307) | ~p0(H_48307, a)))). % 151.76/133.38 tff(c_593245, plain, (![G_48302]: (m1(G_48302, a, a) | ~q0(a, G_48302) | ~r0(G_48302)))). % 151.76/133.38 tff(c_593539, plain, (![H_48307]: (k3(d, H_48307, d) | ~s0(H_48307) | ~p0(H_48307, c)))). % 151.76/133.38 tff(c_593087, plain, (![H_48307]: (k3(e, H_48307, e) | ~s0(H_48307) | ~p0(H_48307, b)))). % 151.76/133.38 tff(c_593635, plain, (![H_48307]: (k3(d, H_48307, d) | ~s0(H_48307) | ~p0(H_48307, e)))). % 151.76/133.38 tff(c_596453, plain, (![I_56538]: (q1(I_56538, I_56538, e) | ~k0(I_56538) | ~l0(I_56538)))). % 151.76/133.38 tff(c_596414, plain, (![G_56537]: (q1(G_56537, G_56537, e) | ~k0(G_56537) | ~r0(G_56537)))). % 151.76/133.38 tff(c_563893, plain, (![G_180]: (~n1(e, G_180, a) | p2(G_180, e, G_180) | ~p0(G_180, a)))). % 151.76/133.38 tff(c_596372, plain, (![H_38]: (~m1(b, e, H_38) | m1(H_38, e, e)))). % 151.76/133.38 tff(c_596351, plain, (![I_49]: (m1(I_49, e, e) | ~k0(I_49) | ~l0(I_49)))). % 151.76/133.38 tff(c_596343, plain, (![G_48302]: (m1(G_48302, e, e) | ~k0(G_48302) | ~r0(G_48302)))). % 151.76/133.38 tff(c_596373, plain, (q1(b, b, e))). % 151.76/133.38 tff(c_596336, plain, (m1(b, e, e))). % 151.76/133.38 tff(c_570528, plain, (![J_49528, H_54804]: (~m1(J_49528, e, H_54804) | m1(H_54804, e, e) | ~k0(J_49528)))). % 151.76/133.38 tff(c_596291, plain, (~q0(e, a))). % 151.76/133.38 tff(c_583818, plain, (![F_55679]: (~n1(e, F_55679, a) | p2(F_55679, e, a) | ~q0(F_55679, a)))). % 151.76/133.38 tff(c_596248, plain, (![I_561, C_56531]: (n5(I_561, C_56531)))). % 151.76/133.38 tff(c_593455, plain, (![H_315, A_56318]: (~r2(H_315) | ~k2(A_56318, H_315) | r3(H_315, A_56318, H_315)))). % 151.76/133.38 tff(c_593705, plain, (![H_48307]: (k3(d, H_48307, d) | ~s0(H_48307) | ~p0(H_48307, b)))). % 151.76/133.38 tff(c_596122, plain, (![H_60]: (k2(H_60, e) | ~s0(H_60) | ~p0(H_60, e)))). % 151.76/133.38 tff(c_596130, plain, (![I_49]: (k2(I_49, e) | ~l0(I_49)))). % 151.76/133.38 tff(c_596123, plain, (![G_48302]: (k2(G_48302, e) | ~r0(G_48302)))). % 151.76/133.38 tff(c_596052, plain, (![E_239, C_237]: (~m1(E_239, e, C_237) | k2(C_237, e)))). % 151.76/133.38 tff(c_596031, plain, (![X_2, G_48302]: (~k1(X_2) | k2(G_48302, X_2) | ~r0(G_48302)))). % 151.76/133.38 tff(c_596029, plain, (![J_49528]: (~k1(J_49528) | k2(e, J_49528) | ~k0(J_49528)))). % 151.76/133.38 tff(c_596026, plain, (k2(b, e))). % 151.76/133.38 tff(c_596043, plain, (![J_50, I_49]: (~k1(J_50) | k2(I_49, J_50) | ~k0(J_50) | ~l0(I_49)))). % 151.76/133.38 tff(c_583311, plain, (![A_205, E_55645, C_55646]: (~k1(A_205) | ~m1(E_55645, A_205, C_55646) | k2(C_55646, A_205)))). % 151.76/133.38 tff(c_571562, plain, (![D_53281]: (~q3(D_53281, c) | q3(c, D_53281) | ~p0(D_53281, D_53281)))). % 151.76/133.38 tff(c_595913, plain, (![G_56293]: (~l1(G_56293, d) | ~l0(G_56293)))). % 151.76/133.38 tff(c_595911, plain, (~l0(e))). % 151.76/133.38 tff(c_595874, plain, (![G_56293]: (~l1(G_56293, e) | ~l0(G_56293)))). % 151.76/133.38 tff(c_595873, plain, (![G_56293]: (~l1(G_56293, b) | ~l0(G_56293)))). % 151.76/133.38 tff(c_571565, plain, (![D_53281]: (~q3(D_53281, b) | q3(b, D_53281) | ~p0(D_53281, D_53281)))). % 151.76/133.38 tff(c_595811, plain, (![Y_56494, Y_5]: (m4(Y_56494, Y_5)))). % 151.76/133.38 tff(c_595709, plain, (![I_327, Y_56478]: (~s2(I_327) | s3(I_327, Y_56478)))). % 151.76/133.38 tff(c_595795, plain, (~p2(d, b, c))). % 151.76/133.38 tff(c_595786, plain, (p4(e, a, a))). % 151.76/133.38 tff(c_595778, plain, (r3(a, a, e))). % 151.76/133.38 tff(c_595719, plain, (![Y_56478]: (s3(c, Y_56478)))). % 151.76/133.38 tff(c_526, plain, (![B_408, J_406, C_409, A_407]: (~s2(B_408) | ~m0(J_406, C_409, C_409) | ~l2(C_409, J_406) | ~m0(B_408, B_408, A_407) | m3(J_406, A_407, J_406)))). % 151.76/133.38 tff(c_595661, plain, (~n0(c, b))). % 151.76/133.38 tff(c_595658, plain, (~n0(c, e))). % 151.76/133.38 tff(c_595579, plain, (![Y_56462, D_56461]: (~n0(Y_56462, D_56461) | q3(D_56461, Y_56462) | ~k0(D_56461)))). % 151.76/133.38 tff(c_440, plain, (![G_329, H_330, F_328]: (~q2(G_329, H_330, F_328) | ~n1(G_329, F_328, H_330) | ~p1(F_328, F_328, H_330) | q2(F_328, G_329, F_328)))). % 151.76/133.38 tff(c_595582, plain, (![D_56461]: (s2(D_56461) | ~k0(D_56461)))). % 151.76/133.38 tff(c_595403, plain, (![D_56446, Y_5]: (~k0(D_56446) | q2(Y_5, D_56446, Y_5)))). % 151.76/133.38 tff(c_595414, plain, (![B_606, Y_56450]: (p5(B_606, Y_56450, Y_56450)))). % 151.76/133.38 tff(c_595435, plain, (r3(b, c, b))). % 151.76/133.38 tff(c_595379, plain, (p2(b, c, c))). % 151.76/133.38 tff(c_595261, plain, (s3(a, e))). % 151.76/133.38 tff(c_595224, plain, (s3(b, a))). % 151.76/133.38 tff(c_595191, plain, (s3(b, e))). % 151.76/133.39 tff(c_595167, plain, (s3(d, c))). % 151.76/133.39 tff(c_380, plain, (![C_278, D_279, E_280]: (~p2(C_278, D_279, C_278) | ~p0(C_278, D_279) | ~n1(E_280, D_279, E_280) | p2(C_278, D_279, D_279)))). % 151.76/133.39 tff(c_595078, plain, (s3(e, c))). % 151.76/133.39 tff(c_595079, plain, (s2(e))). % 151.76/133.39 tff(c_368, plain, (![C_267, D_268, E_269, F_270]: (~p2(C_267, D_268, C_267) | ~l1(E_269, F_270) | ~p1(C_267, E_269, F_270) | p2(C_267, D_268, D_268)))). % 151.76/133.39 tff(c_594572, plain, (![I_56384, I_56385]: (p1(I_56384, I_56385, I_56384) | ~m0(I_56384, I_56385, a)))). % 152.10/133.39 tff(c_594573, plain, (![I_56386, I_56385]: (k3(I_56386, I_56385, I_56386) | ~m0(e, I_56385, a)))). % 152.10/133.39 tff(c_594575, plain, (![I_56386]: (k3(I_56386, e, I_56386) | ~m0(e, I_56386, a)))). % 152.10/133.39 tff(c_594574, plain, (![I_56385]: (l3(e, I_56385) | ~m0(e, I_56385, a)))). % 152.10/133.39 tff(c_593480, plain, (![I_56320, I_56321, I_155]: (~m0(I_56320, I_56321, a) | p1(I_56321, I_155, I_56320)))). % 152.10/133.39 tff(c_594501, plain, (![G_56382]: (n4(c, G_56382) | ~r2(G_56382)))). % 152.10/133.39 tff(c_594460, plain, (![G_56376]: (k3(G_56376, G_56376, c)))). % 152.10/133.39 tff(c_594383, plain, (![I_371, G_56366, G_372]: (~q0(I_371, G_56366) | k3(G_372, G_372, G_56366)))). % 152.10/133.39 tff(c_594437, plain, (![G_56372]: (n4(b, G_56372) | ~r2(G_56372)))). % 152.10/133.39 tff(c_594417, plain, (![G_56365]: (k3(G_56365, G_56365, b)))). % 152.10/133.39 tff(c_594394, plain, (![F_199, H_201, E_198]: (~q0(F_199, F_199) | ~p0(H_201, E_198) | ~l0(E_198) | q1(E_198, F_199, E_198)))). % 152.10/133.39 tff(c_594401, plain, (![G_56365]: (k3(G_56365, G_56365, e)))). % 152.10/133.39 tff(c_594338, plain, (![G_56365]: (k3(G_56365, G_56365, d)))). % 152.10/133.39 tff(c_594030, plain, (![F_158]: (k3(e, F_158, e) | ~m1(F_158, e, b)))). % 152.10/133.39 tff(c_593870, plain, (![F_158]: (k3(d, F_158, d) | ~m1(F_158, e, b)))). % 152.10/133.39 tff(c_593542, plain, (![G_265]: (k3(d, G_265, d) | ~p1(G_265, c, e)))). % 152.10/133.39 tff(c_593167, plain, (![H_53257]: (~s2(H_53257) | q3(H_53257, e) | ~l1(H_53257, e)))). % 152.10/133.39 tff(c_593094, plain, (![G_265]: (k3(e, G_265, e) | ~p1(G_265, b, e)))). % 152.10/133.39 tff(c_593762, plain, (![G_265]: (k3(b, G_265, b) | ~p1(G_265, a, e)))). % 152.10/133.39 tff(c_593640, plain, (![G_265]: (k3(d, G_265, d) | ~p1(G_265, e, e)))). % 152.10/133.39 tff(c_593712, plain, (![G_265]: (k3(d, G_265, d) | ~p1(G_265, b, e)))). % 152.10/133.39 tff(c_593804, plain, (~n0(c, c))). % 152.10/133.39 tff(c_593802, plain, (~n0(b, b))). % 152.10/133.39 tff(c_593760, plain, (![G_48305]: (k3(b, G_48305, b) | ~r0(G_48305)))). % 152.10/133.39 tff(c_593757, plain, (k3(b, a, b))). % 152.10/133.39 tff(c_593756, plain, (k3(b, c, b))). % 152.10/133.39 tff(c_593785, plain, (![C_27, B_26]: (~p0(C_27, B_26) | ~n0(C_27, C_27) | m1(B_26, B_26, c)))). % 152.10/133.39 tff(c_593778, plain, (q2(b, c, d))). % 152.10/133.39 tff(c_593777, plain, (m3(c, b, d))). % 152.10/133.39 tff(c_584023, plain, (![B_55706, A_55707]: (~p2(B_55706, A_55707, a) | k3(b, A_55707, b)))). % 152.10/133.39 tff(c_584028, plain, (![B_55706, A_55707]: (~p2(B_55706, A_55707, b) | k3(d, A_55707, d)))). % 152.10/133.39 tff(c_593639, plain, (![I_49]: (k3(d, I_49, d) | ~l0(I_49)))). % 152.10/133.39 tff(c_593654, plain, (~l2(a, d))). % 152.10/133.39 tff(c_593648, plain, (~q2(d, c, a))). % 152.10/133.39 tff(c_593626, plain, (k3(d, b, d))). % 152.10/133.39 tff(c_584022, plain, (![B_55706, A_55707]: (~p2(B_55706, A_55707, e) | k3(d, A_55707, d)))). % 152.10/133.39 tff(c_593561, plain, (k2(b, a))). % 152.10/133.39 tff(c_583742, plain, (![H_60]: (k2(H_60, a) | ~s0(H_60) | ~p0(H_60, a)))). % 152.10/133.39 tff(c_593540, plain, (![G_48305]: (k3(d, G_48305, d) | ~r0(G_48305)))). % 152.10/133.39 tff(c_593543, plain, (k3(d, c, d))). % 152.10/133.39 tff(c_593537, plain, (k3(d, a, d))). % 152.10/133.39 tff(c_584025, plain, (![B_55706, A_55707]: (~p2(B_55706, A_55707, c) | k3(d, A_55707, d)))). % 152.10/133.39 tff(c_593497, plain, (![I_56322]: (n4(I_56322, a)))). % 152.10/133.39 tff(c_593489, plain, (![I_56320]: (k3(a, a, I_56320)))). % 152.10/133.39 tff(c_593466, plain, (![I_56319, I_155]: (p1(I_56319, I_155, a)))). % 152.10/133.39 tff(c_620, plain, (![B_505, J_503, A_504]: (~r3(B_505, J_503, J_503) | ~r2(B_505) | ~k2(A_504, B_505) | r3(J_503, A_504, B_505)))). % 152.10/133.39 tff(c_570581, plain, (![X_2, I_54811]: (~m0(X_2, X_2, X_2) | p1(X_2, I_54811, X_2)))). % 152.10/133.39 tff(c_583635, plain, (![E_55662, Y_5]: (~l0(E_55662) | ~k0(Y_5) | q1(E_55662, Y_5, Y_5)))). % 152.10/133.39 tff(c_593378, plain, (~q3(c, a))). % 152.10/133.39 tff(c_593358, plain, (![Y_41576]: (k3(c, Y_41576, c)))). % 152.10/133.39 tff(c_593314, plain, (~q0(a, c))). % 152.10/133.39 tff(c_593306, plain, (![J_56304]: (q1(e, e, J_56304) | ~k0(J_56304)))). % 152.10/133.39 tff(c_593255, plain, (![J_49528]: (m1(e, J_49528, J_49528) | ~k0(J_49528)))). % 152.10/133.39 tff(c_570534, plain, (![Y_5, H_54804]: (~m1(Y_5, Y_5, H_54804) | m1(H_54804, Y_5, Y_5)))). % 152.10/133.39 tff(c_583378, plain, (![H_60]: (k2(H_60, c) | ~s0(H_60) | ~p0(H_60, c)))). % 152.10/133.39 tff(c_583436, plain, (![H_60]: (k2(H_60, b) | ~s0(H_60) | ~p0(H_60, b)))). % 152.10/133.39 tff(c_593160, plain, (q3(d, e))). % 152.10/133.39 tff(c_593176, plain, (q3(b, e))). % 152.10/133.39 tff(c_584108, plain, (![X_55711, Y_55710]: (~q3(X_55711, Y_55710) | ~s2(Y_55710) | q3(Y_55710, X_55711)))). % 152.10/133.39 tff(c_584026, plain, (![B_55706, A_55707]: (~p2(B_55706, A_55707, b) | k3(e, A_55707, e)))). % 152.10/133.39 tff(c_184, plain, (![E_106, F_107, G_108]: (~n1(E_106, F_107, E_106) | ~l1(G_108, E_106) | ~l0(G_108) | n1(E_106, F_107, F_107)))). % 152.10/133.39 tff(c_584027, plain, (![B_55706, A_55707]: (~p2(B_55706, A_55707, e) | k3(e, A_55707, e)))). % 152.10/133.39 tff(c_592856, plain, (q3(b, a))). % 152.10/133.39 tff(c_592855, plain, (q3(a, b))). % 152.10/133.39 tff(c_587956, plain, (s2(a))). % 152.10/133.39 tff(c_584305, plain, (k4(e))). % 152.10/133.39 tff(c_584089, plain, (![Y_5, X_4]: (n1(Y_5, Y_5, X_4)))). % 152.10/133.39 tff(c_570531, plain, (![H_54804]: (~m1(d, e, H_54804) | m1(H_54804, e, e)))). % 152.10/133.39 tff(c_584003, plain, (![J_346, C_349, B_348, A_347]: (~n0(J_346, C_349) | ~p2(B_348, A_347, C_349) | k3(J_346, A_347, J_346)))). % 152.10/133.39 tff(c_583912, plain, (![D_55692]: (l2(D_55692, e)))). % 152.10/133.39 tff(c_583871, plain, (![E_245, D_244]: (~n0(e, E_245) | l2(D_244, E_245)))). % 152.10/133.39 tff(c_583873, plain, (![F_605, E_604]: (~s4(F_605) | p5(E_604, E_604, F_605)))). % 152.10/133.39 tff(c_583840, plain, (![Y_5]: (l2(Y_5, Y_5)))). % 152.10/133.39 tff(c_583690, plain, (![E_209, F_210]: (~k1(E_209) | ~q0(F_210, E_209) | q1(E_209, E_209, F_210)))). % 152.10/133.39 tff(c_583792, plain, (![A_55674]: (p3(d, A_55674, A_55674)))). % 152.10/133.39 tff(c_583778, plain, (![A_55671, A_428]: (~m2(A_55671) | m3(A_428, A_55671, A_55671)))). % 152.10/133.39 tff(c_583743, plain, (![G_48302]: (k2(G_48302, a) | ~r0(G_48302)))). % 152.10/133.39 tff(c_583307, plain, (![E_55645, C_55646]: (~m1(E_55645, a, C_55646) | k2(C_55646, a)))). % 152.10/133.39 tff(c_583624, plain, (![E_55662]: (~l0(E_55662) | q1(E_55662, d, d)))). % 152.10/133.39 tff(c_583642, plain, (![E_55662]: (~l0(E_55662) | q1(E_55662, e, e)))). % 152.10/133.39 tff(c_583639, plain, (![E_55662]: (~l0(E_55662) | q1(E_55662, b, b)))). % 152.10/133.39 tff(c_274, plain, (![F_190, G_191, E_189]: (~q1(F_190, F_190, G_191) | ~l0(E_189) | ~k0(G_191) | q1(E_189, F_190, F_190)))). % 152.10/133.39 tff(c_583565, plain, (![Y_5]: (k2(Y_5, d)))). % 152.10/133.39 tff(c_583464, plain, (![I_537, H_536]: (~r3(I_537, I_537, H_536) | p4(H_536, I_537, I_537)))). % 152.10/133.39 tff(c_583437, plain, (![G_48302]: (k2(G_48302, b) | ~r0(G_48302)))). % 152.10/133.39 tff(c_583443, plain, (![I_49]: (k2(I_49, b) | ~l0(I_49)))). % 152.10/133.39 tff(c_583435, plain, (k2(e, b))). % 152.10/133.39 tff(c_583310, plain, (![E_55645, C_55646]: (~m1(E_55645, b, C_55646) | k2(C_55646, b)))). % 152.10/133.39 tff(c_583379, plain, (![G_48302]: (k2(G_48302, c) | ~r0(G_48302)))). % 152.10/133.39 tff(c_583314, plain, (![E_55645, C_55646]: (~m1(E_55645, c, C_55646) | k2(C_55646, c)))). % 152.10/133.39 tff(c_583335, plain, (~l1(c, e))). % 152.10/133.39 tff(c_583331, plain, (~q3(e, c))). % 152.10/133.39 tff(c_583320, plain, (q3(c, c))). % 152.10/133.39 tff(c_583293, plain, (q3(d, c))). % 152.10/133.39 tff(c_583292, plain, (q3(c, d))). % 152.10/133.39 tff(c_330, plain, (![F_240, D_238, E_239, C_237]: (~k2(F_240, D_238) | ~k1(F_240) | ~m1(E_239, D_238, C_237) | k2(C_237, D_238)))). % 152.10/133.39 tff(c_575680, plain, (~q3(b, c))). % 152.10/133.39 tff(c_575675, plain, (q3(b, d))). % 152.10/133.39 tff(c_575674, plain, (q3(d, b))). % 152.10/133.39 tff(c_571501, plain, (p3(e, b, e))). % 152.10/133.39 tff(c_570740, plain, (~m0(d, b, e))). % 152.10/133.39 tff(c_570634, plain, (![I_54813]: (~q3(d, I_54813) | q3(I_54813, I_54813)))). % 152.10/133.39 tff(c_570643, plain, (![I_54813]: (r3(e, I_54813, e)))). % 152.10/133.39 tff(c_570641, plain, (![I_54813]: (k3(I_54813, d, I_54813)))). % 152.10/133.39 tff(c_570642, plain, (l3(e, d))). % 152.10/133.39 tff(c_240, plain, (![J_156, H_154, A_157, I_155]: (~p1(J_156, H_154, A_157) | ~m0(J_156, H_154, A_157) | p1(H_154, I_155, J_156)))). % 152.10/133.39 tff(c_570480, plain, (![X_1]: (~p0(a, X_1) | l1(X_1, a)))). % 152.10/133.39 tff(c_570543, plain, (![X_4]: (l1(d, X_4)))). % 152.10/133.39 tff(c_570492, plain, (~p0(a, a))). % 152.10/133.39 tff(c_108, plain, (![J_40, A_41, I_39, H_38]: (~m1(J_40, A_41, I_39) | ~m1(J_40, I_39, H_38) | m1(H_38, I_39, I_39)))). % 152.10/133.39 tff(c_570491, plain, (~p0(c, e))). % 152.10/133.39 tff(c_570489, plain, (~p0(e, e))). % 152.10/133.39 tff(c_570483, plain, (l1(b, e))). % 152.10/133.39 tff(c_570448, plain, (![D_11, C_10, E_12]: (~m0(D_11, C_10, E_12) | ~p0(E_12, C_10) | l1(C_10, D_11)))). % 152.10/133.39 tff(c_570443, plain, (~l1(b, d))). % 152.10/133.39 tff(c_170, plain, (![J_94, I_93]: (~l1(J_94, d) | ~r0(I_93) | ~p0(J_94, J_94) | n1(I_93, d, J_94)))). % 152.10/133.39 tff(c_570358, plain, (![B_35]: (k3(b, b, B_35) | ~m0(b, b, B_35)))). % 152.10/133.39 tff(c_570079, plain, (![G_159, F_158]: (k3(G_159, G_159, F_158) | ~k0(G_159) | ~m1(F_158, G_159, b)))). % 152.10/133.39 tff(c_570093, plain, (![B_132, C_133]: (~m2(B_132) | k3(C_133, C_133, B_132) | ~p0(C_133, B_132)))). % 152.10/133.39 tff(c_568792, plain, (![D_366, C_365, B_364]: (~m2(D_366) | ~p1(C_365, D_366, B_364) | k3(B_364, B_364, C_365)))). % 152.10/133.39 tff(c_568742, plain, (~n1(e, d, a))). % 152.10/133.39 tff(c_568710, plain, (n4(b, c))). % 152.10/133.39 tff(c_568705, plain, (p3(b, c, c))). % 152.10/133.39 tff(c_563911, plain, (~n1(e, a, a))). % 152.10/133.39 tff(c_578, plain, (![A_456, B_457, D_459, C_458]: (~p2(A_456, B_457, D_459) | ~m3(B_457, C_458, D_459) | p3(A_456, B_457, B_457)))). % 152.10/133.39 tff(c_563910, plain, (~n0(d, d))). % 152.10/133.39 tff(c_563842, plain, (![H_54351]: (~m1(a, H_54351, d) | ~n0(H_54351, d)))). % 152.10/133.39 tff(c_388, plain, (![G_287, F_286]: (~q1(a, G_287, F_286) | ~n1(e, F_286, a) | p2(F_286, e, G_287)))). % 152.10/133.39 tff(c_563799, plain, (![F_54353, G_48302]: (~q0(F_54353, G_48302) | m1(F_54353, a, G_48302) | ~r0(G_48302)))). % 152.10/133.39 tff(c_563817, plain, (![X_2, I_54356]: (~r0(X_2) | ~l0(I_54356) | n1(X_2, I_54356, X_2)))). % 152.10/133.39 tff(c_563820, plain, (![I_54356]: (~l0(I_54356) | n1(b, I_54356, b)))). % 152.10/133.39 tff(c_563811, plain, (~q0(c, c))). % 152.10/133.39 tff(c_563800, plain, (![F_54353]: (~q0(F_54353, c) | m1(F_54353, a, c)))). % 152.10/133.39 tff(c_804, plain, (![G_52, F_51]: (~m1(G_52, c, G_52) | ~q0(F_51, G_52) | m1(F_51, a, G_52)))). % 152.10/133.39 tff(c_563778, plain, (~p0(d, d))). % 152.10/133.39 tff(c_563757, plain, (![H_54348, E_54347]: (n4(H_54348, E_54347) | ~l1(H_54348, d)))). % 152.10/133.39 tff(c_563739, plain, (![D_54339, E_54340, H_339]: (~k2(D_54339, E_54340) | p3(H_339, D_54339, E_54340) | ~l1(H_339, d)))). % 152.10/133.39 tff(c_563748, plain, (![E_54344]: (n4(d, E_54344)))). % 152.10/133.39 tff(c_563738, plain, (![D_54339, E_54340]: (~k2(D_54339, E_54340) | p3(d, D_54339, E_54340)))). % 152.10/133.39 tff(c_558, plain, (![D_435, E_436, F_437, C_434]: (~k2(D_435, E_436) | ~q2(F_437, d, C_434) | p3(C_434, D_435, E_436)))). % 152.10/133.39 tff(c_563720, plain, (p2(b, c, a))). % 152.10/133.39 tff(c_563715, plain, (k2(c, a))). % 152.10/133.39 tff(c_556686, plain, (![F_53299]: (~q3(e, F_53299) | q3(F_53299, F_53299) | ~m1(F_53299, e, b)))). % 152.10/133.39 tff(c_558141, plain, (![B_53958]: (q1(b, b, B_53958) | ~k1(B_53958)))). % 152.10/133.39 tff(c_558128, plain, (![B_53957]: (q1(d, d, B_53957) | ~k1(B_53957)))). % 152.10/133.39 tff(c_558148, plain, (~p0(d, b))). % 152.10/133.39 tff(c_558117, plain, (![B_53955]: (~k1(B_53955) | m1(b, B_53955, B_53955)))). % 152.10/133.39 tff(c_558116, plain, (![B_53955]: (~k1(B_53955) | m1(d, B_53955, B_53955)))). % 152.10/133.39 tff(c_558119, plain, (~s0(c))). % 152.10/133.39 tff(c_558104, plain, (![X_2]: (~r0(X_2) | l3(X_2, b)))). % 152.10/133.39 tff(c_558109, plain, (![A_67, B_68]: (~q0(A_67, A_67) | ~k1(B_68) | m1(A_67, B_68, B_68)))). % 152.10/133.39 tff(c_497056, plain, (![I_49560, H_49561]: (~r0(I_49560) | l3(I_49560, H_49561) | ~s0(H_49561) | ~p0(H_49561, I_49560)))). % 152.10/133.39 tff(c_558085, plain, (q3(e, d))). % 152.10/133.39 tff(c_558084, plain, (q3(d, d))). % 152.10/133.39 tff(c_549420, plain, (![G_265, H_266]: (~q3(G_265, H_266) | q3(H_266, H_266) | ~p1(G_265, H_266, e)))). % 152.10/133.39 tff(c_556648, plain, (![D_53849]: (l2(D_53849, b)))). % 152.10/133.39 tff(c_556604, plain, (![F_53845]: (k3(F_53845, e, F_53845) | ~m1(F_53845, e, b)))). % 152.10/133.39 tff(c_549211, plain, (![G_53298, F_53299]: (p1(G_53298, F_53299, G_53298) | ~k0(G_53298) | ~m1(F_53299, G_53298, b)))). % 152.10/133.39 tff(c_556519, plain, (![H_53257]: (q3(H_53257, H_53257) | ~p0(e, H_53257) | ~l1(H_53257, e)))). % 152.10/133.39 tff(c_556494, plain, (![H_53257]: (q3(H_53257, H_53257) | ~n0(d, H_53257) | ~l1(H_53257, e)))). % 152.10/133.39 tff(c_556475, plain, (![B_132]: (~q3(e, B_132) | q3(B_132, B_132) | ~p0(e, B_132)))). % 152.10/133.39 tff(c_556471, plain, (![D_120]: (~q3(e, D_120) | q3(D_120, D_120) | ~n0(d, D_120)))). % 152.10/133.39 tff(c_549429, plain, (![H_266]: (~q3(e, H_266) | q3(H_266, H_266) | ~p1(H_266, H_266, e)))). % 152.10/133.39 tff(c_556433, plain, (![G_353, F_352]: (n4(G_353, F_352) | ~r2(F_352) | ~k2(G_353, F_352)))). % 152.10/133.39 tff(c_556247, plain, (![J_438, B_440]: (n4(J_438, B_440) | ~k3(B_440, B_440, J_438) | ~r2(B_440)))). % 152.10/133.39 tff(c_556387, plain, (![Y_5]: (q1(Y_5, Y_5, d)))). % 152.10/133.39 tff(c_556386, plain, (q1(e, e, b))). % 152.10/133.39 tff(c_556315, plain, (![B_35, C_36]: (q1(B_35, B_35, C_36) | ~m0(C_36, C_36, B_35)))). % 152.10/133.39 tff(c_556376, plain, (~l1(b, a))). % 152.10/133.39 tff(c_556269, plain, (![B_53823]: (~r0(B_53823) | l3(B_53823, a)))). % 152.10/133.39 tff(c_556373, plain, (m5(e, a))). % 152.10/133.39 tff(c_556367, plain, (p4(e, e, a))). % 152.10/133.39 tff(c_556291, plain, (r3(a, e, a))). % 152.10/133.39 tff(c_556292, plain, (k3(e, a, e))). % 152.10/133.39 tff(c_556323, plain, (q1(d, d, e))). % 152.10/133.39 tff(c_556234, plain, (![H_216, I_217]: (~m1(H_216, I_217, I_217) | q1(H_216, H_216, I_217)))). % 152.10/133.39 tff(c_556268, plain, (p2(a, e, e))). % 152.10/133.39 tff(c_556221, plain, (![X_53816]: (q1(X_53816, c, X_53816)))). % 152.10/133.39 tff(c_556228, plain, (![B_261]: (p2(B_261, a, B_261)))). % 152.10/133.39 tff(c_556238, plain, (![J_525, A_526]: (~p3(J_525, A_526, A_526) | n4(J_525, A_526)))). % 152.10/133.39 tff(c_556220, plain, (![X_53816]: (q1(X_53816, d, X_53816)))). % 152.10/133.39 tff(c_556219, plain, (![X_53816]: (q1(X_53816, a, X_53816)))). % 152.10/133.39 tff(c_556218, plain, (![X_53816]: (q1(X_53816, e, X_53816)))). % 152.10/133.39 tff(c_556217, plain, (![X_53816]: (q1(X_53816, b, X_53816)))). % 152.10/133.39 tff(c_556197, plain, (![B_53812, A_53813, X_2]: (~n0(B_53812, A_53813) | q1(X_2, A_53813, X_2)))). % 152.10/133.39 tff(c_556187, plain, (![X_2]: (r4(X_2)))). % 152.10/133.39 tff(c_556154, plain, (![I_609, I_53800]: (p5(I_609, I_53800, I_609)))). % 152.10/133.39 tff(c_556150, plain, (![I_561]: (q4(I_561, I_561)))). % 152.10/133.39 tff(c_549504, plain, (~l0(d))). % 152.10/133.39 tff(c_549500, plain, (~r2(d))). % 152.10/133.40 tff(c_549214, plain, (![F_53299]: (k3(b, F_53299, b) | ~m1(F_53299, e, b)))). % 152.10/133.40 tff(c_560, plain, (![A_439, B_440, J_438]: (~k3(A_439, B_440, J_438) | ~r2(A_439) | p3(J_438, A_439, B_440)))). % 152.10/133.40 tff(c_588, plain, (![F_468, E_467]: (~q3(F_468, E_467) | ~p2(F_468, E_467, E_467) | q3(E_467, E_467)))). % 152.10/133.40 tff(c_549363, plain, (p4(e, e, b))). % 152.10/133.40 tff(c_549358, plain, (k3(e, b, e))). % 152.10/133.40 tff(c_549357, plain, (r3(b, e, b))). % 152.10/133.40 tff(c_549335, plain, (p2(b, e, e))). % 152.10/133.40 tff(c_549342, plain, (![B_555]: (~m3(B_555, c, a) | p4(c, c, B_555)))). % 152.10/133.40 tff(c_549338, plain, (l3(e, b))). % 152.10/133.40 tff(c_549267, plain, (p2(e, b, e))). % 152.10/133.40 tff(c_549259, plain, (m1(b, e, b))). % 152.10/133.40 tff(c_549258, plain, (k3(b, e, b))). % 152.10/133.40 tff(c_242, plain, (![G_159, F_158]: (~k0(G_159) | ~m1(F_158, G_159, b) | p1(F_158, b, G_159)))). % 152.10/133.40 tff(c_549163, plain, (![H_442]: (s4(H_442) | ~k1(H_442)))). % 152.10/133.40 tff(c_549151, plain, (![A_14]: (~k1(A_14) | l1(A_14, A_14)))). % 152.10/133.40 tff(c_549126, plain, (![X_53287]: (~r0(X_53287) | l3(X_53287, e) | ~k1(X_53287)))). % 152.10/133.40 tff(c_549108, plain, (![X_4]: (~k1(X_4) | n1(X_4, e, e)))). % 152.10/133.40 tff(c_549119, plain, (~r0(a))). % 152.10/133.40 tff(c_549107, plain, (n1(b, e, e))). % 152.10/133.40 tff(c_549089, plain, (![D_53281]: (~p0(D_53281, D_53281) | n1(D_53281, c, D_53281)))). % 152.10/133.40 tff(c_549088, plain, (![D_53281]: (~p0(D_53281, D_53281) | n1(D_53281, b, D_53281)))). % 152.10/133.40 tff(c_549082, plain, (![I_472]: (~r2(I_472) | q3(I_472, I_472)))). % 152.10/133.40 tff(c_164, plain, (![E_88, F_89, D_87]: (~p0(E_88, F_89) | ~p0(D_87, D_87) | n1(D_87, E_88, D_87)))). % 152.10/133.40 tff(c_549070, plain, (![I_275, H_274]: (~m0(I_275, H_274, d) | p2(H_274, H_274, d)))). % 152.10/133.40 tff(c_548992, plain, (![E_121, D_120]: (p1(E_121, D_120, E_121) | ~k0(E_121) | ~n0(d, D_120)))). % 152.10/133.40 tff(c_548996, plain, (![C_133, B_132]: (p1(C_133, B_132, C_133) | ~p0(C_133, B_132)))). % 152.10/133.40 tff(c_549007, plain, (k3(d, e, d))). % 152.10/133.40 tff(c_548980, plain, (![I_135, A_137, H_134]: (~p1(I_135, A_137, H_134) | p1(H_134, I_135, H_134)))). % 152.10/133.40 tff(c_548975, plain, (m5(e, b))). % 152.10/133.40 tff(c_548967, plain, (~k3(c, e, b))). % 152.10/133.40 tff(c_548933, plain, (![C_36, B_35]: (~m0(C_36, C_36, B_35) | m1(B_35, C_36, C_36)))). % 152.10/133.40 tff(c_548924, plain, (m5(e, e))). % 152.10/133.40 tff(c_548906, plain, (~m0(a, e, c))). % 152.10/133.40 tff(c_548878, plain, (![H_53257]: (q3(e, H_53257) | ~l1(H_53257, e)))). % 152.10/133.40 tff(c_548692, plain, (![G_338, H_339]: (~n0(G_338, G_338) | q3(G_338, H_339) | ~l1(H_339, G_338)))). % 152.10/133.40 tff(c_548804, plain, (![H_53249, G_53248]: (k3(H_53249, G_53248, H_53249) | ~p1(G_53248, H_53249, e)))). % 152.10/133.40 tff(c_548803, plain, (![G_53248, H_53249]: (r3(G_53248, H_53249, G_53248) | ~p1(G_53248, H_53249, e)))). % 152.10/133.40 tff(c_548847, plain, (~k0(d))). % 152.10/133.40 tff(c_548846, plain, (~k0(a))). % 152.10/133.40 tff(c_548836, plain, (q3(e, e))). % 152.10/133.40 tff(c_548824, plain, (q3(b, b))). % 152.10/133.40 tff(c_548748, plain, (![E_53237, F_53236]: (~n0(E_53237, F_53236) | q3(F_53236, F_53236) | ~k0(F_53236)))). % 152.10/133.40 tff(c_548675, plain, (![G_265, H_266]: (p2(G_265, H_266, H_266) | ~p1(G_265, H_266, e)))). % 152.10/133.40 tff(c_548784, plain, (![G_53246]: (m5(e, G_53246) | ~r0(G_53246)))). % 152.10/133.40 tff(c_548768, plain, (![G_53241]: (p4(e, e, G_53241) | ~r0(G_53241)))). % 152.10/133.40 tff(c_548775, plain, (![I_53242]: (m5(e, I_53242) | ~l0(I_53242)))). % 152.10/133.40 tff(c_546, plain, (![B_426, C_427]: (~k3(B_426, C_427, B_426) | ~r2(C_427) | m3(B_426, B_426, C_427)))). % 152.10/133.40 tff(c_548758, plain, (![I_53238]: (p4(e, e, I_53238) | ~l0(I_53238)))). % 152.10/133.40 tff(c_548733, plain, (![G_53235]: (r3(G_53235, e, G_53235) | ~r0(G_53235)))). % 152.10/133.40 tff(c_548762, plain, (~p0(a, b))). % 152.10/133.40 tff(c_548734, plain, (![G_53235]: (k3(e, G_53235, e) | ~r0(G_53235)))). % 152.10/133.40 tff(c_548760, plain, (~k0(c))). % 152.10/133.40 tff(c_548712, plain, (![I_53233]: (k3(e, I_53233, e) | ~l0(I_53233)))). % 152.10/133.40 tff(c_548711, plain, (![I_53233]: (r3(I_53233, e, I_53233) | ~l0(I_53233)))). % 152.10/133.40 tff(c_548736, plain, (![F_321, E_320]: (~k0(F_321) | q2(E_320, F_321, F_321)))). % 152.10/133.40 tff(c_548671, plain, (![G_48305]: (p2(G_48305, e, e) | ~r0(G_48305)))). % 152.10/133.40 tff(c_548691, plain, (![I_327]: (~n0(I_327, I_327) | q3(I_327, I_327)))). % 152.10/133.40 tff(c_548674, plain, (![I_49]: (p2(I_49, e, e) | ~l0(I_49)))). % 152.10/133.40 tff(c_586, plain, (![I_466, G_464, H_465]: (~n0(I_466, G_464) | ~q2(I_466, G_464, H_465) | q3(G_464, H_465)))). % 152.10/133.40 tff(c_548645, plain, (![H_283, I_284]: (~p2(e, H_283, I_284) | p2(H_283, I_284, I_284)))). % 152.10/133.40 tff(c_548625, plain, (p4(b, b, e))). % 152.17/133.40 tff(c_548630, plain, (p4(b, b, d))). % 152.17/133.40 tff(c_548598, plain, (![D_331]: (m3(D_331, c, D_331) | ~l2(c, D_331)))). % 152.17/133.40 tff(c_548585, plain, (![J_429]: (~q2(J_429, c, c) | m3(J_429, c, J_429)))). % 152.17/133.40 tff(c_542060, plain, (r3(d, b, c))). % 152.17/133.40 tff(c_497002, plain, (![J_50, I_49]: (~r0(J_50) | l3(J_50, I_49) | ~k0(J_50) | ~l0(I_49)))). % 152.17/133.40 tff(c_497012, plain, (![C_310]: (~r0(C_310) | l3(C_310, e) | ~n1(C_310, e, e)))). % 152.17/133.40 tff(c_482296, plain, (![I_48308, H_48307]: (p2(I_48308, H_48307, I_48308) | ~s0(H_48307) | ~p0(H_48307, I_48308)))). % 152.17/133.40 tff(c_497001, plain, (![X_48306, G_48305]: (~r0(X_48306) | l3(X_48306, G_48305) | ~r0(G_48305)))). % 152.17/133.40 tff(c_497009, plain, (![G_265]: (l3(e, G_265) | ~p1(G_265, e, e)))). % 152.17/133.40 tff(c_497021, plain, (s4(b))). % 152.17/133.40 tff(c_497013, plain, (~r0(d))). % 152.17/133.40 tff(c_497006, plain, (l3(b, e))). % 152.17/133.40 tff(c_506, plain, (![G_391, H_392]: (~p2(G_391, H_392, G_391) | ~r0(G_391) | l3(G_391, H_392)))). % 152.17/133.40 tff(c_496977, plain, (s4(a))). % 152.17/133.40 tff(c_496956, plain, (s4(c))). % 152.17/133.40 tff(c_496952, plain, (s4(d))). % 152.17/133.40 tff(c_496931, plain, (s4(e))). % 152.17/133.40 tff(c_674, plain, (![A_568, C_570, B_569, D_571]: (~l1(A_568, C_570) | ~p3(B_569, C_570, D_571) | s4(A_568)))). % 152.17/133.40 tff(c_286, plain, (![D_203, C_202]: (~p0(D_203, d) | ~s0(C_202) | q1(C_202, C_202, D_203)))). % 152.17/133.40 tff(c_496877, plain, (![J_49528]: (~k0(J_49528) | m1(J_49528, J_49528, e)))). % 152.17/133.40 tff(c_98, plain, (![A_29, J_28]: (~n0(A_29, A_29) | ~k0(J_28) | m1(J_28, J_28, A_29)))). % 152.17/133.40 tff(c_496868, plain, (s2(c))). % 152.17/133.40 tff(c_758, plain, (![E_332, D_331]: (~l2(E_332, D_331) | ~k1(E_332) | q2(D_331, c, E_332)))). % 152.17/133.40 tff(c_538, plain, (![I_421, H_420]: (~k2(c, I_421) | ~r2(H_420) | m3(H_420, I_421, H_420)))). % 152.17/133.40 tff(c_596, plain, (![G_477, H_478]: (~l2(c, G_477) | ~s2(H_478) | r3(G_477, H_478, H_478)))). % 152.17/133.40 tff(c_482292, plain, (![X_48306, G_48305]: (p2(X_48306, G_48305, X_48306) | ~r0(G_48305)))). % 152.17/133.40 tff(c_134, plain, (![H_60, I_61]: (~s0(H_60) | ~p0(H_60, I_61) | m1(H_60, I_61, H_60)))). % 152.17/133.40 tff(c_482287, plain, (![G_48302, X_2]: (~r0(G_48302) | m1(G_48302, X_2, G_48302)))). % 152.17/133.40 tff(c_482280, plain, (l3(d, c))). % 152.17/133.40 tff(c_464996, plain, (![G_344]: (~l0(G_344) | r2(G_344)))). % 152.17/133.40 tff(c_464988, plain, (![D_46801]: (r1(D_46801)))). % 152.17/133.40 tff(c_464976, plain, (![D_46797]: (k3(D_46797, e, D_46797) | ~n0(d, D_46797)))). % 152.17/133.40 tff(c_202, plain, (![E_121, D_120]: (~k0(E_121) | ~n0(d, D_120) | p1(D_120, D_120, E_121)))). % 152.17/133.40 tff(c_464940, plain, (![H_527]: (n4(H_527, H_527)))). % 152.17/133.40 tff(c_398263, plain, (![J_50, I_49]: (p2(J_50, I_49, J_50) | ~k0(J_50) | ~l0(I_49)))). % 152.17/133.40 tff(c_464922, plain, (~r0(c))). % 152.17/133.40 tff(c_464907, plain, (![B_132]: (k3(B_132, e, B_132) | ~p0(e, B_132)))). % 152.17/133.40 tff(c_398293, plain, (![H_41561]: (k3(H_41561, e, H_41561) | ~p1(H_41561, H_41561, e)))). % 152.17/133.40 tff(c_464888, plain, (![B_581]: (~s4(B_581) | m5(B_581, B_581)))). % 152.17/133.40 tff(c_400259, plain, (m1(d, e, e))). % 152.17/133.40 tff(c_650, plain, (![B_534, C_535]: (~k3(B_534, B_534, C_535) | p4(B_534, C_535, B_534)))). % 152.17/133.40 tff(c_398420, plain, (~m0(b, c, e))). % 152.17/133.40 tff(c_398414, plain, (s2(b))). % 152.17/133.40 tff(c_398404, plain, (![H_345]: (~q2(b, H_345, b) | s2(H_345)))). % 152.17/133.40 tff(c_398387, plain, (![Y_41576]: (p2(d, Y_41576, d)))). % 152.17/133.40 tff(c_398383, plain, (p2(b, e, b))). % 152.17/133.40 tff(c_398378, plain, (![Y_5]: (m1(Y_5, d, Y_5)))). % 152.17/133.40 tff(c_398377, plain, (m1(e, b, e))). % 152.17/133.40 tff(c_86, plain, (![C_17, B_16]: (~m0(C_17, C_17, B_16) | m1(B_16, C_17, B_16)))). % 152.17/133.40 tff(c_398347, plain, (![Y_5]: (m1(Y_5, Y_5, Y_5)))). % 152.17/133.40 tff(c_398319, plain, (![H_442]: (p4(H_442, H_442, H_442)))). % 152.17/133.40 tff(c_398312, plain, (![I_327]: (q2(I_327, I_327, I_327)))). % 152.17/133.40 tff(c_802, plain, (![G_265, H_266]: (~p1(G_265, H_266, e) | p2(e, G_265, H_266)))). % 152.17/133.40 tff(c_398247, plain, (![H_41556]: (k5(H_41556)))). % 152.17/133.40 tff(c_428, plain, (![E_319, D_318]: (~m1(E_319, D_318, E_319) | p2(D_318, E_319, D_318)))). % 152.17/133.40 tff(c_398225, plain, (![H_315]: (r3(H_315, H_315, H_315)))). % 152.17/133.40 tff(c_398238, plain, (n1(b, c, b))). % 152.17/133.40 tff(c_398237, plain, (n1(d, c, d))). % 152.17/133.40 tff(c_398236, plain, (n1(e, c, e))). % 152.17/133.40 tff(c_154, plain, (![F_78, E_77]: (~m0(F_78, E_77, c) | n1(E_77, c, E_77)))). % 152.17/133.40 tff(c_610, plain, (![B_491, D_493, C_492]: (~p2(B_491, D_493, C_492) | r3(B_491, C_492, B_491)))). % 152.17/133.40 tff(c_398217, plain, (~m1(c, d, a))). % 152.17/133.40 tff(c_118, plain, (![J_50, I_49]: (~k0(J_50) | ~l0(I_49) | m1(I_49, J_50, I_49)))). % 152.17/133.40 tff(c_397830, plain, (![C_619, D_620]: (~s4(C_619) | r5(C_619, D_620)))). % 152.17/133.40 tff(c_397825, plain, (![H_41482]: (n3(H_41482)))). % 152.17/133.40 tff(c_397805, plain, (![H_315]: (p2(H_315, H_315, H_315)))). % 152.17/133.40 tff(c_397733, plain, (![Y_5]: (q1(Y_5, Y_5, Y_5)))). % 152.17/133.40 tff(c_416, plain, (![C_310]: (~n1(C_310, e, e) | p2(C_310, e, C_310)))). % 152.17/133.40 tff(c_488, plain, (![D_376, C_375]: (~p2(D_376, C_375, C_375) | k3(C_375, D_376, C_375)))). % 152.17/133.40 tff(c_387872, plain, (![D_385]: (k3(D_385, D_385, D_385)))). % 152.17/133.40 tff(c_387880, plain, (![H_442]: (p3(H_442, H_442, H_442)))). % 152.17/133.40 tff(c_387882, plain, (![A_428]: (m3(A_428, A_428, A_428)))). % 152.17/133.40 tff(c_387896, plain, (![I_616]: (q5(I_616, I_616)))). % 152.17/133.40 tff(c_387890, plain, (![H_622]: (s5(H_622)))). % 152.17/133.40 tff(c_387899, plain, (![C_396]: (l3(C_396, C_396)))). % 152.17/133.40 tff(c_387874, plain, (![H_442]: (l4(H_442)))). % 152.17/133.40 tff(c_387865, plain, (![X_40455]: (n2(X_40455)))). % 152.17/133.40 tff(c_387848, plain, (![X_2]: (p1(X_2, X_2, X_2)))). % 152.17/133.40 tff(c_387816, plain, (p4(c, d, c))). % 152.17/133.40 tff(c_330326, plain, (![H_575]: (~k1(H_575) | l5(H_575)))). % 152.17/133.40 tff(c_330336, plain, (m2(d))). % 152.17/133.40 tff(c_249445, plain, (![F_253]: (~s0(F_253) | m2(F_253)))). % 152.17/133.40 tff(c_448, plain, (![H_339, G_338]: (~l1(H_339, G_338) | q2(G_338, G_338, H_339)))). % 152.17/133.40 tff(c_249421, plain, (~l1(c, b))). % 152.17/133.40 tff(c_249413, plain, (p3(b, c, b))). % 152.17/133.40 tff(c_249414, plain, (k2(c, b))). % 152.17/133.40 tff(c_266, plain, (![G_180, F_179]: (~p0(G_180, F_179) | q1(F_179, G_180, G_180)))). % 152.17/133.40 tff(c_214, plain, (![C_133, B_132]: (~p0(C_133, B_132) | p1(B_132, B_132, C_133)))). % 152.17/133.40 tff(c_464, plain, (![G_353, F_352]: (~k2(G_353, F_352) | k3(F_352, F_352, G_353)))). % 152.17/133.40 tff(c_125304, plain, (![A_205]: (k2(A_205, A_205)))). % 152.17/133.40 tff(c_720, plain, (![A_615, J_614]: (~m2(A_615) | ~s4(J_614) | q5(J_614, A_615)))). % 152.17/133.40 tff(c_125245, plain, (![X_3]: (s1(X_3)))). % 152.17/133.40 tff(c_125218, plain, (k4(c))). % 152.17/133.40 tff(c_125209, plain, (q3(e, b))). % 152.17/133.40 tff(c_102174, plain, (r2(c))). % 152.17/133.40 tff(c_101470, plain, (k2(b, c))). % 152.17/133.40 tff(c_51256, plain, (r2(a))). % 152.17/133.40 tff(c_17073, plain, (~s0(e))). % 152.17/133.40 tff(c_822, plain, (![D_98, E_99]: (~l0(D_98) | n1(D_98, E_99, D_98)))). % 152.17/133.40 tff(c_816, plain, (![B_224]: (~s0(B_224) | q1(B_224, b, b)))). % 152.17/133.40 tff(c_17036, plain, (l1(c, c))). % 152.17/133.40 tff(c_17034, plain, (l1(a, a))). % 152.17/133.40 tff(c_17031, plain, (l1(b, b))). % 152.17/133.40 tff(c_80, plain, (![H_9, G_8]: (~n0(H_9, G_8) | l1(G_8, G_8)))). % 152.17/133.40 tff(c_17011, plain, (l1(e, e))). % 152.17/133.40 tff(c_17012, plain, (~l0(b))). % 152.17/133.40 tff(c_684, plain, (![C_580]: (~k4(C_580) | m5(C_580, C_580)))). % 152.17/133.40 tff(c_1218, plain, (~l1(e, c))). % 152.17/133.40 tff(c_1249, plain, (k1(c))). % 152.17/133.40 tff(c_1248, plain, (k1(d))). % 152.17/133.40 tff(c_1247, plain, (k1(a))). % 152.17/133.40 tff(c_1246, plain, (k1(e))). % 152.17/133.40 tff(c_78, plain, (![J_7, I_6]: (~n0(J_7, I_6) | k1(I_6)))). % 152.17/133.40 tff(c_732, plain, (![B_621]: (~k4(B_621) | r5(B_621, B_621)))). % 152.17/133.40 tff(c_772, plain, (![A_205]: (q1(e, A_205, A_205)))). % 152.17/133.40 tff(c_32, plain, (m0(c, b, a))). % 152.17/133.40 tff(c_46, plain, (m0(a, e, e))). % 152.17/133.40 tff(c_70, plain, (m0(d, e, c))). % 152.17/133.40 tff(c_62, plain, (m0(b, b, e))). % 152.17/133.40 tff(c_38, plain, (![X_4, Y_5]: (m0(X_4, d, Y_5)))). % 152.17/133.40 tff(c_24, plain, (![X_1]: (m0(a, X_1, a)))). % 152.17/133.40 tff(c_54, plain, (m0(e, b, c))). % 152.17/133.40 tff(c_1204, plain, (s2(d))). % 152.17/133.40 tff(c_885, plain, (k1(b))). % 152.17/133.40 tff(c_884, plain, (m2(b))). % 152.17/133.40 tff(c_76, plain, (m0(b, a, a))). % 152.17/133.40 tff(c_34, plain, (![X_3]: (q0(X_3, d)))). % 152.17/133.40 tff(c_30, plain, (n0(a, b))). % 152.17/133.40 tff(c_28, plain, (![X_2]: (p0(b, X_2)))). % 152.17/133.40 tff(c_58, plain, (q0(d, b))). % 152.17/133.40 tff(c_36, plain, (p0(c, b))). % 152.17/133.40 tff(c_6, plain, (n0(d, e))). % 152.17/133.40 tff(c_74, plain, (n0(b, a))). % 152.17/133.40 tff(c_68, plain, (n0(c, d))). % 152.17/133.40 tff(c_72, plain, (q0(a, b))). % 152.17/133.40 tff(c_42, plain, (q0(b, e))). % 152.17/133.40 tff(c_52, plain, (n0(d, c))). % 152.17/133.40 tff(c_66, plain, (q0(d, c))). % 152.17/133.40 tff(c_22, plain, (n0(e, b))). % 152.17/133.40 tff(c_60, plain, (n0(e, e))). % 152.17/133.40 tff(c_14, plain, (n0(d, b))). % 152.17/133.40 tff(c_12, plain, (q0(b, b))). % 152.17/133.40 tff(c_10, plain, (s0(b))). % 152.17/133.40 tff(c_2, plain, (s0(d))). % 152.17/133.40 tff(c_18, plain, (r0(b))). % 152.17/133.40 tff(c_26, plain, (r0(e))). % 152.17/133.40 tff(c_40, plain, (l0(a))). % 152.17/133.40 tff(c_48, plain, (l0(c))). % 152.17/133.40 tff(c_56, plain, (k0(e))). % 152.17/133.40 tff(c_64, plain, (k0(b))). % 152.17/133.40 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 152.17/133.40 %------------------------------------------------------------------------------