%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP074-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 : n003.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:07 PM UTC 2025 % Result : Satisfiable 59.06s 49.70s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP074-1 : TPTP v9.0.0. Released v2.4.0. % 0.06/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 : n003.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:23:03 EDT 2025 % 0.13/0.33 % CPUTime : % 59.06/49.69 % 59.06/49.70 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 59.06/49.70 % 59.06/49.70 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 59.06/49.70 %$ patient > of > member > from_loc > agent > weaponry > weapon > unisex > thing > specific > six > singleton > shot > set > present > organism > object > nonreflexive > nonliving > nonexistent > multiple > man > male > living > instrumentality > impartial > human_person > human > group > fire > existent > eventuality > event > entity > cannon > artifact > animate > action > act > actual_world > skf23 > skf9 > skf22 > skf20 > skf18 > skf16 > skf14 > skf12 > skf10 > #nlpp > skc5 > skc4 > skc3 % 59.06/49.70 % 59.06/49.70 %Foreground sorts: % 59.06/49.70 % 59.06/49.70 % 59.06/49.70 %Background operators: % 59.06/49.70 % 59.06/49.70 % 59.06/49.70 %Foreground operators: % 59.06/49.70 tff(nonliving, type, nonliving: ($i * $i) > $o). % 59.06/49.70 tff(skf10, type, skf10: ($i * $i) > $i). % 59.06/49.70 tff(member, type, member: ($i * $i * $i) > $o). % 59.06/49.70 tff(living, type, living: ($i * $i) > $o). % 59.06/49.70 tff(fire, type, fire: ($i * $i) > $o). % 59.06/49.70 tff(human_person, type, human_person: ($i * $i) > $o). % 59.06/49.70 tff(action, type, action: ($i * $i) > $o). % 59.06/49.70 tff(present, type, present: ($i * $i) > $o). % 59.06/49.70 tff(shot, type, shot: ($i * $i) > $o). % 59.06/49.70 tff(skf22, type, skf22: ($i * $i) > $i). % 59.06/49.70 tff(entity, type, entity: ($i * $i) > $o). % 59.06/49.70 tff(eventuality, type, eventuality: ($i * $i) > $o). % 59.06/49.70 tff(weapon, type, weapon: ($i * $i) > $o). % 59.06/49.70 tff(existent, type, existent: ($i * $i) > $o). % 59.06/49.70 tff(singleton, type, singleton: ($i * $i) > $o). % 59.06/49.70 tff(male, type, male: ($i * $i) > $o). % 59.06/49.70 tff(multiple, type, multiple: ($i * $i) > $o). % 59.06/49.70 tff(organism, type, organism: ($i * $i) > $o). % 59.06/49.70 tff(animate, type, animate: ($i * $i) > $o). % 59.06/49.70 tff(of, type, of: ($i * $i * $i) > $o). % 59.06/49.70 tff(skf14, type, skf14: ($i * $i) > $i). % 59.06/49.70 tff(actual_world, type, actual_world: $i > $o). % 59.06/49.70 tff(agent, type, agent: ($i * $i * $i) > $o). % 59.06/49.70 tff(skf9, type, skf9: ($i * $i) > $i). % 59.06/49.70 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 59.06/49.70 tff(group, type, group: ($i * $i) > $o). % 59.06/49.70 tff(artifact, type, artifact: ($i * $i) > $o). % 59.06/49.70 tff(cannon, type, cannon: ($i * $i) > $o). % 59.06/49.70 tff(event, type, event: ($i * $i) > $o). % 59.06/49.70 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 59.06/49.70 tff(patient, type, patient: ($i * $i * $i) > $o). % 59.06/49.70 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 59.06/49.70 tff(skc4, type, skc4: $i). % 59.06/49.70 tff(skc3, type, skc3: $i). % 59.06/49.70 tff(thing, type, thing: ($i * $i) > $o). % 59.06/49.70 tff(human, type, human: ($i * $i) > $o). % 59.06/49.70 tff(six, type, six: ($i * $i) > $o). % 59.06/49.70 tff(skf18, type, skf18: ($i * $i) > $i). % 59.06/49.70 tff(man, type, man: ($i * $i) > $o). % 59.06/49.70 tff(skc5, type, skc5: $i). % 59.06/49.70 tff(weaponry, type, weaponry: ($i * $i) > $o). % 59.06/49.70 tff(unisex, type, unisex: ($i * $i) > $o). % 59.06/49.70 tff(skf16, type, skf16: ($i * $i) > $i). % 59.06/49.70 tff(set, type, set: ($i * $i) > $o). % 59.06/49.70 tff(skf12, type, skf12: ($i * $i) > $i). % 59.06/49.70 tff(impartial, type, impartial: ($i * $i) > $o). % 59.06/49.70 tff(skf23, type, skf23: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 59.06/49.70 tff(object, type, object: ($i * $i) > $o). % 59.06/49.70 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 59.06/49.70 tff(specific, type, specific: ($i * $i) > $o). % 59.06/49.70 tff(skf20, type, skf20: ($i * $i) > $i). % 59.06/49.70 tff(act, type, act: ($i * $i) > $o). % 59.06/49.70 % 59.06/49.70 %Saturated clause set: % 59.06/49.71 tff(c_1087, plain, (![Z_981, V_978, X2_948, Y_971, W_980, X_952, V_945, V_956, V_962, X1_974, X2_160, X1_963, Z_958, V_163, U_157, Z_944, X2_967, X2_964, X1_973, Z_975, V_965, X_954, Y_951, Z_960, X1_979, X2_976, X1_968, X_161, Y_946, X_943, X2_947, Y_162, X_977, Y_950, Z_961, X1_953, X2_966, W_156, Z_158, V_942, Y_972, X_969, X_955, Y_957, X1_159]: (skf23(V_956, X_954, Y_972, Z_981, X1_953, X2_964, W_156, U_157)=skf23(V_945, X_943, Y_950, Z_961, X1_974, X2_966, W_156, U_157) | skf23(V_962, X_969, Y_971, Z_975, X1_973, X2_976, W_156, U_157)=skf23(V_956, X_954, Y_972, Z_981, X1_953, X2_964, W_156, U_157) | skf23(V_962, X_969, Y_971, Z_975, X1_973, X2_976, W_156, U_157)=skf23(V_945, X_943, Y_950, Z_961, X1_974, X2_966, W_156, U_157) | skf23(V_965, X_977, Y_951, Z_944, X1_963, X2_948, W_156, U_157)=skf23(V_962, X_969, Y_971, Z_975, X1_973, X2_976, W_156, U_157) | skf23(V_965, X_977, Y_951, Z_944, X1_963, X2_948, W_156, U_157)=skf23(V_956, X_954, Y_972, Z_981, X1_953, X2_964, W_156, U_157) | skf23(V_965, X_977, Y_951, Z_944, X1_963, X2_948, W_156, U_157)=skf23(V_945, X_943, Y_950, Z_961, X1_974, X2_966, W_156, U_157) | skf23(V_965, X_977, Y_951, Z_944, X1_963, X2_948, W_156, U_157)=skf23(V_942, X_952, Y_957, Z_960, X1_968, X2_967, W_156, U_157) | skf23(V_962, X_969, Y_971, Z_975, X1_973, X2_976, W_156, U_157)=skf23(V_942, X_952, Y_957, Z_960, X1_968, X2_967, W_156, U_157) | skf23(V_956, X_954, Y_972, Z_981, X1_953, X2_964, W_156, U_157)=skf23(V_942, X_952, Y_957, Z_960, X1_968, X2_967, W_156, U_157) | skf23(V_945, X_943, Y_950, Z_961, X1_974, X2_966, W_156, U_157)=skf23(V_942, X_952, Y_957, Z_960, X1_968, X2_967, W_156, U_157) | skf23(V_942, X_952, Y_957, Z_960, X1_968, X2_967, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_965, X_977, Y_951, Z_944, X1_963, X2_948, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_962, X_969, Y_971, Z_975, X1_973, X2_976, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_956, X_954, Y_972, Z_981, X1_953, X2_964, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_945, X_943, Y_950, Z_961, X1_974, X2_966, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157), V_978, W_980, X_955, Y_946, Z_958, X1_979, X2_947)!=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | X2_966=X1_974 | Z_961=X1_974 | Z_961=X2_966 | Z_961=Y_950 | Y_950=X1_974 | Y_950=X2_966 | Y_950=X_943 | Z_961=X_943 | X_943=X1_974 | X_943=X2_966 | X_943=V_945 | Y_950=V_945 | Z_961=V_945 | X1_974=V_945 | X2_966=V_945 | ~member(U_157, X2_966, W_156) | ~member(U_157, X1_974, W_156) | ~member(U_157, Z_961, W_156) | ~member(U_157, Y_950, W_156) | ~member(U_157, X_943, W_156) | ~member(U_157, V_945, W_156) | X2_964=X1_953 | Z_981=X1_953 | Z_981=X2_964 | Z_981=Y_972 | Y_972=X1_953 | Y_972=X2_964 | Y_972=X_954 | Z_981=X_954 | X_954=X1_953 | X_954=X2_964 | X_954=V_956 | Y_972=V_956 | Z_981=V_956 | X1_953=V_956 | X2_964=V_956 | ~member(U_157, X2_964, W_156) | ~member(U_157, X1_953, W_156) | ~member(U_157, Z_981, W_156) | ~member(U_157, Y_972, W_156) | ~member(U_157, X_954, W_156) | ~member(U_157, V_956, W_156) | X2_976=X1_973 | Z_975=X1_973 | Z_975=X2_976 | Z_975=Y_971 | Y_971=X1_973 | Y_971=X2_976 | Y_971=X_969 | Z_975=X_969 | X_969=X1_973 | X_969=X2_976 | X_969=V_962 | Y_971=V_962 | Z_975=V_962 | X1_973=V_962 | X2_976=V_962 | ~member(U_157, X2_976, W_156) | ~member(U_157, X1_973, W_156) | ~member(U_157, Z_975, W_156) | ~member(U_157, Y_971, W_156) | ~member(U_157, X_969, W_156) | ~member(U_157, V_962, W_156) | X2_948=X1_963 | Z_944=X1_963 | Z_944=X2_948 | Z_944=Y_951 | Y_951=X1_963 | Y_951=X2_948 | Y_951=X_977 | Z_944=X_977 | X_977=X1_963 | X_977=X2_948 | X_977=V_965 | Y_951=V_965 | Z_944=V_965 | X1_963=V_965 | X2_948=V_965 | ~member(U_157, X2_948, W_156) | ~member(U_157, X1_963, W_156) | ~member(U_157, Z_944, W_156) | ~member(U_157, Y_951, W_156) | ~member(U_157, X_977, W_156) | ~member(U_157, V_965, W_156) | X2_967=X1_968 | Z_960=X1_968 | Z_960=X2_967 | Z_960=Y_957 | Y_957=X1_968 | Y_957=X2_967 | Y_957=X_952 | Z_960=X_952 | X_952=X1_968 | X_952=X2_967 | X_952=V_942 | Y_957=V_942 | Z_960=V_942 | X1_968=V_942 | X2_967=V_942 | ~member(U_157, X2_967, W_156) | ~member(U_157, X1_968, W_156) | ~member(U_157, Z_960, W_156) | ~member(U_157, Y_957, W_156) | ~member(U_157, X_952, W_156) | ~member(U_157, V_942, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.71 tff(c_1042, plain, (![W_855, X_851, V_840, Z_843, Z_862, X1_842, X1_847, X_865, V_873, X2_160, V_871, X1_867, X1_859, V_163, U_157, X2_844, Y_861, X_850, X2_866, Y_858, Y_857, Z_863, V_849, X1_856, Z_848, Y_870, X2_845, X_869, X_161, Y_162, X_852, Z_872, X2_854, X2_864, W_156, Z_158, U_841, Y_853, X1_159]: (skf23(V_873, X_865, Y_853, Z_872, X1_859, X2_845, W_156, U_157)=skf23(V_871, X_850, Y_870, Z_848, X1_847, X2_844, W_156, U_157) | skf23(V_871, X_850, Y_870, Z_848, X1_847, X2_844, W_156, U_157)=skf23(V_849, X_851, Y_857, Z_862, X1_856, X2_864, W_156, U_157) | skf23(V_873, X_865, Y_853, Z_872, X1_859, X2_845, W_156, U_157)=skf23(V_849, X_851, Y_857, Z_862, X1_856, X2_864, W_156, U_157) | skf23(V_849, X_851, Y_857, Z_862, X1_856, X2_864, W_156, U_157)=skf23(V_840, X_852, Y_858, Z_863, X1_867, X2_866, W_156, U_157) | skf23(V_871, X_850, Y_870, Z_848, X1_847, X2_844, W_156, U_157)=skf23(V_840, X_852, Y_858, Z_863, X1_867, X2_866, W_156, U_157) | skf23(V_873, X_865, Y_853, Z_872, X1_859, X2_845, W_156, U_157)=skf23(V_840, X_852, Y_858, Z_863, X1_867, X2_866, W_156, U_157) | skf23(V_840, X_852, Y_858, Z_863, X1_867, X2_866, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_849, X_851, Y_857, Z_862, X1_856, X2_864, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_871, X_850, Y_870, Z_848, X1_847, X2_844, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_873, X_865, Y_853, Z_872, X1_859, X2_845, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_841 | skf23(V_840, X_852, Y_858, Z_863, X1_867, X2_866, W_156, U_157)=U_841 | skf23(V_849, X_851, Y_857, Z_862, X1_856, X2_864, W_156, U_157)=U_841 | skf23(V_871, X_850, Y_870, Z_848, X1_847, X2_844, W_156, U_157)=U_841 | skf23(V_873, X_865, Y_853, Z_872, X1_859, X2_845, W_156, U_157)=U_841 | ~member(U_157, U_841, W_156) | skf23(U_841, skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157), W_855, X_869, Y_861, Z_843, X1_842, X2_854)!=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | X2_845=X1_859 | Z_872=X1_859 | Z_872=X2_845 | Z_872=Y_853 | Y_853=X1_859 | Y_853=X2_845 | Y_853=X_865 | Z_872=X_865 | X_865=X1_859 | X_865=X2_845 | X_865=V_873 | Y_853=V_873 | Z_872=V_873 | X1_859=V_873 | X2_845=V_873 | ~member(U_157, X2_845, W_156) | ~member(U_157, X1_859, W_156) | ~member(U_157, Z_872, W_156) | ~member(U_157, Y_853, W_156) | ~member(U_157, X_865, W_156) | ~member(U_157, V_873, W_156) | X2_844=X1_847 | Z_848=X1_847 | Z_848=X2_844 | Z_848=Y_870 | Y_870=X1_847 | Y_870=X2_844 | Y_870=X_850 | Z_848=X_850 | X_850=X1_847 | X_850=X2_844 | X_850=V_871 | Y_870=V_871 | Z_848=V_871 | X1_847=V_871 | X2_844=V_871 | ~member(U_157, X2_844, W_156) | ~member(U_157, X1_847, W_156) | ~member(U_157, Z_848, W_156) | ~member(U_157, Y_870, W_156) | ~member(U_157, X_850, W_156) | ~member(U_157, V_871, W_156) | X2_864=X1_856 | Z_862=X1_856 | Z_862=X2_864 | Z_862=Y_857 | Y_857=X1_856 | Y_857=X2_864 | Y_857=X_851 | Z_862=X_851 | X_851=X1_856 | X_851=X2_864 | X_851=V_849 | Y_857=V_849 | Z_862=V_849 | X1_856=V_849 | X2_864=V_849 | ~member(U_157, X2_864, W_156) | ~member(U_157, X1_856, W_156) | ~member(U_157, Z_862, W_156) | ~member(U_157, Y_857, W_156) | ~member(U_157, X_851, W_156) | ~member(U_157, V_849, W_156) | X2_866=X1_867 | Z_863=X1_867 | Z_863=X2_866 | Z_863=Y_858 | Y_858=X1_867 | Y_858=X2_866 | Y_858=X_852 | Z_863=X_852 | X_852=X1_867 | X_852=X2_866 | X_852=V_840 | Y_858=V_840 | Z_863=V_840 | X1_867=V_840 | X2_866=V_840 | ~member(U_157, X2_866, W_156) | ~member(U_157, X1_867, W_156) | ~member(U_157, Z_863, W_156) | ~member(U_157, Y_858, W_156) | ~member(U_157, X_852, W_156) | ~member(U_157, V_840, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.72 tff(c_1064, plain, (![Y_878, W_900, Y_883, X_880, X_891, Z_898, X2_160, Z_902, V_876, V_163, X2_896, V_882, U_157, X1_890, X2_888, X2_877, X_894, X2_881, Y_885, Y_899, Z_908, Z_889, Z_893, V_879, X1_897, X_161, Y_162, V_884, X1_875, X1_906, X_892, U_903, X2_904, W_156, Z_158, X1_886, Y_907, X1_159, X_905, V_874]: (skf23(V_884, X_894, Y_878, Z_898, X1_875, X2_877, W_156, U_157)=skf23(V_876, X_905, Y_907, Z_893, X1_890, X2_881, W_156, U_157) | skf23(V_882, X_891, Y_899, Z_908, X1_886, X2_904, W_156, U_157)=skf23(V_876, X_905, Y_907, Z_893, X1_890, X2_881, W_156, U_157) | skf23(V_884, X_894, Y_878, Z_898, X1_875, X2_877, W_156, U_157)=skf23(V_882, X_891, Y_899, Z_908, X1_886, X2_904, W_156, U_157) | skf23(V_882, X_891, Y_899, Z_908, X1_886, X2_904, W_156, U_157)=skf23(V_874, X_880, Y_883, Z_889, X1_897, X2_896, W_156, U_157) | skf23(V_876, X_905, Y_907, Z_893, X1_890, X2_881, W_156, U_157)=skf23(V_874, X_880, Y_883, Z_889, X1_897, X2_896, W_156, U_157) | skf23(V_884, X_894, Y_878, Z_898, X1_875, X2_877, W_156, U_157)=skf23(V_874, X_880, Y_883, Z_889, X1_897, X2_896, W_156, U_157) | skf23(V_874, X_880, Y_883, Z_889, X1_897, X2_896, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_882, X_891, Y_899, Z_908, X1_886, X2_904, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_876, X_905, Y_907, Z_893, X1_890, X2_881, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_884, X_894, Y_878, Z_898, X1_875, X2_877, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_903 | skf23(V_874, X_880, Y_883, Z_889, X1_897, X2_896, W_156, U_157)=U_903 | skf23(V_882, X_891, Y_899, Z_908, X1_886, X2_904, W_156, U_157)=U_903 | skf23(V_876, X_905, Y_907, Z_893, X1_890, X2_881, W_156, U_157)=U_903 | skf23(V_884, X_894, Y_878, Z_898, X1_875, X2_877, W_156, U_157)=U_903 | ~member(U_157, U_903, W_156) | skf23(U_903, V_879, W_900, X_892, Y_885, Z_902, X1_906, X2_888)!=U_903 | X2_877=X1_875 | Z_898=X1_875 | Z_898=X2_877 | Z_898=Y_878 | Y_878=X1_875 | Y_878=X2_877 | Y_878=X_894 | Z_898=X_894 | X_894=X1_875 | X_894=X2_877 | X_894=V_884 | Y_878=V_884 | Z_898=V_884 | X1_875=V_884 | X2_877=V_884 | ~member(U_157, X2_877, W_156) | ~member(U_157, X1_875, W_156) | ~member(U_157, Z_898, W_156) | ~member(U_157, Y_878, W_156) | ~member(U_157, X_894, W_156) | ~member(U_157, V_884, W_156) | X2_881=X1_890 | Z_893=X1_890 | Z_893=X2_881 | Z_893=Y_907 | Y_907=X1_890 | Y_907=X2_881 | Y_907=X_905 | Z_893=X_905 | X_905=X1_890 | X_905=X2_881 | X_905=V_876 | Y_907=V_876 | Z_893=V_876 | X1_890=V_876 | X2_881=V_876 | ~member(U_157, X2_881, W_156) | ~member(U_157, X1_890, W_156) | ~member(U_157, Z_893, W_156) | ~member(U_157, Y_907, W_156) | ~member(U_157, X_905, W_156) | ~member(U_157, V_876, W_156) | X2_904=X1_886 | Z_908=X1_886 | Z_908=X2_904 | Z_908=Y_899 | Y_899=X1_886 | Y_899=X2_904 | Y_899=X_891 | Z_908=X_891 | X_891=X1_886 | X_891=X2_904 | X_891=V_882 | Y_899=V_882 | Z_908=V_882 | X1_886=V_882 | X2_904=V_882 | ~member(U_157, X2_904, W_156) | ~member(U_157, X1_886, W_156) | ~member(U_157, Z_908, W_156) | ~member(U_157, Y_899, W_156) | ~member(U_157, X_891, W_156) | ~member(U_157, V_882, W_156) | X2_896=X1_897 | Z_889=X1_897 | Z_889=X2_896 | Z_889=Y_883 | Y_883=X1_897 | Y_883=X2_896 | Y_883=X_880 | Z_889=X_880 | X_880=X1_897 | X_880=X2_896 | X_880=V_874 | Y_883=V_874 | Z_889=V_874 | X1_897=V_874 | X2_896=V_874 | ~member(U_157, X2_896, W_156) | ~member(U_157, X1_897, W_156) | ~member(U_157, Z_889, W_156) | ~member(U_157, Y_883, W_156) | ~member(U_157, X_880, W_156) | ~member(U_157, V_874, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.72 tff(c_997, plain, (![X1_762, X1_780, V_757, V_768, X2_160, Y_771, V_778, V_163, U_761, X_759, U_157, X_763, Y_775, Z_766, Z_758, X2_782, X2_772, Y_765, X2_760, X_161, Y_162, X2_756, X1_774, Z_770, X1_783, Y_781, W_156, X_767, V_773, Z_764, Z_158, X1_159, X_776]: (skf23(V_778, X_759, Y_781, Z_766, X1_780, X2_760, W_156, U_157)=skf23(V_773, X_776, Y_771, Z_758, X1_762, X2_782, W_156, U_157) | skf23(V_773, X_776, Y_771, Z_758, X1_762, X2_782, W_156, U_157)=skf23(V_757, X_763, Y_765, Z_770, X1_774, X2_772, W_156, U_157) | skf23(V_778, X_759, Y_781, Z_766, X1_780, X2_760, W_156, U_157)=skf23(V_757, X_763, Y_765, Z_770, X1_774, X2_772, W_156, U_157) | skf23(V_757, X_763, Y_765, Z_770, X1_774, X2_772, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_773, X_776, Y_771, Z_758, X1_762, X2_782, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_778, X_759, Y_781, Z_766, X1_780, X2_760, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_768 | skf23(V_757, X_763, Y_765, Z_770, X1_774, X2_772, W_156, U_157)=V_768 | skf23(V_773, X_776, Y_771, Z_758, X1_762, X2_782, W_156, U_157)=V_768 | skf23(V_778, X_759, Y_781, Z_766, X1_780, X2_760, W_156, U_157)=V_768 | V_768=U_761 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_761 | skf23(V_757, X_763, Y_765, Z_770, X1_774, X2_772, W_156, U_157)=U_761 | skf23(V_773, X_776, Y_771, Z_758, X1_762, X2_782, W_156, U_157)=U_761 | skf23(V_778, X_759, Y_781, Z_766, X1_780, X2_760, W_156, U_157)=U_761 | ~member(U_157, V_768, W_156) | ~member(U_157, U_761, W_156) | skf23(U_761, V_768, skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157), X_767, Y_775, Z_764, X1_783, X2_756)!=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | X2_760=X1_780 | Z_766=X1_780 | Z_766=X2_760 | Z_766=Y_781 | Y_781=X1_780 | Y_781=X2_760 | Y_781=X_759 | Z_766=X_759 | X_759=X1_780 | X_759=X2_760 | X_759=V_778 | Y_781=V_778 | Z_766=V_778 | X1_780=V_778 | X2_760=V_778 | ~member(U_157, X2_760, W_156) | ~member(U_157, X1_780, W_156) | ~member(U_157, Z_766, W_156) | ~member(U_157, Y_781, W_156) | ~member(U_157, X_759, W_156) | ~member(U_157, V_778, W_156) | X2_782=X1_762 | Z_758=X1_762 | Z_758=X2_782 | Z_758=Y_771 | Y_771=X1_762 | Y_771=X2_782 | Y_771=X_776 | Z_758=X_776 | X_776=X1_762 | X_776=X2_782 | X_776=V_773 | Y_771=V_773 | Z_758=V_773 | X1_762=V_773 | X2_782=V_773 | ~member(U_157, X2_782, W_156) | ~member(U_157, X1_762, W_156) | ~member(U_157, Z_758, W_156) | ~member(U_157, Y_771, W_156) | ~member(U_157, X_776, W_156) | ~member(U_157, V_773, W_156) | X2_772=X1_774 | Z_770=X1_774 | Z_770=X2_772 | Z_770=Y_765 | Y_765=X1_774 | Y_765=X2_772 | Y_765=X_763 | Z_770=X_763 | X_763=X1_774 | X_763=X2_772 | X_763=V_757 | Y_765=V_757 | Z_770=V_757 | X1_774=V_757 | X2_772=V_757 | ~member(U_157, X2_772, W_156) | ~member(U_157, X1_774, W_156) | ~member(U_157, Z_770, W_156) | ~member(U_157, Y_765, W_156) | ~member(U_157, X_763, W_156) | ~member(U_157, V_757, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.72 tff(c_975, plain, (![Y_755, Z_750, V_747, X1_745, V_753, X2_741, X_735, X_730, X2_160, Y_748, V_163, U_157, V_726, Z_740, Y_729, V_737, X1_733, X2_744, Z_752, W_728, U_732, X2_738, X5_754, X_161, X2_727, Y_162, X1_749, X_734, X_743, Y_736, W_156, Z_158, X1_731, X1_159, Z_742]: (skf23(V_747, X_735, Y_755, Z_742, X1_733, X2_741, W_156, U_157)=skf23(V_737, X_730, Y_748, Z_750, X1_749, X2_727, W_156, U_157) | skf23(V_737, X_730, Y_748, Z_750, X1_749, X2_727, W_156, U_157)=skf23(V_726, X_734, Y_736, Z_740, X1_745, X2_744, W_156, U_157) | skf23(V_747, X_735, Y_755, Z_742, X1_733, X2_741, W_156, U_157)=skf23(V_726, X_734, Y_736, Z_740, X1_745, X2_744, W_156, U_157) | skf23(V_726, X_734, Y_736, Z_740, X1_745, X2_744, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_737, X_730, Y_748, Z_750, X1_749, X2_727, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_747, X_735, Y_755, Z_742, X1_733, X2_741, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X5_754 | skf23(V_726, X_734, Y_736, Z_740, X1_745, X2_744, W_156, U_157)=X5_754 | skf23(V_737, X_730, Y_748, Z_750, X1_749, X2_727, W_156, U_157)=X5_754 | skf23(V_747, X_735, Y_755, Z_742, X1_733, X2_741, W_156, U_157)=X5_754 | X5_754=U_732 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_732 | skf23(V_726, X_734, Y_736, Z_740, X1_745, X2_744, W_156, U_157)=U_732 | skf23(V_737, X_730, Y_748, Z_750, X1_749, X2_727, W_156, U_157)=U_732 | skf23(V_747, X_735, Y_755, Z_742, X1_733, X2_741, W_156, U_157)=U_732 | ~member(U_157, X5_754, W_156) | ~member(U_157, U_732, W_156) | skf23(U_732, V_753, W_728, X_743, Y_729, Z_752, X1_731, X2_738)!=U_732 | X2_741=X1_733 | Z_742=X1_733 | Z_742=X2_741 | Z_742=Y_755 | Y_755=X1_733 | Y_755=X2_741 | Y_755=X_735 | Z_742=X_735 | X_735=X1_733 | X_735=X2_741 | X_735=V_747 | Y_755=V_747 | Z_742=V_747 | X1_733=V_747 | X2_741=V_747 | ~member(U_157, X2_741, W_156) | ~member(U_157, X1_733, W_156) | ~member(U_157, Z_742, W_156) | ~member(U_157, Y_755, W_156) | ~member(U_157, X_735, W_156) | ~member(U_157, V_747, W_156) | X2_727=X1_749 | Z_750=X1_749 | Z_750=X2_727 | Z_750=Y_748 | Y_748=X1_749 | Y_748=X2_727 | Y_748=X_730 | Z_750=X_730 | X_730=X1_749 | X_730=X2_727 | X_730=V_737 | Y_748=V_737 | Z_750=V_737 | X1_749=V_737 | X2_727=V_737 | ~member(U_157, X2_727, W_156) | ~member(U_157, X1_749, W_156) | ~member(U_157, Z_750, W_156) | ~member(U_157, Y_748, W_156) | ~member(U_157, X_730, W_156) | ~member(U_157, V_737, W_156) | X2_744=X1_745 | Z_740=X1_745 | Z_740=X2_744 | Z_740=Y_736 | Y_736=X1_745 | Y_736=X2_744 | Y_736=X_734 | Z_740=X_734 | X_734=X1_745 | X_734=X2_744 | X_734=V_726 | Y_736=V_726 | Z_740=V_726 | X1_745=V_726 | X2_744=V_726 | ~member(U_157, X2_744, W_156) | ~member(U_157, X1_745, W_156) | ~member(U_157, Z_740, W_156) | ~member(U_157, Y_736, W_156) | ~member(U_157, X_734, W_156) | ~member(U_157, V_726, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.72 tff(c_1019, plain, (![V_810, X_792, X2_795, X2_160, Y_797, X_793, V_163, X2_805, X1_804, U_157, X1_788, X1_799, Z_790, X_785, V_784, Y_798, U_791, X2_786, V_811, V_796, Z_803, Y_809, X_161, X2_794, Z_801, Y_162, W_787, Y_812, W_156, X1_806, Z_158, Z_789, X1_159, X_800]: (skf23(V_811, X_785, Y_797, Z_790, X1_788, X2_795, W_156, U_157)=skf23(V_796, X_793, Y_812, Z_789, X1_799, X2_794, W_156, U_157) | skf23(V_796, X_793, Y_812, Z_789, X1_799, X2_794, W_156, U_157)=skf23(V_784, X_792, Y_798, Z_803, X1_806, X2_805, W_156, U_157) | skf23(V_811, X_785, Y_797, Z_790, X1_788, X2_795, W_156, U_157)=skf23(V_784, X_792, Y_798, Z_803, X1_806, X2_805, W_156, U_157) | skf23(V_784, X_792, Y_798, Z_803, X1_806, X2_805, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_796, X_793, Y_812, Z_789, X1_799, X2_794, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_811, X_785, Y_797, Z_790, X1_788, X2_795, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_810 | skf23(V_784, X_792, Y_798, Z_803, X1_806, X2_805, W_156, U_157)=V_810 | skf23(V_796, X_793, Y_812, Z_789, X1_799, X2_794, W_156, U_157)=V_810 | skf23(V_811, X_785, Y_797, Z_790, X1_788, X2_795, W_156, U_157)=V_810 | V_810=U_791 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_791 | skf23(V_784, X_792, Y_798, Z_803, X1_806, X2_805, W_156, U_157)=U_791 | skf23(V_796, X_793, Y_812, Z_789, X1_799, X2_794, W_156, U_157)=U_791 | skf23(V_811, X_785, Y_797, Z_790, X1_788, X2_795, W_156, U_157)=U_791 | ~member(U_157, V_810, W_156) | ~member(U_157, U_791, W_156) | skf23(U_791, V_810, W_787, X_800, Y_809, Z_801, X1_804, X2_786)!=V_810 | X2_795=X1_788 | Z_790=X1_788 | Z_790=X2_795 | Z_790=Y_797 | Y_797=X1_788 | Y_797=X2_795 | Y_797=X_785 | Z_790=X_785 | X_785=X1_788 | X_785=X2_795 | X_785=V_811 | Y_797=V_811 | Z_790=V_811 | X1_788=V_811 | X2_795=V_811 | ~member(U_157, X2_795, W_156) | ~member(U_157, X1_788, W_156) | ~member(U_157, Z_790, W_156) | ~member(U_157, Y_797, W_156) | ~member(U_157, X_785, W_156) | ~member(U_157, V_811, W_156) | X2_794=X1_799 | Z_789=X1_799 | Z_789=X2_794 | Z_789=Y_812 | Y_812=X1_799 | Y_812=X2_794 | Y_812=X_793 | Z_789=X_793 | X_793=X1_799 | X_793=X2_794 | X_793=V_796 | Y_812=V_796 | Z_789=V_796 | X1_799=V_796 | X2_794=V_796 | ~member(U_157, X2_794, W_156) | ~member(U_157, X1_799, W_156) | ~member(U_157, Z_789, W_156) | ~member(U_157, Y_812, W_156) | ~member(U_157, X_793, W_156) | ~member(U_157, V_796, W_156) | X2_805=X1_806 | Z_803=X1_806 | Z_803=X2_805 | Z_803=Y_798 | Y_798=X1_806 | Y_798=X2_805 | Y_798=X_792 | Z_803=X_792 | X_792=X1_806 | X_792=X2_805 | X_792=V_784 | Y_798=V_784 | Z_803=V_784 | X1_806=V_784 | X2_805=V_784 | ~member(U_157, X2_805, W_156) | ~member(U_157, X1_806, W_156) | ~member(U_157, Z_803, W_156) | ~member(U_157, Y_798, W_156) | ~member(U_157, X_792, W_156) | ~member(U_157, V_784, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.72 tff(c_886, plain, (![X2_627, Y_614, X2_612, Z_618, X2_160, Z_622, X_613, V_163, X1_625, U_157, X1_628, V_611, X2_632, Y_617, Y_616, V_629, U_624, X_619, V_621, X_161, W_631, Y_162, X1_626, W_156, Z_158, Z_623, X1_159]: (skf23(V_629, X_619, Y_614, Z_618, X1_626, X2_632, W_156, U_157)=skf23(V_611, X_613, Y_617, Z_622, X1_628, X2_627, W_156, U_157) | skf23(V_611, X_613, Y_617, Z_622, X1_628, X2_627, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_629, X_619, Y_614, Z_618, X1_626, X2_632, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=W_631 | skf23(V_611, X_613, Y_617, Z_622, X1_628, X2_627, W_156, U_157)=W_631 | skf23(V_629, X_619, Y_614, Z_618, X1_626, X2_632, W_156, U_157)=W_631 | W_631=V_621 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_621 | skf23(V_611, X_613, Y_617, Z_622, X1_628, X2_627, W_156, U_157)=V_621 | skf23(V_629, X_619, Y_614, Z_618, X1_626, X2_632, W_156, U_157)=V_621 | V_621=U_624 | W_631=U_624 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_624 | skf23(V_611, X_613, Y_617, Z_622, X1_628, X2_627, W_156, U_157)=U_624 | skf23(V_629, X_619, Y_614, Z_618, X1_626, X2_632, W_156, U_157)=U_624 | ~member(U_157, W_631, W_156) | ~member(U_157, V_621, W_156) | ~member(U_157, U_624, W_156) | skf23(U_624, V_621, W_631, skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157), Y_616, Z_623, X1_625, X2_612)!=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | X2_632=X1_626 | Z_618=X1_626 | Z_618=X2_632 | Z_618=Y_614 | Y_614=X1_626 | Y_614=X2_632 | Y_614=X_619 | Z_618=X_619 | X_619=X1_626 | X_619=X2_632 | X_619=V_629 | Y_614=V_629 | Z_618=V_629 | X1_626=V_629 | X2_632=V_629 | ~member(U_157, X2_632, W_156) | ~member(U_157, X1_626, W_156) | ~member(U_157, Z_618, W_156) | ~member(U_157, Y_614, W_156) | ~member(U_157, X_619, W_156) | ~member(U_157, V_629, W_156) | X2_627=X1_628 | Z_622=X1_628 | Z_622=X2_627 | Z_622=Y_617 | Y_617=X1_628 | Y_617=X2_627 | Y_617=X_613 | Z_622=X_613 | X_613=X1_628 | X_613=X2_627 | X_613=V_611 | Y_617=V_611 | Z_622=V_611 | X1_628=V_611 | X2_627=V_611 | ~member(U_157, X2_627, W_156) | ~member(U_157, X1_628, W_156) | ~member(U_157, Z_622, W_156) | ~member(U_157, Y_617, W_156) | ~member(U_157, X_613, W_156) | ~member(U_157, V_611, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.72 tff(c_930, plain, (![V_656, X1_659, U_678, V_661, X1_674, Y_666, Z_676, X2_160, X1_664, X_662, V_163, X2_677, U_157, W_668, X2_673, Z_657, X_671, Z_670, Y_667, X_161, Y_162, X5_658, X_672, V_663, W_156, Z_158, Y_665, X2_660, X1_159]: (skf23(V_663, X_671, Y_665, Z_657, X1_664, X2_677, W_156, U_157)=skf23(V_656, X_662, Y_666, Z_670, X1_674, X2_673, W_156, U_157) | skf23(V_656, X_662, Y_666, Z_670, X1_674, X2_673, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_663, X_671, Y_665, Z_657, X1_664, X2_677, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X5_658 | skf23(V_656, X_662, Y_666, Z_670, X1_674, X2_673, W_156, U_157)=X5_658 | skf23(V_663, X_671, Y_665, Z_657, X1_664, X2_677, W_156, U_157)=X5_658 | X5_658=V_661 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_661 | skf23(V_656, X_662, Y_666, Z_670, X1_674, X2_673, W_156, U_157)=V_661 | skf23(V_663, X_671, Y_665, Z_657, X1_664, X2_677, W_156, U_157)=V_661 | V_661=U_678 | X5_658=U_678 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_678 | skf23(V_656, X_662, Y_666, Z_670, X1_674, X2_673, W_156, U_157)=U_678 | skf23(V_663, X_671, Y_665, Z_657, X1_664, X2_677, W_156, U_157)=U_678 | ~member(U_157, X5_658, W_156) | ~member(U_157, V_661, W_156) | ~member(U_157, U_678, W_156) | skf23(U_678, V_661, W_668, X_672, Y_667, Z_676, X1_659, X2_660)!=V_661 | X2_677=X1_664 | Z_657=X1_664 | Z_657=X2_677 | Z_657=Y_665 | Y_665=X1_664 | Y_665=X2_677 | Y_665=X_671 | Z_657=X_671 | X_671=X1_664 | X_671=X2_677 | X_671=V_663 | Y_665=V_663 | Z_657=V_663 | X1_664=V_663 | X2_677=V_663 | ~member(U_157, X2_677, W_156) | ~member(U_157, X1_664, W_156) | ~member(U_157, Z_657, W_156) | ~member(U_157, Y_665, W_156) | ~member(U_157, X_671, W_156) | ~member(U_157, V_663, W_156) | X2_673=X1_674 | Z_670=X1_674 | Z_670=X2_673 | Z_670=Y_666 | Y_666=X1_674 | Y_666=X2_673 | Y_666=X_662 | Z_670=X_662 | X_662=X1_674 | X_662=X2_673 | X_662=V_656 | Y_666=V_656 | Z_670=V_656 | X1_674=V_656 | X2_673=V_656 | ~member(U_157, X2_673, W_156) | ~member(U_157, X1_674, W_156) | ~member(U_157, Z_670, W_156) | ~member(U_157, Y_666, W_156) | ~member(U_157, X_662, W_156) | ~member(U_157, V_656, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.72 tff(c_908, plain, (![X_641, X1_648, V_645, X1_652, X2_160, W_646, X2_635, V_633, V_163, Z_644, X1_636, V_639, U_157, X_640, Z_654, U_655, Z_651, Y_638, X2_647, Y_642, X_161, Y_650, Y_162, X_653, X2_637, W_156, Z_158, X1_159]: (skf23(V_645, X_653, Y_638, Z_651, X1_652, X2_637, W_156, U_157)=skf23(V_633, X_640, Y_642, Z_644, X1_648, X2_647, W_156, U_157) | skf23(V_633, X_640, Y_642, Z_644, X1_648, X2_647, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_645, X_653, Y_638, Z_651, X1_652, X2_637, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=W_646 | skf23(V_633, X_640, Y_642, Z_644, X1_648, X2_647, W_156, U_157)=W_646 | skf23(V_645, X_653, Y_638, Z_651, X1_652, X2_637, W_156, U_157)=W_646 | W_646=V_639 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_639 | skf23(V_633, X_640, Y_642, Z_644, X1_648, X2_647, W_156, U_157)=V_639 | skf23(V_645, X_653, Y_638, Z_651, X1_652, X2_637, W_156, U_157)=V_639 | V_639=U_655 | W_646=U_655 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_655 | skf23(V_633, X_640, Y_642, Z_644, X1_648, X2_647, W_156, U_157)=U_655 | skf23(V_645, X_653, Y_638, Z_651, X1_652, X2_637, W_156, U_157)=U_655 | ~member(U_157, W_646, W_156) | ~member(U_157, V_639, W_156) | ~member(U_157, U_655, W_156) | skf23(U_655, V_639, W_646, X_641, Y_650, Z_654, X1_636, X2_635)!=W_646 | X2_637=X1_652 | Z_651=X1_652 | Z_651=X2_637 | Z_651=Y_638 | Y_638=X1_652 | Y_638=X2_637 | Y_638=X_653 | Z_651=X_653 | X_653=X1_652 | X_653=X2_637 | X_653=V_645 | Y_638=V_645 | Z_651=V_645 | X1_652=V_645 | X2_637=V_645 | ~member(U_157, X2_637, W_156) | ~member(U_157, X1_652, W_156) | ~member(U_157, Z_651, W_156) | ~member(U_157, Y_638, W_156) | ~member(U_157, X_653, W_156) | ~member(U_157, V_645, W_156) | X2_647=X1_648 | Z_644=X1_648 | Z_644=X2_647 | Z_644=Y_642 | Y_642=X1_648 | Y_642=X2_647 | Y_642=X_640 | Z_644=X_640 | X_640=X1_648 | X_640=X2_647 | X_640=V_633 | Y_642=V_633 | Z_644=V_633 | X1_648=V_633 | X2_647=V_633 | ~member(U_157, X2_647, W_156) | ~member(U_157, X1_648, W_156) | ~member(U_157, Z_644, W_156) | ~member(U_157, Y_642, W_156) | ~member(U_157, X_640, W_156) | ~member(U_157, V_633, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.73 tff(c_952, plain, (![U_684, Y_688, X_687, X2_694, Y_699, V_690, X1_691, X2_160, V_163, V_693, U_157, X6_689, Z_686, X2_680, Y_692, X_685, W_682, X1_704, Z_702, V_681, X2_700, Z_696, X_161, X1_701, Y_162, X_683, W_156, Z_158, X1_159, X5_697]: (skf23(V_693, X_683, Y_692, Z_702, X1_704, X2_694, W_156, U_157)=skf23(V_681, X_685, Y_688, Z_696, X1_701, X2_700, W_156, U_157) | skf23(V_681, X_685, Y_688, Z_696, X1_701, X2_700, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_693, X_683, Y_692, Z_702, X1_704, X2_694, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X6_689 | skf23(V_681, X_685, Y_688, Z_696, X1_701, X2_700, W_156, U_157)=X6_689 | skf23(V_693, X_683, Y_692, Z_702, X1_704, X2_694, W_156, U_157)=X6_689 | X6_689=X5_697 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X5_697 | skf23(V_681, X_685, Y_688, Z_696, X1_701, X2_700, W_156, U_157)=X5_697 | skf23(V_693, X_683, Y_692, Z_702, X1_704, X2_694, W_156, U_157)=X5_697 | X5_697=U_684 | X6_689=U_684 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_684 | skf23(V_681, X_685, Y_688, Z_696, X1_701, X2_700, W_156, U_157)=U_684 | skf23(V_693, X_683, Y_692, Z_702, X1_704, X2_694, W_156, U_157)=U_684 | ~member(U_157, X6_689, W_156) | ~member(U_157, X5_697, W_156) | ~member(U_157, U_684, W_156) | skf23(U_684, V_690, W_682, X_687, Y_699, Z_686, X1_691, X2_680)!=U_684 | X2_694=X1_704 | Z_702=X1_704 | Z_702=X2_694 | Z_702=Y_692 | Y_692=X1_704 | Y_692=X2_694 | Y_692=X_683 | Z_702=X_683 | X_683=X1_704 | X_683=X2_694 | X_683=V_693 | Y_692=V_693 | Z_702=V_693 | X1_704=V_693 | X2_694=V_693 | ~member(U_157, X2_694, W_156) | ~member(U_157, X1_704, W_156) | ~member(U_157, Z_702, W_156) | ~member(U_157, Y_692, W_156) | ~member(U_157, X_683, W_156) | ~member(U_157, V_693, W_156) | X2_700=X1_701 | Z_696=X1_701 | Z_696=X2_700 | Z_696=Y_688 | Y_688=X1_701 | Y_688=X2_700 | Y_688=X_685 | Z_696=X_685 | X_685=X1_701 | X_685=X2_700 | X_685=V_681 | Y_688=V_681 | Z_696=V_681 | X1_701=V_681 | X2_700=V_681 | ~member(U_157, X2_700, W_156) | ~member(U_157, X1_701, W_156) | ~member(U_157, Z_696, W_156) | ~member(U_157, Y_688, W_156) | ~member(U_157, X_685, W_156) | ~member(U_157, V_681, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.73 tff(c_841, plain, (![X_575, V_563, X1_568, X1_571, X2_577, Y_573, X2_572, X2_160, U_574, V_163, U_157, X_576, W_564, V_569, X_161, Y_162, Z_565, Z_567, W_156, Z_158, X1_159]: (skf23(V_569, X_576, Y_573, Z_567, X1_571, X2_577, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X_575 | skf23(V_569, X_576, Y_573, Z_567, X1_571, X2_577, W_156, U_157)=X_575 | X_575=W_564 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=W_564 | skf23(V_569, X_576, Y_573, Z_567, X1_571, X2_577, W_156, U_157)=W_564 | W_564=V_563 | X_575=V_563 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_563 | skf23(V_569, X_576, Y_573, Z_567, X1_571, X2_577, W_156, U_157)=V_563 | V_563=U_574 | W_564=U_574 | X_575=U_574 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_574 | skf23(V_569, X_576, Y_573, Z_567, X1_571, X2_577, W_156, U_157)=U_574 | ~member(U_157, X_575, W_156) | ~member(U_157, W_564, W_156) | ~member(U_157, V_563, W_156) | ~member(U_157, U_574, W_156) | skf23(U_574, V_563, W_564, X_575, skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157), Z_565, X1_568, X2_572)!=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | X2_577=X1_571 | Z_567=X1_571 | Z_567=X2_577 | Z_567=Y_573 | Y_573=X1_571 | Y_573=X2_577 | Y_573=X_576 | Z_567=X_576 | X_576=X1_571 | X_576=X2_577 | X_576=V_569 | Y_573=V_569 | Z_567=V_569 | X1_571=V_569 | X2_577=V_569 | ~member(U_157, X2_577, W_156) | ~member(U_157, X1_571, W_156) | ~member(U_157, Z_567, W_156) | ~member(U_157, Y_573, W_156) | ~member(U_157, X_576, W_156) | ~member(U_157, V_569, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.73 tff(c_797, plain, (![X_542, X5_536, X2_544, Y_540, W_525, X2_160, X1_535, V_163, X6_531, U_157, X2_543, X_528, X1_539, V_532, Y_537, Z_541, U_534, X_161, X7_538, Y_162, Z_529, V_530, W_156, Z_158, X1_159]: (skf23(V_532, X_542, Y_540, Z_529, X1_535, X2_544, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X7_538 | skf23(V_532, X_542, Y_540, Z_529, X1_535, X2_544, W_156, U_157)=X7_538 | X7_538=X6_531 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X6_531 | skf23(V_532, X_542, Y_540, Z_529, X1_535, X2_544, W_156, U_157)=X6_531 | X6_531=X5_536 | X7_538=X5_536 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X5_536 | skf23(V_532, X_542, Y_540, Z_529, X1_535, X2_544, W_156, U_157)=X5_536 | X5_536=U_534 | X6_531=U_534 | X7_538=U_534 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_534 | skf23(V_532, X_542, Y_540, Z_529, X1_535, X2_544, W_156, U_157)=U_534 | ~member(U_157, X7_538, W_156) | ~member(U_157, X6_531, W_156) | ~member(U_157, X5_536, W_156) | ~member(U_157, U_534, W_156) | skf23(U_534, V_530, W_525, X_528, Y_537, Z_541, X1_539, X2_543)!=U_534 | X2_544=X1_535 | Z_529=X1_535 | Z_529=X2_544 | Z_529=Y_540 | Y_540=X1_535 | Y_540=X2_544 | Y_540=X_542 | Z_529=X_542 | X_542=X1_535 | X_542=X2_544 | X_542=V_532 | Y_540=V_532 | Z_529=V_532 | X1_535=V_532 | X2_544=V_532 | ~member(U_157, X2_544, W_156) | ~member(U_157, X1_535, W_156) | ~member(U_157, Z_529, W_156) | ~member(U_157, Y_540, W_156) | ~member(U_157, X_542, W_156) | ~member(U_157, V_532, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.73 tff(c_775, plain, (![U_509, X1_514, X2_524, X_521, X2_510, X2_160, X5_515, V_163, Z_516, W_522, U_157, Y_506, X1_520, X_518, Y_517, X_161, Z_508, Y_162, X6_511, W_156, Z_158, V_512, V_523, X1_159]: (skf23(V_512, X_521, Y_517, Z_508, X1_514, X2_524, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X6_511 | skf23(V_512, X_521, Y_517, Z_508, X1_514, X2_524, W_156, U_157)=X6_511 | X6_511=X5_515 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X5_515 | skf23(V_512, X_521, Y_517, Z_508, X1_514, X2_524, W_156, U_157)=X5_515 | X5_515=V_523 | X6_511=V_523 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_523 | skf23(V_512, X_521, Y_517, Z_508, X1_514, X2_524, W_156, U_157)=V_523 | V_523=U_509 | X5_515=U_509 | X6_511=U_509 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_509 | skf23(V_512, X_521, Y_517, Z_508, X1_514, X2_524, W_156, U_157)=U_509 | ~member(U_157, X6_511, W_156) | ~member(U_157, X5_515, W_156) | ~member(U_157, V_523, W_156) | ~member(U_157, U_509, W_156) | skf23(U_509, V_523, W_522, X_518, Y_506, Z_516, X1_520, X2_510)!=V_523 | X2_524=X1_514 | Z_508=X1_514 | Z_508=X2_524 | Z_508=Y_517 | Y_517=X1_514 | Y_517=X2_524 | Y_517=X_521 | Z_508=X_521 | X_521=X1_514 | X_521=X2_524 | X_521=V_512 | Y_517=V_512 | Z_508=V_512 | X1_514=V_512 | X2_524=V_512 | ~member(U_157, X2_524, W_156) | ~member(U_157, X1_514, W_156) | ~member(U_157, Z_508, W_156) | ~member(U_157, Y_517, W_156) | ~member(U_157, X_521, W_156) | ~member(U_157, V_512, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.73 tff(c_863, plain, (![Y_583, X_580, Y_587, X5_582, X2_160, X2_593, V_163, W_588, X_590, U_157, V_592, X1_591, V_584, Z_581, X_161, Y_162, X2_595, Z_578, W_156, X1_586, Z_158, U_594, X1_159]: (skf23(V_584, X_590, Y_587, Z_581, X1_586, X2_593, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X5_582 | skf23(V_584, X_590, Y_587, Z_581, X1_586, X2_593, W_156, U_157)=X5_582 | X5_582=W_588 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=W_588 | skf23(V_584, X_590, Y_587, Z_581, X1_586, X2_593, W_156, U_157)=W_588 | W_588=V_592 | X5_582=V_592 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_592 | skf23(V_584, X_590, Y_587, Z_581, X1_586, X2_593, W_156, U_157)=V_592 | V_592=U_594 | W_588=U_594 | X5_582=U_594 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_594 | skf23(V_584, X_590, Y_587, Z_581, X1_586, X2_593, W_156, U_157)=U_594 | ~member(U_157, X5_582, W_156) | ~member(U_157, W_588, W_156) | ~member(U_157, V_592, W_156) | ~member(U_157, U_594, W_156) | skf23(U_594, V_592, W_588, X_580, Y_583, Z_578, X1_591, X2_595)!=W_588 | X2_593=X1_586 | Z_581=X1_586 | Z_581=X2_593 | Z_581=Y_587 | Y_587=X1_586 | Y_587=X2_593 | Y_587=X_590 | Z_581=X_590 | X_590=X1_586 | X_590=X2_593 | X_590=V_584 | Y_587=V_584 | Z_581=V_584 | X1_586=V_584 | X2_593=V_584 | ~member(U_157, X2_593, W_156) | ~member(U_157, X1_586, W_156) | ~member(U_157, Z_581, W_156) | ~member(U_157, Y_587, W_156) | ~member(U_157, X_590, W_156) | ~member(U_157, V_584, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.73 tff(c_819, plain, (![Y_555, X2_549, X2_561, X2_160, V_163, U_157, Y_557, Z_548, Z_551, X_559, V_558, X_560, V_553, X1_556, W_546, U_552, X_161, X1_547, Y_162, W_156, Z_158, X1_159]: (skf23(V_553, X_559, Y_557, Z_551, X1_556, X2_561, W_156, U_157)=skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157) | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=X_560 | skf23(V_553, X_559, Y_557, Z_551, X1_556, X2_561, W_156, U_157)=X_560 | X_560=W_546 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=W_546 | skf23(V_553, X_559, Y_557, Z_551, X1_556, X2_561, W_156, U_157)=W_546 | W_546=V_558 | X_560=V_558 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=V_558 | skf23(V_553, X_559, Y_557, Z_551, X1_556, X2_561, W_156, U_157)=V_558 | V_558=U_552 | W_546=U_552 | X_560=U_552 | skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157)=U_552 | skf23(V_553, X_559, Y_557, Z_551, X1_556, X2_561, W_156, U_157)=U_552 | ~member(U_157, X_560, W_156) | ~member(U_157, W_546, W_156) | ~member(U_157, V_558, W_156) | ~member(U_157, U_552, W_156) | skf23(U_552, V_558, W_546, X_560, Y_555, Z_548, X1_547, X2_549)!=X_560 | X2_561=X1_556 | Z_551=X1_556 | Z_551=X2_561 | Z_551=Y_557 | Y_557=X1_556 | Y_557=X2_561 | Y_557=X_559 | Z_551=X_559 | X_559=X1_556 | X_559=X2_561 | X_559=V_553 | Y_557=V_553 | Z_551=V_553 | X1_556=V_553 | X2_561=V_553 | ~member(U_157, X2_561, W_156) | ~member(U_157, X1_556, W_156) | ~member(U_157, Z_551, W_156) | ~member(U_157, Y_557, W_156) | ~member(U_157, X_559, W_156) | ~member(U_157, V_553, W_156) | X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.73 tff(c_756, plain, (![X2_169, Y_500, V_498, Z_502, Y_171, X_170, X1_168, W_501, U_505, V_172, U_166, W_164, X1_504, X2_503, X_499]: (skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=Y_171 | Y_171=X_170 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X_170 | X_170=W_164 | Y_171=W_164 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=W_164 | W_164=V_172 | X_170=V_172 | Y_171=V_172 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=V_172 | V_172=U_166 | W_164=U_166 | X_170=U_166 | Y_171=U_166 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=U_166 | ~member(U_505, Y_171, W_501) | ~member(U_505, X_170, W_501) | ~member(U_505, W_164, W_501) | ~member(U_505, V_172, W_501) | ~member(U_505, U_166, W_501) | skf23(U_166, V_172, W_164, X_170, Y_171, skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505), X1_168, X2_169)!=skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505) | X2_503=X1_504 | Z_502=X1_504 | Z_502=X2_503 | Z_502=Y_500 | Y_500=X1_504 | Y_500=X2_503 | Y_500=X_499 | Z_502=X_499 | X_499=X1_504 | X_499=X2_503 | X_499=V_498 | Y_500=V_498 | Z_502=V_498 | X1_504=V_498 | X2_503=V_498 | six(U_505, W_501) | ~member(U_505, X2_503, W_501) | ~member(U_505, X1_504, W_501) | ~member(U_505, Z_502, W_501) | ~member(U_505, Y_500, W_501) | ~member(U_505, X_499, W_501) | ~member(U_505, V_498, W_501)))). % 59.19/49.73 tff(c_753, plain, (![Y_500, V_498, X_206, W_199, X1_204, Z_202, Z_502, X5_197, V_208, X6_198, X2_205, W_501, U_505, Y_207, U_201, X1_504, X2_503, X_499]: (skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X6_198 | X6_198=X5_197 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X5_197 | X5_197=W_199 | X6_198=W_199 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=W_199 | W_199=V_208 | X5_197=V_208 | X6_198=V_208 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=V_208 | V_208=U_201 | W_199=U_201 | X5_197=U_201 | X6_198=U_201 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=U_201 | ~member(U_505, X6_198, W_501) | ~member(U_505, X5_197, W_501) | ~member(U_505, W_199, W_501) | ~member(U_505, V_208, W_501) | ~member(U_505, U_201, W_501) | skf23(U_201, V_208, W_199, X_206, Y_207, Z_202, X1_204, X2_205)!=W_199 | X2_503=X1_504 | Z_502=X1_504 | Z_502=X2_503 | Z_502=Y_500 | Y_500=X1_504 | Y_500=X2_503 | Y_500=X_499 | Z_502=X_499 | X_499=X1_504 | X_499=X2_503 | X_499=V_498 | Y_500=V_498 | Z_502=V_498 | X1_504=V_498 | X2_503=V_498 | six(U_505, W_501) | ~member(U_505, X2_503, W_501) | ~member(U_505, X1_504, W_501) | ~member(U_505, Z_502, W_501) | ~member(U_505, Y_500, W_501) | ~member(U_505, X_499, W_501) | ~member(U_505, V_498, W_501)))). % 59.19/49.73 tff(c_754, plain, (![Y_500, V_498, Z_502, X_181, Y_182, Z_178, X2_180, X1_179, W_501, U_505, V_183, X1_504, W_175, U_177, X2_503, X_499]: (skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=Y_182 | Y_182=X_181 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X_181 | X_181=W_175 | Y_182=W_175 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=W_175 | W_175=V_183 | X_181=V_183 | Y_182=V_183 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=V_183 | V_183=U_177 | W_175=U_177 | X_181=U_177 | Y_182=U_177 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=U_177 | ~member(U_505, Y_182, W_501) | ~member(U_505, X_181, W_501) | ~member(U_505, W_175, W_501) | ~member(U_505, V_183, W_501) | ~member(U_505, U_177, W_501) | skf23(U_177, V_183, W_175, X_181, Y_182, Z_178, X1_179, X2_180)!=Y_182 | X2_503=X1_504 | Z_502=X1_504 | Z_502=X2_503 | Z_502=Y_500 | Y_500=X1_504 | Y_500=X2_503 | Y_500=X_499 | Z_502=X_499 | X_499=X1_504 | X_499=X2_503 | X_499=V_498 | Y_500=V_498 | Z_502=V_498 | X1_504=V_498 | X2_503=V_498 | six(U_505, W_501) | ~member(U_505, X2_503, W_501) | ~member(U_505, X1_504, W_501) | ~member(U_505, Z_502, W_501) | ~member(U_505, Y_500, W_501) | ~member(U_505, X_499, W_501) | ~member(U_505, V_498, W_501)))). % 59.19/49.73 tff(c_755, plain, (![Y_500, V_498, Z_190, V_195, Z_502, W_501, U_505, U_189, W_187, X5_185, X1_191, X1_504, Y_194, X2_503, X_499, X_193, X2_192]: (skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X5_185 | X_193=X5_185 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X_193 | X_193=W_187 | X5_185=W_187 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=W_187 | W_187=V_195 | X_193=V_195 | X5_185=V_195 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=V_195 | V_195=U_189 | W_187=U_189 | X_193=U_189 | X5_185=U_189 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=U_189 | ~member(U_505, X5_185, W_501) | ~member(U_505, X_193, W_501) | ~member(U_505, W_187, W_501) | ~member(U_505, V_195, W_501) | ~member(U_505, U_189, W_501) | skf23(U_189, V_195, W_187, X_193, Y_194, Z_190, X1_191, X2_192)!=X_193 | X2_503=X1_504 | Z_502=X1_504 | Z_502=X2_503 | Z_502=Y_500 | Y_500=X1_504 | Y_500=X2_503 | Y_500=X_499 | Z_502=X_499 | X_499=X1_504 | X_499=X2_503 | X_499=V_498 | Y_500=V_498 | Z_502=V_498 | X1_504=V_498 | X2_503=V_498 | six(U_505, W_501) | ~member(U_505, X2_503, W_501) | ~member(U_505, X1_504, W_501) | ~member(U_505, Z_502, W_501) | ~member(U_505, Y_500, W_501) | ~member(U_505, X_499, W_501) | ~member(U_505, V_498, W_501)))). % 59.19/49.73 tff(c_752, plain, (![Y_500, V_498, Y_152, X7_148, W_143, Z_502, X_151, V_153, U_145, X5_141, W_501, U_505, X8_154, X1_149, X6_142, X1_504, X2_503, X_499, Z_147, X2_150]: (skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X8_154 | X8_154=X7_148 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X7_148 | X7_148=X6_142 | X8_154=X6_142 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X6_142 | X6_142=X5_141 | X7_148=X5_141 | X8_154=X5_141 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X5_141 | X5_141=U_145 | X6_142=U_145 | X7_148=U_145 | X8_154=U_145 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=U_145 | ~member(U_505, X8_154, W_501) | ~member(U_505, X7_148, W_501) | ~member(U_505, X6_142, W_501) | ~member(U_505, X5_141, W_501) | ~member(U_505, U_145, W_501) | skf23(U_145, V_153, W_143, X_151, Y_152, Z_147, X1_149, X2_150)!=U_145 | X2_503=X1_504 | Z_502=X1_504 | Z_502=X2_503 | Z_502=Y_500 | Y_500=X1_504 | Y_500=X2_503 | Y_500=X_499 | Z_502=X_499 | X_499=X1_504 | X_499=X2_503 | X_499=V_498 | Y_500=V_498 | Z_502=V_498 | X1_504=V_498 | X2_503=V_498 | six(U_505, W_501) | ~member(U_505, X2_503, W_501) | ~member(U_505, X1_504, W_501) | ~member(U_505, Z_502, W_501) | ~member(U_505, Y_500, W_501) | ~member(U_505, X_499, W_501) | ~member(U_505, V_498, W_501)))). % 59.19/49.73 tff(c_751, plain, (![Y_500, V_498, X2_135, Z_502, X7_133, X_136, X5_127, W_129, W_501, U_505, Z_132, V_138, X6_128, X1_504, X2_503, Y_137, X_499, X1_134, U_131]: (skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X7_133 | X7_133=X6_128 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X6_128 | X6_128=X5_127 | X7_133=X5_127 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=X5_127 | X5_127=V_138 | X6_128=V_138 | X7_133=V_138 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=V_138 | V_138=U_131 | X5_127=U_131 | X6_128=U_131 | X7_133=U_131 | skf23(V_498, X_499, Y_500, Z_502, X1_504, X2_503, W_501, U_505)=U_131 | ~member(U_505, X7_133, W_501) | ~member(U_505, X6_128, W_501) | ~member(U_505, X5_127, W_501) | ~member(U_505, V_138, W_501) | ~member(U_505, U_131, W_501) | skf23(U_131, V_138, W_129, X_136, Y_137, Z_132, X1_134, X2_135)!=V_138 | X2_503=X1_504 | Z_502=X1_504 | Z_502=X2_503 | Z_502=Y_500 | Y_500=X1_504 | Y_500=X2_503 | Y_500=X_499 | Z_502=X_499 | X_499=X1_504 | X_499=X2_503 | X_499=V_498 | Y_500=V_498 | Z_502=V_498 | X1_504=V_498 | X2_503=V_498 | six(U_505, W_501) | ~member(U_505, X2_503, W_501) | ~member(U_505, X1_504, W_501) | ~member(U_505, Z_502, W_501) | ~member(U_505, Y_500, W_501) | ~member(U_505, X_499, W_501) | ~member(U_505, V_498, W_501)))). % 59.19/49.73 tff(c_130, plain, (![X2_160, V_163, U_157, X_161, Y_162, W_156, Z_158, X1_159]: (X2_160=X1_159 | Z_158=X1_159 | Z_158=X2_160 | Z_158=Y_162 | Y_162=X1_159 | Y_162=X2_160 | Y_162=X_161 | Z_158=X_161 | X_161=X1_159 | X_161=X2_160 | X_161=V_163 | Y_162=V_163 | Z_158=V_163 | X1_159=V_163 | X2_160=V_163 | member(U_157, skf23(V_163, X_161, Y_162, Z_158, X1_159, X2_160, W_156, U_157), W_156) | six(U_157, W_156) | ~member(U_157, X2_160, W_156) | ~member(U_157, X1_159, W_156) | ~member(U_157, Z_158, W_156) | ~member(U_157, Y_162, W_156) | ~member(U_157, X_161, W_156) | ~member(U_157, V_163, W_156)))). % 59.19/49.73 tff(c_126, plain, (![X2_135, X7_133, X8_139, X_136, X5_127, W_129, X4_140, X3_130, Z_132, V_138, X6_128, Y_137, X1_134, U_131]: (X8_139=X7_133 | X7_133=X6_128 | X8_139=X6_128 | X6_128=X5_127 | X7_133=X5_127 | X8_139=X5_127 | X5_127=V_138 | X6_128=V_138 | X7_133=V_138 | X8_139=V_138 | V_138=U_131 | X5_127=U_131 | X6_128=U_131 | X7_133=U_131 | X8_139=U_131 | six(X3_130, X4_140) | ~member(X3_130, X8_139, X4_140) | ~member(X3_130, X7_133, X4_140) | ~member(X3_130, X6_128, X4_140) | ~member(X3_130, X5_127, X4_140) | ~member(X3_130, V_138, X4_140) | ~member(X3_130, U_131, X4_140) | skf23(U_131, V_138, W_129, X_136, Y_137, Z_132, X1_134, X2_135)!=V_138))). % 59.19/49.73 tff(c_128, plain, (![X4_155, Y_152, X7_148, W_143, X_151, V_153, U_145, X5_141, X8_154, X9_146, X1_149, X6_142, X3_144, Z_147, X2_150]: (X9_146=X8_154 | X8_154=X7_148 | X9_146=X7_148 | X7_148=X6_142 | X8_154=X6_142 | X9_146=X6_142 | X6_142=X5_141 | X7_148=X5_141 | X8_154=X5_141 | X9_146=X5_141 | X5_141=U_145 | X6_142=U_145 | X7_148=U_145 | X8_154=U_145 | X9_146=U_145 | six(X3_144, X4_155) | ~member(X3_144, X9_146, X4_155) | ~member(X3_144, X8_154, X4_155) | ~member(X3_144, X7_148, X4_155) | ~member(X3_144, X6_142, X4_155) | ~member(X3_144, X5_141, X4_155) | ~member(X3_144, U_145, X4_155) | skf23(U_145, V_153, W_143, X_151, Y_152, Z_147, X1_149, X2_150)!=U_145))). % 59.19/49.73 tff(c_138, plain, (![X_206, W_199, X1_204, Z_202, X5_197, V_208, X6_198, X2_205, X7_203, X4_209, Y_207, U_201, X3_200]: (X7_203=X6_198 | X6_198=X5_197 | X7_203=X5_197 | X5_197=W_199 | X6_198=W_199 | X7_203=W_199 | W_199=V_208 | X5_197=V_208 | X6_198=V_208 | X7_203=V_208 | V_208=U_201 | W_199=U_201 | X5_197=U_201 | X6_198=U_201 | X7_203=U_201 | six(X3_200, X4_209) | ~member(X3_200, X7_203, X4_209) | ~member(X3_200, X6_198, X4_209) | ~member(X3_200, X5_197, X4_209) | ~member(X3_200, W_199, X4_209) | ~member(X3_200, V_208, X4_209) | ~member(X3_200, U_201, X4_209) | skf23(U_201, V_208, W_199, X_206, Y_207, Z_202, X1_204, X2_205)!=W_199))). % 59.19/49.73 tff(c_134, plain, (![X3_176, X4_184, X_181, Y_182, Z_178, X2_180, X1_179, X5_174, V_183, W_175, U_177]: (Y_182=X5_174 | Y_182=X_181 | X_181=X5_174 | X_181=W_175 | Y_182=W_175 | X5_174=W_175 | W_175=V_183 | X_181=V_183 | Y_182=V_183 | X5_174=V_183 | V_183=U_177 | W_175=U_177 | X_181=U_177 | Y_182=U_177 | X5_174=U_177 | six(X3_176, X4_184) | ~member(X3_176, X5_174, X4_184) | ~member(X3_176, Y_182, X4_184) | ~member(X3_176, X_181, X4_184) | ~member(X3_176, W_175, X4_184) | ~member(X3_176, V_183, X4_184) | ~member(X3_176, U_177, X4_184) | skf23(U_177, V_183, W_175, X_181, Y_182, Z_178, X1_179, X2_180)!=Y_182))). % 59.19/49.73 tff(c_136, plain, (![Z_190, V_195, X4_196, X3_188, U_189, W_187, X5_185, X1_191, X6_186, Y_194, X_193, X2_192]: (X6_186=X5_185 | X_193=X5_185 | X_193=X6_186 | X_193=W_187 | X5_185=W_187 | X6_186=W_187 | W_187=V_195 | X_193=V_195 | X5_185=V_195 | X6_186=V_195 | V_195=U_189 | W_187=U_189 | X_193=U_189 | X5_185=U_189 | X6_186=U_189 | six(X3_188, X4_196) | ~member(X3_188, X6_186, X4_196) | ~member(X3_188, X5_185, X4_196) | ~member(X3_188, X_193, X4_196) | ~member(X3_188, W_187, X4_196) | ~member(X3_188, V_195, X4_196) | ~member(X3_188, U_189, X4_196) | skf23(U_189, V_195, W_187, X_193, Y_194, Z_190, X1_191, X2_192)!=X_193))). % 59.19/49.73 tff(c_132, plain, (![X3_165, X2_169, X4_173, Z_167, Y_171, X_170, X1_168, V_172, U_166, W_164]: (Z_167=Y_171 | Y_171=X_170 | Z_167=X_170 | X_170=W_164 | Y_171=W_164 | Z_167=W_164 | W_164=V_172 | X_170=V_172 | Y_171=V_172 | Z_167=V_172 | V_172=U_166 | W_164=U_166 | X_170=U_166 | Y_171=U_166 | Z_167=U_166 | six(X3_165, X4_173) | ~member(X3_165, Z_167, X4_173) | ~member(X3_165, Y_171, X4_173) | ~member(X3_165, X_170, X4_173) | ~member(X3_165, W_164, X4_173) | ~member(X3_165, V_172, X4_173) | ~member(X3_165, U_166, X4_173) | skf23(U_166, V_172, W_164, X_170, Y_171, Z_167, X1_168, X2_169)!=Z_167))). % 59.19/49.73 tff(c_124, plain, (![W_126, U_124, V_125]: (skf22(W_126, U_124)=V_125 | skf20(W_126, U_124)=V_125 | skf18(W_126, U_124)=V_125 | skf16(W_126, U_124)=V_125 | skf14(W_126, U_124)=V_125 | skf12(W_126, U_124)=V_125 | ~six(U_124, W_126) | ~member(U_124, V_125, W_126)))). % 59.19/49.73 tff(c_584, plain, (![V_216]: (~of(skc3, V_216, skc5) | ~cannon(skc3, V_216)))). % 59.19/49.73 tff(c_122, plain, (![U_121, V_122, W_123]: (~agent(U_121, V_122, W_123) | ~patient(U_121, V_122, W_123) | ~nonreflexive(U_121, V_122)))). % 59.19/49.73 tff(c_551, plain, (skf22(skc4, skc3)!=skf16(skc4, skc3))). % 59.19/49.73 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf22(U_95, V_96)!=skf16(U_95, V_96)))). % 59.19/49.73 tff(c_546, plain, (skf16(skc4, skc3)!=skf14(skc4, skc3))). % 59.19/49.73 tff(c_541, plain, (skf18(skc4, skc3)!=skf16(skc4, skc3))). % 59.19/49.73 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf16(U_117, V_118)!=skf14(U_117, V_118)))). % 59.19/49.73 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf18(U_113, V_114)!=skf16(U_113, V_114)))). % 59.19/49.73 tff(c_536, plain, (skf22(skc4, skc3)!=skf12(skc4, skc3))). % 59.19/49.73 tff(c_531, plain, (skf22(skc4, skc3)!=skf18(skc4, skc3))). % 59.19/49.73 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf22(U_91, V_92)!=skf12(U_91, V_92)))). % 59.19/49.73 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf22(U_97, V_98)!=skf18(U_97, V_98)))). % 59.19/49.73 tff(c_510, plain, (skf20(skc4, skc3)!=skf12(skc4, skc3))). % 59.19/49.73 tff(c_526, plain, (act(skc3, skf12(skc4, skc3)))). % 59.19/49.73 tff(c_522, plain, (action(skc3, skf12(skc4, skc3)))). % 59.19/49.73 tff(c_518, plain, (shot(skc3, skf12(skc4, skc3)))). % 59.19/49.73 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf12(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 59.19/49.73 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf20(U_101, V_102)!=skf12(U_101, V_102)))). % 59.19/49.73 tff(c_499, plain, (![U_37, V_38]: (~act(U_37, V_38) | ~artifact(U_37, V_38)))). % 59.19/49.73 tff(c_504, plain, (skf22(skc4, skc3)!=skf14(skc4, skc3))). % 59.19/49.73 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf22(U_93, V_94)!=skf14(U_93, V_94)))). % 59.19/49.73 tff(c_494, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 59.19/49.73 tff(c_402, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 59.19/49.73 tff(c_485, plain, (skf20(skc4, skc3)!=skf14(skc4, skc3))). % 59.19/49.73 tff(c_489, plain, (~act(skc3, skc4))). % 59.19/49.73 tff(c_480, plain, (~event(skc3, skc4))). % 59.19/49.73 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf20(U_103, V_104)!=skf14(U_103, V_104)))). % 59.19/49.73 tff(c_476, plain, (~eventuality(skc3, skc4))). % 59.19/49.74 tff(c_412, plain, (![U_266, V_267]: (~eventuality(U_266, V_267) | ~group(U_266, V_267)))). % 59.19/49.74 tff(c_471, plain, (skf20(skc4, skc3)!=skf18(skc4, skc3))). % 59.19/49.74 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf20(U_107, V_108)!=skf18(U_107, V_108)))). % 59.19/49.74 tff(c_397, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 59.19/49.74 tff(c_417, plain, (![U_371, V_372]: (artifact(U_371, V_372) | ~cannon(U_371, V_372)))). % 59.19/49.74 tff(c_464, plain, (act(skc3, skf16(skc4, skc3)))). % 59.19/49.74 tff(c_460, plain, (action(skc3, skf16(skc4, skc3)))). % 59.19/49.74 tff(c_456, plain, (shot(skc3, skf16(skc4, skc3)))). % 59.19/49.74 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf16(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 59.19/49.74 tff(c_444, plain, (skf16(skc4, skc3)!=skf12(skc4, skc3))). % 59.19/49.74 tff(c_448, plain, (~artifact(skc3, skc4))). % 59.19/49.74 tff(c_439, plain, (~entity(skc3, skc4))). % 59.19/49.74 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf16(U_115, V_116)!=skf12(U_115, V_116)))). % 59.19/49.74 tff(c_366, plain, (![U_266, V_267]: (~entity(U_266, V_267) | ~group(U_266, V_267)))). % 59.19/49.74 tff(c_355, plain, (![U_349, V_350]: (~animate(U_349, V_350) | ~artifact(U_349, V_350)))). % 59.19/49.74 tff(c_433, plain, (act(skc3, skf18(skc4, skc3)))). % 59.19/49.74 tff(c_429, plain, (action(skc3, skf18(skc4, skc3)))). % 59.19/49.74 tff(c_425, plain, (shot(skc3, skf18(skc4, skc3)))). % 59.19/49.74 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf18(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 59.19/49.74 tff(c_360, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 59.19/49.74 tff(c_268, plain, (![U_323, V_324]: (~multiple(U_323, V_324) | ~eventuality(U_323, V_324)))). % 59.19/49.74 tff(c_407, plain, (skf14(skc4, skc3)!=skf12(skc4, skc3))). % 59.19/49.74 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf14(U_119, V_120)!=skf12(U_119, V_120)))). % 59.19/49.74 tff(c_330, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 59.19/49.74 tff(c_354, plain, (![U_349, V_350]: (~living(U_349, V_350) | ~artifact(U_349, V_350)))). % 59.19/49.74 tff(c_392, plain, (act(skc3, skf22(skc4, skc3)))). % 59.19/49.74 tff(c_388, plain, (action(skc3, skf22(skc4, skc3)))). % 59.19/49.74 tff(c_384, plain, (shot(skc3, skf22(skc4, skc3)))). % 59.19/49.74 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf22(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 59.19/49.74 tff(c_376, plain, (~artifact(skc3, skc5))). % 59.19/49.74 tff(c_274, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 59.19/49.74 tff(c_371, plain, (skf22(skc4, skc3)!=skf20(skc4, skc3))). % 59.19/49.74 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf22(U_99, V_100)!=skf20(U_99, V_100)))). % 59.19/49.74 tff(c_341, plain, (![U_345, V_346]: (~multiple(U_345, V_346) | ~entity(U_345, V_346)))). % 59.19/49.74 tff(c_346, plain, (skf20(skc4, skc3)!=skf16(skc4, skc3))). % 59.19/49.74 tff(c_185, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~artifact(U_37, V_38)))). % 59.19/49.74 tff(c_179, plain, (![U_260, V_261]: (instrumentality(U_260, V_261) | ~weapon(U_260, V_261)))). % 59.19/49.74 tff(c_214, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 59.19/49.74 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf20(U_105, V_106)!=skf16(U_105, V_106)))). % 59.19/49.74 tff(c_279, plain, (skf18(skc4, skc3)!=skf12(skc4, skc3))). % 59.19/49.74 tff(c_336, plain, (skf18(skc4, skc3)!=skf14(skc4, skc3))). % 59.19/49.74 tff(c_208, plain, (![U_276, V_277]: (singleton(U_276, V_277) | ~entity(U_276, V_277)))). % 59.19/49.74 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf18(U_111, V_112)!=skf14(U_111, V_112)))). % 59.19/49.74 tff(c_224, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 59.19/49.74 tff(c_229, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 59.19/49.74 tff(c_325, plain, (act(skc3, skf14(skc4, skc3)))). % 59.19/49.74 tff(c_321, plain, (action(skc3, skf14(skc4, skc3)))). % 59.19/49.74 tff(c_317, plain, (shot(skc3, skf14(skc4, skc3)))). % 59.19/49.74 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf14(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 59.19/49.74 tff(c_309, plain, (act(skc3, skf20(skc4, skc3)))). % 59.19/49.74 tff(c_305, plain, (action(skc3, skf20(skc4, skc3)))). % 59.19/49.74 tff(c_301, plain, (shot(skc3, skf20(skc4, skc3)))). % 59.19/49.74 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf20(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 59.19/49.74 tff(c_190, plain, (![U_266, V_267]: (multiple(U_266, V_267) | ~group(U_266, V_267)))). % 59.19/49.74 tff(c_292, plain, (~act(skc3, skc5))). % 59.19/49.74 tff(c_288, plain, (~event(skc3, skc5))). % 59.19/49.74 tff(c_284, plain, (~eventuality(skc3, skc5))). % 59.19/49.74 tff(c_240, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 59.19/49.74 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf18(U_109, V_110)!=skf12(U_109, V_110)))). % 59.19/49.74 tff(c_239, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~object(U_51, V_52)))). % 59.19/49.74 tff(c_257, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 59.19/49.74 tff(c_203, plain, (![U_274, V_275]: (singleton(U_274, V_275) | ~eventuality(U_274, V_275)))). % 59.19/49.74 tff(c_148, plain, (![U_210]: (shot(skc3, U_210) | ~member(skc3, U_210, skc4)))). % 59.19/49.74 tff(c_252, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 59.19/49.74 tff(c_246, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 59.19/49.74 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 59.19/49.74 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 59.19/49.74 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 59.19/49.74 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 59.19/49.74 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 59.19/49.74 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 59.19/49.74 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 59.19/49.74 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 59.19/49.74 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 59.19/49.74 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 59.19/49.74 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 59.19/49.74 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 59.19/49.74 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 59.19/49.74 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 59.19/49.74 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 59.19/49.74 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 59.19/49.74 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 59.19/49.74 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 59.19/49.74 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 59.19/49.74 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 59.19/49.75 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 59.19/49.75 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 59.19/49.75 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 59.19/49.75 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 59.19/49.75 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 59.19/49.75 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 59.19/49.75 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 59.19/49.75 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 59.19/49.75 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 59.19/49.75 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 59.19/49.75 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 59.19/49.75 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 59.19/49.75 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 59.19/49.75 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 59.19/49.75 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 59.19/49.75 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 59.19/49.75 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 59.19/49.75 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 59.19/49.75 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 59.19/49.75 tff(c_142, plain, (male(skc3, skc5))). % 59.19/49.75 tff(c_146, plain, (six(skc3, skc4))). % 59.19/49.75 tff(c_144, plain, (group(skc3, skc4))). % 59.19/49.75 tff(c_140, plain, (actual_world(skc3))). % 59.19/49.75 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 59.19/49.75 %------------------------------------------------------------------------------