%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MSC016+1 : TPTP v9.0.0. Released v3.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 : n024.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 07:45:11 PM UTC 2025 % Result : CounterSatisfiable 26.89s 11.86s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : MSC016+1 : TPTP v9.0.0. Released v3.5.0. % 0.12/0.13 % 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.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 07:59:06 EDT 2025 % 0.12/0.34 % CPUTime : % 26.89/11.86 % 26.89/11.86 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.89/11.86 % 26.89/11.86 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.89/11.87 %$ p > ld__ > flower > animal > g > #nlpp > pet > h > w > pig > lkg > lilly > k > horse > hill > e > d > cow > c > b > aparna > a % 26.89/11.87 % 26.89/11.87 %Foreground sorts: % 26.89/11.87 % 26.89/11.87 % 26.89/11.87 %Background operators: % 26.89/11.87 % 26.89/11.87 % 26.89/11.87 %Foreground operators: % 26.89/11.87 tff(a, type, a: $i). % 26.89/11.87 tff(cow, type, cow: $i). % 26.89/11.87 tff(g, type, g: ($i * $i) > $i). % 26.89/11.87 tff(w, type, w: $i). % 26.89/11.87 tff(pig, type, pig: $i). % 26.89/11.87 tff(k, type, k: $i). % 26.89/11.87 tff(animal, type, animal: $i > $o). % 26.89/11.87 tff(lkg, type, lkg: $i). % 26.89/11.87 tff(ld__, type, ld__: ($i * $i) > $o). % 26.89/11.87 tff(b, type, b: $i). % 26.89/11.87 tff(horse, type, horse: $i). % 26.89/11.87 tff(h, type, h: $i > $i). % 26.89/11.87 tff(lilly, type, lilly: $i). % 26.89/11.87 tff(pet, type, pet: $i > $i). % 26.89/11.87 tff(d, type, d: $i). % 26.89/11.87 tff(aparna, type, aparna: $i). % 26.89/11.87 tff(p, type, p: ($i * $i * $i) > $o). % 26.89/11.87 tff(e, type, e: $i). % 26.89/11.87 tff(hill, type, hill: $i). % 26.89/11.87 tff(flower, type, flower: $i > $o). % 26.89/11.87 tff(c, type, c: $i). % 26.89/11.87 % 26.89/11.87 %Saturated clause set: % 26.89/11.87 tff(c_30654, plain, (![X1_205, X3_207, Y_69, Z_70]: (~p(g(X1_205, X3_207), Y_69, Z_70) | ~ld__(X1_205, e)))). % 26.89/11.87 tff(c_30647, plain, (![X1_214, X3_212, Y_69, Z_70]: (~p(g(X1_214, X3_212), Y_69, Z_70) | ~ld__(X3_212, e)))). % 26.89/11.87 tff(c_30547, plain, (![X1_36, Y_1820, Z_1821]: (~p(h(X1_36), Y_1820, Z_1821) | ~ld__(X1_36, d)))). % 26.89/11.87 tff(c_30546, plain, (![X2_198, Y_1820, Z_1821]: (~p(h(X2_198), Y_1820, Z_1821) | ~ld__(d, X2_198)))). % 26.89/11.87 tff(c_30538, plain, (![Y1_186, Y_69, Z_70]: (~ld__(h(Y1_186), h(d)) | ~p(h(Y1_186), Y_69, Z_70)))). % 26.89/11.87 tff(c_30364, plain, (![X_1767, X1_32, X3_34, Z_1768]: (~p(X_1767, g(X1_32, X3_34), Z_1768) | ~ld__(e, X1_32) | ~ld__(X1_32, a)))). % 26.89/11.87 tff(c_30363, plain, (![X_1767, X1_32, X3_34, Z_1768]: (~p(X_1767, g(X1_32, X3_34), Z_1768) | ~ld__(e, X1_32) | ~ld__(X3_34, c)))). % 26.89/11.87 tff(c_30362, plain, (![X_1767, X2_206, X4_208, Z_1768]: (~p(X_1767, g(X2_206, X4_208), Z_1768) | ~ld__(e, X2_206) | ~ld__(a, X2_206)))). % 26.89/11.87 tff(c_30361, plain, (![X_1767, X2_215, X4_213, Z_1768]: (~p(X_1767, g(X2_215, X4_213), Z_1768) | ~ld__(e, X2_215) | ~ld__(c, X4_213)))). % 26.89/11.87 tff(c_24914, plain, (![X2_206, X4_208, X_1441, Z_1442]: (~ld__(g(X2_206, X4_208), g(a, c)) | ~p(X_1441, g(X2_206, X4_208), Z_1442) | ~ld__(e, X2_206)))). % 26.89/11.87 tff(c_30295, plain, (![X_1747, X1_32, X3_34, Z_1748]: (~p(X_1747, g(X1_32, X3_34), Z_1748) | ~ld__(e, X3_34) | ~ld__(X1_32, a)))). % 26.89/11.87 tff(c_30294, plain, (![X_1747, X1_32, X3_34, Z_1748]: (~p(X_1747, g(X1_32, X3_34), Z_1748) | ~ld__(e, X3_34) | ~ld__(X3_34, c)))). % 26.89/11.87 tff(c_30293, plain, (![X_1747, X2_206, X4_208, Z_1748]: (~p(X_1747, g(X2_206, X4_208), Z_1748) | ~ld__(e, X4_208) | ~ld__(a, X2_206)))). % 26.89/11.87 tff(c_30292, plain, (![X_1747, X2_215, X4_213, Z_1748]: (~p(X_1747, g(X2_215, X4_213), Z_1748) | ~ld__(e, X4_213) | ~ld__(c, X4_213)))). % 26.89/11.87 tff(c_24911, plain, (![X2_215, X4_213, X_1441, Z_1442]: (~ld__(g(X2_215, X4_213), g(a, c)) | ~p(X_1441, g(X2_215, X4_213), Z_1442) | ~ld__(e, X4_213)))). % 26.89/11.87 tff(c_30042, plain, (![X_1691, X1_32, X3_34, Z_1692]: (~p(X_1691, g(X1_32, X3_34), Z_1692) | ~ld__(X3_34, e) | ~ld__(X1_32, a)))). % 26.89/11.87 tff(c_30039, plain, (![X_1691, X2_215, X4_213, Z_1692]: (~p(X_1691, g(X2_215, X4_213), Z_1692) | ~ld__(X4_213, e) | ~ld__(c, X4_213)))). % 26.89/11.87 tff(c_30040, plain, (![X_1691, X2_206, X4_208, Z_1692]: (~p(X_1691, g(X2_206, X4_208), Z_1692) | ~ld__(X4_208, e) | ~ld__(a, X2_206)))). % 26.89/11.87 tff(c_30041, plain, (![X_1691, X1_32, X3_34, Z_1692]: (~p(X_1691, g(X1_32, X3_34), Z_1692) | ~ld__(X3_34, e) | ~ld__(X3_34, c)))). % 26.89/11.88 tff(c_24917, plain, (![X1_32, X3_34, X_1441, Z_1442]: (~ld__(g(X1_32, X3_34), g(a, c)) | ~p(X_1441, g(X1_32, X3_34), Z_1442) | ~ld__(X3_34, e)))). % 26.89/11.88 tff(c_29973, plain, (![X_1671, X1_32, X3_34, Z_1672]: (~p(X_1671, g(X1_32, X3_34), Z_1672) | ~ld__(X1_32, e) | ~ld__(X1_32, a)))). % 26.89/11.88 tff(c_29972, plain, (![X_1671, X1_32, X3_34, Z_1672]: (~p(X_1671, g(X1_32, X3_34), Z_1672) | ~ld__(X1_32, e) | ~ld__(X3_34, c)))). % 26.89/11.88 tff(c_29971, plain, (![X_1671, X2_206, X4_208, Z_1672]: (~p(X_1671, g(X2_206, X4_208), Z_1672) | ~ld__(X2_206, e) | ~ld__(a, X2_206)))). % 26.89/11.88 tff(c_29970, plain, (![X_1671, X2_215, X4_213, Z_1672]: (~p(X_1671, g(X2_215, X4_213), Z_1672) | ~ld__(X2_215, e) | ~ld__(c, X4_213)))). % 26.89/11.88 tff(c_24920, plain, (![X1_32, X3_34, X_1441, Z_1442]: (~ld__(g(X1_32, X3_34), g(a, c)) | ~p(X_1441, g(X1_32, X3_34), Z_1442) | ~ld__(X1_32, e)))). % 26.89/11.88 tff(c_22586, plain, (![Z_1342, X_1343, X2_215, X4_213]: (~ld__(Z_1342, g(b, b)) | ~p(X_1343, g(X2_215, X4_213), Z_1342) | ~ld__(e, X4_213)))). % 26.89/11.88 tff(c_22589, plain, (![Z_1342, X_1343, X2_206, X4_208]: (~ld__(Z_1342, g(b, b)) | ~p(X_1343, g(X2_206, X4_208), Z_1342) | ~ld__(e, X2_206)))). % 26.89/11.88 tff(c_22592, plain, (![Z_1342, X_1343, X1_32, X3_34]: (~ld__(Z_1342, g(b, b)) | ~p(X_1343, g(X1_32, X3_34), Z_1342) | ~ld__(X3_34, e)))). % 26.89/11.88 tff(c_22595, plain, (![Z_1342, X_1343, X1_32, X3_34]: (~ld__(Z_1342, g(b, b)) | ~p(X_1343, g(X1_32, X3_34), Z_1342) | ~ld__(X1_32, e)))). % 26.89/11.88 tff(c_29821, plain, (~ld__(g(a, c), g(a, c)))). % 26.89/11.88 tff(c_10052, plain, (![Z_572, Y_573, Y1_55]: (~ld__(Z_572, k) | ~ld__(Y_573, g(a, c)) | ~p(h(Y1_55), Y_573, Z_572)))). % 26.89/11.88 tff(c_568, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_878, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_570, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_388, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_1054, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_894, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_1038, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_554, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_1036, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_406, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_550, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_408, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_392, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_410, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_28206, plain, (![Y1_180, Y_69, Z_70]: (~p(pet(Y1_180), Y_69, Z_70)))). % 26.89/11.88 tff(c_552, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_572, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_390, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_27698, plain, (~ld__(g(b, b), g(b, b)))). % 26.89/11.88 tff(c_896, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_9433, plain, (![Z_552, Y1_55, Y_553]: (~ld__(Z_552, k) | ~ld__(Z_552, g(b, b)) | ~p(h(Y1_55), Y_553, Z_552)))). % 26.89/11.88 tff(c_1058, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.88 tff(c_892, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_1040, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_876, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_27190, plain, (![Z_1541]: (~p(a, w, Z_1541)))). % 26.89/11.89 tff(c_27118, plain, (![X_1538, Z_1539]: (~ld__(X_1538, g(e, e)) | ~p(X_1538, w, Z_1539)))). % 26.89/11.89 tff(c_1056, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_874, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_786, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_26748, plain, (![Z_1527, X_1528]: (~ld__(Z_1527, b) | ~p(X_1528, w, Z_1527)))). % 26.89/11.89 tff(c_948, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_946, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_928, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_766, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_1034, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_444, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_842, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_788, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_460, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_16688, plain, (![Z_70, X_68, X2_955, X4_956]: (~ld__(Z_70, k) | ~p(X_68, g(X2_955, X4_956), Z_70) | ~ld__(c, X4_956)))). % 26.89/11.89 tff(c_566, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_496, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_15354, plain, (![Z_70, X_68, X2_920, X4_921]: (~ld__(Z_70, k) | ~p(X_68, g(X2_920, X4_921), Z_70) | ~ld__(a, X2_920)))). % 26.89/11.89 tff(c_462, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_446, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_24923, plain, (![X_1441, Y1_55, Z_1442]: (~p(X_1441, h(Y1_55), Z_1442)))). % 26.89/11.89 tff(c_24926, plain, (![X_1441, Y1_18, Z_1442]: (~p(X_1441, pet(Y1_18), Z_1442)))). % 26.89/11.89 tff(c_24950, plain, (![X_1441, Z_1442]: (~p(X_1441, d, Z_1442)))). % 26.89/11.89 tff(c_24953, plain, (![X_1441, Z_1442]: (~p(X_1441, c, Z_1442)))). % 26.89/11.89 tff(c_544, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_24956, plain, (![X_1441, Z_1442]: (~p(X_1441, lilly, Z_1442)))). % 26.89/11.89 tff(c_24959, plain, (![X_1441, Z_1442]: (~p(X_1441, hill, Z_1442)))). % 26.89/11.89 tff(c_24962, plain, (![X_1441, Z_1442]: (~p(X_1441, aparna, Z_1442)))). % 26.89/11.89 tff(c_564, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_24947, plain, (![X_1441, Z_1442]: (~p(X_1441, horse, Z_1442)))). % 26.89/11.89 tff(c_24944, plain, (![X_1441, Z_1442]: (~p(X_1441, cow, Z_1442)))). % 26.89/11.89 tff(c_24938, plain, (![X_1441, Z_1442]: (~p(X_1441, k, Z_1442)))). % 26.89/11.89 tff(c_24932, plain, (![X_1441, Z_1442]: (~p(X_1441, pig, Z_1442)))). % 26.89/11.89 tff(c_24929, plain, (![X_1441, Z_1442]: (~p(X_1441, e, Z_1442)))). % 26.89/11.89 tff(c_1002, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_1032, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_514, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_886, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_872, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_338, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_300, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.89 tff(c_386, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_500, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_442, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_518, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_784, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_932, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_840, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_824, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_12509, plain, (![Z_764, X_765, X1_32, X3_34]: (~ld__(Z_764, k) | ~p(X_765, g(X1_32, X3_34), Z_764) | ~ld__(X1_32, a)))). % 26.89/11.90 tff(c_870, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_838, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_298, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_21892, plain, (![Y1_55, Z_1310]: (~p(h(Y1_55), w, Z_1310)))). % 26.89/11.90 tff(c_334, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_21907, plain, (![Z_1310]: (~p(k, w, Z_1310)))). % 26.89/11.90 tff(c_404, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_888, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_546, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_21370, plain, (![Z_1267, X_1268]: (~ld__(Z_1267, a) | ~p(X_1268, a, Z_1267)))). % 26.89/11.90 tff(c_768, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_516, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_950, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_986, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_12506, plain, (![Z_764, X_765, X1_32, X3_34]: (~ld__(Z_764, k) | ~p(X_765, g(X1_32, X3_34), Z_764) | ~ld__(X3_34, c)))). % 26.89/11.90 tff(c_356, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_770, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_930, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_402, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_384, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_890, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_19769, plain, (![Z_1174, X_1175]: (~ld__(Z_1174, c) | ~p(X_1175, b, Z_1174)))). % 26.89/11.90 tff(c_1030, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_984, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_19635, plain, (~ld__(d, d))). % 26.89/11.90 tff(c_1050, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_382, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_1048, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_548, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_822, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_562, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_19007, plain, (![Z_1106, X_1108]: (~ld__(Z_1106, hill) | ~p(X_1108, lkg, Z_1106)))). % 26.89/11.90 tff(c_1000, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_336, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_1052, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_400, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_18548, plain, (![X_1066, Z_1068]: (~ld__(X_1066, k) | ~p(X_1066, lkg, Z_1068)))). % 26.89/11.90 tff(c_1004, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_280, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_464, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_284, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_352, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_868, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_282, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_982, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_354, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_498, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_302, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_820, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_1400, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_1558, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_16870, plain, (![X2_955, X4_956, Y_69, Z_70]: (~p(g(X2_955, X4_956), Y_69, Z_70) | ~ld__(e, X4_956)))). % 26.89/11.90 tff(c_16658, plain, (![X_68, Y_69, X2_955, X4_956]: (~p(X_68, Y_69, g(X2_955, X4_956)) | ~ld__(b, X4_956)))). % 26.89/11.90 tff(c_1398, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_3940, plain, (![X2_215, X4_213, X1_214, X3_212]: (ld__(g(X2_215, X4_213), g(X1_214, X3_212)) | ~ld__(X3_212, X4_213)))). % 26.89/11.90 tff(c_1560, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_1396, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_1562, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_834, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_782, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 26.89/11.90 tff(c_15781, plain, (![Y_69, Z_70]: (~p(b, Y_69, Z_70)))). % 26.89/11.90 tff(c_762, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_15664, plain, (~ld__(e, e))). % 27.11/11.91 tff(c_15536, plain, (![X2_920, X4_921, Y_69, Z_70]: (~p(g(X2_920, X4_921), Y_69, Z_70) | ~ld__(e, X2_920)))). % 27.11/11.91 tff(c_15324, plain, (![X_68, Y_69, X2_920, X4_921]: (~p(X_68, Y_69, g(X2_920, X4_921)) | ~ld__(b, X2_920)))). % 27.11/11.91 tff(c_456, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_3827, plain, (![X2_206, X4_208, X1_205, X3_207]: (ld__(g(X2_206, X4_208), g(X1_205, X3_207)) | ~ld__(X1_205, X2_206)))). % 27.11/11.91 tff(c_814, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_944, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_922, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_998, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_436, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_348, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_14363, plain, (![Y_890, X_891]: (~ld__(Y_890, w) | ~p(X_891, Y_890, b)))). % 27.11/11.91 tff(c_328, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_13639, plain, (![X_838, Y_839, X1_32, X3_34]: (~p(X_838, Y_839, g(X1_32, X3_34)) | ~ld__(X3_34, b)))). % 27.11/11.91 tff(c_780, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_13642, plain, (![X_838, Y_839, X1_32, X3_34]: (~p(X_838, Y_839, g(X1_32, X3_34)) | ~ld__(X1_32, b)))). % 27.11/11.91 tff(c_494, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_13551, plain, (![Y_829, X_830]: (~ld__(Y_829, a) | ~p(X_830, Y_829, a)))). % 27.11/11.91 tff(c_942, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_13645, plain, (![X_838, Y_839, Y1_55]: (~p(X_838, Y_839, h(Y1_55))))). % 27.11/11.91 tff(c_13648, plain, (![X_838, Y_839, Y1_18]: (~p(X_838, Y_839, pet(Y1_18))))). % 27.11/11.91 tff(c_13678, plain, (![X_838, Y_839]: (~p(X_838, Y_839, lilly)))). % 27.11/11.91 tff(c_836, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_13684, plain, (![X_838, Y_839]: (~p(X_838, Y_839, aparna)))). % 27.11/11.91 tff(c_13690, plain, (![X_838, Y_839]: (~p(X_838, Y_839, w)))). % 27.11/11.91 tff(c_13672, plain, (![X_838, Y_839]: (~p(X_838, Y_839, d)))). % 27.11/11.91 tff(c_512, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_13669, plain, (![X_838, Y_839]: (~p(X_838, Y_839, horse)))). % 27.11/11.91 tff(c_13666, plain, (![X_838, Y_839]: (~p(X_838, Y_839, cow)))). % 27.11/11.91 tff(c_13657, plain, (![X_838, Y_839]: (~p(X_838, Y_839, lkg)))). % 27.11/11.91 tff(c_13654, plain, (![X_838, Y_839]: (~p(X_838, Y_839, pig)))). % 27.11/11.91 tff(c_13651, plain, (![X_838, Y_839]: (~p(X_838, Y_839, e)))). % 27.11/11.91 tff(c_274, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_760, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_330, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_940, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_778, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_13130, plain, (![Y_69, Z_70]: (~p(c, Y_69, Z_70)))). % 27.11/11.91 tff(c_832, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_818, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_510, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_350, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_296, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_996, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_764, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_924, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_490, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_332, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_440, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_926, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_458, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_976, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_346, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_11347, plain, (![Y_677, X_678]: (~ld__(Y_677, b) | ~p(X_678, Y_677, c)))). % 27.11/11.91 tff(c_816, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_292, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_492, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_11005, plain, (![Y_641, X_643]: (~ld__(Y_641, lkg) | ~p(X_643, Y_641, hill)))). % 27.11/11.91 tff(c_508, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_10893, plain, (![X_632, Y_634]: (~ld__(X_632, k) | ~p(X_632, Y_634, hill)))). % 27.11/11.91 tff(c_276, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_278, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_994, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_438, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_980, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_294, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_454, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_978, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1556, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1344, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1450, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1552, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1290, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1288, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1394, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1392, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1554, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(X_68, g(e, e)) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_9023, plain, (![X_510, Z_511]: (~ld__(X_510, a) | ~p(X_510, b, Z_511)))). % 27.11/11.91 tff(c_1346, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_8999, plain, (![X_510, Z_511]: (~ld__(X_510, a) | ~p(X_510, a, Z_511)))). % 27.11/11.91 tff(c_1506, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1504, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.91 tff(c_1452, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_1292, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_1454, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_7729, plain, (![Z_419, Y_420]: (~ld__(Z_419, c) | ~ld__(Z_419, a) | ~p(a, Y_420, Z_419)))). % 27.11/11.92 tff(c_1390, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(X_68, g(e, e)) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_1508, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_7027, plain, (![Y_390, Z_391]: (~ld__(Y_390, b) | ~ld__(Y_390, a) | ~p(a, Y_390, Z_391)))). % 27.11/11.92 tff(c_1342, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, g(e, e)) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_720, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_7248, plain, (![Y_398, Z_399]: (~ld__(Y_398, b) | ~ld__(Z_399, a) | ~p(a, Y_398, Z_399)))). % 27.11/11.92 tff(c_8000, plain, (~ld__(c, c))). % 27.11/11.92 tff(c_7466, plain, (![Z_408, Y_409]: (~ld__(Z_408, c) | ~ld__(Y_409, a) | ~p(a, Y_409, Z_408)))). % 27.11/11.92 tff(c_736, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_7766, plain, (~ld__(w, w))). % 27.11/11.92 tff(c_738, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_6004, plain, (![Y_69, X1_326, X2_327, Z_70]: (~ld__(Y_69, w) | ~p(g(X1_326, X2_327), Y_69, Z_70)))). % 27.11/11.92 tff(c_7761, plain, (~ld__(b, b))). % 27.11/11.92 tff(c_6001, plain, (![Z_70, X1_326, X2_327, Y_69]: (~ld__(Z_70, b) | ~p(g(X1_326, X2_327), Y_69, Z_70)))). % 27.11/11.92 tff(c_722, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3568, plain, (![X2_198, X1_197]: (ld__(h(X2_198), h(X1_197)) | ~ld__(X1_197, X2_198)))). % 27.11/11.92 tff(c_1208, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_1222, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_740, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_1224, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_6511, plain, (![X_359, Y_360]: (~ld__(X_359, a) | ~p(X_359, Y_360, a)))). % 27.11/11.92 tff(c_6945, plain, (~ld__(k, k))). % 27.11/11.92 tff(c_1226, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, b) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_1206, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_718, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_6619, plain, (~ld__(a, a))). % 27.11/11.92 tff(c_1204, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, c) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_6523, plain, (![X_359, Y_360]: (~ld__(X_359, a) | ~p(X_359, Y_360, c)))). % 27.11/11.92 tff(c_1448, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_1282, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_6428, plain, (![Y_69, Z_70]: (~p(w, Y_69, Z_70)))). % 27.11/11.92 tff(c_6426, plain, (~ld__(lkg, lkg))). % 27.11/11.92 tff(c_2782, plain, (![Y_69, Z_70]: (~ld__(Y_69, lkg) | ~p(k, Y_69, Z_70)))). % 27.11/11.92 tff(c_1446, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_6207, plain, (~ld__(hill, hill))). % 27.11/11.92 tff(c_1340, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_2788, plain, (![Z_70, Y_69]: (~ld__(Z_70, hill) | ~p(k, Y_69, Z_70)))). % 27.11/11.92 tff(c_6201, plain, (![Y_69, Z_70]: (~p(d, Y_69, Z_70)))). % 27.11/11.92 tff(c_1500, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_6089, plain, (![Y_69, Z_70]: (~p(e, Y_69, Z_70)))). % 27.11/11.92 tff(c_1444, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Z_70, b) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3185, plain, (![X1_16, X2_17, Y1_18]: (ld__(g(X1_16, X2_17), pet(Y1_18))))). % 27.11/11.92 tff(c_3184, plain, (![X1_53, X2_54, Y1_55]: (ld__(g(X1_53, X2_54), h(Y1_55))))). % 27.11/11.92 tff(c_3200, plain, (![X1_56, X2_57]: (ld__(g(X1_56, X2_57), w)))). % 27.11/11.92 tff(c_1336, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3194, plain, (![X1_44, X2_45]: (ld__(g(X1_44, X2_45), c)))). % 27.11/11.92 tff(c_3195, plain, (![X1_25, Y1_26]: (ld__(h(X1_25), pet(Y1_26))))). % 27.11/11.92 tff(c_3196, plain, (![X1_14, X2_15]: (ld__(g(X1_14, X2_15), lilly)))). % 27.11/11.92 tff(c_1498, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, k) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3189, plain, (![X1_58, X2_59]: (ld__(g(X1_58, X2_59), k)))). % 27.11/11.92 tff(c_3192, plain, (![X1_12, X2_13]: (ld__(g(X1_12, X2_13), horse)))). % 27.11/11.92 tff(c_3191, plain, (![X1_10, X2_11]: (ld__(g(X1_10, X2_11), cow)))). % 27.11/11.92 tff(c_3188, plain, (![X1_60, X2_61]: (ld__(g(X1_60, X2_61), lkg)))). % 27.11/11.92 tff(c_3197, plain, (![X1_62, X2_63]: (ld__(g(X1_62, X2_63), hill)))). % 27.11/11.92 tff(c_1286, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3186, plain, (![X1_51, X2_52]: (ld__(g(X1_51, X2_52), e)))). % 27.11/11.92 tff(c_3198, plain, (![X1_8, X2_9]: (ld__(g(X1_8, X2_9), aparna)))). % 27.11/11.92 tff(c_3199, plain, (![X1_41, X2_42]: (ld__(g(X1_41, X2_42), b)))). % 27.11/11.92 tff(c_1502, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, k) | ~ld__(Y_69, w) | ~ld__(Y_69, g(a, c)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3190, plain, (![X1_39, X2_40]: (ld__(g(X1_39, X2_40), a)))). % 27.11/11.92 tff(c_3193, plain, (![X1_47, X2_48]: (ld__(g(X1_47, X2_48), d)))). % 27.11/11.92 tff(c_3187, plain, (![X1_19, X2_20]: (ld__(g(X1_19, X2_20), pig)))). % 27.11/11.92 tff(c_3219, plain, (![X1_38]: (ld__(h(X1_38), a)))). % 27.11/11.92 tff(c_3221, plain, (![X1_24]: (ld__(h(X1_24), lilly)))). % 27.11/11.92 tff(c_1284, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Z_70, b) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3208, plain, (![X1_67]: (ld__(h(X1_67), k)))). % 27.11/11.92 tff(c_3210, plain, (![X1_49]: (ld__(h(X1_49), d)))). % 27.11/11.92 tff(c_3222, plain, (![X1_23]: (ld__(h(X1_23), horse)))). % 27.11/11.92 tff(c_1338, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, k) | ~ld__(Y_69, w) | ~ld__(Z_70, g(b, b)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3207, plain, (![X1_22]: (ld__(h(X1_22), cow)))). % 27.11/11.92 tff(c_3201, plain, (![X1_50]: (ld__(h(X1_50), e)))). % 27.11/11.92 tff(c_3220, plain, (![X1_27]: (ld__(h(X1_27), pig)))). % 27.11/11.92 tff(c_3204, plain, (![X1_4]: (ld__(pet(X1_4), b)))). % 27.11/11.92 tff(c_3209, plain, (![X1_46]: (ld__(h(X1_46), c)))). % 27.11/11.92 tff(c_610, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3212, plain, (![X1_7]: (ld__(pet(X1_7), e)))). % 27.11/11.92 tff(c_3213, plain, (![X1_29]: (ld__(pet(X1_29), k)))). % 27.11/11.92 tff(c_3202, plain, (![X1_64]: (ld__(h(X1_64), lkg)))). % 27.11/11.92 tff(c_1170, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3206, plain, (![X1_30]: (ld__(pet(X1_30), lkg)))). % 27.11/11.92 tff(c_3205, plain, (![X1_31]: (ld__(pet(X1_31), w)))). % 27.11/11.92 tff(c_3211, plain, (![X1_21]: (ld__(h(X1_21), aparna)))). % 27.11/11.92 tff(c_3223, plain, (![X1_3]: (ld__(pet(X1_3), a)))). % 27.11/11.92 tff(c_3216, plain, (![X1_43]: (ld__(h(X1_43), b)))). % 27.11/11.92 tff(c_630, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3217, plain, (![X1_5]: (ld__(pet(X1_5), c)))). % 27.11/11.92 tff(c_3218, plain, (![X1_6]: (ld__(pet(X1_6), d)))). % 27.11/11.92 tff(c_3214, plain, (![X1_28]: (ld__(pet(X1_28), hill)))). % 27.11/11.92 tff(c_612, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3203, plain, (![X1_66]: (ld__(h(X1_66), w)))). % 27.11/11.92 tff(c_3215, plain, (![X1_65]: (ld__(h(X1_65), hill)))). % 27.11/11.92 tff(c_3288, plain, (ld__(hill, lkg))). % 27.11/11.92 tff(c_3291, plain, (ld__(e, d))). % 27.11/11.92 tff(c_3232, plain, (ld__(hill, pig))). % 27.11/11.92 tff(c_1100, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3233, plain, (ld__(hill, lilly))). % 27.11/11.92 tff(c_3275, plain, (ld__(b, k))). % 27.11/11.92 tff(c_3294, plain, (ld__(e, lkg))). % 27.11/11.92 tff(c_614, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.92 tff(c_3228, plain, (ld__(b, pig))). % 27.11/11.92 tff(c_3265, plain, (ld__(a, cow))). % 27.11/11.92 tff(c_3283, plain, (ld__(b, aparna))). % 27.11/11.92 tff(c_3290, plain, (ld__(b, hill))). % 27.11/11.92 tff(c_3278, plain, (ld__(a, lkg))). % 27.11/11.93 tff(c_666, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3285, plain, (ld__(a, hill))). % 27.11/11.93 tff(c_3277, plain, (ld__(e, pig))). % 27.11/11.93 tff(c_3239, plain, (ld__(b, lilly))). % 27.11/11.93 tff(c_1116, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3269, plain, (ld__(c, horse))). % 27.11/11.93 tff(c_3243, plain, (ld__(e, horse))). % 27.11/11.93 tff(c_3299, plain, (ld__(c, lkg))). % 27.11/11.93 tff(c_3249, plain, (ld__(b, cow))). % 27.11/11.93 tff(c_3267, plain, (ld__(a, k))). % 27.11/11.93 tff(c_668, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3242, plain, (ld__(e, cow))). % 27.11/11.93 tff(c_3226, plain, (ld__(d, horse))). % 27.11/11.93 tff(c_3244, plain, (ld__(hill, cow))). % 27.11/11.93 tff(c_1172, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3296, plain, (ld__(b, lkg))). % 27.11/11.93 tff(c_3272, plain, (ld__(a, w))). % 27.11/11.93 tff(c_3292, plain, (ld__(b, e))). % 27.11/11.93 tff(c_3266, plain, (ld__(a, pig))). % 27.11/11.93 tff(c_3289, plain, (ld__(b, d))). % 27.11/11.93 tff(c_628, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3246, plain, (ld__(c, pig))). % 27.11/11.93 tff(c_3247, plain, (ld__(w, lilly))). % 27.11/11.93 tff(c_3231, plain, (ld__(d, cow))). % 27.11/11.93 tff(c_1150, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3248, plain, (ld__(lkg, cow))). % 27.11/11.93 tff(c_3298, plain, (ld__(w, d))). % 27.11/11.93 tff(c_3287, plain, (ld__(b, a))). % 27.11/11.93 tff(c_3286, plain, (ld__(a, e))). % 27.11/11.93 tff(c_3225, plain, (ld__(e, lilly))). % 27.11/11.93 tff(c_1168, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3240, plain, (ld__(b, horse))). % 27.11/11.93 tff(c_3252, plain, (ld__(w, horse))). % 27.11/11.93 tff(c_3237, plain, (ld__(e, aparna))). % 27.11/11.93 tff(c_158, plain, (![X3_34, X4_35, X1_32, X2_33]: (~ld__(X3_34, X4_35) | ld__(g(X1_32, X3_34), g(X2_33, X4_35))))). % 27.11/11.93 tff(c_3284, plain, (ld__(b, w))). % 27.11/11.93 tff(c_3304, plain, (ld__(c, d))). % 27.11/11.93 tff(c_3260, plain, (ld__(a, aparna))). % 27.11/11.93 tff(c_3245, plain, (ld__(hill, horse))). % 27.11/11.93 tff(c_3238, plain, (ld__(lkg, aparna))). % 27.11/11.93 tff(c_682, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3250, plain, (ld__(k, aparna))). % 27.11/11.93 tff(c_3241, plain, (ld__(c, lilly))). % 27.11/11.93 tff(c_3251, plain, (ld__(k, cow))). % 27.11/11.93 tff(c_160, plain, (![X1_32, X2_33, X3_34, X4_35]: (~ld__(X1_32, X2_33) | ld__(g(X1_32, X3_34), g(X2_33, X4_35))))). % 27.11/11.93 tff(c_3268, plain, (ld__(w, cow))). % 27.11/11.93 tff(c_3234, plain, (ld__(d, lilly))). % 27.11/11.93 tff(c_3227, plain, (ld__(k, horse))). % 27.11/11.93 tff(c_3264, plain, (ld__(c, k))). % 27.11/11.93 tff(c_3230, plain, (ld__(c, aparna))). % 27.11/11.93 tff(c_1118, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3253, plain, (ld__(lkg, pig))). % 27.11/11.93 tff(c_3254, plain, (ld__(k, lilly))). % 27.11/11.93 tff(c_3263, plain, (ld__(d, aparna))). % 27.11/11.93 tff(c_6, plain, (p(h(d), g(a, c), g(b, b)))). % 27.11/11.93 tff(c_3259, plain, (ld__(a, horse))). % 27.11/11.93 tff(c_3258, plain, (ld__(a, d))). % 27.11/11.93 tff(c_3257, plain, (ld__(lkg, horse))). % 27.11/11.93 tff(c_3256, plain, (ld__(k, lkg))). % 27.11/11.93 tff(c_3255, plain, (ld__(k, pig))). % 27.11/11.93 tff(c_632, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3235, plain, (ld__(hill, aparna))). % 27.11/11.93 tff(c_3236, plain, (ld__(d, pig))). % 27.11/11.93 tff(c_3262, plain, (ld__(w, aparna))). % 27.11/11.93 tff(c_162, plain, (![X1_36, X2_37]: (ld__(h(X1_36), h(X2_37)) | ~ld__(X1_36, X2_37)))). % 27.11/11.93 tff(c_3295, plain, (ld__(c, b))). % 27.11/11.93 tff(c_3282, plain, (ld__(w, e))). % 27.11/11.93 tff(c_3281, plain, (ld__(w, hill))). % 27.11/11.93 tff(c_3280, plain, (ld__(e, hill))). % 27.11/11.93 tff(c_3293, plain, (ld__(d, hill))). % 27.11/11.93 tff(c_664, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3279, plain, (ld__(c, a))). % 27.11/11.93 tff(c_3229, plain, (ld__(c, cow))). % 27.11/11.93 tff(c_3261, plain, (ld__(lkg, lilly))). % 27.11/11.93 tff(c_8, plain, (p(h(d), g(e, e), k))). % 27.11/11.93 tff(c_3276, plain, (ld__(k, hill))). % 27.11/11.93 tff(c_3297, plain, (ld__(c, w))). % 27.11/11.93 tff(c_3274, plain, (ld__(w, lkg))). % 27.11/11.93 tff(c_3273, plain, (ld__(e, k))). % 27.11/11.93 tff(c_3301, plain, (ld__(d, lkg))). % 27.11/11.93 tff(c_1154, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_3300, plain, (ld__(d, k))). % 27.11/11.93 tff(c_3302, plain, (ld__(c, hill))). % 27.11/11.93 tff(c_3303, plain, (ld__(c, e))). % 27.11/11.93 tff(c_4, plain, (p(g(e, e), w, b))). % 27.11/11.93 tff(c_3271, plain, (ld__(w, pig))). % 27.11/11.93 tff(c_3270, plain, (ld__(w, k))). % 27.11/11.93 tff(c_3224, plain, (ld__(a, lilly))). % 27.11/11.93 tff(c_24, plain, (![Y_2, X_1]: (ld__(Y_2, X_1) | ~ld__(X_1, Y_2)))). % 27.11/11.93 tff(c_244, plain, (![Y1_55, X1_53, X2_54]: (ld__(h(Y1_55), g(X1_53, X2_54))))). % 27.11/11.93 tff(c_1098, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_94, plain, (![Y1_18, X1_16, X2_17]: (ld__(pet(Y1_18), g(X1_16, X2_17))))). % 27.11/11.93 tff(c_236, plain, (![X1_51, X2_52]: (ld__(e, g(X1_51, X2_52))))). % 27.11/11.93 tff(c_2824, plain, (![Y_69, Z_70]: (~p(pig, Y_69, Z_70)))). % 27.11/11.93 tff(c_96, plain, (![X1_19, X2_20]: (ld__(pig, g(X1_19, X2_20))))). % 27.11/11.93 tff(c_2804, plain, (![Y_69, Z_70]: (~p(lkg, Y_69, Z_70)))). % 27.11/11.93 tff(c_250, plain, (![X1_60, X2_61]: (ld__(lkg, g(X1_60, X2_61))))). % 27.11/11.93 tff(c_248, plain, (![X1_58, X2_59]: (ld__(k, g(X1_58, X2_59))))). % 27.11/11.93 tff(c_180, plain, (![X1_39, X2_40]: (ld__(a, g(X1_39, X2_40))))). % 27.11/11.93 tff(c_2685, plain, (![Y_69, Z_70]: (~p(cow, Y_69, Z_70)))). % 27.11/11.93 tff(c_1152, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, c) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_88, plain, (![X1_10, X2_11]: (ld__(cow, g(X1_10, X2_11))))). % 27.11/11.93 tff(c_2665, plain, (![Y_69, Z_70]: (~p(horse, Y_69, Z_70)))). % 27.11/11.93 tff(c_90, plain, (![X1_12, X2_13]: (ld__(horse, g(X1_12, X2_13))))). % 27.11/11.93 tff(c_220, plain, (![X1_47, X2_48]: (ld__(d, g(X1_47, X2_48))))). % 27.11/11.93 tff(c_204, plain, (![X1_44, X2_45]: (ld__(c, g(X1_44, X2_45))))). % 27.11/11.93 tff(c_106, plain, (![Y1_26, X1_25]: (ld__(pet(Y1_26), h(X1_25))))). % 27.11/11.93 tff(c_2566, plain, (![Y_69, Z_70]: (~p(lilly, Y_69, Z_70)))). % 27.11/11.93 tff(c_92, plain, (![X1_14, X2_15]: (ld__(lilly, g(X1_14, X2_15))))). % 27.11/11.93 tff(c_2489, plain, (![Y_69, Z_70]: (~p(hill, Y_69, Z_70)))). % 27.11/11.93 tff(c_1114, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, b) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_252, plain, (![X1_62, X2_63]: (ld__(hill, g(X1_62, X2_63))))). % 27.11/11.93 tff(c_2469, plain, (![Y_69, Z_70]: (~p(aparna, Y_69, Z_70)))). % 27.11/11.93 tff(c_86, plain, (![X1_8, X2_9]: (ld__(aparna, g(X1_8, X2_9))))). % 27.11/11.93 tff(c_184, plain, (![X1_41, X2_42]: (ld__(b, g(X1_41, X2_42))))). % 27.11/11.93 tff(c_246, plain, (![X1_56, X2_57]: (ld__(w, g(X1_56, X2_57))))). % 27.11/11.93 tff(c_232, plain, (![X1_50]: (ld__(e, h(X1_50))))). % 27.11/11.93 tff(c_254, plain, (![X1_64]: (ld__(lkg, h(X1_64))))). % 27.11/11.93 tff(c_258, plain, (![X1_66]: (ld__(w, h(X1_66))))). % 27.11/11.93 tff(c_46, plain, (![X1_4]: (ld__(b, pet(X1_4))))). % 27.11/11.93 tff(c_686, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_154, plain, (![X1_31]: (ld__(w, pet(X1_31))))). % 27.11/11.93 tff(c_142, plain, (![X1_30]: (ld__(lkg, pet(X1_30))))). % 27.11/11.93 tff(c_100, plain, (![X1_22]: (ld__(cow, h(X1_22))))). % 27.11/11.93 tff(c_260, plain, (![X1_67]: (ld__(k, h(X1_67))))). % 27.11/11.93 tff(c_214, plain, (![X1_46]: (ld__(c, h(X1_46))))). % 27.11/11.93 tff(c_228, plain, (![X1_49]: (ld__(d, h(X1_49))))). % 27.11/11.93 tff(c_2, plain, (p(a, b, c))). % 27.11/11.93 tff(c_10, plain, (p(k, lkg, hill))). % 27.11/11.93 tff(c_98, plain, (![X1_21]: (ld__(aparna, h(X1_21))))). % 27.11/11.93 tff(c_684, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, b) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(Z_70, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.93 tff(c_82, plain, (![X1_7]: (ld__(e, pet(X1_7))))). % 27.11/11.93 tff(c_130, plain, (![X1_29]: (ld__(k, pet(X1_29))))). % 27.11/11.93 tff(c_118, plain, (![X1_28]: (ld__(hill, pet(X1_28))))). % 27.11/11.94 tff(c_256, plain, (![X1_65]: (ld__(hill, h(X1_65))))). % 27.11/11.94 tff(c_12, plain, (p(a, a, a))). % 27.11/11.94 tff(c_194, plain, (![X1_43]: (ld__(b, h(X1_43))))). % 27.11/11.94 tff(c_58, plain, (![X1_5]: (ld__(c, pet(X1_5))))). % 27.11/11.94 tff(c_70, plain, (![X1_6]: (ld__(d, pet(X1_6))))). % 27.11/11.94 tff(c_172, plain, (![X1_38]: (ld__(a, h(X1_38))))). % 27.11/11.94 tff(c_1096, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, c) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(Y_69, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_108, plain, (![X1_27]: (ld__(pig, h(X1_27))))). % 27.11/11.94 tff(c_104, plain, (![X1_24]: (ld__(lilly, h(X1_24))))). % 27.11/11.94 tff(c_102, plain, (![X1_23]: (ld__(horse, h(X1_23))))). % 27.11/11.94 tff(c_34, plain, (![X1_3]: (ld__(a, pet(X1_3))))). % 27.11/11.94 tff(c_32, plain, (ld__(lilly, a))). % 27.11/11.94 tff(c_80, plain, (ld__(lilly, e))). % 27.11/11.94 tff(c_66, plain, (ld__(horse, d))). % 27.11/11.94 tff(c_126, plain, (ld__(horse, k))). % 27.11/11.94 tff(c_48, plain, (ld__(pig, b))). % 27.11/11.94 tff(c_1728, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_52, plain, (ld__(cow, c))). % 27.11/11.94 tff(c_50, plain, (ld__(aparna, c))). % 27.11/11.94 tff(c_64, plain, (ld__(cow, d))). % 27.11/11.94 tff(c_120, plain, (ld__(pig, hill))). % 27.11/11.94 tff(c_116, plain, (ld__(lilly, hill))). % 27.11/11.94 tff(c_68, plain, (ld__(lilly, d))). % 27.11/11.94 tff(c_110, plain, (ld__(aparna, hill))). % 27.11/11.94 tff(c_72, plain, (ld__(pig, d))). % 27.11/11.94 tff(c_74, plain, (ld__(aparna, e))). % 27.11/11.94 tff(c_1730, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_134, plain, (ld__(aparna, lkg))). % 27.11/11.94 tff(c_44, plain, (ld__(lilly, b))). % 27.11/11.94 tff(c_42, plain, (ld__(horse, b))). % 27.11/11.94 tff(c_56, plain, (ld__(lilly, c))). % 27.11/11.94 tff(c_76, plain, (ld__(cow, e))). % 27.11/11.94 tff(c_78, plain, (ld__(horse, e))). % 27.11/11.94 tff(c_112, plain, (ld__(cow, hill))). % 27.11/11.94 tff(c_114, plain, (ld__(horse, hill))). % 27.11/11.94 tff(c_60, plain, (ld__(pig, c))). % 27.11/11.94 tff(c_1726, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(X_68, g(e, e)) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_152, plain, (ld__(lilly, w))). % 27.11/11.94 tff(c_136, plain, (ld__(cow, lkg))). % 27.11/11.94 tff(c_40, plain, (ld__(cow, b))). % 27.11/11.94 tff(c_122, plain, (ld__(aparna, k))). % 27.11/11.94 tff(c_124, plain, (ld__(cow, k))). % 27.11/11.94 tff(c_150, plain, (ld__(horse, w))). % 27.11/11.94 tff(c_144, plain, (ld__(pig, lkg))). % 27.11/11.94 tff(c_128, plain, (ld__(lilly, k))). % 27.11/11.94 tff(c_132, plain, (ld__(pig, k))). % 27.11/11.94 tff(c_1620, plain, (![Y_69, Z_70, X_68]: (~ld__(Y_69, lkg) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_270, plain, (ld__(lkg, k))). % 27.11/11.94 tff(c_138, plain, (ld__(horse, lkg))). % 27.11/11.94 tff(c_166, plain, (ld__(d, a))). % 27.11/11.94 tff(c_30, plain, (ld__(horse, a))). % 27.11/11.94 tff(c_26, plain, (ld__(aparna, a))). % 27.11/11.94 tff(c_140, plain, (ld__(lilly, lkg))). % 27.11/11.94 tff(c_146, plain, (ld__(aparna, w))). % 27.11/11.94 tff(c_62, plain, (ld__(aparna, d))). % 27.11/11.94 tff(c_212, plain, (ld__(k, c))). % 27.11/11.94 tff(c_1674, plain, (![Y_69, X_68, Z_70]: (~ld__(Y_69, lkg) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_28, plain, (ld__(cow, a))). % 27.11/11.94 tff(c_36, plain, (ld__(pig, a))). % 27.11/11.94 tff(c_174, plain, (ld__(k, a))). % 27.11/11.94 tff(c_148, plain, (ld__(cow, w))). % 27.11/11.94 tff(c_54, plain, (ld__(horse, c))). % 27.11/11.94 tff(c_268, plain, (ld__(k, w))). % 27.11/11.94 tff(c_22, plain, (animal(pet(aparna)))). % 27.11/11.94 tff(c_156, plain, (ld__(pig, w))). % 27.11/11.94 tff(c_164, plain, (ld__(w, a))). % 27.11/11.94 tff(c_1618, plain, (![Z_70, X_68, Y_69]: (~ld__(Z_70, hill) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_242, plain, (ld__(k, e))). % 27.11/11.94 tff(c_272, plain, (ld__(lkg, w))). % 27.11/11.94 tff(c_186, plain, (ld__(k, b))). % 27.11/11.94 tff(c_264, plain, (ld__(hill, k))). % 27.11/11.94 tff(c_84, plain, (ld__(pig, e))). % 27.11/11.94 tff(c_168, plain, (ld__(lkg, a))). % 27.11/11.94 tff(c_170, plain, (ld__(a, c))). % 27.11/11.94 tff(c_240, plain, (ld__(hill, e))). % 27.11/11.94 tff(c_266, plain, (ld__(hill, w))). % 27.11/11.94 tff(c_1622, plain, (![X_68, Z_70, Y_69]: (~ld__(X_68, k) | ~ld__(Z_70, b) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_234, plain, (ld__(e, w))). % 27.11/11.94 tff(c_38, plain, (ld__(aparna, b))). % 27.11/11.94 tff(c_188, plain, (ld__(w, b))). % 27.11/11.94 tff(c_176, plain, (ld__(hill, a))). % 27.11/11.94 tff(c_178, plain, (ld__(e, a))). % 27.11/11.94 tff(c_182, plain, (ld__(a, b))). % 27.11/11.94 tff(c_262, plain, (ld__(lkg, hill))). % 27.11/11.94 tff(c_190, plain, (ld__(d, b))). % 27.11/11.94 tff(c_192, plain, (ld__(hill, b))). % 27.11/11.94 tff(c_1676, plain, (![X_68, Y_69, Z_70]: (~ld__(X_68, k) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_230, plain, (ld__(d, e))). % 27.11/11.94 tff(c_196, plain, (ld__(e, b))). % 27.11/11.94 tff(c_224, plain, (ld__(hill, d))). % 27.11/11.94 tff(c_238, plain, (ld__(lkg, e))). % 27.11/11.94 tff(c_198, plain, (ld__(b, c))). % 27.11/11.94 tff(c_200, plain, (ld__(lkg, b))). % 27.11/11.94 tff(c_202, plain, (ld__(w, c))). % 27.11/11.94 tff(c_226, plain, (ld__(d, w))). % 27.11/11.94 tff(c_206, plain, (ld__(lkg, c))). % 27.11/11.94 tff(c_1672, plain, (![Z_70, Y_69, X_68]: (~ld__(Z_70, hill) | ~ld__(Y_69, w) | ~ld__(X_68, h(d)) | ~ld__(X_68, a) | ~p(X_68, Y_69, Z_70)))). % 27.11/11.94 tff(c_222, plain, (ld__(k, d))). % 27.11/11.94 tff(c_218, plain, (ld__(lkg, d))). % 27.11/11.94 tff(c_216, plain, (ld__(hill, c))). % 27.11/11.94 tff(c_208, plain, (ld__(e, c))). % 27.11/11.94 tff(c_210, plain, (ld__(d, c))). % 27.11/11.94 tff(c_14, plain, (flower(lilly))). % 27.11/11.94 tff(c_16, plain, (animal(pig))). % 27.11/11.94 tff(c_18, plain, (animal(horse))). % 27.11/11.94 tff(c_20, plain, (animal(cow))). % 27.11/11.94 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.11/11.94 %------------------------------------------------------------------------------