%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP057-1 : TPTP v9.0.0. Released v2.4.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 : n019.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:48:04 PM UTC 2025 % Result : Satisfiable 35.85s 24.69s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NLP057-1 : TPTP v9.0.0. Released v2.4.0. % 0.04/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.14/0.33 % Computer : n019.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Tue Apr 8 08:18:47 EDT 2025 % 0.14/0.33 % CPUTime : % 35.80/24.68 % 35.85/24.69 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.85/24.69 % 35.85/24.69 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.85/24.70 %$ ssSkP0 > patient > of > member > agent > woman > unisex > thing > substance_matter > specific > singleton > shake_beverage > set > relname > relation > present > possession > past > organism > order > object > nonreflexive > nonliving > nonhuman > nonexistent > multiple > mia_forename > living > impartial > human_person > human > group > general > forename > food > five > female > existent > eventuality > event > entity > dollar > currency > cost > cash > beverage > animate > act > abstraction > actual_world > skf21 > skf10 > skf8 > skf20 > skf18 > skf16 > skf14 > skf12 > #nlpp > skc9 > skc8 > skc7 > skc6 > skc5 % 35.85/24.70 % 35.85/24.70 %Foreground sorts: % 35.85/24.70 % 35.85/24.70 % 35.85/24.70 %Background operators: % 35.85/24.70 % 35.85/24.70 % 35.85/24.70 %Foreground operators: % 35.85/24.70 tff(nonliving, type, nonliving: ($i * $i) > $o). % 35.85/24.70 tff(relation, type, relation: ($i * $i) > $o). % 35.85/24.70 tff(member, type, member: ($i * $i * $i) > $o). % 35.85/24.70 tff(forename, type, forename: ($i * $i) > $o). % 35.85/24.70 tff(skc7, type, skc7: $i). % 35.85/24.70 tff(female, type, female: ($i * $i) > $o). % 35.85/24.70 tff(living, type, living: ($i * $i) > $o). % 35.85/24.70 tff(cost, type, cost: ($i * $i) > $o). % 35.85/24.70 tff(human_person, type, human_person: ($i * $i) > $o). % 35.85/24.70 tff(present, type, present: ($i * $i) > $o). % 35.85/24.70 tff(entity, type, entity: ($i * $i) > $o). % 35.85/24.70 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 35.85/24.70 tff(skc9, type, skc9: $i). % 35.85/24.70 tff(past, type, past: ($i * $i) > $o). % 35.85/24.70 tff(beverage, type, beverage: ($i * $i) > $o). % 35.85/24.70 tff(eventuality, type, eventuality: ($i * $i) > $o). % 35.85/24.70 tff(existent, type, existent: ($i * $i) > $o). % 35.85/24.70 tff(abstraction, type, abstraction: ($i * $i) > $o). % 35.85/24.70 tff(skc8, type, skc8: $i). % 35.85/24.70 tff(relname, type, relname: ($i * $i) > $o). % 35.85/24.70 tff(possession, type, possession: ($i * $i) > $o). % 35.85/24.70 tff(singleton, type, singleton: ($i * $i) > $o). % 35.85/24.70 tff(multiple, type, multiple: ($i * $i) > $o). % 35.85/24.70 tff(organism, type, organism: ($i * $i) > $o). % 35.85/24.70 tff(shake_beverage, type, shake_beverage: ($i * $i) > $o). % 35.85/24.70 tff(animate, type, animate: ($i * $i) > $o). % 35.85/24.70 tff(of, type, of: ($i * $i * $i) > $o). % 35.85/24.70 tff(skf14, type, skf14: ($i * $i) > $i). % 35.85/24.70 tff(actual_world, type, actual_world: $i > $o). % 35.85/24.70 tff(dollar, type, dollar: ($i * $i) > $o). % 35.85/24.70 tff(agent, type, agent: ($i * $i * $i) > $o). % 35.85/24.70 tff(group, type, group: ($i * $i) > $o). % 35.85/24.70 tff(five, type, five: ($i * $i) > $o). % 35.85/24.70 tff(general, type, general: ($i * $i) > $o). % 35.85/24.70 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 35.85/24.70 tff(food, type, food: ($i * $i) > $o). % 35.85/24.70 tff(event, type, event: ($i * $i) > $o). % 35.85/24.70 tff(woman, type, woman: ($i * $i) > $o). % 35.85/24.70 tff(currency, type, currency: ($i * $i) > $o). % 35.85/24.70 tff(patient, type, patient: ($i * $i * $i) > $o). % 35.85/24.70 tff(skf8, type, skf8: ($i * $i) > $i). % 35.85/24.70 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 35.85/24.70 tff(cash, type, cash: ($i * $i) > $o). % 35.85/24.70 tff(thing, type, thing: ($i * $i) > $o). % 35.85/24.70 tff(human, type, human: ($i * $i) > $o). % 35.85/24.70 tff(skf10, type, skf10: ($i * $i * $i) > $i). % 35.85/24.70 tff(skf18, type, skf18: ($i * $i) > $i). % 35.85/24.70 tff(ssSkP0, type, ssSkP0: ($i * $i * $i) > $o). % 35.85/24.70 tff(skc5, type, skc5: $i). % 35.85/24.70 tff(unisex, type, unisex: ($i * $i) > $o). % 35.85/24.70 tff(skf16, type, skf16: ($i * $i) > $i). % 35.85/24.70 tff(set, type, set: ($i * $i) > $o). % 35.85/24.70 tff(skf12, type, skf12: ($i * $i) > $i). % 35.85/24.70 tff(skc6, type, skc6: $i). % 35.85/24.70 tff(impartial, type, impartial: ($i * $i) > $o). % 35.85/24.70 tff(object, type, object: ($i * $i) > $o). % 35.85/24.70 tff(order, type, order: ($i * $i) > $o). % 35.85/24.70 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 35.85/24.70 tff(specific, type, specific: ($i * $i) > $o). % 35.85/24.70 tff(skf20, type, skf20: ($i * $i) > $i). % 35.85/24.70 tff(act, type, act: ($i * $i) > $o). % 35.85/24.70 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 35.85/24.70 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i) > $i). % 35.85/24.70 % 35.85/24.70 %Saturated clause set: % 35.85/24.70 tff(c_1628, plain, (![X_1499, Y_1506, X_1507, X1_1502, V_1508, Z_1512, Y_1497, U_178, X_181, Y_1524, Z_179, V_1509, Y_182, V_1516, X_1523, X1_1518, V_1498, W_1513, Y_1504, X_1522, X1_180, Z_1503, X1_1517, W_177, V_1501, X_1514, V_183, Z_1519, Z_1521, Z_1510, X1_1520, X1_1511, Y_1496]: (skf21(V_1516, X_1499, Y_1524, Z_1521, X1_1520, W_177, U_178)=skf21(V_1501, X_1514, Y_1504, Z_1519, X1_1502, W_177, U_178) | skf21(V_1516, X_1499, Y_1524, Z_1521, X1_1520, W_177, U_178)=skf21(V_1508, X_1507, Y_1496, Z_1512, X1_1511, W_177, U_178) | skf21(V_1508, X_1507, Y_1496, Z_1512, X1_1511, W_177, U_178)=skf21(V_1501, X_1514, Y_1504, Z_1519, X1_1502, W_177, U_178) | skf21(V_1508, X_1507, Y_1496, Z_1512, X1_1511, W_177, U_178)=skf21(V_1498, X_1523, Y_1497, Z_1510, X1_1518, W_177, U_178) | skf21(V_1516, X_1499, Y_1524, Z_1521, X1_1520, W_177, U_178)=skf21(V_1498, X_1523, Y_1497, Z_1510, X1_1518, W_177, U_178) | skf21(V_1501, X_1514, Y_1504, Z_1519, X1_1502, W_177, U_178)=skf21(V_1498, X_1523, Y_1497, Z_1510, X1_1518, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1498, X_1523, Y_1497, Z_1510, X1_1518, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1508, X_1507, Y_1496, Z_1512, X1_1511, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1516, X_1499, Y_1524, Z_1521, X1_1520, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1501, X_1514, Y_1504, Z_1519, X1_1502, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1509, W_1513, X_1522, Y_1506, Z_1503, X1_1517)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1519=X1_1502 | Z_1519=Y_1504 | Y_1504=X1_1502 | Y_1504=X_1514 | Z_1519=X_1514 | X_1514=X1_1502 | X_1514=V_1501 | Y_1504=V_1501 | Z_1519=V_1501 | X1_1502=V_1501 | ~member(U_178, X1_1502, W_177) | ~member(U_178, Z_1519, W_177) | ~member(U_178, Y_1504, W_177) | ~member(U_178, X_1514, W_177) | ~member(U_178, V_1501, W_177) | Z_1521=X1_1520 | Z_1521=Y_1524 | Y_1524=X1_1520 | Y_1524=X_1499 | Z_1521=X_1499 | X_1499=X1_1520 | X_1499=V_1516 | Y_1524=V_1516 | Z_1521=V_1516 | X1_1520=V_1516 | ~member(U_178, X1_1520, W_177) | ~member(U_178, Z_1521, W_177) | ~member(U_178, Y_1524, W_177) | ~member(U_178, X_1499, W_177) | ~member(U_178, V_1516, W_177) | Z_1512=X1_1511 | Z_1512=Y_1496 | Y_1496=X1_1511 | Y_1496=X_1507 | Z_1512=X_1507 | X_1507=X1_1511 | X_1507=V_1508 | Y_1496=V_1508 | Z_1512=V_1508 | X1_1511=V_1508 | ~member(U_178, X1_1511, W_177) | ~member(U_178, Z_1512, W_177) | ~member(U_178, Y_1496, W_177) | ~member(U_178, X_1507, W_177) | ~member(U_178, V_1508, W_177) | Z_1510=X1_1518 | Z_1510=Y_1497 | Y_1497=X1_1518 | Y_1497=X_1523 | Z_1510=X_1523 | X_1523=X1_1518 | X_1523=V_1498 | Y_1497=V_1498 | Z_1510=V_1498 | X1_1518=V_1498 | ~member(U_178, X1_1518, W_177) | ~member(U_178, Z_1510, W_177) | ~member(U_178, Y_1497, W_177) | ~member(U_178, X_1523, W_177) | ~member(U_178, V_1498, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.85/24.71 tff(c_1598, plain, (![Z_1356, Y_1350, X_1360, X1_1355, U_178, X_181, X1_1363, Z_179, X1_1370, V_1362, U_1351, V_1367, X_1372, Y_1359, Y_182, Y_1374, W_1365, X1_1368, V_1361, Y_1357, X1_180, V_1353, X_1366, W_177, V_183, Z_1371, Z_1364, Z_1369, X_1352]: (skf21(V_1367, X_1352, Y_1374, Z_1371, X1_1370, W_177, U_178)=skf21(V_1353, X_1366, Y_1357, Z_1369, X1_1355, W_177, U_178) | skf21(V_1367, X_1352, Y_1374, Z_1371, X1_1370, W_177, U_178)=skf21(V_1361, X_1360, Y_1350, Z_1364, X1_1363, W_177, U_178) | skf21(V_1361, X_1360, Y_1350, Z_1364, X1_1363, W_177, U_178)=skf21(V_1353, X_1366, Y_1357, Z_1369, X1_1355, W_177, U_178) | skf21(V_1361, X_1360, Y_1350, Z_1364, X1_1363, W_177, U_178)=skf10(U_1351, W_177, U_178) | skf21(V_1367, X_1352, Y_1374, Z_1371, X1_1370, W_177, U_178)=skf10(U_1351, W_177, U_178) | skf21(V_1353, X_1366, Y_1357, Z_1369, X1_1355, W_177, U_178)=skf10(U_1351, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1351, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1361, X_1360, Y_1350, Z_1364, X1_1363, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1367, X_1352, Y_1374, Z_1371, X1_1370, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1353, X_1366, Y_1357, Z_1369, X1_1355, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1362, W_1365, X_1372, Y_1359, Z_1356, X1_1368)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1369=X1_1355 | Z_1369=Y_1357 | Y_1357=X1_1355 | Y_1357=X_1366 | Z_1369=X_1366 | X_1366=X1_1355 | X_1366=V_1353 | Y_1357=V_1353 | Z_1369=V_1353 | X1_1355=V_1353 | ~member(U_178, X1_1355, W_177) | ~member(U_178, Z_1369, W_177) | ~member(U_178, Y_1357, W_177) | ~member(U_178, X_1366, W_177) | ~member(U_178, V_1353, W_177) | Z_1371=X1_1370 | Z_1371=Y_1374 | Y_1374=X1_1370 | Y_1374=X_1352 | Z_1371=X_1352 | X_1352=X1_1370 | X_1352=V_1367 | Y_1374=V_1367 | Z_1371=V_1367 | X1_1370=V_1367 | ~member(U_178, X1_1370, W_177) | ~member(U_178, Z_1371, W_177) | ~member(U_178, Y_1374, W_177) | ~member(U_178, X_1352, W_177) | ~member(U_178, V_1367, W_177) | Z_1364=X1_1363 | Z_1364=Y_1350 | Y_1350=X1_1363 | Y_1350=X_1360 | Z_1364=X_1360 | X_1360=X1_1363 | X_1360=V_1361 | Y_1350=V_1361 | Z_1364=V_1361 | X1_1363=V_1361 | ~member(U_178, X1_1363, W_177) | ~member(U_178, Z_1364, W_177) | ~member(U_178, Y_1350, W_177) | ~member(U_178, X_1360, W_177) | ~member(U_178, V_1361, W_177) | ssSkP0(U_1351, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.85/24.71 tff(c_1629, plain, (![X_1499, Y_1506, X_1507, X1_1502, V_1508, W_211, Z_1512, Y_1497, V_210, Y_1524, V_1509, V_1516, X_1523, X1_1518, V_1498, W_1513, Y_1504, X_1522, Z_1503, X1_1517, V_1501, X_1514, Z_1519, Z_1521, Z_1510, X1_1520, U_209, X1_1511, Y_1496]: (skf21(V_1516, X_1499, Y_1524, Z_1521, X1_1520, V_210, W_211)=skf21(V_1501, X_1514, Y_1504, Z_1519, X1_1502, V_210, W_211) | skf21(V_1516, X_1499, Y_1524, Z_1521, X1_1520, V_210, W_211)=skf21(V_1508, X_1507, Y_1496, Z_1512, X1_1511, V_210, W_211) | skf21(V_1508, X_1507, Y_1496, Z_1512, X1_1511, V_210, W_211)=skf21(V_1501, X_1514, Y_1504, Z_1519, X1_1502, V_210, W_211) | skf21(V_1508, X_1507, Y_1496, Z_1512, X1_1511, V_210, W_211)=skf21(V_1498, X_1523, Y_1497, Z_1510, X1_1518, V_210, W_211) | skf21(V_1516, X_1499, Y_1524, Z_1521, X1_1520, V_210, W_211)=skf21(V_1498, X_1523, Y_1497, Z_1510, X1_1518, V_210, W_211) | skf21(V_1501, X_1514, Y_1504, Z_1519, X1_1502, V_210, W_211)=skf21(V_1498, X_1523, Y_1497, Z_1510, X1_1518, V_210, W_211) | skf21(V_1498, X_1523, Y_1497, Z_1510, X1_1518, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1508, X_1507, Y_1496, Z_1512, X1_1511, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1516, X_1499, Y_1524, Z_1521, X1_1520, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1501, X_1514, Y_1504, Z_1519, X1_1502, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1509, W_1513, X_1522, Y_1506, Z_1503, X1_1517)!=skf10(U_209, V_210, W_211) | Z_1519=X1_1502 | Z_1519=Y_1504 | Y_1504=X1_1502 | Y_1504=X_1514 | Z_1519=X_1514 | X_1514=X1_1502 | X_1514=V_1501 | Y_1504=V_1501 | Z_1519=V_1501 | X1_1502=V_1501 | ~member(W_211, X1_1502, V_210) | ~member(W_211, Z_1519, V_210) | ~member(W_211, Y_1504, V_210) | ~member(W_211, X_1514, V_210) | ~member(W_211, V_1501, V_210) | Z_1521=X1_1520 | Z_1521=Y_1524 | Y_1524=X1_1520 | Y_1524=X_1499 | Z_1521=X_1499 | X_1499=X1_1520 | X_1499=V_1516 | Y_1524=V_1516 | Z_1521=V_1516 | X1_1520=V_1516 | ~member(W_211, X1_1520, V_210) | ~member(W_211, Z_1521, V_210) | ~member(W_211, Y_1524, V_210) | ~member(W_211, X_1499, V_210) | ~member(W_211, V_1516, V_210) | Z_1512=X1_1511 | Z_1512=Y_1496 | Y_1496=X1_1511 | Y_1496=X_1507 | Z_1512=X_1507 | X_1507=X1_1511 | X_1507=V_1508 | Y_1496=V_1508 | Z_1512=V_1508 | X1_1511=V_1508 | ~member(W_211, X1_1511, V_210) | ~member(W_211, Z_1512, V_210) | ~member(W_211, Y_1496, V_210) | ~member(W_211, X_1507, V_210) | ~member(W_211, V_1508, V_210) | Z_1510=X1_1518 | Z_1510=Y_1497 | Y_1497=X1_1518 | Y_1497=X_1523 | Z_1510=X_1523 | X_1523=X1_1518 | X_1523=V_1498 | Y_1497=V_1498 | Z_1510=V_1498 | X1_1518=V_1498 | five(W_211, V_210) | ~member(W_211, X1_1518, V_210) | ~member(W_211, Z_1510, V_210) | ~member(W_211, Y_1497, V_210) | ~member(W_211, X_1523, V_210) | ~member(W_211, V_1498, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.85/24.71 tff(c_1573, plain, (![Z_1336, Y_1327, V_1333, V_1347, X1_1343, U_178, U_1342, X_181, Z_179, X_1346, V_1329, Y_182, X_1335, X1_1349, X_1330, X1_180, Z_1340, Y_1334, W_177, V_183, Z_1337, Z_1326, X1_1345, W_1331, Y_1339, Y_1328, X1_1344, X_1348]: (skf21(V_1347, X_1346, Y_1339, Z_1326, X1_1349, W_177, U_178)=skf21(V_1333, X_1335, Y_1327, Z_1336, X1_1345, W_177, U_178) | skf21(V_1333, X_1335, Y_1327, Z_1336, X1_1345, W_177, U_178)=skf21(V_1329, X_1348, Y_1328, Z_1340, X1_1344, W_177, U_178) | skf21(V_1347, X_1346, Y_1339, Z_1326, X1_1349, W_177, U_178)=skf21(V_1329, X_1348, Y_1328, Z_1340, X1_1344, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1329, X_1348, Y_1328, Z_1340, X1_1344, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1333, X_1335, Y_1327, Z_1336, X1_1345, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1347, X_1346, Y_1339, Z_1326, X1_1349, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1342 | skf21(V_1329, X_1348, Y_1328, Z_1340, X1_1344, W_177, U_178)=U_1342 | skf21(V_1333, X_1335, Y_1327, Z_1336, X1_1345, W_177, U_178)=U_1342 | skf21(V_1347, X_1346, Y_1339, Z_1326, X1_1349, W_177, U_178)=U_1342 | ~member(U_178, U_1342, W_177) | skf21(U_1342, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_1331, X_1330, Y_1334, Z_1337, X1_1343)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1326=X1_1349 | Z_1326=Y_1339 | Y_1339=X1_1349 | Y_1339=X_1346 | Z_1326=X_1346 | X_1346=X1_1349 | X_1346=V_1347 | Y_1339=V_1347 | Z_1326=V_1347 | X1_1349=V_1347 | ~member(U_178, X1_1349, W_177) | ~member(U_178, Z_1326, W_177) | ~member(U_178, Y_1339, W_177) | ~member(U_178, X_1346, W_177) | ~member(U_178, V_1347, W_177) | Z_1336=X1_1345 | Z_1336=Y_1327 | Y_1327=X1_1345 | Y_1327=X_1335 | Z_1336=X_1335 | X_1335=X1_1345 | X_1335=V_1333 | Y_1327=V_1333 | Z_1336=V_1333 | X1_1345=V_1333 | ~member(U_178, X1_1345, W_177) | ~member(U_178, Z_1336, W_177) | ~member(U_178, Y_1327, W_177) | ~member(U_178, X_1335, W_177) | ~member(U_178, V_1333, W_177) | Z_1340=X1_1344 | Z_1340=Y_1328 | Y_1328=X1_1344 | Y_1328=X_1348 | Z_1340=X_1348 | X_1348=X1_1344 | X_1348=V_1329 | Y_1328=V_1329 | Z_1340=V_1329 | X1_1344=V_1329 | ~member(U_178, X1_1344, W_177) | ~member(U_178, Z_1340, W_177) | ~member(U_178, Y_1328, W_177) | ~member(U_178, X_1348, W_177) | ~member(U_178, V_1329, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.85/24.71 tff(c_1548, plain, (![X1_1302, Z_1314, V_1305, U_178, X1_1321, W_1308, X1_1313, X_1325, X_181, Z_179, Z_1311, V_1315, Y_182, X_1306, X_1317, Z_1316, Y_1303, X1_180, Y_1318, W_177, Y_1323, X1_1301, V_183, V_1324, V_1309, X_1320, Z_1304, U_1310, Y_1312]: (skf21(V_1324, X_1306, Y_1318, Z_1314, X1_1302, W_177, U_178)=skf21(V_1309, X_1320, Y_1323, Z_1311, X1_1301, W_177, U_178) | skf21(V_1324, X_1306, Y_1318, Z_1314, X1_1302, W_177, U_178)=skf21(V_1305, X_1325, Y_1303, Z_1316, X1_1321, W_177, U_178) | skf21(V_1309, X_1320, Y_1323, Z_1311, X1_1301, W_177, U_178)=skf21(V_1305, X_1325, Y_1303, Z_1316, X1_1321, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1305, X_1325, Y_1303, Z_1316, X1_1321, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1324, X_1306, Y_1318, Z_1314, X1_1302, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1309, X_1320, Y_1323, Z_1311, X1_1301, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1310 | skf21(V_1305, X_1325, Y_1303, Z_1316, X1_1321, W_177, U_178)=U_1310 | skf21(V_1324, X_1306, Y_1318, Z_1314, X1_1302, W_177, U_178)=U_1310 | skf21(V_1309, X_1320, Y_1323, Z_1311, X1_1301, W_177, U_178)=U_1310 | ~member(U_178, U_1310, W_177) | skf21(U_1310, V_1315, W_1308, X_1317, Y_1312, Z_1304, X1_1313)!=U_1310 | Z_1311=X1_1301 | Z_1311=Y_1323 | Y_1323=X1_1301 | Y_1323=X_1320 | Z_1311=X_1320 | X_1320=X1_1301 | X_1320=V_1309 | Y_1323=V_1309 | Z_1311=V_1309 | X1_1301=V_1309 | ~member(U_178, X1_1301, W_177) | ~member(U_178, Z_1311, W_177) | ~member(U_178, Y_1323, W_177) | ~member(U_178, X_1320, W_177) | ~member(U_178, V_1309, W_177) | Z_1314=X1_1302 | Z_1314=Y_1318 | Y_1318=X1_1302 | Y_1318=X_1306 | Z_1314=X_1306 | X_1306=X1_1302 | X_1306=V_1324 | Y_1318=V_1324 | Z_1314=V_1324 | X1_1302=V_1324 | ~member(U_178, X1_1302, W_177) | ~member(U_178, Z_1314, W_177) | ~member(U_178, Y_1318, W_177) | ~member(U_178, X_1306, W_177) | ~member(U_178, V_1324, W_177) | Z_1316=X1_1321 | Z_1316=Y_1303 | Y_1303=X1_1321 | Y_1303=X_1325 | Z_1316=X_1325 | X_1325=X1_1321 | X_1325=V_1305 | Y_1303=V_1305 | Z_1316=V_1305 | X1_1321=V_1305 | ~member(U_178, X1_1321, W_177) | ~member(U_178, Z_1316, W_177) | ~member(U_178, Y_1303, W_177) | ~member(U_178, X_1325, W_177) | ~member(U_178, V_1305, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.85/24.71 tff(c_1518, plain, (![X_1198, U_178, V_1183, Y_1195, Y_1191, X_181, Z_179, Z_1197, V_1193, Y_182, X_1180, Z_1184, Z_1190, X1_1199, V_1181, X1_180, X_1192, W_177, U_1187, V_183, X1_1188, X1_1185, U_1182, Y_1196, W_1179]: (skf21(V_1183, X_1192, Y_1195, Z_1184, X1_1188, W_177, U_178)=skf10(U_1187, W_177, U_178) | skf21(V_1193, X_1198, Y_1196, Z_1190, X1_1199, W_177, U_178)=skf21(V_1183, X_1192, Y_1195, Z_1184, X1_1188, W_177, U_178) | skf21(V_1193, X_1198, Y_1196, Z_1190, X1_1199, W_177, U_178)=skf10(U_1187, W_177, U_178) | skf21(V_1193, X_1198, Y_1196, Z_1190, X1_1199, W_177, U_178)=skf10(U_1182, W_177, U_178) | skf21(V_1183, X_1192, Y_1195, Z_1184, X1_1188, W_177, U_178)=skf10(U_1182, W_177, U_178) | skf10(U_1187, W_177, U_178)=skf10(U_1182, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1182, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1193, X_1198, Y_1196, Z_1190, X1_1199, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1183, X_1192, Y_1195, Z_1184, X1_1188, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1187, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1181, W_1179, X_1180, Y_1191, Z_1197, X1_1185)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_1187, W_177, U_178) | Z_1184=X1_1188 | Z_1184=Y_1195 | Y_1195=X1_1188 | Y_1195=X_1192 | Z_1184=X_1192 | X_1192=X1_1188 | X_1192=V_1183 | Y_1195=V_1183 | Z_1184=V_1183 | X1_1188=V_1183 | ~member(U_178, X1_1188, W_177) | ~member(U_178, Z_1184, W_177) | ~member(U_178, Y_1195, W_177) | ~member(U_178, X_1192, W_177) | ~member(U_178, V_1183, W_177) | Z_1190=X1_1199 | Z_1190=Y_1196 | Y_1196=X1_1199 | Y_1196=X_1198 | Z_1190=X_1198 | X_1198=X1_1199 | X_1198=V_1193 | Y_1196=V_1193 | Z_1190=V_1193 | X1_1199=V_1193 | ~member(U_178, X1_1199, W_177) | ~member(U_178, Z_1190, W_177) | ~member(U_178, Y_1196, W_177) | ~member(U_178, X_1198, W_177) | ~member(U_178, V_1193, W_177) | ssSkP0(U_1182, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.85/24.72 tff(c_1599, plain, (![Z_1356, Y_1350, W_211, X_1360, X1_1355, V_210, X1_1363, X1_1370, V_1362, U_1351, V_1367, X_1372, Y_1359, Y_1374, W_1365, X1_1368, V_1361, Y_1357, V_1353, X_1366, Z_1371, U_209, Z_1364, Z_1369, X_1352]: (skf21(V_1367, X_1352, Y_1374, Z_1371, X1_1370, V_210, W_211)=skf21(V_1353, X_1366, Y_1357, Z_1369, X1_1355, V_210, W_211) | skf21(V_1367, X_1352, Y_1374, Z_1371, X1_1370, V_210, W_211)=skf21(V_1361, X_1360, Y_1350, Z_1364, X1_1363, V_210, W_211) | skf21(V_1361, X_1360, Y_1350, Z_1364, X1_1363, V_210, W_211)=skf21(V_1353, X_1366, Y_1357, Z_1369, X1_1355, V_210, W_211) | skf21(V_1361, X_1360, Y_1350, Z_1364, X1_1363, V_210, W_211)=skf10(U_1351, V_210, W_211) | skf21(V_1367, X_1352, Y_1374, Z_1371, X1_1370, V_210, W_211)=skf10(U_1351, V_210, W_211) | skf21(V_1353, X_1366, Y_1357, Z_1369, X1_1355, V_210, W_211)=skf10(U_1351, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1351, V_210, W_211) | skf21(V_1361, X_1360, Y_1350, Z_1364, X1_1363, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1367, X_1352, Y_1374, Z_1371, X1_1370, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1353, X_1366, Y_1357, Z_1369, X1_1355, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1362, W_1365, X_1372, Y_1359, Z_1356, X1_1368)!=skf10(U_209, V_210, W_211) | Z_1369=X1_1355 | Z_1369=Y_1357 | Y_1357=X1_1355 | Y_1357=X_1366 | Z_1369=X_1366 | X_1366=X1_1355 | X_1366=V_1353 | Y_1357=V_1353 | Z_1369=V_1353 | X1_1355=V_1353 | ~member(W_211, X1_1355, V_210) | ~member(W_211, Z_1369, V_210) | ~member(W_211, Y_1357, V_210) | ~member(W_211, X_1366, V_210) | ~member(W_211, V_1353, V_210) | Z_1371=X1_1370 | Z_1371=Y_1374 | Y_1374=X1_1370 | Y_1374=X_1352 | Z_1371=X_1352 | X_1352=X1_1370 | X_1352=V_1367 | Y_1374=V_1367 | Z_1371=V_1367 | X1_1370=V_1367 | ~member(W_211, X1_1370, V_210) | ~member(W_211, Z_1371, V_210) | ~member(W_211, Y_1374, V_210) | ~member(W_211, X_1352, V_210) | ~member(W_211, V_1367, V_210) | Z_1364=X1_1363 | Z_1364=Y_1350 | Y_1350=X1_1363 | Y_1350=X_1360 | Z_1364=X_1360 | X_1360=X1_1363 | X_1360=V_1361 | Y_1350=V_1361 | Z_1364=V_1361 | X1_1363=V_1361 | five(W_211, V_210) | ~member(W_211, X1_1363, V_210) | ~member(W_211, Z_1364, V_210) | ~member(W_211, Y_1350, V_210) | ~member(W_211, X_1360, V_210) | ~member(W_211, V_1361, V_210) | ssSkP0(U_1351, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 35.85/24.72 tff(c_1491, plain, (![Z_1129, U_178, X_181, V_1133, Z_179, U_1139, W_1124, X1_1135, X_1138, Y_182, Z_1134, Y_1131, X1_1128, X_1136, X_1137, X1_180, W_177, U_1122, X1_1127, V_183, Y_1123, Y_1141, Z_1140, V_1125]: (skf21(V_1133, X_1138, Y_1131, Z_1134, X1_1127, W_177, U_178)=skf10(U_1139, W_177, U_178) | skf21(V_1125, X_1136, Y_1123, Z_1129, X1_1135, W_177, U_178)=skf10(U_1139, W_177, U_178) | skf21(V_1133, X_1138, Y_1131, Z_1134, X1_1127, W_177, U_178)=skf21(V_1125, X_1136, Y_1123, Z_1129, X1_1135, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1125, X_1136, Y_1123, Z_1129, X1_1135, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1139, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1133, X_1138, Y_1131, Z_1134, X1_1127, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1122 | skf21(V_1125, X_1136, Y_1123, Z_1129, X1_1135, W_177, U_178)=U_1122 | skf10(U_1139, W_177, U_178)=U_1122 | skf21(V_1133, X_1138, Y_1131, Z_1134, X1_1127, W_177, U_178)=U_1122 | ~member(U_178, U_1122, W_177) | skf21(U_1122, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_1124, X_1137, Y_1141, Z_1140, X1_1128)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1134=X1_1127 | Z_1134=Y_1131 | Y_1131=X1_1127 | Y_1131=X_1138 | Z_1134=X_1138 | X_1138=X1_1127 | X_1138=V_1133 | Y_1131=V_1133 | Z_1134=V_1133 | X1_1127=V_1133 | ~member(U_178, X1_1127, W_177) | ~member(U_178, Z_1134, W_177) | ~member(U_178, Y_1131, W_177) | ~member(U_178, X_1138, W_177) | ~member(U_178, V_1133, W_177) | ssSkP0(U_1139, W_177, U_178) | Z_1129=X1_1135 | Z_1129=Y_1123 | Y_1123=X1_1135 | Y_1123=X_1136 | Z_1129=X_1136 | X_1136=X1_1135 | X_1136=V_1125 | Y_1123=V_1125 | Z_1129=V_1125 | X1_1135=V_1125 | ~member(U_178, X1_1135, W_177) | ~member(U_178, Z_1129, W_177) | ~member(U_178, Y_1123, W_177) | ~member(U_178, X_1136, W_177) | ~member(U_178, V_1125, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.85/24.72 tff(c_1574, plain, (![Z_1336, Y_1327, V_1333, W_211, V_1347, V_210, X1_1343, U_1342, X_1346, V_1329, X_1335, X1_1349, X_1330, Z_1340, Y_1334, Z_1337, Z_1326, X1_1345, W_1331, Y_1339, Y_1328, X1_1344, U_209, X_1348]: (skf21(V_1347, X_1346, Y_1339, Z_1326, X1_1349, V_210, W_211)=skf21(V_1333, X_1335, Y_1327, Z_1336, X1_1345, V_210, W_211) | skf21(V_1333, X_1335, Y_1327, Z_1336, X1_1345, V_210, W_211)=skf21(V_1329, X_1348, Y_1328, Z_1340, X1_1344, V_210, W_211) | skf21(V_1347, X_1346, Y_1339, Z_1326, X1_1349, V_210, W_211)=skf21(V_1329, X_1348, Y_1328, Z_1340, X1_1344, V_210, W_211) | skf21(V_1329, X_1348, Y_1328, Z_1340, X1_1344, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1333, X_1335, Y_1327, Z_1336, X1_1345, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1347, X_1346, Y_1339, Z_1326, X1_1349, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1342 | skf21(V_1329, X_1348, Y_1328, Z_1340, X1_1344, V_210, W_211)=U_1342 | skf21(V_1333, X_1335, Y_1327, Z_1336, X1_1345, V_210, W_211)=U_1342 | skf21(V_1347, X_1346, Y_1339, Z_1326, X1_1349, V_210, W_211)=U_1342 | ~member(W_211, U_1342, V_210) | skf21(U_1342, skf10(U_209, V_210, W_211), W_1331, X_1330, Y_1334, Z_1337, X1_1343)!=skf10(U_209, V_210, W_211) | Z_1326=X1_1349 | Z_1326=Y_1339 | Y_1339=X1_1349 | Y_1339=X_1346 | Z_1326=X_1346 | X_1346=X1_1349 | X_1346=V_1347 | Y_1339=V_1347 | Z_1326=V_1347 | X1_1349=V_1347 | ~member(W_211, X1_1349, V_210) | ~member(W_211, Z_1326, V_210) | ~member(W_211, Y_1339, V_210) | ~member(W_211, X_1346, V_210) | ~member(W_211, V_1347, V_210) | Z_1336=X1_1345 | Z_1336=Y_1327 | Y_1327=X1_1345 | Y_1327=X_1335 | Z_1336=X_1335 | X_1335=X1_1345 | X_1335=V_1333 | Y_1327=V_1333 | Z_1336=V_1333 | X1_1345=V_1333 | ~member(W_211, X1_1345, V_210) | ~member(W_211, Z_1336, V_210) | ~member(W_211, Y_1327, V_210) | ~member(W_211, X_1335, V_210) | ~member(W_211, V_1333, V_210) | Z_1340=X1_1344 | Z_1340=Y_1328 | Y_1328=X1_1344 | Y_1328=X_1348 | Z_1340=X_1348 | X_1348=X1_1344 | X_1348=V_1329 | Y_1328=V_1329 | Z_1340=V_1329 | X1_1344=V_1329 | five(W_211, V_210) | ~member(W_211, X1_1344, V_210) | ~member(W_211, Z_1340, V_210) | ~member(W_211, Y_1328, V_210) | ~member(W_211, X_1348, V_210) | ~member(W_211, V_1329, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.85/24.72 tff(c_1441, plain, (![V_1097, X1_1089, X1_1096, Z_1090, U_178, X_181, Z_179, X_1085, X1_1095, X_1099, Z_1093, Y_182, V_1084, Y_1082, X_1098, X1_180, Y_1088, W_177, V_183, Y_1083, Z_1100, U_1092, V_1087]: (skf21(V_1087, X_1098, Y_1088, Z_1100, X1_1089, W_177, U_178)=skf21(V_1084, X_1099, Y_1083, Z_1093, X1_1095, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1084, X_1099, Y_1083, Z_1093, X1_1095, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1087, X_1098, Y_1088, Z_1100, X1_1089, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_1097 | skf21(V_1084, X_1099, Y_1083, Z_1093, X1_1095, W_177, U_178)=V_1097 | skf21(V_1087, X_1098, Y_1088, Z_1100, X1_1089, W_177, U_178)=V_1097 | V_1097=U_1092 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1092 | skf21(V_1084, X_1099, Y_1083, Z_1093, X1_1095, W_177, U_178)=U_1092 | skf21(V_1087, X_1098, Y_1088, Z_1100, X1_1089, W_177, U_178)=U_1092 | ~member(U_178, V_1097, W_177) | ~member(U_178, U_1092, W_177) | skf21(U_1092, V_1097, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_1085, Y_1082, Z_1090, X1_1096)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1100=X1_1089 | Z_1100=Y_1088 | Y_1088=X1_1089 | Y_1088=X_1098 | Z_1100=X_1098 | X_1098=X1_1089 | X_1098=V_1087 | Y_1088=V_1087 | Z_1100=V_1087 | X1_1089=V_1087 | ~member(U_178, X1_1089, W_177) | ~member(U_178, Z_1100, W_177) | ~member(U_178, Y_1088, W_177) | ~member(U_178, X_1098, W_177) | ~member(U_178, V_1087, W_177) | Z_1093=X1_1095 | Z_1093=Y_1083 | Y_1083=X1_1095 | Y_1083=X_1099 | Z_1093=X_1099 | X_1099=X1_1095 | X_1099=V_1084 | Y_1083=V_1084 | Z_1093=V_1084 | X1_1095=V_1084 | ~member(U_178, X1_1095, W_177) | ~member(U_178, Z_1093, W_177) | ~member(U_178, Y_1083, W_177) | ~member(U_178, X_1099, W_177) | ~member(U_178, V_1084, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.85/24.72 tff(c_1549, plain, (![X1_1302, Z_1314, W_211, V_210, V_1305, X1_1321, W_1308, X1_1313, X_1325, Z_1311, V_1315, X_1306, X_1317, Z_1316, Y_1303, Y_1318, Y_1323, X1_1301, V_1324, V_1309, U_209, X_1320, Z_1304, U_1310, Y_1312]: (skf21(V_1324, X_1306, Y_1318, Z_1314, X1_1302, V_210, W_211)=skf21(V_1309, X_1320, Y_1323, Z_1311, X1_1301, V_210, W_211) | skf21(V_1324, X_1306, Y_1318, Z_1314, X1_1302, V_210, W_211)=skf21(V_1305, X_1325, Y_1303, Z_1316, X1_1321, V_210, W_211) | skf21(V_1309, X_1320, Y_1323, Z_1311, X1_1301, V_210, W_211)=skf21(V_1305, X_1325, Y_1303, Z_1316, X1_1321, V_210, W_211) | skf21(V_1305, X_1325, Y_1303, Z_1316, X1_1321, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1324, X_1306, Y_1318, Z_1314, X1_1302, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1309, X_1320, Y_1323, Z_1311, X1_1301, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1310 | skf21(V_1305, X_1325, Y_1303, Z_1316, X1_1321, V_210, W_211)=U_1310 | skf21(V_1324, X_1306, Y_1318, Z_1314, X1_1302, V_210, W_211)=U_1310 | skf21(V_1309, X_1320, Y_1323, Z_1311, X1_1301, V_210, W_211)=U_1310 | ~member(W_211, U_1310, V_210) | skf21(U_1310, V_1315, W_1308, X_1317, Y_1312, Z_1304, X1_1313)!=U_1310 | Z_1311=X1_1301 | Z_1311=Y_1323 | Y_1323=X1_1301 | Y_1323=X_1320 | Z_1311=X_1320 | X_1320=X1_1301 | X_1320=V_1309 | Y_1323=V_1309 | Z_1311=V_1309 | X1_1301=V_1309 | ~member(W_211, X1_1301, V_210) | ~member(W_211, Z_1311, V_210) | ~member(W_211, Y_1323, V_210) | ~member(W_211, X_1320, V_210) | ~member(W_211, V_1309, V_210) | Z_1314=X1_1302 | Z_1314=Y_1318 | Y_1318=X1_1302 | Y_1318=X_1306 | Z_1314=X_1306 | X_1306=X1_1302 | X_1306=V_1324 | Y_1318=V_1324 | Z_1314=V_1324 | X1_1302=V_1324 | ~member(W_211, X1_1302, V_210) | ~member(W_211, Z_1314, V_210) | ~member(W_211, Y_1318, V_210) | ~member(W_211, X_1306, V_210) | ~member(W_211, V_1324, V_210) | Z_1316=X1_1321 | Z_1316=Y_1303 | Y_1303=X1_1321 | Y_1303=X_1325 | Z_1316=X_1325 | X_1325=X1_1321 | X_1325=V_1305 | Y_1303=V_1305 | Z_1316=V_1305 | X1_1321=V_1305 | five(W_211, V_210) | ~member(W_211, X1_1321, V_210) | ~member(W_211, Z_1316, V_210) | ~member(W_211, Y_1303, V_210) | ~member(W_211, X_1325, V_210) | ~member(W_211, V_1305, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.72 tff(c_1416, plain, (![Y_1080, U_1067, W_1079, U_178, X1_1078, V_1064, X_181, Z_179, V_1069, Y_1081, Z_1071, Y_182, X_1062, Z_1070, X_1077, Z_1076, X1_1068, Y_1063, X1_180, W_177, V_183, X_1065, X1_1075, V_1072]: (skf21(V_1072, X_1062, Y_1081, Z_1071, X1_1068, W_177, U_178)=skf21(V_1064, X_1077, Y_1063, Z_1070, X1_1075, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1064, X_1077, Y_1063, Z_1070, X1_1075, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1072, X_1062, Y_1081, Z_1071, X1_1068, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_1069 | skf21(V_1064, X_1077, Y_1063, Z_1070, X1_1075, W_177, U_178)=V_1069 | skf21(V_1072, X_1062, Y_1081, Z_1071, X1_1068, W_177, U_178)=V_1069 | V_1069=U_1067 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1067 | skf21(V_1064, X_1077, Y_1063, Z_1070, X1_1075, W_177, U_178)=U_1067 | skf21(V_1072, X_1062, Y_1081, Z_1071, X1_1068, W_177, U_178)=U_1067 | ~member(U_178, V_1069, W_177) | ~member(U_178, U_1067, W_177) | skf21(U_1067, V_1069, W_1079, X_1065, Y_1080, Z_1076, X1_1078)!=V_1069 | Z_1071=X1_1068 | Z_1071=Y_1081 | Y_1081=X1_1068 | Y_1081=X_1062 | Z_1071=X_1062 | X_1062=X1_1068 | X_1062=V_1072 | Y_1081=V_1072 | Z_1071=V_1072 | X1_1068=V_1072 | ~member(U_178, X1_1068, W_177) | ~member(U_178, Z_1071, W_177) | ~member(U_178, Y_1081, W_177) | ~member(U_178, X_1062, W_177) | ~member(U_178, V_1072, W_177) | Z_1070=X1_1075 | Z_1070=Y_1063 | Y_1063=X1_1075 | Y_1063=X_1077 | Z_1070=X_1077 | X_1077=X1_1075 | X_1077=V_1064 | Y_1063=V_1064 | Z_1070=V_1064 | X1_1075=V_1064 | ~member(U_178, X1_1075, W_177) | ~member(U_178, Z_1070, W_177) | ~member(U_178, Y_1063, W_177) | ~member(U_178, X_1077, W_177) | ~member(U_178, V_1064, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1388, plain, (![X_1010, U_178, V_1011, X_996, X_181, Z_179, Y_1002, X1_1006, X1_1001, Y_182, Y_992, V_991, Z_1000, V_993, X_994, X1_1009, Z_1007, W_997, Y_1004, X1_180, W_177, X4_995, V_183, Z_1005, U_999]: (skf21(V_993, X_1010, Y_992, Z_1007, X1_1009, W_177, U_178)=skf21(V_991, X_996, Y_1002, Z_1005, X1_1001, W_177, U_178) | skf21(V_993, X_1010, Y_992, Z_1007, X1_1009, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_991, X_996, Y_1002, Z_1005, X1_1001, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_995 | skf21(V_993, X_1010, Y_992, Z_1007, X1_1009, W_177, U_178)=X4_995 | skf21(V_991, X_996, Y_1002, Z_1005, X1_1001, W_177, U_178)=X4_995 | X4_995=U_999 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_999 | skf21(V_993, X_1010, Y_992, Z_1007, X1_1009, W_177, U_178)=U_999 | skf21(V_991, X_996, Y_1002, Z_1005, X1_1001, W_177, U_178)=U_999 | ~member(U_178, X4_995, W_177) | ~member(U_178, U_999, W_177) | skf21(U_999, V_1011, W_997, X_994, Y_1004, Z_1000, X1_1006)!=U_999 | Z_1005=X1_1001 | Z_1005=Y_1002 | Y_1002=X1_1001 | Y_1002=X_996 | Z_1005=X_996 | X_996=X1_1001 | X_996=V_991 | Y_1002=V_991 | Z_1005=V_991 | X1_1001=V_991 | ~member(U_178, X1_1001, W_177) | ~member(U_178, Z_1005, W_177) | ~member(U_178, Y_1002, W_177) | ~member(U_178, X_996, W_177) | ~member(U_178, V_991, W_177) | Z_1007=X1_1009 | Z_1007=Y_992 | Y_992=X1_1009 | Y_992=X_1010 | Z_1007=X_1010 | X_1010=X1_1009 | X_1010=V_993 | Y_992=V_993 | Z_1007=V_993 | X1_1009=V_993 | ~member(U_178, X1_1009, W_177) | ~member(U_178, Z_1007, W_177) | ~member(U_178, Y_992, W_177) | ~member(U_178, X_1010, W_177) | ~member(U_178, V_993, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1361, plain, (![U_946, U_178, Z_955, V_952, X_181, U_944, Z_179, Y_958, X_949, Y_182, X_957, Y_959, X1_180, V_943, W_177, X1_950, Z_948, V_183, X1_954, U_951, W_945]: (skf21(V_952, X_949, Y_958, Z_955, X1_954, W_177, U_178)=skf10(U_951, W_177, U_178) | skf21(V_952, X_949, Y_958, Z_955, X1_954, W_177, U_178)=skf10(U_944, W_177, U_178) | skf10(U_951, W_177, U_178)=skf10(U_944, W_177, U_178) | skf10(U_946, W_177, U_178)=skf10(U_944, W_177, U_178) | skf21(V_952, X_949, Y_958, Z_955, X1_954, W_177, U_178)=skf10(U_946, W_177, U_178) | skf10(U_951, W_177, U_178)=skf10(U_946, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_946, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_944, W_177, U_178) | skf21(V_952, X_949, Y_958, Z_955, X1_954, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_951, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_943, W_945, X_957, Y_959, Z_948, X1_950)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_951, W_177, U_178) | Z_955=X1_954 | Z_955=Y_958 | Y_958=X1_954 | Y_958=X_949 | Z_955=X_949 | X_949=X1_954 | X_949=V_952 | Y_958=V_952 | Z_955=V_952 | X1_954=V_952 | ~member(U_178, X1_954, W_177) | ~member(U_178, Z_955, W_177) | ~member(U_178, Y_958, W_177) | ~member(U_178, X_949, W_177) | ~member(U_178, V_952, W_177) | ssSkP0(U_944, W_177, U_178) | ssSkP0(U_946, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1519, plain, (![W_211, X_1198, V_210, V_1183, Y_1195, Y_1191, Z_1197, V_1193, X_1180, Z_1184, Z_1190, X1_1199, V_1181, X_1192, U_1187, X1_1188, X1_1185, U_1182, Y_1196, U_209, W_1179]: (skf21(V_1183, X_1192, Y_1195, Z_1184, X1_1188, V_210, W_211)=skf10(U_1187, V_210, W_211) | skf21(V_1193, X_1198, Y_1196, Z_1190, X1_1199, V_210, W_211)=skf21(V_1183, X_1192, Y_1195, Z_1184, X1_1188, V_210, W_211) | skf21(V_1193, X_1198, Y_1196, Z_1190, X1_1199, V_210, W_211)=skf10(U_1187, V_210, W_211) | skf21(V_1193, X_1198, Y_1196, Z_1190, X1_1199, V_210, W_211)=skf10(U_1182, V_210, W_211) | skf21(V_1183, X_1192, Y_1195, Z_1184, X1_1188, V_210, W_211)=skf10(U_1182, V_210, W_211) | skf10(U_1187, V_210, W_211)=skf10(U_1182, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1182, V_210, W_211) | skf21(V_1193, X_1198, Y_1196, Z_1190, X1_1199, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1183, X_1192, Y_1195, Z_1184, X1_1188, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1187, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1181, W_1179, X_1180, Y_1191, Z_1197, X1_1185)!=skf10(U_209, V_210, W_211) | ssSkP0(U_1187, V_210, W_211) | Z_1184=X1_1188 | Z_1184=Y_1195 | Y_1195=X1_1188 | Y_1195=X_1192 | Z_1184=X_1192 | X_1192=X1_1188 | X_1192=V_1183 | Y_1195=V_1183 | Z_1184=V_1183 | X1_1188=V_1183 | ~member(W_211, X1_1188, V_210) | ~member(W_211, Z_1184, V_210) | ~member(W_211, Y_1195, V_210) | ~member(W_211, X_1192, V_210) | ~member(W_211, V_1183, V_210) | Z_1190=X1_1199 | Z_1190=Y_1196 | Y_1196=X1_1199 | Y_1196=X_1198 | Z_1190=X_1198 | X_1198=X1_1199 | X_1198=V_1193 | Y_1196=V_1193 | Z_1190=V_1193 | X1_1199=V_1193 | five(W_211, V_210) | ~member(W_211, X1_1199, V_210) | ~member(W_211, Z_1190, V_210) | ~member(W_211, Y_1196, V_210) | ~member(W_211, X_1198, V_210) | ~member(W_211, V_1193, V_210) | ssSkP0(U_1182, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.72 tff(c_1310, plain, (![U_895, U_897, Y_910, U_178, Y_902, X_181, Z_179, Z_909, Y_182, X1_899, U_908, W_896, X1_180, W_177, V_903, V_183, X_907, X1_900, X_906, Z_904]: (skf21(V_903, X_907, Y_902, Z_904, X1_899, W_177, U_178)=skf10(U_908, W_177, U_178) | skf10(U_908, W_177, U_178)=skf10(U_897, W_177, U_178) | skf21(V_903, X_907, Y_902, Z_904, X1_899, W_177, U_178)=skf10(U_897, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_897, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_908, W_177, U_178) | skf21(V_903, X_907, Y_902, Z_904, X1_899, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_895 | skf10(U_897, W_177, U_178)=U_895 | skf10(U_908, W_177, U_178)=U_895 | skf21(V_903, X_907, Y_902, Z_904, X1_899, W_177, U_178)=U_895 | ~member(U_178, U_895, W_177) | skf21(U_895, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_896, X_906, Y_910, Z_909, X1_900)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_904=X1_899 | Z_904=Y_902 | Y_902=X1_899 | Y_902=X_907 | Z_904=X_907 | X_907=X1_899 | X_907=V_903 | Y_902=V_903 | Z_904=V_903 | X1_899=V_903 | ~member(U_178, X1_899, W_177) | ~member(U_178, Z_904, W_177) | ~member(U_178, Y_902, W_177) | ~member(U_178, X_907, W_177) | ~member(U_178, V_903, W_177) | ssSkP0(U_908, W_177, U_178) | ssSkP0(U_897, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1492, plain, (![Z_1129, W_211, V_210, V_1133, U_1139, W_1124, X1_1135, X_1138, Z_1134, Y_1131, X1_1128, X_1136, X_1137, U_1122, X1_1127, Y_1123, Y_1141, Z_1140, V_1125, U_209]: (skf21(V_1133, X_1138, Y_1131, Z_1134, X1_1127, V_210, W_211)=skf10(U_1139, V_210, W_211) | skf21(V_1125, X_1136, Y_1123, Z_1129, X1_1135, V_210, W_211)=skf10(U_1139, V_210, W_211) | skf21(V_1133, X_1138, Y_1131, Z_1134, X1_1127, V_210, W_211)=skf21(V_1125, X_1136, Y_1123, Z_1129, X1_1135, V_210, W_211) | skf21(V_1125, X_1136, Y_1123, Z_1129, X1_1135, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1139, V_210, W_211) | skf21(V_1133, X_1138, Y_1131, Z_1134, X1_1127, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1122 | skf21(V_1125, X_1136, Y_1123, Z_1129, X1_1135, V_210, W_211)=U_1122 | skf10(U_1139, V_210, W_211)=U_1122 | skf21(V_1133, X_1138, Y_1131, Z_1134, X1_1127, V_210, W_211)=U_1122 | ~member(W_211, U_1122, V_210) | skf21(U_1122, skf10(U_209, V_210, W_211), W_1124, X_1137, Y_1141, Z_1140, X1_1128)!=skf10(U_209, V_210, W_211) | Z_1134=X1_1127 | Z_1134=Y_1131 | Y_1131=X1_1127 | Y_1131=X_1138 | Z_1134=X_1138 | X_1138=X1_1127 | X_1138=V_1133 | Y_1131=V_1133 | Z_1134=V_1133 | X1_1127=V_1133 | ~member(W_211, X1_1127, V_210) | ~member(W_211, Z_1134, V_210) | ~member(W_211, Y_1131, V_210) | ~member(W_211, X_1138, V_210) | ~member(W_211, V_1133, V_210) | ssSkP0(U_1139, V_210, W_211) | Z_1129=X1_1135 | Z_1129=Y_1123 | Y_1123=X1_1135 | Y_1123=X_1136 | Z_1129=X_1136 | X_1136=X1_1135 | X_1136=V_1125 | Y_1123=V_1125 | Z_1129=V_1125 | X1_1135=V_1125 | five(W_211, V_210) | ~member(W_211, X1_1135, V_210) | ~member(W_211, Z_1129, V_210) | ~member(W_211, Y_1123, V_210) | ~member(W_211, X_1136, V_210) | ~member(W_211, V_1125, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.72 tff(c_1257, plain, (![X_825, X_836, U_824, U_178, X_181, Z_179, U_832, Z_830, X1_833, V_827, Y_828, Y_182, X1_829, Z_837, V_834, X1_180, W_177, V_183, Y_823]: (skf21(V_827, X_836, Y_828, Z_837, X1_829, W_177, U_178)=skf10(U_824, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_824, W_177, U_178) | skf21(V_827, X_836, Y_828, Z_837, X1_829, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_834 | skf10(U_824, W_177, U_178)=V_834 | skf21(V_827, X_836, Y_828, Z_837, X1_829, W_177, U_178)=V_834 | V_834=U_832 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_832 | skf10(U_824, W_177, U_178)=U_832 | skf21(V_827, X_836, Y_828, Z_837, X1_829, W_177, U_178)=U_832 | ~member(U_178, V_834, W_177) | ~member(U_178, U_832, W_177) | skf21(U_832, V_834, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_825, Y_823, Z_830, X1_833)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_837=X1_829 | Z_837=Y_828 | Y_828=X1_829 | Y_828=X_836 | Z_837=X_836 | X_836=X1_829 | X_836=V_827 | Y_828=V_827 | Z_837=V_827 | X1_829=V_827 | ~member(U_178, X1_829, W_177) | ~member(U_178, Z_837, W_177) | ~member(U_178, Y_828, W_177) | ~member(U_178, X_836, W_177) | ~member(U_178, V_827, W_177) | ssSkP0(U_824, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1467, plain, (![Z_1105, X1_1113, Z_1101, Y_1102, U_1121, W_211, V_210, V_1117, U_1108, X1_1115, X1_1111, Z_1112, V_1120, Y_1116, X_1104, Y_1109, X_1107, X_1118, U_209, V_1103, W_1119]: (skf21(V_1117, X_1104, Y_1109, Z_1101, X1_1111, V_210, W_211)=skf10(U_1121, V_210, W_211) | skf21(V_1117, X_1104, Y_1109, Z_1101, X1_1111, V_210, W_211)=skf21(V_1103, X_1118, Y_1102, Z_1112, X1_1115, V_210, W_211) | skf21(V_1103, X_1118, Y_1102, Z_1112, X1_1115, V_210, W_211)=skf10(U_1121, V_210, W_211) | skf21(V_1103, X_1118, Y_1102, Z_1112, X1_1115, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1117, X_1104, Y_1109, Z_1101, X1_1111, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1121, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1108 | skf21(V_1103, X_1118, Y_1102, Z_1112, X1_1115, V_210, W_211)=U_1108 | skf21(V_1117, X_1104, Y_1109, Z_1101, X1_1111, V_210, W_211)=U_1108 | skf10(U_1121, V_210, W_211)=U_1108 | ~member(W_211, U_1108, V_210) | skf21(U_1108, V_1120, W_1119, X_1107, Y_1116, Z_1105, X1_1113)!=U_1108 | ssSkP0(U_1121, V_210, W_211) | Z_1101=X1_1111 | Z_1101=Y_1109 | Y_1109=X1_1111 | Y_1109=X_1104 | Z_1101=X_1104 | X_1104=X1_1111 | X_1104=V_1117 | Y_1109=V_1117 | Z_1101=V_1117 | X1_1111=V_1117 | ~member(W_211, X1_1111, V_210) | ~member(W_211, Z_1101, V_210) | ~member(W_211, Y_1109, V_210) | ~member(W_211, X_1104, V_210) | ~member(W_211, V_1117, V_210) | Z_1112=X1_1115 | Z_1112=Y_1102 | Y_1102=X1_1115 | Y_1102=X_1118 | Z_1112=X_1118 | X_1118=X1_1115 | X_1118=V_1103 | Y_1102=V_1103 | Z_1112=V_1103 | X1_1115=V_1103 | five(W_211, V_210) | ~member(W_211, X1_1115, V_210) | ~member(W_211, Z_1112, V_210) | ~member(W_211, Y_1102, V_210) | ~member(W_211, X_1118, V_210) | ~member(W_211, V_1103, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.72 tff(c_1442, plain, (![V_1097, X1_1089, X1_1096, W_211, Z_1090, V_210, X_1085, X1_1095, X_1099, Z_1093, V_1084, Y_1082, X_1098, Y_1088, Y_1083, Z_1100, U_209, U_1092, V_1087]: (skf21(V_1087, X_1098, Y_1088, Z_1100, X1_1089, V_210, W_211)=skf21(V_1084, X_1099, Y_1083, Z_1093, X1_1095, V_210, W_211) | skf21(V_1084, X_1099, Y_1083, Z_1093, X1_1095, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1087, X_1098, Y_1088, Z_1100, X1_1089, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_1097 | skf21(V_1084, X_1099, Y_1083, Z_1093, X1_1095, V_210, W_211)=V_1097 | skf21(V_1087, X_1098, Y_1088, Z_1100, X1_1089, V_210, W_211)=V_1097 | V_1097=U_1092 | skf10(U_209, V_210, W_211)=U_1092 | skf21(V_1084, X_1099, Y_1083, Z_1093, X1_1095, V_210, W_211)=U_1092 | skf21(V_1087, X_1098, Y_1088, Z_1100, X1_1089, V_210, W_211)=U_1092 | ~member(W_211, V_1097, V_210) | ~member(W_211, U_1092, V_210) | skf21(U_1092, V_1097, skf10(U_209, V_210, W_211), X_1085, Y_1082, Z_1090, X1_1096)!=skf10(U_209, V_210, W_211) | Z_1100=X1_1089 | Z_1100=Y_1088 | Y_1088=X1_1089 | Y_1088=X_1098 | Z_1100=X_1098 | X_1098=X1_1089 | X_1098=V_1087 | Y_1088=V_1087 | Z_1100=V_1087 | X1_1089=V_1087 | ~member(W_211, X1_1089, V_210) | ~member(W_211, Z_1100, V_210) | ~member(W_211, Y_1088, V_210) | ~member(W_211, X_1098, V_210) | ~member(W_211, V_1087, V_210) | Z_1093=X1_1095 | Z_1093=Y_1083 | Y_1083=X1_1095 | Y_1083=X_1099 | Z_1093=X_1099 | X_1099=X1_1095 | X_1099=V_1084 | Y_1083=V_1084 | Z_1093=V_1084 | X1_1095=V_1084 | five(W_211, V_210) | ~member(W_211, X1_1095, V_210) | ~member(W_211, Z_1093, V_210) | ~member(W_211, Y_1083, V_210) | ~member(W_211, X_1099, V_210) | ~member(W_211, V_1084, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.72 tff(c_1156, plain, (![V_757, U_178, U_752, X_181, Y_748, Z_179, V_756, X1_759, Y_182, Y_751, W_747, X1_180, X_755, W_177, Z_753, V_183, Z_760, X1_750]: (skf21(V_756, X_755, Y_748, Z_753, X1_750, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_747 | skf21(V_756, X_755, Y_748, Z_753, X1_750, W_177, U_178)=W_747 | W_747=V_757 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_757 | skf21(V_756, X_755, Y_748, Z_753, X1_750, W_177, U_178)=V_757 | V_757=U_752 | W_747=U_752 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_752 | skf21(V_756, X_755, Y_748, Z_753, X1_750, W_177, U_178)=U_752 | ~member(U_178, W_747, W_177) | ~member(U_178, V_757, W_177) | ~member(U_178, U_752, W_177) | skf21(U_752, V_757, W_747, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), Y_751, Z_760, X1_759)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_753=X1_750 | Z_753=Y_748 | Y_748=X1_750 | Y_748=X_755 | Z_753=X_755 | X_755=X1_750 | X_755=V_756 | Y_748=V_756 | Z_753=V_756 | X1_750=V_756 | ~member(U_178, X1_750, W_177) | ~member(U_178, Z_753, W_177) | ~member(U_178, Y_748, W_177) | ~member(U_178, X_755, W_177) | ~member(U_178, V_756, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1282, plain, (![X1_843, X_840, U_839, Y_852, U_178, X_181, Z_179, Z_849, Y_182, V_846, X1_850, X_838, X1_180, Z_845, W_177, V_183, W_851, U_841, Y_853, V_844]: (skf21(V_846, X_838, Y_853, Z_845, X1_843, W_177, U_178)=skf10(U_839, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_839, W_177, U_178) | skf21(V_846, X_838, Y_853, Z_845, X1_843, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_844 | skf10(U_839, W_177, U_178)=V_844 | skf21(V_846, X_838, Y_853, Z_845, X1_843, W_177, U_178)=V_844 | V_844=U_841 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_841 | skf10(U_839, W_177, U_178)=U_841 | skf21(V_846, X_838, Y_853, Z_845, X1_843, W_177, U_178)=U_841 | ~member(U_178, V_844, W_177) | ~member(U_178, U_841, W_177) | skf21(U_841, V_844, W_851, X_840, Y_852, Z_849, X1_850)!=V_844 | Z_845=X1_843 | Z_845=Y_853 | Y_853=X1_843 | Y_853=X_838 | Z_845=X_838 | X_838=X1_843 | X_838=V_846 | Y_853=V_846 | Z_845=V_846 | X1_843=V_846 | ~member(U_178, X1_843, W_177) | ~member(U_178, Z_845, W_177) | ~member(U_178, Y_853, W_177) | ~member(U_178, X_838, W_177) | ~member(U_178, V_846, W_177) | ssSkP0(U_839, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1232, plain, (![X_821, Y_806, X4_808, Z_813, U_178, X_820, X_181, Z_179, W_809, U_819, Y_817, Y_182, U_811, Z_822, X1_816, V_807, X1_812, V_818, X1_180, W_177, V_183]: (skf21(V_807, X_820, Y_806, Z_813, X1_816, W_177, U_178)=skf10(U_811, W_177, U_178) | skf21(V_807, X_820, Y_806, Z_813, X1_816, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_811, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_808 | skf21(V_807, X_820, Y_806, Z_813, X1_816, W_177, U_178)=X4_808 | skf10(U_811, W_177, U_178)=X4_808 | X4_808=U_819 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_819 | skf21(V_807, X_820, Y_806, Z_813, X1_816, W_177, U_178)=U_819 | skf10(U_811, W_177, U_178)=U_819 | ~member(U_178, X4_808, W_177) | ~member(U_178, U_819, W_177) | skf21(U_819, V_818, W_809, X_821, Y_817, Z_822, X1_812)!=U_819 | ssSkP0(U_811, W_177, U_178) | Z_813=X1_816 | Z_813=Y_806 | Y_806=X1_816 | Y_806=X_820 | Z_813=X_820 | X_820=X1_816 | X_820=V_807 | Y_806=V_807 | Z_813=V_807 | X1_816=V_807 | ~member(U_178, X1_816, W_177) | ~member(U_178, Z_813, W_177) | ~member(U_178, Y_806, W_177) | ~member(U_178, X_820, W_177) | ~member(U_178, V_807, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1206, plain, (![X1_784, V_790, U_178, U_786, X_181, Z_179, V_778, Y_782, Z_783, Z_787, Y_182, X1_792, X_789, X1_180, W_177, W_780, X_779, V_183, Y_781]: (skf21(V_790, X_789, Y_781, Z_787, X1_784, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_780 | skf21(V_790, X_789, Y_781, Z_787, X1_784, W_177, U_178)=W_780 | W_780=V_778 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_778 | skf21(V_790, X_789, Y_781, Z_787, X1_784, W_177, U_178)=V_778 | V_778=U_786 | W_780=U_786 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_786 | skf21(V_790, X_789, Y_781, Z_787, X1_784, W_177, U_178)=U_786 | ~member(U_178, W_780, W_177) | ~member(U_178, V_778, W_177) | ~member(U_178, U_786, W_177) | skf21(U_786, V_778, W_780, X_779, Y_782, Z_783, X1_792)!=W_780 | Z_787=X1_784 | Z_787=Y_781 | Y_781=X1_784 | Y_781=X_789 | Z_787=X_789 | X_789=X1_784 | X_789=V_790 | Y_781=V_790 | Z_787=V_790 | X1_784=V_790 | ~member(U_178, X1_784, W_177) | ~member(U_178, Z_787, W_177) | ~member(U_178, Y_781, W_177) | ~member(U_178, X_789, W_177) | ~member(U_178, V_790, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1028, plain, (![V_656, X1_652, U_178, X_181, Z_179, Z_647, Z_655, U_662, Y_182, Y_649, W_654, V_659, X4_650, X_658, X1_180, W_177, Y_661, V_183, X_653, X1_651]: (skf21(V_659, X_658, Y_649, Z_655, X1_651, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_650 | skf21(V_659, X_658, Y_649, Z_655, X1_651, W_177, U_178)=X4_650 | X4_650=V_656 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_656 | skf21(V_659, X_658, Y_649, Z_655, X1_651, W_177, U_178)=V_656 | V_656=U_662 | X4_650=U_662 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_662 | skf21(V_659, X_658, Y_649, Z_655, X1_651, W_177, U_178)=U_662 | ~member(U_178, X4_650, W_177) | ~member(U_178, V_656, W_177) | ~member(U_178, U_662, W_177) | skf21(U_662, V_656, W_654, X_653, Y_661, Z_647, X1_652)!=V_656 | Z_655=X1_651 | Z_655=Y_649 | Y_649=X1_651 | Y_649=X_658 | Z_655=X_658 | X_658=X1_651 | X_658=V_659 | Y_649=V_659 | Z_655=V_659 | X1_651=V_659 | ~member(U_178, X1_651, W_177) | ~member(U_178, Z_655, W_177) | ~member(U_178, Y_649, W_177) | ~member(U_178, X_658, W_177) | ~member(U_178, V_659, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1130, plain, (![X1_730, V_725, U_723, U_178, X_181, Z_179, Y_727, Y_182, U_733, W_734, U_729, X1_180, W_177, V_183, X_728, U_722, Z_732]: (skf10(U_733, W_177, U_178)=skf10(U_722, W_177, U_178) | skf10(U_729, W_177, U_178)=skf10(U_722, W_177, U_178) | skf10(U_733, W_177, U_178)=skf10(U_729, W_177, U_178) | skf10(U_729, W_177, U_178)=skf10(U_723, W_177, U_178) | skf10(U_723, W_177, U_178)=skf10(U_722, W_177, U_178) | skf10(U_733, W_177, U_178)=skf10(U_723, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_723, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_729, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_722, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_733, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_725, W_734, X_728, Y_727, Z_732, X1_730)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_733, W_177, U_178) | ssSkP0(U_722, W_177, U_178) | ssSkP0(U_729, W_177, U_178) | ssSkP0(U_723, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1362, plain, (![U_946, W_211, V_210, Z_955, V_952, U_944, Y_958, X_949, X_957, Y_959, V_943, X1_950, Z_948, X1_954, U_209, U_951, W_945]: (skf21(V_952, X_949, Y_958, Z_955, X1_954, V_210, W_211)=skf10(U_951, V_210, W_211) | skf21(V_952, X_949, Y_958, Z_955, X1_954, V_210, W_211)=skf10(U_944, V_210, W_211) | skf10(U_951, V_210, W_211)=skf10(U_944, V_210, W_211) | skf10(U_946, V_210, W_211)=skf10(U_944, V_210, W_211) | skf21(V_952, X_949, Y_958, Z_955, X1_954, V_210, W_211)=skf10(U_946, V_210, W_211) | skf10(U_951, V_210, W_211)=skf10(U_946, V_210, W_211) | skf10(U_946, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_944, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_952, X_949, Y_958, Z_955, X1_954, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_951, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_943, W_945, X_957, Y_959, Z_948, X1_950)!=skf10(U_209, V_210, W_211) | ssSkP0(U_951, V_210, W_211) | Z_955=X1_954 | Z_955=Y_958 | Y_958=X1_954 | Y_958=X_949 | Z_955=X_949 | X_949=X1_954 | X_949=V_952 | Y_958=V_952 | Z_955=V_952 | X1_954=V_952 | five(W_211, V_210) | ~member(W_211, X1_954, V_210) | ~member(W_211, Z_955, V_210) | ~member(W_211, Y_958, V_210) | ~member(W_211, X_949, V_210) | ~member(W_211, V_952, V_210) | ssSkP0(U_944, V_210, W_211) | ssSkP0(U_946, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.72 tff(c_1104, plain, (![U_178, X_181, Z_179, U_704, Y_182, U_699, X1_710, X1_180, U_703, W_177, V_183, W_705, Z_709, U_700, Y_708, X_706]: (skf10(U_703, W_177, U_178)=skf10(U_700, W_177, U_178) | skf10(U_700, W_177, U_178)=skf10(U_699, W_177, U_178) | skf10(U_703, W_177, U_178)=skf10(U_699, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_699, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_700, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_703, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_704 | skf10(U_699, W_177, U_178)=U_704 | skf10(U_700, W_177, U_178)=U_704 | skf10(U_703, W_177, U_178)=U_704 | ~member(U_178, U_704, W_177) | skf21(U_704, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_705, X_706, Y_708, Z_709, X1_710)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_703, W_177, U_178) | ssSkP0(U_700, W_177, U_178) | ssSkP0(U_699, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.72 tff(c_1181, plain, (![X1_762, X5_767, Y_763, U_178, X_181, Z_179, X4_769, U_761, X1_765, V_774, V_771, Y_764, Y_182, W_777, Z_766, X1_180, W_177, V_183, X_773, Z_770, X_776]: (skf21(V_774, X_773, Y_763, Z_770, X1_765, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X5_767 | skf21(V_774, X_773, Y_763, Z_770, X1_765, W_177, U_178)=X5_767 | X5_767=X4_769 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_769 | skf21(V_774, X_773, Y_763, Z_770, X1_765, W_177, U_178)=X4_769 | X4_769=U_761 | X5_767=U_761 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_761 | skf21(V_774, X_773, Y_763, Z_770, X1_765, W_177, U_178)=U_761 | ~member(U_178, X5_767, W_177) | ~member(U_178, X4_769, W_177) | ~member(U_178, U_761, W_177) | skf21(U_761, V_771, W_777, X_776, Y_764, Z_766, X1_762)!=U_761 | Z_770=X1_765 | Z_770=Y_763 | Y_763=X1_765 | Y_763=X_773 | Z_770=X_773 | X_773=X1_765 | X_773=V_774 | Y_763=V_774 | Z_770=V_774 | X1_765=V_774 | ~member(U_178, X1_765, W_177) | ~member(U_178, Z_770, W_177) | ~member(U_178, Y_763, W_177) | ~member(U_178, X_773, W_177) | ~member(U_178, V_774, W_177) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.73 tff(c_1311, plain, (![U_895, U_897, W_211, Y_910, V_210, Y_902, Z_909, X1_899, U_908, W_896, V_903, X_907, X1_900, U_209, X_906, Z_904]: (skf21(V_903, X_907, Y_902, Z_904, X1_899, V_210, W_211)=skf10(U_908, V_210, W_211) | skf10(U_908, V_210, W_211)=skf10(U_897, V_210, W_211) | skf21(V_903, X_907, Y_902, Z_904, X1_899, V_210, W_211)=skf10(U_897, V_210, W_211) | skf10(U_897, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_908, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_903, X_907, Y_902, Z_904, X1_899, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_895 | skf10(U_897, V_210, W_211)=U_895 | skf10(U_908, V_210, W_211)=U_895 | skf21(V_903, X_907, Y_902, Z_904, X1_899, V_210, W_211)=U_895 | ~member(W_211, U_895, V_210) | skf21(U_895, skf10(U_209, V_210, W_211), W_896, X_906, Y_910, Z_909, X1_900)!=skf10(U_209, V_210, W_211) | Z_904=X1_899 | Z_904=Y_902 | Y_902=X1_899 | Y_902=X_907 | Z_904=X_907 | X_907=X1_899 | X_907=V_903 | Y_902=V_903 | Z_904=V_903 | X1_899=V_903 | five(W_211, V_210) | ~member(W_211, X1_899, V_210) | ~member(W_211, Z_904, V_210) | ~member(W_211, Y_902, V_210) | ~member(W_211, X_907, V_210) | ~member(W_211, V_903, V_210) | ssSkP0(U_908, V_210, W_211) | ssSkP0(U_897, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_978, plain, (![X1_629, Z_631, U_628, U_178, X_181, Z_179, X_633, Y_630, Y_182, U_626, U_624, V_632, X1_180, W_177, V_183]: (skf10(U_626, W_177, U_178)=skf10(U_624, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_624, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_626, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_632 | skf10(U_624, W_177, U_178)=V_632 | skf10(U_626, W_177, U_178)=V_632 | V_632=U_628 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_628 | skf10(U_624, W_177, U_178)=U_628 | skf10(U_626, W_177, U_178)=U_628 | ~member(U_178, V_632, W_177) | ~member(U_178, U_628, W_177) | skf21(U_628, V_632, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_633, Y_630, Z_631, X1_629)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_626, W_177, U_178) | ssSkP0(U_624, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.73 tff(c_1336, plain, (![U_917, Y_918, V_924, W_211, V_210, U_913, Z_911, Y_922, Z_914, U_927, V_926, X1_921, X1_920, W_925, U_209, X_912, X_916]: (skf21(V_924, X_912, Y_918, Z_911, X1_920, V_210, W_211)=skf10(U_927, V_210, W_211) | skf21(V_924, X_912, Y_918, Z_911, X1_920, V_210, W_211)=skf10(U_913, V_210, W_211) | skf10(U_927, V_210, W_211)=skf10(U_913, V_210, W_211) | skf10(U_913, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_924, X_912, Y_918, Z_911, X1_920, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_927, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_917 | skf10(U_913, V_210, W_211)=U_917 | skf21(V_924, X_912, Y_918, Z_911, X1_920, V_210, W_211)=U_917 | skf10(U_927, V_210, W_211)=U_917 | ~member(W_211, U_917, V_210) | skf21(U_917, V_926, W_925, X_916, Y_922, Z_914, X1_921)!=U_917 | ssSkP0(U_927, V_210, W_211) | Z_911=X1_920 | Z_911=Y_918 | Y_918=X1_920 | Y_918=X_912 | Z_911=X_912 | X_912=X1_920 | X_912=V_924 | Y_918=V_924 | Z_911=V_924 | X1_920=V_924 | five(W_211, V_210) | ~member(W_211, X1_920, V_210) | ~member(W_211, Z_911, V_210) | ~member(W_211, Y_918, V_210) | ~member(W_211, X_912, V_210) | ~member(W_211, V_924, V_210) | ssSkP0(U_913, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_1258, plain, (![X_825, X_836, W_211, U_824, V_210, U_832, Z_830, X1_833, V_827, Y_828, X1_829, Z_837, V_834, U_209, Y_823]: (skf21(V_827, X_836, Y_828, Z_837, X1_829, V_210, W_211)=skf10(U_824, V_210, W_211) | skf10(U_824, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_827, X_836, Y_828, Z_837, X1_829, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_834 | skf10(U_824, V_210, W_211)=V_834 | skf21(V_827, X_836, Y_828, Z_837, X1_829, V_210, W_211)=V_834 | V_834=U_832 | skf10(U_209, V_210, W_211)=U_832 | skf10(U_824, V_210, W_211)=U_832 | skf21(V_827, X_836, Y_828, Z_837, X1_829, V_210, W_211)=U_832 | ~member(W_211, V_834, V_210) | ~member(W_211, U_832, V_210) | skf21(U_832, V_834, skf10(U_209, V_210, W_211), X_825, Y_823, Z_830, X1_833)!=skf10(U_209, V_210, W_211) | Z_837=X1_829 | Z_837=Y_828 | Y_828=X1_829 | Y_828=X_836 | Z_837=X_836 | X_836=X1_829 | X_836=V_827 | Y_828=V_827 | Z_837=V_827 | X1_829=V_827 | five(W_211, V_210) | ~member(W_211, X1_829, V_210) | ~member(W_211, Z_837, V_210) | ~member(W_211, Y_828, V_210) | ~member(W_211, X_836, V_210) | ~member(W_211, V_827, V_210) | ssSkP0(U_824, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_1233, plain, (![X_821, Y_806, X4_808, W_211, Z_813, V_210, X_820, W_809, U_819, Y_817, U_811, Z_822, X1_816, V_807, X1_812, V_818, U_209]: (skf21(V_807, X_820, Y_806, Z_813, X1_816, V_210, W_211)=skf10(U_811, V_210, W_211) | skf21(V_807, X_820, Y_806, Z_813, X1_816, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_811, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_808 | skf21(V_807, X_820, Y_806, Z_813, X1_816, V_210, W_211)=X4_808 | skf10(U_811, V_210, W_211)=X4_808 | X4_808=U_819 | skf10(U_209, V_210, W_211)=U_819 | skf21(V_807, X_820, Y_806, Z_813, X1_816, V_210, W_211)=U_819 | skf10(U_811, V_210, W_211)=U_819 | ~member(W_211, X4_808, V_210) | ~member(W_211, U_819, V_210) | skf21(U_819, V_818, W_809, X_821, Y_817, Z_822, X1_812)!=U_819 | ssSkP0(U_811, V_210, W_211) | Z_813=X1_816 | Z_813=Y_806 | Y_806=X1_816 | Y_806=X_820 | Z_813=X_820 | X_820=X1_816 | X_820=V_807 | Y_806=V_807 | Z_813=V_807 | X1_816=V_807 | five(W_211, V_210) | ~member(W_211, X1_816, V_210) | ~member(W_211, Z_813, V_210) | ~member(W_211, Y_806, V_210) | ~member(W_211, X_820, V_210) | ~member(W_211, V_807, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_1283, plain, (![X1_843, X_840, W_211, U_839, V_210, Y_852, Z_849, V_846, X1_850, X_838, Z_845, W_851, U_209, U_841, Y_853, V_844]: (skf21(V_846, X_838, Y_853, Z_845, X1_843, V_210, W_211)=skf10(U_839, V_210, W_211) | skf10(U_839, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_846, X_838, Y_853, Z_845, X1_843, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_844 | skf10(U_839, V_210, W_211)=V_844 | skf21(V_846, X_838, Y_853, Z_845, X1_843, V_210, W_211)=V_844 | V_844=U_841 | skf10(U_209, V_210, W_211)=U_841 | skf10(U_839, V_210, W_211)=U_841 | skf21(V_846, X_838, Y_853, Z_845, X1_843, V_210, W_211)=U_841 | ~member(W_211, V_844, V_210) | ~member(W_211, U_841, V_210) | skf21(U_841, V_844, W_851, X_840, Y_852, Z_849, X1_850)!=V_844 | Z_845=X1_843 | Z_845=Y_853 | Y_853=X1_843 | Y_853=X_838 | Z_845=X_838 | X_838=X1_843 | X_838=V_846 | Y_853=V_846 | Z_845=V_846 | X1_843=V_846 | five(W_211, V_210) | ~member(W_211, X1_843, V_210) | ~member(W_211, Z_845, V_210) | ~member(W_211, Y_853, V_210) | ~member(W_211, X_838, V_210) | ~member(W_211, V_846, V_210) | ssSkP0(U_839, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_945, plain, (![Z_607, U_178, W_609, X_181, Z_179, Y_182, X1_610, Y_611, U_603, X1_180, W_177, U_604, V_608, V_183]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_603, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_609 | skf10(U_603, W_177, U_178)=W_609 | W_609=V_608 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_608 | skf10(U_603, W_177, U_178)=V_608 | V_608=U_604 | W_609=U_604 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_604 | skf10(U_603, W_177, U_178)=U_604 | ~member(U_178, W_609, W_177) | ~member(U_178, V_608, W_177) | ~member(U_178, U_604, W_177) | skf21(U_604, V_608, W_609, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), Y_611, Z_607, X1_610)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_603, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.73 tff(c_1157, plain, (![V_757, W_211, V_210, U_752, Y_748, V_756, X1_759, Y_751, W_747, X_755, Z_753, Z_760, U_209, X1_750]: (skf21(V_756, X_755, Y_748, Z_753, X1_750, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_747 | skf21(V_756, X_755, Y_748, Z_753, X1_750, V_210, W_211)=W_747 | W_747=V_757 | skf10(U_209, V_210, W_211)=V_757 | skf21(V_756, X_755, Y_748, Z_753, X1_750, V_210, W_211)=V_757 | V_757=U_752 | W_747=U_752 | skf10(U_209, V_210, W_211)=U_752 | skf21(V_756, X_755, Y_748, Z_753, X1_750, V_210, W_211)=U_752 | ~member(W_211, W_747, V_210) | ~member(W_211, V_757, V_210) | ~member(W_211, U_752, V_210) | skf21(U_752, V_757, W_747, skf10(U_209, V_210, W_211), Y_751, Z_760, X1_759)!=skf10(U_209, V_210, W_211) | Z_753=X1_750 | Z_753=Y_748 | Y_748=X1_750 | Y_748=X_755 | Z_753=X_755 | X_755=X1_750 | X_755=V_756 | Y_748=V_756 | Z_753=V_756 | X1_750=V_756 | five(W_211, V_210) | ~member(W_211, X1_750, V_210) | ~member(W_211, Z_753, V_210) | ~member(W_211, Y_748, V_210) | ~member(W_211, X_755, V_210) | ~member(W_211, V_756, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_790, plain, (![U_543, X1_546, X1_172, Z_544, X_174, Z_171, Y_541, U_170, W_545, W_168, V_542, V_176, X_547]: (skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=X_174 | X_174=W_168 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=W_168 | W_168=V_176 | X_174=V_176 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=V_176 | V_176=U_170 | W_168=U_170 | X_174=U_170 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=U_170 | ~member(U_543, X_174, W_545) | ~member(U_543, W_168, W_545) | ~member(U_543, V_176, W_545) | ~member(U_543, U_170, W_545) | skf21(U_170, V_176, W_168, X_174, skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543), Z_171, X1_172)!=skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543) | Z_544=X1_546 | Z_544=Y_541 | Y_541=X1_546 | Y_541=X_547 | Z_544=X_547 | X_547=X1_546 | X_547=V_542 | Y_541=V_542 | Z_544=V_542 | X1_546=V_542 | five(U_543, W_545) | ~member(U_543, X1_546, W_545) | ~member(U_543, Z_544, W_545) | ~member(U_543, Y_541, W_545) | ~member(U_543, X_547, W_545) | ~member(U_543, V_542, W_545)))). % 35.98/24.73 tff(c_1029, plain, (![V_656, X1_652, W_211, V_210, Z_647, Z_655, U_662, Y_649, W_654, V_659, X4_650, X_658, Y_661, X_653, U_209, X1_651]: (skf21(V_659, X_658, Y_649, Z_655, X1_651, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_650 | skf21(V_659, X_658, Y_649, Z_655, X1_651, V_210, W_211)=X4_650 | X4_650=V_656 | skf10(U_209, V_210, W_211)=V_656 | skf21(V_659, X_658, Y_649, Z_655, X1_651, V_210, W_211)=V_656 | V_656=U_662 | X4_650=U_662 | skf10(U_209, V_210, W_211)=U_662 | skf21(V_659, X_658, Y_649, Z_655, X1_651, V_210, W_211)=U_662 | ~member(W_211, X4_650, V_210) | ~member(W_211, V_656, V_210) | ~member(W_211, U_662, V_210) | skf21(U_662, V_656, W_654, X_653, Y_661, Z_647, X1_652)!=V_656 | Z_655=X1_651 | Z_655=Y_649 | Y_649=X1_651 | Y_649=X_658 | Z_655=X_658 | X_658=X1_651 | X_658=V_659 | Y_649=V_659 | Z_655=V_659 | X1_651=V_659 | five(W_211, V_210) | ~member(W_211, X1_651, V_210) | ~member(W_211, Z_655, V_210) | ~member(W_211, Y_649, V_210) | ~member(W_211, X_658, V_210) | ~member(W_211, V_659, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_1207, plain, (![X1_784, W_211, V_790, V_210, U_786, V_778, Y_782, Z_783, Z_787, X1_792, X_789, W_780, X_779, U_209, Y_781]: (skf21(V_790, X_789, Y_781, Z_787, X1_784, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_780 | skf21(V_790, X_789, Y_781, Z_787, X1_784, V_210, W_211)=W_780 | W_780=V_778 | skf10(U_209, V_210, W_211)=V_778 | skf21(V_790, X_789, Y_781, Z_787, X1_784, V_210, W_211)=V_778 | V_778=U_786 | W_780=U_786 | skf10(U_209, V_210, W_211)=U_786 | skf21(V_790, X_789, Y_781, Z_787, X1_784, V_210, W_211)=U_786 | ~member(W_211, W_780, V_210) | ~member(W_211, V_778, V_210) | ~member(W_211, U_786, V_210) | skf21(U_786, V_778, W_780, X_779, Y_782, Z_783, X1_792)!=W_780 | Z_787=X1_784 | Z_787=Y_781 | Y_781=X1_784 | Y_781=X_789 | Z_787=X_789 | X_789=X1_784 | X_789=V_790 | Y_781=V_790 | Z_787=V_790 | X1_784=V_790 | five(W_211, V_210) | ~member(W_211, X1_784, V_210) | ~member(W_211, Z_787, V_210) | ~member(W_211, Y_781, V_210) | ~member(W_211, X_789, V_210) | ~member(W_211, V_790, V_210) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_920, plain, (![V_599, X5_591, X1_596, X4_602, U_178, X_181, Z_179, Y_182, U_598, X_593, W_600, Z_590, X1_180, U_592, W_177, V_183, Y_595]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_592, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X5_591 | skf10(U_592, W_177, U_178)=X5_591 | X5_591=X4_602 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_602 | skf10(U_592, W_177, U_178)=X4_602 | X4_602=U_598 | X5_591=U_598 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_598 | skf10(U_592, W_177, U_178)=U_598 | ~member(U_178, X5_591, W_177) | ~member(U_178, X4_602, W_177) | ~member(U_178, U_598, W_177) | skf21(U_598, V_599, W_600, X_593, Y_595, Z_590, X1_596)!=U_598 | ssSkP0(U_592, W_177, U_178) | Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 35.98/24.73 tff(c_1131, plain, (![W_211, X1_730, V_725, V_210, U_723, Y_727, U_733, W_734, U_729, X_728, U_209, U_722, Z_732]: (skf10(U_733, V_210, W_211)=skf10(U_722, V_210, W_211) | skf10(U_729, V_210, W_211)=skf10(U_722, V_210, W_211) | skf10(U_733, V_210, W_211)=skf10(U_729, V_210, W_211) | skf10(U_729, V_210, W_211)=skf10(U_723, V_210, W_211) | skf10(U_723, V_210, W_211)=skf10(U_722, V_210, W_211) | skf10(U_733, V_210, W_211)=skf10(U_723, V_210, W_211) | skf10(U_723, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_729, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_722, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_733, V_210, W_211)=skf10(U_209, V_210, W_211) | five(W_211, V_210) | skf21(skf10(U_209, V_210, W_211), V_725, W_734, X_728, Y_727, Z_732, X1_730)!=skf10(U_209, V_210, W_211) | ssSkP0(U_733, V_210, W_211) | ssSkP0(U_722, V_210, W_211) | ssSkP0(U_729, V_210, W_211) | ssSkP0(U_723, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 35.98/24.73 tff(c_789, plain, (![U_543, X1_546, W_148, Z_544, V_156, Y_541, Y_155, W_545, X1_152, X_154, V_542, Z_151, U_150, X_547, X4_157]: (skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=X4_157 | X4_157=W_148 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=W_148 | W_148=V_156 | X4_157=V_156 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=V_156 | V_156=U_150 | W_148=U_150 | X4_157=U_150 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=U_150 | ~member(U_543, X4_157, W_545) | ~member(U_543, W_148, W_545) | ~member(U_543, V_156, W_545) | ~member(U_543, U_150, W_545) | skf21(U_150, V_156, W_148, X_154, Y_155, Z_151, X1_152)!=W_148 | Z_544=X1_546 | Z_544=Y_541 | Y_541=X1_546 | Y_541=X_547 | Z_544=X_547 | X_547=X1_546 | X_547=V_542 | Y_541=V_542 | Z_544=V_542 | X1_546=V_542 | five(U_543, W_545) | ~member(U_543, X1_546, W_545) | ~member(U_543, Z_544, W_545) | ~member(U_543, Y_541, W_545) | ~member(U_543, X_547, W_545) | ~member(U_543, V_542, W_545)))). % 35.98/24.73 tff(c_787, plain, (![U_543, X1_546, V_195, X6_185, U_188, X4_196, Z_544, Y_541, X5_184, Z_189, W_545, X1_191, V_542, Y_194, W_186, X_193, X_547]: (skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=X6_185 | X6_185=X5_184 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=X5_184 | X5_184=X4_196 | X6_185=X4_196 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=X4_196 | X4_196=U_188 | X5_184=U_188 | X6_185=U_188 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=U_188 | ~member(U_543, X6_185, W_545) | ~member(U_543, X5_184, W_545) | ~member(U_543, X4_196, W_545) | ~member(U_543, U_188, W_545) | skf21(U_188, V_195, W_186, X_193, Y_194, Z_189, X1_191)!=U_188 | Z_544=X1_546 | Z_544=Y_541 | Y_541=X1_546 | Y_541=X_547 | Z_544=X_547 | X_547=X1_546 | X_547=V_542 | Y_541=V_542 | Z_544=V_542 | X1_546=V_542 | five(U_543, W_545) | ~member(U_543, X1_546, W_545) | ~member(U_543, Z_544, W_545) | ~member(U_543, Y_541, W_545) | ~member(U_543, X_547, W_545) | ~member(U_543, V_542, W_545)))). % 35.98/24.73 tff(c_786, plain, (![U_543, X1_546, Z_161, X1_162, Z_544, Y_541, W_158, W_545, V_542, U_160, V_166, X_164, X_547, Y_165]: (skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=X_164 | X_164=W_158 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=W_158 | W_158=V_166 | X_164=V_166 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=V_166 | V_166=U_160 | W_158=U_160 | X_164=U_160 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=U_160 | ~member(U_543, X_164, W_545) | ~member(U_543, W_158, W_545) | ~member(U_543, V_166, W_545) | ~member(U_543, U_160, W_545) | skf21(U_160, V_166, W_158, X_164, Y_165, Z_161, X1_162)!=X_164 | Z_544=X1_546 | Z_544=Y_541 | Y_541=X1_546 | Y_541=X_547 | Z_544=X_547 | X_547=X1_546 | X_547=V_542 | Y_541=V_542 | Z_544=V_542 | X1_546=V_542 | five(U_543, W_545) | ~member(U_543, X1_546, W_545) | ~member(U_543, Z_544, W_545) | ~member(U_543, Y_541, W_545) | ~member(U_543, X_547, W_545) | ~member(U_543, V_542, W_545)))). % 36.04/24.73 tff(c_1105, plain, (![W_211, V_210, U_704, U_699, X1_710, U_703, W_705, Z_709, U_700, U_209, Y_708, X_706]: (skf10(U_703, V_210, W_211)=skf10(U_700, V_210, W_211) | skf10(U_700, V_210, W_211)=skf10(U_699, V_210, W_211) | skf10(U_703, V_210, W_211)=skf10(U_699, V_210, W_211) | skf10(U_699, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_700, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_703, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_704 | skf10(U_699, V_210, W_211)=U_704 | skf10(U_700, V_210, W_211)=U_704 | skf10(U_703, V_210, W_211)=U_704 | five(W_211, V_210) | ~member(W_211, U_704, V_210) | skf21(U_704, skf10(U_209, V_210, W_211), W_705, X_706, Y_708, Z_709, X1_710)!=skf10(U_209, V_210, W_211) | ssSkP0(U_703, V_210, W_211) | ssSkP0(U_700, V_210, W_211) | ssSkP0(U_699, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_1080, plain, (![W_211, V_210, Y_695, U_698, W_688, Z_694, U_686, U_690, V_692, U_687, X1_693, X_697, U_209]: (skf10(U_698, V_210, W_211)=skf10(U_687, V_210, W_211) | skf10(U_690, V_210, W_211)=skf10(U_687, V_210, W_211) | skf10(U_698, V_210, W_211)=skf10(U_690, V_210, W_211) | skf10(U_690, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_687, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_698, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_686 | skf10(U_690, V_210, W_211)=U_686 | skf10(U_687, V_210, W_211)=U_686 | skf10(U_698, V_210, W_211)=U_686 | five(W_211, V_210) | ~member(W_211, U_686, V_210) | skf21(U_686, V_692, W_688, X_697, Y_695, Z_694, X1_693)!=U_686 | ssSkP0(U_698, V_210, W_211) | ssSkP0(U_687, V_210, W_211) | ssSkP0(U_690, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_979, plain, (![X1_629, Z_631, U_628, W_211, V_210, X_633, Y_630, U_626, U_624, V_632, U_209]: (skf10(U_626, V_210, W_211)=skf10(U_624, V_210, W_211) | skf10(U_624, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_626, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_632 | skf10(U_624, V_210, W_211)=V_632 | skf10(U_626, V_210, W_211)=V_632 | V_632=U_628 | skf10(U_209, V_210, W_211)=U_628 | skf10(U_624, V_210, W_211)=U_628 | skf10(U_626, V_210, W_211)=U_628 | five(W_211, V_210) | ~member(W_211, V_632, V_210) | ~member(W_211, U_628, V_210) | skf21(U_628, V_632, skf10(U_209, V_210, W_211), X_633, Y_630, Z_631, X1_629)!=skf10(U_209, V_210, W_211) | ssSkP0(U_626, V_210, W_211) | ssSkP0(U_624, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_1004, plain, (![W_211, V_210, Z_636, W_644, X1_642, U_637, U_646, Y_645, V_635, U_209, U_641, X_638]: (skf10(U_641, V_210, W_211)=skf10(U_637, V_210, W_211) | skf10(U_637, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_641, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_635 | skf10(U_637, V_210, W_211)=V_635 | skf10(U_641, V_210, W_211)=V_635 | V_635=U_646 | skf10(U_209, V_210, W_211)=U_646 | skf10(U_637, V_210, W_211)=U_646 | skf10(U_641, V_210, W_211)=U_646 | five(W_211, V_210) | ~member(W_211, V_635, V_210) | ~member(W_211, U_646, V_210) | skf21(U_646, V_635, W_644, X_638, Y_645, Z_636, X1_642)!=V_635 | ssSkP0(U_641, V_210, W_211) | ssSkP0(U_637, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_1054, plain, (![U_667, U_673, W_211, V_210, X4_664, X1_668, V_671, Y_670, Z_675, X_674, W_665, U_663, U_209]: (skf10(U_667, V_210, W_211)=skf10(U_663, V_210, W_211) | skf10(U_663, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_667, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_664 | skf10(U_663, V_210, W_211)=X4_664 | skf10(U_667, V_210, W_211)=X4_664 | X4_664=U_673 | skf10(U_209, V_210, W_211)=U_673 | skf10(U_663, V_210, W_211)=U_673 | skf10(U_667, V_210, W_211)=U_673 | five(W_211, V_210) | ~member(W_211, X4_664, V_210) | ~member(W_211, U_673, V_210) | skf21(U_673, V_671, W_665, X_674, Y_670, Z_675, X1_668)!=U_673 | ssSkP0(U_667, V_210, W_211) | ssSkP0(U_663, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_946, plain, (![Z_607, W_211, V_210, W_609, X1_610, Y_611, U_603, U_604, V_608, U_209]: (skf10(U_603, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_609 | skf10(U_603, V_210, W_211)=W_609 | W_609=V_608 | skf10(U_209, V_210, W_211)=V_608 | skf10(U_603, V_210, W_211)=V_608 | V_608=U_604 | W_609=U_604 | skf10(U_209, V_210, W_211)=U_604 | skf10(U_603, V_210, W_211)=U_604 | five(W_211, V_210) | ~member(W_211, W_609, V_210) | ~member(W_211, V_608, V_210) | ~member(W_211, U_604, V_210) | skf21(U_604, V_608, W_609, skf10(U_209, V_210, W_211), Y_611, Z_607, X1_610)!=skf10(U_209, V_210, W_211) | ssSkP0(U_603, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_921, plain, (![V_599, X5_591, X1_596, X4_602, W_211, V_210, U_598, X_593, W_600, Z_590, U_592, U_209, Y_595]: (skf10(U_592, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X5_591 | skf10(U_592, V_210, W_211)=X5_591 | X5_591=X4_602 | skf10(U_209, V_210, W_211)=X4_602 | skf10(U_592, V_210, W_211)=X4_602 | X4_602=U_598 | X5_591=U_598 | skf10(U_209, V_210, W_211)=U_598 | skf10(U_592, V_210, W_211)=U_598 | five(W_211, V_210) | ~member(W_211, X5_591, V_210) | ~member(W_211, X4_602, V_210) | ~member(W_211, U_598, V_210) | skf21(U_598, V_599, W_600, X_593, Y_595, Z_590, X1_596)!=U_598 | ssSkP0(U_592, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_788, plain, (![U_543, X1_546, W_199, Z_202, X4_208, X5_197, Z_544, X_205, Y_541, V_207, W_545, V_542, U_201, X1_203, Y_206, X_547]: (skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=X5_197 | X5_197=X4_208 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=X4_208 | X4_208=V_207 | X5_197=V_207 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=V_207 | V_207=U_201 | X4_208=U_201 | X5_197=U_201 | skf21(V_542, X_547, Y_541, Z_544, X1_546, W_545, U_543)=U_201 | ~member(U_543, X5_197, W_545) | ~member(U_543, X4_208, W_545) | ~member(U_543, V_207, W_545) | ~member(U_543, U_201, W_545) | skf21(U_201, V_207, W_199, X_205, Y_206, Z_202, X1_203)!=V_207 | Z_544=X1_546 | Z_544=Y_541 | Y_541=X1_546 | Y_541=X_547 | Z_544=X_547 | X_547=X1_546 | X_547=V_542 | Y_541=V_542 | Z_544=V_542 | X1_546=V_542 | five(U_543, W_545) | ~member(U_543, X1_546, W_545) | ~member(U_543, Z_544, W_545) | ~member(U_543, Y_541, W_545) | ~member(U_543, X_547, W_545) | ~member(U_543, V_542, W_545)))). % 36.04/24.73 tff(c_864, plain, (![Y_580, W_211, V_210, X1_584, U_585, Z_582, X4_583, V_587, X_578, W_579, U_576, U_209]: (skf10(U_576, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_583 | skf10(U_576, V_210, W_211)=X4_583 | X4_583=V_587 | skf10(U_209, V_210, W_211)=V_587 | skf10(U_576, V_210, W_211)=V_587 | V_587=U_585 | X4_583=U_585 | skf10(U_209, V_210, W_211)=U_585 | skf10(U_576, V_210, W_211)=U_585 | five(W_211, V_210) | ~member(W_211, X4_583, V_210) | ~member(W_211, V_587, V_210) | ~member(W_211, U_585, V_210) | skf21(U_585, V_587, W_579, X_578, Y_580, Z_582, X1_584)!=V_587 | ssSkP0(U_576, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_822, plain, (![Y_570, X1_568, W_211, V_210, U_562, W_564, V_569, X_567, U_566, Z_565, U_209]: (skf10(U_562, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_564 | skf10(U_562, V_210, W_211)=W_564 | W_564=V_569 | skf10(U_209, V_210, W_211)=V_569 | skf10(U_562, V_210, W_211)=V_569 | V_569=U_566 | W_564=U_566 | skf10(U_209, V_210, W_211)=U_566 | skf10(U_562, V_210, W_211)=U_566 | five(W_211, V_210) | ~member(W_211, W_564, V_210) | ~member(W_211, V_569, V_210) | ~member(W_211, U_566, V_210) | skf21(U_566, V_569, W_564, X_567, Y_570, Z_565, X1_568)!=W_564 | ssSkP0(U_562, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_958, plain, (![V_26]: (skf8(skc5, V_26)=skf20(V_26, skc5) | skf8(skc5, V_26)=skf18(V_26, skc5) | skf8(skc5, V_26)=skf16(V_26, skc5) | skf8(skc5, V_26)=skf14(V_26, skc5) | skf8(skc5, V_26)=skf12(V_26, skc5) | skf10(skc8, V_26, skc5)=skf20(V_26, skc5) | skf10(skc8, V_26, skc5)=skf18(V_26, skc5) | skf10(skc8, V_26, skc5)=skf16(V_26, skc5) | skf10(skc8, V_26, skc5)=skf14(V_26, skc5) | skf10(skc8, V_26, skc5)=skf12(V_26, skc5) | ~five(skc5, V_26)))). % 36.04/24.73 tff(c_690, plain, (![Z_488, X_493, W_211, V_210, X1_486, W_492, V_494, U_487, U_209]: (skf10(U_209, V_210, W_211)=X_493 | X_493=W_492 | skf10(U_209, V_210, W_211)=W_492 | W_492=V_494 | X_493=V_494 | skf10(U_209, V_210, W_211)=V_494 | V_494=U_487 | W_492=U_487 | X_493=U_487 | skf10(U_209, V_210, W_211)=U_487 | five(W_211, V_210) | ~member(W_211, X_493, V_210) | ~member(W_211, W_492, V_210) | ~member(W_211, V_494, V_210) | ~member(W_211, U_487, V_210) | skf21(U_487, V_494, W_492, X_493, skf10(U_209, V_210, W_211), Z_488, X1_486)!=skf10(U_209, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_766, plain, (![Z_540, W_211, V_210, X_535, W_533, X1_539, V_538, Y_536, U_209, U_537]: (skf10(U_209, V_210, W_211)=X_535 | X_535=W_533 | skf10(U_209, V_210, W_211)=W_533 | W_533=V_538 | X_535=V_538 | skf10(U_209, V_210, W_211)=V_538 | V_538=U_537 | W_533=U_537 | X_535=U_537 | skf10(U_209, V_210, W_211)=U_537 | five(W_211, V_210) | ~member(W_211, X_535, V_210) | ~member(W_211, W_533, V_210) | ~member(W_211, V_538, V_210) | ~member(W_211, U_537, V_210) | skf21(U_537, V_538, W_533, X_535, Y_536, Z_540, X1_539)!=X_535 | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_747, plain, (![W_530, X5_525, W_211, Z_524, X4_527, V_210, X6_526, V_528, Y_522, U_518, X_529, U_209, X1_519]: (skf10(U_209, V_210, W_211)=X6_526 | X6_526=X5_525 | skf10(U_209, V_210, W_211)=X5_525 | X5_525=X4_527 | X6_526=X4_527 | skf10(U_209, V_210, W_211)=X4_527 | X4_527=U_518 | X5_525=U_518 | X6_526=U_518 | skf10(U_209, V_210, W_211)=U_518 | five(W_211, V_210) | ~member(W_211, X6_526, V_210) | ~member(W_211, X5_525, V_210) | ~member(W_211, X4_527, V_210) | ~member(W_211, U_518, V_210) | skf21(U_518, V_528, W_530, X_529, Y_522, Z_524, X1_519)!=U_518 | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_895, plain, (![V_588]: (skf8(skc5, V_588)=skf20(V_588, skc5) | skf8(skc5, V_588)=skf18(V_588, skc5) | skf8(skc5, V_588)=skf16(V_588, skc5) | skf8(skc5, V_588)=skf14(V_588, skc5) | skf8(skc5, V_588)=skf12(V_588, skc5) | ~ssSkP0(skc8, V_588, skc5) | ~five(skc5, V_588) | ~group(skc5, V_588)))). % 36.04/24.73 tff(c_842, plain, (![V_573]: (member(skc5, skf8(skc5, V_573), V_573) | ~ssSkP0(skc8, V_573, skc5) | ~five(skc5, V_573) | ~group(skc5, V_573)))). % 36.04/24.73 tff(c_728, plain, (![X5_507, W_211, V_210, Z_506, X4_508, V_515, Y_516, U_517, X_512, X1_510, W_513, U_209]: (skf10(U_209, V_210, W_211)=X5_507 | X5_507=X4_508 | skf10(U_209, V_210, W_211)=X4_508 | X4_508=V_515 | X5_507=V_515 | skf10(U_209, V_210, W_211)=V_515 | V_515=U_517 | X4_508=U_517 | X5_507=U_517 | skf10(U_209, V_210, W_211)=U_517 | five(W_211, V_210) | ~member(W_211, X5_507, V_210) | ~member(W_211, X4_508, V_210) | ~member(W_211, V_515, V_210) | ~member(W_211, U_517, V_210) | skf21(U_517, V_515, W_513, X_512, Y_516, Z_506, X1_510)!=V_515 | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_847, plain, (~human(skc5, skc8))). % 36.04/24.73 tff(c_843, plain, (nonhuman(skc5, skc8))). % 36.04/24.73 tff(c_805, plain, (![V_557, W_556, Y_559]: (member(skc5, skf8(skc5, V_557), V_557) | ~of(skc5, W_556, Y_559) | ~woman(skc5, Y_559) | ~agent(skc5, skc6, Y_559) | ~ssSkP0(W_556, V_557, skc5) | ~forename(skc5, W_556) | ~mia_forename(skc5, W_556) | ~nonhuman(skc5, W_556) | ~five(skc5, V_557) | ~group(skc5, V_557)))). % 36.04/24.73 tff(c_709, plain, (![Y_500, W_211, V_210, U_503, V_495, X_498, Z_501, W_499, X4_502, X1_504, U_209]: (skf10(U_209, V_210, W_211)=X4_502 | X4_502=W_499 | skf10(U_209, V_210, W_211)=W_499 | W_499=V_495 | X4_502=V_495 | skf10(U_209, V_210, W_211)=V_495 | V_495=U_503 | W_499=U_503 | X4_502=U_503 | skf10(U_209, V_210, W_211)=U_503 | five(W_211, V_210) | ~member(W_211, X4_502, V_210) | ~member(W_211, W_499, V_210) | ~member(W_211, V_495, V_210) | ~member(W_211, U_503, V_210) | skf21(U_503, V_495, W_499, X_498, Y_500, Z_501, X1_504)!=W_499 | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.73 tff(c_186, plain, (![Y_227, U_224, V_228, X_226, Z_225, W_223]: (member(U_224, skf8(U_224, V_228), V_228) | ~actual_world(U_224) | ~shake_beverage(U_224, Z_225) | ~patient(U_224, X_226, Z_225) | ~order(U_224, X_226) | ~nonreflexive(U_224, X_226) | ~past(U_224, X_226) | ~event(U_224, X_226) | ~of(U_224, W_223, Y_227) | ~woman(U_224, Y_227) | ~agent(U_224, X_226, Y_227) | ~ssSkP0(W_223, V_228, U_224) | ~forename(U_224, W_223) | ~mia_forename(U_224, W_223) | ~nonhuman(U_224, W_223) | ~five(U_224, V_228) | ~group(U_224, V_228)))). % 36.04/24.73 tff(c_798, plain, (![V_551]: (~dollar(skc5, skf8(skc5, V_551))))). % 36.04/24.73 tff(c_184, plain, (![U_217, W_216, X1_219, V_222, Y_221, X_220, Z_218]: (~actual_world(U_217) | ~shake_beverage(U_217, X1_219) | ~patient(U_217, Y_221, X1_219) | ~order(U_217, Y_221) | ~nonreflexive(U_217, Y_221) | ~past(U_217, Y_221) | ~event(U_217, Y_221) | ~of(U_217, X_220, Z_218) | ~woman(U_217, Z_218) | ~agent(U_217, Y_221, Z_218) | ~ssSkP0(X_220, W_216, U_217) | ~forename(U_217, X_220) | ~mia_forename(U_217, X_220) | ~nonhuman(U_217, X_220) | ~five(U_217, W_216) | ~group(U_217, W_216) | ~dollar(U_217, skf8(U_217, V_222))))). % 36.04/24.73 tff(c_150, plain, (![U_178, X_181, Z_179, Y_182, X1_180, W_177, V_183]: (Z_179=X1_180 | Z_179=Y_182 | Y_182=X1_180 | Y_182=X_181 | Z_179=X_181 | X_181=X1_180 | X_181=V_183 | Y_182=V_183 | Z_179=V_183 | X1_180=V_183 | member(U_178, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_177) | five(U_178, W_177) | ~member(U_178, X1_180, W_177) | ~member(U_178, Z_179, W_177) | ~member(U_178, Y_182, W_177) | ~member(U_178, X_181, W_177) | ~member(U_178, V_183, W_177)))). % 36.04/24.73 tff(c_146, plain, (![Z_161, X3_159, X1_162, X4_167, X2_163, W_158, U_160, V_166, X_164, Y_165]: (X_164=X4_167 | X_164=W_158 | X4_167=W_158 | W_158=V_166 | X_164=V_166 | X4_167=V_166 | V_166=U_160 | W_158=U_160 | X_164=U_160 | X4_167=U_160 | five(X2_163, X3_159) | ~member(X2_163, X4_167, X3_159) | ~member(X2_163, X_164, X3_159) | ~member(X2_163, W_158, X3_159) | ~member(X2_163, V_166, X3_159) | ~member(X2_163, U_160, X3_159) | skf21(U_160, V_166, W_158, X_164, Y_165, Z_161, X1_162)!=X_164))). % 36.04/24.74 tff(c_152, plain, (![V_195, X6_185, U_188, X7_190, X4_196, X5_184, X3_187, Z_189, X1_191, Y_194, W_186, X_193, X2_192]: (X7_190=X6_185 | X6_185=X5_184 | X7_190=X5_184 | X5_184=X4_196 | X6_185=X4_196 | X7_190=X4_196 | X4_196=U_188 | X5_184=U_188 | X6_185=U_188 | X7_190=U_188 | five(X2_192, X3_187) | ~member(X2_192, X7_190, X3_187) | ~member(X2_192, X6_185, X3_187) | ~member(X2_192, X5_184, X3_187) | ~member(X2_192, X4_196, X3_187) | ~member(X2_192, U_188, X3_187) | skf21(U_188, V_195, W_186, X_193, Y_194, Z_189, X1_191)!=U_188))). % 36.04/24.74 tff(c_154, plain, (![W_199, Z_202, X4_208, X5_197, X_205, X6_198, V_207, U_201, X2_204, X3_200, X1_203, Y_206]: (X6_198=X5_197 | X5_197=X4_208 | X6_198=X4_208 | X4_208=V_207 | X5_197=V_207 | X6_198=V_207 | V_207=U_201 | X4_208=U_201 | X5_197=U_201 | X6_198=U_201 | five(X2_204, X3_200) | ~member(X2_204, X6_198, X3_200) | ~member(X2_204, X5_197, X3_200) | ~member(X2_204, X4_208, X3_200) | ~member(X2_204, V_207, X3_200) | ~member(X2_204, U_201, X3_200) | skf21(U_201, V_207, W_199, X_205, Y_206, Z_202, X1_203)!=V_207))). % 36.04/24.74 tff(c_144, plain, (![X3_149, W_148, V_156, X5_147, Y_155, X1_152, X2_153, X_154, Z_151, U_150, X4_157]: (X5_147=X4_157 | X4_157=W_148 | X5_147=W_148 | W_148=V_156 | X4_157=V_156 | X5_147=V_156 | V_156=U_150 | W_148=U_150 | X4_157=U_150 | X5_147=U_150 | five(X2_153, X3_149) | ~member(X2_153, X5_147, X3_149) | ~member(X2_153, X4_157, X3_149) | ~member(X2_153, W_148, X3_149) | ~member(X2_153, V_156, X3_149) | ~member(X2_153, U_150, X3_149) | skf21(U_150, V_156, W_148, X_154, Y_155, Z_151, X1_152)!=W_148))). % 36.04/24.74 tff(c_148, plain, (![Y_175, X3_169, X1_172, X_174, X2_173, Z_171, U_170, W_168, V_176]: (Y_175=X_174 | X_174=W_168 | Y_175=W_168 | W_168=V_176 | X_174=V_176 | Y_175=V_176 | V_176=U_170 | W_168=U_170 | X_174=U_170 | Y_175=U_170 | five(X2_173, X3_169) | ~member(X2_173, Y_175, X3_169) | ~member(X2_173, X_174, X3_169) | ~member(X2_173, W_168, X3_169) | ~member(X2_173, V_176, X3_169) | ~member(X2_173, U_170, X3_169) | skf21(U_170, V_176, W_168, X_174, Y_175, Z_171, X1_172)!=Y_175))). % 36.04/24.74 tff(c_665, plain, (![U_209, V_210, W_211]: (skf10(U_209, V_210, W_211)=skf20(V_210, W_211) | skf10(U_209, V_210, W_211)=skf18(V_210, W_211) | skf10(U_209, V_210, W_211)=skf16(V_210, W_211) | skf10(U_209, V_210, W_211)=skf14(V_210, W_211) | skf10(U_209, V_210, W_211)=skf12(V_210, W_211) | ~five(W_211, V_210) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.74 tff(c_142, plain, (![W_146, U_144, V_145]: (skf20(W_146, U_144)=V_145 | skf18(W_146, U_144)=V_145 | skf16(W_146, U_144)=V_145 | skf14(W_146, U_144)=V_145 | skf12(W_146, U_144)=V_145 | ~five(U_144, W_146) | ~member(U_144, V_145, W_146)))). % 36.04/24.74 tff(c_636, plain, (![W_471]: (skc8=W_471 | ~forename(skc5, W_471) | ~of(skc5, W_471, skc9)))). % 36.04/24.74 tff(c_182, plain, (![U_212, V_213, W_214, X_215]: (~event(U_212, V_213) | ~agent(U_212, V_213, W_214) | ~patient(U_212, V_213, skf10(W_214, X_215, U_212)) | ~present(U_212, V_213) | ~nonreflexive(U_212, V_213) | ~cost(U_212, V_213)))). % 36.04/24.74 tff(c_140, plain, (![W_142, V_141, U_140, X_143]: (W_142=V_141 | ~entity(U_140, X_143) | ~of(U_140, V_141, X_143) | ~forename(U_140, W_142) | ~of(U_140, W_142, X_143) | ~forename(U_140, V_141)))). % 36.04/24.74 tff(c_180, plain, (![W_211, U_209, V_210]: (member(W_211, skf10(U_209, V_210, W_211), V_210) | ssSkP0(U_209, V_210, W_211)))). % 36.04/24.74 tff(c_629, plain, (~act(skc5, skc7))). % 36.04/24.74 tff(c_615, plain, (![U_47, V_48]: (~act(U_47, V_48) | ~beverage(U_47, V_48)))). % 36.04/24.74 tff(c_624, plain, (~agent(skc5, skc6, skc7))). % 36.04/24.74 tff(c_138, plain, (![U_137, V_138, W_139]: (~agent(U_137, V_138, W_139) | ~patient(U_137, V_138, W_139) | ~nonreflexive(U_137, V_138)))). % 36.04/24.74 tff(c_591, plain, (![U_47, V_48]: (~cost(U_47, V_48) | ~beverage(U_47, V_48)))). % 36.04/24.74 tff(c_515, plain, (![U_41, V_42]: (~entity(U_41, V_42) | ~act(U_41, V_42)))). % 36.04/24.74 tff(c_602, plain, (~food(skc5, skc9))). % 36.04/24.74 tff(c_110, plain, (![U_109, V_110]: (member(U_109, skf18(V_110, U_109), V_110) | ~five(U_109, V_110)))). % 36.04/24.74 tff(c_537, plain, (![U_77, V_78]: (~food(U_77, V_78) | ~human_person(U_77, V_78)))). % 36.04/24.74 tff(c_597, plain, (~abstraction(skc5, skc7))). % 36.04/24.74 tff(c_532, plain, (![U_419, V_420]: (~abstraction(U_419, V_420) | ~beverage(U_419, V_420)))). % 36.04/24.74 tff(c_516, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~cost(U_27, V_28)))). % 36.04/24.74 tff(c_504, plain, (![U_25, V_26]: (~abstraction(U_25, V_26) | ~five(U_25, V_26)))). % 36.04/24.74 tff(c_136, plain, (![V_136, U_135]: (~five(V_136, U_135) | skf14(U_135, V_136)!=skf12(U_135, V_136)))). % 36.04/24.74 tff(c_581, plain, (~animate(skc5, skc7))). % 36.04/24.74 tff(c_562, plain, (![U_47, V_48]: (~animate(U_47, V_48) | ~beverage(U_47, V_48)))). % 36.04/24.74 tff(c_556, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~five(U_25, V_26)))). % 36.04/24.74 tff(c_108, plain, (![U_107, V_108]: (member(U_107, skf20(V_108, U_107), V_108) | ~five(U_107, V_108)))). % 36.04/24.74 tff(c_549, plain, (![U_41, V_42]: (~abstraction(U_41, V_42) | ~act(U_41, V_42)))). % 36.04/24.74 tff(c_567, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~five(U_25, V_26)))). % 36.04/24.74 tff(c_550, plain, (![U_27, V_28]: (~abstraction(U_27, V_28) | ~cost(U_27, V_28)))). % 36.04/24.74 tff(c_486, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 36.04/24.74 tff(c_464, plain, (![U_387, V_388]: (~animate(U_387, V_388) | ~food(U_387, V_388)))). % 36.04/24.74 tff(c_112, plain, (![U_111, V_112]: (member(U_111, skf16(V_112, U_111), V_112) | ~five(U_111, V_112)))). % 36.04/24.74 tff(c_498, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 36.04/24.74 tff(c_551, plain, (~abstraction(skc5, skc6))). % 36.04/24.74 tff(c_469, plain, (![U_29, V_30]: (~abstraction(U_29, V_30) | ~event(U_29, V_30)))). % 36.04/24.74 tff(c_120, plain, (![V_120, U_119]: (~five(V_120, U_119) | skf20(U_119, V_120)!=skf14(U_119, V_120)))). % 36.04/24.74 tff(c_463, plain, (![U_387, V_388]: (~living(U_387, V_388) | ~food(U_387, V_388)))). % 36.04/24.74 tff(c_531, plain, (~beverage(skc5, skc6))). % 36.04/24.74 tff(c_455, plain, (![U_47, V_48]: (entity(U_47, V_48) | ~beverage(U_47, V_48)))). % 36.04/24.74 tff(c_523, plain, (~beverage(skc5, skc9))). % 36.04/24.74 tff(c_450, plain, (![U_47, V_48]: (~female(U_47, V_48) | ~beverage(U_47, V_48)))). % 36.04/24.74 tff(c_134, plain, (![V_134, U_133]: (~five(V_134, U_133) | skf16(U_133, V_134)!=skf14(U_133, V_134)))). % 36.04/24.74 tff(c_517, plain, (~entity(skc5, skc6))). % 36.04/24.74 tff(c_492, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~event(U_29, V_30)))). % 36.04/24.74 tff(c_445, plain, (![U_21, V_22]: (~abstraction(U_21, V_22) | ~group(U_21, V_22)))). % 36.04/24.74 tff(c_132, plain, (![V_132, U_131]: (~five(V_132, U_131) | skf16(U_131, V_132)!=skf12(U_131, V_132)))). % 36.04/24.74 tff(c_403, plain, (![U_369, V_370]: (~multiple(U_369, V_370) | ~eventuality(U_369, V_370)))). % 36.04/24.74 tff(c_420, plain, (![U_371, V_372]: (impartial(U_371, V_372) | ~food(U_371, V_372)))). % 36.04/24.74 tff(c_375, plain, (![U_59, V_60]: (~eventuality(U_59, V_60) | ~entity(U_59, V_60)))). % 36.04/24.74 tff(c_381, plain, (![U_5, V_6]: (abstraction(U_5, V_6) | ~cash(U_5, V_6)))). % 36.04/24.74 tff(c_353, plain, (![U_341, V_342]: (~multiple(U_341, V_342) | ~entity(U_341, V_342)))). % 36.04/24.74 tff(c_114, plain, (![U_113, V_114]: (member(U_113, skf14(V_114, U_113), V_114) | ~five(U_113, V_114)))). % 36.04/24.74 tff(c_347, plain, (![U_17, V_18]: (~entity(U_17, V_18) | ~abstraction(U_17, V_18)))). % 36.04/24.74 tff(c_475, plain, (abstraction(skc5, skc8))). % 36.04/24.74 tff(c_359, plain, (![U_345, V_346]: (abstraction(U_345, V_346) | ~forename(U_345, V_346)))). % 36.04/24.74 tff(c_118, plain, (![V_118, U_117]: (~five(V_118, U_117) | skf20(U_117, V_118)!=skf12(U_117, V_118)))). % 36.04/24.74 tff(c_387, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~abstraction(U_17, V_18)))). % 36.04/24.74 tff(c_419, plain, (![U_371, V_372]: (nonliving(U_371, V_372) | ~food(U_371, V_372)))). % 36.04/24.74 tff(c_418, plain, (![U_371, V_372]: (entity(U_371, V_372) | ~food(U_371, V_372)))). % 36.04/24.74 tff(c_417, plain, (![U_371, V_372]: (~female(U_371, V_372) | ~food(U_371, V_372)))). % 36.04/24.74 tff(c_392, plain, (![U_363, V_364]: (~multiple(U_363, V_364) | ~abstraction(U_363, V_364)))). % 36.04/24.74 tff(c_116, plain, (![U_115, V_116]: (member(U_115, skf12(V_116, U_115), V_116) | ~five(U_115, V_116)))). % 36.04/24.74 tff(c_248, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 36.04/24.74 tff(c_437, plain, (~cost(skc5, skc9))). % 36.04/24.74 tff(c_436, plain, (~act(skc5, skc9))). % 36.04/24.74 tff(c_122, plain, (![V_122, U_121]: (~five(V_122, U_121) | skf20(U_121, V_122)!=skf16(U_121, V_122)))). % 36.04/24.74 tff(c_429, plain, (~event(skc5, skc9))). % 36.04/24.74 tff(c_425, plain, (~eventuality(skc5, skc9))). % 36.04/24.74 tff(c_319, plain, (![U_37, V_38]: (~female(U_37, V_38) | ~eventuality(U_37, V_38)))). % 36.04/24.74 tff(c_258, plain, (![U_49, V_50]: (object(U_49, V_50) | ~food(U_49, V_50)))). % 36.04/24.74 tff(c_240, plain, (![U_31, V_32]: (singleton(U_31, V_32) | ~eventuality(U_31, V_32)))). % 36.04/24.74 tff(c_130, plain, (![V_130, U_129]: (~five(V_130, U_129) | skf18(U_129, V_130)!=skf16(U_129, V_130)))). % 36.04/24.74 tff(c_341, plain, (![U_333, V_334]: (~female(U_333, V_334) | ~abstraction(U_333, V_334)))). % 36.04/24.74 tff(c_294, plain, (![U_311, V_312]: (singleton(U_311, V_312) | ~abstraction(U_311, V_312)))). % 36.04/24.74 tff(c_329, plain, (![U_33, V_34]: (~general(U_33, V_34) | ~eventuality(U_33, V_34)))). % 36.04/24.74 tff(c_126, plain, (![V_126, U_125]: (~five(V_126, U_125) | skf18(U_125, V_126)!=skf12(U_125, V_126)))). % 36.04/24.74 tff(c_304, plain, (![U_315, V_316]: (abstraction(U_315, V_316) | ~currency(U_315, V_316)))). % 36.04/24.74 tff(c_320, plain, (![U_65, V_66]: (~female(U_65, V_66) | ~object(U_65, V_66)))). % 36.04/24.74 tff(c_274, plain, (![U_295, V_296]: (~existent(U_295, V_296) | ~eventuality(U_295, V_296)))). % 36.04/24.74 tff(c_370, plain, (entity(skc5, skc9))). % 36.04/24.74 tff(c_253, plain, (![U_77, V_78]: (entity(U_77, V_78) | ~human_person(U_77, V_78)))). % 36.04/24.74 tff(c_128, plain, (![V_128, U_127]: (~five(V_128, U_127) | skf18(U_127, V_128)!=skf14(U_127, V_128)))). % 36.04/24.74 tff(c_364, plain, (~abstraction(skc5, skc9))). % 36.04/24.74 tff(c_309, plain, (![U_317, V_318]: (~human(U_317, V_318) | ~abstraction(U_317, V_318)))). % 36.04/24.74 tff(c_206, plain, (![U_67, V_68]: (relation(U_67, V_68) | ~forename(U_67, V_68)))). % 36.04/24.74 tff(c_124, plain, (![V_124, U_123]: (~five(V_124, U_123) | skf20(U_123, V_124)!=skf18(U_123, V_124)))). % 36.04/24.74 tff(c_289, plain, (![U_309, V_310]: (singleton(U_309, V_310) | ~entity(U_309, V_310)))). % 36.04/24.74 tff(c_234, plain, (![U_77, V_78]: (living(U_77, V_78) | ~human_person(U_77, V_78)))). % 36.04/24.74 tff(c_328, plain, (![U_57, V_58]: (~general(U_57, V_58) | ~entity(U_57, V_58)))). % 36.04/24.75 tff(c_268, plain, (![U_77, V_78]: (impartial(U_77, V_78) | ~human_person(U_77, V_78)))). % 36.04/24.75 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~abstraction(U_19, V_20)))). % 36.04/24.75 tff(c_100, plain, (![U_99, V_100]: (~nonliving(U_99, V_100) | ~living(U_99, V_100)))). % 36.04/24.75 tff(c_335, plain, (human(skc5, skc9))). % 36.04/24.75 tff(c_86, plain, (![U_85, V_86]: (human(U_85, V_86) | ~human_person(U_85, V_86)))). % 36.04/24.75 tff(c_96, plain, (![U_95, V_96]: (~singleton(U_95, V_96) | ~multiple(U_95, V_96)))). % 36.04/24.75 tff(c_94, plain, (![U_93, V_94]: (~specific(U_93, V_94) | ~general(U_93, V_94)))). % 36.04/24.75 tff(c_92, plain, (![U_91, V_92]: (~unisex(U_91, V_92) | ~female(U_91, V_92)))). % 36.04/24.75 tff(c_30, plain, (![U_29, V_30]: (eventuality(U_29, V_30) | ~event(U_29, V_30)))). % 36.04/24.75 tff(c_98, plain, (![U_97, V_98]: (~present(U_97, V_98) | ~past(U_97, V_98)))). % 36.04/24.75 tff(c_16, plain, (![U_15, V_16]: (nonhuman(U_15, V_16) | ~abstraction(U_15, V_16)))). % 36.04/24.75 tff(c_299, plain, (female(skc5, skc9))). % 36.04/24.75 tff(c_8, plain, (![U_7, V_8]: (possession(U_7, V_8) | ~currency(U_7, V_8)))). % 36.04/24.75 tff(c_90, plain, (![U_89, V_90]: (female(U_89, V_90) | ~woman(U_89, V_90)))). % 36.04/24.75 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~abstraction(U_11, V_12)))). % 36.04/24.75 tff(c_56, plain, (![U_55, V_56]: (thing(U_55, V_56) | ~entity(U_55, V_56)))). % 36.04/24.75 tff(c_6, plain, (![U_5, V_6]: (currency(U_5, V_6) | ~cash(U_5, V_6)))). % 36.04/24.75 tff(c_102, plain, (![U_101, V_102]: (~nonhuman(U_101, V_102) | ~human(U_101, V_102)))). % 36.04/24.75 tff(c_72, plain, (![U_71, V_72]: (abstraction(U_71, V_72) | ~relation(U_71, V_72)))). % 36.04/24.75 tff(c_58, plain, (![U_57, V_58]: (specific(U_57, V_58) | ~entity(U_57, V_58)))). % 36.04/24.75 tff(c_280, plain, (animate(skc5, skc9))). % 36.04/24.75 tff(c_88, plain, (![U_87, V_88]: (animate(U_87, V_88) | ~human_person(U_87, V_88)))). % 36.04/24.75 tff(c_48, plain, (![U_47, V_48]: (food(U_47, V_48) | ~beverage(U_47, V_48)))). % 36.04/24.75 tff(c_36, plain, (![U_35, V_36]: (nonexistent(U_35, V_36) | ~eventuality(U_35, V_36)))). % 36.04/24.75 tff(c_10, plain, (![U_9, V_10]: (abstraction(U_9, V_10) | ~possession(U_9, V_10)))). % 36.04/24.75 tff(c_263, plain, (human_person(skc5, skc9))). % 36.04/24.75 tff(c_82, plain, (![U_81, V_82]: (impartial(U_81, V_82) | ~organism(U_81, V_82)))). % 36.04/24.75 tff(c_76, plain, (![U_75, V_76]: (human_person(U_75, V_76) | ~woman(U_75, V_76)))). % 36.04/24.75 tff(c_52, plain, (![U_51, V_52]: (object(U_51, V_52) | ~substance_matter(U_51, V_52)))). % 36.04/24.75 tff(c_80, plain, (![U_79, V_80]: (entity(U_79, V_80) | ~organism(U_79, V_80)))). % 36.04/24.75 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 36.04/24.75 tff(c_104, plain, (![U_103, V_104]: (~existent(U_103, V_104) | ~nonexistent(U_103, V_104)))). % 36.04/24.75 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~five(U_25, V_26)))). % 36.04/24.75 tff(c_54, plain, (![U_53, V_54]: (entity(U_53, V_54) | ~object(U_53, V_54)))). % 36.04/24.75 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 36.04/24.75 tff(c_32, plain, (![U_31, V_32]: (thing(U_31, V_32) | ~eventuality(U_31, V_32)))). % 36.04/24.75 tff(c_84, plain, (![U_83, V_84]: (living(U_83, V_84) | ~organism(U_83, V_84)))). % 36.04/24.75 tff(c_74, plain, (![U_73, V_74]: (forename(U_73, V_74) | ~mia_forename(U_73, V_74)))). % 36.04/24.75 tff(c_106, plain, (![U_105, V_106]: (~animate(U_105, V_106) | ~nonliving(U_105, V_106)))). % 36.04/24.75 tff(c_38, plain, (![U_37, V_38]: (unisex(U_37, V_38) | ~eventuality(U_37, V_38)))). % 36.04/24.75 tff(c_18, plain, (![U_17, V_18]: (general(U_17, V_18) | ~abstraction(U_17, V_18)))). % 36.04/24.75 tff(c_219, plain, (act(skc5, skc6))). % 36.04/24.75 tff(c_42, plain, (![U_41, V_42]: (event(U_41, V_42) | ~act(U_41, V_42)))). % 36.04/24.75 tff(c_40, plain, (![U_39, V_40]: (act(U_39, V_40) | ~order(U_39, V_40)))). % 36.04/24.75 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~cost(U_27, V_28)))). % 36.04/24.75 tff(c_62, plain, (![U_61, V_62]: (nonliving(U_61, V_62) | ~object(U_61, V_62)))). % 36.04/24.75 tff(c_44, plain, (![U_43, V_44]: (event(U_43, V_44) | ~order(U_43, V_44)))). % 36.04/24.75 tff(c_70, plain, (![U_69, V_70]: (relation(U_69, V_70) | ~relname(U_69, V_70)))). % 36.04/24.75 tff(c_50, plain, (![U_49, V_50]: (substance_matter(U_49, V_50) | ~food(U_49, V_50)))). % 36.04/24.75 tff(c_66, plain, (![U_65, V_66]: (unisex(U_65, V_66) | ~object(U_65, V_66)))). % 36.04/24.75 tff(c_60, plain, (![U_59, V_60]: (existent(U_59, V_60) | ~entity(U_59, V_60)))). % 36.04/24.75 tff(c_198, plain, (beverage(skc5, skc7))). % 36.04/24.75 tff(c_46, plain, (![U_45, V_46]: (beverage(U_45, V_46) | ~shake_beverage(U_45, V_46)))). % 36.04/24.75 tff(c_78, plain, (![U_77, V_78]: (organism(U_77, V_78) | ~human_person(U_77, V_78)))). % 36.04/24.75 tff(c_4, plain, (![U_3, V_4]: (cash(U_3, V_4) | ~dollar(U_3, V_4)))). % 36.04/24.75 tff(c_68, plain, (![U_67, V_68]: (relname(U_67, V_68) | ~forename(U_67, V_68)))). % 36.04/24.75 tff(c_34, plain, (![U_33, V_34]: (specific(U_33, V_34) | ~eventuality(U_33, V_34)))). % 36.04/24.75 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 36.04/24.75 tff(c_64, plain, (![U_63, V_64]: (impartial(U_63, V_64) | ~object(U_63, V_64)))). % 36.04/24.75 tff(c_176, plain, (agent(skc5, skc6, skc9))). % 36.04/24.75 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 36.04/24.75 tff(c_178, plain, (patient(skc5, skc6, skc7))). % 36.04/24.75 tff(c_174, plain, (of(skc5, skc8, skc9))). % 36.04/24.75 tff(c_162, plain, (order(skc5, skc6))). % 36.04/24.75 tff(c_160, plain, (shake_beverage(skc5, skc7))). % 36.04/24.75 tff(c_158, plain, (woman(skc5, skc9))). % 36.04/24.75 tff(c_164, plain, (nonreflexive(skc5, skc6))). % 36.04/24.75 tff(c_166, plain, (past(skc5, skc6))). % 36.04/24.75 tff(c_168, plain, (event(skc5, skc6))). % 36.04/24.75 tff(c_170, plain, (forename(skc5, skc8))). % 36.04/24.75 tff(c_172, plain, (mia_forename(skc5, skc8))). % 36.04/24.75 tff(c_156, plain, (actual_world(skc5))). % 36.04/24.75 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 36.04/24.75 %------------------------------------------------------------------------------