%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP054-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 : n021.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 27.55s 18.11s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NLP054-1 : TPTP v9.0.0. Released v2.4.0. % 0.03/0.12 % 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.33 % Computer : n021.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Apr 8 08:18:13 EDT 2025 % 0.13/0.33 % CPUTime : % 27.55/18.11 % 27.55/18.11 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 27.55/18.11 % 27.55/18.11 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 27.55/18.12 %$ 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 % 27.55/18.12 % 27.55/18.12 %Foreground sorts: % 27.55/18.12 % 27.55/18.12 % 27.55/18.12 %Background operators: % 27.55/18.12 % 27.55/18.12 % 27.55/18.12 %Foreground operators: % 27.55/18.12 tff(nonliving, type, nonliving: ($i * $i) > $o). % 27.55/18.12 tff(relation, type, relation: ($i * $i) > $o). % 27.55/18.12 tff(member, type, member: ($i * $i * $i) > $o). % 27.55/18.12 tff(forename, type, forename: ($i * $i) > $o). % 27.55/18.12 tff(skc7, type, skc7: $i). % 27.55/18.12 tff(female, type, female: ($i * $i) > $o). % 27.55/18.12 tff(living, type, living: ($i * $i) > $o). % 27.55/18.12 tff(cost, type, cost: ($i * $i) > $o). % 27.55/18.12 tff(human_person, type, human_person: ($i * $i) > $o). % 27.55/18.12 tff(present, type, present: ($i * $i) > $o). % 27.55/18.12 tff(entity, type, entity: ($i * $i) > $o). % 27.55/18.12 tff(substance_matter, type, substance_matter: ($i * $i) > $o). % 27.55/18.12 tff(skc9, type, skc9: $i). % 27.55/18.12 tff(past, type, past: ($i * $i) > $o). % 27.55/18.12 tff(beverage, type, beverage: ($i * $i) > $o). % 27.55/18.12 tff(eventuality, type, eventuality: ($i * $i) > $o). % 27.55/18.12 tff(existent, type, existent: ($i * $i) > $o). % 27.55/18.12 tff(abstraction, type, abstraction: ($i * $i) > $o). % 27.55/18.12 tff(skc8, type, skc8: $i). % 27.55/18.12 tff(relname, type, relname: ($i * $i) > $o). % 27.55/18.12 tff(possession, type, possession: ($i * $i) > $o). % 27.55/18.12 tff(singleton, type, singleton: ($i * $i) > $o). % 27.55/18.12 tff(multiple, type, multiple: ($i * $i) > $o). % 27.55/18.12 tff(organism, type, organism: ($i * $i) > $o). % 27.55/18.12 tff(shake_beverage, type, shake_beverage: ($i * $i) > $o). % 27.55/18.12 tff(animate, type, animate: ($i * $i) > $o). % 27.55/18.12 tff(of, type, of: ($i * $i * $i) > $o). % 27.55/18.12 tff(skf14, type, skf14: ($i * $i) > $i). % 27.55/18.12 tff(actual_world, type, actual_world: $i > $o). % 27.55/18.12 tff(dollar, type, dollar: ($i * $i) > $o). % 27.55/18.12 tff(agent, type, agent: ($i * $i * $i) > $o). % 27.55/18.12 tff(group, type, group: ($i * $i) > $o). % 27.55/18.12 tff(five, type, five: ($i * $i) > $o). % 27.55/18.12 tff(general, type, general: ($i * $i) > $o). % 27.55/18.12 tff(nonhuman, type, nonhuman: ($i * $i) > $o). % 27.55/18.12 tff(food, type, food: ($i * $i) > $o). % 27.55/18.12 tff(event, type, event: ($i * $i) > $o). % 27.55/18.12 tff(woman, type, woman: ($i * $i) > $o). % 27.55/18.12 tff(currency, type, currency: ($i * $i) > $o). % 27.55/18.12 tff(patient, type, patient: ($i * $i * $i) > $o). % 27.55/18.12 tff(skf8, type, skf8: ($i * $i) > $i). % 27.55/18.12 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 27.55/18.12 tff(cash, type, cash: ($i * $i) > $o). % 27.55/18.12 tff(thing, type, thing: ($i * $i) > $o). % 27.55/18.12 tff(human, type, human: ($i * $i) > $o). % 27.55/18.12 tff(skf10, type, skf10: ($i * $i * $i) > $i). % 27.55/18.12 tff(skf18, type, skf18: ($i * $i) > $i). % 27.55/18.12 tff(ssSkP0, type, ssSkP0: ($i * $i * $i) > $o). % 27.55/18.12 tff(skc5, type, skc5: $i). % 27.55/18.12 tff(unisex, type, unisex: ($i * $i) > $o). % 27.55/18.12 tff(skf16, type, skf16: ($i * $i) > $i). % 27.55/18.12 tff(set, type, set: ($i * $i) > $o). % 27.55/18.12 tff(skf12, type, skf12: ($i * $i) > $i). % 27.55/18.12 tff(skc6, type, skc6: $i). % 27.55/18.12 tff(impartial, type, impartial: ($i * $i) > $o). % 27.55/18.12 tff(object, type, object: ($i * $i) > $o). % 27.55/18.12 tff(order, type, order: ($i * $i) > $o). % 27.55/18.12 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 27.55/18.12 tff(specific, type, specific: ($i * $i) > $o). % 27.55/18.12 tff(skf20, type, skf20: ($i * $i) > $i). % 27.55/18.12 tff(act, type, act: ($i * $i) > $o). % 27.55/18.12 tff(mia_forename, type, mia_forename: ($i * $i) > $o). % 27.55/18.12 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i) > $i). % 27.55/18.12 % 27.55/18.12 %Saturated clause set: % 27.55/18.12 tff(c_1625, plain, (![X_1529, Z_1556, Z_1542, Z_1545, U_178, Y_1538, X1_1530, V_1533, X_181, X1_1551, Z_179, X_1557, V_1549, X1_1540, V_1531, Y_1532, Y_182, Y_1552, X_1554, V_1550, Y_1544, X1_1546, X1_180, Y_1555, W_177, V_183, Z_1543, X1_1553, W_1537, Z_1547, X_1536, X_1539, V_1534]: (skf21(V_1534, X_1539, Y_1544, Z_1542, X1_1546, W_177, U_178)=skf21(V_1531, X_1529, Y_1538, Z_1545, X1_1553, W_177, U_178) | skf21(V_1549, X_1557, Y_1552, Z_1556, X1_1540, W_177, U_178)=skf21(V_1534, X_1539, Y_1544, Z_1542, X1_1546, W_177, U_178) | skf21(V_1549, X_1557, Y_1552, Z_1556, X1_1540, W_177, U_178)=skf21(V_1531, X_1529, Y_1538, Z_1545, X1_1553, W_177, U_178) | skf21(V_1549, X_1557, Y_1552, Z_1556, X1_1540, W_177, U_178)=skf21(V_1533, X_1554, Y_1532, Z_1543, X1_1551, W_177, U_178) | skf21(V_1534, X_1539, Y_1544, Z_1542, X1_1546, W_177, U_178)=skf21(V_1533, X_1554, Y_1532, Z_1543, X1_1551, W_177, U_178) | skf21(V_1533, X_1554, Y_1532, Z_1543, X1_1551, W_177, U_178)=skf21(V_1531, X_1529, Y_1538, Z_1545, X1_1553, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1533, X_1554, Y_1532, Z_1543, X1_1551, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1549, X_1557, Y_1552, Z_1556, X1_1540, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1534, X_1539, Y_1544, Z_1542, X1_1546, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1531, X_1529, Y_1538, Z_1545, X1_1553, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1550, W_1537, X_1536, Y_1555, Z_1547, X1_1530)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1545=X1_1553 | Z_1545=Y_1538 | Y_1538=X1_1553 | Y_1538=X_1529 | Z_1545=X_1529 | X_1529=X1_1553 | X_1529=V_1531 | Y_1538=V_1531 | Z_1545=V_1531 | X1_1553=V_1531 | ~member(U_178, X1_1553, W_177) | ~member(U_178, Z_1545, W_177) | ~member(U_178, Y_1538, W_177) | ~member(U_178, X_1529, W_177) | ~member(U_178, V_1531, W_177) | Z_1542=X1_1546 | Z_1542=Y_1544 | Y_1544=X1_1546 | Y_1544=X_1539 | Z_1542=X_1539 | X_1539=X1_1546 | X_1539=V_1534 | Y_1544=V_1534 | Z_1542=V_1534 | X1_1546=V_1534 | ~member(U_178, X1_1546, W_177) | ~member(U_178, Z_1542, W_177) | ~member(U_178, Y_1544, W_177) | ~member(U_178, X_1539, W_177) | ~member(U_178, V_1534, W_177) | Z_1556=X1_1540 | Z_1556=Y_1552 | Y_1552=X1_1540 | Y_1552=X_1557 | Z_1556=X_1557 | X_1557=X1_1540 | X_1557=V_1549 | Y_1552=V_1549 | Z_1556=V_1549 | X1_1540=V_1549 | ~member(U_178, X1_1540, W_177) | ~member(U_178, Z_1556, W_177) | ~member(U_178, Y_1552, W_177) | ~member(U_178, X_1557, W_177) | ~member(U_178, V_1549, W_177) | Z_1543=X1_1551 | Z_1543=Y_1532 | Y_1532=X1_1551 | Y_1532=X_1554 | Z_1543=X_1554 | X_1554=X1_1551 | X_1554=V_1533 | Y_1532=V_1533 | Z_1543=V_1533 | X1_1551=V_1533 | ~member(U_178, X1_1551, W_177) | ~member(U_178, Z_1543, W_177) | ~member(U_178, Y_1532, W_177) | ~member(U_178, X_1554, W_177) | ~member(U_178, V_1533, 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.55/18.12 tff(c_1596, plain, (![V_1413, Z_1419, X1_1425, U_178, Z_1416, X_1412, X_1426, X_181, Z_179, Z_1415, X_1418, U_1420, Y_1430, Y_1408, Y_182, X1_1422, X_1427, Y_1409, W_1428, X1_1429, X1_180, W_177, V_183, V_1417, V_1414, Y_1407, Z_1406, V_1410, X1_1424]: (skf21(V_1417, X_1427, Y_1407, Z_1415, X1_1424, W_177, U_178)=skf10(U_1420, W_177, U_178) | skf21(V_1417, X_1427, Y_1407, Z_1415, X1_1424, W_177, U_178)=skf21(V_1413, X_1418, Y_1408, Z_1406, X1_1429, W_177, U_178) | skf21(V_1413, X_1418, Y_1408, Z_1406, X1_1429, W_177, U_178)=skf10(U_1420, W_177, U_178) | skf21(V_1413, X_1418, Y_1408, Z_1406, X1_1429, W_177, U_178)=skf21(V_1410, X_1426, Y_1409, Z_1419, X1_1422, W_177, U_178) | skf21(V_1417, X_1427, Y_1407, Z_1415, X1_1424, W_177, U_178)=skf21(V_1410, X_1426, Y_1409, Z_1419, X1_1422, W_177, U_178) | skf21(V_1410, X_1426, Y_1409, Z_1419, X1_1422, W_177, U_178)=skf10(U_1420, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1410, X_1426, Y_1409, Z_1419, X1_1422, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1413, X_1418, Y_1408, Z_1406, X1_1429, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1417, X_1427, Y_1407, Z_1415, X1_1424, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1420, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1414, W_1428, X_1412, Y_1430, Z_1416, X1_1425)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_1420, W_177, U_178) | Z_1415=X1_1424 | Z_1415=Y_1407 | Y_1407=X1_1424 | Y_1407=X_1427 | Z_1415=X_1427 | X_1427=X1_1424 | X_1427=V_1417 | Y_1407=V_1417 | Z_1415=V_1417 | X1_1424=V_1417 | ~member(U_178, X1_1424, W_177) | ~member(U_178, Z_1415, W_177) | ~member(U_178, Y_1407, W_177) | ~member(U_178, X_1427, W_177) | ~member(U_178, V_1417, W_177) | Z_1406=X1_1429 | Z_1406=Y_1408 | Y_1408=X1_1429 | Y_1408=X_1418 | Z_1406=X_1418 | X_1418=X1_1429 | X_1418=V_1413 | Y_1408=V_1413 | Z_1406=V_1413 | X1_1429=V_1413 | ~member(U_178, X1_1429, W_177) | ~member(U_178, Z_1406, W_177) | ~member(U_178, Y_1408, W_177) | ~member(U_178, X_1418, W_177) | ~member(U_178, V_1413, W_177) | Z_1419=X1_1422 | Z_1419=Y_1409 | Y_1409=X1_1422 | Y_1409=X_1426 | Z_1419=X_1426 | X_1426=X1_1422 | X_1426=V_1410 | Y_1409=V_1410 | Z_1419=V_1410 | X1_1422=V_1410 | ~member(U_178, X1_1422, W_177) | ~member(U_178, Z_1419, W_177) | ~member(U_178, Y_1409, W_177) | ~member(U_178, X_1426, W_177) | ~member(U_178, V_1410, 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.55/18.13 tff(c_1626, plain, (![X_1529, Z_1556, Z_1542, Z_1545, W_211, V_210, Y_1538, X1_1530, V_1533, X1_1551, X_1557, V_1549, X1_1540, V_1531, Y_1532, Y_1552, X_1554, V_1550, Y_1544, X1_1546, Y_1555, Z_1543, X1_1553, W_1537, Z_1547, X_1536, U_209, X_1539, V_1534]: (skf21(V_1534, X_1539, Y_1544, Z_1542, X1_1546, V_210, W_211)=skf21(V_1531, X_1529, Y_1538, Z_1545, X1_1553, V_210, W_211) | skf21(V_1549, X_1557, Y_1552, Z_1556, X1_1540, V_210, W_211)=skf21(V_1534, X_1539, Y_1544, Z_1542, X1_1546, V_210, W_211) | skf21(V_1549, X_1557, Y_1552, Z_1556, X1_1540, V_210, W_211)=skf21(V_1531, X_1529, Y_1538, Z_1545, X1_1553, V_210, W_211) | skf21(V_1549, X_1557, Y_1552, Z_1556, X1_1540, V_210, W_211)=skf21(V_1533, X_1554, Y_1532, Z_1543, X1_1551, V_210, W_211) | skf21(V_1534, X_1539, Y_1544, Z_1542, X1_1546, V_210, W_211)=skf21(V_1533, X_1554, Y_1532, Z_1543, X1_1551, V_210, W_211) | skf21(V_1533, X_1554, Y_1532, Z_1543, X1_1551, V_210, W_211)=skf21(V_1531, X_1529, Y_1538, Z_1545, X1_1553, V_210, W_211) | skf21(V_1533, X_1554, Y_1532, Z_1543, X1_1551, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1549, X_1557, Y_1552, Z_1556, X1_1540, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1534, X_1539, Y_1544, Z_1542, X1_1546, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1531, X_1529, Y_1538, Z_1545, X1_1553, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1550, W_1537, X_1536, Y_1555, Z_1547, X1_1530)!=skf10(U_209, V_210, W_211) | Z_1545=X1_1553 | Z_1545=Y_1538 | Y_1538=X1_1553 | Y_1538=X_1529 | Z_1545=X_1529 | X_1529=X1_1553 | X_1529=V_1531 | Y_1538=V_1531 | Z_1545=V_1531 | X1_1553=V_1531 | ~member(W_211, X1_1553, V_210) | ~member(W_211, Z_1545, V_210) | ~member(W_211, Y_1538, V_210) | ~member(W_211, X_1529, V_210) | ~member(W_211, V_1531, V_210) | Z_1542=X1_1546 | Z_1542=Y_1544 | Y_1544=X1_1546 | Y_1544=X_1539 | Z_1542=X_1539 | X_1539=X1_1546 | X_1539=V_1534 | Y_1544=V_1534 | Z_1542=V_1534 | X1_1546=V_1534 | ~member(W_211, X1_1546, V_210) | ~member(W_211, Z_1542, V_210) | ~member(W_211, Y_1544, V_210) | ~member(W_211, X_1539, V_210) | ~member(W_211, V_1534, V_210) | Z_1556=X1_1540 | Z_1556=Y_1552 | Y_1552=X1_1540 | Y_1552=X_1557 | Z_1556=X_1557 | X_1557=X1_1540 | X_1557=V_1549 | Y_1552=V_1549 | Z_1556=V_1549 | X1_1540=V_1549 | ~member(W_211, X1_1540, V_210) | ~member(W_211, Z_1556, V_210) | ~member(W_211, Y_1552, V_210) | ~member(W_211, X_1557, V_210) | ~member(W_211, V_1549, V_210) | Z_1543=X1_1551 | Z_1543=Y_1532 | Y_1532=X1_1551 | Y_1532=X_1554 | Z_1543=X_1554 | X_1554=X1_1551 | X_1554=V_1533 | Y_1532=V_1533 | Z_1543=V_1533 | X1_1551=V_1533 | five(W_211, V_210) | ~member(W_211, X1_1551, V_210) | ~member(W_211, Z_1543, V_210) | ~member(W_211, Y_1532, V_210) | ~member(W_211, X_1554, V_210) | ~member(W_211, V_1533, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.13 tff(c_1570, plain, (![Y_1360, W_1367, X_1371, U_178, Y_1381, X_181, X1_1363, Z_179, Z_1366, X1_1370, V_1378, X_1372, Y_182, Y_1374, V_1373, X1_1364, V_1361, Z_1365, Z_1379, X1_180, W_177, X1_1380, V_183, X_1377, X_1382, Y_1376, Z_1369, U_1359]: (skf21(V_1378, X_1372, Y_1374, Z_1366, X1_1364, W_177, U_178)=skf21(V_1373, X_1382, Y_1376, Z_1379, X1_1363, W_177, U_178) | skf21(V_1373, X_1382, Y_1376, Z_1379, X1_1363, W_177, U_178)=skf21(V_1361, X_1377, Y_1360, Z_1365, X1_1370, W_177, U_178) | skf21(V_1378, X_1372, Y_1374, Z_1366, X1_1364, W_177, U_178)=skf21(V_1361, X_1377, Y_1360, Z_1365, X1_1370, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1361, X_1377, Y_1360, Z_1365, X1_1370, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1373, X_1382, Y_1376, Z_1379, X1_1363, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1378, X_1372, Y_1374, Z_1366, X1_1364, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1359 | skf21(V_1361, X_1377, Y_1360, Z_1365, X1_1370, W_177, U_178)=U_1359 | skf21(V_1373, X_1382, Y_1376, Z_1379, X1_1363, W_177, U_178)=U_1359 | skf21(V_1378, X_1372, Y_1374, Z_1366, X1_1364, W_177, U_178)=U_1359 | ~member(U_178, U_1359, W_177) | skf21(U_1359, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_1367, X_1371, Y_1381, Z_1369, X1_1380)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1366=X1_1364 | Z_1366=Y_1374 | Y_1374=X1_1364 | Y_1374=X_1372 | Z_1366=X_1372 | X_1372=X1_1364 | X_1372=V_1378 | Y_1374=V_1378 | Z_1366=V_1378 | X1_1364=V_1378 | ~member(U_178, X1_1364, W_177) | ~member(U_178, Z_1366, W_177) | ~member(U_178, Y_1374, W_177) | ~member(U_178, X_1372, W_177) | ~member(U_178, V_1378, W_177) | Z_1379=X1_1363 | Z_1379=Y_1376 | Y_1376=X1_1363 | Y_1376=X_1382 | Z_1379=X_1382 | X_1382=X1_1363 | X_1382=V_1373 | Y_1376=V_1373 | Z_1379=V_1373 | X1_1363=V_1373 | ~member(U_178, X1_1363, W_177) | ~member(U_178, Z_1379, W_177) | ~member(U_178, Y_1376, W_177) | ~member(U_178, X_1382, W_177) | ~member(U_178, V_1373, W_177) | Z_1365=X1_1370 | Z_1365=Y_1360 | Y_1360=X1_1370 | Y_1360=X_1377 | Z_1365=X_1377 | X_1377=X1_1370 | X_1377=V_1361 | Y_1360=V_1361 | Z_1365=V_1361 | X1_1370=V_1361 | ~member(U_178, X1_1370, W_177) | ~member(U_178, Z_1365, W_177) | ~member(U_178, Y_1360, W_177) | ~member(U_178, X_1377, W_177) | ~member(U_178, V_1361, 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.55/18.13 tff(c_1545, plain, (![V_1339, X_1358, X1_1346, W_1356, Y_1338, V_1347, U_178, X_181, Z_179, X_1357, X1_1336, Z_1343, V_1340, U_1335, Y_1337, X1_1352, Y_182, Z_1350, X_1341, X1_1348, Z_1353, V_1342, Z_1354, X1_180, Y_1334, W_177, V_183, X_1355, Y_1345]: (skf21(V_1342, X_1341, Y_1337, Z_1343, X1_1336, W_177, U_178)=skf21(V_1339, X_1358, Y_1345, Z_1353, X1_1348, W_177, U_178) | skf21(V_1342, X_1341, Y_1337, Z_1343, X1_1336, W_177, U_178)=skf21(V_1340, X_1355, Y_1338, Z_1350, X1_1352, W_177, U_178) | skf21(V_1340, X_1355, Y_1338, Z_1350, X1_1352, W_177, U_178)=skf21(V_1339, X_1358, Y_1345, Z_1353, X1_1348, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1340, X_1355, Y_1338, Z_1350, X1_1352, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1342, X_1341, Y_1337, Z_1343, X1_1336, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1339, X_1358, Y_1345, Z_1353, X1_1348, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1335 | skf21(V_1340, X_1355, Y_1338, Z_1350, X1_1352, W_177, U_178)=U_1335 | skf21(V_1342, X_1341, Y_1337, Z_1343, X1_1336, W_177, U_178)=U_1335 | skf21(V_1339, X_1358, Y_1345, Z_1353, X1_1348, W_177, U_178)=U_1335 | ~member(U_178, U_1335, W_177) | skf21(U_1335, V_1347, W_1356, X_1357, Y_1334, Z_1354, X1_1346)!=U_1335 | Z_1353=X1_1348 | Z_1353=Y_1345 | Y_1345=X1_1348 | Y_1345=X_1358 | Z_1353=X_1358 | X_1358=X1_1348 | X_1358=V_1339 | Y_1345=V_1339 | Z_1353=V_1339 | X1_1348=V_1339 | ~member(U_178, X1_1348, W_177) | ~member(U_178, Z_1353, W_177) | ~member(U_178, Y_1345, W_177) | ~member(U_178, X_1358, W_177) | ~member(U_178, V_1339, W_177) | Z_1343=X1_1336 | Z_1343=Y_1337 | Y_1337=X1_1336 | Y_1337=X_1341 | Z_1343=X_1341 | X_1341=X1_1336 | X_1341=V_1342 | Y_1337=V_1342 | Z_1343=V_1342 | X1_1336=V_1342 | ~member(U_178, X1_1336, W_177) | ~member(U_178, Z_1343, W_177) | ~member(U_178, Y_1337, W_177) | ~member(U_178, X_1341, W_177) | ~member(U_178, V_1342, W_177) | Z_1350=X1_1352 | Z_1350=Y_1338 | Y_1338=X1_1352 | Y_1338=X_1355 | Z_1350=X_1355 | X_1355=X1_1352 | X_1355=V_1340 | Y_1338=V_1340 | Z_1350=V_1340 | X1_1352=V_1340 | ~member(U_178, X1_1352, W_177) | ~member(U_178, Z_1350, W_177) | ~member(U_178, Y_1338, W_177) | ~member(U_178, X_1355, W_177) | ~member(U_178, V_1340, 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.55/18.13 tff(c_1515, plain, (![U_1215, V_1219, U_178, X_1229, Z_1212, X_181, Z_179, X_1223, Z_1221, X_1217, Z_1220, Y_1232, Y_1214, Y_182, Y_1213, X1_1226, V_1222, X1_180, W_177, V_183, W_1230, U_1224, V_1218, X1_1228, X1_1231]: (skf21(V_1222, X_1229, Y_1213, Z_1220, X1_1226, W_177, U_178)=skf10(U_1224, W_177, U_178) | skf21(V_1222, X_1229, Y_1213, Z_1220, X1_1226, W_177, U_178)=skf21(V_1218, X_1223, Y_1214, Z_1212, X1_1231, W_177, U_178) | skf21(V_1218, X_1223, Y_1214, Z_1212, X1_1231, W_177, U_178)=skf10(U_1224, W_177, U_178) | skf21(V_1218, X_1223, Y_1214, Z_1212, X1_1231, W_177, U_178)=skf10(U_1215, W_177, U_178) | skf21(V_1222, X_1229, Y_1213, Z_1220, X1_1226, W_177, U_178)=skf10(U_1215, W_177, U_178) | skf10(U_1224, W_177, U_178)=skf10(U_1215, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1215, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1218, X_1223, Y_1214, Z_1212, X1_1231, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1222, X_1229, Y_1213, Z_1220, X1_1226, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1224, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_1219, W_1230, X_1217, Y_1232, Z_1221, X1_1228)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_1224, W_177, U_178) | Z_1220=X1_1226 | Z_1220=Y_1213 | Y_1213=X1_1226 | Y_1213=X_1229 | Z_1220=X_1229 | X_1229=X1_1226 | X_1229=V_1222 | Y_1213=V_1222 | Z_1220=V_1222 | X1_1226=V_1222 | ~member(U_178, X1_1226, W_177) | ~member(U_178, Z_1220, W_177) | ~member(U_178, Y_1213, W_177) | ~member(U_178, X_1229, W_177) | ~member(U_178, V_1222, W_177) | Z_1212=X1_1231 | Z_1212=Y_1214 | Y_1214=X1_1231 | Y_1214=X_1223 | Z_1212=X_1223 | X_1223=X1_1231 | X_1223=V_1218 | Y_1214=V_1218 | Z_1212=V_1218 | X1_1231=V_1218 | ~member(U_178, X1_1231, W_177) | ~member(U_178, Z_1212, W_177) | ~member(U_178, Y_1214, W_177) | ~member(U_178, X_1223, W_177) | ~member(U_178, V_1218, W_177) | ssSkP0(U_1215, 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.55/18.13 tff(c_1597, plain, (![V_1413, Z_1419, W_211, V_210, X1_1425, Z_1416, X_1412, X_1426, Z_1415, X_1418, U_1420, Y_1430, Y_1408, X1_1422, X_1427, Y_1409, W_1428, X1_1429, V_1417, U_209, V_1414, Y_1407, Z_1406, V_1410, X1_1424]: (skf21(V_1417, X_1427, Y_1407, Z_1415, X1_1424, V_210, W_211)=skf10(U_1420, V_210, W_211) | skf21(V_1417, X_1427, Y_1407, Z_1415, X1_1424, V_210, W_211)=skf21(V_1413, X_1418, Y_1408, Z_1406, X1_1429, V_210, W_211) | skf21(V_1413, X_1418, Y_1408, Z_1406, X1_1429, V_210, W_211)=skf10(U_1420, V_210, W_211) | skf21(V_1413, X_1418, Y_1408, Z_1406, X1_1429, V_210, W_211)=skf21(V_1410, X_1426, Y_1409, Z_1419, X1_1422, V_210, W_211) | skf21(V_1417, X_1427, Y_1407, Z_1415, X1_1424, V_210, W_211)=skf21(V_1410, X_1426, Y_1409, Z_1419, X1_1422, V_210, W_211) | skf21(V_1410, X_1426, Y_1409, Z_1419, X1_1422, V_210, W_211)=skf10(U_1420, V_210, W_211) | skf21(V_1410, X_1426, Y_1409, Z_1419, X1_1422, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1413, X_1418, Y_1408, Z_1406, X1_1429, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1417, X_1427, Y_1407, Z_1415, X1_1424, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1420, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1414, W_1428, X_1412, Y_1430, Z_1416, X1_1425)!=skf10(U_209, V_210, W_211) | ssSkP0(U_1420, V_210, W_211) | Z_1415=X1_1424 | Z_1415=Y_1407 | Y_1407=X1_1424 | Y_1407=X_1427 | Z_1415=X_1427 | X_1427=X1_1424 | X_1427=V_1417 | Y_1407=V_1417 | Z_1415=V_1417 | X1_1424=V_1417 | ~member(W_211, X1_1424, V_210) | ~member(W_211, Z_1415, V_210) | ~member(W_211, Y_1407, V_210) | ~member(W_211, X_1427, V_210) | ~member(W_211, V_1417, V_210) | Z_1406=X1_1429 | Z_1406=Y_1408 | Y_1408=X1_1429 | Y_1408=X_1418 | Z_1406=X_1418 | X_1418=X1_1429 | X_1418=V_1413 | Y_1408=V_1413 | Z_1406=V_1413 | X1_1429=V_1413 | ~member(W_211, X1_1429, V_210) | ~member(W_211, Z_1406, V_210) | ~member(W_211, Y_1408, V_210) | ~member(W_211, X_1418, V_210) | ~member(W_211, V_1413, V_210) | Z_1419=X1_1422 | Z_1419=Y_1409 | Y_1409=X1_1422 | Y_1409=X_1426 | Z_1419=X_1426 | X_1426=X1_1422 | X_1426=V_1410 | Y_1409=V_1410 | Z_1419=V_1410 | X1_1422=V_1410 | five(W_211, V_210) | ~member(W_211, X1_1422, V_210) | ~member(W_211, Z_1419, V_210) | ~member(W_211, Y_1409, V_210) | ~member(W_211, X_1426, V_210) | ~member(W_211, V_1410, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.13 tff(c_1488, plain, (![X_1168, X1_1167, Z_1165, U_178, Y_1155, X_1171, V_1157, Z_1161, X_181, Z_179, W_1172, X_1170, V_1156, Y_182, X1_1164, U_1162, Y_1174, Z_1173, Y_1163, X1_180, W_177, V_183, X1_1160, U_1169]: (skf21(V_1157, X_1171, Y_1174, Z_1165, X1_1164, W_177, U_178)=skf10(U_1162, W_177, U_178) | skf21(V_1156, X_1170, Y_1155, Z_1161, X1_1167, W_177, U_178)=skf10(U_1162, W_177, U_178) | skf21(V_1157, X_1171, Y_1174, Z_1165, X1_1164, W_177, U_178)=skf21(V_1156, X_1170, Y_1155, Z_1161, X1_1167, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1156, X_1170, Y_1155, Z_1161, X1_1167, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1162, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1157, X_1171, Y_1174, Z_1165, X1_1164, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1169 | skf21(V_1156, X_1170, Y_1155, Z_1161, X1_1167, W_177, U_178)=U_1169 | skf10(U_1162, W_177, U_178)=U_1169 | skf21(V_1157, X_1171, Y_1174, Z_1165, X1_1164, W_177, U_178)=U_1169 | ~member(U_178, U_1169, W_177) | skf21(U_1169, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_1172, X_1168, Y_1163, Z_1173, X1_1160)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1165=X1_1164 | Z_1165=Y_1174 | Y_1174=X1_1164 | Y_1174=X_1171 | Z_1165=X_1171 | X_1171=X1_1164 | X_1171=V_1157 | Y_1174=V_1157 | Z_1165=V_1157 | X1_1164=V_1157 | ~member(U_178, X1_1164, W_177) | ~member(U_178, Z_1165, W_177) | ~member(U_178, Y_1174, W_177) | ~member(U_178, X_1171, W_177) | ~member(U_178, V_1157, W_177) | ssSkP0(U_1162, W_177, U_178) | Z_1161=X1_1167 | Z_1161=Y_1155 | Y_1155=X1_1167 | Y_1155=X_1170 | Z_1161=X_1170 | X_1170=X1_1167 | X_1170=V_1156 | Y_1155=V_1156 | Z_1161=V_1156 | X1_1167=V_1156 | ~member(U_178, X1_1167, W_177) | ~member(U_178, Z_1161, W_177) | ~member(U_178, Y_1155, W_177) | ~member(U_178, X_1170, W_177) | ~member(U_178, V_1156, 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.55/18.13 tff(c_1571, plain, (![Y_1360, W_211, W_1367, X_1371, V_210, Y_1381, X1_1363, Z_1366, X1_1370, V_1378, X_1372, Y_1374, V_1373, X1_1364, V_1361, Z_1365, Z_1379, X1_1380, X_1377, X_1382, Y_1376, U_209, Z_1369, U_1359]: (skf21(V_1378, X_1372, Y_1374, Z_1366, X1_1364, V_210, W_211)=skf21(V_1373, X_1382, Y_1376, Z_1379, X1_1363, V_210, W_211) | skf21(V_1373, X_1382, Y_1376, Z_1379, X1_1363, V_210, W_211)=skf21(V_1361, X_1377, Y_1360, Z_1365, X1_1370, V_210, W_211) | skf21(V_1378, X_1372, Y_1374, Z_1366, X1_1364, V_210, W_211)=skf21(V_1361, X_1377, Y_1360, Z_1365, X1_1370, V_210, W_211) | skf21(V_1361, X_1377, Y_1360, Z_1365, X1_1370, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1373, X_1382, Y_1376, Z_1379, X1_1363, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1378, X_1372, Y_1374, Z_1366, X1_1364, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1359 | skf21(V_1361, X_1377, Y_1360, Z_1365, X1_1370, V_210, W_211)=U_1359 | skf21(V_1373, X_1382, Y_1376, Z_1379, X1_1363, V_210, W_211)=U_1359 | skf21(V_1378, X_1372, Y_1374, Z_1366, X1_1364, V_210, W_211)=U_1359 | ~member(W_211, U_1359, V_210) | skf21(U_1359, skf10(U_209, V_210, W_211), W_1367, X_1371, Y_1381, Z_1369, X1_1380)!=skf10(U_209, V_210, W_211) | Z_1366=X1_1364 | Z_1366=Y_1374 | Y_1374=X1_1364 | Y_1374=X_1372 | Z_1366=X_1372 | X_1372=X1_1364 | X_1372=V_1378 | Y_1374=V_1378 | Z_1366=V_1378 | X1_1364=V_1378 | ~member(W_211, X1_1364, V_210) | ~member(W_211, Z_1366, V_210) | ~member(W_211, Y_1374, V_210) | ~member(W_211, X_1372, V_210) | ~member(W_211, V_1378, V_210) | Z_1379=X1_1363 | Z_1379=Y_1376 | Y_1376=X1_1363 | Y_1376=X_1382 | Z_1379=X_1382 | X_1382=X1_1363 | X_1382=V_1373 | Y_1376=V_1373 | Z_1379=V_1373 | X1_1363=V_1373 | ~member(W_211, X1_1363, V_210) | ~member(W_211, Z_1379, V_210) | ~member(W_211, Y_1376, V_210) | ~member(W_211, X_1382, V_210) | ~member(W_211, V_1373, V_210) | Z_1365=X1_1370 | Z_1365=Y_1360 | Y_1360=X1_1370 | Y_1360=X_1377 | Z_1365=X_1377 | X_1377=X1_1370 | X_1377=V_1361 | Y_1360=V_1361 | Z_1365=V_1361 | X1_1370=V_1361 | five(W_211, V_210) | ~member(W_211, X1_1370, V_210) | ~member(W_211, Z_1365, V_210) | ~member(W_211, Y_1360, V_210) | ~member(W_211, X_1377, V_210) | ~member(W_211, V_1361, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.13 tff(c_1463, plain, (![X_1150, U_1153, V_1139, X1_1148, U_178, U_1146, Y_1136, X_181, Z_179, V_1144, V_1149, X_1134, Y_1143, X1_1154, Y_182, Z_1145, Z_1151, Z_1137, X1_180, W_177, V_183, Y_1141, X1_1152, W_1140, X_1135]: (skf21(V_1144, X_1135, Y_1143, Z_1151, X1_1154, W_177, U_178)=skf10(U_1153, W_177, U_178) | skf21(V_1144, X_1135, Y_1143, Z_1151, X1_1154, W_177, U_178)=skf21(V_1139, X_1150, Y_1136, Z_1145, X1_1148, W_177, U_178) | skf21(V_1139, X_1150, Y_1136, Z_1145, X1_1148, W_177, U_178)=skf10(U_1153, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1139, X_1150, Y_1136, Z_1145, X1_1148, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1144, X_1135, Y_1143, Z_1151, X1_1154, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_1153, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1146 | skf21(V_1139, X_1150, Y_1136, Z_1145, X1_1148, W_177, U_178)=U_1146 | skf21(V_1144, X_1135, Y_1143, Z_1151, X1_1154, W_177, U_178)=U_1146 | skf10(U_1153, W_177, U_178)=U_1146 | ~member(U_178, U_1146, W_177) | skf21(U_1146, V_1149, W_1140, X_1134, Y_1141, Z_1137, X1_1152)!=U_1146 | ssSkP0(U_1153, W_177, U_178) | Z_1151=X1_1154 | Z_1151=Y_1143 | Y_1143=X1_1154 | Y_1143=X_1135 | Z_1151=X_1135 | X_1135=X1_1154 | X_1135=V_1144 | Y_1143=V_1144 | Z_1151=V_1144 | X1_1154=V_1144 | ~member(U_178, X1_1154, W_177) | ~member(U_178, Z_1151, W_177) | ~member(U_178, Y_1143, W_177) | ~member(U_178, X_1135, W_177) | ~member(U_178, V_1144, W_177) | Z_1145=X1_1148 | Z_1145=Y_1136 | Y_1136=X1_1148 | Y_1136=X_1150 | Z_1145=X_1150 | X_1150=X1_1148 | X_1150=V_1139 | Y_1136=V_1139 | Z_1145=V_1139 | X1_1148=V_1139 | ~member(U_178, X1_1148, W_177) | ~member(U_178, Z_1145, W_177) | ~member(U_178, Y_1136, W_177) | ~member(U_178, X_1150, W_177) | ~member(U_178, V_1139, 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.55/18.13 tff(c_1438, plain, (![X_1128, U_178, X1_1119, V_1117, Z_1132, X_181, Z_179, X_1130, X1_1129, Y_182, Y_1120, Z_1123, Z_1126, X_1115, X1_1122, Y_1116, X1_180, V_1131, W_177, V_183, V_1125, U_1118, Y_1124]: (skf21(V_1131, X_1128, Y_1120, Z_1123, X1_1122, W_177, U_178)=skf21(V_1117, X_1130, Y_1116, Z_1126, X1_1129, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1117, X_1130, Y_1116, Z_1126, X1_1129, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1131, X_1128, Y_1120, Z_1123, X1_1122, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_1125 | skf21(V_1117, X_1130, Y_1116, Z_1126, X1_1129, W_177, U_178)=V_1125 | skf21(V_1131, X_1128, Y_1120, Z_1123, X1_1122, W_177, U_178)=V_1125 | V_1125=U_1118 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1118 | skf21(V_1117, X_1130, Y_1116, Z_1126, X1_1129, W_177, U_178)=U_1118 | skf21(V_1131, X_1128, Y_1120, Z_1123, X1_1122, W_177, U_178)=U_1118 | ~member(U_178, V_1125, W_177) | ~member(U_178, U_1118, W_177) | skf21(U_1118, V_1125, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_1115, Y_1124, Z_1132, X1_1119)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_1123=X1_1122 | Z_1123=Y_1120 | Y_1120=X1_1122 | Y_1120=X_1128 | Z_1123=X_1128 | X_1128=X1_1122 | X_1128=V_1131 | Y_1120=V_1131 | Z_1123=V_1131 | X1_1122=V_1131 | ~member(U_178, X1_1122, W_177) | ~member(U_178, Z_1123, W_177) | ~member(U_178, Y_1120, W_177) | ~member(U_178, X_1128, W_177) | ~member(U_178, V_1131, W_177) | Z_1126=X1_1129 | Z_1126=Y_1116 | Y_1116=X1_1129 | Y_1116=X_1130 | Z_1126=X_1130 | X_1130=X1_1129 | X_1130=V_1117 | Y_1116=V_1117 | Z_1126=V_1117 | X1_1129=V_1117 | ~member(U_178, X1_1129, W_177) | ~member(U_178, Z_1126, W_177) | ~member(U_178, Y_1116, W_177) | ~member(U_178, X_1130, W_177) | ~member(U_178, V_1117, 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.55/18.13 tff(c_1413, plain, (![Z_1105, U_1110, V_1113, U_178, Z_1099, X_181, Z_179, W_1106, V_1096, Y_182, X_1101, X_1112, Z_1098, X1_1111, X1_180, W_177, V_183, V_1114, Y_1100, X1_1109, Y_1095, Y_1104, X_1103, X1_1102]: (skf21(V_1114, X_1101, Y_1100, Z_1098, X1_1111, W_177, U_178)=skf21(V_1096, X_1112, Y_1095, Z_1105, X1_1109, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1096, X_1112, Y_1095, Z_1105, X1_1109, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1114, X_1101, Y_1100, Z_1098, X1_1111, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_1113 | skf21(V_1096, X_1112, Y_1095, Z_1105, X1_1109, W_177, U_178)=V_1113 | skf21(V_1114, X_1101, Y_1100, Z_1098, X1_1111, W_177, U_178)=V_1113 | V_1113=U_1110 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1110 | skf21(V_1096, X_1112, Y_1095, Z_1105, X1_1109, W_177, U_178)=U_1110 | skf21(V_1114, X_1101, Y_1100, Z_1098, X1_1111, W_177, U_178)=U_1110 | ~member(U_178, V_1113, W_177) | ~member(U_178, U_1110, W_177) | skf21(U_1110, V_1113, W_1106, X_1103, Y_1104, Z_1099, X1_1102)!=V_1113 | Z_1098=X1_1111 | Z_1098=Y_1100 | Y_1100=X1_1111 | Y_1100=X_1101 | Z_1098=X_1101 | X_1101=X1_1111 | X_1101=V_1114 | Y_1100=V_1114 | Z_1098=V_1114 | X1_1111=V_1114 | ~member(U_178, X1_1111, W_177) | ~member(U_178, Z_1098, W_177) | ~member(U_178, Y_1100, W_177) | ~member(U_178, X_1101, W_177) | ~member(U_178, V_1114, W_177) | Z_1105=X1_1109 | Z_1105=Y_1095 | Y_1095=X1_1109 | Y_1095=X_1112 | Z_1105=X_1112 | X_1112=X1_1109 | X_1112=V_1096 | Y_1095=V_1096 | Z_1105=V_1096 | X1_1109=V_1096 | ~member(U_178, X1_1109, W_177) | ~member(U_178, Z_1105, W_177) | ~member(U_178, Y_1095, W_177) | ~member(U_178, X_1112, W_177) | ~member(U_178, V_1096, 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.55/18.13 tff(c_1386, plain, (![X1_1055, U_178, X_1057, V_1058, X_181, Z_179, X4_1046, U_1052, X_1041, Y_182, X_1059, Y_1040, W_1048, Z_1051, Y_1056, X1_180, W_177, Z_1047, V_1042, V_183, Z_1060, V_1050, X1_1054, Y_1049, X1_1043]: (skf21(V_1050, X_1057, Y_1056, Z_1060, X1_1043, W_177, U_178)=skf21(V_1042, X_1059, Y_1040, Z_1047, X1_1054, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1042, X_1059, Y_1040, Z_1047, X1_1054, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf21(V_1050, X_1057, Y_1056, Z_1060, X1_1043, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_1046 | skf21(V_1042, X_1059, Y_1040, Z_1047, X1_1054, W_177, U_178)=X4_1046 | skf21(V_1050, X_1057, Y_1056, Z_1060, X1_1043, W_177, U_178)=X4_1046 | X4_1046=U_1052 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_1052 | skf21(V_1042, X_1059, Y_1040, Z_1047, X1_1054, W_177, U_178)=U_1052 | skf21(V_1050, X_1057, Y_1056, Z_1060, X1_1043, W_177, U_178)=U_1052 | ~member(U_178, X4_1046, W_177) | ~member(U_178, U_1052, W_177) | skf21(U_1052, V_1058, W_1048, X_1041, Y_1049, Z_1051, X1_1055)!=U_1052 | Z_1060=X1_1043 | Z_1060=Y_1056 | Y_1056=X1_1043 | Y_1056=X_1057 | Z_1060=X_1057 | X_1057=X1_1043 | X_1057=V_1050 | Y_1056=V_1050 | Z_1060=V_1050 | X1_1043=V_1050 | ~member(U_178, X1_1043, W_177) | ~member(U_178, Z_1060, W_177) | ~member(U_178, Y_1056, W_177) | ~member(U_178, X_1057, W_177) | ~member(U_178, V_1050, W_177) | Z_1047=X1_1054 | Z_1047=Y_1040 | Y_1040=X1_1054 | Y_1040=X_1059 | Z_1047=X_1059 | X_1059=X1_1054 | X_1059=V_1042 | Y_1040=V_1042 | Z_1047=V_1042 | X1_1054=V_1042 | ~member(U_178, X1_1054, W_177) | ~member(U_178, Z_1047, W_177) | ~member(U_178, Y_1040, W_177) | ~member(U_178, X_1059, W_177) | ~member(U_178, V_1042, 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.55/18.13 tff(c_1358, plain, (![V_978, X_981, U_991, U_178, W_992, X_181, Z_179, Y_977, Z_987, U_979, Y_182, X1_989, Y_983, V_976, X_990, X1_180, W_177, U_986, V_183, X1_982, Z_984]: (skf10(U_991, W_177, U_178)=skf10(U_986, W_177, U_178) | skf10(U_991, W_177, U_178)=skf10(U_979, W_177, U_178) | skf10(U_986, W_177, U_178)=skf10(U_979, W_177, U_178) | skf21(V_978, X_990, Y_977, Z_987, X1_989, W_177, U_178)=skf10(U_979, W_177, U_178) | skf21(V_978, X_990, Y_977, Z_987, X1_989, W_177, U_178)=skf10(U_991, W_177, U_178) | skf21(V_978, X_990, Y_977, Z_987, X1_989, W_177, U_178)=skf10(U_986, W_177, U_178) | skf21(V_978, X_990, Y_977, Z_987, X1_989, 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_979, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_991, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_986, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_976, W_992, X_981, Y_983, Z_984, X1_982)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_986, W_177, U_178) | ssSkP0(U_991, W_177, U_178) | ssSkP0(U_979, W_177, U_178) | Z_987=X1_989 | Z_987=Y_977 | Y_977=X1_989 | Y_977=X_990 | Z_987=X_990 | X_990=X1_989 | X_990=V_978 | Y_977=V_978 | Z_987=V_978 | X1_989=V_978 | ~member(U_178, X1_989, W_177) | ~member(U_178, Z_987, W_177) | ~member(U_178, Y_977, W_177) | ~member(U_178, X_990, W_177) | ~member(U_178, V_978, 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.55/18.13 tff(c_1516, plain, (![U_1215, V_1219, W_211, V_210, X_1229, Z_1212, X_1223, Z_1221, X_1217, Z_1220, Y_1232, Y_1214, Y_1213, X1_1226, V_1222, W_1230, U_1224, V_1218, X1_1228, U_209, X1_1231]: (skf21(V_1222, X_1229, Y_1213, Z_1220, X1_1226, V_210, W_211)=skf10(U_1224, V_210, W_211) | skf21(V_1222, X_1229, Y_1213, Z_1220, X1_1226, V_210, W_211)=skf21(V_1218, X_1223, Y_1214, Z_1212, X1_1231, V_210, W_211) | skf21(V_1218, X_1223, Y_1214, Z_1212, X1_1231, V_210, W_211)=skf10(U_1224, V_210, W_211) | skf21(V_1218, X_1223, Y_1214, Z_1212, X1_1231, V_210, W_211)=skf10(U_1215, V_210, W_211) | skf21(V_1222, X_1229, Y_1213, Z_1220, X1_1226, V_210, W_211)=skf10(U_1215, V_210, W_211) | skf10(U_1224, V_210, W_211)=skf10(U_1215, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1215, V_210, W_211) | skf21(V_1218, X_1223, Y_1214, Z_1212, X1_1231, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1222, X_1229, Y_1213, Z_1220, X1_1226, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1224, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_1219, W_1230, X_1217, Y_1232, Z_1221, X1_1228)!=skf10(U_209, V_210, W_211) | ssSkP0(U_1224, V_210, W_211) | Z_1220=X1_1226 | Z_1220=Y_1213 | Y_1213=X1_1226 | Y_1213=X_1229 | Z_1220=X_1229 | X_1229=X1_1226 | X_1229=V_1222 | Y_1213=V_1222 | Z_1220=V_1222 | X1_1226=V_1222 | ~member(W_211, X1_1226, V_210) | ~member(W_211, Z_1220, V_210) | ~member(W_211, Y_1213, V_210) | ~member(W_211, X_1229, V_210) | ~member(W_211, V_1222, V_210) | Z_1212=X1_1231 | Z_1212=Y_1214 | Y_1214=X1_1231 | Y_1214=X_1223 | Z_1212=X_1223 | X_1223=X1_1231 | X_1223=V_1218 | Y_1214=V_1218 | Z_1212=V_1218 | X1_1231=V_1218 | five(W_211, V_210) | ~member(W_211, X1_1231, V_210) | ~member(W_211, Z_1212, V_210) | ~member(W_211, Y_1214, V_210) | ~member(W_211, X_1223, V_210) | ~member(W_211, V_1218, V_210) | ssSkP0(U_1215, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.13 tff(c_1306, plain, (![Y_929, U_924, U_178, Z_928, X_926, X_181, Z_179, Z_922, W_927, Y_182, V_915, U_919, X1_921, X1_918, X1_180, W_177, V_183, Y_920, X_923, U_914]: (skf21(V_915, X_926, Y_929, Z_922, X1_921, W_177, U_178)=skf10(U_919, W_177, U_178) | skf10(U_919, W_177, U_178)=skf10(U_914, W_177, U_178) | skf21(V_915, X_926, Y_929, Z_922, X1_921, W_177, U_178)=skf10(U_914, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_914, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_919, W_177, U_178) | skf21(V_915, X_926, Y_929, Z_922, X1_921, W_177, U_178)=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_924 | skf10(U_914, W_177, U_178)=U_924 | skf10(U_919, W_177, U_178)=U_924 | skf21(V_915, X_926, Y_929, Z_922, X1_921, W_177, U_178)=U_924 | ~member(U_178, U_924, W_177) | skf21(U_924, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_927, X_923, Y_920, Z_928, X1_918)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_922=X1_921 | Z_922=Y_929 | Y_929=X1_921 | Y_929=X_926 | Z_922=X_926 | X_926=X1_921 | X_926=V_915 | Y_929=V_915 | Z_922=V_915 | X1_921=V_915 | ~member(U_178, X1_921, W_177) | ~member(U_178, Z_922, W_177) | ~member(U_178, Y_929, W_177) | ~member(U_178, X_926, W_177) | ~member(U_178, V_915, W_177) | ssSkP0(U_919, W_177, U_178) | ssSkP0(U_914, 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.55/18.13 tff(c_1489, plain, (![X_1168, X1_1167, Z_1165, W_211, V_210, Y_1155, X_1171, V_1157, Z_1161, W_1172, X_1170, V_1156, X1_1164, U_1162, Y_1174, Z_1173, Y_1163, U_209, X1_1160, U_1169]: (skf21(V_1157, X_1171, Y_1174, Z_1165, X1_1164, V_210, W_211)=skf10(U_1162, V_210, W_211) | skf21(V_1156, X_1170, Y_1155, Z_1161, X1_1167, V_210, W_211)=skf10(U_1162, V_210, W_211) | skf21(V_1157, X_1171, Y_1174, Z_1165, X1_1164, V_210, W_211)=skf21(V_1156, X_1170, Y_1155, Z_1161, X1_1167, V_210, W_211) | skf21(V_1156, X_1170, Y_1155, Z_1161, X1_1167, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1162, V_210, W_211) | skf21(V_1157, X_1171, Y_1174, Z_1165, X1_1164, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1169 | skf21(V_1156, X_1170, Y_1155, Z_1161, X1_1167, V_210, W_211)=U_1169 | skf10(U_1162, V_210, W_211)=U_1169 | skf21(V_1157, X_1171, Y_1174, Z_1165, X1_1164, V_210, W_211)=U_1169 | ~member(W_211, U_1169, V_210) | skf21(U_1169, skf10(U_209, V_210, W_211), W_1172, X_1168, Y_1163, Z_1173, X1_1160)!=skf10(U_209, V_210, W_211) | Z_1165=X1_1164 | Z_1165=Y_1174 | Y_1174=X1_1164 | Y_1174=X_1171 | Z_1165=X_1171 | X_1171=X1_1164 | X_1171=V_1157 | Y_1174=V_1157 | Z_1165=V_1157 | X1_1164=V_1157 | ~member(W_211, X1_1164, V_210) | ~member(W_211, Z_1165, V_210) | ~member(W_211, Y_1174, V_210) | ~member(W_211, X_1171, V_210) | ~member(W_211, V_1157, V_210) | ssSkP0(U_1162, V_210, W_211) | Z_1161=X1_1167 | Z_1161=Y_1155 | Y_1155=X1_1167 | Y_1155=X_1170 | Z_1161=X_1170 | X_1170=X1_1167 | X_1170=V_1156 | Y_1155=V_1156 | Z_1161=V_1156 | X1_1167=V_1156 | five(W_211, V_210) | ~member(W_211, X1_1167, V_210) | ~member(W_211, Z_1161, V_210) | ~member(W_211, Y_1155, V_210) | ~member(W_211, X_1170, V_210) | ~member(W_211, V_1156, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.13 tff(c_1230, plain, (![V_861, Z_865, X_862, U_178, U_854, X1_858, X_181, Z_179, X1_855, Y_182, V_864, U_853, Y_860, Z_859, X1_180, W_177, V_183, X_852, Y_856]: (skf21(V_864, X_862, Y_856, Z_859, X1_858, W_177, U_178)=skf10(U_853, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_853, W_177, U_178) | skf21(V_864, X_862, Y_856, Z_859, X1_858, 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_861 | skf10(U_853, W_177, U_178)=V_861 | skf21(V_864, X_862, Y_856, Z_859, X1_858, W_177, U_178)=V_861 | V_861=U_854 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_854 | skf10(U_853, W_177, U_178)=U_854 | skf21(V_864, X_862, Y_856, Z_859, X1_858, W_177, U_178)=U_854 | ~member(U_178, V_861, W_177) | ~member(U_178, U_854, W_177) | skf21(U_854, V_861, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_852, Y_860, Z_865, X1_855)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_859=X1_858 | Z_859=Y_856 | Y_856=X1_858 | Y_856=X_862 | Z_859=X_862 | X_862=X1_858 | X_862=V_864 | Y_856=V_864 | Z_859=V_864 | X1_858=V_864 | ~member(U_178, X1_858, W_177) | ~member(U_178, Z_859, W_177) | ~member(U_178, Y_856, W_177) | ~member(U_178, X_862, W_177) | ~member(U_178, V_864, W_177) | ssSkP0(U_853, 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.55/18.14 tff(c_1464, plain, (![X_1150, U_1153, V_1139, W_211, X1_1148, V_210, U_1146, Y_1136, V_1144, V_1149, X_1134, Y_1143, X1_1154, Z_1145, Z_1151, Z_1137, Y_1141, X1_1152, W_1140, U_209, X_1135]: (skf21(V_1144, X_1135, Y_1143, Z_1151, X1_1154, V_210, W_211)=skf10(U_1153, V_210, W_211) | skf21(V_1144, X_1135, Y_1143, Z_1151, X1_1154, V_210, W_211)=skf21(V_1139, X_1150, Y_1136, Z_1145, X1_1148, V_210, W_211) | skf21(V_1139, X_1150, Y_1136, Z_1145, X1_1148, V_210, W_211)=skf10(U_1153, V_210, W_211) | skf21(V_1139, X_1150, Y_1136, Z_1145, X1_1148, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1144, X_1135, Y_1143, Z_1151, X1_1154, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=skf10(U_1153, V_210, W_211) | skf10(U_209, V_210, W_211)=U_1146 | skf21(V_1139, X_1150, Y_1136, Z_1145, X1_1148, V_210, W_211)=U_1146 | skf21(V_1144, X_1135, Y_1143, Z_1151, X1_1154, V_210, W_211)=U_1146 | skf10(U_1153, V_210, W_211)=U_1146 | ~member(W_211, U_1146, V_210) | skf21(U_1146, V_1149, W_1140, X_1134, Y_1141, Z_1137, X1_1152)!=U_1146 | ssSkP0(U_1153, V_210, W_211) | Z_1151=X1_1154 | Z_1151=Y_1143 | Y_1143=X1_1154 | Y_1143=X_1135 | Z_1151=X_1135 | X_1135=X1_1154 | X_1135=V_1144 | Y_1143=V_1144 | Z_1151=V_1144 | X1_1154=V_1144 | ~member(W_211, X1_1154, V_210) | ~member(W_211, Z_1151, V_210) | ~member(W_211, Y_1143, V_210) | ~member(W_211, X_1135, V_210) | ~member(W_211, V_1144, V_210) | Z_1145=X1_1148 | Z_1145=Y_1136 | Y_1136=X1_1148 | Y_1136=X_1150 | Z_1145=X_1150 | X_1150=X1_1148 | X_1150=V_1139 | Y_1136=V_1139 | Z_1145=V_1139 | X1_1148=V_1139 | five(W_211, V_210) | ~member(W_211, X1_1148, V_210) | ~member(W_211, Z_1145, V_210) | ~member(W_211, Y_1136, V_210) | ~member(W_211, X_1150, V_210) | ~member(W_211, V_1139, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_1439, plain, (![X_1128, W_211, V_210, X1_1119, V_1117, Z_1132, X_1130, X1_1129, Y_1120, Z_1123, Z_1126, X_1115, X1_1122, Y_1116, V_1131, V_1125, U_209, U_1118, Y_1124]: (skf21(V_1131, X_1128, Y_1120, Z_1123, X1_1122, V_210, W_211)=skf21(V_1117, X_1130, Y_1116, Z_1126, X1_1129, V_210, W_211) | skf21(V_1117, X_1130, Y_1116, Z_1126, X1_1129, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_1131, X_1128, Y_1120, Z_1123, X1_1122, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_1125 | skf21(V_1117, X_1130, Y_1116, Z_1126, X1_1129, V_210, W_211)=V_1125 | skf21(V_1131, X_1128, Y_1120, Z_1123, X1_1122, V_210, W_211)=V_1125 | V_1125=U_1118 | skf10(U_209, V_210, W_211)=U_1118 | skf21(V_1117, X_1130, Y_1116, Z_1126, X1_1129, V_210, W_211)=U_1118 | skf21(V_1131, X_1128, Y_1120, Z_1123, X1_1122, V_210, W_211)=U_1118 | ~member(W_211, V_1125, V_210) | ~member(W_211, U_1118, V_210) | skf21(U_1118, V_1125, skf10(U_209, V_210, W_211), X_1115, Y_1124, Z_1132, X1_1119)!=skf10(U_209, V_210, W_211) | Z_1123=X1_1122 | Z_1123=Y_1120 | Y_1120=X1_1122 | Y_1120=X_1128 | Z_1123=X_1128 | X_1128=X1_1122 | X_1128=V_1131 | Y_1120=V_1131 | Z_1123=V_1131 | X1_1122=V_1131 | ~member(W_211, X1_1122, V_210) | ~member(W_211, Z_1123, V_210) | ~member(W_211, Y_1120, V_210) | ~member(W_211, X_1128, V_210) | ~member(W_211, V_1131, V_210) | Z_1126=X1_1129 | Z_1126=Y_1116 | Y_1116=X1_1129 | Y_1116=X_1130 | Z_1126=X_1130 | X_1130=X1_1129 | X_1130=V_1117 | Y_1116=V_1117 | Z_1126=V_1117 | X1_1129=V_1117 | five(W_211, V_210) | ~member(W_211, X1_1129, V_210) | ~member(W_211, Z_1126, V_210) | ~member(W_211, Y_1116, V_210) | ~member(W_211, X_1130, V_210) | ~member(W_211, V_1117, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_1044, plain, (![X1_740, X_735, Y_737, U_178, U_738, X_181, Z_179, V_734, Y_182, W_730, Z_733, X1_180, W_177, V_183, X1_741, Y_736, V_739, Z_742]: (skf21(V_734, X_735, Y_737, Z_733, X1_741, 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_730 | skf21(V_734, X_735, Y_737, Z_733, X1_741, W_177, U_178)=W_730 | W_730=V_739 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_739 | skf21(V_734, X_735, Y_737, Z_733, X1_741, W_177, U_178)=V_739 | V_739=U_738 | W_730=U_738 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_738 | skf21(V_734, X_735, Y_737, Z_733, X1_741, W_177, U_178)=U_738 | ~member(U_178, W_730, W_177) | ~member(U_178, V_739, W_177) | ~member(U_178, U_738, W_177) | skf21(U_738, V_739, W_730, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), Y_736, Z_742, X1_740)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | Z_733=X1_741 | Z_733=Y_737 | Y_737=X1_741 | Y_737=X_735 | Z_733=X_735 | X_735=X1_741 | X_735=V_734 | Y_737=V_734 | Z_733=V_734 | X1_741=V_734 | ~member(U_178, X1_741, W_177) | ~member(U_178, Z_733, W_177) | ~member(U_178, Y_737, W_177) | ~member(U_178, X_735, W_177) | ~member(U_178, V_734, 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.55/18.14 tff(c_1280, plain, (![U_895, U_884, X_891, V_898, U_178, Z_887, X_181, Z_179, W_893, X_889, Z_885, X1_890, Y_182, Y_892, X1_180, Y_888, X1_897, W_177, V_899, V_183]: (skf21(V_899, X_889, Y_888, Z_885, X1_897, W_177, U_178)=skf10(U_884, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_884, W_177, U_178) | skf21(V_899, X_889, Y_888, Z_885, X1_897, 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_898 | skf10(U_884, W_177, U_178)=V_898 | skf21(V_899, X_889, Y_888, Z_885, X1_897, W_177, U_178)=V_898 | V_898=U_895 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_895 | skf10(U_884, W_177, U_178)=U_895 | skf21(V_899, X_889, Y_888, Z_885, X1_897, W_177, U_178)=U_895 | ~member(U_178, V_898, W_177) | ~member(U_178, U_895, W_177) | skf21(U_895, V_898, W_893, X_891, Y_892, Z_887, X1_890)!=V_898 | Z_885=X1_897 | Z_885=Y_888 | Y_888=X1_897 | Y_888=X_889 | Z_885=X_889 | X_889=X1_897 | X_889=V_899 | Y_888=V_899 | Z_885=V_899 | X1_897=V_899 | ~member(U_178, X1_897, W_177) | ~member(U_178, Z_885, W_177) | ~member(U_178, Y_888, W_177) | ~member(U_178, X_889, W_177) | ~member(U_178, V_899, W_177) | ssSkP0(U_884, 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.55/18.14 tff(c_1255, plain, (![Z_876, W_883, U_178, X_181, Z_179, Y_867, U_879, Y_182, X1_878, X4_873, V_880, V_868, Z_870, X1_180, W_177, X_869, V_183, X1_875, X_881, Y_882, U_874]: (skf21(V_868, X_881, Y_867, Z_876, X1_878, W_177, U_178)=skf10(U_879, W_177, U_178) | skf21(V_868, X_881, Y_867, Z_876, X1_878, 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_879, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_873 | skf21(V_868, X_881, Y_867, Z_876, X1_878, W_177, U_178)=X4_873 | skf10(U_879, W_177, U_178)=X4_873 | X4_873=U_874 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_874 | skf21(V_868, X_881, Y_867, Z_876, X1_878, W_177, U_178)=U_874 | skf10(U_879, W_177, U_178)=U_874 | ~member(U_178, X4_873, W_177) | ~member(U_178, U_874, W_177) | skf21(U_874, V_880, W_883, X_869, Y_882, Z_870, X1_875)!=U_874 | ssSkP0(U_879, W_177, U_178) | Z_876=X1_878 | Z_876=Y_867 | Y_867=X1_878 | Y_867=X_881 | Z_876=X_881 | X_881=X1_878 | X_881=V_868 | Y_867=V_868 | Z_876=V_868 | X1_878=V_868 | ~member(U_178, X1_878, W_177) | ~member(U_178, Z_876, W_177) | ~member(U_178, Y_867, W_177) | ~member(U_178, X_881, W_177) | ~member(U_178, V_868, 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.55/18.14 tff(c_1203, plain, (![X_814, Z_820, Y_819, X1_825, U_178, X_181, W_815, Z_179, Z_816, Y_821, X_818, Y_182, X1_180, W_177, V_183, X1_824, V_817, U_823, V_812]: (skf21(V_817, X_818, Y_821, Z_816, X1_825, 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_815 | skf21(V_817, X_818, Y_821, Z_816, X1_825, W_177, U_178)=W_815 | W_815=V_812 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_812 | skf21(V_817, X_818, Y_821, Z_816, X1_825, W_177, U_178)=V_812 | V_812=U_823 | W_815=U_823 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_823 | skf21(V_817, X_818, Y_821, Z_816, X1_825, W_177, U_178)=U_823 | ~member(U_178, W_815, W_177) | ~member(U_178, V_812, W_177) | ~member(U_178, U_823, W_177) | skf21(U_823, V_812, W_815, X_814, Y_819, Z_820, X1_824)!=W_815 | Z_816=X1_825 | Z_816=Y_821 | Y_821=X1_825 | Y_821=X_818 | Z_816=X_818 | X_818=X1_825 | X_818=V_817 | Y_821=V_817 | Z_816=V_817 | X1_825=V_817 | ~member(U_178, X1_825, W_177) | ~member(U_178, Z_816, W_177) | ~member(U_178, Y_821, W_177) | ~member(U_178, X_818, W_177) | ~member(U_178, V_817, 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.55/18.14 tff(c_970, plain, (![V_661, Y_669, U_178, X_181, Z_179, V_668, X_662, Z_660, X_666, X4_663, U_671, Y_182, X1_670, Z_657, X1_665, W_667, Y_664, X1_180, W_177, V_183]: (skf21(V_661, X_662, Y_664, Z_660, X1_670, 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_663 | skf21(V_661, X_662, Y_664, Z_660, X1_670, W_177, U_178)=X4_663 | X4_663=V_668 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_668 | skf21(V_661, X_662, Y_664, Z_660, X1_670, W_177, U_178)=V_668 | V_668=U_671 | X4_663=U_671 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_671 | skf21(V_661, X_662, Y_664, Z_660, X1_670, W_177, U_178)=U_671 | ~member(U_178, X4_663, W_177) | ~member(U_178, V_668, W_177) | ~member(U_178, U_671, W_177) | skf21(U_671, V_668, W_667, X_666, Y_669, Z_657, X1_665)!=V_668 | Z_660=X1_670 | Z_660=Y_664 | Y_664=X1_670 | Y_664=X_662 | Z_660=X_662 | X_662=X1_670 | X_662=V_661 | Y_664=V_661 | Z_660=V_661 | X1_670=V_661 | ~member(U_178, X1_670, W_177) | ~member(U_178, Z_660, W_177) | ~member(U_178, Y_664, W_177) | ~member(U_178, X_662, W_177) | ~member(U_178, V_661, 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.55/18.14 tff(c_1152, plain, (![U_771, W_781, V_769, U_178, X_181, Z_179, U_778, Y_775, Y_182, U_780, X1_180, W_177, V_183, X_773, X1_774, U_770, Z_776]: (skf10(U_780, W_177, U_178)=skf10(U_778, W_177, U_178) | skf10(U_780, W_177, U_178)=skf10(U_771, W_177, U_178) | skf10(U_778, W_177, U_178)=skf10(U_771, W_177, U_178) | skf10(U_771, W_177, U_178)=skf10(U_770, W_177, U_178) | skf10(U_780, W_177, U_178)=skf10(U_770, W_177, U_178) | skf10(U_778, W_177, U_178)=skf10(U_770, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_770, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_771, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_780, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_778, W_177, U_178) | skf21(skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), V_769, W_781, X_773, Y_775, Z_776, X1_774)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_778, W_177, U_178) | ssSkP0(U_780, W_177, U_178) | ssSkP0(U_771, W_177, U_178) | ssSkP0(U_770, 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.55/18.14 tff(c_1359, plain, (![V_978, X_981, W_211, U_991, V_210, W_992, Y_977, Z_987, U_979, X1_989, Y_983, V_976, X_990, U_986, X1_982, U_209, Z_984]: (skf10(U_991, V_210, W_211)=skf10(U_986, V_210, W_211) | skf10(U_991, V_210, W_211)=skf10(U_979, V_210, W_211) | skf10(U_986, V_210, W_211)=skf10(U_979, V_210, W_211) | skf21(V_978, X_990, Y_977, Z_987, X1_989, V_210, W_211)=skf10(U_979, V_210, W_211) | skf21(V_978, X_990, Y_977, Z_987, X1_989, V_210, W_211)=skf10(U_991, V_210, W_211) | skf21(V_978, X_990, Y_977, Z_987, X1_989, V_210, W_211)=skf10(U_986, V_210, W_211) | skf21(V_978, X_990, Y_977, Z_987, X1_989, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_979, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_991, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_986, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(skf10(U_209, V_210, W_211), V_976, W_992, X_981, Y_983, Z_984, X1_982)!=skf10(U_209, V_210, W_211) | ssSkP0(U_986, V_210, W_211) | ssSkP0(U_991, V_210, W_211) | ssSkP0(U_979, V_210, W_211) | Z_987=X1_989 | Z_987=Y_977 | Y_977=X1_989 | Y_977=X_990 | Z_987=X_990 | X_990=X1_989 | X_990=V_978 | Y_977=V_978 | Z_987=V_978 | X1_989=V_978 | five(W_211, V_210) | ~member(W_211, X1_989, V_210) | ~member(W_211, Z_987, V_210) | ~member(W_211, Y_977, V_210) | ~member(W_211, X_990, V_210) | ~member(W_211, V_978, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_1178, plain, (![X1_808, U_178, Y_802, X_181, Z_179, U_794, Y_182, X_809, W_810, Z_798, V_799, X4_806, V_807, X1_180, Z_803, W_177, X5_804, V_183, X1_796, Y_801, X_800]: (skf21(V_799, X_800, Y_802, Z_798, X1_808, 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_804 | skf21(V_799, X_800, Y_802, Z_798, X1_808, W_177, U_178)=X5_804 | X5_804=X4_806 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_806 | skf21(V_799, X_800, Y_802, Z_798, X1_808, W_177, U_178)=X4_806 | X4_806=U_794 | X5_804=U_794 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_794 | skf21(V_799, X_800, Y_802, Z_798, X1_808, W_177, U_178)=U_794 | ~member(U_178, X5_804, W_177) | ~member(U_178, X4_806, W_177) | ~member(U_178, U_794, W_177) | skf21(U_794, V_807, W_810, X_809, Y_801, Z_803, X1_796)!=U_794 | Z_798=X1_808 | Z_798=Y_802 | Y_802=X1_808 | Y_802=X_800 | Z_798=X_800 | X_800=X1_808 | X_800=V_799 | Y_802=V_799 | Z_798=V_799 | X1_808=V_799 | ~member(U_178, X1_808, W_177) | ~member(U_178, Z_798, W_177) | ~member(U_178, Y_802, W_177) | ~member(U_178, X_800, W_177) | ~member(U_178, V_799, 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.55/18.14 tff(c_1126, plain, (![U_178, X_181, X_748, Z_179, U_755, Y_182, U_747, W_751, X1_180, W_177, X1_746, V_183, Y_752, U_757, U_753, Z_754]: (skf10(U_757, W_177, U_178)=skf10(U_753, W_177, U_178) | skf10(U_753, W_177, U_178)=skf10(U_747, W_177, U_178) | skf10(U_757, W_177, U_178)=skf10(U_747, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_747, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_753, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_757, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_755 | skf10(U_747, W_177, U_178)=U_755 | skf10(U_753, W_177, U_178)=U_755 | skf10(U_757, W_177, U_178)=U_755 | ~member(U_178, U_755, W_177) | skf21(U_755, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), W_751, X_748, Y_752, Z_754, X1_746)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_757, W_177, U_178) | ssSkP0(U_753, W_177, U_178) | ssSkP0(U_747, 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.55/18.14 tff(c_1307, plain, (![Y_929, U_924, W_211, V_210, Z_928, X_926, Z_922, W_927, V_915, U_919, X1_921, X1_918, Y_920, U_209, X_923, U_914]: (skf21(V_915, X_926, Y_929, Z_922, X1_921, V_210, W_211)=skf10(U_919, V_210, W_211) | skf10(U_919, V_210, W_211)=skf10(U_914, V_210, W_211) | skf21(V_915, X_926, Y_929, Z_922, X1_921, V_210, W_211)=skf10(U_914, V_210, W_211) | skf10(U_914, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_919, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_915, X_926, Y_929, Z_922, X1_921, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_924 | skf10(U_914, V_210, W_211)=U_924 | skf10(U_919, V_210, W_211)=U_924 | skf21(V_915, X_926, Y_929, Z_922, X1_921, V_210, W_211)=U_924 | ~member(W_211, U_924, V_210) | skf21(U_924, skf10(U_209, V_210, W_211), W_927, X_923, Y_920, Z_928, X1_918)!=skf10(U_209, V_210, W_211) | Z_922=X1_921 | Z_922=Y_929 | Y_929=X1_921 | Y_929=X_926 | Z_922=X_926 | X_926=X1_921 | X_926=V_915 | Y_929=V_915 | Z_922=V_915 | X1_921=V_915 | five(W_211, V_210) | ~member(W_211, X1_921, V_210) | ~member(W_211, Z_922, V_210) | ~member(W_211, Y_929, V_210) | ~member(W_211, X_926, V_210) | ~member(W_211, V_915, V_210) | ssSkP0(U_919, V_210, W_211) | ssSkP0(U_914, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_948, plain, (![U_178, X_181, Z_179, Z_654, Y_182, U_655, U_646, V_647, X1_180, W_177, Y_650, X1_645, V_183, U_652, X_649]: (skf10(U_652, 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_646, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_652, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_647 | skf10(U_646, W_177, U_178)=V_647 | skf10(U_652, W_177, U_178)=V_647 | V_647=U_655 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_655 | skf10(U_646, W_177, U_178)=U_655 | skf10(U_652, W_177, U_178)=U_655 | ~member(U_178, V_647, W_177) | ~member(U_178, U_655, W_177) | skf21(U_655, V_647, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), X_649, Y_650, Z_654, X1_645)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_652, 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.55/18.14 tff(c_1002, plain, (![X1_706, U_705, U_178, X_181, U_708, Z_179, U_707, Z_715, V_712, Y_182, X_711, Y_717, W_713, X1_180, U_710, W_177, V_183]: (skf10(U_710, W_177, U_178)=skf10(U_705, W_177, U_178) | skf10(U_707, W_177, U_178)=skf10(U_705, W_177, U_178) | skf10(U_710, W_177, U_178)=skf10(U_707, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_707, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_705, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_710, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_708 | skf10(U_707, W_177, U_178)=U_708 | skf10(U_705, W_177, U_178)=U_708 | skf10(U_710, W_177, U_178)=U_708 | ~member(U_178, U_708, W_177) | skf21(U_708, V_712, W_713, X_711, Y_717, Z_715, X1_706)!=U_708 | ssSkP0(U_710, W_177, U_178) | ssSkP0(U_705, W_177, U_178) | ssSkP0(U_707, 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.55/18.14 tff(c_1231, plain, (![V_861, Z_865, X_862, W_211, V_210, U_854, X1_858, X1_855, V_864, U_853, Y_860, Z_859, X_852, Y_856, U_209]: (skf21(V_864, X_862, Y_856, Z_859, X1_858, V_210, W_211)=skf10(U_853, V_210, W_211) | skf10(U_853, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_864, X_862, Y_856, Z_859, X1_858, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_861 | skf10(U_853, V_210, W_211)=V_861 | skf21(V_864, X_862, Y_856, Z_859, X1_858, V_210, W_211)=V_861 | V_861=U_854 | skf10(U_209, V_210, W_211)=U_854 | skf10(U_853, V_210, W_211)=U_854 | skf21(V_864, X_862, Y_856, Z_859, X1_858, V_210, W_211)=U_854 | ~member(W_211, V_861, V_210) | ~member(W_211, U_854, V_210) | skf21(U_854, V_861, skf10(U_209, V_210, W_211), X_852, Y_860, Z_865, X1_855)!=skf10(U_209, V_210, W_211) | Z_859=X1_858 | Z_859=Y_856 | Y_856=X1_858 | Y_856=X_862 | Z_859=X_862 | X_862=X1_858 | X_862=V_864 | Y_856=V_864 | Z_859=V_864 | X1_858=V_864 | five(W_211, V_210) | ~member(W_211, X1_858, V_210) | ~member(W_211, Z_859, V_210) | ~member(W_211, Y_856, V_210) | ~member(W_211, X_862, V_210) | ~member(W_211, V_864, V_210) | ssSkP0(U_853, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_904, plain, (![U_628, U_178, X4_625, Z_622, X_181, Z_179, Y_182, U_626, V_629, W_632, X1_627, X_621, U_620, Y_631, X1_180, W_177, V_183]: (skf10(U_628, W_177, U_178)=skf10(U_620, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_620, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_628, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_625 | skf10(U_620, W_177, U_178)=X4_625 | skf10(U_628, W_177, U_178)=X4_625 | X4_625=U_626 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_626 | skf10(U_620, W_177, U_178)=U_626 | skf10(U_628, W_177, U_178)=U_626 | ~member(U_178, X4_625, W_177) | ~member(U_178, U_626, W_177) | skf21(U_626, V_629, W_632, X_621, Y_631, Z_622, X1_627)!=U_626 | ssSkP0(U_628, W_177, U_178) | ssSkP0(U_620, 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.55/18.14 tff(c_837, plain, (![U_178, Y_587, X_181, Z_179, V_581, U_585, Z_582, Y_182, W_578, U_579, X1_180, W_177, V_183, X1_586]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_579, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=W_578 | skf10(U_579, W_177, U_178)=W_578 | W_578=V_581 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=V_581 | skf10(U_579, W_177, U_178)=V_581 | V_581=U_585 | W_578=U_585 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_585 | skf10(U_579, W_177, U_178)=U_585 | ~member(U_178, W_578, W_177) | ~member(U_178, V_581, W_177) | ~member(U_178, U_585, W_177) | skf21(U_585, V_581, W_578, skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178), Y_587, Z_582, X1_586)!=skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178) | ssSkP0(U_579, 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.55/18.14 tff(c_1281, plain, (![U_895, U_884, X_891, W_211, V_210, V_898, Z_887, W_893, X_889, Z_885, X1_890, Y_892, Y_888, X1_897, V_899, U_209]: (skf21(V_899, X_889, Y_888, Z_885, X1_897, V_210, W_211)=skf10(U_884, V_210, W_211) | skf10(U_884, V_210, W_211)=skf10(U_209, V_210, W_211) | skf21(V_899, X_889, Y_888, Z_885, X1_897, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_898 | skf10(U_884, V_210, W_211)=V_898 | skf21(V_899, X_889, Y_888, Z_885, X1_897, V_210, W_211)=V_898 | V_898=U_895 | skf10(U_209, V_210, W_211)=U_895 | skf10(U_884, V_210, W_211)=U_895 | skf21(V_899, X_889, Y_888, Z_885, X1_897, V_210, W_211)=U_895 | ~member(W_211, V_898, V_210) | ~member(W_211, U_895, V_210) | skf21(U_895, V_898, W_893, X_891, Y_892, Z_887, X1_890)!=V_898 | Z_885=X1_897 | Z_885=Y_888 | Y_888=X1_897 | Y_888=X_889 | Z_885=X_889 | X_889=X1_897 | X_889=V_899 | Y_888=V_899 | Z_885=V_899 | X1_897=V_899 | five(W_211, V_210) | ~member(W_211, X1_897, V_210) | ~member(W_211, Z_885, V_210) | ~member(W_211, Y_888, V_210) | ~member(W_211, X_889, V_210) | ~member(W_211, V_899, V_210) | ssSkP0(U_884, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_1045, plain, (![X1_740, X_735, Y_737, W_211, V_210, U_738, V_734, W_730, Z_733, X1_741, U_209, Y_736, V_739, Z_742]: (skf21(V_734, X_735, Y_737, Z_733, X1_741, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_730 | skf21(V_734, X_735, Y_737, Z_733, X1_741, V_210, W_211)=W_730 | W_730=V_739 | skf10(U_209, V_210, W_211)=V_739 | skf21(V_734, X_735, Y_737, Z_733, X1_741, V_210, W_211)=V_739 | V_739=U_738 | W_730=U_738 | skf10(U_209, V_210, W_211)=U_738 | skf21(V_734, X_735, Y_737, Z_733, X1_741, V_210, W_211)=U_738 | ~member(W_211, W_730, V_210) | ~member(W_211, V_739, V_210) | ~member(W_211, U_738, V_210) | skf21(U_738, V_739, W_730, skf10(U_209, V_210, W_211), Y_736, Z_742, X1_740)!=skf10(U_209, V_210, W_211) | Z_733=X1_741 | Z_733=Y_737 | Y_737=X1_741 | Y_737=X_735 | Z_733=X_735 | X_735=X1_741 | X_735=V_734 | Y_737=V_734 | Z_733=V_734 | X1_741=V_734 | five(W_211, V_210) | ~member(W_211, X1_741, V_210) | ~member(W_211, Z_733, V_210) | ~member(W_211, Y_737, V_210) | ~member(W_211, X_735, V_210) | ~member(W_211, V_734, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_971, plain, (![V_661, W_211, Y_669, V_210, V_668, X_662, Z_660, X_666, X4_663, U_671, X1_670, Z_657, X1_665, W_667, Y_664, U_209]: (skf21(V_661, X_662, Y_664, Z_660, X1_670, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_663 | skf21(V_661, X_662, Y_664, Z_660, X1_670, V_210, W_211)=X4_663 | X4_663=V_668 | skf10(U_209, V_210, W_211)=V_668 | skf21(V_661, X_662, Y_664, Z_660, X1_670, V_210, W_211)=V_668 | V_668=U_671 | X4_663=U_671 | skf10(U_209, V_210, W_211)=U_671 | skf21(V_661, X_662, Y_664, Z_660, X1_670, V_210, W_211)=U_671 | ~member(W_211, X4_663, V_210) | ~member(W_211, V_668, V_210) | ~member(W_211, U_671, V_210) | skf21(U_671, V_668, W_667, X_666, Y_669, Z_657, X1_665)!=V_668 | Z_660=X1_670 | Z_660=Y_664 | Y_664=X1_670 | Y_664=X_662 | Z_660=X_662 | X_662=X1_670 | X_662=V_661 | Y_664=V_661 | Z_660=V_661 | X1_670=V_661 | five(W_211, V_210) | ~member(W_211, X1_670, V_210) | ~member(W_211, Z_660, V_210) | ~member(W_211, Y_664, V_210) | ~member(W_211, X_662, V_210) | ~member(W_211, V_661, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_815, plain, (![X_568, U_565, U_178, X_181, Z_179, X1_573, Z_570, W_577, X4_574, Y_182, Y_567, V_569, X1_180, W_177, V_183, U_576, X5_571]: (skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=skf10(U_565, W_177, U_178) | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X5_571 | skf10(U_565, W_177, U_178)=X5_571 | X5_571=X4_574 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=X4_574 | skf10(U_565, W_177, U_178)=X4_574 | X4_574=U_576 | X5_571=U_576 | skf21(V_183, X_181, Y_182, Z_179, X1_180, W_177, U_178)=U_576 | skf10(U_565, W_177, U_178)=U_576 | ~member(U_178, X5_571, W_177) | ~member(U_178, X4_574, W_177) | ~member(U_178, U_576, W_177) | skf21(U_576, V_569, W_577, X_568, Y_567, Z_570, X1_573)!=U_576 | ssSkP0(U_565, 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.55/18.14 tff(c_1204, plain, (![X_814, Z_820, Y_819, W_211, X1_825, V_210, W_815, Z_816, Y_821, X_818, X1_824, V_817, U_209, U_823, V_812]: (skf21(V_817, X_818, Y_821, Z_816, X1_825, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_815 | skf21(V_817, X_818, Y_821, Z_816, X1_825, V_210, W_211)=W_815 | W_815=V_812 | skf10(U_209, V_210, W_211)=V_812 | skf21(V_817, X_818, Y_821, Z_816, X1_825, V_210, W_211)=V_812 | V_812=U_823 | W_815=U_823 | skf10(U_209, V_210, W_211)=U_823 | skf21(V_817, X_818, Y_821, Z_816, X1_825, V_210, W_211)=U_823 | ~member(W_211, W_815, V_210) | ~member(W_211, V_812, V_210) | ~member(W_211, U_823, V_210) | skf21(U_823, V_812, W_815, X_814, Y_819, Z_820, X1_824)!=W_815 | Z_816=X1_825 | Z_816=Y_821 | Y_821=X1_825 | Y_821=X_818 | Z_816=X_818 | X_818=X1_825 | X_818=V_817 | Y_821=V_817 | Z_816=V_817 | X1_825=V_817 | five(W_211, V_210) | ~member(W_211, X1_825, V_210) | ~member(W_211, Z_816, V_210) | ~member(W_211, Y_821, V_210) | ~member(W_211, X_818, V_210) | ~member(W_211, V_817, V_210) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_1153, plain, (![U_771, W_781, V_769, W_211, V_210, U_778, Y_775, U_780, X_773, X1_774, U_770, U_209, Z_776]: (skf10(U_780, V_210, W_211)=skf10(U_778, V_210, W_211) | skf10(U_780, V_210, W_211)=skf10(U_771, V_210, W_211) | skf10(U_778, V_210, W_211)=skf10(U_771, V_210, W_211) | skf10(U_771, V_210, W_211)=skf10(U_770, V_210, W_211) | skf10(U_780, V_210, W_211)=skf10(U_770, V_210, W_211) | skf10(U_778, V_210, W_211)=skf10(U_770, V_210, W_211) | skf10(U_770, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_771, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_780, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_778, 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_769, W_781, X_773, Y_775, Z_776, X1_774)!=skf10(U_209, V_210, W_211) | ssSkP0(U_778, V_210, W_211) | ssSkP0(U_780, V_210, W_211) | ssSkP0(U_771, V_210, W_211) | ssSkP0(U_770, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_790, plain, (![W_547, X1_172, V_544, X_174, Z_171, X_549, U_170, X1_548, U_545, W_168, V_176, Y_543, Z_546]: (skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=X_174 | X_174=W_168 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=W_168 | W_168=V_176 | X_174=V_176 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=V_176 | V_176=U_170 | W_168=U_170 | X_174=U_170 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=U_170 | ~member(U_545, X_174, W_547) | ~member(U_545, W_168, W_547) | ~member(U_545, V_176, W_547) | ~member(U_545, U_170, W_547) | skf21(U_170, V_176, W_168, X_174, skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545), Z_171, X1_172)!=skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545) | Z_546=X1_548 | Z_546=Y_543 | Y_543=X1_548 | Y_543=X_549 | Z_546=X_549 | X_549=X1_548 | X_549=V_544 | Y_543=V_544 | Z_546=V_544 | X1_548=V_544 | five(U_545, W_547) | ~member(U_545, X1_548, W_547) | ~member(U_545, Z_546, W_547) | ~member(U_545, Y_543, W_547) | ~member(U_545, X_549, W_547) | ~member(U_545, V_544, W_547)))). % 27.55/18.14 tff(c_789, plain, (![W_547, W_148, V_544, V_156, X_549, Y_155, X1_548, X1_152, U_545, X_154, Y_543, Z_151, Z_546, U_150, X4_157]: (skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=X4_157 | X4_157=W_148 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=W_148 | W_148=V_156 | X4_157=V_156 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=V_156 | V_156=U_150 | W_148=U_150 | X4_157=U_150 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=U_150 | ~member(U_545, X4_157, W_547) | ~member(U_545, W_148, W_547) | ~member(U_545, V_156, W_547) | ~member(U_545, U_150, W_547) | skf21(U_150, V_156, W_148, X_154, Y_155, Z_151, X1_152)!=W_148 | Z_546=X1_548 | Z_546=Y_543 | Y_543=X1_548 | Y_543=X_549 | Z_546=X_549 | X_549=X1_548 | X_549=V_544 | Y_543=V_544 | Z_546=V_544 | X1_548=V_544 | five(U_545, W_547) | ~member(U_545, X1_548, W_547) | ~member(U_545, Z_546, W_547) | ~member(U_545, Y_543, W_547) | ~member(U_545, X_549, W_547) | ~member(U_545, V_544, W_547)))). % 27.55/18.14 tff(c_787, plain, (![W_547, V_195, X6_185, V_544, U_188, X4_196, X_549, X5_184, Z_189, X1_548, U_545, X1_191, Y_194, Y_543, Z_546, W_186, X_193]: (skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=X6_185 | X6_185=X5_184 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=X5_184 | X5_184=X4_196 | X6_185=X4_196 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=X4_196 | X4_196=U_188 | X5_184=U_188 | X6_185=U_188 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=U_188 | ~member(U_545, X6_185, W_547) | ~member(U_545, X5_184, W_547) | ~member(U_545, X4_196, W_547) | ~member(U_545, U_188, W_547) | skf21(U_188, V_195, W_186, X_193, Y_194, Z_189, X1_191)!=U_188 | Z_546=X1_548 | Z_546=Y_543 | Y_543=X1_548 | Y_543=X_549 | Z_546=X_549 | X_549=X1_548 | X_549=V_544 | Y_543=V_544 | Z_546=V_544 | X1_548=V_544 | five(U_545, W_547) | ~member(U_545, X1_548, W_547) | ~member(U_545, Z_546, W_547) | ~member(U_545, Y_543, W_547) | ~member(U_545, X_549, W_547) | ~member(U_545, V_544, W_547)))). % 27.55/18.14 tff(c_1127, plain, (![W_211, V_210, X_748, U_755, U_747, W_751, X1_746, Y_752, U_757, U_209, U_753, Z_754]: (skf10(U_757, V_210, W_211)=skf10(U_753, V_210, W_211) | skf10(U_753, V_210, W_211)=skf10(U_747, V_210, W_211) | skf10(U_757, V_210, W_211)=skf10(U_747, V_210, W_211) | skf10(U_747, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_753, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_757, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_755 | skf10(U_747, V_210, W_211)=U_755 | skf10(U_753, V_210, W_211)=U_755 | skf10(U_757, V_210, W_211)=U_755 | five(W_211, V_210) | ~member(W_211, U_755, V_210) | skf21(U_755, skf10(U_209, V_210, W_211), W_751, X_748, Y_752, Z_754, X1_746)!=skf10(U_209, V_210, W_211) | ssSkP0(U_757, V_210, W_211) | ssSkP0(U_753, V_210, W_211) | ssSkP0(U_747, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_1003, plain, (![X1_706, U_705, W_211, V_210, U_708, U_707, Z_715, V_712, X_711, Y_717, W_713, U_710, U_209]: (skf10(U_710, V_210, W_211)=skf10(U_705, V_210, W_211) | skf10(U_707, V_210, W_211)=skf10(U_705, V_210, W_211) | skf10(U_710, V_210, W_211)=skf10(U_707, V_210, W_211) | skf10(U_707, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_705, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_710, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=U_708 | skf10(U_707, V_210, W_211)=U_708 | skf10(U_705, V_210, W_211)=U_708 | skf10(U_710, V_210, W_211)=U_708 | five(W_211, V_210) | ~member(W_211, U_708, V_210) | skf21(U_708, V_712, W_713, X_711, Y_717, Z_715, X1_706)!=U_708 | ssSkP0(U_710, V_210, W_211) | ssSkP0(U_705, V_210, W_211) | ssSkP0(U_707, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_949, plain, (![W_211, V_210, Z_654, U_655, U_646, V_647, Y_650, X1_645, U_652, U_209, X_649]: (skf10(U_652, V_210, W_211)=skf10(U_646, V_210, W_211) | skf10(U_646, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_652, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_647 | skf10(U_646, V_210, W_211)=V_647 | skf10(U_652, V_210, W_211)=V_647 | V_647=U_655 | skf10(U_209, V_210, W_211)=U_655 | skf10(U_646, V_210, W_211)=U_655 | skf10(U_652, V_210, W_211)=U_655 | five(W_211, V_210) | ~member(W_211, V_647, V_210) | ~member(W_211, U_655, V_210) | skf21(U_655, V_647, skf10(U_209, V_210, W_211), X_649, Y_650, Z_654, X1_645)!=skf10(U_209, V_210, W_211) | ssSkP0(U_652, V_210, W_211) | ssSkP0(U_646, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_927, plain, (![Y_636, W_211, W_641, V_210, U_634, U_633, X1_639, U_640, X_644, U_209, Z_638, V_642]: (skf10(U_634, V_210, W_211)=skf10(U_633, V_210, W_211) | skf10(U_634, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_633, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=V_642 | skf10(U_634, V_210, W_211)=V_642 | skf10(U_633, V_210, W_211)=V_642 | V_642=U_640 | skf10(U_209, V_210, W_211)=U_640 | skf10(U_634, V_210, W_211)=U_640 | skf10(U_633, V_210, W_211)=U_640 | five(W_211, V_210) | ~member(W_211, V_642, V_210) | ~member(W_211, U_640, V_210) | skf21(U_640, V_642, W_641, X_644, Y_636, Z_638, X1_639)!=V_642 | ssSkP0(U_633, V_210, W_211) | ssSkP0(U_634, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_1106, plain, (![V_26]: (skf8(skc5, V_26)=skf20(V_26, skc5) | skf8(skc5, V_26)=skf18(V_26, skc5) | skf8(skc5, V_26)=skf16(V_26, skc5) | skf8(skc5, V_26)=skf14(V_26, skc5) | skf8(skc5, V_26)=skf12(V_26, skc5) | skf10(skc8, V_26, skc5)=skf20(V_26, skc5) | skf10(skc8, V_26, skc5)=skf18(V_26, skc5) | skf10(skc8, V_26, skc5)=skf16(V_26, skc5) | skf10(skc8, V_26, skc5)=skf14(V_26, skc5) | skf10(skc8, V_26, skc5)=skf12(V_26, skc5) | ~five(skc5, V_26)))). % 27.55/18.14 tff(c_1028, plain, (![V_727]: (member(skc5, skf8(skc5, V_727), V_727) | ~group(skc5, V_727) | skf10(skc8, V_727, skc5)=skf20(V_727, skc5) | skf10(skc8, V_727, skc5)=skf18(V_727, skc5) | skf10(skc8, V_727, skc5)=skf16(V_727, skc5) | skf10(skc8, V_727, skc5)=skf14(V_727, skc5) | skf10(skc8, V_727, skc5)=skf12(V_727, skc5) | ~five(skc5, V_727)))). % 27.55/18.14 tff(c_786, plain, (![W_547, Z_161, V_544, X1_162, X_549, W_158, X1_548, U_545, U_160, Y_543, V_166, Z_546, X_164, Y_165]: (skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=X_164 | X_164=W_158 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=W_158 | W_158=V_166 | X_164=V_166 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=V_166 | V_166=U_160 | W_158=U_160 | X_164=U_160 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=U_160 | ~member(U_545, X_164, W_547) | ~member(U_545, W_158, W_547) | ~member(U_545, V_166, W_547) | ~member(U_545, U_160, W_547) | skf21(U_160, V_166, W_158, X_164, Y_165, Z_161, X1_162)!=X_164 | Z_546=X1_548 | Z_546=Y_543 | Y_543=X1_548 | Y_543=X_549 | Z_546=X_549 | X_549=X1_548 | X_549=V_544 | Y_543=V_544 | Z_546=V_544 | X1_548=V_544 | five(U_545, W_547) | ~member(U_545, X1_548, W_547) | ~member(U_545, Z_546, W_547) | ~member(U_545, Y_543, W_547) | ~member(U_545, X_549, W_547) | ~member(U_545, V_544, W_547)))). % 27.55/18.14 tff(c_1024, plain, (![V_719, V_724]: (member(skc5, skf8(skc5, V_719), V_719) | ~group(skc5, V_719) | skf10(V_724, V_719, skc5)=skf20(V_719, skc5) | skf10(V_724, V_719, skc5)=skf18(V_719, skc5) | skf10(V_724, V_719, skc5)=skf16(V_719, skc5) | skf10(V_724, V_719, skc5)=skf14(V_719, skc5) | skf10(V_724, V_719, skc5)=skf12(V_719, skc5) | ~five(skc5, V_719) | ~abstraction(skc5, V_724)))). % 27.55/18.14 tff(c_986, plain, (![X_699, V_701, V_704, U_15, W_702, Y_698, V_16]: (member(U_15, skf8(U_15, V_701), V_701) | ~actual_world(U_15) | ~group(U_15, V_701) | ~patient(U_15, X_699, Y_698) | ~shake_beverage(U_15, Y_698) | ~event(U_15, X_699) | ~past(U_15, X_699) | ~nonreflexive(U_15, X_699) | ~order(U_15, X_699) | ~agent(U_15, X_699, W_702) | ~woman(U_15, W_702) | ~of(U_15, V_704, W_702) | ~mia_forename(U_15, V_704) | ~forename(U_15, V_704) | skf10(V_16, V_701, U_15)=skf20(V_701, U_15) | skf10(V_16, V_701, U_15)=skf18(V_701, U_15) | skf10(V_16, V_701, U_15)=skf16(V_701, U_15) | skf10(V_16, V_701, U_15)=skf14(V_701, U_15) | skf10(V_16, V_701, U_15)=skf12(V_701, U_15) | ~five(U_15, V_701) | ~abstraction(U_15, V_16)))). % 27.55/18.14 tff(c_905, plain, (![U_628, W_211, V_210, X4_625, Z_622, U_626, V_629, W_632, X1_627, X_621, U_620, Y_631, U_209]: (skf10(U_628, V_210, W_211)=skf10(U_620, V_210, W_211) | skf10(U_620, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_628, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_625 | skf10(U_620, V_210, W_211)=X4_625 | skf10(U_628, V_210, W_211)=X4_625 | X4_625=U_626 | skf10(U_209, V_210, W_211)=U_626 | skf10(U_620, V_210, W_211)=U_626 | skf10(U_628, V_210, W_211)=U_626 | five(W_211, V_210) | ~member(W_211, X4_625, V_210) | ~member(W_211, U_626, V_210) | skf21(U_626, V_629, W_632, X_621, Y_631, Z_622, X1_627)!=U_626 | ssSkP0(U_628, V_210, W_211) | ssSkP0(U_620, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.14 tff(c_799, plain, (![W_211, V_210, W_564, Y_560, V_561, X_563, U_209]: (member(W_211, skf8(W_211, V_210), V_210) | ~actual_world(W_211) | ~nonhuman(W_211, U_209) | ~group(W_211, V_210) | ~patient(W_211, X_563, Y_560) | ~shake_beverage(W_211, Y_560) | ~event(W_211, X_563) | ~past(W_211, X_563) | ~nonreflexive(W_211, X_563) | ~order(W_211, X_563) | ~agent(W_211, X_563, W_564) | ~woman(W_211, W_564) | ~of(W_211, V_561, W_564) | ~mia_forename(W_211, V_561) | ~forename(W_211, V_561) | 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)))). % 27.55/18.15 tff(c_981, plain, (![V_689, X1_686, W_688, X_685, Y_682, V_684, U_15, V_16]: (~actual_world(U_15) | ~dollar(U_15, skf8(U_15, X1_686)) | ~group(U_15, V_684) | ~patient(U_15, X_685, Y_682) | ~shake_beverage(U_15, Y_682) | ~event(U_15, X_685) | ~past(U_15, X_685) | ~nonreflexive(U_15, X_685) | ~order(U_15, X_685) | ~agent(U_15, X_685, W_688) | ~woman(U_15, W_688) | ~of(U_15, V_689, W_688) | ~mia_forename(U_15, V_689) | ~forename(U_15, V_689) | skf10(V_16, V_684, U_15)=skf20(V_684, U_15) | skf10(V_16, V_684, U_15)=skf18(V_684, U_15) | skf10(V_16, V_684, U_15)=skf16(V_684, U_15) | skf10(V_16, V_684, U_15)=skf14(V_684, U_15) | skf10(V_16, V_684, U_15)=skf12(V_684, U_15) | ~five(U_15, V_684) | ~abstraction(U_15, V_16)))). % 27.55/18.15 tff(c_795, plain, (![W_211, V_210, Y_552, X_550, X1_556, V_554, U_209, W_551]: (~actual_world(W_211) | ~nonhuman(W_211, U_209) | ~dollar(W_211, skf8(W_211, X1_556)) | ~group(W_211, V_210) | ~patient(W_211, X_550, Y_552) | ~shake_beverage(W_211, Y_552) | ~event(W_211, X_550) | ~past(W_211, X_550) | ~nonreflexive(W_211, X_550) | ~order(W_211, X_550) | ~agent(W_211, X_550, W_551) | ~woman(W_211, W_551) | ~of(W_211, V_554, W_551) | ~mia_forename(W_211, V_554) | ~forename(W_211, V_554) | 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)))). % 27.55/18.15 tff(c_838, plain, (![W_211, V_210, Y_587, V_581, U_585, Z_582, W_578, U_579, U_209, X1_586]: (skf10(U_579, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_578 | skf10(U_579, V_210, W_211)=W_578 | W_578=V_581 | skf10(U_209, V_210, W_211)=V_581 | skf10(U_579, V_210, W_211)=V_581 | V_581=U_585 | W_578=U_585 | skf10(U_209, V_210, W_211)=U_585 | skf10(U_579, V_210, W_211)=U_585 | five(W_211, V_210) | ~member(W_211, W_578, V_210) | ~member(W_211, V_581, V_210) | ~member(W_211, U_585, V_210) | skf21(U_585, V_581, W_578, skf10(U_209, V_210, W_211), Y_587, Z_582, X1_586)!=skf10(U_209, V_210, W_211) | ssSkP0(U_579, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.15 tff(c_788, plain, (![W_547, W_199, Z_202, X4_208, V_544, X5_197, X_205, X_549, V_207, X1_548, U_545, U_201, Y_543, X1_203, Z_546, Y_206]: (skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=X5_197 | X5_197=X4_208 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=X4_208 | X4_208=V_207 | X5_197=V_207 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=V_207 | V_207=U_201 | X4_208=U_201 | X5_197=U_201 | skf21(V_544, X_549, Y_543, Z_546, X1_548, W_547, U_545)=U_201 | ~member(U_545, X5_197, W_547) | ~member(U_545, X4_208, W_547) | ~member(U_545, V_207, W_547) | ~member(U_545, U_201, W_547) | skf21(U_201, V_207, W_199, X_205, Y_206, Z_202, X1_203)!=V_207 | Z_546=X1_548 | Z_546=Y_543 | Y_543=X1_548 | Y_543=X_549 | Z_546=X_549 | X_549=X1_548 | X_549=V_544 | Y_543=V_544 | Z_546=V_544 | X1_548=V_544 | five(U_545, W_547) | ~member(U_545, X1_548, W_547) | ~member(U_545, Z_546, W_547) | ~member(U_545, Y_543, W_547) | ~member(U_545, X_549, W_547) | ~member(U_545, V_544, W_547)))). % 27.55/18.15 tff(c_860, plain, (![U_589, V_596, W_211, V_210, X_598, Z_592, X1_591, W_593, U_209, Y_595, U_594]: (skf10(U_589, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=W_593 | skf10(U_589, V_210, W_211)=W_593 | W_593=V_596 | skf10(U_209, V_210, W_211)=V_596 | skf10(U_589, V_210, W_211)=V_596 | V_596=U_594 | W_593=U_594 | skf10(U_209, V_210, W_211)=U_594 | skf10(U_589, V_210, W_211)=U_594 | five(W_211, V_210) | ~member(W_211, W_593, V_210) | ~member(W_211, V_596, V_210) | ~member(W_211, U_594, V_210) | skf21(U_594, V_596, W_593, X_598, Y_595, Z_592, X1_591)!=W_593 | ssSkP0(U_589, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.15 tff(c_882, plain, (![V_599, X1_605, W_211, W_607, V_210, U_601, Z_600, X_608, U_604, Y_610, X4_603, U_209]: (skf10(U_601, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X4_603 | skf10(U_601, V_210, W_211)=X4_603 | X4_603=V_599 | skf10(U_209, V_210, W_211)=V_599 | skf10(U_601, V_210, W_211)=V_599 | V_599=U_604 | X4_603=U_604 | skf10(U_209, V_210, W_211)=U_604 | skf10(U_601, V_210, W_211)=U_604 | five(W_211, V_210) | ~member(W_211, X4_603, V_210) | ~member(W_211, V_599, V_210) | ~member(W_211, U_604, V_210) | skf21(U_604, V_599, W_607, X_608, Y_610, Z_600, X1_605)!=V_599 | ssSkP0(U_601, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.15 tff(c_816, plain, (![X_568, W_211, V_210, U_565, X1_573, Z_570, W_577, X4_574, Y_567, V_569, U_576, X5_571, U_209]: (skf10(U_565, V_210, W_211)=skf10(U_209, V_210, W_211) | skf10(U_209, V_210, W_211)=X5_571 | skf10(U_565, V_210, W_211)=X5_571 | X5_571=X4_574 | skf10(U_209, V_210, W_211)=X4_574 | skf10(U_565, V_210, W_211)=X4_574 | X4_574=U_576 | X5_571=U_576 | skf10(U_209, V_210, W_211)=U_576 | skf10(U_565, V_210, W_211)=U_576 | five(W_211, V_210) | ~member(W_211, X5_571, V_210) | ~member(W_211, X4_574, V_210) | ~member(W_211, U_576, V_210) | skf21(U_576, V_569, W_577, X_568, Y_567, Z_570, X1_573)!=U_576 | ssSkP0(U_565, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.15 tff(c_690, plain, (![V_496, W_211, V_210, W_494, U_489, X1_488, X_495, U_209, Z_490]: (skf10(U_209, V_210, W_211)=X_495 | X_495=W_494 | skf10(U_209, V_210, W_211)=W_494 | W_494=V_496 | X_495=V_496 | skf10(U_209, V_210, W_211)=V_496 | V_496=U_489 | W_494=U_489 | X_495=U_489 | skf10(U_209, V_210, W_211)=U_489 | five(W_211, V_210) | ~member(W_211, X_495, V_210) | ~member(W_211, W_494, V_210) | ~member(W_211, V_496, V_210) | ~member(W_211, U_489, V_210) | skf21(U_489, V_496, W_494, X_495, skf10(U_209, V_210, W_211), Z_490, X1_488)!=skf10(U_209, V_210, W_211) | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.15 tff(c_728, plain, (![W_211, V_210, X1_512, V_517, Y_518, X5_509, X4_510, X_514, W_515, Z_508, U_519, U_209]: (skf10(U_209, V_210, W_211)=X5_509 | X5_509=X4_510 | skf10(U_209, V_210, W_211)=X4_510 | X4_510=V_517 | X5_509=V_517 | skf10(U_209, V_210, W_211)=V_517 | V_517=U_519 | X4_510=U_519 | X5_509=U_519 | skf10(U_209, V_210, W_211)=U_519 | five(W_211, V_210) | ~member(W_211, X5_509, V_210) | ~member(W_211, X4_510, V_210) | ~member(W_211, V_517, V_210) | ~member(W_211, U_519, V_210) | skf21(U_519, V_517, W_515, X_514, Y_518, Z_508, X1_512)!=V_517 | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.15 tff(c_709, plain, (![W_211, V_210, X4_504, Y_502, X1_506, W_501, U_505, V_497, Z_503, X_500, U_209]: (skf10(U_209, V_210, W_211)=X4_504 | X4_504=W_501 | skf10(U_209, V_210, W_211)=W_501 | W_501=V_497 | X4_504=V_497 | skf10(U_209, V_210, W_211)=V_497 | V_497=U_505 | W_501=U_505 | X4_504=U_505 | skf10(U_209, V_210, W_211)=U_505 | five(W_211, V_210) | ~member(W_211, X4_504, V_210) | ~member(W_211, W_501, V_210) | ~member(W_211, V_497, V_210) | ~member(W_211, U_505, V_210) | skf21(U_505, V_497, W_501, X_500, Y_502, Z_503, X1_506)!=W_501 | ssSkP0(U_209, V_210, W_211)))). % 27.55/18.15 tff(c_766, plain, (![W_211, V_210, Y_538, X1_541, U_539, V_540, Z_542, X_537, U_209, W_535]: (skf10(U_209, V_210, W_211)=X_537 | X_537=W_535 | skf10(U_209, V_210, W_211)=W_535 | W_535=V_540 | X_537=V_540 | skf10(U_209, V_210, W_211)=V_540 | V_540=U_539 | W_535=U_539 | X_537=U_539 | skf10(U_209, V_210, W_211)=U_539 | five(W_211, V_210) | ~member(W_211, X_537, V_210) | ~member(W_211, W_535, V_210) | ~member(W_211, V_540, V_210) | ~member(W_211, U_539, V_210) | skf21(U_539, V_540, W_535, X_537, Y_538, Z_542, X1_541)!=X_537 | ssSkP0(U_209, V_210, W_211)))). % 27.74/18.15 tff(c_747, plain, (![Y_524, W_211, V_210, U_520, X5_527, W_532, X_531, Z_526, X1_521, V_530, U_209, X4_529, X6_528]: (skf10(U_209, V_210, W_211)=X6_528 | X6_528=X5_527 | skf10(U_209, V_210, W_211)=X5_527 | X5_527=X4_529 | X6_528=X4_529 | skf10(U_209, V_210, W_211)=X4_529 | X4_529=U_520 | X5_527=U_520 | X6_528=U_520 | skf10(U_209, V_210, W_211)=U_520 | five(W_211, V_210) | ~member(W_211, X6_528, V_210) | ~member(W_211, X5_527, V_210) | ~member(W_211, X4_529, V_210) | ~member(W_211, U_520, V_210) | skf21(U_520, V_530, W_532, X_531, Y_524, Z_526, X1_521)!=U_520 | ssSkP0(U_209, V_210, W_211)))). % 27.74/18.15 tff(c_184, plain, (![U_217, W_216, X1_219, V_222, Y_221, X_220, Z_218]: (member(U_217, skf8(U_217, Z_218), Z_218) | ~actual_world(U_217) | ~nonhuman(U_217, X1_219) | ~ssSkP0(X1_219, Z_218, U_217) | ~group(U_217, Z_218) | ~five(U_217, Z_218) | ~patient(U_217, X_220, Y_221) | ~shake_beverage(U_217, Y_221) | ~event(U_217, X_220) | ~past(U_217, X_220) | ~nonreflexive(U_217, X_220) | ~order(U_217, X_220) | ~agent(U_217, X_220, W_216) | ~woman(U_217, W_216) | ~of(U_217, V_222, W_216) | ~mia_forename(U_217, V_222) | ~forename(U_217, V_222)))). % 27.74/18.15 tff(c_186, plain, (![U_224, X_228, X2_227, X1_226, V_230, Y_229, Z_225, W_223]: (~actual_world(U_224) | ~nonhuman(U_224, X2_227) | ~ssSkP0(X2_227, Z_225, U_224) | ~dollar(U_224, skf8(U_224, X1_226)) | ~group(U_224, Z_225) | ~five(U_224, Z_225) | ~patient(U_224, X_228, Y_229) | ~shake_beverage(U_224, Y_229) | ~event(U_224, X_228) | ~past(U_224, X_228) | ~nonreflexive(U_224, X_228) | ~order(U_224, X_228) | ~agent(U_224, X_228, W_223) | ~woman(U_224, W_223) | ~of(U_224, V_230, W_223) | ~mia_forename(U_224, V_230) | ~forename(U_224, V_230)))). % 27.74/18.15 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.74/18.15 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.74/18.15 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.74/18.15 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.74/18.15 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.74/18.15 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.74/18.15 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.74/18.15 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.74/18.15 tff(c_636, plain, (![W_473]: (skc8=W_473 | ~forename(skc5, W_473) | ~of(skc5, W_473, skc9)))). % 27.74/18.15 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.74/18.15 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.74/18.15 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.74/18.15 tff(c_629, plain, (~act(skc5, skc7))). % 27.74/18.15 tff(c_615, plain, (![U_47, V_48]: (~act(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.74/18.15 tff(c_624, plain, (~agent(skc5, skc6, skc7))). % 27.74/18.15 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.74/18.15 tff(c_591, plain, (![U_47, V_48]: (~cost(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.74/18.15 tff(c_515, plain, (![U_41, V_42]: (~entity(U_41, V_42) | ~act(U_41, V_42)))). % 27.74/18.15 tff(c_602, plain, (~food(skc5, skc9))). % 27.74/18.15 tff(c_110, plain, (![U_109, V_110]: (member(U_109, skf18(V_110, U_109), V_110) | ~five(U_109, V_110)))). % 27.74/18.15 tff(c_537, plain, (![U_77, V_78]: (~food(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.74/18.15 tff(c_597, plain, (~abstraction(skc5, skc7))). % 27.74/18.15 tff(c_532, plain, (![U_421, V_422]: (~abstraction(U_421, V_422) | ~beverage(U_421, V_422)))). % 27.74/18.15 tff(c_516, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~cost(U_27, V_28)))). % 27.74/18.15 tff(c_504, plain, (![U_25, V_26]: (~abstraction(U_25, V_26) | ~five(U_25, V_26)))). % 27.74/18.15 tff(c_136, plain, (![V_136, U_135]: (~five(V_136, U_135) | skf14(U_135, V_136)!=skf12(U_135, V_136)))). % 27.74/18.15 tff(c_581, plain, (~animate(skc5, skc7))). % 27.74/18.15 tff(c_562, plain, (![U_47, V_48]: (~animate(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.74/18.15 tff(c_556, plain, (![U_25, V_26]: (~eventuality(U_25, V_26) | ~five(U_25, V_26)))). % 27.74/18.15 tff(c_108, plain, (![U_107, V_108]: (member(U_107, skf20(V_108, U_107), V_108) | ~five(U_107, V_108)))). % 27.74/18.15 tff(c_549, plain, (![U_41, V_42]: (~abstraction(U_41, V_42) | ~act(U_41, V_42)))). % 27.74/18.15 tff(c_567, plain, (![U_25, V_26]: (~entity(U_25, V_26) | ~five(U_25, V_26)))). % 27.74/18.15 tff(c_550, plain, (![U_27, V_28]: (~abstraction(U_27, V_28) | ~cost(U_27, V_28)))). % 27.74/18.15 tff(c_486, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~group(U_21, V_22)))). % 27.74/18.15 tff(c_464, plain, (![U_389, V_390]: (~animate(U_389, V_390) | ~food(U_389, V_390)))). % 27.74/18.15 tff(c_112, plain, (![U_111, V_112]: (member(U_111, skf16(V_112, U_111), V_112) | ~five(U_111, V_112)))). % 27.74/18.15 tff(c_498, plain, (![U_21, V_22]: (~eventuality(U_21, V_22) | ~group(U_21, V_22)))). % 27.74/18.15 tff(c_551, plain, (~abstraction(skc5, skc6))). % 27.74/18.15 tff(c_469, plain, (![U_29, V_30]: (~abstraction(U_29, V_30) | ~event(U_29, V_30)))). % 27.74/18.15 tff(c_120, plain, (![V_120, U_119]: (~five(V_120, U_119) | skf20(U_119, V_120)!=skf14(U_119, V_120)))). % 27.74/18.15 tff(c_463, plain, (![U_389, V_390]: (~living(U_389, V_390) | ~food(U_389, V_390)))). % 27.74/18.15 tff(c_531, plain, (~beverage(skc5, skc6))). % 27.74/18.15 tff(c_455, plain, (![U_47, V_48]: (entity(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.74/18.15 tff(c_523, plain, (~beverage(skc5, skc9))). % 27.74/18.15 tff(c_450, plain, (![U_47, V_48]: (~female(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.74/18.15 tff(c_134, plain, (![V_134, U_133]: (~five(V_134, U_133) | skf16(U_133, V_134)!=skf14(U_133, V_134)))). % 27.74/18.15 tff(c_517, plain, (~entity(skc5, skc6))). % 27.74/18.15 tff(c_492, plain, (![U_29, V_30]: (~entity(U_29, V_30) | ~event(U_29, V_30)))). % 27.74/18.15 tff(c_445, plain, (![U_21, V_22]: (~abstraction(U_21, V_22) | ~group(U_21, V_22)))). % 27.74/18.15 tff(c_132, plain, (![V_132, U_131]: (~five(V_132, U_131) | skf16(U_131, V_132)!=skf12(U_131, V_132)))). % 27.74/18.15 tff(c_403, plain, (![U_371, V_372]: (~multiple(U_371, V_372) | ~eventuality(U_371, V_372)))). % 27.74/18.15 tff(c_420, plain, (![U_373, V_374]: (impartial(U_373, V_374) | ~food(U_373, V_374)))). % 27.74/18.15 tff(c_375, plain, (![U_59, V_60]: (~eventuality(U_59, V_60) | ~entity(U_59, V_60)))). % 27.74/18.15 tff(c_381, plain, (![U_5, V_6]: (abstraction(U_5, V_6) | ~cash(U_5, V_6)))). % 27.74/18.15 tff(c_353, plain, (![U_343, V_344]: (~multiple(U_343, V_344) | ~entity(U_343, V_344)))). % 27.74/18.15 tff(c_114, plain, (![U_113, V_114]: (member(U_113, skf14(V_114, U_113), V_114) | ~five(U_113, V_114)))). % 27.74/18.15 tff(c_347, plain, (![U_17, V_18]: (~entity(U_17, V_18) | ~abstraction(U_17, V_18)))). % 27.74/18.15 tff(c_475, plain, (abstraction(skc5, skc8))). % 27.74/18.15 tff(c_359, plain, (![U_347, V_348]: (abstraction(U_347, V_348) | ~forename(U_347, V_348)))). % 27.74/18.15 tff(c_118, plain, (![V_118, U_117]: (~five(V_118, U_117) | skf20(U_117, V_118)!=skf12(U_117, V_118)))). % 27.74/18.15 tff(c_387, plain, (![U_17, V_18]: (~eventuality(U_17, V_18) | ~abstraction(U_17, V_18)))). % 27.74/18.15 tff(c_419, plain, (![U_373, V_374]: (nonliving(U_373, V_374) | ~food(U_373, V_374)))). % 27.74/18.15 tff(c_418, plain, (![U_373, V_374]: (entity(U_373, V_374) | ~food(U_373, V_374)))). % 27.74/18.15 tff(c_417, plain, (![U_373, V_374]: (~female(U_373, V_374) | ~food(U_373, V_374)))). % 27.74/18.15 tff(c_392, plain, (![U_365, V_366]: (~multiple(U_365, V_366) | ~abstraction(U_365, V_366)))). % 27.74/18.15 tff(c_116, plain, (![U_115, V_116]: (member(U_115, skf12(V_116, U_115), V_116) | ~five(U_115, V_116)))). % 27.74/18.15 tff(c_248, plain, (![U_21, V_22]: (multiple(U_21, V_22) | ~group(U_21, V_22)))). % 27.74/18.15 tff(c_437, plain, (~cost(skc5, skc9))). % 27.74/18.16 tff(c_436, plain, (~act(skc5, skc9))). % 27.74/18.16 tff(c_122, plain, (![V_122, U_121]: (~five(V_122, U_121) | skf20(U_121, V_122)!=skf16(U_121, V_122)))). % 27.74/18.16 tff(c_429, plain, (~event(skc5, skc9))). % 27.74/18.16 tff(c_425, plain, (~eventuality(skc5, skc9))). % 27.74/18.16 tff(c_319, plain, (![U_37, V_38]: (~female(U_37, V_38) | ~eventuality(U_37, V_38)))). % 27.74/18.16 tff(c_258, plain, (![U_49, V_50]: (object(U_49, V_50) | ~food(U_49, V_50)))). % 27.74/18.16 tff(c_240, plain, (![U_31, V_32]: (singleton(U_31, V_32) | ~eventuality(U_31, V_32)))). % 27.74/18.16 tff(c_130, plain, (![V_130, U_129]: (~five(V_130, U_129) | skf18(U_129, V_130)!=skf16(U_129, V_130)))). % 27.74/18.16 tff(c_341, plain, (![U_335, V_336]: (~female(U_335, V_336) | ~abstraction(U_335, V_336)))). % 27.74/18.16 tff(c_294, plain, (![U_313, V_314]: (singleton(U_313, V_314) | ~abstraction(U_313, V_314)))). % 27.74/18.16 tff(c_329, plain, (![U_33, V_34]: (~general(U_33, V_34) | ~eventuality(U_33, V_34)))). % 27.74/18.16 tff(c_126, plain, (![V_126, U_125]: (~five(V_126, U_125) | skf18(U_125, V_126)!=skf12(U_125, V_126)))). % 27.74/18.16 tff(c_304, plain, (![U_317, V_318]: (abstraction(U_317, V_318) | ~currency(U_317, V_318)))). % 27.74/18.16 tff(c_320, plain, (![U_65, V_66]: (~female(U_65, V_66) | ~object(U_65, V_66)))). % 27.74/18.16 tff(c_274, plain, (![U_297, V_298]: (~existent(U_297, V_298) | ~eventuality(U_297, V_298)))). % 27.74/18.16 tff(c_370, plain, (entity(skc5, skc9))). % 27.74/18.16 tff(c_253, plain, (![U_77, V_78]: (entity(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.74/18.16 tff(c_128, plain, (![V_128, U_127]: (~five(V_128, U_127) | skf18(U_127, V_128)!=skf14(U_127, V_128)))). % 27.74/18.16 tff(c_364, plain, (~abstraction(skc5, skc9))). % 27.74/18.16 tff(c_309, plain, (![U_319, V_320]: (~human(U_319, V_320) | ~abstraction(U_319, V_320)))). % 27.74/18.16 tff(c_206, plain, (![U_67, V_68]: (relation(U_67, V_68) | ~forename(U_67, V_68)))). % 27.74/18.16 tff(c_124, plain, (![V_124, U_123]: (~five(V_124, U_123) | skf20(U_123, V_124)!=skf18(U_123, V_124)))). % 27.74/18.16 tff(c_289, plain, (![U_311, V_312]: (singleton(U_311, V_312) | ~entity(U_311, V_312)))). % 27.74/18.16 tff(c_234, plain, (![U_77, V_78]: (living(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.74/18.16 tff(c_328, plain, (![U_57, V_58]: (~general(U_57, V_58) | ~entity(U_57, V_58)))). % 27.74/18.16 tff(c_268, plain, (![U_77, V_78]: (impartial(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.74/18.16 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~abstraction(U_19, V_20)))). % 27.74/18.16 tff(c_100, plain, (![U_99, V_100]: (~nonliving(U_99, V_100) | ~living(U_99, V_100)))). % 27.74/18.16 tff(c_335, plain, (human(skc5, skc9))). % 27.74/18.16 tff(c_86, plain, (![U_85, V_86]: (human(U_85, V_86) | ~human_person(U_85, V_86)))). % 27.74/18.16 tff(c_96, plain, (![U_95, V_96]: (~singleton(U_95, V_96) | ~multiple(U_95, V_96)))). % 27.74/18.16 tff(c_94, plain, (![U_93, V_94]: (~specific(U_93, V_94) | ~general(U_93, V_94)))). % 27.74/18.16 tff(c_92, plain, (![U_91, V_92]: (~unisex(U_91, V_92) | ~female(U_91, V_92)))). % 27.74/18.16 tff(c_30, plain, (![U_29, V_30]: (eventuality(U_29, V_30) | ~event(U_29, V_30)))). % 27.74/18.16 tff(c_98, plain, (![U_97, V_98]: (~present(U_97, V_98) | ~past(U_97, V_98)))). % 27.74/18.16 tff(c_16, plain, (![U_15, V_16]: (nonhuman(U_15, V_16) | ~abstraction(U_15, V_16)))). % 27.74/18.16 tff(c_299, plain, (female(skc5, skc9))). % 27.74/18.16 tff(c_8, plain, (![U_7, V_8]: (possession(U_7, V_8) | ~currency(U_7, V_8)))). % 27.74/18.16 tff(c_90, plain, (![U_89, V_90]: (female(U_89, V_90) | ~woman(U_89, V_90)))). % 27.74/18.16 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~abstraction(U_11, V_12)))). % 27.74/18.16 tff(c_56, plain, (![U_55, V_56]: (thing(U_55, V_56) | ~entity(U_55, V_56)))). % 27.74/18.16 tff(c_6, plain, (![U_5, V_6]: (currency(U_5, V_6) | ~cash(U_5, V_6)))). % 27.74/18.16 tff(c_102, plain, (![U_101, V_102]: (~nonhuman(U_101, V_102) | ~human(U_101, V_102)))). % 27.74/18.16 tff(c_72, plain, (![U_71, V_72]: (abstraction(U_71, V_72) | ~relation(U_71, V_72)))). % 27.74/18.16 tff(c_58, plain, (![U_57, V_58]: (specific(U_57, V_58) | ~entity(U_57, V_58)))). % 27.74/18.16 tff(c_280, plain, (animate(skc5, skc9))). % 27.74/18.16 tff(c_88, plain, (![U_87, V_88]: (animate(U_87, V_88) | ~human_person(U_87, V_88)))). % 27.74/18.16 tff(c_48, plain, (![U_47, V_48]: (food(U_47, V_48) | ~beverage(U_47, V_48)))). % 27.74/18.16 tff(c_36, plain, (![U_35, V_36]: (nonexistent(U_35, V_36) | ~eventuality(U_35, V_36)))). % 27.74/18.16 tff(c_10, plain, (![U_9, V_10]: (abstraction(U_9, V_10) | ~possession(U_9, V_10)))). % 27.74/18.16 tff(c_263, plain, (human_person(skc5, skc9))). % 27.74/18.16 tff(c_82, plain, (![U_81, V_82]: (impartial(U_81, V_82) | ~organism(U_81, V_82)))). % 27.74/18.16 tff(c_76, plain, (![U_75, V_76]: (human_person(U_75, V_76) | ~woman(U_75, V_76)))). % 27.74/18.16 tff(c_52, plain, (![U_51, V_52]: (object(U_51, V_52) | ~substance_matter(U_51, V_52)))). % 27.74/18.16 tff(c_80, plain, (![U_79, V_80]: (entity(U_79, V_80) | ~organism(U_79, V_80)))). % 27.74/18.16 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 27.74/18.16 tff(c_104, plain, (![U_103, V_104]: (~existent(U_103, V_104) | ~nonexistent(U_103, V_104)))). % 27.74/18.16 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~five(U_25, V_26)))). % 27.74/18.16 tff(c_54, plain, (![U_53, V_54]: (entity(U_53, V_54) | ~object(U_53, V_54)))). % 27.74/18.16 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 27.74/18.16 tff(c_32, plain, (![U_31, V_32]: (thing(U_31, V_32) | ~eventuality(U_31, V_32)))). % 27.74/18.16 tff(c_84, plain, (![U_83, V_84]: (living(U_83, V_84) | ~organism(U_83, V_84)))). % 27.74/18.16 tff(c_74, plain, (![U_73, V_74]: (forename(U_73, V_74) | ~mia_forename(U_73, V_74)))). % 27.74/18.16 tff(c_106, plain, (![U_105, V_106]: (~animate(U_105, V_106) | ~nonliving(U_105, V_106)))). % 27.74/18.16 tff(c_38, plain, (![U_37, V_38]: (unisex(U_37, V_38) | ~eventuality(U_37, V_38)))). % 27.74/18.16 tff(c_18, plain, (![U_17, V_18]: (general(U_17, V_18) | ~abstraction(U_17, V_18)))). % 27.74/18.16 tff(c_219, plain, (act(skc5, skc6))). % 27.74/18.16 tff(c_42, plain, (![U_41, V_42]: (event(U_41, V_42) | ~act(U_41, V_42)))). % 27.74/18.16 tff(c_40, plain, (![U_39, V_40]: (act(U_39, V_40) | ~order(U_39, V_40)))). % 27.74/18.16 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~cost(U_27, V_28)))). % 27.74/18.16 tff(c_62, plain, (![U_61, V_62]: (nonliving(U_61, V_62) | ~object(U_61, V_62)))). % 27.74/18.16 tff(c_44, plain, (![U_43, V_44]: (event(U_43, V_44) | ~order(U_43, V_44)))). % 27.74/18.16 tff(c_70, plain, (![U_69, V_70]: (relation(U_69, V_70) | ~relname(U_69, V_70)))). % 27.74/18.16 tff(c_50, plain, (![U_49, V_50]: (substance_matter(U_49, V_50) | ~food(U_49, V_50)))). % 27.74/18.16 tff(c_66, plain, (![U_65, V_66]: (unisex(U_65, V_66) | ~object(U_65, V_66)))). % 27.74/18.16 tff(c_60, plain, (![U_59, V_60]: (existent(U_59, V_60) | ~entity(U_59, V_60)))). % 27.74/18.16 tff(c_198, plain, (beverage(skc5, skc7))). % 27.74/18.16 tff(c_46, plain, (![U_45, V_46]: (beverage(U_45, V_46) | ~shake_beverage(U_45, V_46)))). % 27.74/18.16 tff(c_78, plain, (![U_77, V_78]: (organism(U_77, V_78) | ~human_person(U_77, V_78)))). % 27.74/18.16 tff(c_4, plain, (![U_3, V_4]: (cash(U_3, V_4) | ~dollar(U_3, V_4)))). % 27.74/18.16 tff(c_68, plain, (![U_67, V_68]: (relname(U_67, V_68) | ~forename(U_67, V_68)))). % 27.74/18.16 tff(c_34, plain, (![U_33, V_34]: (specific(U_33, V_34) | ~eventuality(U_33, V_34)))). % 27.74/18.16 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 27.74/18.16 tff(c_64, plain, (![U_63, V_64]: (impartial(U_63, V_64) | ~object(U_63, V_64)))). % 27.74/18.16 tff(c_176, plain, (agent(skc5, skc6, skc9))). % 27.74/18.16 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 27.74/18.16 tff(c_178, plain, (patient(skc5, skc6, skc7))). % 27.74/18.16 tff(c_174, plain, (of(skc5, skc8, skc9))). % 27.74/18.16 tff(c_162, plain, (order(skc5, skc6))). % 27.74/18.16 tff(c_160, plain, (shake_beverage(skc5, skc7))). % 27.74/18.16 tff(c_158, plain, (woman(skc5, skc9))). % 27.74/18.16 tff(c_164, plain, (nonreflexive(skc5, skc6))). % 27.74/18.16 tff(c_166, plain, (past(skc5, skc6))). % 27.74/18.16 tff(c_168, plain, (event(skc5, skc6))). % 27.74/18.16 tff(c_170, plain, (forename(skc5, skc8))). % 27.74/18.16 tff(c_172, plain, (mia_forename(skc5, skc8))). % 27.74/18.16 tff(c_156, plain, (actual_world(skc5))). % 27.74/18.16 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 27.74/18.16 %------------------------------------------------------------------------------