%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP082-1 : TPTP v9.0.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n015.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:09 PM UTC 2025 % Result : Satisfiable 56.65s 47.62s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : NLP082-1 : TPTP v9.0.0. Released v2.4.0. % 0.12/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n015.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.19/0.33 % WCLimit : 300 % 0.19/0.33 % DateTime : Tue Apr 8 08:25:05 EDT 2025 % 0.19/0.33 % CPUTime : % 56.65/47.62 % 56.65/47.62 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.65/47.62 % 56.65/47.62 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.65/47.63 %$ patient > of > member > from_loc > agent > weaponry > weapon > unisex > thing > specific > sound > six > singleton > shot > set > scream > revenge > present > organism > object > nonreflexive > nonliving > nonexistent > multiple > man > male > living > instrumentality > impartial > human_person > human > group > fire > existent > eventuality > event > entity > cry > cannon > artifact > animate > action > act > actual_world > skf21 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skf8 > skc9 > skc8 > skc15 > skc14 > skc13 > skc12 > skc11 > skc10 % 56.65/47.63 % 56.65/47.63 %Foreground sorts: % 56.65/47.63 % 56.65/47.63 % 56.65/47.63 %Background operators: % 56.65/47.63 % 56.65/47.63 % 56.65/47.63 %Foreground operators: % 56.65/47.63 tff(nonliving, type, nonliving: ($i * $i) > $o). % 56.65/47.63 tff(skf10, type, skf10: ($i * $i) > $i). % 56.65/47.63 tff(member, type, member: ($i * $i * $i) > $o). % 56.65/47.63 tff(living, type, living: ($i * $i) > $o). % 56.65/47.63 tff(fire, type, fire: ($i * $i) > $o). % 56.65/47.63 tff(human_person, type, human_person: ($i * $i) > $o). % 56.65/47.63 tff(action, type, action: ($i * $i) > $o). % 56.65/47.63 tff(present, type, present: ($i * $i) > $o). % 56.65/47.63 tff(shot, type, shot: ($i * $i) > $o). % 56.65/47.63 tff(skc11, type, skc11: $i). % 56.65/47.63 tff(entity, type, entity: ($i * $i) > $o). % 56.65/47.63 tff(skc9, type, skc9: $i). % 56.65/47.63 tff(eventuality, type, eventuality: ($i * $i) > $o). % 56.65/47.63 tff(weapon, type, weapon: ($i * $i) > $o). % 56.65/47.63 tff(existent, type, existent: ($i * $i) > $o). % 56.65/47.63 tff(skc8, type, skc8: $i). % 56.65/47.63 tff(scream, type, scream: ($i * $i) > $o). % 56.65/47.63 tff(skc14, type, skc14: $i). % 56.65/47.63 tff(singleton, type, singleton: ($i * $i) > $o). % 56.65/47.63 tff(skc13, type, skc13: $i). % 56.65/47.63 tff(male, type, male: ($i * $i) > $o). % 56.65/47.63 tff(skf8, type, skf8: $i > $i). % 56.65/47.63 tff(multiple, type, multiple: ($i * $i) > $o). % 56.65/47.63 tff(organism, type, organism: ($i * $i) > $o). % 56.65/47.63 tff(animate, type, animate: ($i * $i) > $o). % 56.65/47.63 tff(of, type, of: ($i * $i * $i) > $o). % 56.65/47.63 tff(skf14, type, skf14: ($i * $i) > $i). % 56.65/47.63 tff(actual_world, type, actual_world: $i > $o). % 56.65/47.63 tff(agent, type, agent: ($i * $i * $i) > $o). % 56.65/47.63 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 56.65/47.63 tff(group, type, group: ($i * $i) > $o). % 56.65/47.63 tff(revenge, type, revenge: ($i * $i) > $o). % 56.65/47.63 tff(skf21, type, skf21: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 56.65/47.63 tff(artifact, type, artifact: ($i * $i) > $o). % 56.65/47.63 tff(cannon, type, cannon: ($i * $i) > $o). % 56.65/47.63 tff(cry, type, cry: ($i * $i) > $o). % 56.65/47.63 tff(event, type, event: ($i * $i) > $o). % 56.65/47.63 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 56.65/47.63 tff(patient, type, patient: ($i * $i * $i) > $o). % 56.65/47.63 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 56.65/47.63 tff(thing, type, thing: ($i * $i) > $o). % 56.65/47.63 tff(skc15, type, skc15: $i). % 56.65/47.63 tff(human, type, human: ($i * $i) > $o). % 56.65/47.63 tff(six, type, six: ($i * $i) > $o). % 56.65/47.63 tff(skf18, type, skf18: ($i * $i) > $i). % 56.65/47.63 tff(man, type, man: ($i * $i) > $o). % 56.65/47.63 tff(sound, type, sound: ($i * $i) > $o). % 56.65/47.63 tff(weaponry, type, weaponry: ($i * $i) > $o). % 56.65/47.63 tff(unisex, type, unisex: ($i * $i) > $o). % 56.65/47.63 tff(skf16, type, skf16: ($i * $i) > $i). % 56.65/47.63 tff(set, type, set: ($i * $i) > $o). % 56.65/47.63 tff(skf12, type, skf12: ($i * $i) > $i). % 56.65/47.63 tff(impartial, type, impartial: ($i * $i) > $o). % 56.65/47.63 tff(object, type, object: ($i * $i) > $o). % 56.65/47.63 tff(skc12, type, skc12: $i). % 56.65/47.63 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 56.65/47.63 tff(specific, type, specific: ($i * $i) > $o). % 56.65/47.63 tff(skf20, type, skf20: ($i * $i) > $i). % 56.65/47.63 tff(skc10, type, skc10: $i). % 56.65/47.63 tff(act, type, act: ($i * $i) > $o). % 56.65/47.63 % 56.65/47.63 %Saturated clause set: % 56.65/47.64 tff(c_1548, plain, (![Z_1072, X_1079, V_1082, Y_1086, X_1053, X1_1078, U_203, V_1052, Y_1081, X_1067, X2_1051, Z_204, X_1063, X2_1062, X2_1074, Y_208, V_1070, X1_1083, X1_1088, Z_1061, W_1069, Z_1050, W_202, Z_1066, Y_1071, X2_1057, Y_1060, V_1077, X1_1068, X_1058, X1_205, X1_1064, X2_206, V_209, Z_1080, V_1054, X1_1075, X_1049, X_207, Y_1055, V_1076, X2_1065, Y_1073, Z_1084, X2_1059]: (skf21(V_1082, X_1058, Y_1071, Z_1084, X1_1083, X2_1062, W_202, U_203)=skf21(V_1052, X_1049, Y_1073, Z_1061, X1_1068, X2_1057, W_202, U_203) | skf21(V_1077, X_1067, Y_1060, Z_1080, X1_1078, X2_1065, W_202, U_203)=skf21(V_1052, X_1049, Y_1073, Z_1061, X1_1068, X2_1057, W_202, U_203) | skf21(V_1082, X_1058, Y_1071, Z_1084, X1_1083, X2_1062, W_202, U_203)=skf21(V_1077, X_1067, Y_1060, Z_1080, X1_1078, X2_1065, W_202, U_203) | skf21(V_1077, X_1067, Y_1060, Z_1080, X1_1078, X2_1065, W_202, U_203)=skf21(V_1076, X_1079, Y_1055, Z_1066, X1_1088, X2_1059, W_202, U_203) | skf21(V_1076, X_1079, Y_1055, Z_1066, X1_1088, X2_1059, W_202, U_203)=skf21(V_1052, X_1049, Y_1073, Z_1061, X1_1068, X2_1057, W_202, U_203) | skf21(V_1082, X_1058, Y_1071, Z_1084, X1_1083, X2_1062, W_202, U_203)=skf21(V_1076, X_1079, Y_1055, Z_1066, X1_1088, X2_1059, W_202, U_203) | skf21(V_1076, X_1079, Y_1055, Z_1066, X1_1088, X2_1059, W_202, U_203)=skf21(V_1070, X_1063, Y_1086, Z_1050, X1_1075, X2_1074, W_202, U_203) | skf21(V_1077, X_1067, Y_1060, Z_1080, X1_1078, X2_1065, W_202, U_203)=skf21(V_1070, X_1063, Y_1086, Z_1050, X1_1075, X2_1074, W_202, U_203) | skf21(V_1070, X_1063, Y_1086, Z_1050, X1_1075, X2_1074, W_202, U_203)=skf21(V_1052, X_1049, Y_1073, Z_1061, X1_1068, X2_1057, W_202, U_203) | skf21(V_1082, X_1058, Y_1071, Z_1084, X1_1083, X2_1062, W_202, U_203)=skf21(V_1070, X_1063, Y_1086, Z_1050, X1_1075, X2_1074, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1070, X_1063, Y_1086, Z_1050, X1_1075, X2_1074, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1076, X_1079, Y_1055, Z_1066, X1_1088, X2_1059, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1077, X_1067, Y_1060, Z_1080, X1_1078, X2_1065, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1052, X_1049, Y_1073, Z_1061, X1_1068, X2_1057, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1082, X_1058, Y_1071, Z_1084, X1_1083, X2_1062, W_202, U_203) | skf21(skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), V_1054, W_1069, X_1053, Y_1081, Z_1072, X1_1064, X2_1051)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_1062=X1_1083 | Z_1084=X1_1083 | Z_1084=X2_1062 | Z_1084=Y_1071 | Y_1071=X1_1083 | Y_1071=X2_1062 | Y_1071=X_1058 | Z_1084=X_1058 | X_1058=X1_1083 | X_1058=X2_1062 | X_1058=V_1082 | Y_1071=V_1082 | Z_1084=V_1082 | X1_1083=V_1082 | X2_1062=V_1082 | ~member(U_203, X2_1062, W_202) | ~member(U_203, X1_1083, W_202) | ~member(U_203, Z_1084, W_202) | ~member(U_203, Y_1071, W_202) | ~member(U_203, X_1058, W_202) | ~member(U_203, V_1082, W_202) | X2_1057=X1_1068 | Z_1061=X1_1068 | Z_1061=X2_1057 | Z_1061=Y_1073 | Y_1073=X1_1068 | Y_1073=X2_1057 | Y_1073=X_1049 | Z_1061=X_1049 | X_1049=X1_1068 | X_1049=X2_1057 | X_1049=V_1052 | Y_1073=V_1052 | Z_1061=V_1052 | X1_1068=V_1052 | X2_1057=V_1052 | ~member(U_203, X2_1057, W_202) | ~member(U_203, X1_1068, W_202) | ~member(U_203, Z_1061, W_202) | ~member(U_203, Y_1073, W_202) | ~member(U_203, X_1049, W_202) | ~member(U_203, V_1052, W_202) | X2_1065=X1_1078 | Z_1080=X1_1078 | Z_1080=X2_1065 | Z_1080=Y_1060 | Y_1060=X1_1078 | Y_1060=X2_1065 | Y_1060=X_1067 | Z_1080=X_1067 | X_1067=X1_1078 | X_1067=X2_1065 | X_1067=V_1077 | Y_1060=V_1077 | Z_1080=V_1077 | X1_1078=V_1077 | X2_1065=V_1077 | ~member(U_203, X2_1065, W_202) | ~member(U_203, X1_1078, W_202) | ~member(U_203, Z_1080, W_202) | ~member(U_203, Y_1060, W_202) | ~member(U_203, X_1067, W_202) | ~member(U_203, V_1077, W_202) | X2_1059=X1_1088 | Z_1066=X1_1088 | Z_1066=X2_1059 | Z_1066=Y_1055 | Y_1055=X1_1088 | Y_1055=X2_1059 | Y_1055=X_1079 | Z_1066=X_1079 | X_1079=X1_1088 | X_1079=X2_1059 | X_1079=V_1076 | Y_1055=V_1076 | Z_1066=V_1076 | X1_1088=V_1076 | X2_1059=V_1076 | ~member(U_203, X2_1059, W_202) | ~member(U_203, X1_1088, W_202) | ~member(U_203, Z_1066, W_202) | ~member(U_203, Y_1055, W_202) | ~member(U_203, X_1079, W_202) | ~member(U_203, V_1076, W_202) | X2_1074=X1_1075 | Z_1050=X1_1075 | Z_1050=X2_1074 | Z_1050=Y_1086 | Y_1086=X1_1075 | Y_1086=X2_1074 | Y_1086=X_1063 | Z_1050=X_1063 | X_1063=X1_1075 | X_1063=X2_1074 | X_1063=V_1070 | Y_1086=V_1070 | Z_1050=V_1070 | X1_1075=V_1070 | X2_1074=V_1070 | ~member(U_203, X2_1074, W_202) | ~member(U_203, X1_1075, W_202) | ~member(U_203, Z_1050, W_202) | ~member(U_203, Y_1086, W_202) | ~member(U_203, X_1063, W_202) | ~member(U_203, V_1070, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.64 tff(c_1525, plain, (![V_1012, X_1009, Y_1010, V_995, X2_999, V_1005, W_984, Y_998, U_203, X1_1002, X2_985, X1_1006, X1_994, X2_1000, X2_993, X1_1001, X_1004, Z_204, Y_208, X_1011, Y_992, W_202, Z_1008, X_1003, Y_1015, X1_205, V_1007, X_990, X2_986, X2_206, Z_991, V_209, X_207, Y_988, X1_982, Z_989, Z_983, Z_996, U_997]: (skf21(V_1012, X_1004, Y_998, Z_996, X1_994, X2_1000, W_202, U_203)=skf21(V_1007, X_1009, Y_988, Z_1008, X1_982, X2_986, W_202, U_203) | skf21(V_1007, X_1009, Y_988, Z_1008, X1_982, X2_986, W_202, U_203)=skf21(V_1005, X_1003, Y_1015, Z_991, X1_1002, X2_993, W_202, U_203) | skf21(V_1012, X_1004, Y_998, Z_996, X1_994, X2_1000, W_202, U_203)=skf21(V_1005, X_1003, Y_1015, Z_991, X1_1002, X2_993, W_202, U_203) | skf21(V_995, X_990, Y_1010, Z_983, X1_1001, X2_999, W_202, U_203)=skf21(V_1005, X_1003, Y_1015, Z_991, X1_1002, X2_993, W_202, U_203) | skf21(V_995, X_990, Y_1010, Z_983, X1_1001, X2_999, W_202, U_203)=skf21(V_1007, X_1009, Y_988, Z_1008, X1_982, X2_986, W_202, U_203) | skf21(V_995, X_990, Y_1010, Z_983, X1_1001, X2_999, W_202, U_203)=skf21(V_1012, X_1004, Y_998, Z_996, X1_994, X2_1000, W_202, U_203) | skf21(V_995, X_990, Y_1010, Z_983, X1_1001, X2_999, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1005, X_1003, Y_1015, Z_991, X1_1002, X2_993, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1007, X_1009, Y_988, Z_1008, X1_982, X2_986, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=skf21(V_1012, X_1004, Y_998, Z_996, X1_994, X2_1000, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_997 | skf21(V_995, X_990, Y_1010, Z_983, X1_1001, X2_999, W_202, U_203)=U_997 | skf21(V_1005, X_1003, Y_1015, Z_991, X1_1002, X2_993, W_202, U_203)=U_997 | skf21(V_1007, X_1009, Y_988, Z_1008, X1_982, X2_986, W_202, U_203)=U_997 | skf21(V_1012, X_1004, Y_998, Z_996, X1_994, X2_1000, W_202, U_203)=U_997 | ~member(U_203, U_997, W_202) | skf21(U_997, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), W_984, X_1011, Y_992, Z_989, X1_1006, X2_985)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_1000=X1_994 | Z_996=X1_994 | Z_996=X2_1000 | Z_996=Y_998 | Y_998=X1_994 | Y_998=X2_1000 | Y_998=X_1004 | Z_996=X_1004 | X_1004=X1_994 | X_1004=X2_1000 | X_1004=V_1012 | Y_998=V_1012 | Z_996=V_1012 | X1_994=V_1012 | X2_1000=V_1012 | ~member(U_203, X2_1000, W_202) | ~member(U_203, X1_994, W_202) | ~member(U_203, Z_996, W_202) | ~member(U_203, Y_998, W_202) | ~member(U_203, X_1004, W_202) | ~member(U_203, V_1012, W_202) | X2_986=X1_982 | Z_1008=X1_982 | Z_1008=X2_986 | Z_1008=Y_988 | Y_988=X1_982 | Y_988=X2_986 | Y_988=X_1009 | Z_1008=X_1009 | X_1009=X1_982 | X_1009=X2_986 | X_1009=V_1007 | Y_988=V_1007 | Z_1008=V_1007 | X1_982=V_1007 | X2_986=V_1007 | ~member(U_203, X2_986, W_202) | ~member(U_203, X1_982, W_202) | ~member(U_203, Z_1008, W_202) | ~member(U_203, Y_988, W_202) | ~member(U_203, X_1009, W_202) | ~member(U_203, V_1007, W_202) | X2_993=X1_1002 | Z_991=X1_1002 | Z_991=X2_993 | Z_991=Y_1015 | Y_1015=X1_1002 | Y_1015=X2_993 | Y_1015=X_1003 | Z_991=X_1003 | X_1003=X1_1002 | X_1003=X2_993 | X_1003=V_1005 | Y_1015=V_1005 | Z_991=V_1005 | X1_1002=V_1005 | X2_993=V_1005 | ~member(U_203, X2_993, W_202) | ~member(U_203, X1_1002, W_202) | ~member(U_203, Z_991, W_202) | ~member(U_203, Y_1015, W_202) | ~member(U_203, X_1003, W_202) | ~member(U_203, V_1005, W_202) | X2_999=X1_1001 | Z_983=X1_1001 | Z_983=X2_999 | Z_983=Y_1010 | Y_1010=X1_1001 | Y_1010=X2_999 | Y_1010=X_990 | Z_983=X_990 | X_990=X1_1001 | X_990=X2_999 | X_990=V_995 | Y_1010=V_995 | Z_983=V_995 | X1_1001=V_995 | X2_999=V_995 | ~member(U_203, X2_999, W_202) | ~member(U_203, X1_1001, W_202) | ~member(U_203, Z_983, W_202) | ~member(U_203, Y_1010, W_202) | ~member(U_203, X_990, W_202) | ~member(U_203, V_995, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.64 tff(c_1503, plain, (![Z_981, Y_971, U_968, Y_976, Y_960, X_948, X2_963, Z_977, X1_952, V_951, V_962, X1_974, U_203, X1_967, Y_969, X1_956, W_947, X2_975, Z_204, X_949, Y_208, W_202, X_972, Z_957, Y_978, Z_964, X1_205, V_965, X1_961, X2_206, V_209, X_953, X2_954, X_207, X_958, Z_950, V_970, X2_973, X2_966, V_959]: (skf21(V_965, X_953, Y_969, Z_957, X1_956, X2_973, W_202, U_203)=skf21(V_959, X_972, Y_971, Z_977, X1_952, X2_975, W_202, U_203) | skf21(V_965, X_953, Y_969, Z_957, X1_956, X2_973, W_202, U_203)=skf21(V_951, X_948, Y_976, Z_981, X1_974, X2_954, W_202, U_203) | skf21(V_959, X_972, Y_971, Z_977, X1_952, X2_975, W_202, U_203)=skf21(V_951, X_948, Y_976, Z_981, X1_974, X2_954, W_202, U_203) | skf21(V_962, X_958, Y_978, Z_950, X1_967, X2_966, W_202, U_203)=skf21(V_951, X_948, Y_976, Z_981, X1_974, X2_954, W_202, U_203) | skf21(V_965, X_953, Y_969, Z_957, X1_956, X2_973, W_202, U_203)=skf21(V_962, X_958, Y_978, Z_950, X1_967, X2_966, W_202, U_203) | skf21(V_962, X_958, Y_978, Z_950, X1_967, X2_966, W_202, U_203)=skf21(V_959, X_972, Y_971, Z_977, X1_952, X2_975, W_202, U_203) | skf21(V_962, X_958, Y_978, Z_950, X1_967, X2_966, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_951, X_948, Y_976, Z_981, X1_974, X2_954, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_965, X_953, Y_969, Z_957, X1_956, X2_973, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_959, X_972, Y_971, Z_977, X1_952, X2_975, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_968 | skf21(V_962, X_958, Y_978, Z_950, X1_967, X2_966, W_202, U_203)=U_968 | skf21(V_951, X_948, Y_976, Z_981, X1_974, X2_954, W_202, U_203)=U_968 | skf21(V_965, X_953, Y_969, Z_957, X1_956, X2_973, W_202, U_203)=U_968 | skf21(V_959, X_972, Y_971, Z_977, X1_952, X2_975, W_202, U_203)=U_968 | ~member(U_203, U_968, W_202) | skf21(U_968, V_970, W_947, X_949, Y_960, Z_964, X1_961, X2_963)!=U_968 | X2_975=X1_952 | Z_977=X1_952 | Z_977=X2_975 | Z_977=Y_971 | Y_971=X1_952 | Y_971=X2_975 | Y_971=X_972 | Z_977=X_972 | X_972=X1_952 | X_972=X2_975 | X_972=V_959 | Y_971=V_959 | Z_977=V_959 | X1_952=V_959 | X2_975=V_959 | ~member(U_203, X2_975, W_202) | ~member(U_203, X1_952, W_202) | ~member(U_203, Z_977, W_202) | ~member(U_203, Y_971, W_202) | ~member(U_203, X_972, W_202) | ~member(U_203, V_959, W_202) | X2_973=X1_956 | Z_957=X1_956 | Z_957=X2_973 | Z_957=Y_969 | Y_969=X1_956 | Y_969=X2_973 | Y_969=X_953 | Z_957=X_953 | X_953=X1_956 | X_953=X2_973 | X_953=V_965 | Y_969=V_965 | Z_957=V_965 | X1_956=V_965 | X2_973=V_965 | ~member(U_203, X2_973, W_202) | ~member(U_203, X1_956, W_202) | ~member(U_203, Z_957, W_202) | ~member(U_203, Y_969, W_202) | ~member(U_203, X_953, W_202) | ~member(U_203, V_965, W_202) | X2_954=X1_974 | Z_981=X1_974 | Z_981=X2_954 | Z_981=Y_976 | Y_976=X1_974 | Y_976=X2_954 | Y_976=X_948 | Z_981=X_948 | X_948=X1_974 | X_948=X2_954 | X_948=V_951 | Y_976=V_951 | Z_981=V_951 | X1_974=V_951 | X2_954=V_951 | ~member(U_203, X2_954, W_202) | ~member(U_203, X1_974, W_202) | ~member(U_203, Z_981, W_202) | ~member(U_203, Y_976, W_202) | ~member(U_203, X_948, W_202) | ~member(U_203, V_951, W_202) | X2_966=X1_967 | Z_950=X1_967 | Z_950=X2_966 | Z_950=Y_978 | Y_978=X1_967 | Y_978=X2_966 | Y_978=X_958 | Z_950=X_958 | X_958=X1_967 | X_958=X2_966 | X_958=V_962 | Y_978=V_962 | Z_950=V_962 | X1_967=V_962 | X2_966=V_962 | ~member(U_203, X2_966, W_202) | ~member(U_203, X1_967, W_202) | ~member(U_203, Z_950, W_202) | ~member(U_203, Y_978, W_202) | ~member(U_203, X_958, W_202) | ~member(U_203, V_962, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.64 tff(c_1458, plain, (![X_873, X2_865, X1_881, U_203, Z_874, Z_864, Y_884, X_878, Y_867, Z_204, Y_208, V_875, Z_863, W_202, V_885, X1_872, X_871, X1_205, U_870, Z_882, Y_888, X2_206, V_866, X2_883, X1_862, V_209, V_877, X2_880, X_207, X1_886, Y_887, X2_868, X_879]: (skf21(V_885, X_879, Y_884, Z_864, X1_862, X2_883, W_202, U_203)=skf21(V_866, X_873, Y_867, Z_882, X1_886, X2_868, W_202, U_203) | skf21(V_885, X_879, Y_884, Z_864, X1_862, X2_883, W_202, U_203)=skf21(V_875, X_871, Y_888, Z_863, X1_881, X2_880, W_202, U_203) | skf21(V_875, X_871, Y_888, Z_863, X1_881, X2_880, W_202, U_203)=skf21(V_866, X_873, Y_867, Z_882, X1_886, X2_868, W_202, U_203) | skf21(V_875, X_871, Y_888, Z_863, X1_881, X2_880, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_885, X_879, Y_884, Z_864, X1_862, X2_883, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_866, X_873, Y_867, Z_882, X1_886, X2_868, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_877 | skf21(V_875, X_871, Y_888, Z_863, X1_881, X2_880, W_202, U_203)=V_877 | skf21(V_885, X_879, Y_884, Z_864, X1_862, X2_883, W_202, U_203)=V_877 | skf21(V_866, X_873, Y_867, Z_882, X1_886, X2_868, W_202, U_203)=V_877 | V_877=U_870 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_870 | skf21(V_875, X_871, Y_888, Z_863, X1_881, X2_880, W_202, U_203)=U_870 | skf21(V_885, X_879, Y_884, Z_864, X1_862, X2_883, W_202, U_203)=U_870 | skf21(V_866, X_873, Y_867, Z_882, X1_886, X2_868, W_202, U_203)=U_870 | ~member(U_203, V_877, W_202) | ~member(U_203, U_870, W_202) | skf21(U_870, V_877, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), X_878, Y_887, Z_874, X1_872, X2_865)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_868=X1_886 | Z_882=X1_886 | Z_882=X2_868 | Z_882=Y_867 | Y_867=X1_886 | Y_867=X2_868 | Y_867=X_873 | Z_882=X_873 | X_873=X1_886 | X_873=X2_868 | X_873=V_866 | Y_867=V_866 | Z_882=V_866 | X1_886=V_866 | X2_868=V_866 | ~member(U_203, X2_868, W_202) | ~member(U_203, X1_886, W_202) | ~member(U_203, Z_882, W_202) | ~member(U_203, Y_867, W_202) | ~member(U_203, X_873, W_202) | ~member(U_203, V_866, W_202) | X2_883=X1_862 | Z_864=X1_862 | Z_864=X2_883 | Z_864=Y_884 | Y_884=X1_862 | Y_884=X2_883 | Y_884=X_879 | Z_864=X_879 | X_879=X1_862 | X_879=X2_883 | X_879=V_885 | Y_884=V_885 | Z_864=V_885 | X1_862=V_885 | X2_883=V_885 | ~member(U_203, X2_883, W_202) | ~member(U_203, X1_862, W_202) | ~member(U_203, Z_864, W_202) | ~member(U_203, Y_884, W_202) | ~member(U_203, X_879, W_202) | ~member(U_203, V_885, W_202) | X2_880=X1_881 | Z_863=X1_881 | Z_863=X2_880 | Z_863=Y_888 | Y_888=X1_881 | Y_888=X2_880 | Y_888=X_871 | Z_863=X_871 | X_871=X1_881 | X_871=X2_880 | X_871=V_875 | Y_888=V_875 | Z_863=V_875 | X1_881=V_875 | X2_880=V_875 | ~member(U_203, X2_880, W_202) | ~member(U_203, X1_881, W_202) | ~member(U_203, Z_863, W_202) | ~member(U_203, Y_888, W_202) | ~member(U_203, X_871, W_202) | ~member(U_203, V_875, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.64 tff(c_1436, plain, (![X_858, U_849, Z_840, U_203, X_833, Z_853, X1_848, Z_835, Z_857, Y_854, Z_204, X_845, Y_208, Y_847, V_843, W_859, W_202, Y_860, X1_834, Y_844, X1_861, X_839, X1_850, X2_852, X1_205, X2_842, X2_206, V_841, V_209, X2_851, X_207, X2_846, V_836, V_855]: (skf21(V_855, X_845, Y_860, Z_840, X1_850, X2_851, W_202, U_203)=skf21(V_836, X_858, Y_847, Z_857, X1_834, X2_842, W_202, U_203) | skf21(V_843, X_839, Y_854, Z_835, X1_848, X2_846, W_202, U_203)=skf21(V_836, X_858, Y_847, Z_857, X1_834, X2_842, W_202, U_203) | skf21(V_855, X_845, Y_860, Z_840, X1_850, X2_851, W_202, U_203)=skf21(V_843, X_839, Y_854, Z_835, X1_848, X2_846, W_202, U_203) | skf21(V_843, X_839, Y_854, Z_835, X1_848, X2_846, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_836, X_858, Y_847, Z_857, X1_834, X2_842, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_855, X_845, Y_860, Z_840, X1_850, X2_851, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_841 | skf21(V_843, X_839, Y_854, Z_835, X1_848, X2_846, W_202, U_203)=V_841 | skf21(V_836, X_858, Y_847, Z_857, X1_834, X2_842, W_202, U_203)=V_841 | skf21(V_855, X_845, Y_860, Z_840, X1_850, X2_851, W_202, U_203)=V_841 | V_841=U_849 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_849 | skf21(V_843, X_839, Y_854, Z_835, X1_848, X2_846, W_202, U_203)=U_849 | skf21(V_836, X_858, Y_847, Z_857, X1_834, X2_842, W_202, U_203)=U_849 | skf21(V_855, X_845, Y_860, Z_840, X1_850, X2_851, W_202, U_203)=U_849 | ~member(U_203, V_841, W_202) | ~member(U_203, U_849, W_202) | skf21(U_849, V_841, W_859, X_833, Y_844, Z_853, X1_861, X2_852)!=V_841 | X2_851=X1_850 | Z_840=X1_850 | Z_840=X2_851 | Z_840=Y_860 | Y_860=X1_850 | Y_860=X2_851 | Y_860=X_845 | Z_840=X_845 | X_845=X1_850 | X_845=X2_851 | X_845=V_855 | Y_860=V_855 | Z_840=V_855 | X1_850=V_855 | X2_851=V_855 | ~member(U_203, X2_851, W_202) | ~member(U_203, X1_850, W_202) | ~member(U_203, Z_840, W_202) | ~member(U_203, Y_860, W_202) | ~member(U_203, X_845, W_202) | ~member(U_203, V_855, W_202) | X2_842=X1_834 | Z_857=X1_834 | Z_857=X2_842 | Z_857=Y_847 | Y_847=X1_834 | Y_847=X2_842 | Y_847=X_858 | Z_857=X_858 | X_858=X1_834 | X_858=X2_842 | X_858=V_836 | Y_847=V_836 | Z_857=V_836 | X1_834=V_836 | X2_842=V_836 | ~member(U_203, X2_842, W_202) | ~member(U_203, X1_834, W_202) | ~member(U_203, Z_857, W_202) | ~member(U_203, Y_847, W_202) | ~member(U_203, X_858, W_202) | ~member(U_203, V_836, W_202) | X2_846=X1_848 | Z_835=X1_848 | Z_835=X2_846 | Z_835=Y_854 | Y_854=X1_848 | Y_854=X2_846 | Y_854=X_839 | Z_835=X_839 | X_839=X1_848 | X_839=X2_846 | X_839=V_843 | Y_854=V_843 | Z_835=V_843 | X1_848=V_843 | X2_846=V_843 | ~member(U_203, X2_846, W_202) | ~member(U_203, X1_848, W_202) | ~member(U_203, Z_835, W_202) | ~member(U_203, Y_854, W_202) | ~member(U_203, X_839, W_202) | ~member(U_203, V_843, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.64 tff(c_1480, plain, (![X2_900, Y_905, W_890, V_907, X_891, X1_911, Z_902, X1_909, U_203, X1_916, Z_914, X2_913, V_912, Z_204, X_903, Y_208, Z_897, X5_918, V_915, W_202, X1_899, X2_908, X1_205, Z_893, Y_892, Y_904, Y_917, X2_206, V_209, X_207, V_896, X_906, X_901, U_898, X2_894]: (skf21(V_915, X_891, Y_905, Z_897, X1_911, X2_913, W_202, U_203)=skf21(V_912, X_901, Y_892, Z_914, X1_899, X2_894, W_202, U_203) | skf21(V_912, X_901, Y_892, Z_914, X1_899, X2_894, W_202, U_203)=skf21(V_907, X_903, Y_917, Z_893, X1_909, X2_908, W_202, U_203) | skf21(V_915, X_891, Y_905, Z_897, X1_911, X2_913, W_202, U_203)=skf21(V_907, X_903, Y_917, Z_893, X1_909, X2_908, W_202, U_203) | skf21(V_907, X_903, Y_917, Z_893, X1_909, X2_908, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_912, X_901, Y_892, Z_914, X1_899, X2_894, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_915, X_891, Y_905, Z_897, X1_911, X2_913, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_918 | skf21(V_907, X_903, Y_917, Z_893, X1_909, X2_908, W_202, U_203)=X5_918 | skf21(V_912, X_901, Y_892, Z_914, X1_899, X2_894, W_202, U_203)=X5_918 | skf21(V_915, X_891, Y_905, Z_897, X1_911, X2_913, W_202, U_203)=X5_918 | X5_918=U_898 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_898 | skf21(V_907, X_903, Y_917, Z_893, X1_909, X2_908, W_202, U_203)=U_898 | skf21(V_912, X_901, Y_892, Z_914, X1_899, X2_894, W_202, U_203)=U_898 | skf21(V_915, X_891, Y_905, Z_897, X1_911, X2_913, W_202, U_203)=U_898 | ~member(U_203, X5_918, W_202) | ~member(U_203, U_898, W_202) | skf21(U_898, V_896, W_890, X_906, Y_904, Z_902, X1_916, X2_900)!=U_898 | X2_913=X1_911 | Z_897=X1_911 | Z_897=X2_913 | Z_897=Y_905 | Y_905=X1_911 | Y_905=X2_913 | Y_905=X_891 | Z_897=X_891 | X_891=X1_911 | X_891=X2_913 | X_891=V_915 | Y_905=V_915 | Z_897=V_915 | X1_911=V_915 | X2_913=V_915 | ~member(U_203, X2_913, W_202) | ~member(U_203, X1_911, W_202) | ~member(U_203, Z_897, W_202) | ~member(U_203, Y_905, W_202) | ~member(U_203, X_891, W_202) | ~member(U_203, V_915, W_202) | X2_894=X1_899 | Z_914=X1_899 | Z_914=X2_894 | Z_914=Y_892 | Y_892=X1_899 | Y_892=X2_894 | Y_892=X_901 | Z_914=X_901 | X_901=X1_899 | X_901=X2_894 | X_901=V_912 | Y_892=V_912 | Z_914=V_912 | X1_899=V_912 | X2_894=V_912 | ~member(U_203, X2_894, W_202) | ~member(U_203, X1_899, W_202) | ~member(U_203, Z_914, W_202) | ~member(U_203, Y_892, W_202) | ~member(U_203, X_901, W_202) | ~member(U_203, V_912, W_202) | X2_908=X1_909 | Z_893=X1_909 | Z_893=X2_908 | Z_893=Y_917 | Y_917=X1_909 | Y_917=X2_908 | Y_917=X_903 | Z_893=X_903 | X_903=X1_909 | X_903=X2_908 | X_903=V_907 | Y_917=V_907 | Z_893=V_907 | X1_909=V_907 | X2_908=V_907 | ~member(U_203, X2_908, W_202) | ~member(U_203, X1_909, W_202) | ~member(U_203, Z_893, W_202) | ~member(U_203, Y_917, W_202) | ~member(U_203, X_903, W_202) | ~member(U_203, V_907, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.64 tff(c_1369, plain, (![V_746, U_741, Y_759, U_203, X_748, X_760, Y_758, Z_204, X1_754, Y_761, X2_743, Y_208, W_202, W_744, Z_747, Z_752, V_751, X1_205, V_749, X2_206, V_209, X2_756, X1_757, X_207, X2_753, X1_750, Z_742]: (skf21(V_751, X_748, Y_761, Z_742, X1_754, X2_753, W_202, U_203)=skf21(V_749, X_760, Y_758, Z_752, X1_757, X2_743, W_202, U_203) | skf21(V_751, X_748, Y_761, Z_742, X1_754, X2_753, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_749, X_760, Y_758, Z_752, X1_757, X2_743, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_744 | skf21(V_751, X_748, Y_761, Z_742, X1_754, X2_753, W_202, U_203)=W_744 | skf21(V_749, X_760, Y_758, Z_752, X1_757, X2_743, W_202, U_203)=W_744 | W_744=V_746 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_746 | skf21(V_751, X_748, Y_761, Z_742, X1_754, X2_753, W_202, U_203)=V_746 | skf21(V_749, X_760, Y_758, Z_752, X1_757, X2_743, W_202, U_203)=V_746 | V_746=U_741 | W_744=U_741 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_741 | skf21(V_751, X_748, Y_761, Z_742, X1_754, X2_753, W_202, U_203)=U_741 | skf21(V_749, X_760, Y_758, Z_752, X1_757, X2_743, W_202, U_203)=U_741 | ~member(U_203, W_744, W_202) | ~member(U_203, V_746, W_202) | ~member(U_203, U_741, W_202) | skf21(U_741, V_746, W_744, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), Y_759, Z_747, X1_750, X2_756)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_743=X1_757 | Z_752=X1_757 | Z_752=X2_743 | Z_752=Y_758 | Y_758=X1_757 | Y_758=X2_743 | Y_758=X_760 | Z_752=X_760 | X_760=X1_757 | X_760=X2_743 | X_760=V_749 | Y_758=V_749 | Z_752=V_749 | X1_757=V_749 | X2_743=V_749 | ~member(U_203, X2_743, W_202) | ~member(U_203, X1_757, W_202) | ~member(U_203, Z_752, W_202) | ~member(U_203, Y_758, W_202) | ~member(U_203, X_760, W_202) | ~member(U_203, V_749, W_202) | X2_753=X1_754 | Z_742=X1_754 | Z_742=X2_753 | Z_742=Y_761 | Y_761=X1_754 | Y_761=X2_753 | Y_761=X_748 | Z_742=X_748 | X_748=X1_754 | X_748=X2_753 | X_748=V_751 | Y_761=V_751 | Z_742=V_751 | X1_754=V_751 | X2_753=V_751 | ~member(U_203, X2_753, W_202) | ~member(U_203, X1_754, W_202) | ~member(U_203, Z_742, W_202) | ~member(U_203, Y_761, W_202) | ~member(U_203, X_748, W_202) | ~member(U_203, V_751, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.64 tff(c_1391, plain, (![X6_771, X1_778, W_781, X2_787, Y_777, V_772, U_203, Y_782, X5_774, Z_767, X1_770, Z_204, X_763, X_769, Y_208, X1_776, W_202, Z_766, X2_786, U_780, V_785, X1_205, X2_206, V_765, V_209, X2_775, X_207, Z_764, Y_773, X_783]: (skf21(V_772, X_769, Y_782, Z_764, X1_776, X2_775, W_202, U_203)=skf21(V_765, X_783, Y_777, Z_766, X1_778, X2_787, W_202, U_203) | skf21(V_772, X_769, Y_782, Z_764, X1_776, X2_775, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_765, X_783, Y_777, Z_766, X1_778, X2_787, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X6_771 | skf21(V_772, X_769, Y_782, Z_764, X1_776, X2_775, W_202, U_203)=X6_771 | skf21(V_765, X_783, Y_777, Z_766, X1_778, X2_787, W_202, U_203)=X6_771 | X6_771=X5_774 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_774 | skf21(V_772, X_769, Y_782, Z_764, X1_776, X2_775, W_202, U_203)=X5_774 | skf21(V_765, X_783, Y_777, Z_766, X1_778, X2_787, W_202, U_203)=X5_774 | X5_774=U_780 | X6_771=U_780 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_780 | skf21(V_772, X_769, Y_782, Z_764, X1_776, X2_775, W_202, U_203)=U_780 | skf21(V_765, X_783, Y_777, Z_766, X1_778, X2_787, W_202, U_203)=U_780 | ~member(U_203, X6_771, W_202) | ~member(U_203, X5_774, W_202) | ~member(U_203, U_780, W_202) | skf21(U_780, V_785, W_781, X_763, Y_773, Z_767, X1_770, X2_786)!=U_780 | X2_787=X1_778 | Z_766=X1_778 | Z_766=X2_787 | Z_766=Y_777 | Y_777=X1_778 | Y_777=X2_787 | Y_777=X_783 | Z_766=X_783 | X_783=X1_778 | X_783=X2_787 | X_783=V_765 | Y_777=V_765 | Z_766=V_765 | X1_778=V_765 | X2_787=V_765 | ~member(U_203, X2_787, W_202) | ~member(U_203, X1_778, W_202) | ~member(U_203, Z_766, W_202) | ~member(U_203, Y_777, W_202) | ~member(U_203, X_783, W_202) | ~member(U_203, V_765, W_202) | X2_775=X1_776 | Z_764=X1_776 | Z_764=X2_775 | Z_764=Y_782 | Y_782=X1_776 | Y_782=X2_775 | Y_782=X_769 | Z_764=X_769 | X_769=X1_776 | X_769=X2_775 | X_769=V_772 | Y_782=V_772 | Z_764=V_772 | X1_776=V_772 | X2_775=V_772 | ~member(U_203, X2_775, W_202) | ~member(U_203, X1_776, W_202) | ~member(U_203, Z_764, W_202) | ~member(U_203, Y_782, W_202) | ~member(U_203, X_769, W_202) | ~member(U_203, V_772, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_1347, plain, (![W_737, X1_735, Z_726, U_203, X2_729, Z_719, V_731, U_718, X_722, X2_721, Z_204, X2_732, Y_208, W_202, X1_733, X_727, Z_724, V_738, X1_205, X2_206, V_209, X_740, X_207, Y_730, Y_725, Y_736, X1_720, V_728]: (skf21(V_738, X_740, Y_725, Z_724, X1_735, X2_721, W_202, U_203)=skf21(V_728, X_727, Y_736, Z_719, X1_733, X2_732, W_202, U_203) | skf21(V_728, X_727, Y_736, Z_719, X1_733, X2_732, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_738, X_740, Y_725, Z_724, X1_735, X2_721, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_737 | skf21(V_728, X_727, Y_736, Z_719, X1_733, X2_732, W_202, U_203)=W_737 | skf21(V_738, X_740, Y_725, Z_724, X1_735, X2_721, W_202, U_203)=W_737 | W_737=V_731 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_731 | skf21(V_728, X_727, Y_736, Z_719, X1_733, X2_732, W_202, U_203)=V_731 | skf21(V_738, X_740, Y_725, Z_724, X1_735, X2_721, W_202, U_203)=V_731 | V_731=U_718 | W_737=U_718 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_718 | skf21(V_728, X_727, Y_736, Z_719, X1_733, X2_732, W_202, U_203)=U_718 | skf21(V_738, X_740, Y_725, Z_724, X1_735, X2_721, W_202, U_203)=U_718 | ~member(U_203, W_737, W_202) | ~member(U_203, V_731, W_202) | ~member(U_203, U_718, W_202) | skf21(U_718, V_731, W_737, X_722, Y_730, Z_726, X1_720, X2_729)!=W_737 | X2_721=X1_735 | Z_724=X1_735 | Z_724=X2_721 | Z_724=Y_725 | Y_725=X1_735 | Y_725=X2_721 | Y_725=X_740 | Z_724=X_740 | X_740=X1_735 | X_740=X2_721 | X_740=V_738 | Y_725=V_738 | Z_724=V_738 | X1_735=V_738 | X2_721=V_738 | ~member(U_203, X2_721, W_202) | ~member(U_203, X1_735, W_202) | ~member(U_203, Z_724, W_202) | ~member(U_203, Y_725, W_202) | ~member(U_203, X_740, W_202) | ~member(U_203, V_738, W_202) | X2_732=X1_733 | Z_719=X1_733 | Z_719=X2_732 | Z_719=Y_736 | Y_736=X1_733 | Y_736=X2_732 | Y_736=X_727 | Z_719=X_727 | X_727=X1_733 | X_727=X2_732 | X_727=V_728 | Y_736=V_728 | Z_719=V_728 | X1_733=V_728 | X2_732=V_728 | ~member(U_203, X2_732, W_202) | ~member(U_203, X1_733, W_202) | ~member(U_203, Z_719, W_202) | ~member(U_203, Y_736, W_202) | ~member(U_203, X_727, W_202) | ~member(U_203, V_728, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_1413, plain, (![Y_788, W_805, U_203, Z_810, X1_807, U_789, X1_804, X2_808, Z_204, Y_208, Z_790, X2_792, W_202, Y_791, X1_205, X_801, V_800, V_796, X_797, X2_206, Y_809, X2_803, V_209, V_802, X_207, X_798, X1_794, Z_806, X5_799]: (skf21(V_800, X_798, Y_809, Z_790, X1_804, X2_803, W_202, U_203)=skf21(V_796, X_797, Y_788, Z_806, X1_794, X2_808, W_202, U_203) | skf21(V_800, X_798, Y_809, Z_790, X1_804, X2_803, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_796, X_797, Y_788, Z_806, X1_794, X2_808, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_799 | skf21(V_800, X_798, Y_809, Z_790, X1_804, X2_803, W_202, U_203)=X5_799 | skf21(V_796, X_797, Y_788, Z_806, X1_794, X2_808, W_202, U_203)=X5_799 | X5_799=V_802 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_802 | skf21(V_800, X_798, Y_809, Z_790, X1_804, X2_803, W_202, U_203)=V_802 | skf21(V_796, X_797, Y_788, Z_806, X1_794, X2_808, W_202, U_203)=V_802 | V_802=U_789 | X5_799=U_789 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_789 | skf21(V_800, X_798, Y_809, Z_790, X1_804, X2_803, W_202, U_203)=U_789 | skf21(V_796, X_797, Y_788, Z_806, X1_794, X2_808, W_202, U_203)=U_789 | ~member(U_203, X5_799, W_202) | ~member(U_203, V_802, W_202) | ~member(U_203, U_789, W_202) | skf21(U_789, V_802, W_805, X_801, Y_791, Z_810, X1_807, X2_792)!=V_802 | X2_808=X1_794 | Z_806=X1_794 | Z_806=X2_808 | Z_806=Y_788 | Y_788=X1_794 | Y_788=X2_808 | Y_788=X_797 | Z_806=X_797 | X_797=X1_794 | X_797=X2_808 | X_797=V_796 | Y_788=V_796 | Z_806=V_796 | X1_794=V_796 | X2_808=V_796 | ~member(U_203, X2_808, W_202) | ~member(U_203, X1_794, W_202) | ~member(U_203, Z_806, W_202) | ~member(U_203, Y_788, W_202) | ~member(U_203, X_797, W_202) | ~member(U_203, V_796, W_202) | X2_803=X1_804 | Z_790=X1_804 | Z_790=X2_803 | Z_790=Y_809 | Y_809=X1_804 | Y_809=X2_803 | Y_809=X_798 | Z_790=X_798 | X_798=X1_804 | X_798=X2_803 | X_798=V_800 | Y_809=V_800 | Z_790=V_800 | X1_804=V_800 | X2_803=V_800 | ~member(U_203, X2_803, W_202) | ~member(U_203, X1_804, W_202) | ~member(U_203, Z_790, W_202) | ~member(U_203, Y_809, W_202) | ~member(U_203, X_798, W_202) | ~member(U_203, V_800, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_1324, plain, (![U_689, Y_699, U_203, X1_697, Z_204, Y_208, X2_687, W_202, V_695, X1_205, X_696, X2_206, V_688, W_690, X_694, Z_700, V_209, X1_693, X_207, X2_701, Z_691]: (skf21(V_695, X_694, Y_699, Z_700, X1_693, X2_701, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X_696 | skf21(V_695, X_694, Y_699, Z_700, X1_693, X2_701, W_202, U_203)=X_696 | X_696=W_690 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_690 | skf21(V_695, X_694, Y_699, Z_700, X1_693, X2_701, W_202, U_203)=W_690 | W_690=V_688 | X_696=V_688 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_688 | skf21(V_695, X_694, Y_699, Z_700, X1_693, X2_701, W_202, U_203)=V_688 | V_688=U_689 | W_690=U_689 | X_696=U_689 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_689 | skf21(V_695, X_694, Y_699, Z_700, X1_693, X2_701, W_202, U_203)=U_689 | ~member(U_203, X_696, W_202) | ~member(U_203, W_690, W_202) | ~member(U_203, V_688, W_202) | ~member(U_203, U_689, W_202) | skf21(U_689, V_688, W_690, X_696, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), Z_691, X1_697, X2_687)!=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | X2_701=X1_693 | Z_700=X1_693 | Z_700=X2_701 | Z_700=Y_699 | Y_699=X1_693 | Y_699=X2_701 | Y_699=X_694 | Z_700=X_694 | X_694=X1_693 | X_694=X2_701 | X_694=V_695 | Y_699=V_695 | Z_700=V_695 | X1_693=V_695 | X2_701=V_695 | ~member(U_203, X2_701, W_202) | ~member(U_203, X1_693, W_202) | ~member(U_203, Z_700, W_202) | ~member(U_203, Y_699, W_202) | ~member(U_203, X_694, W_202) | ~member(U_203, V_695, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_1236, plain, (![X6_617, Z_614, X5_616, U_203, X2_629, U_625, Z_204, Y_208, W_202, W_613, Z_628, X_619, X1_618, X_621, X1_205, V_615, Y_626, X2_206, Y_627, V_209, X2_630, X_207, X1_622, V_620]: (skf21(V_620, X_619, Y_626, Z_628, X1_618, X2_630, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X6_617 | skf21(V_620, X_619, Y_626, Z_628, X1_618, X2_630, W_202, U_203)=X6_617 | X6_617=X5_616 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_616 | skf21(V_620, X_619, Y_626, Z_628, X1_618, X2_630, W_202, U_203)=X5_616 | X5_616=V_615 | X6_617=V_615 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_615 | skf21(V_620, X_619, Y_626, Z_628, X1_618, X2_630, W_202, U_203)=V_615 | V_615=U_625 | X5_616=U_625 | X6_617=U_625 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_625 | skf21(V_620, X_619, Y_626, Z_628, X1_618, X2_630, W_202, U_203)=U_625 | ~member(U_203, X6_617, W_202) | ~member(U_203, X5_616, W_202) | ~member(U_203, V_615, W_202) | ~member(U_203, U_625, W_202) | skf21(U_625, V_615, W_613, X_621, Y_627, Z_614, X1_622, X2_629)!=V_615 | X2_630=X1_618 | Z_628=X1_618 | Z_628=X2_630 | Z_628=Y_626 | Y_626=X1_618 | Y_626=X2_630 | Y_626=X_619 | Z_628=X_619 | X_619=X1_618 | X_619=X2_630 | X_619=V_620 | Y_626=V_620 | Z_628=V_620 | X1_618=V_620 | X2_630=V_620 | ~member(U_203, X2_630, W_202) | ~member(U_203, X1_618, W_202) | ~member(U_203, Z_628, W_202) | ~member(U_203, Y_626, W_202) | ~member(U_203, X_619, W_202) | ~member(U_203, V_620, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_1258, plain, (![V_641, Z_642, X_639, X2_649, X5_638, Y_647, Z_648, Y_644, U_203, W_646, U_640, X_651, Z_204, Y_208, W_202, X6_636, X1_205, V_643, X7_632, X2_206, V_209, X_207, X1_634, X2_633, X1_637]: (skf21(V_641, X_639, Y_647, Z_648, X1_637, X2_649, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X7_632 | skf21(V_641, X_639, Y_647, Z_648, X1_637, X2_649, W_202, U_203)=X7_632 | X7_632=X6_636 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X6_636 | skf21(V_641, X_639, Y_647, Z_648, X1_637, X2_649, W_202, U_203)=X6_636 | X6_636=X5_638 | X7_632=X5_638 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_638 | skf21(V_641, X_639, Y_647, Z_648, X1_637, X2_649, W_202, U_203)=X5_638 | X5_638=U_640 | X6_636=U_640 | X7_632=U_640 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_640 | skf21(V_641, X_639, Y_647, Z_648, X1_637, X2_649, W_202, U_203)=U_640 | ~member(U_203, X7_632, W_202) | ~member(U_203, X6_636, W_202) | ~member(U_203, X5_638, W_202) | ~member(U_203, U_640, W_202) | skf21(U_640, V_643, W_646, X_651, Y_644, Z_642, X1_634, X2_633)!=U_640 | X2_649=X1_637 | Z_648=X1_637 | Z_648=X2_649 | Z_648=Y_647 | Y_647=X1_637 | Y_647=X2_649 | Y_647=X_639 | Z_648=X_639 | X_639=X1_637 | X_639=X2_649 | X_639=V_641 | Y_647=V_641 | Z_648=V_641 | X1_637=V_641 | X2_649=V_641 | ~member(U_203, X2_649, W_202) | ~member(U_203, X1_637, W_202) | ~member(U_203, Z_648, W_202) | ~member(U_203, Y_647, W_202) | ~member(U_203, X_639, W_202) | ~member(U_203, V_641, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_1302, plain, (![V_672, Z_683, V_675, U_670, U_203, X_677, Z_682, Z_204, X2_684, Y_208, W_202, X_674, X1_676, X2_685, X1_205, W_678, Y_671, Y_680, X2_206, V_209, X_207, X1_673]: (skf21(V_675, X_674, Y_680, Z_682, X1_673, X2_685, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X_677 | skf21(V_675, X_674, Y_680, Z_682, X1_673, X2_685, W_202, U_203)=X_677 | X_677=W_678 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_678 | skf21(V_675, X_674, Y_680, Z_682, X1_673, X2_685, W_202, U_203)=W_678 | W_678=V_672 | X_677=V_672 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_672 | skf21(V_675, X_674, Y_680, Z_682, X1_673, X2_685, W_202, U_203)=V_672 | V_672=U_670 | W_678=U_670 | X_677=U_670 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_670 | skf21(V_675, X_674, Y_680, Z_682, X1_673, X2_685, W_202, U_203)=U_670 | ~member(U_203, X_677, W_202) | ~member(U_203, W_678, W_202) | ~member(U_203, V_672, W_202) | ~member(U_203, U_670, W_202) | skf21(U_670, V_672, W_678, X_677, Y_671, Z_683, X1_676, X2_684)!=X_677 | X2_685=X1_673 | Z_682=X1_673 | Z_682=X2_685 | Z_682=Y_680 | Y_680=X1_673 | Y_680=X2_685 | Y_680=X_674 | Z_682=X_674 | X_674=X1_673 | X_674=X2_685 | X_674=V_675 | Y_680=V_675 | Z_682=V_675 | X1_673=V_675 | X2_685=V_675 | ~member(U_203, X2_685, W_202) | ~member(U_203, X1_673, W_202) | ~member(U_203, Z_682, W_202) | ~member(U_203, Y_680, W_202) | ~member(U_203, X_674, W_202) | ~member(U_203, V_675, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_1280, plain, (![X2_667, X1_666, Y_669, U_203, U_654, Z_204, Y_208, W_202, W_660, Z_661, X1_205, V_662, Y_664, X2_206, X_659, X_656, Z_665, V_209, X2_652, X5_658, X_207, V_657, X1_655]: (skf21(V_657, X_656, Y_664, Z_665, X1_655, X2_667, W_202, U_203)=skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203) | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=X5_658 | skf21(V_657, X_656, Y_664, Z_665, X1_655, X2_667, W_202, U_203)=X5_658 | X5_658=W_660 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=W_660 | skf21(V_657, X_656, Y_664, Z_665, X1_655, X2_667, W_202, U_203)=W_660 | W_660=V_662 | X5_658=V_662 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=V_662 | skf21(V_657, X_656, Y_664, Z_665, X1_655, X2_667, W_202, U_203)=V_662 | V_662=U_654 | W_660=U_654 | X5_658=U_654 | skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203)=U_654 | skf21(V_657, X_656, Y_664, Z_665, X1_655, X2_667, W_202, U_203)=U_654 | ~member(U_203, X5_658, W_202) | ~member(U_203, W_660, W_202) | ~member(U_203, V_662, W_202) | ~member(U_203, U_654, W_202) | skf21(U_654, V_662, W_660, X_659, Y_669, Z_661, X1_666, X2_652)!=W_660 | X2_667=X1_655 | Z_665=X1_655 | Z_665=X2_667 | Z_665=Y_664 | Y_664=X1_655 | Y_664=X2_667 | Y_664=X_656 | Z_665=X_656 | X_656=X1_655 | X_656=X2_667 | X_656=V_657 | Y_664=V_657 | Z_665=V_657 | X1_655=V_657 | X2_667=V_657 | ~member(U_203, X2_667, W_202) | ~member(U_203, X1_655, W_202) | ~member(U_203, Z_665, W_202) | ~member(U_203, Y_664, W_202) | ~member(U_203, X_656, W_202) | ~member(U_203, V_657, W_202) | X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_1213, plain, (![U_612, U_212, W_606, X_607, X1_610, Y_611, X2_609, X_216, Z_605, V_218, V_608, X2_215, Y_217, W_210, X1_214]: (skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=Y_217 | Y_217=X_216 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X_216 | X_216=W_210 | Y_217=W_210 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=W_210 | W_210=V_218 | X_216=V_218 | Y_217=V_218 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=V_218 | V_218=U_212 | W_210=U_212 | X_216=U_212 | Y_217=U_212 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=U_212 | ~member(U_612, Y_217, W_606) | ~member(U_612, X_216, W_606) | ~member(U_612, W_210, W_606) | ~member(U_612, V_218, W_606) | ~member(U_612, U_212, W_606) | skf21(U_212, V_218, W_210, X_216, Y_217, skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612), X1_214, X2_215)!=skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612) | X2_609=X1_610 | Z_605=X1_610 | Z_605=X2_609 | Z_605=Y_611 | Y_611=X1_610 | Y_611=X2_609 | Y_611=X_607 | Z_605=X_607 | X_607=X1_610 | X_607=X2_609 | X_607=V_608 | Y_611=V_608 | Z_605=V_608 | X1_610=V_608 | X2_609=V_608 | six(U_612, W_606) | ~member(U_612, X2_609, W_606) | ~member(U_612, X1_610, W_606) | ~member(U_612, Z_605, W_606) | ~member(U_612, Y_611, W_606) | ~member(U_612, X_607, W_606) | ~member(U_612, V_608, W_606)))). % 56.65/47.65 tff(c_1216, plain, (![U_612, W_606, X_144, X_607, Y_145, Z_141, X1_610, Y_611, X2_609, U_140, X1_142, Z_605, V_608, V_146, X2_143, W_138]: (skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=Y_145 | Y_145=X_144 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X_144 | X_144=W_138 | Y_145=W_138 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=W_138 | W_138=V_146 | X_144=V_146 | Y_145=V_146 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=V_146 | V_146=U_140 | W_138=U_140 | X_144=U_140 | Y_145=U_140 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=U_140 | ~member(U_612, Y_145, W_606) | ~member(U_612, X_144, W_606) | ~member(U_612, W_138, W_606) | ~member(U_612, V_146, W_606) | ~member(U_612, U_140, W_606) | skf21(U_140, V_146, W_138, X_144, Y_145, Z_141, X1_142, X2_143)!=Y_145 | X2_609=X1_610 | Z_605=X1_610 | Z_605=X2_609 | Z_605=Y_611 | Y_611=X1_610 | Y_611=X2_609 | Y_611=X_607 | Z_605=X_607 | X_607=X1_610 | X_607=X2_609 | X_607=V_608 | Y_611=V_608 | Z_605=V_608 | X1_610=V_608 | X2_609=V_608 | six(U_612, W_606) | ~member(U_612, X2_609, W_606) | ~member(U_612, X1_610, W_606) | ~member(U_612, Z_605, W_606) | ~member(U_612, Y_611, W_606) | ~member(U_612, X_607, W_606) | ~member(U_612, V_608, W_606)))). % 56.65/47.65 tff(c_1214, plain, (![U_612, X_156, X2_155, W_606, X5_148, X_607, X1_154, U_152, Z_153, X1_610, Y_611, X2_609, Y_157, V_158, Z_605, V_608, W_150]: (skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X5_148 | X_156=X5_148 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X_156 | X_156=W_150 | X5_148=W_150 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=W_150 | W_150=V_158 | X_156=V_158 | X5_148=V_158 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=V_158 | V_158=U_152 | W_150=U_152 | X_156=U_152 | X5_148=U_152 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=U_152 | ~member(U_612, X5_148, W_606) | ~member(U_612, X_156, W_606) | ~member(U_612, W_150, W_606) | ~member(U_612, V_158, W_606) | ~member(U_612, U_152, W_606) | skf21(U_152, V_158, W_150, X_156, Y_157, Z_153, X1_154, X2_155)!=X_156 | X2_609=X1_610 | Z_605=X1_610 | Z_605=X2_609 | Z_605=Y_611 | Y_611=X1_610 | Y_611=X2_609 | Y_611=X_607 | Z_605=X_607 | X_607=X1_610 | X_607=X2_609 | X_607=V_608 | Y_611=V_608 | Z_605=V_608 | X1_610=V_608 | X2_609=V_608 | six(U_612, W_606) | ~member(U_612, X2_609, W_606) | ~member(U_612, X1_610, W_606) | ~member(U_612, Z_605, W_606) | ~member(U_612, Y_611, W_606) | ~member(U_612, X_607, W_606) | ~member(U_612, V_608, W_606)))). % 56.65/47.65 tff(c_1215, plain, (![U_612, U_164, X6_161, Y_170, W_162, W_606, X_607, X1_610, Y_611, X2_609, X1_167, X_169, Z_165, Z_605, V_171, V_608, X2_168, X5_160]: (skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X6_161 | X6_161=X5_160 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X5_160 | X5_160=W_162 | X6_161=W_162 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=W_162 | W_162=V_171 | X5_160=V_171 | X6_161=V_171 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=V_171 | V_171=U_164 | W_162=U_164 | X5_160=U_164 | X6_161=U_164 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=U_164 | ~member(U_612, X6_161, W_606) | ~member(U_612, X5_160, W_606) | ~member(U_612, W_162, W_606) | ~member(U_612, V_171, W_606) | ~member(U_612, U_164, W_606) | skf21(U_164, V_171, W_162, X_169, Y_170, Z_165, X1_167, X2_168)!=W_162 | X2_609=X1_610 | Z_605=X1_610 | Z_605=X2_609 | Z_605=Y_611 | Y_611=X1_610 | Y_611=X2_609 | Y_611=X_607 | Z_605=X_607 | X_607=X1_610 | X_607=X2_609 | X_607=V_608 | Y_611=V_608 | Z_605=V_608 | X1_610=V_608 | X2_609=V_608 | six(U_612, W_606) | ~member(U_612, X2_609, W_606) | ~member(U_612, X1_610, W_606) | ~member(U_612, Z_605, W_606) | ~member(U_612, Y_611, W_606) | ~member(U_612, X_607, W_606) | ~member(U_612, V_608, W_606)))). % 56.65/47.65 tff(c_1217, plain, (![X8_200, U_612, V_199, X6_188, X2_196, W_606, X7_194, X_607, W_189, Z_193, X1_610, Y_611, X2_609, X1_195, Z_605, U_191, V_608, X_197, Y_198, X5_187]: (skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X8_200 | X8_200=X7_194 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X7_194 | X7_194=X6_188 | X8_200=X6_188 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X6_188 | X6_188=X5_187 | X7_194=X5_187 | X8_200=X5_187 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X5_187 | X5_187=U_191 | X6_188=U_191 | X7_194=U_191 | X8_200=U_191 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=U_191 | ~member(U_612, X8_200, W_606) | ~member(U_612, X7_194, W_606) | ~member(U_612, X6_188, W_606) | ~member(U_612, X5_187, W_606) | ~member(U_612, U_191, W_606) | skf21(U_191, V_199, W_189, X_197, Y_198, Z_193, X1_195, X2_196)!=U_191 | X2_609=X1_610 | Z_605=X1_610 | Z_605=X2_609 | Z_605=Y_611 | Y_611=X1_610 | Y_611=X2_609 | Y_611=X_607 | Z_605=X_607 | X_607=X1_610 | X_607=X2_609 | X_607=V_608 | Y_611=V_608 | Z_605=V_608 | X1_610=V_608 | X2_609=V_608 | six(U_612, W_606) | ~member(U_612, X2_609, W_606) | ~member(U_612, X1_610, W_606) | ~member(U_612, Z_605, W_606) | ~member(U_612, Y_611, W_606) | ~member(U_612, X_607, W_606) | ~member(U_612, V_608, W_606)))). % 56.65/47.65 tff(c_1212, plain, (![V_184, U_612, X5_173, W_606, X6_174, X_607, Z_178, X1_610, Y_611, X_182, X2_609, Y_183, Z_605, X1_180, V_608, W_175, U_177, X2_181, X7_179]: (skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X7_179 | X7_179=X6_174 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X6_174 | X6_174=X5_173 | X7_179=X5_173 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=X5_173 | X5_173=V_184 | X6_174=V_184 | X7_179=V_184 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=V_184 | V_184=U_177 | X5_173=U_177 | X6_174=U_177 | X7_179=U_177 | skf21(V_608, X_607, Y_611, Z_605, X1_610, X2_609, W_606, U_612)=U_177 | ~member(U_612, X7_179, W_606) | ~member(U_612, X6_174, W_606) | ~member(U_612, X5_173, W_606) | ~member(U_612, V_184, W_606) | ~member(U_612, U_177, W_606) | skf21(U_177, V_184, W_175, X_182, Y_183, Z_178, X1_180, X2_181)!=V_184 | X2_609=X1_610 | Z_605=X1_610 | Z_605=X2_609 | Z_605=Y_611 | Y_611=X1_610 | Y_611=X2_609 | Y_611=X_607 | Z_605=X_607 | X_607=X1_610 | X_607=X2_609 | X_607=V_608 | Y_611=V_608 | Z_605=V_608 | X1_610=V_608 | X2_609=V_608 | six(U_612, W_606) | ~member(U_612, X2_609, W_606) | ~member(U_612, X1_610, W_606) | ~member(U_612, Z_605, W_606) | ~member(U_612, Y_611, W_606) | ~member(U_612, X_607, W_606) | ~member(U_612, V_608, W_606)))). % 56.65/47.65 tff(c_146, plain, (![U_203, Z_204, Y_208, W_202, X1_205, X2_206, V_209, X_207]: (X2_206=X1_205 | Z_204=X1_205 | Z_204=X2_206 | Z_204=Y_208 | Y_208=X1_205 | Y_208=X2_206 | Y_208=X_207 | Z_204=X_207 | X_207=X1_205 | X_207=X2_206 | X_207=V_209 | Y_208=V_209 | Z_204=V_209 | X1_205=V_209 | X2_206=V_209 | member(U_203, skf21(V_209, X_207, Y_208, Z_204, X1_205, X2_206, W_202, U_203), W_202) | six(U_203, W_202) | ~member(U_203, X2_206, W_202) | ~member(U_203, X1_205, W_202) | ~member(U_203, Z_204, W_202) | ~member(U_203, Y_208, W_202) | ~member(U_203, X_207, W_202) | ~member(U_203, V_209, W_202)))). % 56.65/47.65 tff(c_142, plain, (![X3_176, V_184, X5_173, X6_174, Z_178, X_182, Y_183, X1_180, X4_186, X8_185, W_175, U_177, X2_181, X7_179]: (X8_185=X7_179 | X7_179=X6_174 | X8_185=X6_174 | X6_174=X5_173 | X7_179=X5_173 | X8_185=X5_173 | X5_173=V_184 | X6_174=V_184 | X7_179=V_184 | X8_185=V_184 | V_184=U_177 | X5_173=U_177 | X6_174=U_177 | X7_179=U_177 | X8_185=U_177 | six(X3_176, X4_186) | ~member(X3_176, X8_185, X4_186) | ~member(X3_176, X7_179, X4_186) | ~member(X3_176, X6_174, X4_186) | ~member(X3_176, X5_173, X4_186) | ~member(X3_176, V_184, X4_186) | ~member(X3_176, U_177, X4_186) | skf21(U_177, V_184, W_175, X_182, Y_183, Z_178, X1_180, X2_181)!=V_184))). % 56.65/47.65 tff(c_148, plain, (![Z_213, X4_219, U_212, X_216, V_218, X2_215, X3_211, Y_217, W_210, X1_214]: (Z_213=Y_217 | Y_217=X_216 | Z_213=X_216 | X_216=W_210 | Y_217=W_210 | Z_213=W_210 | W_210=V_218 | X_216=V_218 | Y_217=V_218 | Z_213=V_218 | V_218=U_212 | W_210=U_212 | X_216=U_212 | Y_217=U_212 | Z_213=U_212 | six(X3_211, X4_219) | ~member(X3_211, Z_213, X4_219) | ~member(X3_211, Y_217, X4_219) | ~member(X3_211, X_216, X4_219) | ~member(X3_211, W_210, X4_219) | ~member(X3_211, V_218, X4_219) | ~member(X3_211, U_212, X4_219) | skf21(U_212, V_218, W_210, X_216, Y_217, Z_213, X1_214, X2_215)!=Z_213))). % 56.65/47.65 tff(c_138, plain, (![X_156, X2_155, X3_151, X5_148, X1_154, U_152, X6_149, Z_153, Y_157, V_158, W_150, X4_159]: (X6_149=X5_148 | X_156=X5_148 | X_156=X6_149 | X_156=W_150 | X5_148=W_150 | X6_149=W_150 | W_150=V_158 | X_156=V_158 | X5_148=V_158 | X6_149=V_158 | V_158=U_152 | W_150=U_152 | X_156=U_152 | X5_148=U_152 | X6_149=U_152 | six(X3_151, X4_159) | ~member(X3_151, X6_149, X4_159) | ~member(X3_151, X5_148, X4_159) | ~member(X3_151, X_156, X4_159) | ~member(X3_151, W_150, X4_159) | ~member(X3_151, V_158, X4_159) | ~member(X3_151, U_152, X4_159) | skf21(U_152, V_158, W_150, X_156, Y_157, Z_153, X1_154, X2_155)!=X_156))). % 56.65/47.65 tff(c_140, plain, (![U_164, X7_166, X6_161, Y_170, W_162, X1_167, X3_163, X_169, Z_165, V_171, X2_168, X4_172, X5_160]: (X7_166=X6_161 | X6_161=X5_160 | X7_166=X5_160 | X5_160=W_162 | X6_161=W_162 | X7_166=W_162 | W_162=V_171 | X5_160=V_171 | X6_161=V_171 | X7_166=V_171 | V_171=U_164 | W_162=U_164 | X5_160=U_164 | X6_161=U_164 | X7_166=U_164 | six(X3_163, X4_172) | ~member(X3_163, X7_166, X4_172) | ~member(X3_163, X6_161, X4_172) | ~member(X3_163, X5_160, X4_172) | ~member(X3_163, W_162, X4_172) | ~member(X3_163, V_171, X4_172) | ~member(X3_163, U_164, X4_172) | skf21(U_164, V_171, W_162, X_169, Y_170, Z_165, X1_167, X2_168)!=W_162))). % 56.65/47.65 tff(c_136, plain, (![X4_147, X_144, Y_145, Z_141, X3_139, X5_137, U_140, X1_142, V_146, X2_143, W_138]: (Y_145=X5_137 | Y_145=X_144 | X_144=X5_137 | X_144=W_138 | Y_145=W_138 | X5_137=W_138 | W_138=V_146 | X_144=V_146 | Y_145=V_146 | X5_137=V_146 | V_146=U_140 | W_138=U_140 | X_144=U_140 | Y_145=U_140 | X5_137=U_140 | six(X3_139, X4_147) | ~member(X3_139, X5_137, X4_147) | ~member(X3_139, Y_145, X4_147) | ~member(X3_139, X_144, X4_147) | ~member(X3_139, W_138, X4_147) | ~member(X3_139, V_146, X4_147) | ~member(X3_139, U_140, X4_147) | skf21(U_140, V_146, W_138, X_144, Y_145, Z_141, X1_142, X2_143)!=Y_145))). % 56.65/47.65 tff(c_144, plain, (![X8_200, V_199, X6_188, X2_196, X3_190, X4_201, X7_194, W_189, Z_193, X1_195, U_191, X_197, Y_198, X5_187, X9_192]: (X9_192=X8_200 | X8_200=X7_194 | X9_192=X7_194 | X7_194=X6_188 | X8_200=X6_188 | X9_192=X6_188 | X6_188=X5_187 | X7_194=X5_187 | X8_200=X5_187 | X9_192=X5_187 | X5_187=U_191 | X6_188=U_191 | X7_194=U_191 | X8_200=U_191 | X9_192=U_191 | six(X3_190, X4_201) | ~member(X3_190, X9_192, X4_201) | ~member(X3_190, X8_200, X4_201) | ~member(X3_190, X7_194, X4_201) | ~member(X3_190, X6_188, X4_201) | ~member(X3_190, X5_187, X4_201) | ~member(X3_190, U_191, X4_201) | skf21(U_191, V_199, W_189, X_197, Y_198, Z_193, X1_195, X2_196)!=U_191))). % 56.65/47.65 tff(c_134, plain, (![W_136, U_134, V_135]: (skf20(W_136, U_134)=V_135 | skf18(W_136, U_134)=V_135 | skf16(W_136, U_134)=V_135 | skf14(W_136, U_134)=V_135 | skf12(W_136, U_134)=V_135 | skf10(W_136, U_134)=V_135 | ~six(U_134, W_136) | ~member(U_134, V_135, W_136)))). % 56.65/47.65 tff(c_1046, plain, (~member(skc8, skc15, skc13))). % 56.65/47.65 tff(c_1037, plain, (![U_231]: (~agent(skc8, skf8(U_231), U_231) | ~member(skc8, U_231, skc13)))). % 56.65/47.65 tff(c_1040, plain, (~agent(skc8, skc9, skc12))). % 56.65/47.65 tff(c_132, plain, (![U_131, V_132, W_133]: (~agent(U_131, V_132, W_133) | ~patient(U_131, V_132, W_133) | ~nonreflexive(U_131, V_132)))). % 56.65/47.65 tff(c_1027, plain, (skf14(skc13, skc8)!=skf10(skc13, skc8))). % 56.65/47.65 tff(c_126, plain, (![V_126, U_125]: (~six(V_126, U_125) | skf14(U_125, V_126)!=skf10(U_125, V_126)))). % 56.65/47.65 tff(c_1022, plain, (skf12(skc13, skc8)!=skf10(skc13, skc8))). % 56.65/47.65 tff(c_130, plain, (![V_130, U_129]: (~six(V_130, U_129) | skf12(U_129, V_130)!=skf10(U_129, V_130)))). % 56.65/47.65 tff(c_1017, plain, (skf20(skc13, skc8)!=skf16(skc13, skc8))). % 56.65/47.65 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf20(U_107, V_108)!=skf16(U_107, V_108)))). % 56.65/47.65 tff(c_1012, plain, (skf16(skc13, skc8)!=skf14(skc13, skc8))). % 56.65/47.65 tff(c_124, plain, (![V_124, U_123]: (~six(V_124, U_123) | skf16(U_123, V_124)!=skf14(U_123, V_124)))). % 56.65/47.65 tff(c_1007, plain, (act(skc8, skf12(skc13, skc8)))). % 56.65/47.65 tff(c_1003, plain, (action(skc8, skf12(skc13, skc8)))). % 56.65/47.65 tff(c_999, plain, (shot(skc8, skf12(skc13, skc8)))). % 56.65/47.65 tff(c_98, plain, (![U_97, V_98]: (member(U_97, skf12(V_98, U_97), V_98) | ~six(U_97, V_98)))). % 56.65/47.65 tff(c_196, plain, (![U_231]: (patient(skc8, skf8(U_231), U_231) | ~member(skc8, U_231, skc13)))). % 56.65/47.65 tff(c_989, plain, (![V_233]: (agent(skc8, skf8(V_233), skc15)))). % 56.65/47.65 tff(c_962, plain, (skf20(skc13, skc8)!=skf18(skc13, skc8))). % 56.65/47.65 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf20(U_109, V_110)!=skf18(U_109, V_110)))). % 56.65/47.65 tff(c_929, plain, (act(skc8, skf10(skc13, skc8)))). % 56.65/47.65 tff(c_956, plain, (![V_230]: (from_loc(skc8, skf8(V_230), skc14)))). % 56.65/47.65 tff(c_913, plain, (act(skc8, skf18(skc13, skc8)))). % 56.65/47.65 tff(c_925, plain, (action(skc8, skf10(skc13, skc8)))). % 56.65/47.65 tff(c_921, plain, (shot(skc8, skf10(skc13, skc8)))). % 56.65/47.65 tff(c_100, plain, (![U_99, V_100]: (member(U_99, skf10(V_100, U_99), V_100) | ~six(U_99, V_100)))). % 56.65/47.65 tff(c_909, plain, (action(skc8, skf18(skc13, skc8)))). % 56.65/47.65 tff(c_905, plain, (shot(skc8, skf18(skc13, skc8)))). % 56.65/47.65 tff(c_92, plain, (![U_91, V_92]: (member(U_91, skf18(V_92, U_91), V_92) | ~six(U_91, V_92)))). % 56.65/47.65 tff(c_897, plain, (skf18(skc13, skc8)!=skf14(skc13, skc8))). % 56.65/47.65 tff(c_892, plain, (~act(skc8, skc14))). % 56.65/47.66 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf18(U_115, V_116)!=skf14(U_115, V_116)))). % 56.65/47.66 tff(c_876, plain, (![U_47, V_48]: (~act(U_47, V_48) | ~artifact(U_47, V_48)))). % 56.65/47.66 tff(c_887, plain, (skf16(skc13, skc8)!=skf12(skc13, skc8))). % 56.65/47.66 tff(c_882, plain, (~artifact(skc8, skc12))). % 56.65/47.66 tff(c_122, plain, (![V_122, U_121]: (~six(V_122, U_121) | skf16(U_121, V_122)!=skf12(U_121, V_122)))). % 56.65/47.66 tff(c_867, plain, (![U_47, V_48]: (~cry(U_47, V_48) | ~artifact(U_47, V_48)))). % 56.65/47.66 tff(c_837, plain, (![U_27, V_28]: (~entity(U_27, V_28) | ~act(U_27, V_28)))). % 56.65/47.66 tff(c_838, plain, (![U_21, V_22]: (~entity(U_21, V_22) | ~cry(U_21, V_22)))). % 56.65/47.66 tff(c_859, plain, (skf18(skc13, skc8)!=skf10(skc13, skc8))). % 56.65/47.66 tff(c_848, plain, (skf20(skc13, skc8)!=skf12(skc13, skc8))). % 56.65/47.66 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf18(U_111, V_112)!=skf10(U_111, V_112)))). % 56.65/47.66 tff(c_853, plain, (![V_486]: (~artifact(skc8, skf8(V_486))))). % 56.65/47.66 tff(c_836, plain, (![V_384]: (~entity(skc8, skf8(V_384))))). % 56.65/47.66 tff(c_843, plain, (~artifact(skc8, skc9))). % 56.65/47.66 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf20(U_103, V_104)!=skf12(U_103, V_104)))). % 56.65/47.66 tff(c_839, plain, (~entity(skc8, skc9))). % 56.65/47.66 tff(c_695, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~event(U_7, V_8)))). % 56.65/47.66 tff(c_700, plain, (![U_244, V_245]: (~artifact(U_244, V_245) | ~human_person(U_244, V_245)))). % 56.65/47.66 tff(c_817, plain, (skf14(skc13, skc8)!=skf12(skc13, skc8))). % 56.65/47.66 tff(c_812, plain, (~animate(skc8, skc14))). % 56.65/47.66 tff(c_128, plain, (![V_128, U_127]: (~six(V_128, U_127) | skf14(U_127, V_128)!=skf12(U_127, V_128)))). % 56.65/47.66 tff(c_808, plain, (artifact(skc8, skc14))). % 56.65/47.66 tff(c_761, plain, (![U_462, V_463]: (artifact(U_462, V_463) | ~cannon(U_462, V_463)))). % 56.65/47.66 tff(c_803, plain, (skf18(skc13, skc8)!=skf12(skc13, skc8))). % 56.65/47.66 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf18(U_113, V_114)!=skf12(U_113, V_114)))). % 56.65/47.66 tff(c_798, plain, (~artifact(skc8, skc13))). % 56.65/47.66 tff(c_794, plain, (~entity(skc8, skc13))). % 56.65/47.66 tff(c_710, plain, (![U_31, V_32]: (~entity(U_31, V_32) | ~group(U_31, V_32)))). % 56.65/47.66 tff(c_789, plain, (skf20(skc13, skc8)!=skf14(skc13, skc8))). % 56.65/47.66 tff(c_776, plain, (skf16(skc13, skc8)!=skf10(skc13, skc8))). % 56.65/47.66 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf20(U_105, V_106)!=skf14(U_105, V_106)))). % 56.65/47.66 tff(c_784, plain, (~cry(skc8, skc13))). % 56.65/47.66 tff(c_783, plain, (~act(skc8, skc13))). % 56.65/47.66 tff(c_771, plain, (~event(skc8, skc13))). % 56.65/47.66 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf16(U_119, V_120)!=skf10(U_119, V_120)))). % 56.65/47.66 tff(c_767, plain, (~eventuality(skc8, skc13))). % 56.65/47.66 tff(c_674, plain, (![U_31, V_32]: (~eventuality(U_31, V_32) | ~group(U_31, V_32)))). % 56.65/47.66 tff(c_566, plain, (![U_392, V_393]: (~animate(U_392, V_393) | ~artifact(U_392, V_393)))). % 56.65/47.66 tff(c_551, plain, (![U_39, V_40]: (instrumentality(U_39, V_40) | ~cannon(U_39, V_40)))). % 56.65/47.66 tff(c_756, plain, (skf18(skc13, skc8)!=skf16(skc13, skc8))). % 56.65/47.66 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf18(U_117, V_118)!=skf16(U_117, V_118)))). % 56.65/47.66 tff(c_751, plain, (act(skc8, skf20(skc13, skc8)))). % 56.65/47.66 tff(c_747, plain, (action(skc8, skf20(skc13, skc8)))). % 56.65/47.66 tff(c_743, plain, (shot(skc8, skf20(skc13, skc8)))). % 56.65/47.66 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf20(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 56.65/47.66 tff(c_735, plain, (act(skc8, skf14(skc13, skc8)))). % 56.65/47.66 tff(c_731, plain, (action(skc8, skf14(skc13, skc8)))). % 56.65/47.66 tff(c_727, plain, (shot(skc8, skf14(skc13, skc8)))). % 56.65/47.66 tff(c_718, plain, (~artifact(skc8, skc15))). % 56.65/47.66 tff(c_719, plain, (~artifact(skc8, skc11))). % 56.65/47.66 tff(c_96, plain, (![U_95, V_96]: (member(U_95, skf14(V_96, U_95), V_96) | ~six(U_95, V_96)))). % 56.65/47.66 tff(c_558, plain, (![U_47, V_48]: (~male(U_47, V_48) | ~artifact(U_47, V_48)))). % 56.65/47.66 tff(c_338, plain, (![U_322, V_323]: (~multiple(U_322, V_323) | ~entity(U_322, V_323)))). % 56.65/47.66 tff(c_705, plain, (skf20(skc13, skc8)!=skf10(skc13, skc8))). % 56.65/47.66 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf20(U_101, V_102)!=skf10(U_101, V_102)))). % 56.65/47.66 tff(c_567, plain, (![U_392, V_393]: (~living(U_392, V_393) | ~artifact(U_392, V_393)))). % 56.65/47.66 tff(c_348, plain, (![U_55, V_56]: (~eventuality(U_55, V_56) | ~entity(U_55, V_56)))). % 56.65/47.66 tff(c_690, plain, (act(skc8, skf16(skc13, skc8)))). % 56.65/47.66 tff(c_686, plain, (action(skc8, skf16(skc13, skc8)))). % 56.65/47.66 tff(c_682, plain, (shot(skc8, skf16(skc13, skc8)))). % 56.65/47.66 tff(c_94, plain, (![U_93, V_94]: (member(U_93, skf16(V_94, U_93), V_94) | ~six(U_93, V_94)))). % 56.65/47.66 tff(c_343, plain, (![U_324, V_325]: (~multiple(U_324, V_325) | ~eventuality(U_324, V_325)))). % 56.65/47.66 tff(c_243, plain, (![U_47, V_48]: (impartial(U_47, V_48) | ~artifact(U_47, V_48)))). % 56.65/47.66 tff(c_667, plain, (![V_226]: (present(skc8, skf8(V_226))))). % 56.65/47.66 tff(c_222, plain, (![U_65, V_66]: (impartial(U_65, V_66) | ~human_person(U_65, V_66)))). % 56.65/47.66 tff(c_261, plain, (![U_47, V_48]: (entity(U_47, V_48) | ~artifact(U_47, V_48)))). % 56.65/47.66 tff(c_636, plain, (![V_224]: (nonreflexive(skc8, skf8(V_224))))). % 56.65/47.66 tff(c_572, plain, (entity(skc8, skc15))). % 56.65/47.66 tff(c_214, plain, (![U_65, V_66]: (entity(U_65, V_66) | ~human_person(U_65, V_66)))). % 56.65/47.66 tff(c_254, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~artifact(U_47, V_48)))). % 56.65/47.66 tff(c_283, plain, (![U_61, V_62]: (~male(U_61, V_62) | ~object(U_61, V_62)))). % 56.65/47.66 tff(c_208, plain, (![U_244, V_245]: (living(U_244, V_245) | ~human_person(U_244, V_245)))). % 56.65/47.66 tff(c_228, plain, (![U_41, V_42]: (instrumentality(U_41, V_42) | ~weapon(U_41, V_42)))). % 56.65/47.66 tff(c_545, plain, (![V_384]: (event(skc8, skf8(V_384))))). % 56.65/47.66 tff(c_532, plain, (![V_222]: (fire(skc8, skf8(V_222))))). % 56.65/47.66 tff(c_540, plain, (~cry(skc8, skc11))). % 56.65/47.66 tff(c_539, plain, (~act(skc8, skc11))). % 56.65/47.66 tff(c_374, plain, (~act(skc8, skc15))). % 56.65/47.66 tff(c_375, plain, (~cry(skc8, skc15))). % 56.65/47.66 tff(c_367, plain, (~event(skc8, skc11))). % 56.65/47.66 tff(c_363, plain, (~event(skc8, skc15))). % 56.65/47.66 tff(c_359, plain, (~eventuality(skc8, skc11))). % 56.65/47.66 tff(c_358, plain, (~eventuality(skc8, skc15))). % 56.65/47.66 tff(c_333, plain, (![U_320, V_321]: (~male(U_320, V_321) | ~eventuality(U_320, V_321)))). % 56.65/47.66 tff(c_312, plain, (![U_31, V_32]: (multiple(U_31, V_32) | ~group(U_31, V_32)))). % 56.65/47.66 tff(c_184, plain, (![U_220]: (shot(skc8, U_220) | ~member(skc8, U_220, skc13)))). % 56.65/47.66 tff(c_317, plain, (![U_314, V_315]: (~existent(U_314, V_315) | ~eventuality(U_314, V_315)))). % 56.65/47.66 tff(c_322, plain, (![U_316, V_317]: (singleton(U_316, V_317) | ~eventuality(U_316, V_317)))). % 56.65/47.66 tff(c_307, plain, (![U_51, V_52]: (singleton(U_51, V_52) | ~entity(U_51, V_52)))). % 56.65/47.66 tff(c_18, plain, (![U_17, V_18]: (unisex(U_17, V_18) | ~eventuality(U_17, V_18)))). % 56.65/47.66 tff(c_20, plain, (![U_19, V_20]: (event(U_19, V_20) | ~scream(U_19, V_20)))). % 56.65/47.66 tff(c_10, plain, (![U_9, V_10]: (thing(U_9, V_10) | ~eventuality(U_9, V_10)))). % 56.65/47.66 tff(c_16, plain, (![U_15, V_16]: (nonexistent(U_15, V_16) | ~eventuality(U_15, V_16)))). % 56.65/47.66 tff(c_34, plain, (![U_33, V_34]: (multiple(U_33, V_34) | ~set(U_33, V_34)))). % 56.65/47.66 tff(c_302, plain, (act(skc8, skc10))). % 56.65/47.66 tff(c_12, plain, (![U_11, V_12]: (singleton(U_11, V_12) | ~thing(U_11, V_12)))). % 56.65/47.66 tff(c_298, plain, (action(skc8, skc10))). % 56.65/47.66 tff(c_24, plain, (![U_23, V_24]: (action(U_23, V_24) | ~revenge(U_23, V_24)))). % 56.65/47.67 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~act(U_27, V_28)))). % 56.65/47.67 tff(c_6, plain, (![U_5, V_6]: (event(U_5, V_6) | ~sound(U_5, V_6)))). % 56.65/47.67 tff(c_88, plain, (![U_87, V_88]: (~animate(U_87, V_88) | ~nonliving(U_87, V_88)))). % 56.65/47.67 tff(c_22, plain, (![U_21, V_22]: (event(U_21, V_22) | ~cry(U_21, V_22)))). % 56.65/47.67 tff(c_86, plain, (![U_85, V_86]: (~existent(U_85, V_86) | ~nonexistent(U_85, V_86)))). % 56.65/47.67 tff(c_8, plain, (![U_7, V_8]: (eventuality(U_7, V_8) | ~event(U_7, V_8)))). % 56.65/47.67 tff(c_80, plain, (![U_79, V_80]: (~unisex(U_79, V_80) | ~male(U_79, V_80)))). % 56.65/47.67 tff(c_30, plain, (![U_29, V_30]: (action(U_29, V_30) | ~shot(U_29, V_30)))). % 56.65/47.67 tff(c_82, plain, (![U_81, V_82]: (~singleton(U_81, V_82) | ~multiple(U_81, V_82)))). % 56.65/47.67 tff(c_36, plain, (![U_35, V_36]: (group(U_35, V_36) | ~six(U_35, V_36)))). % 56.65/47.67 tff(c_84, plain, (![U_83, V_84]: (~nonliving(U_83, V_84) | ~living(U_83, V_84)))). % 56.65/47.67 tff(c_32, plain, (![U_31, V_32]: (set(U_31, V_32) | ~group(U_31, V_32)))). % 56.65/47.67 tff(c_78, plain, (![U_77, V_78]: (male(U_77, V_78) | ~man(U_77, V_78)))). % 56.65/47.67 tff(c_56, plain, (![U_55, V_56]: (existent(U_55, V_56) | ~entity(U_55, V_56)))). % 56.65/47.67 tff(c_50, plain, (![U_49, V_50]: (entity(U_49, V_50) | ~object(U_49, V_50)))). % 56.65/47.67 tff(c_54, plain, (![U_53, V_54]: (specific(U_53, V_54) | ~entity(U_53, V_54)))). % 56.65/47.67 tff(c_38, plain, (![U_37, V_38]: (event(U_37, V_38) | ~fire(U_37, V_38)))). % 56.65/47.67 tff(c_58, plain, (![U_57, V_58]: (nonliving(U_57, V_58) | ~object(U_57, V_58)))). % 56.65/47.67 tff(c_4, plain, (![U_3, V_4]: (sound(U_3, V_4) | ~scream(U_3, V_4)))). % 56.65/47.67 tff(c_248, plain, (animate(skc8, skc15))). % 56.65/47.67 tff(c_76, plain, (![U_75, V_76]: (animate(U_75, V_76) | ~human_person(U_75, V_76)))). % 56.65/47.67 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~object(U_59, V_60)))). % 56.65/47.67 tff(c_62, plain, (![U_61, V_62]: (unisex(U_61, V_62) | ~object(U_61, V_62)))). % 56.65/47.67 tff(c_237, plain, (human(skc8, skc15))). % 56.65/47.67 tff(c_233, plain, (human_person(skc8, skc15))). % 56.65/47.67 tff(c_64, plain, (![U_63, V_64]: (human_person(U_63, V_64) | ~man(U_63, V_64)))). % 56.65/47.67 tff(c_44, plain, (![U_43, V_44]: (instrumentality(U_43, V_44) | ~weaponry(U_43, V_44)))). % 56.65/47.67 tff(c_48, plain, (![U_47, V_48]: (object(U_47, V_48) | ~artifact(U_47, V_48)))). % 56.65/47.67 tff(c_70, plain, (![U_69, V_70]: (impartial(U_69, V_70) | ~organism(U_69, V_70)))). % 56.65/47.67 tff(c_52, plain, (![U_51, V_52]: (thing(U_51, V_52) | ~entity(U_51, V_52)))). % 56.65/47.67 tff(c_26, plain, (![U_25, V_26]: (act(U_25, V_26) | ~action(U_25, V_26)))). % 56.65/47.67 tff(c_46, plain, (![U_45, V_46]: (artifact(U_45, V_46) | ~instrumentality(U_45, V_46)))). % 56.65/47.67 tff(c_68, plain, (![U_67, V_68]: (entity(U_67, V_68) | ~organism(U_67, V_68)))). % 56.65/47.67 tff(c_14, plain, (![U_13, V_14]: (specific(U_13, V_14) | ~eventuality(U_13, V_14)))). % 56.65/47.67 tff(c_66, plain, (![U_65, V_66]: (organism(U_65, V_66) | ~human_person(U_65, V_66)))). % 56.65/47.67 tff(c_42, plain, (![U_41, V_42]: (weaponry(U_41, V_42) | ~weapon(U_41, V_42)))). % 56.65/47.67 tff(c_72, plain, (![U_71, V_72]: (living(U_71, V_72) | ~organism(U_71, V_72)))). % 56.65/47.67 tff(c_74, plain, (![U_73, V_74]: (human(U_73, V_74) | ~human_person(U_73, V_74)))). % 56.65/47.67 tff(c_40, plain, (![U_39, V_40]: (weapon(U_39, V_40) | ~cannon(U_39, V_40)))). % 56.65/47.67 tff(c_176, plain, (of(skc8, skc14, skc15))). % 56.65/47.67 tff(c_182, plain, (patient(skc8, skc9, skc12))). % 56.65/47.67 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 56.65/47.67 tff(c_178, plain, (of(skc8, skc9, skc10))). % 56.65/47.67 tff(c_180, plain, (agent(skc8, skc9, skc11))). % 56.65/47.67 tff(c_154, plain, (male(skc8, skc15))). % 56.65/47.67 tff(c_156, plain, (cannon(skc8, skc14))). % 56.65/47.67 tff(c_158, plain, (cry(skc8, skc12))). % 56.65/47.67 tff(c_174, plain, (six(skc8, skc13))). % 56.65/47.67 tff(c_172, plain, (group(skc8, skc13))). % 56.65/47.67 tff(c_152, plain, (man(skc8, skc15))). % 56.65/47.67 tff(c_170, plain, (scream(skc8, skc9))). % 56.65/47.67 tff(c_160, plain, (male(skc8, skc11))). % 56.65/47.67 tff(c_162, plain, (revenge(skc8, skc10))). % 56.65/47.67 tff(c_164, plain, (event(skc8, skc9))). % 56.65/47.67 tff(c_166, plain, (present(skc8, skc9))). % 56.65/47.67 tff(c_168, plain, (nonreflexive(skc8, skc9))). % 56.65/47.67 tff(c_150, plain, (actual_world(skc8))). % 56.65/47.67 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.65/47.67 %------------------------------------------------------------------------------