%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP055-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n014.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:03 PM UTC 2025 % Result : Satisfiable 26.93s 18.13s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NLP055-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 08:17:35 EDT 2025 % 0.13/0.34 % CPUTime : % 26.93/18.13 % 26.93/18.13 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 26.93/18.13 % 26.93/18.13 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 26.93/18.14 %$ 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 % 26.93/18.14 % 26.93/18.14 %Foreground sorts: % 26.93/18.14 % 26.93/18.14 % 26.93/18.14 %Background operators: % 26.93/18.14 % 26.93/18.14 % 26.93/18.14 %Foreground operators: % 26.93/18.14 tff(nonliving, type, nonliving: ($i * $i) > $o). % 26.93/18.14 tff(relation, type, relation: ($i * $i) > $o). % 26.93/18.14 tff(member, type, member: ($i * $i * $i) > $o). % 26.93/18.14 tff(forename, type, forename: ($i * $i) > $o). % 26.93/18.14 tff(skc7, type, skc7: $i). % 26.93/18.14 tff(female, type, female: ($i * $i) > $o). % 26.93/18.14 tff(living, type, living: ($i * $i) > $o). % 26.93/18.14 tff(cost, type, cost: ($i * $i) > $o). % 26.93/18.14 tff(human_person, type, human_person: ($i * $i) > $o). % 26.93/18.14 tff(present, type, present: ($i * $i) > $o). % 26.93/18.14 tff(entity, type, entity: ($i * $i) > $o). % 26.93/18.14 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 26.93/18.14 tff(skc9, type, skc9: $i). % 26.93/18.14 tff(past, type, past: ($i * $i) > $o). % 26.93/18.14 tff(beverage, type, beverage: ($i * $i) > $o). % 26.93/18.14 tff(eventuality, type, eventuality: ($i * $i) > $o). % 26.93/18.14 tff(existent, type, existent: ($i * $i) > $o). % 26.93/18.14 tff(abstraction, type, abstraction: ($i * $i) > $o). % 26.93/18.14 tff(skc8, type, skc8: $i). % 26.93/18.14 tff(relname, type, relname: ($i * $i) > $o). % 26.93/18.14 tff(possession, type, possession: ($i * $i) > $o). % 26.93/18.14 tff(singleton, type, singleton: ($i * $i) > $o). % 26.93/18.14 tff(multiple, type, multiple: ($i * $i) > $o). % 26.93/18.14 tff(organism, type, organism: ($i * $i) > $o). % 26.93/18.14 tff(shake_beverage, type, shake_beverage: ($i * $i) > $o). % 26.93/18.14 tff(animate, type, animate: ($i * $i) > $o). % 26.93/18.14 tff(of, type, of: ($i * $i * $i) > $o). % 26.93/18.14 tff(skf14, type, skf14: ($i * $i) > $i). % 26.93/18.14 tff(actual_world, type, actual_world: $i > $o). % 26.93/18.14 tff(dollar, type, dollar: ($i * $i) > $o). % 26.93/18.14 tff(agent, type, agent: ($i * $i * $i) > $o). % 26.93/18.14 tff(group, type, group: ($i * $i) > $o). % 26.93/18.14 tff(five, type, five: ($i * $i) > $o). % 26.93/18.14 tff(general, type, general: ($i * $i) > $o). % 26.93/18.14 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 26.93/18.14 tff(food, type, food: ($i * $i) > $o). % 26.93/18.14 tff(event, type, event: ($i * $i) > $o). % 26.93/18.14 tff(woman, type, woman: ($i * $i) > $o). % 26.93/18.14 tff(currency, type, currency: ($i * $i) > $o). % 26.93/18.14 tff(patient, type, patient: ($i * $i * $i) > $o). % 26.93/18.14 tff(skf8, type, skf8: ($i * $i) > $i). % 26.93/18.14 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 26.93/18.14 tff(cash, type, cash: ($i * $i) > $o). % 26.93/18.14 tff(thing, type, thing: ($i * $i) > $o). % 26.93/18.14 tff(human, type, human: ($i * $i) > $o). % 26.93/18.14 tff(skf10, type, skf10: ($i * $i * $i) > $i). % 26.93/18.14 tff(skf18, type, skf18: ($i * $i) > $i). % 26.93/18.14 tff(ssSkP0, type, ssSkP0: ($i * $i * $i) > $o). % 26.93/18.14 tff(skc5, type, skc5: $i). % 26.93/18.14 tff(unisex, type, unisex: ($i * $i) > $o). % 26.93/18.14 tff(skf16, type, skf16: ($i * $i) > $i). % 26.93/18.14 tff(set, type, set: ($i * $i) > $o). % 26.93/18.14 tff(skf12, type, skf12: ($i * $i) > $i). % 26.93/18.14 tff(skc6, type, skc6: $i). % 26.93/18.14 tff(impartial, type, impartial: ($i * $i) > $o). % 26.93/18.14 tff(object, type, object: ($i * $i) > $o). % 26.93/18.14 tff(order, type, order: ($i * $i) > $o). % 26.93/18.14 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 26.93/18.14 tff(specific, type, specific: ($i * $i) > $o). % 26.93/18.14 tff(skf20, type, skf20: ($i * $i) > $i). % 26.93/18.14 tff(act, type, act: ($i * $i) > $o). % 26.93/18.14 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 26.93/18.14 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i) > $i). % 26.93/18.14 % 26.93/18.14 %Saturated clause set: % 26.93/18.15 tff(c_1488, plain, (![V_1492, X_1499, X_1488, X1_1505, X1_1509, X_1507, Z_1512, U_178, Z_1489, X_181, Z_179, X1_1508, X1_1497, V_1490, W_1503, Y_1491, V_1513, Y_1498, Z_1516, Y_182, Z_1496, Y_1515, V_1495, X_1511, X1_180, W_177, V_1501, V_183, X1_1506, Y_1500, Y_1493, X_1510, Z_1502]: (skf21(V_1513, X_1488, Y_1493, Z_1489, X1_1497, W_177, U_178)=skf21(V_1501, X_1499, Y_1498, Z_1512, X1_1508, W_177, U_178) | skf21(V_1501, X_1499, Y_1498, Z_1512, X1_1508, W_177, U_178)=skf21(V_1490, X_1507, Y_1500, Z_1516, X1_1505, W_177, U_178) | skf21(V_1513, X_1488, Y_1493, Z_1489, X1_1497, W_177, U_178)=skf21(V_1490, X_1507, Y_1500, Z_1516, X1_1505, W_177, U_178) | skf21(V_1492, X_1511, Y_1491, Z_1502, X1_1506, W_177, U_178)=skf21(V_1490, X_1507, Y_1500, Z_1516, X1_1505, W_177, U_178) | skf21(V_1501, X_1499, Y_1498, Z_1512, X1_1508, W_177, U_178)=skf21(V_1492, X_1511, Y_1491, Z_1502, X1_1506, W_177, U_178) | skf21(V_1513, X_1488, Y_1493, Z_1489, X1_1497, W_177, U_178)=skf21(V_1492, X_1511, Y_1491, Z_1502, X1_1506, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1492, X_1511, Y_1491, Z_1502, X1_1506, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1490, X_1507, Y_1500, Z_1516, X1_1505, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1501, X_1499, Y_1498, Z_1512, X1_1508, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1513, X_1488, Y_1493, Z_1489, X1_1497, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1495, W_1503, X_1510, Y_1515, Z_1496, X1_1509)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1489=X1_1497 | Z_1489=Y_1493 | Y_1493=X1_1497 | Y_1493=X_1488 | Z_1489=X_1488 | X_1488=X1_1497 | X_1488=V_1513 | Y_1493=V_1513 | Z_1489=V_1513 | X1_1497=V_1513 | ~member(U_178, X1_1497, W_177) | ~member(U_178, Z_1489, W_177) | ~member(U_178, Y_1493, W_177) | ~member(U_178, X_1488, W_177) | ~member(U_178, V_1513, W_177) | Z_1512=X1_1508 | Z_1512=Y_1498 | Y_1498=X1_1508 | Y_1498=X_1499 | Z_1512=X_1499 | X_1499=X1_1508 | X_1499=V_1501 | Y_1498=V_1501 | Z_1512=V_1501 | X1_1508=V_1501 | ~member(U_178, X1_1508, W_177) | ~member(U_178, Z_1512, W_177) | ~member(U_178, Y_1498, W_177) | ~member(U_178, X_1499, W_177) | ~member(U_178, V_1501, W_177) | Z_1516=X1_1505 | Z_1516=Y_1500 | Y_1500=X1_1505 | Y_1500=X_1507 | Z_1516=X_1507 | X_1507=X1_1505 | X_1507=V_1490 | Y_1500=V_1490 | Z_1516=V_1490 | X1_1505=V_1490 | ~member(U_178, X1_1505, W_177) | ~member(U_178, Z_1516, W_177) | ~member(U_178, Y_1500, W_177) | ~member(U_178, X_1507, W_177) | ~member(U_178, V_1490, W_177) | Z_1502=X1_1506 | Z_1502=Y_1491 | Y_1491=X1_1506 | Y_1491=X_1511 | Z_1502=X_1511 | X_1511=X1_1506 | X_1511=V_1492 | Y_1491=V_1492 | Z_1502=V_1492 | X1_1506=V_1492 | ~member(U_178, X1_1506, W_177) | ~member(U_178, Z_1502, W_177) | ~member(U_178, Y_1491, W_177) | ~member(U_178, X_1511, W_177) | ~member(U_178, V_1492, 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)))). % 26.93/18.15 tff(c_1461, plain, (![Z_1356, Y_1365, V_1366, X1_1355, U_178, X_1364, X_181, Z_179, V_1345, V_1362, U_1351, X1_1347, Z_1343, X_1361, Y_1344, Y_182, Y_1348, Z_1349, Z_1353, X1_1360, X1_180, Y_1352, W_177, V_183, W_1357, V_1354, X_1342, X1_1350, X_1363]: (skf21(V_1354, X_1364, Y_1352, Z_1349, X1_1355, W_177, U_178)=skf10(U_1351, W_177, U_178) | skf21(V_1366, X_1342, Y_1348, Z_1353, X1_1347, W_177, U_178)=skf10(U_1351, W_177, U_178) | skf21(V_1366, X_1342, Y_1348, Z_1353, X1_1347, W_177, U_178)=skf21(V_1354, X_1364, Y_1352, Z_1349, X1_1355, W_177, U_178) | skf21(V_1366, X_1342, Y_1348, Z_1353, X1_1347, W_177, U_178)=skf21(V_1345, X_1363, Y_1344, Z_1356, X1_1360, W_177, U_178) | skf21(V_1345, X_1363, Y_1344, Z_1356, X1_1360, W_177, U_178)=skf10(U_1351, W_177, U_178) | skf21(V_1354, X_1364, Y_1352, Z_1349, X1_1355, W_177, U_178)=skf21(V_1345, X_1363, Y_1344, Z_1356, X1_1360, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1345, X_1363, Y_1344, Z_1356, X1_1360, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1366, X_1342, Y_1348, Z_1353, X1_1347, 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_1354, X_1364, Y_1352, Z_1349, 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_1357, X_1361, Y_1365, Z_1343, X1_1350)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1349=X1_1355 | Z_1349=Y_1352 | Y_1352=X1_1355 | Y_1352=X_1364 | Z_1349=X_1364 | X_1364=X1_1355 | X_1364=V_1354 | Y_1352=V_1354 | Z_1349=V_1354 | X1_1355=V_1354 | ~member(U_178, X1_1355, W_177) | ~member(U_178, Z_1349, W_177) | ~member(U_178, Y_1352, W_177) | ~member(U_178, X_1364, W_177) | ~member(U_178, V_1354, W_177) | ssSkP0(U_1351, W_177, U_178) | Z_1353=X1_1347 | Z_1353=Y_1348 | Y_1348=X1_1347 | Y_1348=X_1342 | Z_1353=X_1342 | X_1342=X1_1347 | X_1342=V_1366 | Y_1348=V_1366 | Z_1353=V_1366 | X1_1347=V_1366 | ~member(U_178, X1_1347, W_177) | ~member(U_178, Z_1353, W_177) | ~member(U_178, Y_1348, W_177) | ~member(U_178, X_1342, W_177) | ~member(U_178, V_1366, W_177) | Z_1356=X1_1360 | Z_1356=Y_1344 | Y_1344=X1_1360 | Y_1344=X_1363 | Z_1356=X_1363 | X_1363=X1_1360 | X_1363=V_1345 | Y_1344=V_1345 | Z_1356=V_1345 | X1_1360=V_1345 | ~member(U_178, X1_1360, W_177) | ~member(U_178, Z_1356, W_177) | ~member(U_178, Y_1344, W_177) | ~member(U_178, X_1363, W_177) | ~member(U_178, V_1345, 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)))). % 26.93/18.15 tff(c_1489, plain, (![V_1492, X_1499, X_1488, X1_1505, X1_1509, X_1507, W_211, Z_1512, V_210, Z_1489, X1_1508, X1_1497, V_1490, W_1503, Y_1491, V_1513, Y_1498, Z_1516, Z_1496, Y_1515, V_1495, X_1511, V_1501, X1_1506, U_209, Y_1500, Y_1493, X_1510, Z_1502]: (skf21(V_1513, X_1488, Y_1493, Z_1489, X1_1497, V_210, W_211)=skf21(V_1501, X_1499, Y_1498, Z_1512, X1_1508, V_210, W_211) | skf21(V_1501, X_1499, Y_1498, Z_1512, X1_1508, V_210, W_211)=skf21(V_1490, X_1507, Y_1500, Z_1516, X1_1505, V_210, W_211) | skf21(V_1513, X_1488, Y_1493, Z_1489, X1_1497, V_210, W_211)=skf21(V_1490, X_1507, Y_1500, Z_1516, X1_1505, V_210, W_211) | skf21(V_1492, X_1511, Y_1491, Z_1502, X1_1506, V_210, W_211)=skf21(V_1490, X_1507, Y_1500, Z_1516, X1_1505, V_210, W_211) | skf21(V_1501, X_1499, Y_1498, Z_1512, X1_1508, V_210, W_211)=skf21(V_1492, X_1511, Y_1491, Z_1502, X1_1506, V_210, W_211) | skf21(V_1513, X_1488, Y_1493, Z_1489, X1_1497, V_210, W_211)=skf21(V_1492, X_1511, Y_1491, Z_1502, X1_1506, V_210, W_211) | skf21(V_1492, X_1511, Y_1491, Z_1502, X1_1506, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1490, X_1507, Y_1500, Z_1516, X1_1505, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1501, X_1499, Y_1498, Z_1512, X1_1508, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1513, X_1488, Y_1493, Z_1489, X1_1497, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1495, W_1503, X_1510, Y_1515, Z_1496, X1_1509)!=skf10(U_209, V_210, W_211) | Z_1489=X1_1497 | Z_1489=Y_1493 | Y_1493=X1_1497 | Y_1493=X_1488 | Z_1489=X_1488 | X_1488=X1_1497 | X_1488=V_1513 | Y_1493=V_1513 | Z_1489=V_1513 | X1_1497=V_1513 | ~member(W_211, X1_1497, V_210) | ~member(W_211, Z_1489, V_210) | ~member(W_211, Y_1493, V_210) | ~member(W_211, X_1488, V_210) | ~member(W_211, V_1513, V_210) | Z_1512=X1_1508 | Z_1512=Y_1498 | Y_1498=X1_1508 | Y_1498=X_1499 | Z_1512=X_1499 | X_1499=X1_1508 | X_1499=V_1501 | Y_1498=V_1501 | Z_1512=V_1501 | X1_1508=V_1501 | ~member(W_211, X1_1508, V_210) | ~member(W_211, Z_1512, V_210) | ~member(W_211, Y_1498, V_210) | ~member(W_211, X_1499, V_210) | ~member(W_211, V_1501, V_210) | Z_1516=X1_1505 | Z_1516=Y_1500 | Y_1500=X1_1505 | Y_1500=X_1507 | Z_1516=X_1507 | X_1507=X1_1505 | X_1507=V_1490 | Y_1500=V_1490 | Z_1516=V_1490 | X1_1505=V_1490 | ~member(W_211, X1_1505, V_210) | ~member(W_211, Z_1516, V_210) | ~member(W_211, Y_1500, V_210) | ~member(W_211, X_1507, V_210) | ~member(W_211, V_1490, V_210) | Z_1502=X1_1506 | Z_1502=Y_1491 | Y_1491=X1_1506 | Y_1491=X_1511 | Z_1502=X_1511 | X_1511=X1_1506 | X_1511=V_1492 | Y_1491=V_1492 | Z_1502=V_1492 | X1_1506=V_1492 | five(W_211, V_210) | ~member(W_211, X1_1506, V_210) | ~member(W_211, Z_1502, V_210) | ~member(W_211, Y_1491, V_210) | ~member(W_211, X_1511, V_210) | ~member(W_211, V_1492, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.15 tff(c_1439, plain, (![X1_1329, Z_1331, V_1341, U_1340, X1_1332, X_1336, U_178, V_1323, X_181, X1_1325, Z_179, Y_1322, Z_1324, Z_1328, Y_182, V_1319, X_1339, Y_1330, X1_180, Y_1318, Y_1320, X_1326, W_177, X1_1334, W_1335, V_183, Z_1337, X_1327]: (skf21(V_1341, X_1339, Y_1320, Z_1328, X1_1332, W_177, U_178)=skf21(V_1323, X_1326, Y_1322, Z_1337, X1_1325, W_177, U_178) | skf21(V_1323, X_1326, Y_1322, Z_1337, X1_1325, W_177, U_178)=skf21(V_1319, X_1336, Y_1318, Z_1331, X1_1334, W_177, U_178) | skf21(V_1341, X_1339, Y_1320, Z_1328, X1_1332, W_177, U_178)=skf21(V_1319, X_1336, Y_1318, Z_1331, X1_1334, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1319, X_1336, Y_1318, Z_1331, X1_1334, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1323, X_1326, Y_1322, Z_1337, X1_1325, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1341, X_1339, Y_1320, Z_1328, X1_1332, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1340 | skf21(V_1319, X_1336, Y_1318, Z_1331, X1_1334, W_177, U_178)=U_1340 | skf21(V_1323, X_1326, Y_1322, Z_1337, X1_1325, W_177, U_178)=U_1340 | skf21(V_1341, X_1339, Y_1320, Z_1328, X1_1332, W_177, U_178)=U_1340 | ~member(U_178, U_1340, W_177) | skf21(U_1340, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_1335, X_1327, Y_1330, Z_1324, X1_1329)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1328=X1_1332 | Z_1328=Y_1320 | Y_1320=X1_1332 | Y_1320=X_1339 | Z_1328=X_1339 | X_1339=X1_1332 | X_1339=V_1341 | Y_1320=V_1341 | Z_1328=V_1341 | X1_1332=V_1341 | ~member(U_178, X1_1332, W_177) | ~member(U_178, Z_1328, W_177) | ~member(U_178, Y_1320, W_177) | ~member(U_178, X_1339, W_177) | ~member(U_178, V_1341, W_177) | Z_1337=X1_1325 | Z_1337=Y_1322 | Y_1322=X1_1325 | Y_1322=X_1326 | Z_1337=X_1326 | X_1326=X1_1325 | X_1326=V_1323 | Y_1322=V_1323 | Z_1337=V_1323 | X1_1325=V_1323 | ~member(U_178, X1_1325, W_177) | ~member(U_178, Z_1337, W_177) | ~member(U_178, Y_1322, W_177) | ~member(U_178, X_1326, W_177) | ~member(U_178, V_1323, W_177) | Z_1331=X1_1334 | Z_1331=Y_1318 | Y_1318=X1_1334 | Y_1318=X_1336 | Z_1331=X_1336 | X_1336=X1_1334 | X_1336=V_1319 | Y_1318=V_1319 | Z_1331=V_1319 | X1_1334=V_1319 | ~member(U_178, X1_1334, W_177) | ~member(U_178, Z_1331, W_177) | ~member(U_178, Y_1318, W_177) | ~member(U_178, X_1336, W_177) | ~member(U_178, V_1319, 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)))). % 27.04/18.15 tff(c_1417, plain, (![W_1304, V_1295, V_1305, U_178, X1_1313, X_181, Z_179, Z_1310, V_1299, Z_1317, X_1293, X1_1303, X_1298, Y_182, U_1300, Z_1296, Z_1312, Y_1314, Y_1294, X1_180, W_177, V_183, X_1316, X_1315, Y_1309, X1_1307, X1_1297, Y_1306, V_1302]: (skf21(V_1305, X_1298, Y_1309, Z_1312, X1_1297, W_177, U_178)=skf21(V_1299, X_1293, Y_1314, Z_1296, X1_1307, W_177, U_178) | skf21(V_1305, X_1298, Y_1309, Z_1312, X1_1297, W_177, U_178)=skf21(V_1295, X_1315, Y_1294, Z_1310, X1_1313, W_177, U_178) | skf21(V_1299, X_1293, Y_1314, Z_1296, X1_1307, W_177, U_178)=skf21(V_1295, X_1315, Y_1294, Z_1310, X1_1313, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1295, X_1315, Y_1294, Z_1310, X1_1313, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1305, X_1298, Y_1309, Z_1312, X1_1297, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1299, X_1293, Y_1314, Z_1296, X1_1307, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1300 | skf21(V_1295, X_1315, Y_1294, Z_1310, X1_1313, W_177, U_178)=U_1300 | skf21(V_1305, X_1298, Y_1309, Z_1312, X1_1297, W_177, U_178)=U_1300 | skf21(V_1299, X_1293, Y_1314, Z_1296, X1_1307, W_177, U_178)=U_1300 | ~member(U_178, U_1300, W_177) | skf21(U_1300, V_1302, W_1304, X_1316, Y_1306, Z_1317, X1_1303)!=U_1300 | Z_1296=X1_1307 | Z_1296=Y_1314 | Y_1314=X1_1307 | Y_1314=X_1293 | Z_1296=X_1293 | X_1293=X1_1307 | X_1293=V_1299 | Y_1314=V_1299 | Z_1296=V_1299 | X1_1307=V_1299 | ~member(U_178, X1_1307, W_177) | ~member(U_178, Z_1296, W_177) | ~member(U_178, Y_1314, W_177) | ~member(U_178, X_1293, W_177) | ~member(U_178, V_1299, W_177) | Z_1312=X1_1297 | Z_1312=Y_1309 | Y_1309=X1_1297 | Y_1309=X_1298 | Z_1312=X_1298 | X_1298=X1_1297 | X_1298=V_1305 | Y_1309=V_1305 | Z_1312=V_1305 | X1_1297=V_1305 | ~member(U_178, X1_1297, W_177) | ~member(U_178, Z_1312, W_177) | ~member(U_178, Y_1309, W_177) | ~member(U_178, X_1298, W_177) | ~member(U_178, V_1305, W_177) | Z_1310=X1_1313 | Z_1310=Y_1294 | Y_1294=X1_1313 | Y_1294=X_1315 | Z_1310=X_1315 | X_1315=X1_1313 | X_1315=V_1295 | Y_1294=V_1295 | Z_1310=V_1295 | X1_1313=V_1295 | ~member(U_178, X1_1313, W_177) | ~member(U_178, Z_1310, W_177) | ~member(U_178, Y_1294, W_177) | ~member(U_178, X_1315, W_177) | ~member(U_178, V_1295, 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)))). % 27.04/18.15 tff(c_1390, plain, (![W_1184, X1_1178, Y_1180, U_1179, V_1191, U_178, V_1187, X_1171, Y_1176, Z_1172, X_181, Z_179, X_1186, X1_1183, X1_1175, V_1182, Y_182, X_1189, U_1173, Z_1181, X1_180, W_177, Z_1177, V_183, Y_1190]: (skf21(V_1182, X_1189, Y_1180, Z_1177, X1_1183, W_177, U_178)=skf10(U_1179, W_177, U_178) | skf21(V_1191, X_1171, Y_1176, Z_1181, X1_1175, W_177, U_178)=skf10(U_1179, W_177, U_178) | skf21(V_1191, X_1171, Y_1176, Z_1181, X1_1175, W_177, U_178)=skf21(V_1182, X_1189, Y_1180, Z_1177, X1_1183, W_177, U_178) | skf21(V_1191, X_1171, Y_1176, Z_1181, X1_1175, W_177, U_178)=skf10(U_1173, W_177, U_178) | skf10(U_1179, W_177, U_178)=skf10(U_1173, W_177, U_178) | skf21(V_1182, X_1189, Y_1180, Z_1177, X1_1183, W_177, U_178)=skf10(U_1173, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1173, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1191, X_1171, Y_1176, Z_1181, X1_1175, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1179, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1182, X_1189, Y_1180, Z_1177, X1_1183, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1187, W_1184, X_1186, Y_1190, Z_1172, X1_1178)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1177=X1_1183 | Z_1177=Y_1180 | Y_1180=X1_1183 | Y_1180=X_1189 | Z_1177=X_1189 | X_1189=X1_1183 | X_1189=V_1182 | Y_1180=V_1182 | Z_1177=V_1182 | X1_1183=V_1182 | ~member(U_178, X1_1183, W_177) | ~member(U_178, Z_1177, W_177) | ~member(U_178, Y_1180, W_177) | ~member(U_178, X_1189, W_177) | ~member(U_178, V_1182, W_177) | ssSkP0(U_1179, W_177, U_178) | Z_1181=X1_1175 | Z_1181=Y_1176 | Y_1176=X1_1175 | Y_1176=X_1171 | Z_1181=X_1171 | X_1171=X1_1175 | X_1171=V_1191 | Y_1176=V_1191 | Z_1181=V_1191 | X1_1175=V_1191 | ~member(U_178, X1_1175, W_177) | ~member(U_178, Z_1181, W_177) | ~member(U_178, Y_1176, W_177) | ~member(U_178, X_1171, W_177) | ~member(U_178, V_1191, W_177) | ssSkP0(U_1173, 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)))). % 27.04/18.15 tff(c_1462, plain, (![Z_1356, Y_1365, V_1366, W_211, X1_1355, V_210, X_1364, V_1345, V_1362, U_1351, X1_1347, Z_1343, X_1361, Y_1344, Y_1348, Z_1349, Z_1353, X1_1360, Y_1352, W_1357, V_1354, X_1342, X1_1350, X_1363, U_209]: (skf21(V_1354, X_1364, Y_1352, Z_1349, X1_1355, V_210, W_211)=skf10(U_1351, V_210, W_211) | skf21(V_1366, X_1342, Y_1348, Z_1353, X1_1347, V_210, W_211)=skf10(U_1351, V_210, W_211) | skf21(V_1366, X_1342, Y_1348, Z_1353, X1_1347, V_210, W_211)=skf21(V_1354, X_1364, Y_1352, Z_1349, X1_1355, V_210, W_211) | skf21(V_1366, X_1342, Y_1348, Z_1353, X1_1347, V_210, W_211)=skf21(V_1345, X_1363, Y_1344, Z_1356, X1_1360, V_210, W_211) | skf21(V_1345, X_1363, Y_1344, Z_1356, X1_1360, V_210, W_211)=skf10(U_1351, V_210, W_211) | skf21(V_1354, X_1364, Y_1352, Z_1349, X1_1355, V_210, W_211)=skf21(V_1345, X_1363, Y_1344, Z_1356, X1_1360, V_210, W_211) | skf21(V_1345, X_1363, Y_1344, Z_1356, X1_1360, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1366, X_1342, Y_1348, Z_1353, X1_1347, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1351, V_210, W_211) | skf21(V_1354, X_1364, Y_1352, Z_1349, X1_1355, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1362, W_1357, X_1361, Y_1365, Z_1343, X1_1350)!=skf10(U_209, V_210, W_211) | Z_1349=X1_1355 | Z_1349=Y_1352 | Y_1352=X1_1355 | Y_1352=X_1364 | Z_1349=X_1364 | X_1364=X1_1355 | X_1364=V_1354 | Y_1352=V_1354 | Z_1349=V_1354 | X1_1355=V_1354 | ~member(W_211, X1_1355, V_210) | ~member(W_211, Z_1349, V_210) | ~member(W_211, Y_1352, V_210) | ~member(W_211, X_1364, V_210) | ~member(W_211, V_1354, V_210) | ssSkP0(U_1351, V_210, W_211) | Z_1353=X1_1347 | Z_1353=Y_1348 | Y_1348=X1_1347 | Y_1348=X_1342 | Z_1353=X_1342 | X_1342=X1_1347 | X_1342=V_1366 | Y_1348=V_1366 | Z_1353=V_1366 | X1_1347=V_1366 | ~member(W_211, X1_1347, V_210) | ~member(W_211, Z_1353, V_210) | ~member(W_211, Y_1348, V_210) | ~member(W_211, X_1342, V_210) | ~member(W_211, V_1366, V_210) | Z_1356=X1_1360 | Z_1356=Y_1344 | Y_1344=X1_1360 | Y_1344=X_1363 | Z_1356=X_1363 | X_1363=X1_1360 | X_1363=V_1345 | Y_1344=V_1345 | Z_1356=V_1345 | X1_1360=V_1345 | five(W_211, V_210) | ~member(W_211, X1_1360, V_210) | ~member(W_211, Z_1356, V_210) | ~member(W_211, Y_1344, V_210) | ~member(W_211, X_1363, V_210) | ~member(W_211, V_1345, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.15 tff(c_1366, plain, (![Z_1129, U_1132, X1_1126, U_1114, X1_1120, U_178, X_1122, Y_1125, X_181, V_1133, Z_179, Z_1119, Y_1117, Y_182, X1_1124, W_1127, Z_1123, X_1131, X1_180, W_177, V_183, Y_1115, V_1118, X_1121]: (skf21(V_1133, X_1131, Y_1115, Z_1123, X1_1126, W_177, U_178)=skf21(V_1118, X_1121, Y_1117, Z_1129, X1_1120, W_177, U_178) | skf21(V_1118, X_1121, Y_1117, Z_1129, X1_1120, W_177, U_178)=skf10(U_1114, W_177, U_178) | skf21(V_1133, X_1131, Y_1115, Z_1123, X1_1126, W_177, U_178)=skf10(U_1114, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1114, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1118, X_1121, Y_1117, Z_1129, X1_1120, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1133, X_1131, Y_1115, Z_1123, X1_1126, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1132 | skf10(U_1114, W_177, U_178)=U_1132 | skf21(V_1118, X_1121, Y_1117, Z_1129, X1_1120, W_177, U_178)=U_1132 | skf21(V_1133, X_1131, Y_1115, Z_1123, X1_1126, W_177, U_178)=U_1132 | ~member(U_178, U_1132, W_177) | skf21(U_1132, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_1127, X_1122, Y_1125, Z_1119, X1_1124)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1123=X1_1126 | Z_1123=Y_1115 | Y_1115=X1_1126 | Y_1115=X_1131 | Z_1123=X_1131 | X_1131=X1_1126 | X_1131=V_1133 | Y_1115=V_1133 | Z_1123=V_1133 | X1_1126=V_1133 | ~member(U_178, X1_1126, W_177) | ~member(U_178, Z_1123, W_177) | ~member(U_178, Y_1115, W_177) | ~member(U_178, X_1131, W_177) | ~member(U_178, V_1133, W_177) | Z_1129=X1_1120 | Z_1129=Y_1117 | Y_1117=X1_1120 | Y_1117=X_1121 | Z_1129=X_1121 | X_1121=X1_1120 | X_1121=V_1118 | Y_1117=V_1118 | Z_1129=V_1118 | X1_1120=V_1118 | ~member(U_178, X1_1120, W_177) | ~member(U_178, Z_1129, W_177) | ~member(U_178, Y_1117, W_177) | ~member(U_178, X_1121, W_177) | ~member(U_178, V_1118, W_177) | ssSkP0(U_1114, 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)))). % 27.04/18.15 tff(c_1440, plain, (![X1_1329, Z_1331, V_1341, W_211, U_1340, V_210, X1_1332, X_1336, V_1323, X1_1325, Y_1322, Z_1324, Z_1328, V_1319, X_1339, Y_1330, Y_1318, Y_1320, X_1326, X1_1334, W_1335, Z_1337, X_1327, U_209]: (skf21(V_1341, X_1339, Y_1320, Z_1328, X1_1332, V_210, W_211)=skf21(V_1323, X_1326, Y_1322, Z_1337, X1_1325, V_210, W_211) | skf21(V_1323, X_1326, Y_1322, Z_1337, X1_1325, V_210, W_211)=skf21(V_1319, X_1336, Y_1318, Z_1331, X1_1334, V_210, W_211) | skf21(V_1341, X_1339, Y_1320, Z_1328, X1_1332, V_210, W_211)=skf21(V_1319, X_1336, Y_1318, Z_1331, X1_1334, V_210, W_211) | skf21(V_1319, X_1336, Y_1318, Z_1331, X1_1334, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1323, X_1326, Y_1322, Z_1337, X1_1325, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1341, X_1339, Y_1320, Z_1328, X1_1332, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1340 | skf21(V_1319, X_1336, Y_1318, Z_1331, X1_1334, V_210, W_211)=U_1340 | skf21(V_1323, X_1326, Y_1322, Z_1337, X1_1325, V_210, W_211)=U_1340 | skf21(V_1341, X_1339, Y_1320, Z_1328, X1_1332, V_210, W_211)=U_1340 | ~member(W_211, U_1340, V_210) | skf21(U_1340, skf10(U_209, V_210, W_211), W_1335, X_1327, Y_1330, Z_1324, X1_1329)!=skf10(U_209, V_210, W_211) | Z_1328=X1_1332 | Z_1328=Y_1320 | Y_1320=X1_1332 | Y_1320=X_1339 | Z_1328=X_1339 | X_1339=X1_1332 | X_1339=V_1341 | Y_1320=V_1341 | Z_1328=V_1341 | X1_1332=V_1341 | ~member(W_211, X1_1332, V_210) | ~member(W_211, Z_1328, V_210) | ~member(W_211, Y_1320, V_210) | ~member(W_211, X_1339, V_210) | ~member(W_211, V_1341, V_210) | Z_1337=X1_1325 | Z_1337=Y_1322 | Y_1322=X1_1325 | Y_1322=X_1326 | Z_1337=X_1326 | X_1326=X1_1325 | X_1326=V_1323 | Y_1322=V_1323 | Z_1337=V_1323 | X1_1325=V_1323 | ~member(W_211, X1_1325, V_210) | ~member(W_211, Z_1337, V_210) | ~member(W_211, Y_1322, V_210) | ~member(W_211, X_1326, V_210) | ~member(W_211, V_1323, V_210) | Z_1331=X1_1334 | Z_1331=Y_1318 | Y_1318=X1_1334 | Y_1318=X_1336 | Z_1331=X_1336 | X_1336=X1_1334 | X_1336=V_1319 | Y_1318=V_1319 | Z_1331=V_1319 | X1_1334=V_1319 | five(W_211, V_210) | ~member(W_211, X1_1334, V_210) | ~member(W_211, Z_1331, V_210) | ~member(W_211, Y_1318, V_210) | ~member(W_211, X_1336, V_210) | ~member(W_211, V_1319, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1300, plain, (![Y_1053, X_1068, X1_1069, U_178, X_181, V_1063, Z_179, Z_1067, Y_182, Y_1071, Z_1059, X_1066, X1_1060, X1_180, Z_1062, W_177, V_183, U_1057, V_1054, V_1056, Y_1055, X1_1065, X_1070]: (skf21(V_1056, X_1066, Y_1055, Z_1067, X1_1069, W_177, U_178)=skf21(V_1054, X_1070, Y_1053, Z_1062, X1_1065, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1054, X_1070, Y_1053, Z_1062, X1_1065, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1056, X_1066, Y_1055, Z_1067, X1_1069, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_1063 | skf21(V_1054, X_1070, Y_1053, Z_1062, X1_1065, W_177, U_178)=V_1063 | skf21(V_1056, X_1066, Y_1055, Z_1067, X1_1069, W_177, U_178)=V_1063 | V_1063=U_1057 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1057 | skf21(V_1054, X_1070, Y_1053, Z_1062, X1_1065, W_177, U_178)=U_1057 | skf21(V_1056, X_1066, Y_1055, Z_1067, X1_1069, W_177, U_178)=U_1057 | ~member(U_178, V_1063, W_177) | ~member(U_178, U_1057, W_177) | skf21(U_1057, V_1063, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_1068, Y_1071, Z_1059, X1_1060)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1067=X1_1069 | Z_1067=Y_1055 | Y_1055=X1_1069 | Y_1055=X_1066 | Z_1067=X_1066 | X_1066=X1_1069 | X_1066=V_1056 | Y_1055=V_1056 | Z_1067=V_1056 | X1_1069=V_1056 | ~member(U_178, X1_1069, W_177) | ~member(U_178, Z_1067, W_177) | ~member(U_178, Y_1055, W_177) | ~member(U_178, X_1066, W_177) | ~member(U_178, V_1056, W_177) | Z_1062=X1_1065 | Z_1062=Y_1053 | Y_1053=X1_1065 | Y_1053=X_1070 | Z_1062=X_1070 | X_1070=X1_1065 | X_1070=V_1054 | Y_1053=V_1054 | Z_1062=V_1054 | X1_1065=V_1054 | ~member(U_178, X1_1065, W_177) | ~member(U_178, Z_1062, W_177) | ~member(U_178, Y_1053, W_177) | ~member(U_178, X_1070, W_177) | ~member(U_178, V_1054, 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)))). % 27.04/18.16 tff(c_1344, plain, (![V_1097, Z_1106, U_1098, Y_1102, U_178, Z_1094, Y_1096, X_181, Z_179, X1_1110, Z_1093, Y_182, V_1105, X1_1111, W_1112, X_1095, X1_180, W_177, V_183, V_1099, X_1113, X1_1109, Y_1107, U_1101, X_1103]: (skf21(V_1099, X_1095, Y_1107, Z_1094, X1_1110, W_177, U_178)=skf10(U_1101, W_177, U_178) | skf21(V_1097, X_1113, Y_1096, Z_1106, X1_1109, W_177, U_178)=skf10(U_1101, W_177, U_178) | skf21(V_1099, X_1095, Y_1107, Z_1094, X1_1110, W_177, U_178)=skf21(V_1097, X_1113, Y_1096, Z_1106, X1_1109, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1097, X_1113, Y_1096, Z_1106, X1_1109, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1101, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1099, X_1095, Y_1107, Z_1094, X1_1110, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1098 | skf21(V_1097, X_1113, Y_1096, Z_1106, X1_1109, W_177, U_178)=U_1098 | skf10(U_1101, W_177, U_178)=U_1098 | skf21(V_1099, X_1095, Y_1107, Z_1094, X1_1110, W_177, U_178)=U_1098 | ~member(U_178, U_1098, W_177) | skf21(U_1098, V_1105, W_1112, X_1103, Y_1102, Z_1093, X1_1111)!=U_1098 | Z_1094=X1_1110 | Z_1094=Y_1107 | Y_1107=X1_1110 | Y_1107=X_1095 | Z_1094=X_1095 | X_1095=X1_1110 | X_1095=V_1099 | Y_1107=V_1099 | Z_1094=V_1099 | X1_1110=V_1099 | ~member(U_178, X1_1110, W_177) | ~member(U_178, Z_1094, W_177) | ~member(U_178, Y_1107, W_177) | ~member(U_178, X_1095, W_177) | ~member(U_178, V_1099, W_177) | ssSkP0(U_1101, W_177, U_178) | Z_1106=X1_1109 | Z_1106=Y_1096 | Y_1096=X1_1109 | Y_1096=X_1113 | Z_1106=X_1113 | X_1113=X1_1109 | X_1113=V_1097 | Y_1096=V_1097 | Z_1106=V_1097 | X1_1109=V_1097 | ~member(U_178, X1_1109, W_177) | ~member(U_178, Z_1106, W_177) | ~member(U_178, Y_1096, W_177) | ~member(U_178, X_1113, W_177) | ~member(U_178, V_1097, 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)))). % 27.04/18.16 tff(c_1274, plain, (![W_971, Y_981, U_178, Z_977, V_967, X1_974, X_181, Z_179, X_984, X1_980, Y_182, Z_986, V_969, X_983, X_976, X1_180, Z_982, W_177, V_183, X1_985, U_978, Y_972, V_975, Y_968]: (skf21(V_969, X_983, Y_968, Z_977, X1_980, W_177, U_178)=skf21(V_967, X_984, Y_981, Z_986, X1_974, W_177, U_178) | skf21(V_969, X_983, Y_968, Z_977, X1_980, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_967, X_984, Y_981, Z_986, X1_974, 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_975 | skf21(V_969, X_983, Y_968, Z_977, X1_980, W_177, U_178)=V_975 | skf21(V_967, X_984, Y_981, Z_986, X1_974, W_177, U_178)=V_975 | V_975=U_978 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_978 | skf21(V_969, X_983, Y_968, Z_977, X1_980, W_177, U_178)=U_978 | skf21(V_967, X_984, Y_981, Z_986, X1_974, W_177, U_178)=U_978 | ~member(U_178, V_975, W_177) | ~member(U_178, U_978, W_177) | skf21(U_978, V_975, W_971, X_976, Y_972, Z_982, X1_985)!=V_975 | Z_986=X1_974 | Z_986=Y_981 | Y_981=X1_974 | Y_981=X_984 | Z_986=X_984 | X_984=X1_974 | X_984=V_967 | Y_981=V_967 | Z_986=V_967 | X1_974=V_967 | ~member(U_178, X1_974, W_177) | ~member(U_178, Z_986, W_177) | ~member(U_178, Y_981, W_177) | ~member(U_178, X_984, W_177) | ~member(U_178, V_967, W_177) | Z_977=X1_980 | Z_977=Y_968 | Y_968=X1_980 | Y_968=X_983 | Z_977=X_983 | X_983=X1_980 | X_983=V_969 | Y_968=V_969 | Z_977=V_969 | X1_980=V_969 | ~member(U_178, X1_980, W_177) | ~member(U_178, Z_977, W_177) | ~member(U_178, Y_968, W_177) | ~member(U_178, X_983, W_177) | ~member(U_178, V_969, 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)))). % 27.04/18.16 tff(c_1322, plain, (![X_1079, X1_1085, Z_1083, U_178, V_1075, X_181, Z_179, X4_1086, Z_1082, Y_182, X1_1072, V_1088, Y_1074, X1_180, W_177, W_1077, V_183, X_1087, V_1090, Z_1091, X_1081, U_1078, Y_1089, Y_1073, X1_1092]: (skf21(V_1088, X_1081, Y_1073, Z_1091, X1_1092, W_177, U_178)=skf21(V_1075, X_1087, Y_1074, Z_1082, X1_1085, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1075, X_1087, Y_1074, Z_1082, X1_1085, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1088, X_1081, Y_1073, Z_1091, X1_1092, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_1086 | skf21(V_1075, X_1087, Y_1074, Z_1082, X1_1085, W_177, U_178)=X4_1086 | skf21(V_1088, X_1081, Y_1073, Z_1091, X1_1092, W_177, U_178)=X4_1086 | X4_1086=U_1078 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1078 | skf21(V_1075, X_1087, Y_1074, Z_1082, X1_1085, W_177, U_178)=U_1078 | skf21(V_1088, X_1081, Y_1073, Z_1091, X1_1092, W_177, U_178)=U_1078 | ~member(U_178, X4_1086, W_177) | ~member(U_178, U_1078, W_177) | skf21(U_1078, V_1090, W_1077, X_1079, Y_1089, Z_1083, X1_1072)!=U_1078 | Z_1091=X1_1092 | Z_1091=Y_1073 | Y_1073=X1_1092 | Y_1073=X_1081 | Z_1091=X_1081 | X_1081=X1_1092 | X_1081=V_1088 | Y_1073=V_1088 | Z_1091=V_1088 | X1_1092=V_1088 | ~member(U_178, X1_1092, W_177) | ~member(U_178, Z_1091, W_177) | ~member(U_178, Y_1073, W_177) | ~member(U_178, X_1081, W_177) | ~member(U_178, V_1088, W_177) | Z_1082=X1_1085 | Z_1082=Y_1074 | Y_1074=X1_1085 | Y_1074=X_1087 | Z_1082=X_1087 | X_1087=X1_1085 | X_1087=V_1075 | Y_1074=V_1075 | Z_1082=V_1075 | X1_1085=V_1075 | ~member(U_178, X1_1085, W_177) | ~member(U_178, Z_1082, W_177) | ~member(U_178, Y_1074, W_177) | ~member(U_178, X_1087, W_177) | ~member(U_178, V_1075, 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)))). % 27.04/18.16 tff(c_1251, plain, (![X_948, U_941, U_178, V_951, U_935, X_181, Z_179, Y_182, Z_938, Y_944, U_937, X1_946, Z_945, X1_180, W_936, W_177, X_943, V_183, Y_950, X1_947, V_942]: (skf21(V_942, X_948, Y_944, Z_945, X1_946, W_177, U_178)=skf10(U_941, W_177, U_178) | skf10(U_941, W_177, U_178)=skf10(U_935, W_177, U_178) | skf21(V_942, X_948, Y_944, Z_945, X1_946, W_177, U_178)=skf10(U_935, W_177, U_178) | skf10(U_937, W_177, U_178)=skf10(U_935, W_177, U_178) | skf10(U_941, W_177, U_178)=skf10(U_937, W_177, U_178) | skf21(V_942, X_948, Y_944, Z_945, X1_946, W_177, U_178)=skf10(U_937, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_937, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_935, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_941, W_177, U_178) | skf21(V_942, X_948, Y_944, Z_945, X1_946, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_951, W_936, X_943, Y_950, Z_938, X1_947)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_945=X1_946 | Z_945=Y_944 | Y_944=X1_946 | Y_944=X_948 | Z_945=X_948 | X_948=X1_946 | X_948=V_942 | Y_944=V_942 | Z_945=V_942 | X1_946=V_942 | ~member(U_178, X1_946, W_177) | ~member(U_178, Z_945, W_177) | ~member(U_178, Y_944, W_177) | ~member(U_178, X_948, W_177) | ~member(U_178, V_942, W_177) | ssSkP0(U_941, W_177, U_178) | ssSkP0(U_935, W_177, U_178) | ssSkP0(U_937, 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)))). % 27.04/18.16 tff(c_1391, plain, (![W_1184, X1_1178, Y_1180, U_1179, W_211, V_1191, V_210, V_1187, X_1171, Y_1176, Z_1172, X_1186, X1_1183, X1_1175, V_1182, X_1189, U_1173, Z_1181, Z_1177, U_209, Y_1190]: (skf21(V_1182, X_1189, Y_1180, Z_1177, X1_1183, V_210, W_211)=skf10(U_1179, V_210, W_211) | skf21(V_1191, X_1171, Y_1176, Z_1181, X1_1175, V_210, W_211)=skf10(U_1179, V_210, W_211) | skf21(V_1191, X_1171, Y_1176, Z_1181, X1_1175, V_210, W_211)=skf21(V_1182, X_1189, Y_1180, Z_1177, X1_1183, V_210, W_211) | skf21(V_1191, X_1171, Y_1176, Z_1181, X1_1175, V_210, W_211)=skf10(U_1173, V_210, W_211) | skf10(U_1179, V_210, W_211)=skf10(U_1173, V_210, W_211) | skf21(V_1182, X_1189, Y_1180, Z_1177, X1_1183, V_210, W_211)=skf10(U_1173, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1173, V_210, W_211) | skf21(V_1191, X_1171, Y_1176, Z_1181, X1_1175, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1179, V_210, W_211) | skf21(V_1182, X_1189, Y_1180, Z_1177, X1_1183, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1187, W_1184, X_1186, Y_1190, Z_1172, X1_1178)!=skf10(U_209, V_210, W_211) | Z_1177=X1_1183 | Z_1177=Y_1180 | Y_1180=X1_1183 | Y_1180=X_1189 | Z_1177=X_1189 | X_1189=X1_1183 | X_1189=V_1182 | Y_1180=V_1182 | Z_1177=V_1182 | X1_1183=V_1182 | ~member(W_211, X1_1183, V_210) | ~member(W_211, Z_1177, V_210) | ~member(W_211, Y_1180, V_210) | ~member(W_211, X_1189, V_210) | ~member(W_211, V_1182, V_210) | ssSkP0(U_1179, V_210, W_211) | Z_1181=X1_1175 | Z_1181=Y_1176 | Y_1176=X1_1175 | Y_1176=X_1171 | Z_1181=X_1171 | X_1171=X1_1175 | X_1171=V_1191 | Y_1176=V_1191 | Z_1181=V_1191 | X1_1175=V_1191 | five(W_211, V_210) | ~member(W_211, X1_1175, V_210) | ~member(W_211, Z_1181, V_210) | ~member(W_211, Y_1176, V_210) | ~member(W_211, X_1171, V_210) | ~member(W_211, V_1191, V_210) | ssSkP0(U_1173, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1205, plain, (![U_873, U_178, Y_875, X_181, Z_179, X_878, Y_880, V_886, Y_182, Z_882, X1_180, W_177, Z_883, V_183, U_887, X1_884, X1_876, X_881, U_874, W_888]: (skf21(V_886, X_881, Y_875, Z_883, X1_884, W_177, U_178)=skf10(U_887, W_177, U_178) | skf21(V_886, X_881, Y_875, Z_883, X1_884, W_177, U_178)=skf10(U_874, W_177, U_178) | skf10(U_887, W_177, U_178)=skf10(U_874, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_874, W_177, U_178) | skf21(V_886, X_881, Y_875, Z_883, X1_884, 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_887, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_873 | skf10(U_874, W_177, U_178)=U_873 | skf21(V_886, X_881, Y_875, Z_883, X1_884, W_177, U_178)=U_873 | skf10(U_887, W_177, U_178)=U_873 | ~member(U_178, U_873, W_177) | skf21(U_873, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_888, X_878, Y_880, Z_882, X1_876)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_887, W_177, U_178) | Z_883=X1_884 | Z_883=Y_875 | Y_875=X1_884 | Y_875=X_881 | Z_883=X_881 | X_881=X1_884 | X_881=V_886 | Y_875=V_886 | Z_883=V_886 | X1_884=V_886 | ~member(U_178, X1_884, W_177) | ~member(U_178, Z_883, W_177) | ~member(U_178, Y_875, W_177) | ~member(U_178, X_881, W_177) | ~member(U_178, V_886, W_177) | ssSkP0(U_874, 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)))). % 27.04/18.16 tff(c_1367, plain, (![Z_1129, U_1132, X1_1126, U_1114, W_211, X1_1120, V_210, X_1122, Y_1125, V_1133, Z_1119, Y_1117, X1_1124, W_1127, Z_1123, X_1131, Y_1115, U_209, V_1118, X_1121]: (skf21(V_1133, X_1131, Y_1115, Z_1123, X1_1126, V_210, W_211)=skf21(V_1118, X_1121, Y_1117, Z_1129, X1_1120, V_210, W_211) | skf21(V_1118, X_1121, Y_1117, Z_1129, X1_1120, V_210, W_211)=skf10(U_1114, V_210, W_211) | skf21(V_1133, X_1131, Y_1115, Z_1123, X1_1126, V_210, W_211)=skf10(U_1114, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1114, V_210, W_211) | skf21(V_1118, X_1121, Y_1117, Z_1129, X1_1120, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1133, X_1131, Y_1115, Z_1123, X1_1126, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1132 | skf10(U_1114, V_210, W_211)=U_1132 | skf21(V_1118, X_1121, Y_1117, Z_1129, X1_1120, V_210, W_211)=U_1132 | skf21(V_1133, X_1131, Y_1115, Z_1123, X1_1126, V_210, W_211)=U_1132 | ~member(W_211, U_1132, V_210) | skf21(U_1132, skf10(U_209, V_210, W_211), W_1127, X_1122, Y_1125, Z_1119, X1_1124)!=skf10(U_209, V_210, W_211) | Z_1123=X1_1126 | Z_1123=Y_1115 | Y_1115=X1_1126 | Y_1115=X_1131 | Z_1123=X_1131 | X_1131=X1_1126 | X_1131=V_1133 | Y_1115=V_1133 | Z_1123=V_1133 | X1_1126=V_1133 | ~member(W_211, X1_1126, V_210) | ~member(W_211, Z_1123, V_210) | ~member(W_211, Y_1115, V_210) | ~member(W_211, X_1131, V_210) | ~member(W_211, V_1133, V_210) | Z_1129=X1_1120 | Z_1129=Y_1117 | Y_1117=X1_1120 | Y_1117=X_1121 | Z_1129=X_1121 | X_1121=X1_1120 | X_1121=V_1118 | Y_1117=V_1118 | Z_1129=V_1118 | X1_1120=V_1118 | five(W_211, V_210) | ~member(W_211, X1_1120, V_210) | ~member(W_211, Z_1129, V_210) | ~member(W_211, Y_1117, V_210) | ~member(W_211, X_1121, V_210) | ~member(W_211, V_1118, V_210) | ssSkP0(U_1114, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1181, plain, (![Y_838, X_844, U_178, X_181, Z_179, X_833, U_832, U_843, Y_182, Z_839, Z_837, X1_845, V_834, V_842, X1_180, W_177, V_183, Y_831, X1_841]: (skf21(V_834, X_844, Y_831, Z_839, X1_841, W_177, U_178)=skf10(U_832, W_177, U_178) | skf21(V_834, X_844, Y_831, Z_839, X1_841, 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_832, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_842 | skf21(V_834, X_844, Y_831, Z_839, X1_841, W_177, U_178)=V_842 | skf10(U_832, W_177, U_178)=V_842 | V_842=U_843 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_843 | skf21(V_834, X_844, Y_831, Z_839, X1_841, W_177, U_178)=U_843 | skf10(U_832, W_177, U_178)=U_843 | ~member(U_178, V_842, W_177) | ~member(U_178, U_843, W_177) | skf21(U_843, V_842, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_833, Y_838, Z_837, X1_845)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_832, W_177, U_178) | Z_839=X1_841 | Z_839=Y_831 | Y_831=X1_841 | Y_831=X_844 | Z_839=X_844 | X_844=X1_841 | X_844=V_834 | Y_831=V_834 | Z_839=V_834 | X1_841=V_834 | ~member(U_178, X1_841, W_177) | ~member(U_178, Z_839, W_177) | ~member(U_178, Y_831, W_177) | ~member(U_178, X_844, W_177) | ~member(U_178, V_834, 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)))). % 27.04/18.16 tff(c_1345, plain, (![V_1097, Z_1106, U_1098, Y_1102, W_211, V_210, Z_1094, Y_1096, X1_1110, Z_1093, V_1105, X1_1111, W_1112, X_1095, V_1099, X_1113, X1_1109, U_209, Y_1107, U_1101, X_1103]: (skf21(V_1099, X_1095, Y_1107, Z_1094, X1_1110, V_210, W_211)=skf10(U_1101, V_210, W_211) | skf21(V_1097, X_1113, Y_1096, Z_1106, X1_1109, V_210, W_211)=skf10(U_1101, V_210, W_211) | skf21(V_1099, X_1095, Y_1107, Z_1094, X1_1110, V_210, W_211)=skf21(V_1097, X_1113, Y_1096, Z_1106, X1_1109, V_210, W_211) | skf21(V_1097, X_1113, Y_1096, Z_1106, X1_1109, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1101, V_210, W_211) | skf21(V_1099, X_1095, Y_1107, Z_1094, X1_1110, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1098 | skf21(V_1097, X_1113, Y_1096, Z_1106, X1_1109, V_210, W_211)=U_1098 | skf10(U_1101, V_210, W_211)=U_1098 | skf21(V_1099, X_1095, Y_1107, Z_1094, X1_1110, V_210, W_211)=U_1098 | ~member(W_211, U_1098, V_210) | skf21(U_1098, V_1105, W_1112, X_1103, Y_1102, Z_1093, X1_1111)!=U_1098 | Z_1094=X1_1110 | Z_1094=Y_1107 | Y_1107=X1_1110 | Y_1107=X_1095 | Z_1094=X_1095 | X_1095=X1_1110 | X_1095=V_1099 | Y_1107=V_1099 | Z_1094=V_1099 | X1_1110=V_1099 | ~member(W_211, X1_1110, V_210) | ~member(W_211, Z_1094, V_210) | ~member(W_211, Y_1107, V_210) | ~member(W_211, X_1095, V_210) | ~member(W_211, V_1099, V_210) | ssSkP0(U_1101, V_210, W_211) | Z_1106=X1_1109 | Z_1106=Y_1096 | Y_1096=X1_1109 | Y_1096=X_1113 | Z_1106=X_1113 | X_1113=X1_1109 | X_1113=V_1097 | Y_1096=V_1097 | Z_1106=V_1097 | X1_1109=V_1097 | five(W_211, V_210) | ~member(W_211, X1_1109, V_210) | ~member(W_211, Z_1106, V_210) | ~member(W_211, Y_1096, V_210) | ~member(W_211, X_1113, V_210) | ~member(W_211, V_1097, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1301, plain, (![Y_1053, X_1068, X1_1069, W_211, V_210, V_1063, Z_1067, Y_1071, Z_1059, X_1066, X1_1060, Z_1062, U_1057, V_1054, V_1056, Y_1055, U_209, X1_1065, X_1070]: (skf21(V_1056, X_1066, Y_1055, Z_1067, X1_1069, V_210, W_211)=skf21(V_1054, X_1070, Y_1053, Z_1062, X1_1065, V_210, W_211) | skf21(V_1054, X_1070, Y_1053, Z_1062, X1_1065, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1056, X_1066, Y_1055, Z_1067, X1_1069, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_1063 | skf21(V_1054, X_1070, Y_1053, Z_1062, X1_1065, V_210, W_211)=V_1063 | skf21(V_1056, X_1066, Y_1055, Z_1067, X1_1069, V_210, W_211)=V_1063 | V_1063=U_1057 | skf10(U_209, V_210, W_211)=U_1057 | skf21(V_1054, X_1070, Y_1053, Z_1062, X1_1065, V_210, W_211)=U_1057 | skf21(V_1056, X_1066, Y_1055, Z_1067, X1_1069, V_210, W_211)=U_1057 | ~member(W_211, V_1063, V_210) | ~member(W_211, U_1057, V_210) | skf21(U_1057, V_1063, skf10(U_209, V_210, W_211), X_1068, Y_1071, Z_1059, X1_1060)!=skf10(U_209, V_210, W_211) | Z_1067=X1_1069 | Z_1067=Y_1055 | Y_1055=X1_1069 | Y_1055=X_1066 | Z_1067=X_1066 | X_1066=X1_1069 | X_1066=V_1056 | Y_1055=V_1056 | Z_1067=V_1056 | X1_1069=V_1056 | ~member(W_211, X1_1069, V_210) | ~member(W_211, Z_1067, V_210) | ~member(W_211, Y_1055, V_210) | ~member(W_211, X_1066, V_210) | ~member(W_211, V_1056, V_210) | Z_1062=X1_1065 | Z_1062=Y_1053 | Y_1053=X1_1065 | Y_1053=X_1070 | Z_1062=X_1070 | X_1070=X1_1065 | X_1070=V_1054 | Y_1053=V_1054 | Z_1062=V_1054 | X1_1065=V_1054 | five(W_211, V_210) | ~member(W_211, X1_1065, V_210) | ~member(W_211, Z_1062, V_210) | ~member(W_211, Y_1053, V_210) | ~member(W_211, X_1070, V_210) | ~member(W_211, V_1054, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1114, plain, (![W_771, V_780, U_178, X_181, Z_179, Y_775, Y_182, Y_772, U_776, Z_777, Z_784, X1_180, W_177, X_779, V_183, V_781, X1_774, X1_783]: (skf21(V_780, X_779, Y_772, Z_777, X1_774, 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_771 | skf21(V_780, X_779, Y_772, Z_777, X1_774, W_177, U_178)=W_771 | W_771=V_781 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_781 | skf21(V_780, X_779, Y_772, Z_777, X1_774, W_177, U_178)=V_781 | V_781=U_776 | W_771=U_776 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_776 | skf21(V_780, X_779, Y_772, Z_777, X1_774, W_177, U_178)=U_776 | ~member(U_178, W_771, W_177) | ~member(U_178, V_781, W_177) | ~member(U_178, U_776, W_177) | skf21(U_776, V_781, W_771, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), Y_775, Z_784, X1_783)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_777=X1_774 | Z_777=Y_772 | Y_772=X1_774 | Y_772=X_779 | Z_777=X_779 | X_779=X1_774 | X_779=V_780 | Y_772=V_780 | Z_777=V_780 | X1_774=V_780 | ~member(U_178, X1_774, W_177) | ~member(U_178, Z_777, W_177) | ~member(U_178, Y_772, W_177) | ~member(U_178, X_779, W_177) | ~member(U_178, V_780, 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)))). % 27.04/18.16 tff(c_1275, plain, (![W_971, Y_981, W_211, V_210, Z_977, V_967, X1_974, X_984, X1_980, Z_986, V_969, X_983, X_976, Z_982, X1_985, U_209, U_978, Y_972, V_975, Y_968]: (skf21(V_969, X_983, Y_968, Z_977, X1_980, V_210, W_211)=skf21(V_967, X_984, Y_981, Z_986, X1_974, V_210, W_211) | skf21(V_969, X_983, Y_968, Z_977, X1_980, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_967, X_984, Y_981, Z_986, X1_974, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_975 | skf21(V_969, X_983, Y_968, Z_977, X1_980, V_210, W_211)=V_975 | skf21(V_967, X_984, Y_981, Z_986, X1_974, V_210, W_211)=V_975 | V_975=U_978 | skf10(U_209, V_210, W_211)=U_978 | skf21(V_969, X_983, Y_968, Z_977, X1_980, V_210, W_211)=U_978 | skf21(V_967, X_984, Y_981, Z_986, X1_974, V_210, W_211)=U_978 | ~member(W_211, V_975, V_210) | ~member(W_211, U_978, V_210) | skf21(U_978, V_975, W_971, X_976, Y_972, Z_982, X1_985)!=V_975 | Z_986=X1_974 | Z_986=Y_981 | Y_981=X1_974 | Y_981=X_984 | Z_986=X_984 | X_984=X1_974 | X_984=V_967 | Y_981=V_967 | Z_986=V_967 | X1_974=V_967 | ~member(W_211, X1_974, V_210) | ~member(W_211, Z_986, V_210) | ~member(W_211, Y_981, V_210) | ~member(W_211, X_984, V_210) | ~member(W_211, V_967, V_210) | Z_977=X1_980 | Z_977=Y_968 | Y_968=X1_980 | Y_968=X_983 | Z_977=X_983 | X_983=X1_980 | X_983=V_969 | Y_968=V_969 | Z_977=V_969 | X1_980=V_969 | five(W_211, V_210) | ~member(W_211, X1_980, V_210) | ~member(W_211, Z_977, V_210) | ~member(W_211, Y_968, V_210) | ~member(W_211, X_983, V_210) | ~member(W_211, V_969, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1137, plain, (![V_810, X4_808, X1_814, Z_813, U_178, Y_799, X_181, Z_179, X1_798, Y_182, U_803, W_802, X_806, Z_807, U_800, Y_811, X1_180, W_177, X_804, V_183, V_812]: (skf21(V_810, X_806, Y_799, Z_813, X1_814, W_177, U_178)=skf10(U_800, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_800, W_177, U_178) | skf21(V_810, X_806, Y_799, Z_813, X1_814, 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_808 | skf10(U_800, W_177, U_178)=X4_808 | skf21(V_810, X_806, Y_799, Z_813, X1_814, W_177, U_178)=X4_808 | X4_808=U_803 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_803 | skf10(U_800, W_177, U_178)=U_803 | skf21(V_810, X_806, Y_799, Z_813, X1_814, W_177, U_178)=U_803 | ~member(U_178, X4_808, W_177) | ~member(U_178, U_803, W_177) | skf21(U_803, V_812, W_802, X_804, Y_811, Z_807, X1_798)!=U_803 | Z_813=X1_814 | Z_813=Y_799 | Y_799=X1_814 | Y_799=X_806 | Z_813=X_806 | X_806=X1_814 | X_806=V_810 | Y_799=V_810 | Z_813=V_810 | X1_814=V_810 | ~member(U_178, X1_814, W_177) | ~member(U_178, Z_813, W_177) | ~member(U_178, Y_799, W_177) | ~member(U_178, X_806, W_177) | ~member(U_178, V_810, W_177) | ssSkP0(U_800, 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)))). % 27.04/18.16 tff(c_1092, plain, (![W_770, U_178, X_181, Z_179, V_767, X5_760, X1_755, Z_759, V_764, X_769, Y_182, Z_763, X1_758, Y_757, X4_762, U_754, X_766, X1_180, W_177, V_183, Y_756]: (skf21(V_767, X_766, Y_756, Z_763, X1_758, 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_760 | skf21(V_767, X_766, Y_756, Z_763, X1_758, W_177, U_178)=X5_760 | X5_760=X4_762 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_762 | skf21(V_767, X_766, Y_756, Z_763, X1_758, W_177, U_178)=X4_762 | X4_762=U_754 | X5_760=U_754 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_754 | skf21(V_767, X_766, Y_756, Z_763, X1_758, W_177, U_178)=U_754 | ~member(U_178, X5_760, W_177) | ~member(U_178, X4_762, W_177) | ~member(U_178, U_754, W_177) | skf21(U_754, V_764, W_770, X_769, Y_757, Z_759, X1_755)!=U_754 | Z_763=X1_758 | Z_763=Y_756 | Y_756=X1_758 | Y_756=X_766 | Z_763=X_766 | X_766=X1_758 | X_766=V_767 | Y_756=V_767 | Z_763=V_767 | X1_758=V_767 | ~member(U_178, X1_758, W_177) | ~member(U_178, Z_763, W_177) | ~member(U_178, Y_756, W_177) | ~member(U_178, X_766, W_177) | ~member(U_178, V_767, 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)))). % 27.04/18.16 tff(c_935, plain, (![V_641, X_630, U_178, Y_633, X_181, Z_179, X_640, U_637, Y_182, X1_635, X1_643, V_629, X1_180, Z_634, W_177, V_183, W_631, Z_638, Y_632]: (skf21(V_641, X_640, Y_632, Z_638, X1_635, 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_631 | skf21(V_641, X_640, Y_632, Z_638, X1_635, W_177, U_178)=W_631 | W_631=V_629 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_629 | skf21(V_641, X_640, Y_632, Z_638, X1_635, W_177, U_178)=V_629 | V_629=U_637 | W_631=U_637 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_637 | skf21(V_641, X_640, Y_632, Z_638, X1_635, W_177, U_178)=U_637 | ~member(U_178, W_631, W_177) | ~member(U_178, V_629, W_177) | ~member(U_178, U_637, W_177) | skf21(U_637, V_629, W_631, X_630, Y_633, Z_634, X1_643)!=W_631 | Z_638=X1_635 | Z_638=Y_632 | Y_632=X1_635 | Y_632=X_640 | Z_638=X_640 | X_640=X1_635 | X_640=V_641 | Y_632=V_641 | Z_638=V_641 | X1_635=V_641 | ~member(U_178, X1_635, W_177) | ~member(U_178, Z_638, W_177) | ~member(U_178, Y_632, W_177) | ~member(U_178, X_640, W_177) | ~member(U_178, V_641, 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)))). % 27.04/18.16 tff(c_1047, plain, (![X_718, U_178, X_181, Z_179, U_713, Y_723, Y_182, U_720, Z_725, U_714, X1_180, W_177, V_183, V_721, X1_719, W_716, U_722]: (skf10(U_720, W_177, U_178)=skf10(U_713, W_177, U_178) | skf10(U_722, W_177, U_178)=skf10(U_720, W_177, U_178) | skf10(U_722, W_177, U_178)=skf10(U_713, W_177, U_178) | skf10(U_722, W_177, U_178)=skf10(U_714, W_177, U_178) | skf10(U_720, W_177, U_178)=skf10(U_714, W_177, U_178) | skf10(U_714, W_177, U_178)=skf10(U_713, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_714, 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_720, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_713, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_721, W_716, X_718, Y_723, Z_725, X1_719)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_713, W_177, U_178) | ssSkP0(U_720, W_177, U_178) | ssSkP0(U_722, W_177, U_178) | ssSkP0(U_714, 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)))). % 27.04/18.16 tff(c_1252, plain, (![X_948, W_211, V_210, U_941, V_951, U_935, Z_938, Y_944, U_937, X1_946, Z_945, W_936, X_943, Y_950, X1_947, U_209, V_942]: (skf21(V_942, X_948, Y_944, Z_945, X1_946, V_210, W_211)=skf10(U_941, V_210, W_211) | skf10(U_941, V_210, W_211)=skf10(U_935, V_210, W_211) | skf21(V_942, X_948, Y_944, Z_945, X1_946, V_210, W_211)=skf10(U_935, V_210, W_211) | skf10(U_937, V_210, W_211)=skf10(U_935, V_210, W_211) | skf10(U_941, V_210, W_211)=skf10(U_937, V_210, W_211) | skf21(V_942, X_948, Y_944, Z_945, X1_946, V_210, W_211)=skf10(U_937, V_210, W_211) | skf10(U_937, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_935, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_941, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_942, X_948, Y_944, Z_945, X1_946, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_951, W_936, X_943, Y_950, Z_938, X1_947)!=skf10(U_209, V_210, W_211) | Z_945=X1_946 | Z_945=Y_944 | Y_944=X1_946 | Y_944=X_948 | Z_945=X_948 | X_948=X1_946 | X_948=V_942 | Y_944=V_942 | Z_945=V_942 | X1_946=V_942 | five(W_211, V_210) | ~member(W_211, X1_946, V_210) | ~member(W_211, Z_945, V_210) | ~member(W_211, Y_944, V_210) | ~member(W_211, X_948, V_210) | ~member(W_211, V_942, V_210) | ssSkP0(U_941, V_210, W_211) | ssSkP0(U_935, V_210, W_211) | ssSkP0(U_937, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1024, plain, (![U_692, U_178, U_701, X_181, Z_179, Y_696, X_691, Y_182, U_690, W_693, X1_180, W_177, Z_700, V_183, X1_699, U_695]: (skf10(U_701, W_177, U_178)=skf10(U_695, W_177, U_178) | skf10(U_695, W_177, U_178)=skf10(U_692, W_177, U_178) | skf10(U_701, W_177, U_178)=skf10(U_692, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_692, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_695, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_701, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_690 | skf10(U_692, W_177, U_178)=U_690 | skf10(U_695, W_177, U_178)=U_690 | skf10(U_701, W_177, U_178)=U_690 | ~member(U_178, U_690, W_177) | skf21(U_690, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_693, X_691, Y_696, Z_700, X1_699)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_701, W_177, U_178) | ssSkP0(U_695, W_177, U_178) | ssSkP0(U_692, 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)))). % 27.04/18.16 tff(c_1206, plain, (![U_873, W_211, V_210, Y_875, X_878, Y_880, V_886, Z_882, Z_883, U_887, X1_884, X1_876, U_209, X_881, U_874, W_888]: (skf21(V_886, X_881, Y_875, Z_883, X1_884, V_210, W_211)=skf10(U_887, V_210, W_211) | skf21(V_886, X_881, Y_875, Z_883, X1_884, V_210, W_211)=skf10(U_874, V_210, W_211) | skf10(U_887, V_210, W_211)=skf10(U_874, V_210, W_211) | skf10(U_874, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_886, X_881, Y_875, Z_883, X1_884, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_887, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_873 | skf10(U_874, V_210, W_211)=U_873 | skf21(V_886, X_881, Y_875, Z_883, X1_884, V_210, W_211)=U_873 | skf10(U_887, V_210, W_211)=U_873 | ~member(W_211, U_873, V_210) | skf21(U_873, skf10(U_209, V_210, W_211), W_888, X_878, Y_880, Z_882, X1_876)!=skf10(U_209, V_210, W_211) | ssSkP0(U_887, V_210, W_211) | Z_883=X1_884 | Z_883=Y_875 | Y_875=X1_884 | Y_875=X_881 | Z_883=X_881 | X_881=X1_884 | X_881=V_886 | Y_875=V_886 | Z_883=V_886 | X1_884=V_886 | five(W_211, V_210) | ~member(W_211, X1_884, V_210) | ~member(W_211, Z_883, V_210) | ~member(W_211, Y_875, V_210) | ~member(W_211, X_881, V_210) | ~member(W_211, V_886, V_210) | ssSkP0(U_874, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1070, plain, (![V_747, X1_742, U_178, X_181, Z_179, W_745, X1_743, Y_182, X_749, X_744, X1_180, X4_741, W_177, V_183, V_750, Y_752, Y_740, Z_738, U_753, Z_746]: (skf21(V_750, X_749, Y_740, Z_746, X1_742, 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_741 | skf21(V_750, X_749, Y_740, Z_746, X1_742, W_177, U_178)=X4_741 | X4_741=V_747 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_747 | skf21(V_750, X_749, Y_740, Z_746, X1_742, W_177, U_178)=V_747 | V_747=U_753 | X4_741=U_753 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_753 | skf21(V_750, X_749, Y_740, Z_746, X1_742, W_177, U_178)=U_753 | ~member(U_178, X4_741, W_177) | ~member(U_178, V_747, W_177) | ~member(U_178, U_753, W_177) | skf21(U_753, V_747, W_745, X_744, Y_752, Z_738, X1_743)!=V_747 | Z_746=X1_742 | Z_746=Y_740 | Y_740=X1_742 | Y_740=X_749 | Z_746=X_749 | X_749=X1_742 | X_749=V_750 | Y_740=V_750 | Z_746=V_750 | X1_742=V_750 | ~member(U_178, X1_742, W_177) | ~member(U_178, Z_746, W_177) | ~member(U_178, Y_740, W_177) | ~member(U_178, X_749, W_177) | ~member(U_178, V_750, 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)))). % 27.04/18.16 tff(c_957, plain, (![U_178, X_645, X_181, Z_179, U_644, V_651, Y_182, U_646, X1_654, X1_180, W_177, Y_650, V_183, U_652, Z_649]: (skf10(U_646, W_177, U_178)=skf10(U_644, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_646, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_644, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_651 | skf10(U_646, W_177, U_178)=V_651 | skf10(U_644, W_177, U_178)=V_651 | V_651=U_652 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_652 | skf10(U_646, W_177, U_178)=U_652 | skf10(U_644, W_177, U_178)=U_652 | ~member(U_178, V_651, W_177) | ~member(U_178, U_652, W_177) | skf21(U_652, V_651, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_645, Y_650, Z_649, X1_654)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_644, W_177, U_178) | ssSkP0(U_646, 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)))). % 27.04/18.16 tff(c_1228, plain, (![V_894, X_891, W_211, X_898, V_210, V_900, Y_901, W_905, X1_902, U_892, Z_889, Z_890, X1_903, Y_897, U_896, U_209, U_893]: (skf21(V_894, X_891, Y_901, Z_890, X1_902, V_210, W_211)=skf10(U_896, V_210, W_211) | skf10(U_896, V_210, W_211)=skf10(U_892, V_210, W_211) | skf21(V_894, X_891, Y_901, Z_890, X1_902, V_210, W_211)=skf10(U_892, V_210, W_211) | skf10(U_892, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_896, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_894, X_891, Y_901, Z_890, X1_902, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_893 | skf10(U_892, V_210, W_211)=U_893 | skf10(U_896, V_210, W_211)=U_893 | skf21(V_894, X_891, Y_901, Z_890, X1_902, V_210, W_211)=U_893 | ~member(W_211, U_893, V_210) | skf21(U_893, V_900, W_905, X_898, Y_897, Z_889, X1_903)!=U_893 | Z_890=X1_902 | Z_890=Y_901 | Y_901=X1_902 | Y_901=X_891 | Z_890=X_891 | X_891=X1_902 | X_891=V_894 | Y_901=V_894 | Z_890=V_894 | X1_902=V_894 | five(W_211, V_210) | ~member(W_211, X1_902, V_210) | ~member(W_211, Z_890, V_210) | ~member(W_211, Y_901, V_210) | ~member(W_211, X_891, V_210) | ~member(W_211, V_894, V_210) | ssSkP0(U_896, V_210, W_211) | ssSkP0(U_892, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1182, plain, (![Y_838, W_211, V_210, X_844, X_833, U_832, U_843, Z_839, Z_837, X1_845, V_834, V_842, Y_831, U_209, X1_841]: (skf21(V_834, X_844, Y_831, Z_839, X1_841, V_210, W_211)=skf10(U_832, V_210, W_211) | skf21(V_834, X_844, Y_831, Z_839, X1_841, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_832, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_842 | skf21(V_834, X_844, Y_831, Z_839, X1_841, V_210, W_211)=V_842 | skf10(U_832, V_210, W_211)=V_842 | V_842=U_843 | skf10(U_209, V_210, W_211)=U_843 | skf21(V_834, X_844, Y_831, Z_839, X1_841, V_210, W_211)=U_843 | skf10(U_832, V_210, W_211)=U_843 | ~member(W_211, V_842, V_210) | ~member(W_211, U_843, V_210) | skf21(U_843, V_842, skf10(U_209, V_210, W_211), X_833, Y_838, Z_837, X1_845)!=skf10(U_209, V_210, W_211) | ssSkP0(U_832, V_210, W_211) | Z_839=X1_841 | Z_839=Y_831 | Y_831=X1_841 | Y_831=X_844 | Z_839=X_844 | X_844=X1_841 | X_844=V_834 | Y_831=V_834 | Z_839=V_834 | X1_841=V_834 | five(W_211, V_210) | ~member(W_211, X1_841, V_210) | ~member(W_211, Z_839, V_210) | ~member(W_211, Y_831, V_210) | ~member(W_211, X_844, V_210) | ~member(W_211, V_834, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_868, plain, (![U_178, W_591, X_181, Z_179, U_586, Y_593, U_585, Y_182, X1_180, W_177, V_183, Z_589, V_590, X1_592]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_585, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_591 | skf10(U_585, W_177, U_178)=W_591 | W_591=V_590 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_590 | skf10(U_585, W_177, U_178)=V_590 | V_590=U_586 | W_591=U_586 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_586 | skf10(U_585, W_177, U_178)=U_586 | ~member(U_178, W_591, W_177) | ~member(U_178, V_590, W_177) | ~member(U_178, U_586, W_177) | skf21(U_586, V_590, W_591, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), Y_593, Z_589, X1_592)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_585, 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)))). % 27.04/18.16 tff(c_1138, plain, (![V_810, X4_808, X1_814, W_211, Z_813, V_210, Y_799, X1_798, U_803, W_802, X_806, Z_807, U_800, Y_811, X_804, U_209, V_812]: (skf21(V_810, X_806, Y_799, Z_813, X1_814, V_210, W_211)=skf10(U_800, V_210, W_211) | skf10(U_800, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_810, X_806, Y_799, Z_813, X1_814, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_808 | skf10(U_800, V_210, W_211)=X4_808 | skf21(V_810, X_806, Y_799, Z_813, X1_814, V_210, W_211)=X4_808 | X4_808=U_803 | skf10(U_209, V_210, W_211)=U_803 | skf10(U_800, V_210, W_211)=U_803 | skf21(V_810, X_806, Y_799, Z_813, X1_814, V_210, W_211)=U_803 | ~member(W_211, X4_808, V_210) | ~member(W_211, U_803, V_210) | skf21(U_803, V_812, W_802, X_804, Y_811, Z_807, X1_798)!=U_803 | Z_813=X1_814 | Z_813=Y_799 | Y_799=X1_814 | Y_799=X_806 | Z_813=X_806 | X_806=X1_814 | X_806=V_810 | Y_799=V_810 | Z_813=V_810 | X1_814=V_810 | five(W_211, V_210) | ~member(W_211, X1_814, V_210) | ~member(W_211, Z_813, V_210) | ~member(W_211, Y_799, V_210) | ~member(W_211, X_806, V_210) | ~member(W_211, V_810, V_210) | ssSkP0(U_800, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.16 tff(c_1160, plain, (![X_821, W_211, V_819, V_210, Z_824, X1_826, Z_830, X1_815, U_827, V_818, X_828, W_823, U_817, Y_829, Y_816, U_209]: (skf21(V_818, X_828, Y_816, Z_824, X1_826, V_210, W_211)=skf10(U_817, V_210, W_211) | skf21(V_818, X_828, Y_816, Z_824, X1_826, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_817, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_819 | skf21(V_818, X_828, Y_816, Z_824, X1_826, V_210, W_211)=V_819 | skf10(U_817, V_210, W_211)=V_819 | V_819=U_827 | skf10(U_209, V_210, W_211)=U_827 | skf21(V_818, X_828, Y_816, Z_824, X1_826, V_210, W_211)=U_827 | skf10(U_817, V_210, W_211)=U_827 | ~member(W_211, V_819, V_210) | ~member(W_211, U_827, V_210) | skf21(U_827, V_819, W_823, X_821, Y_829, Z_830, X1_815)!=V_819 | ssSkP0(U_817, V_210, W_211) | Z_824=X1_826 | Z_824=Y_816 | Y_816=X1_826 | Y_816=X_828 | Z_824=X_828 | X_828=X1_826 | X_828=V_818 | Y_816=V_818 | Z_824=V_818 | X1_826=V_818 | five(W_211, V_210) | ~member(W_211, X1_826, V_210) | ~member(W_211, Z_824, V_210) | ~member(W_211, Y_816, V_210) | ~member(W_211, X_828, V_210) | ~member(W_211, V_818, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_1115, plain, (![W_771, V_780, W_211, V_210, Y_775, Y_772, U_776, Z_777, Z_784, X_779, V_781, X1_774, U_209, X1_783]: (skf21(V_780, X_779, Y_772, Z_777, X1_774, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_771 | skf21(V_780, X_779, Y_772, Z_777, X1_774, V_210, W_211)=W_771 | W_771=V_781 | skf10(U_209, V_210, W_211)=V_781 | skf21(V_780, X_779, Y_772, Z_777, X1_774, V_210, W_211)=V_781 | V_781=U_776 | W_771=U_776 | skf10(U_209, V_210, W_211)=U_776 | skf21(V_780, X_779, Y_772, Z_777, X1_774, V_210, W_211)=U_776 | ~member(W_211, W_771, V_210) | ~member(W_211, V_781, V_210) | ~member(W_211, U_776, V_210) | skf21(U_776, V_781, W_771, skf10(U_209, V_210, W_211), Y_775, Z_784, X1_783)!=skf10(U_209, V_210, W_211) | Z_777=X1_774 | Z_777=Y_772 | Y_772=X1_774 | Y_772=X_779 | Z_777=X_779 | X_779=X1_774 | X_779=V_780 | Y_772=V_780 | Z_777=V_780 | X1_774=V_780 | five(W_211, V_210) | ~member(W_211, X1_774, V_210) | ~member(W_211, Z_777, V_210) | ~member(W_211, Y_772, V_210) | ~member(W_211, X_779, V_210) | ~member(W_211, V_780, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 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)))). % 27.04/18.17 tff(c_846, plain, (![U_178, U_574, X_579, X_181, Z_179, U_578, V_581, Y_182, X1_580, Z_577, X1_180, W_177, V_183, W_576, Y_582]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_574, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_576 | skf10(U_574, W_177, U_178)=W_576 | W_576=V_581 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_581 | skf10(U_574, W_177, U_178)=V_581 | V_581=U_578 | W_576=U_578 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_578 | skf10(U_574, W_177, U_178)=U_578 | ~member(U_178, W_576, W_177) | ~member(U_178, V_581, W_177) | ~member(U_178, U_578, W_177) | skf21(U_578, V_581, W_576, X_579, Y_582, Z_577, X1_580)!=W_576 | ssSkP0(U_574, 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)))). % 27.04/18.17 tff(c_890, plain, (![V_606, X_597, X4_602, U_178, X_181, Z_179, Y_182, X1_603, U_595, X1_180, W_598, W_177, U_604, Y_599, V_183, Z_601]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_595, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_602 | skf10(U_595, W_177, U_178)=X4_602 | X4_602=V_606 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_606 | skf10(U_595, W_177, U_178)=V_606 | V_606=U_604 | X4_602=U_604 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_604 | skf10(U_595, W_177, U_178)=U_604 | ~member(U_178, X4_602, W_177) | ~member(U_178, V_606, W_177) | ~member(U_178, U_604, W_177) | skf21(U_604, V_606, W_598, X_597, Y_599, Z_601, X1_603)!=V_606 | ssSkP0(U_595, 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)))). % 27.04/18.17 tff(c_1093, plain, (![W_211, W_770, V_210, V_767, X5_760, X1_755, Z_759, V_764, X_769, Z_763, X1_758, Y_757, X4_762, U_754, X_766, Y_756, U_209]: (skf21(V_767, X_766, Y_756, Z_763, X1_758, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X5_760 | skf21(V_767, X_766, Y_756, Z_763, X1_758, V_210, W_211)=X5_760 | X5_760=X4_762 | skf10(U_209, V_210, W_211)=X4_762 | skf21(V_767, X_766, Y_756, Z_763, X1_758, V_210, W_211)=X4_762 | X4_762=U_754 | X5_760=U_754 | skf10(U_209, V_210, W_211)=U_754 | skf21(V_767, X_766, Y_756, Z_763, X1_758, V_210, W_211)=U_754 | ~member(W_211, X5_760, V_210) | ~member(W_211, X4_762, V_210) | ~member(W_211, U_754, V_210) | skf21(U_754, V_764, W_770, X_769, Y_757, Z_759, X1_755)!=U_754 | Z_763=X1_758 | Z_763=Y_756 | Y_756=X1_758 | Y_756=X_766 | Z_763=X_766 | X_766=X1_758 | X_766=V_767 | Y_756=V_767 | Z_763=V_767 | X1_758=V_767 | five(W_211, V_210) | ~member(W_211, X1_758, V_210) | ~member(W_211, Z_763, V_210) | ~member(W_211, Y_756, V_210) | ~member(W_211, X_766, V_210) | ~member(W_211, V_767, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_1048, plain, (![W_211, X_718, V_210, U_713, Y_723, U_720, Z_725, U_714, V_721, X1_719, U_209, W_716, U_722]: (skf10(U_720, V_210, W_211)=skf10(U_713, V_210, W_211) | skf10(U_722, V_210, W_211)=skf10(U_720, V_210, W_211) | skf10(U_722, V_210, W_211)=skf10(U_713, V_210, W_211) | skf10(U_722, V_210, W_211)=skf10(U_714, V_210, W_211) | skf10(U_720, V_210, W_211)=skf10(U_714, V_210, W_211) | skf10(U_714, V_210, W_211)=skf10(U_713, V_210, W_211) | skf10(U_714, 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_720, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_713, 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_721, W_716, X_718, Y_723, Z_725, X1_719)!=skf10(U_209, V_210, W_211) | ssSkP0(U_713, V_210, W_211) | ssSkP0(U_720, V_210, W_211) | ssSkP0(U_722, V_210, W_211) | ssSkP0(U_714, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 tff(c_1025, plain, (![U_692, W_211, V_210, U_701, Y_696, X_691, U_690, W_693, Z_700, X1_699, U_209, U_695]: (skf10(U_701, V_210, W_211)=skf10(U_695, V_210, W_211) | skf10(U_695, V_210, W_211)=skf10(U_692, V_210, W_211) | skf10(U_701, V_210, W_211)=skf10(U_692, V_210, W_211) | skf10(U_692, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_695, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_701, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_690 | skf10(U_692, V_210, W_211)=U_690 | skf10(U_695, V_210, W_211)=U_690 | skf10(U_701, V_210, W_211)=U_690 | five(W_211, V_210) | ~member(W_211, U_690, V_210) | skf21(U_690, skf10(U_209, V_210, W_211), W_693, X_691, Y_696, Z_700, X1_699)!=skf10(U_209, V_210, W_211) | ssSkP0(U_701, V_210, W_211) | ssSkP0(U_695, V_210, W_211) | ssSkP0(U_692, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_1003, plain, (![U_684, U_689, W_211, U_681, V_210, V_682, Y_679, Z_686, U_677, X1_687, W_678, X_683, U_209]: (skf10(U_689, V_210, W_211)=skf10(U_681, V_210, W_211) | skf10(U_681, V_210, W_211)=skf10(U_677, V_210, W_211) | skf10(U_689, V_210, W_211)=skf10(U_677, V_210, W_211) | skf10(U_677, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_681, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_689, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_684 | skf10(U_677, V_210, W_211)=U_684 | skf10(U_681, V_210, W_211)=U_684 | skf10(U_689, V_210, W_211)=U_684 | five(W_211, V_210) | ~member(W_211, U_684, V_210) | skf21(U_684, V_682, W_678, X_683, Y_679, Z_686, X1_687)!=U_684 | ssSkP0(U_689, V_210, W_211) | ssSkP0(U_681, V_210, W_211) | ssSkP0(U_677, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_958, plain, (![W_211, V_210, X_645, U_644, V_651, U_646, X1_654, Y_650, U_652, U_209, Z_649]: (skf10(U_646, V_210, W_211)=skf10(U_644, V_210, W_211) | skf10(U_646, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_644, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_651 | skf10(U_646, V_210, W_211)=V_651 | skf10(U_644, V_210, W_211)=V_651 | V_651=U_652 | skf10(U_209, V_210, W_211)=U_652 | skf10(U_646, V_210, W_211)=U_652 | skf10(U_644, V_210, W_211)=U_652 | five(W_211, V_210) | ~member(W_211, V_651, V_210) | ~member(W_211, U_652, V_210) | skf21(U_652, V_651, skf10(U_209, V_210, W_211), X_645, Y_650, Z_649, X1_654)!=skf10(U_209, V_210, W_211) | ssSkP0(U_644, V_210, W_211) | ssSkP0(U_646, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_980, plain, (![U_656, W_211, V_210, W_662, V_658, U_657, U_663, U_209, X_660, Z_666, Y_665, X1_655]: (skf10(U_657, V_210, W_211)=skf10(U_656, V_210, W_211) | skf10(U_657, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_656, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_658 | skf10(U_657, V_210, W_211)=V_658 | skf10(U_656, V_210, W_211)=V_658 | V_658=U_663 | skf10(U_209, V_210, W_211)=U_663 | skf10(U_657, V_210, W_211)=U_663 | skf10(U_656, V_210, W_211)=U_663 | five(W_211, V_210) | ~member(W_211, V_658, V_210) | ~member(W_211, U_663, V_210) | skf21(U_663, V_658, W_662, X_660, Y_665, Z_666, X1_655)!=V_658 | ssSkP0(U_656, V_210, W_211) | ssSkP0(U_657, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_914, plain, (![U_628, X4_621, Z_626, W_211, V_210, X_625, U_616, U_624, W_623, U_209, Y_619, X1_622, V_620]: (skf10(U_624, V_210, W_211)=skf10(U_616, V_210, W_211) | skf10(U_616, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_624, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_621 | skf10(U_616, V_210, W_211)=X4_621 | skf10(U_624, V_210, W_211)=X4_621 | X4_621=U_628 | skf10(U_209, V_210, W_211)=U_628 | skf10(U_616, V_210, W_211)=U_628 | skf10(U_624, V_210, W_211)=U_628 | five(W_211, V_210) | ~member(W_211, X4_621, V_210) | ~member(W_211, U_628, V_210) | skf21(U_628, V_620, W_623, X_625, Y_619, Z_626, X1_622)!=U_628 | ssSkP0(U_624, V_210, W_211) | ssSkP0(U_616, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_869, plain, (![W_211, V_210, W_591, U_586, Y_593, U_585, Z_589, V_590, U_209, X1_592]: (skf10(U_585, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_591 | skf10(U_585, V_210, W_211)=W_591 | W_591=V_590 | skf10(U_209, V_210, W_211)=V_590 | skf10(U_585, V_210, W_211)=V_590 | V_590=U_586 | W_591=U_586 | skf10(U_209, V_210, W_211)=U_586 | skf10(U_585, V_210, W_211)=U_586 | five(W_211, V_210) | ~member(W_211, W_591, V_210) | ~member(W_211, V_590, V_210) | ~member(W_211, U_586, V_210) | skf21(U_586, V_590, W_591, skf10(U_209, V_210, W_211), Y_593, Z_589, X1_592)!=skf10(U_209, V_210, W_211) | ssSkP0(U_585, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_891, plain, (![V_606, X_597, X4_602, W_211, V_210, X1_603, U_595, W_598, U_604, Y_599, U_209, Z_601]: (skf10(U_595, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_602 | skf10(U_595, V_210, W_211)=X4_602 | X4_602=V_606 | skf10(U_209, V_210, W_211)=V_606 | skf10(U_595, V_210, W_211)=V_606 | V_606=U_604 | X4_602=U_604 | skf10(U_209, V_210, W_211)=U_604 | skf10(U_595, V_210, W_211)=U_604 | five(W_211, V_210) | ~member(W_211, X4_602, V_210) | ~member(W_211, V_606, V_210) | ~member(W_211, U_604, V_210) | skf21(U_604, V_606, W_598, X_597, Y_599, Z_601, X1_603)!=V_606 | ssSkP0(U_595, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 tff(c_847, plain, (![W_211, V_210, U_574, X_579, U_578, V_581, X1_580, Z_577, W_576, U_209, Y_582]: (skf10(U_574, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_576 | skf10(U_574, V_210, W_211)=W_576 | W_576=V_581 | skf10(U_209, V_210, W_211)=V_581 | skf10(U_574, V_210, W_211)=V_581 | V_581=U_578 | W_576=U_578 | skf10(U_209, V_210, W_211)=U_578 | skf10(U_574, V_210, W_211)=U_578 | five(W_211, V_210) | ~member(W_211, W_576, V_210) | ~member(W_211, V_581, V_210) | ~member(W_211, U_578, V_210) | skf21(U_578, V_581, W_576, X_579, Y_582, Z_577, X1_580)!=W_576 | ssSkP0(U_574, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 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)))). % 27.04/18.17 tff(c_825, plain, (![X_564, W_211, V_210, Y_566, U_569, X5_562, V_570, X4_573, X1_567, U_563, Z_561, U_209, W_571]: (skf10(U_563, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X5_562 | skf10(U_563, V_210, W_211)=X5_562 | X5_562=X4_573 | skf10(U_209, V_210, W_211)=X4_573 | skf10(U_563, V_210, W_211)=X4_573 | X4_573=U_569 | X5_562=U_569 | skf10(U_209, V_210, W_211)=U_569 | skf10(U_563, V_210, W_211)=U_569 | five(W_211, V_210) | ~member(W_211, X5_562, V_210) | ~member(W_211, X4_573, V_210) | ~member(W_211, U_569, V_210) | skf21(U_569, V_570, W_571, X_564, Y_566, Z_561, X1_567)!=U_569 | ssSkP0(U_563, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 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) | ~ssSkP0(X_226, V_228, U_224) | ~order(U_224, X_226) | ~nonreflexive(U_224, X_226) | ~past(U_224, X_226) | ~event(U_224, X_226) | ~nonhuman(U_224, X_226) | ~of(U_224, W_223, Y_227) | ~woman(U_224, Y_227) | ~agent(U_224, X_226, Y_227) | ~forename(U_224, W_223) | ~mia_forename(U_224, W_223) | ~five(U_224, V_228) | ~group(U_224, V_228)))). % 27.04/18.17 tff(c_798, plain, (~nonhuman(skc5, skc6))). % 27.04/18.17 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) | ~ssSkP0(Y_221, W_216, U_217) | ~order(U_217, Y_221) | ~nonreflexive(U_217, Y_221) | ~past(U_217, Y_221) | ~event(U_217, Y_221) | ~nonhuman(U_217, Y_221) | ~of(U_217, X_220, Z_218) | ~woman(U_217, Z_218) | ~agent(U_217, Y_221, Z_218) | ~forename(U_217, X_220) | ~mia_forename(U_217, X_220) | ~five(U_217, W_216) | ~group(U_217, W_216) | ~dollar(U_217, skf8(U_217, V_222))))). % 27.04/18.17 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)))). % 27.04/18.17 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))). % 27.04/18.17 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))). % 27.04/18.17 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))). % 27.04/18.17 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))). % 27.04/18.17 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))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 tff(c_636, plain, (![W_471]: (skc8=W_471 | ~forename(skc5, W_471) | ~of(skc5, W_471, skc9)))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 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)))). % 27.04/18.17 tff(c_629, plain, (~act(skc5, skc7))). % 27.04/18.17 tff(c_615, plain, (![U_47, V_48]: (~act(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.04/18.17 tff(c_624, plain, (~agent(skc5, skc6, skc7))). % 27.04/18.17 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)))). % 27.04/18.17 tff(c_591, plain, (![U_47, V_48]: (~cost(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.04/18.17 tff(c_515, plain, (![U_41, V_42]: (~entity(U_41, V_42) | ~act(U_41, V_42)))). % 27.04/18.17 tff(c_602, plain, (~food(skc5, skc9))). % 27.04/18.17 tff(c_110, plain, (![U_109, V_110]: (member(U_109, skf18(V_110, U_109), V_110) | ~five(U_109, V_110)))). % 27.04/18.17 tff(c_537, plain, (![U_77, V_78]: (~food(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.04/18.17 tff(c_597, plain, (~abstraction(skc5, skc7))). % 27.04/18.17 tff(c_532, plain, (![U_419, V_420]: (~abstraction(U_419, V_420) | ~beverage(U_419, V_420)))). % 27.04/18.17 tff(c_516, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~cost(U_27, V_28)))). % 27.04/18.17 tff(c_504, plain, (![U_25, V_26]: (~abstraction(U_25, V_26) | ~five(U_25, V_26)))). % 27.04/18.17 tff(c_136, plain, (![V_136, U_135]: (~five(V_136, U_135) | skf14(U_135, V_136)!=skf12(U_135, V_136)))). % 27.04/18.17 tff(c_581, plain, (~animate(skc5, skc7))). % 27.04/18.17 tff(c_562, plain, (![U_47, V_48]: (~animate(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.04/18.17 tff(c_556, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~five(U_25, V_26)))). % 27.04/18.17 tff(c_108, plain, (![U_107, V_108]: (member(U_107, skf20(V_108, U_107), V_108) | ~five(U_107, V_108)))). % 27.04/18.17 tff(c_549, plain, (![U_41, V_42]: (~abstraction(U_41, V_42) | ~act(U_41, V_42)))). % 27.04/18.17 tff(c_567, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~five(U_25, V_26)))). % 27.04/18.18 tff(c_550, plain, (![U_27, V_28]: (~abstraction(U_27, V_28) | ~cost(U_27, V_28)))). % 27.04/18.18 tff(c_486, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 27.04/18.18 tff(c_464, plain, (![U_387, V_388]: (~animate(U_387, V_388) | ~food(U_387, V_388)))). % 27.04/18.18 tff(c_112, plain, (![U_111, V_112]: (member(U_111, skf16(V_112, U_111), V_112) | ~five(U_111, V_112)))). % 27.04/18.18 tff(c_498, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 27.04/18.18 tff(c_551, plain, (~abstraction(skc5, skc6))). % 27.04/18.18 tff(c_469, plain, (![U_29, V_30]: (~abstraction(U_29, V_30) | ~event(U_29, V_30)))). % 27.04/18.18 tff(c_120, plain, (![V_120, U_119]: (~five(V_120, U_119) | skf20(U_119, V_120)!=skf14(U_119, V_120)))). % 27.04/18.18 tff(c_463, plain, (![U_387, V_388]: (~living(U_387, V_388) | ~food(U_387, V_388)))). % 27.04/18.18 tff(c_531, plain, (~beverage(skc5, skc6))). % 27.04/18.18 tff(c_455, plain, (![U_47, V_48]: (entity(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.04/18.18 tff(c_523, plain, (~beverage(skc5, skc9))). % 27.04/18.18 tff(c_450, plain, (![U_47, V_48]: (~female(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.04/18.18 tff(c_134, plain, (![V_134, U_133]: (~five(V_134, U_133) | skf16(U_133, V_134)!=skf14(U_133, V_134)))). % 27.04/18.18 tff(c_517, plain, (~entity(skc5, skc6))). % 27.04/18.18 tff(c_492, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~event(U_29, V_30)))). % 27.04/18.18 tff(c_445, plain, (![U_21, V_22]: (~abstraction(U_21, V_22) | ~group(U_21, V_22)))). % 27.04/18.18 tff(c_132, plain, (![V_132, U_131]: (~five(V_132, U_131) | skf16(U_131, V_132)!=skf12(U_131, V_132)))). % 27.04/18.18 tff(c_403, plain, (![U_369, V_370]: (~multiple(U_369, V_370) | ~eventuality(U_369, V_370)))). % 27.04/18.18 tff(c_420, plain, (![U_371, V_372]: (impartial(U_371, V_372) | ~food(U_371, V_372)))). % 27.04/18.18 tff(c_375, plain, (![U_59, V_60]: (~eventuality(U_59, V_60) | ~entity(U_59, V_60)))). % 27.04/18.18 tff(c_381, plain, (![U_5, V_6]: (abstraction(U_5, V_6) | ~cash(U_5, V_6)))). % 27.04/18.18 tff(c_353, plain, (![U_341, V_342]: (~multiple(U_341, V_342) | ~entity(U_341, V_342)))). % 27.04/18.18 tff(c_114, plain, (![U_113, V_114]: (member(U_113, skf14(V_114, U_113), V_114) | ~five(U_113, V_114)))). % 27.04/18.18 tff(c_347, plain, (![U_17, V_18]: (~entity(U_17, V_18) | ~abstraction(U_17, V_18)))). % 27.04/18.18 tff(c_475, plain, (abstraction(skc5, skc8))). % 27.04/18.18 tff(c_359, plain, (![U_345, V_346]: (abstraction(U_345, V_346) | ~forename(U_345, V_346)))). % 27.04/18.18 tff(c_118, plain, (![V_118, U_117]: (~five(V_118, U_117) | skf20(U_117, V_118)!=skf12(U_117, V_118)))). % 27.04/18.18 tff(c_387, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~abstraction(U_17, V_18)))). % 27.04/18.18 tff(c_419, plain, (![U_371, V_372]: (nonliving(U_371, V_372) | ~food(U_371, V_372)))). % 27.04/18.18 tff(c_418, plain, (![U_371, V_372]: (entity(U_371, V_372) | ~food(U_371, V_372)))). % 27.04/18.18 tff(c_417, plain, (![U_371, V_372]: (~female(U_371, V_372) | ~food(U_371, V_372)))). % 27.04/18.18 tff(c_392, plain, (![U_363, V_364]: (~multiple(U_363, V_364) | ~abstraction(U_363, V_364)))). % 27.04/18.18 tff(c_116, plain, (![U_115, V_116]: (member(U_115, skf12(V_116, U_115), V_116) | ~five(U_115, V_116)))). % 27.04/18.18 tff(c_248, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 27.04/18.18 tff(c_437, plain, (~cost(skc5, skc9))). % 27.04/18.18 tff(c_436, plain, (~act(skc5, skc9))). % 27.04/18.18 tff(c_122, plain, (![V_122, U_121]: (~five(V_122, U_121) | skf20(U_121, V_122)!=skf16(U_121, V_122)))). % 27.04/18.18 tff(c_429, plain, (~event(skc5, skc9))). % 27.04/18.18 tff(c_425, plain, (~eventuality(skc5, skc9))). % 27.04/18.18 tff(c_319, plain, (![U_37, V_38]: (~female(U_37, V_38) | ~eventuality(U_37, V_38)))). % 27.04/18.18 tff(c_258, plain, (![U_49, V_50]: (object(U_49, V_50) | ~food(U_49, V_50)))). % 27.04/18.18 tff(c_240, plain, (![U_31, V_32]: (singleton(U_31, V_32) | ~eventuality(U_31, V_32)))). % 27.04/18.18 tff(c_130, plain, (![V_130, U_129]: (~five(V_130, U_129) | skf18(U_129, V_130)!=skf16(U_129, V_130)))). % 27.04/18.18 tff(c_341, plain, (![U_333, V_334]: (~female(U_333, V_334) | ~abstraction(U_333, V_334)))). % 27.04/18.18 tff(c_294, plain, (![U_311, V_312]: (singleton(U_311, V_312) | ~abstraction(U_311, V_312)))). % 27.04/18.18 tff(c_329, plain, (![U_33, V_34]: (~general(U_33, V_34) | ~eventuality(U_33, V_34)))). % 27.04/18.18 tff(c_126, plain, (![V_126, U_125]: (~five(V_126, U_125) | skf18(U_125, V_126)!=skf12(U_125, V_126)))). % 27.04/18.18 tff(c_304, plain, (![U_315, V_316]: (abstraction(U_315, V_316) | ~currency(U_315, V_316)))). % 27.04/18.18 tff(c_320, plain, (![U_65, V_66]: (~female(U_65, V_66) | ~object(U_65, V_66)))). % 27.04/18.18 tff(c_274, plain, (![U_295, V_296]: (~existent(U_295, V_296) | ~eventuality(U_295, V_296)))). % 27.04/18.18 tff(c_370, plain, (entity(skc5, skc9))). % 27.04/18.18 tff(c_253, plain, (![U_77, V_78]: (entity(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.04/18.18 tff(c_128, plain, (![V_128, U_127]: (~five(V_128, U_127) | skf18(U_127, V_128)!=skf14(U_127, V_128)))). % 27.04/18.18 tff(c_364, plain, (~abstraction(skc5, skc9))). % 27.04/18.18 tff(c_309, plain, (![U_317, V_318]: (~human(U_317, V_318) | ~abstraction(U_317, V_318)))). % 27.04/18.18 tff(c_206, plain, (![U_67, V_68]: (relation(U_67, V_68) | ~forename(U_67, V_68)))). % 27.04/18.18 tff(c_124, plain, (![V_124, U_123]: (~five(V_124, U_123) | skf20(U_123, V_124)!=skf18(U_123, V_124)))). % 27.04/18.18 tff(c_289, plain, (![U_309, V_310]: (singleton(U_309, V_310) | ~entity(U_309, V_310)))). % 27.04/18.18 tff(c_234, plain, (![U_77, V_78]: (living(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.04/18.18 tff(c_328, plain, (![U_57, V_58]: (~general(U_57, V_58) | ~entity(U_57, V_58)))). % 27.04/18.18 tff(c_268, plain, (![U_77, V_78]: (impartial(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.04/18.18 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~abstraction(U_19, V_20)))). % 27.04/18.18 tff(c_100, plain, (![U_99, V_100]: (~nonliving(U_99, V_100) | ~living(U_99, V_100)))). % 27.04/18.18 tff(c_335, plain, (human(skc5, skc9))). % 27.04/18.18 tff(c_86, plain, (![U_85, V_86]: (human(U_85, V_86) | ~human_person(U_85, V_86)))). % 27.04/18.18 tff(c_96, plain, (![U_95, V_96]: (~singleton(U_95, V_96) | ~multiple(U_95, V_96)))). % 27.04/18.18 tff(c_94, plain, (![U_93, V_94]: (~specific(U_93, V_94) | ~general(U_93, V_94)))). % 27.04/18.18 tff(c_92, plain, (![U_91, V_92]: (~unisex(U_91, V_92) | ~female(U_91, V_92)))). % 27.04/18.18 tff(c_30, plain, (![U_29, V_30]: (eventuality(U_29, V_30) | ~event(U_29, V_30)))). % 27.04/18.18 tff(c_98, plain, (![U_97, V_98]: (~present(U_97, V_98) | ~past(U_97, V_98)))). % 27.04/18.18 tff(c_16, plain, (![U_15, V_16]: (nonhuman(U_15, V_16) | ~abstraction(U_15, V_16)))). % 27.04/18.18 tff(c_299, plain, (female(skc5, skc9))). % 27.04/18.18 tff(c_8, plain, (![U_7, V_8]: (possession(U_7, V_8) | ~currency(U_7, V_8)))). % 27.04/18.18 tff(c_90, plain, (![U_89, V_90]: (female(U_89, V_90) | ~woman(U_89, V_90)))). % 27.04/18.18 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~abstraction(U_11, V_12)))). % 27.04/18.18 tff(c_56, plain, (![U_55, V_56]: (thing(U_55, V_56) | ~entity(U_55, V_56)))). % 27.04/18.18 tff(c_6, plain, (![U_5, V_6]: (currency(U_5, V_6) | ~cash(U_5, V_6)))). % 27.04/18.18 tff(c_102, plain, (![U_101, V_102]: (~nonhuman(U_101, V_102) | ~human(U_101, V_102)))). % 27.04/18.18 tff(c_72, plain, (![U_71, V_72]: (abstraction(U_71, V_72) | ~relation(U_71, V_72)))). % 27.04/18.18 tff(c_58, plain, (![U_57, V_58]: (specific(U_57, V_58) | ~entity(U_57, V_58)))). % 27.04/18.18 tff(c_280, plain, (animate(skc5, skc9))). % 27.04/18.18 tff(c_88, plain, (![U_87, V_88]: (animate(U_87, V_88) | ~human_person(U_87, V_88)))). % 27.04/18.18 tff(c_48, plain, (![U_47, V_48]: (food(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.04/18.18 tff(c_36, plain, (![U_35, V_36]: (nonexistent(U_35, V_36) | ~eventuality(U_35, V_36)))). % 27.04/18.18 tff(c_10, plain, (![U_9, V_10]: (abstraction(U_9, V_10) | ~possession(U_9, V_10)))). % 27.04/18.18 tff(c_263, plain, (human_person(skc5, skc9))). % 27.04/18.18 tff(c_82, plain, (![U_81, V_82]: (impartial(U_81, V_82) | ~organism(U_81, V_82)))). % 27.04/18.18 tff(c_76, plain, (![U_75, V_76]: (human_person(U_75, V_76) | ~woman(U_75, V_76)))). % 27.04/18.18 tff(c_52, plain, (![U_51, V_52]: (object(U_51, V_52) | ~substance_matter(U_51, V_52)))). % 27.04/18.18 tff(c_80, plain, (![U_79, V_80]: (entity(U_79, V_80) | ~organism(U_79, V_80)))). % 27.04/18.18 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 27.04/18.18 tff(c_104, plain, (![U_103, V_104]: (~existent(U_103, V_104) | ~nonexistent(U_103, V_104)))). % 27.04/18.18 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~five(U_25, V_26)))). % 27.04/18.18 tff(c_54, plain, (![U_53, V_54]: (entity(U_53, V_54) | ~object(U_53, V_54)))). % 27.04/18.18 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 27.04/18.18 tff(c_32, plain, (![U_31, V_32]: (thing(U_31, V_32) | ~eventuality(U_31, V_32)))). % 27.04/18.18 tff(c_84, plain, (![U_83, V_84]: (living(U_83, V_84) | ~organism(U_83, V_84)))). % 27.04/18.18 tff(c_74, plain, (![U_73, V_74]: (forename(U_73, V_74) | ~mia_forename(U_73, V_74)))). % 27.04/18.19 tff(c_106, plain, (![U_105, V_106]: (~animate(U_105, V_106) | ~nonliving(U_105, V_106)))). % 27.04/18.19 tff(c_38, plain, (![U_37, V_38]: (unisex(U_37, V_38) | ~eventuality(U_37, V_38)))). % 27.04/18.19 tff(c_18, plain, (![U_17, V_18]: (general(U_17, V_18) | ~abstraction(U_17, V_18)))). % 27.04/18.19 tff(c_219, plain, (act(skc5, skc6))). % 27.04/18.19 tff(c_42, plain, (![U_41, V_42]: (event(U_41, V_42) | ~act(U_41, V_42)))). % 27.04/18.19 tff(c_40, plain, (![U_39, V_40]: (act(U_39, V_40) | ~order(U_39, V_40)))). % 27.04/18.19 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~cost(U_27, V_28)))). % 27.04/18.19 tff(c_62, plain, (![U_61, V_62]: (nonliving(U_61, V_62) | ~object(U_61, V_62)))). % 27.04/18.19 tff(c_44, plain, (![U_43, V_44]: (event(U_43, V_44) | ~order(U_43, V_44)))). % 27.04/18.19 tff(c_70, plain, (![U_69, V_70]: (relation(U_69, V_70) | ~relname(U_69, V_70)))). % 27.04/18.19 tff(c_50, plain, (![U_49, V_50]: (substance_matter(U_49, V_50) | ~food(U_49, V_50)))). % 27.04/18.19 tff(c_66, plain, (![U_65, V_66]: (unisex(U_65, V_66) | ~object(U_65, V_66)))). % 27.04/18.19 tff(c_60, plain, (![U_59, V_60]: (existent(U_59, V_60) | ~entity(U_59, V_60)))). % 27.04/18.19 tff(c_198, plain, (beverage(skc5, skc7))). % 27.04/18.19 tff(c_46, plain, (![U_45, V_46]: (beverage(U_45, V_46) | ~shake_beverage(U_45, V_46)))). % 27.04/18.19 tff(c_78, plain, (![U_77, V_78]: (organism(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.04/18.19 tff(c_4, plain, (![U_3, V_4]: (cash(U_3, V_4) | ~dollar(U_3, V_4)))). % 27.04/18.19 tff(c_68, plain, (![U_67, V_68]: (relname(U_67, V_68) | ~forename(U_67, V_68)))). % 27.04/18.19 tff(c_34, plain, (![U_33, V_34]: (specific(U_33, V_34) | ~eventuality(U_33, V_34)))). % 27.04/18.19 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 27.04/18.19 tff(c_64, plain, (![U_63, V_64]: (impartial(U_63, V_64) | ~object(U_63, V_64)))). % 27.04/18.19 tff(c_176, plain, (agent(skc5, skc6, skc9))). % 27.04/18.19 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 27.04/18.19 tff(c_178, plain, (patient(skc5, skc6, skc7))). % 27.04/18.19 tff(c_174, plain, (of(skc5, skc8, skc9))). % 27.04/18.19 tff(c_162, plain, (order(skc5, skc6))). % 27.04/18.19 tff(c_160, plain, (shake_beverage(skc5, skc7))). % 27.04/18.19 tff(c_158, plain, (woman(skc5, skc9))). % 27.04/18.19 tff(c_164, plain, (nonreflexive(skc5, skc6))). % 27.04/18.19 tff(c_166, plain, (past(skc5, skc6))). % 27.04/18.19 tff(c_168, plain, (event(skc5, skc6))). % 27.04/18.19 tff(c_170, plain, (forename(skc5, skc8))). % 27.04/18.19 tff(c_172, plain, (mia_forename(skc5, skc8))). % 27.04/18.19 tff(c_156, plain, (actual_world(skc5))). % 27.04/18.19 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 27.04/18.19 %------------------------------------------------------------------------------