%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : NLP078-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 : n016.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:08 PM UTC 2025 % Result : Satisfiable 63.13s 54.18s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.12 % Problem : NLP078-1 : TPTP v9.0.0. Released v2.4.0. % 0.02/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.34 % Computer : n016.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Tue Apr 8 08:24:23 EDT 2025 % 0.12/0.34 % CPUTime : % 63.13/54.18 % 63.13/54.18 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 63.13/54.18 % 63.13/54.18 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 63.13/54.19 %$ 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 > skf22 > skf20 > skf18 > skf16 > skf14 > skf12 > #nlpp > skf9 > skf10 > skc3 > skc2 % 63.13/54.19 % 63.13/54.19 %Foreground sorts: % 63.13/54.19 % 63.13/54.19 % 63.13/54.19 %Background operators: % 63.13/54.19 % 63.13/54.19 % 63.13/54.19 %Foreground operators: % 63.13/54.19 tff(nonliving, type, nonliving: ($i * $i) > $o). % 63.13/54.19 tff(member, type, member: ($i * $i * $i) > $o). % 63.13/54.19 tff(living, type, living: ($i * $i) > $o). % 63.13/54.19 tff(fire, type, fire: ($i * $i) > $o). % 63.13/54.19 tff(human_person, type, human_person: ($i * $i) > $o). % 63.13/54.19 tff(action, type, action: ($i * $i) > $o). % 63.13/54.19 tff(present, type, present: ($i * $i) > $o). % 63.13/54.19 tff(shot, type, shot: ($i * $i) > $o). % 63.13/54.19 tff(skf22, type, skf22: ($i * $i) > $i). % 63.13/54.19 tff(entity, type, entity: ($i * $i) > $o). % 63.13/54.19 tff(eventuality, type, eventuality: ($i * $i) > $o). % 63.13/54.19 tff(weapon, type, weapon: ($i * $i) > $o). % 63.13/54.19 tff(existent, type, existent: ($i * $i) > $o). % 63.13/54.19 tff(singleton, type, singleton: ($i * $i) > $o). % 63.13/54.19 tff(male, type, male: ($i * $i) > $o). % 63.13/54.19 tff(multiple, type, multiple: ($i * $i) > $o). % 63.13/54.19 tff(organism, type, organism: ($i * $i) > $o). % 63.13/54.19 tff(animate, type, animate: ($i * $i) > $o). % 63.13/54.19 tff(of, type, of: ($i * $i * $i) > $o). % 63.13/54.19 tff(skf14, type, skf14: ($i * $i) > $i). % 63.13/54.19 tff(actual_world, type, actual_world: $i > $o). % 63.13/54.19 tff(agent, type, agent: ($i * $i * $i) > $o). % 63.13/54.19 tff(skf10, type, skf10: $i > $i). % 63.13/54.19 tff(instrumentality, type, instrumentality: ($i * $i) > $o). % 63.13/54.19 tff(group, type, group: ($i * $i) > $o). % 63.13/54.19 tff(artifact, type, artifact: ($i * $i) > $o). % 63.13/54.19 tff(cannon, type, cannon: ($i * $i) > $o). % 63.13/54.19 tff(event, type, event: ($i * $i) > $o). % 63.13/54.19 tff(skc2, type, skc2: $i). % 63.13/54.19 tff(from_loc, type, from_loc: ($i * $i * $i) > $o). % 63.13/54.19 tff(patient, type, patient: ($i * $i * $i) > $o). % 63.13/54.19 tff(nonexistent, type, nonexistent: ($i * $i) > $o). % 63.13/54.19 tff(skc3, type, skc3: $i). % 63.13/54.19 tff(thing, type, thing: ($i * $i) > $o). % 63.13/54.19 tff(skf9, type, skf9: $i > $i). % 63.13/54.19 tff(human, type, human: ($i * $i) > $o). % 63.13/54.19 tff(six, type, six: ($i * $i) > $o). % 63.13/54.19 tff(skf18, type, skf18: ($i * $i) > $i). % 63.13/54.19 tff(man, type, man: ($i * $i) > $o). % 63.13/54.19 tff(weaponry, type, weaponry: ($i * $i) > $o). % 63.13/54.19 tff(unisex, type, unisex: ($i * $i) > $o). % 63.13/54.19 tff(skf16, type, skf16: ($i * $i) > $i). % 63.13/54.19 tff(set, type, set: ($i * $i) > $o). % 63.13/54.19 tff(skf12, type, skf12: ($i * $i) > $i). % 63.13/54.19 tff(impartial, type, impartial: ($i * $i) > $o). % 63.13/54.19 tff(skf23, type, skf23: ($i * $i * $i * $i * $i * $i * $i * $i) > $i). % 63.13/54.19 tff(object, type, object: ($i * $i) > $o). % 63.13/54.19 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o). % 63.13/54.19 tff(specific, type, specific: ($i * $i) > $o). % 63.13/54.19 tff(skf20, type, skf20: ($i * $i) > $i). % 63.13/54.19 tff(act, type, act: ($i * $i) > $o). % 63.13/54.19 % 63.13/54.19 %Saturated clause set: % 63.13/54.20 tff(c_1048, plain, (![Z_183, V_935, Y_932, W_931, X1_937, X2_933, X1_964, X2_955, X1_960, V_949, X2_950, V_945, X1_959, Z_936, V_963, X2_185, X_951, Y_958, X_962, X1_956, X2_929, Z_954, Y_947, Y_944, W_181, X2_957, V_927, Z_934, V_965, X1_961, X1_184, Y_948, Y_187, X_930, X_943, X_186, Z_926, Z_952, V_188, U_182, X2_940, X_939, Z_946, Y_942, X_941]: (skf23(V_945, X_941, Y_947, Z_954, X1_964, X2_957, W_181, U_182)=skf23(V_927, X_951, Y_944, Z_934, X1_956, X2_950, W_181, U_182) | skf23(V_949, X_930, Y_932, Z_946, X1_959, X2_929, W_181, U_182)=skf23(V_945, X_941, Y_947, Z_954, X1_964, X2_957, W_181, U_182) | skf23(V_949, X_930, Y_932, Z_946, X1_959, X2_929, W_181, U_182)=skf23(V_927, X_951, Y_944, Z_934, X1_956, X2_950, W_181, U_182) | skf23(V_949, X_930, Y_932, Z_946, X1_959, X2_929, W_181, U_182)=skf23(V_935, X_943, Y_948, Z_936, X1_961, X2_955, W_181, U_182) | skf23(V_945, X_941, Y_947, Z_954, X1_964, X2_957, W_181, U_182)=skf23(V_935, X_943, Y_948, Z_936, X1_961, X2_955, W_181, U_182) | skf23(V_935, X_943, Y_948, Z_936, X1_961, X2_955, W_181, U_182)=skf23(V_927, X_951, Y_944, Z_934, X1_956, X2_950, W_181, U_182) | skf23(V_965, X_962, Y_942, Z_952, X1_960, X2_933, W_181, U_182)=skf23(V_935, X_943, Y_948, Z_936, X1_961, X2_955, W_181, U_182) | skf23(V_965, X_962, Y_942, Z_952, X1_960, X2_933, W_181, U_182)=skf23(V_949, X_930, Y_932, Z_946, X1_959, X2_929, W_181, U_182) | skf23(V_965, X_962, Y_942, Z_952, X1_960, X2_933, W_181, U_182)=skf23(V_945, X_941, Y_947, Z_954, X1_964, X2_957, W_181, U_182) | skf23(V_965, X_962, Y_942, Z_952, X1_960, X2_933, W_181, U_182)=skf23(V_927, X_951, Y_944, Z_934, X1_956, X2_950, W_181, U_182) | skf23(V_965, X_962, Y_942, Z_952, X1_960, X2_933, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_935, X_943, Y_948, Z_936, X1_961, X2_955, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_949, X_930, Y_932, Z_946, X1_959, X2_929, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_945, X_941, Y_947, Z_954, X1_964, X2_957, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_927, X_951, Y_944, Z_934, X1_956, X2_950, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), V_963, W_931, X_939, Y_958, Z_926, X1_937, X2_940)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_950=X1_956 | Z_934=X1_956 | Z_934=X2_950 | Z_934=Y_944 | Y_944=X1_956 | Y_944=X2_950 | Y_944=X_951 | Z_934=X_951 | X_951=X1_956 | X_951=X2_950 | X_951=V_927 | Y_944=V_927 | Z_934=V_927 | X1_956=V_927 | X2_950=V_927 | ~member(U_182, X2_950, W_181) | ~member(U_182, X1_956, W_181) | ~member(U_182, Z_934, W_181) | ~member(U_182, Y_944, W_181) | ~member(U_182, X_951, W_181) | ~member(U_182, V_927, W_181) | X2_957=X1_964 | Z_954=X1_964 | Z_954=X2_957 | Z_954=Y_947 | Y_947=X1_964 | Y_947=X2_957 | Y_947=X_941 | Z_954=X_941 | X_941=X1_964 | X_941=X2_957 | X_941=V_945 | Y_947=V_945 | Z_954=V_945 | X1_964=V_945 | X2_957=V_945 | ~member(U_182, X2_957, W_181) | ~member(U_182, X1_964, W_181) | ~member(U_182, Z_954, W_181) | ~member(U_182, Y_947, W_181) | ~member(U_182, X_941, W_181) | ~member(U_182, V_945, W_181) | X2_929=X1_959 | Z_946=X1_959 | Z_946=X2_929 | Z_946=Y_932 | Y_932=X1_959 | Y_932=X2_929 | Y_932=X_930 | Z_946=X_930 | X_930=X1_959 | X_930=X2_929 | X_930=V_949 | Y_932=V_949 | Z_946=V_949 | X1_959=V_949 | X2_929=V_949 | ~member(U_182, X2_929, W_181) | ~member(U_182, X1_959, W_181) | ~member(U_182, Z_946, W_181) | ~member(U_182, Y_932, W_181) | ~member(U_182, X_930, W_181) | ~member(U_182, V_949, W_181) | X2_955=X1_961 | Z_936=X1_961 | Z_936=X2_955 | Z_936=Y_948 | Y_948=X1_961 | Y_948=X2_955 | Y_948=X_943 | Z_936=X_943 | X_943=X1_961 | X_943=X2_955 | X_943=V_935 | Y_948=V_935 | Z_936=V_935 | X1_961=V_935 | X2_955=V_935 | ~member(U_182, X2_955, W_181) | ~member(U_182, X1_961, W_181) | ~member(U_182, Z_936, W_181) | ~member(U_182, Y_948, W_181) | ~member(U_182, X_943, W_181) | ~member(U_182, V_935, W_181) | X2_933=X1_960 | Z_952=X1_960 | Z_952=X2_933 | Z_952=Y_942 | Y_942=X1_960 | Y_942=X2_933 | Y_942=X_962 | Z_952=X_962 | X_962=X1_960 | X_962=X2_933 | X_962=V_965 | Y_942=V_965 | Z_952=V_965 | X1_960=V_965 | X2_933=V_965 | ~member(U_182, X2_933, W_181) | ~member(U_182, X1_960, W_181) | ~member(U_182, Z_952, W_181) | ~member(U_182, Y_942, W_181) | ~member(U_182, X_962, W_181) | ~member(U_182, V_965, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.20 tff(c_1003, plain, (![Z_183, X1_854, X2_825, X_836, Z_843, Z_851, X2_185, Y_839, X_833, Z_827, X1_848, X2_826, Y_832, X1_844, X_842, X_850, X_845, Y_840, U_838, X2_830, W_835, V_857, V_856, W_181, X1_849, X2_841, Z_834, X1_184, Y_187, Z_829, V_847, X_186, Y_837, X2_846, V_188, U_182, V_855, X1_852, Y_853]: (skf23(V_855, X_842, Y_840, Z_851, X1_848, X2_841, W_181, U_182)=skf23(V_847, X_833, Y_853, Z_827, X1_852, X2_825, W_181, U_182) | skf23(V_856, X_845, Y_839, Z_834, X1_844, X2_830, W_181, U_182)=skf23(V_847, X_833, Y_853, Z_827, X1_852, X2_825, W_181, U_182) | skf23(V_856, X_845, Y_839, Z_834, X1_844, X2_830, W_181, U_182)=skf23(V_855, X_842, Y_840, Z_851, X1_848, X2_841, W_181, U_182) | skf23(V_857, X_850, Y_832, Z_843, X1_849, X2_826, W_181, U_182)=skf23(V_856, X_845, Y_839, Z_834, X1_844, X2_830, W_181, U_182) | skf23(V_857, X_850, Y_832, Z_843, X1_849, X2_826, W_181, U_182)=skf23(V_847, X_833, Y_853, Z_827, X1_852, X2_825, W_181, U_182) | skf23(V_857, X_850, Y_832, Z_843, X1_849, X2_826, W_181, U_182)=skf23(V_855, X_842, Y_840, Z_851, X1_848, X2_841, W_181, U_182) | skf23(V_857, X_850, Y_832, Z_843, X1_849, X2_826, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_856, X_845, Y_839, Z_834, X1_844, X2_830, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_847, X_833, Y_853, Z_827, X1_852, X2_825, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_855, X_842, Y_840, Z_851, X1_848, X2_841, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_838 | skf23(V_857, X_850, Y_832, Z_843, X1_849, X2_826, W_181, U_182)=U_838 | skf23(V_856, X_845, Y_839, Z_834, X1_844, X2_830, W_181, U_182)=U_838 | skf23(V_847, X_833, Y_853, Z_827, X1_852, X2_825, W_181, U_182)=U_838 | skf23(V_855, X_842, Y_840, Z_851, X1_848, X2_841, W_181, U_182)=U_838 | ~member(U_182, U_838, W_181) | skf23(U_838, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), W_835, X_836, Y_837, Z_829, X1_854, X2_846)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_841=X1_848 | Z_851=X1_848 | Z_851=X2_841 | Z_851=Y_840 | Y_840=X1_848 | Y_840=X2_841 | Y_840=X_842 | Z_851=X_842 | X_842=X1_848 | X_842=X2_841 | X_842=V_855 | Y_840=V_855 | Z_851=V_855 | X1_848=V_855 | X2_841=V_855 | ~member(U_182, X2_841, W_181) | ~member(U_182, X1_848, W_181) | ~member(U_182, Z_851, W_181) | ~member(U_182, Y_840, W_181) | ~member(U_182, X_842, W_181) | ~member(U_182, V_855, W_181) | X2_825=X1_852 | Z_827=X1_852 | Z_827=X2_825 | Z_827=Y_853 | Y_853=X1_852 | Y_853=X2_825 | Y_853=X_833 | Z_827=X_833 | X_833=X1_852 | X_833=X2_825 | X_833=V_847 | Y_853=V_847 | Z_827=V_847 | X1_852=V_847 | X2_825=V_847 | ~member(U_182, X2_825, W_181) | ~member(U_182, X1_852, W_181) | ~member(U_182, Z_827, W_181) | ~member(U_182, Y_853, W_181) | ~member(U_182, X_833, W_181) | ~member(U_182, V_847, W_181) | X2_830=X1_844 | Z_834=X1_844 | Z_834=X2_830 | Z_834=Y_839 | Y_839=X1_844 | Y_839=X2_830 | Y_839=X_845 | Z_834=X_845 | X_845=X1_844 | X_845=X2_830 | X_845=V_856 | Y_839=V_856 | Z_834=V_856 | X1_844=V_856 | X2_830=V_856 | ~member(U_182, X2_830, W_181) | ~member(U_182, X1_844, W_181) | ~member(U_182, Z_834, W_181) | ~member(U_182, Y_839, W_181) | ~member(U_182, X_845, W_181) | ~member(U_182, V_856, W_181) | X2_826=X1_849 | Z_843=X1_849 | Z_843=X2_826 | Z_843=Y_832 | Y_832=X1_849 | Y_832=X2_826 | Y_832=X_850 | Z_843=X_850 | X_850=X1_849 | X_850=X2_826 | X_850=V_857 | Y_832=V_857 | Z_843=V_857 | X1_849=V_857 | X2_826=V_857 | ~member(U_182, X2_826, W_181) | ~member(U_182, X1_849, W_181) | ~member(U_182, Z_843, W_181) | ~member(U_182, Y_832, W_181) | ~member(U_182, X_850, W_181) | ~member(U_182, V_857, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.20 tff(c_1025, plain, (![X2_882, X1_863, Z_183, Z_880, X_884, X_888, X2_887, X2_185, X_878, W_891, X1_860, Z_875, V_864, W_181, V_890, U_866, Y_876, V_867, V_885, X1_877, Y_870, X1_184, Z_889, Y_868, X2_862, Y_187, Z_858, X2_883, X_186, X1_873, Z_872, V_188, U_182, X_874, X_881, Y_871, V_892, X1_886, X2_879, Y_865]: (skf23(V_885, X_884, Y_868, Z_889, X1_873, X2_887, W_181, U_182)=skf23(V_864, X_878, Y_865, Z_858, X1_877, X2_882, W_181, U_182) | skf23(V_867, X_881, Y_871, Z_872, X1_860, X2_879, W_181, U_182)=skf23(V_864, X_878, Y_865, Z_858, X1_877, X2_882, W_181, U_182) | skf23(V_885, X_884, Y_868, Z_889, X1_873, X2_887, W_181, U_182)=skf23(V_867, X_881, Y_871, Z_872, X1_860, X2_879, W_181, U_182) | skf23(V_892, X_888, Y_870, Z_880, X1_886, X2_862, W_181, U_182)=skf23(V_867, X_881, Y_871, Z_872, X1_860, X2_879, W_181, U_182) | skf23(V_892, X_888, Y_870, Z_880, X1_886, X2_862, W_181, U_182)=skf23(V_864, X_878, Y_865, Z_858, X1_877, X2_882, W_181, U_182) | skf23(V_892, X_888, Y_870, Z_880, X1_886, X2_862, W_181, U_182)=skf23(V_885, X_884, Y_868, Z_889, X1_873, X2_887, W_181, U_182) | skf23(V_892, X_888, Y_870, Z_880, X1_886, X2_862, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_867, X_881, Y_871, Z_872, X1_860, X2_879, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_864, X_878, Y_865, Z_858, X1_877, X2_882, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_885, X_884, Y_868, Z_889, X1_873, X2_887, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_866 | skf23(V_892, X_888, Y_870, Z_880, X1_886, X2_862, W_181, U_182)=U_866 | skf23(V_867, X_881, Y_871, Z_872, X1_860, X2_879, W_181, U_182)=U_866 | skf23(V_864, X_878, Y_865, Z_858, X1_877, X2_882, W_181, U_182)=U_866 | skf23(V_885, X_884, Y_868, Z_889, X1_873, X2_887, W_181, U_182)=U_866 | ~member(U_182, U_866, W_181) | skf23(U_866, V_890, W_891, X_874, Y_876, Z_875, X1_863, X2_883)!=U_866 | X2_887=X1_873 | Z_889=X1_873 | Z_889=X2_887 | Z_889=Y_868 | Y_868=X1_873 | Y_868=X2_887 | Y_868=X_884 | Z_889=X_884 | X_884=X1_873 | X_884=X2_887 | X_884=V_885 | Y_868=V_885 | Z_889=V_885 | X1_873=V_885 | X2_887=V_885 | ~member(U_182, X2_887, W_181) | ~member(U_182, X1_873, W_181) | ~member(U_182, Z_889, W_181) | ~member(U_182, Y_868, W_181) | ~member(U_182, X_884, W_181) | ~member(U_182, V_885, W_181) | X2_882=X1_877 | Z_858=X1_877 | Z_858=X2_882 | Z_858=Y_865 | Y_865=X1_877 | Y_865=X2_882 | Y_865=X_878 | Z_858=X_878 | X_878=X1_877 | X_878=X2_882 | X_878=V_864 | Y_865=V_864 | Z_858=V_864 | X1_877=V_864 | X2_882=V_864 | ~member(U_182, X2_882, W_181) | ~member(U_182, X1_877, W_181) | ~member(U_182, Z_858, W_181) | ~member(U_182, Y_865, W_181) | ~member(U_182, X_878, W_181) | ~member(U_182, V_864, W_181) | X2_879=X1_860 | Z_872=X1_860 | Z_872=X2_879 | Z_872=Y_871 | Y_871=X1_860 | Y_871=X2_879 | Y_871=X_881 | Z_872=X_881 | X_881=X1_860 | X_881=X2_879 | X_881=V_867 | Y_871=V_867 | Z_872=V_867 | X1_860=V_867 | X2_879=V_867 | ~member(U_182, X2_879, W_181) | ~member(U_182, X1_860, W_181) | ~member(U_182, Z_872, W_181) | ~member(U_182, Y_871, W_181) | ~member(U_182, X_881, W_181) | ~member(U_182, V_867, W_181) | X2_862=X1_886 | Z_880=X1_886 | Z_880=X2_862 | Z_880=Y_870 | Y_870=X1_886 | Y_870=X2_862 | Y_870=X_888 | Z_880=X_888 | X_888=X1_886 | X_888=X2_862 | X_888=V_892 | Y_870=V_892 | Z_880=V_892 | X1_886=V_892 | X2_862=V_892 | ~member(U_182, X2_862, W_181) | ~member(U_182, X1_886, W_181) | ~member(U_182, Z_880, W_181) | ~member(U_182, Y_870, W_181) | ~member(U_182, X_888, W_181) | ~member(U_182, V_892, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.20 tff(c_958, plain, (![X_758, Z_183, X1_742, Y_760, X2_185, V_748, V_767, X1_765, Z_759, X1_754, X_763, Y_753, U_747, W_181, V_755, X2_744, X2_750, X1_184, V_749, X_766, Y_187, X2_745, Z_743, X2_756, X_186, Y_752, Z_757, X_762, V_188, U_182, Z_764, X1_761, Y_746]: (skf23(V_749, X_766, Y_746, Z_759, X1_754, X2_750, W_181, U_182)=skf23(V_748, X_758, Y_753, Z_743, X1_765, X2_756, W_181, U_182) | skf23(V_767, X_762, Y_752, Z_757, X1_761, X2_745, W_181, U_182)=skf23(V_748, X_758, Y_753, Z_743, X1_765, X2_756, W_181, U_182) | skf23(V_767, X_762, Y_752, Z_757, X1_761, X2_745, W_181, U_182)=skf23(V_749, X_766, Y_746, Z_759, X1_754, X2_750, W_181, U_182) | skf23(V_767, X_762, Y_752, Z_757, X1_761, X2_745, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_748, X_758, Y_753, Z_743, X1_765, X2_756, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_749, X_766, Y_746, Z_759, X1_754, X2_750, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_755 | skf23(V_767, X_762, Y_752, Z_757, X1_761, X2_745, W_181, U_182)=V_755 | skf23(V_748, X_758, Y_753, Z_743, X1_765, X2_756, W_181, U_182)=V_755 | skf23(V_749, X_766, Y_746, Z_759, X1_754, X2_750, W_181, U_182)=V_755 | V_755=U_747 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_747 | skf23(V_767, X_762, Y_752, Z_757, X1_761, X2_745, W_181, U_182)=U_747 | skf23(V_748, X_758, Y_753, Z_743, X1_765, X2_756, W_181, U_182)=U_747 | skf23(V_749, X_766, Y_746, Z_759, X1_754, X2_750, W_181, U_182)=U_747 | ~member(U_182, V_755, W_181) | ~member(U_182, U_747, W_181) | skf23(U_747, V_755, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), X_763, Y_760, Z_764, X1_742, X2_744)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_750=X1_754 | Z_759=X1_754 | Z_759=X2_750 | Z_759=Y_746 | Y_746=X1_754 | Y_746=X2_750 | Y_746=X_766 | Z_759=X_766 | X_766=X1_754 | X_766=X2_750 | X_766=V_749 | Y_746=V_749 | Z_759=V_749 | X1_754=V_749 | X2_750=V_749 | ~member(U_182, X2_750, W_181) | ~member(U_182, X1_754, W_181) | ~member(U_182, Z_759, W_181) | ~member(U_182, Y_746, W_181) | ~member(U_182, X_766, W_181) | ~member(U_182, V_749, W_181) | X2_756=X1_765 | Z_743=X1_765 | Z_743=X2_756 | Z_743=Y_753 | Y_753=X1_765 | Y_753=X2_756 | Y_753=X_758 | Z_743=X_758 | X_758=X1_765 | X_758=X2_756 | X_758=V_748 | Y_753=V_748 | Z_743=V_748 | X1_765=V_748 | X2_756=V_748 | ~member(U_182, X2_756, W_181) | ~member(U_182, X1_765, W_181) | ~member(U_182, Z_743, W_181) | ~member(U_182, Y_753, W_181) | ~member(U_182, X_758, W_181) | ~member(U_182, V_748, W_181) | X2_745=X1_761 | Z_757=X1_761 | Z_757=X2_745 | Z_757=Y_752 | Y_752=X1_761 | Y_752=X2_745 | Y_752=X_762 | Z_757=X_762 | X_762=X1_761 | X_762=X2_745 | X_762=V_767 | Y_752=V_767 | Z_757=V_767 | X1_761=V_767 | X2_745=V_767 | ~member(U_182, X2_745, W_181) | ~member(U_182, X1_761, W_181) | ~member(U_182, Z_757, W_181) | ~member(U_182, Y_752, W_181) | ~member(U_182, X_762, W_181) | ~member(U_182, V_767, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.20 tff(c_936, plain, (![Y_726, Z_183, X_731, X2_730, V_736, X2_185, X1_725, X1_729, X_722, X_733, V_737, V_734, X2_714, W_181, X5_716, Y_717, Z_728, V_738, X1_184, X1_732, X1_710, Y_187, X2_715, W_713, Y_724, X_186, V_188, U_182, Z_721, Z_735, U_711, X_720, X2_723, Z_727, Y_719]: (skf23(V_737, X_722, Y_724, Z_728, X1_710, X2_714, W_181, U_182)=skf23(V_734, X_720, Y_717, Z_735, X1_725, X2_730, W_181, U_182) | skf23(V_738, X_733, Y_719, Z_727, X1_732, X2_715, W_181, U_182)=skf23(V_737, X_722, Y_724, Z_728, X1_710, X2_714, W_181, U_182) | skf23(V_738, X_733, Y_719, Z_727, X1_732, X2_715, W_181, U_182)=skf23(V_734, X_720, Y_717, Z_735, X1_725, X2_730, W_181, U_182) | skf23(V_738, X_733, Y_719, Z_727, X1_732, X2_715, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_737, X_722, Y_724, Z_728, X1_710, X2_714, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_734, X_720, Y_717, Z_735, X1_725, X2_730, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_716 | skf23(V_738, X_733, Y_719, Z_727, X1_732, X2_715, W_181, U_182)=X5_716 | skf23(V_737, X_722, Y_724, Z_728, X1_710, X2_714, W_181, U_182)=X5_716 | skf23(V_734, X_720, Y_717, Z_735, X1_725, X2_730, W_181, U_182)=X5_716 | X5_716=U_711 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_711 | skf23(V_738, X_733, Y_719, Z_727, X1_732, X2_715, W_181, U_182)=U_711 | skf23(V_737, X_722, Y_724, Z_728, X1_710, X2_714, W_181, U_182)=U_711 | skf23(V_734, X_720, Y_717, Z_735, X1_725, X2_730, W_181, U_182)=U_711 | ~member(U_182, X5_716, W_181) | ~member(U_182, U_711, W_181) | skf23(U_711, V_736, W_713, X_731, Y_726, Z_721, X1_729, X2_723)!=U_711 | X2_730=X1_725 | Z_735=X1_725 | Z_735=X2_730 | Z_735=Y_717 | Y_717=X1_725 | Y_717=X2_730 | Y_717=X_720 | Z_735=X_720 | X_720=X1_725 | X_720=X2_730 | X_720=V_734 | Y_717=V_734 | Z_735=V_734 | X1_725=V_734 | X2_730=V_734 | ~member(U_182, X2_730, W_181) | ~member(U_182, X1_725, W_181) | ~member(U_182, Z_735, W_181) | ~member(U_182, Y_717, W_181) | ~member(U_182, X_720, W_181) | ~member(U_182, V_734, W_181) | X2_714=X1_710 | Z_728=X1_710 | Z_728=X2_714 | Z_728=Y_724 | Y_724=X1_710 | Y_724=X2_714 | Y_724=X_722 | Z_728=X_722 | X_722=X1_710 | X_722=X2_714 | X_722=V_737 | Y_724=V_737 | Z_728=V_737 | X1_710=V_737 | X2_714=V_737 | ~member(U_182, X2_714, W_181) | ~member(U_182, X1_710, W_181) | ~member(U_182, Z_728, W_181) | ~member(U_182, Y_724, W_181) | ~member(U_182, X_722, W_181) | ~member(U_182, V_737, W_181) | X2_715=X1_732 | Z_727=X1_732 | Z_727=X2_715 | Z_727=Y_719 | Y_719=X1_732 | Y_719=X2_715 | Y_719=X_733 | Z_727=X_733 | X_733=X1_732 | X_733=X2_715 | X_733=V_738 | Y_719=V_738 | Z_727=V_738 | X1_732=V_738 | X2_715=V_738 | ~member(U_182, X2_715, W_181) | ~member(U_182, X1_732, W_181) | ~member(U_182, Z_727, W_181) | ~member(U_182, Y_719, W_181) | ~member(U_182, X_733, W_181) | ~member(U_182, V_738, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.20 tff(c_980, plain, (![Z_183, Z_785, V_780, Z_772, V_775, Y_777, X2_784, X2_770, U_786, X2_185, X1_781, X2_768, Z_783, X2_779, Y_793, X_794, W_181, Z_774, X1_782, W_788, X1_184, V_796, Y_787, Y_187, X1_771, X_791, X_795, X_186, X1_789, V_188, V_792, U_182, X_790, Y_773]: (skf23(V_792, X_795, Y_793, Z_772, X1_782, X2_784, W_181, U_182)=skf23(V_780, X_790, Y_787, Z_774, X1_781, X2_768, W_181, U_182) | skf23(V_796, X_791, Y_777, Z_783, X1_789, X2_770, W_181, U_182)=skf23(V_780, X_790, Y_787, Z_774, X1_781, X2_768, W_181, U_182) | skf23(V_796, X_791, Y_777, Z_783, X1_789, X2_770, W_181, U_182)=skf23(V_792, X_795, Y_793, Z_772, X1_782, X2_784, W_181, U_182) | skf23(V_796, X_791, Y_777, Z_783, X1_789, X2_770, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_780, X_790, Y_787, Z_774, X1_781, X2_768, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_792, X_795, Y_793, Z_772, X1_782, X2_784, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_775 | skf23(V_796, X_791, Y_777, Z_783, X1_789, X2_770, W_181, U_182)=V_775 | skf23(V_780, X_790, Y_787, Z_774, X1_781, X2_768, W_181, U_182)=V_775 | skf23(V_792, X_795, Y_793, Z_772, X1_782, X2_784, W_181, U_182)=V_775 | V_775=U_786 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_786 | skf23(V_796, X_791, Y_777, Z_783, X1_789, X2_770, W_181, U_182)=U_786 | skf23(V_780, X_790, Y_787, Z_774, X1_781, X2_768, W_181, U_182)=U_786 | skf23(V_792, X_795, Y_793, Z_772, X1_782, X2_784, W_181, U_182)=U_786 | ~member(U_182, V_775, W_181) | ~member(U_182, U_786, W_181) | skf23(U_786, V_775, W_788, X_794, Y_773, Z_785, X1_771, X2_779)!=V_775 | X2_784=X1_782 | Z_772=X1_782 | Z_772=X2_784 | Z_772=Y_793 | Y_793=X1_782 | Y_793=X2_784 | Y_793=X_795 | Z_772=X_795 | X_795=X1_782 | X_795=X2_784 | X_795=V_792 | Y_793=V_792 | Z_772=V_792 | X1_782=V_792 | X2_784=V_792 | ~member(U_182, X2_784, W_181) | ~member(U_182, X1_782, W_181) | ~member(U_182, Z_772, W_181) | ~member(U_182, Y_793, W_181) | ~member(U_182, X_795, W_181) | ~member(U_182, V_792, W_181) | X2_768=X1_781 | Z_774=X1_781 | Z_774=X2_768 | Z_774=Y_787 | Y_787=X1_781 | Y_787=X2_768 | Y_787=X_790 | Z_774=X_790 | X_790=X1_781 | X_790=X2_768 | X_790=V_780 | Y_787=V_780 | Z_774=V_780 | X1_781=V_780 | X2_768=V_780 | ~member(U_182, X2_768, W_181) | ~member(U_182, X1_781, W_181) | ~member(U_182, Z_774, W_181) | ~member(U_182, Y_787, W_181) | ~member(U_182, X_790, W_181) | ~member(U_182, V_780, W_181) | X2_770=X1_789 | Z_783=X1_789 | Z_783=X2_770 | Z_783=Y_777 | Y_777=X1_789 | Y_777=X2_770 | Y_777=X_791 | Z_783=X_791 | X_791=X1_789 | X_791=X2_770 | X_791=V_796 | Y_777=V_796 | Z_783=V_796 | X1_789=V_796 | X2_770=V_796 | ~member(U_182, X2_770, W_181) | ~member(U_182, X1_789, W_181) | ~member(U_182, Z_783, W_181) | ~member(U_182, Y_777, W_181) | ~member(U_182, X_791, W_181) | ~member(U_182, V_796, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_891, plain, (![Z_183, X_655, X1_663, Y_658, X2_185, W_651, Z_654, Y_649, W_181, U_650, Z_661, X1_657, X1_184, V_647, V_662, Y_187, Y_653, V_643, X_659, X1_656, X2_652, X2_644, Z_645, X_186, V_188, U_182, X2_660]: (skf23(V_662, X_659, Y_649, Z_654, X1_657, X2_644, W_181, U_182)=skf23(V_647, X_655, Y_658, Z_661, X1_663, X2_652, W_181, U_182) | skf23(V_662, X_659, Y_649, Z_654, X1_657, X2_644, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_647, X_655, Y_658, Z_661, X1_663, X2_652, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_651 | skf23(V_662, X_659, Y_649, Z_654, X1_657, X2_644, W_181, U_182)=W_651 | skf23(V_647, X_655, Y_658, Z_661, X1_663, X2_652, W_181, U_182)=W_651 | W_651=V_643 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_643 | skf23(V_662, X_659, Y_649, Z_654, X1_657, X2_644, W_181, U_182)=V_643 | skf23(V_647, X_655, Y_658, Z_661, X1_663, X2_652, W_181, U_182)=V_643 | V_643=U_650 | W_651=U_650 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_650 | skf23(V_662, X_659, Y_649, Z_654, X1_657, X2_644, W_181, U_182)=U_650 | skf23(V_647, X_655, Y_658, Z_661, X1_663, X2_652, W_181, U_182)=U_650 | ~member(U_182, W_651, W_181) | ~member(U_182, V_643, W_181) | ~member(U_182, U_650, W_181) | skf23(U_650, V_643, W_651, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), Y_653, Z_645, X1_656, X2_660)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_652=X1_663 | Z_661=X1_663 | Z_661=X2_652 | Z_661=Y_658 | Y_658=X1_663 | Y_658=X2_652 | Y_658=X_655 | Z_661=X_655 | X_655=X1_663 | X_655=X2_652 | X_655=V_647 | Y_658=V_647 | Z_661=V_647 | X1_663=V_647 | X2_652=V_647 | ~member(U_182, X2_652, W_181) | ~member(U_182, X1_663, W_181) | ~member(U_182, Z_661, W_181) | ~member(U_182, Y_658, W_181) | ~member(U_182, X_655, W_181) | ~member(U_182, V_647, W_181) | X2_644=X1_657 | Z_654=X1_657 | Z_654=X2_644 | Z_654=Y_649 | Y_649=X1_657 | Y_649=X2_644 | Y_649=X_659 | Z_654=X_659 | X_659=X1_657 | X_659=X2_644 | X_659=V_662 | Y_649=V_662 | Z_654=V_662 | X1_657=V_662 | X2_644=V_662 | ~member(U_182, X2_644, W_181) | ~member(U_182, X1_657, W_181) | ~member(U_182, Z_654, W_181) | ~member(U_182, Y_649, W_181) | ~member(U_182, X_659, W_181) | ~member(U_182, V_662, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_847, plain, (![Z_183, X1_612, X2_605, X2_599, X2_185, X1_617, W_606, X_613, V_618, X1_609, Y_596, W_181, V_614, Y_607, Z_608, X1_184, V_610, X_615, Y_187, X5_600, U_604, Z_595, Z_598, X_186, X_616, V_188, U_182, X2_611, Y_602]: (skf23(V_618, X_613, Y_602, Z_608, X1_612, X2_599, W_181, U_182)=skf23(V_614, X_616, Y_596, Z_598, X1_617, X2_611, W_181, U_182) | skf23(V_618, X_613, Y_602, Z_608, X1_612, X2_599, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_614, X_616, Y_596, Z_598, X1_617, X2_611, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_600 | skf23(V_618, X_613, Y_602, Z_608, X1_612, X2_599, W_181, U_182)=X5_600 | skf23(V_614, X_616, Y_596, Z_598, X1_617, X2_611, W_181, U_182)=X5_600 | X5_600=V_610 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_610 | skf23(V_618, X_613, Y_602, Z_608, X1_612, X2_599, W_181, U_182)=V_610 | skf23(V_614, X_616, Y_596, Z_598, X1_617, X2_611, W_181, U_182)=V_610 | V_610=U_604 | X5_600=U_604 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_604 | skf23(V_618, X_613, Y_602, Z_608, X1_612, X2_599, W_181, U_182)=U_604 | skf23(V_614, X_616, Y_596, Z_598, X1_617, X2_611, W_181, U_182)=U_604 | ~member(U_182, X5_600, W_181) | ~member(U_182, V_610, W_181) | ~member(U_182, U_604, W_181) | skf23(U_604, V_610, W_606, X_615, Y_607, Z_595, X1_609, X2_605)!=V_610 | X2_611=X1_617 | Z_598=X1_617 | Z_598=X2_611 | Z_598=Y_596 | Y_596=X1_617 | Y_596=X2_611 | Y_596=X_616 | Z_598=X_616 | X_616=X1_617 | X_616=X2_611 | X_616=V_614 | Y_596=V_614 | Z_598=V_614 | X1_617=V_614 | X2_611=V_614 | ~member(U_182, X2_611, W_181) | ~member(U_182, X1_617, W_181) | ~member(U_182, Z_598, W_181) | ~member(U_182, Y_596, W_181) | ~member(U_182, X_616, W_181) | ~member(U_182, V_614, W_181) | X2_599=X1_612 | Z_608=X1_612 | Z_608=X2_599 | Z_608=Y_602 | Y_602=X1_612 | Y_602=X2_599 | Y_602=X_613 | Z_608=X_613 | X_613=X1_612 | X_613=X2_599 | X_613=V_618 | Y_602=V_618 | Z_608=V_618 | X1_612=V_618 | X2_599=V_618 | ~member(U_182, X2_599, W_181) | ~member(U_182, X1_612, W_181) | ~member(U_182, Z_608, W_181) | ~member(U_182, Y_602, W_181) | ~member(U_182, X_613, W_181) | ~member(U_182, V_618, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_869, plain, (![V_641, Z_183, X2_623, X2_185, X1_636, W_635, X_622, Z_633, V_619, W_181, Y_629, X2_631, X1_627, X2_625, X1_184, Z_624, X_637, V_626, Y_187, U_638, Z_630, X_186, X1_634, V_188, U_182, X_620, Y_640, Y_632]: (skf23(V_641, X_637, Y_629, Z_633, X1_636, X2_623, W_181, U_182)=skf23(V_619, X_622, Y_632, Z_630, X1_634, X2_631, W_181, U_182) | skf23(V_641, X_637, Y_629, Z_633, X1_636, X2_623, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_619, X_622, Y_632, Z_630, X1_634, X2_631, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_635 | skf23(V_641, X_637, Y_629, Z_633, X1_636, X2_623, W_181, U_182)=W_635 | skf23(V_619, X_622, Y_632, Z_630, X1_634, X2_631, W_181, U_182)=W_635 | W_635=V_626 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_626 | skf23(V_641, X_637, Y_629, Z_633, X1_636, X2_623, W_181, U_182)=V_626 | skf23(V_619, X_622, Y_632, Z_630, X1_634, X2_631, W_181, U_182)=V_626 | V_626=U_638 | W_635=U_638 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_638 | skf23(V_641, X_637, Y_629, Z_633, X1_636, X2_623, W_181, U_182)=U_638 | skf23(V_619, X_622, Y_632, Z_630, X1_634, X2_631, W_181, U_182)=U_638 | ~member(U_182, W_635, W_181) | ~member(U_182, V_626, W_181) | ~member(U_182, U_638, W_181) | skf23(U_638, V_626, W_635, X_620, Y_640, Z_624, X1_627, X2_625)!=W_635 | X2_631=X1_634 | Z_630=X1_634 | Z_630=X2_631 | Z_630=Y_632 | Y_632=X1_634 | Y_632=X2_631 | Y_632=X_622 | Z_630=X_622 | X_622=X1_634 | X_622=X2_631 | X_622=V_619 | Y_632=V_619 | Z_630=V_619 | X1_634=V_619 | X2_631=V_619 | ~member(U_182, X2_631, W_181) | ~member(U_182, X1_634, W_181) | ~member(U_182, Z_630, W_181) | ~member(U_182, Y_632, W_181) | ~member(U_182, X_622, W_181) | ~member(U_182, V_619, W_181) | X2_623=X1_636 | Z_633=X1_636 | Z_633=X2_623 | Z_633=Y_629 | Y_629=X1_636 | Y_629=X2_623 | Y_629=X_637 | Z_633=X_637 | X_637=X1_636 | X_637=X2_623 | X_637=V_641 | Y_629=V_641 | Z_633=V_641 | X1_636=V_641 | X2_623=V_641 | ~member(U_182, X2_623, W_181) | ~member(U_182, X1_636, W_181) | ~member(U_182, Z_633, W_181) | ~member(U_182, Y_629, W_181) | ~member(U_182, X_637, W_181) | ~member(U_182, V_641, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_913, plain, (![Z_183, X1_685, U_673, X6_671, Y_669, V_686, X_681, Z_676, X2_185, X2_666, X2_677, Y_674, X2_684, Z_672, Y_678, W_181, X1_667, X5_679, X1_184, Y_187, W_665, V_670, V_688, X_675, X_683, X_186, V_188, U_182, X1_682, Z_680]: (skf23(V_688, X_683, Y_669, Z_676, X1_682, X2_666, W_181, U_182)=skf23(V_686, X_675, Y_674, Z_680, X1_667, X2_684, W_181, U_182) | skf23(V_688, X_683, Y_669, Z_676, X1_682, X2_666, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_686, X_675, Y_674, Z_680, X1_667, X2_684, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X6_671 | skf23(V_688, X_683, Y_669, Z_676, X1_682, X2_666, W_181, U_182)=X6_671 | skf23(V_686, X_675, Y_674, Z_680, X1_667, X2_684, W_181, U_182)=X6_671 | X6_671=X5_679 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_679 | skf23(V_688, X_683, Y_669, Z_676, X1_682, X2_666, W_181, U_182)=X5_679 | skf23(V_686, X_675, Y_674, Z_680, X1_667, X2_684, W_181, U_182)=X5_679 | X5_679=U_673 | X6_671=U_673 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_673 | skf23(V_688, X_683, Y_669, Z_676, X1_682, X2_666, W_181, U_182)=U_673 | skf23(V_686, X_675, Y_674, Z_680, X1_667, X2_684, W_181, U_182)=U_673 | ~member(U_182, X6_671, W_181) | ~member(U_182, X5_679, W_181) | ~member(U_182, U_673, W_181) | skf23(U_673, V_670, W_665, X_681, Y_678, Z_672, X1_685, X2_677)!=U_673 | X2_684=X1_667 | Z_680=X1_667 | Z_680=X2_684 | Z_680=Y_674 | Y_674=X1_667 | Y_674=X2_684 | Y_674=X_675 | Z_680=X_675 | X_675=X1_667 | X_675=X2_684 | X_675=V_686 | Y_674=V_686 | Z_680=V_686 | X1_667=V_686 | X2_684=V_686 | ~member(U_182, X2_684, W_181) | ~member(U_182, X1_667, W_181) | ~member(U_182, Z_680, W_181) | ~member(U_182, Y_674, W_181) | ~member(U_182, X_675, W_181) | ~member(U_182, V_686, W_181) | X2_666=X1_682 | Z_676=X1_682 | Z_676=X2_666 | Z_676=Y_669 | Y_669=X1_682 | Y_669=X2_666 | Y_669=X_683 | Z_676=X_683 | X_683=X1_682 | X_683=X2_666 | X_683=V_688 | Y_669=V_688 | Z_676=V_688 | X1_682=V_688 | X2_666=V_688 | ~member(U_182, X2_666, W_181) | ~member(U_182, X1_682, W_181) | ~member(U_182, Z_676, W_181) | ~member(U_182, Y_669, W_181) | ~member(U_182, X_683, W_181) | ~member(U_182, V_688, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_824, plain, (![Z_183, X_568, X2_572, X2_185, Z_570, V_578, X2_579, X1_577, X_565, U_564, Y_574, X1_566, W_181, X1_184, Y_187, V_575, X_186, V_188, U_182, Z_567, W_571]: (skf23(V_575, X_565, Y_574, Z_567, X1_566, X2_572, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X_568 | skf23(V_575, X_565, Y_574, Z_567, X1_566, X2_572, W_181, U_182)=X_568 | X_568=W_571 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_571 | skf23(V_575, X_565, Y_574, Z_567, X1_566, X2_572, W_181, U_182)=W_571 | W_571=V_578 | X_568=V_578 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_578 | skf23(V_575, X_565, Y_574, Z_567, X1_566, X2_572, W_181, U_182)=V_578 | V_578=U_564 | W_571=U_564 | X_568=U_564 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_564 | skf23(V_575, X_565, Y_574, Z_567, X1_566, X2_572, W_181, U_182)=U_564 | ~member(U_182, X_568, W_181) | ~member(U_182, W_571, W_181) | ~member(U_182, V_578, W_181) | ~member(U_182, U_564, W_181) | skf23(U_564, V_578, W_571, X_568, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), Z_570, X1_577, X2_579)!=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | X2_572=X1_566 | Z_567=X1_566 | Z_567=X2_572 | Z_567=Y_574 | Y_574=X1_566 | Y_574=X2_572 | Y_574=X_565 | Z_567=X_565 | X_565=X1_566 | X_565=X2_572 | X_565=V_575 | Y_574=V_575 | Z_567=V_575 | X1_566=V_575 | X2_572=V_575 | ~member(U_182, X2_572, W_181) | ~member(U_182, X1_566, W_181) | ~member(U_182, Z_567, W_181) | ~member(U_182, Y_574, W_181) | ~member(U_182, X_565, W_181) | ~member(U_182, V_575, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_780, plain, (![Z_183, X_527, X7_526, U_525, X5_536, X2_544, Y_540, W_541, V_533, X2_185, X1_535, X2_538, X6_531, X1_528, Z_534, W_181, X1_184, Y_187, V_542, Y_532, Z_529, X_186, V_188, U_182, X_537]: (skf23(V_542, X_527, Y_540, Z_529, X1_528, X2_538, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X7_526 | skf23(V_542, X_527, Y_540, Z_529, X1_528, X2_538, W_181, U_182)=X7_526 | X7_526=X6_531 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X6_531 | skf23(V_542, X_527, Y_540, Z_529, X1_528, X2_538, W_181, U_182)=X6_531 | X6_531=X5_536 | X7_526=X5_536 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_536 | skf23(V_542, X_527, Y_540, Z_529, X1_528, X2_538, W_181, U_182)=X5_536 | X5_536=U_525 | X6_531=U_525 | X7_526=U_525 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_525 | skf23(V_542, X_527, Y_540, Z_529, X1_528, X2_538, W_181, U_182)=U_525 | ~member(U_182, X7_526, W_181) | ~member(U_182, X6_531, W_181) | ~member(U_182, X5_536, W_181) | ~member(U_182, U_525, W_181) | skf23(U_525, V_533, W_541, X_537, Y_532, Z_534, X1_535, X2_544)!=U_525 | X2_538=X1_528 | Z_529=X1_528 | Z_529=X2_538 | Z_529=Y_540 | Y_540=X1_528 | Y_540=X2_538 | Y_540=X_527 | Z_529=X_527 | X_527=X1_528 | X_527=X2_538 | X_527=V_542 | Y_540=V_542 | Z_529=V_542 | X1_528=V_542 | X2_538=V_542 | ~member(U_182, X2_538, W_181) | ~member(U_182, X1_528, W_181) | ~member(U_182, Z_529, W_181) | ~member(U_182, Y_540, W_181) | ~member(U_182, X_527, W_181) | ~member(U_182, V_542, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_758, plain, (![Z_183, X2_524, X2_185, W_522, X_517, V_521, Y_511, X2_518, W_181, Y_520, X1_516, Z_510, U_512, X1_184, Z_515, Y_187, V_513, X1_509, X_186, V_188, U_182, X_508]: (skf23(V_521, X_508, Y_520, Z_510, X1_509, X2_518, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X_517 | skf23(V_521, X_508, Y_520, Z_510, X1_509, X2_518, W_181, U_182)=X_517 | X_517=W_522 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_522 | skf23(V_521, X_508, Y_520, Z_510, X1_509, X2_518, W_181, U_182)=W_522 | W_522=V_513 | X_517=V_513 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_513 | skf23(V_521, X_508, Y_520, Z_510, X1_509, X2_518, W_181, U_182)=V_513 | V_513=U_512 | W_522=U_512 | X_517=U_512 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_512 | skf23(V_521, X_508, Y_520, Z_510, X1_509, X2_518, W_181, U_182)=U_512 | ~member(U_182, X_517, W_181) | ~member(U_182, W_522, W_181) | ~member(U_182, V_513, W_181) | ~member(U_182, U_512, W_181) | skf23(U_512, V_513, W_522, X_517, Y_511, Z_515, X1_516, X2_524)!=X_517 | X2_518=X1_509 | Z_510=X1_509 | Z_510=X2_518 | Z_510=Y_520 | Y_520=X1_509 | Y_520=X2_518 | Y_520=X_508 | Z_510=X_508 | X_508=X1_509 | X_508=X2_518 | X_508=V_521 | Y_520=V_521 | Z_510=V_521 | X1_509=V_521 | X2_518=V_521 | ~member(U_182, X2_518, W_181) | ~member(U_182, X1_509, W_181) | ~member(U_182, Z_510, W_181) | ~member(U_182, Y_520, W_181) | ~member(U_182, X_508, W_181) | ~member(U_182, V_521, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_736, plain, (![Z_183, V_496, W_490, V_504, X1_492, X2_185, X2_501, Z_505, X1_506, W_181, X5_497, Y_498, X1_184, Y_187, Y_503, X_491, X_186, V_188, X_495, U_182, U_500, X2_494, Z_493]: (skf23(V_504, X_491, Y_503, Z_493, X1_492, X2_501, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_497 | skf23(V_504, X_491, Y_503, Z_493, X1_492, X2_501, W_181, U_182)=X5_497 | X5_497=W_490 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=W_490 | skf23(V_504, X_491, Y_503, Z_493, X1_492, X2_501, W_181, U_182)=W_490 | W_490=V_496 | X5_497=V_496 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_496 | skf23(V_504, X_491, Y_503, Z_493, X1_492, X2_501, W_181, U_182)=V_496 | V_496=U_500 | W_490=U_500 | X5_497=U_500 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_500 | skf23(V_504, X_491, Y_503, Z_493, X1_492, X2_501, W_181, U_182)=U_500 | ~member(U_182, X5_497, W_181) | ~member(U_182, W_490, W_181) | ~member(U_182, V_496, W_181) | ~member(U_182, U_500, W_181) | skf23(U_500, V_496, W_490, X_495, Y_498, Z_505, X1_506, X2_494)!=W_490 | X2_501=X1_492 | Z_493=X1_492 | Z_493=X2_501 | Z_493=Y_503 | Y_503=X1_492 | Y_503=X2_501 | Y_503=X_491 | Z_493=X_491 | X_491=X1_492 | X_491=X2_501 | X_491=V_504 | Y_503=V_504 | Z_493=V_504 | X1_492=V_504 | X2_501=V_504 | ~member(U_182, X2_501, W_181) | ~member(U_182, X1_492, W_181) | ~member(U_182, Z_493, W_181) | ~member(U_182, Y_503, W_181) | ~member(U_182, X_491, W_181) | ~member(U_182, V_504, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_802, plain, (![Z_183, X2_555, Z_549, W_563, X2_185, V_545, X2_557, Z_552, W_181, X6_550, X_551, X1_548, X1_184, Y_187, Y_560, X1_556, V_561, X5_553, X_186, V_188, U_182, Y_554, U_559, X_547]: (skf23(V_561, X_547, Y_560, Z_549, X1_548, X2_557, W_181, U_182)=skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182) | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X6_550 | skf23(V_561, X_547, Y_560, Z_549, X1_548, X2_557, W_181, U_182)=X6_550 | X6_550=X5_553 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=X5_553 | skf23(V_561, X_547, Y_560, Z_549, X1_548, X2_557, W_181, U_182)=X5_553 | X5_553=V_545 | X6_550=V_545 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=V_545 | skf23(V_561, X_547, Y_560, Z_549, X1_548, X2_557, W_181, U_182)=V_545 | V_545=U_559 | X5_553=U_559 | X6_550=U_559 | skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182)=U_559 | skf23(V_561, X_547, Y_560, Z_549, X1_548, X2_557, W_181, U_182)=U_559 | ~member(U_182, X6_550, W_181) | ~member(U_182, X5_553, W_181) | ~member(U_182, V_545, W_181) | ~member(U_182, U_559, W_181) | skf23(U_559, V_545, W_563, X_551, Y_554, Z_552, X1_556, X2_555)!=V_545 | X2_557=X1_548 | Z_549=X1_548 | Z_549=X2_557 | Z_549=Y_560 | Y_560=X1_548 | Y_560=X2_557 | Y_560=X_547 | Z_549=X_547 | X_547=X1_548 | X_547=X2_557 | X_547=V_561 | Y_560=V_561 | Z_549=V_561 | X1_548=V_561 | X2_557=V_561 | ~member(U_182, X2_557, W_181) | ~member(U_182, X1_548, W_181) | ~member(U_182, Z_549, W_181) | ~member(U_182, Y_560, W_181) | ~member(U_182, X_547, W_181) | ~member(U_182, V_561, W_181) | X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_715, plain, (![U_484, Y_485, X1_193, Y_196, V_197, X_195, W_189, V_489, X1_487, U_191, X2_194, Z_486, X_488, X2_483, W_482]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=Y_196 | Y_196=X_195 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X_195 | X_195=W_189 | Y_196=W_189 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=W_189 | W_189=V_197 | X_195=V_197 | Y_196=V_197 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_197 | V_197=U_191 | W_189=U_191 | X_195=U_191 | Y_196=U_191 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_191 | ~member(U_484, Y_196, W_482) | ~member(U_484, X_195, W_482) | ~member(U_484, W_189, W_482) | ~member(U_484, V_197, W_482) | ~member(U_484, U_191, W_482) | skf23(U_191, V_197, W_189, X_195, Y_196, skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484), X1_193, X2_194)!=skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484) | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 63.13/54.21 tff(c_714, plain, (![U_484, Y_485, X_206, X1_204, W_200, V_208, V_489, X2_205, X1_487, U_202, Y_207, Z_203, Z_486, X_488, X2_483, W_482]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=Y_207 | Y_207=X_206 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X_206 | X_206=W_200 | Y_207=W_200 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_202 | ~member(U_484, Y_207, W_482) | ~member(U_484, X_206, W_482) | ~member(U_484, W_200, W_482) | ~member(U_484, V_208, W_482) | ~member(U_484, U_202, W_482) | skf23(U_202, V_208, W_200, X_206, Y_207, Z_203, X1_204, X2_205)!=Y_207 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 63.13/54.21 tff(c_713, plain, (![U_484, Y_485, X6_153, X2_160, V_163, U_156, Z_157, V_489, W_154, X1_487, X7_158, X5_152, X_161, Y_162, Z_486, X_488, X2_483, W_482, X1_159]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X7_158 | X7_158=X6_153 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X6_153 | X6_153=X5_152 | X7_158=X5_152 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X5_152 | X5_152=V_163 | X6_153=V_163 | X7_158=V_163 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_163 | V_163=U_156 | X5_152=U_156 | X6_153=U_156 | X7_158=U_156 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_156 | ~member(U_484, X7_158, W_482) | ~member(U_484, X6_153, W_482) | ~member(U_484, X5_152, W_482) | ~member(U_484, V_163, W_482) | ~member(U_484, U_156, W_482) | skf23(U_156, V_163, W_154, X_161, Y_162, Z_157, X1_159, X2_160)!=V_163 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 63.13/54.21 tff(c_716, plain, (![U_484, Y_485, Z_172, X5_166, V_178, X_176, V_489, X1_487, U_170, X6_167, X1_174, Y_177, X7_173, X2_175, X8_179, W_168, Z_486, X_488, X2_483, W_482]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X8_179 | X8_179=X7_173 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X7_173 | X7_173=X6_167 | X8_179=X6_167 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X6_167 | X6_167=X5_166 | X7_173=X5_166 | X8_179=X5_166 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X5_166 | X5_166=U_170 | X6_167=U_170 | X7_173=U_170 | X8_179=U_170 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_170 | ~member(U_484, X8_179, W_482) | ~member(U_484, X7_173, W_482) | ~member(U_484, X6_167, W_482) | ~member(U_484, X5_166, W_482) | ~member(U_484, U_170, W_482) | skf23(U_170, V_178, W_168, X_176, Y_177, Z_172, X1_174, X2_175)!=U_170 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 63.13/54.21 tff(c_717, plain, (![U_484, Y_485, Y_136, V_137, X5_127, X1_133, V_489, W_129, X1_487, Z_132, X_135, X2_134, Z_486, X_488, X2_483, W_482, U_131]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X5_127 | X_135=X5_127 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X_135 | X_135=W_129 | X5_127=W_129 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=W_129 | W_129=V_137 | X_135=V_137 | X5_127=V_137 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_137 | V_137=U_131 | W_129=U_131 | X_135=U_131 | X5_127=U_131 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_131 | ~member(U_484, X5_127, W_482) | ~member(U_484, X_135, W_482) | ~member(U_484, W_129, W_482) | ~member(U_484, V_137, W_482) | ~member(U_484, U_131, W_482) | skf23(U_131, V_137, W_129, X_135, Y_136, Z_132, X1_133, X2_134)!=X_135 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 63.13/54.21 tff(c_712, plain, (![U_484, Y_485, X6_140, X2_147, X5_139, V_489, X1_487, X1_146, X_148, W_141, Z_144, V_150, Z_486, X_488, X2_483, W_482, U_143, Y_149]: (skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X6_140 | X6_140=X5_139 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=X5_139 | X5_139=W_141 | X6_140=W_141 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=W_141 | W_141=V_150 | X5_139=V_150 | X6_140=V_150 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=V_150 | V_150=U_143 | W_141=U_143 | X5_139=U_143 | X6_140=U_143 | skf23(V_489, X_488, Y_485, Z_486, X1_487, X2_483, W_482, U_484)=U_143 | ~member(U_484, X6_140, W_482) | ~member(U_484, X5_139, W_482) | ~member(U_484, W_141, W_482) | ~member(U_484, V_150, W_482) | ~member(U_484, U_143, W_482) | skf23(U_143, V_150, W_141, X_148, Y_149, Z_144, X1_146, X2_147)!=W_141 | X2_483=X1_487 | Z_486=X1_487 | Z_486=X2_483 | Z_486=Y_485 | Y_485=X1_487 | Y_485=X2_483 | Y_485=X_488 | Z_486=X_488 | X_488=X1_487 | X_488=X2_483 | X_488=V_489 | Y_485=V_489 | Z_486=V_489 | X1_487=V_489 | X2_483=V_489 | six(U_484, W_482) | ~member(U_484, X2_483, W_482) | ~member(U_484, X1_487, W_482) | ~member(U_484, Z_486, W_482) | ~member(U_484, Y_485, W_482) | ~member(U_484, X_488, W_482) | ~member(U_484, V_489, W_482)))). % 63.13/54.21 tff(c_134, plain, (![Z_183, X2_185, W_181, X1_184, Y_187, X_186, V_188, U_182]: (X2_185=X1_184 | Z_183=X1_184 | Z_183=X2_185 | Z_183=Y_187 | Y_187=X1_184 | Y_187=X2_185 | Y_187=X_186 | Z_183=X_186 | X_186=X1_184 | X_186=X2_185 | X_186=V_188 | Y_187=V_188 | Z_183=V_188 | X1_184=V_188 | X2_185=V_188 | member(U_182, skf23(V_188, X_186, Y_187, Z_183, X1_184, X2_185, W_181, U_182), W_181) | six(U_182, W_181) | ~member(U_182, X2_185, W_181) | ~member(U_182, X1_184, W_181) | ~member(U_182, Z_183, W_181) | ~member(U_182, Y_187, W_181) | ~member(U_182, X_186, W_181) | ~member(U_182, V_188, W_181)))). % 63.13/54.21 tff(c_128, plain, (![X4_151, X6_140, X2_147, X5_139, X3_142, X1_146, X_148, W_141, Z_144, V_150, U_143, X7_145, Y_149]: (X7_145=X6_140 | X6_140=X5_139 | X7_145=X5_139 | X5_139=W_141 | X6_140=W_141 | X7_145=W_141 | W_141=V_150 | X5_139=V_150 | X6_140=V_150 | X7_145=V_150 | V_150=U_143 | W_141=U_143 | X5_139=U_143 | X6_140=U_143 | X7_145=U_143 | six(X3_142, X4_151) | ~member(X3_142, X7_145, X4_151) | ~member(X3_142, X6_140, X4_151) | ~member(X3_142, X5_139, X4_151) | ~member(X3_142, W_141, X4_151) | ~member(X3_142, V_150, X4_151) | ~member(X3_142, U_143, X4_151) | skf23(U_143, V_150, W_141, X_148, Y_149, Z_144, X1_146, X2_147)!=W_141))). % 63.13/54.21 tff(c_130, plain, (![X6_153, X2_160, V_163, U_156, Z_157, W_154, X7_158, X8_164, X5_152, X_161, Y_162, X3_155, X1_159, X4_165]: (X8_164=X7_158 | X7_158=X6_153 | X8_164=X6_153 | X6_153=X5_152 | X7_158=X5_152 | X8_164=X5_152 | X5_152=V_163 | X6_153=V_163 | X7_158=V_163 | X8_164=V_163 | V_163=U_156 | X5_152=U_156 | X6_153=U_156 | X7_158=U_156 | X8_164=U_156 | six(X3_155, X4_165) | ~member(X3_155, X8_164, X4_165) | ~member(X3_155, X7_158, X4_165) | ~member(X3_155, X6_153, X4_165) | ~member(X3_155, X5_152, X4_165) | ~member(X3_155, V_163, X4_165) | ~member(X3_155, U_156, X4_165) | skf23(U_156, V_163, W_154, X_161, Y_162, Z_157, X1_159, X2_160)!=V_163))). % 63.13/54.21 tff(c_138, plain, (![X3_201, X_206, X1_204, W_200, V_208, X2_205, X4_209, U_202, Y_207, X5_199, Z_203]: (Y_207=X5_199 | Y_207=X_206 | X_206=X5_199 | X_206=W_200 | Y_207=W_200 | X5_199=W_200 | W_200=V_208 | X_206=V_208 | Y_207=V_208 | X5_199=V_208 | V_208=U_202 | W_200=U_202 | X_206=U_202 | Y_207=U_202 | X5_199=U_202 | six(X3_201, X4_209) | ~member(X3_201, X5_199, X4_209) | ~member(X3_201, Y_207, X4_209) | ~member(X3_201, X_206, X4_209) | ~member(X3_201, W_200, X4_209) | ~member(X3_201, V_208, X4_209) | ~member(X3_201, U_202, X4_209) | skf23(U_202, V_208, W_200, X_206, Y_207, Z_203, X1_204, X2_205)!=Y_207))). % 63.13/54.21 tff(c_136, plain, (![X1_193, Y_196, V_197, X_195, X3_190, W_189, Z_192, U_191, X2_194, X4_198]: (Z_192=Y_196 | Y_196=X_195 | Z_192=X_195 | X_195=W_189 | Y_196=W_189 | Z_192=W_189 | W_189=V_197 | X_195=V_197 | Y_196=V_197 | Z_192=V_197 | V_197=U_191 | W_189=U_191 | X_195=U_191 | Y_196=U_191 | Z_192=U_191 | six(X3_190, X4_198) | ~member(X3_190, Z_192, X4_198) | ~member(X3_190, Y_196, X4_198) | ~member(X3_190, X_195, X4_198) | ~member(X3_190, W_189, X4_198) | ~member(X3_190, V_197, X4_198) | ~member(X3_190, U_191, X4_198) | skf23(U_191, V_197, W_189, X_195, Y_196, Z_192, X1_193, X2_194)!=Z_192))). % 63.13/54.21 tff(c_132, plain, (![Z_172, X3_169, X5_166, X4_180, V_178, X_176, X9_171, U_170, X6_167, X1_174, Y_177, X7_173, X2_175, X8_179, W_168]: (X9_171=X8_179 | X8_179=X7_173 | X9_171=X7_173 | X7_173=X6_167 | X8_179=X6_167 | X9_171=X6_167 | X6_167=X5_166 | X7_173=X5_166 | X8_179=X5_166 | X9_171=X5_166 | X5_166=U_170 | X6_167=U_170 | X7_173=U_170 | X8_179=U_170 | X9_171=U_170 | six(X3_169, X4_180) | ~member(X3_169, X9_171, X4_180) | ~member(X3_169, X8_179, X4_180) | ~member(X3_169, X7_173, X4_180) | ~member(X3_169, X6_167, X4_180) | ~member(X3_169, X5_166, X4_180) | ~member(X3_169, U_170, X4_180) | skf23(U_170, V_178, W_168, X_176, Y_177, Z_172, X1_174, X2_175)!=U_170))). % 63.13/54.21 tff(c_126, plain, (![X4_138, Y_136, V_137, X5_127, X1_133, W_129, X3_130, Z_132, X_135, X2_134, X6_128, U_131]: (X6_128=X5_127 | X_135=X5_127 | X_135=X6_128 | X_135=W_129 | X5_127=W_129 | X6_128=W_129 | W_129=V_137 | X_135=V_137 | X5_127=V_137 | X6_128=V_137 | V_137=U_131 | W_129=U_131 | X_135=U_131 | X5_127=U_131 | X6_128=U_131 | six(X3_130, X4_138) | ~member(X3_130, X6_128, X4_138) | ~member(X3_130, X5_127, X4_138) | ~member(X3_130, X_135, X4_138) | ~member(X3_130, W_129, X4_138) | ~member(X3_130, V_137, X4_138) | ~member(X3_130, U_131, X4_138) | skf23(U_131, V_137, W_129, X_135, Y_136, Z_132, X1_133, X2_134)!=X_135))). % 63.13/54.21 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)))). % 63.13/54.21 tff(c_545, plain, (![U_219]: (~of(skc2, U_219, skc3) | ~cannon(skc2, U_219) | ~member(skc2, U_219, skc3)))). % 63.13/54.21 tff(c_543, plain, (skf20(skc3, skc2)!=skf14(skc3, skc2))). % 63.13/54.21 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)))). % 63.13/54.21 tff(c_104, plain, (![V_104, U_103]: (~six(V_104, U_103) | skf20(U_103, V_104)!=skf14(U_103, V_104)))). % 63.13/54.21 tff(c_538, plain, (skf18(skc3, skc2)!=skf16(skc3, skc2))). % 63.13/54.21 tff(c_533, plain, (skf22(skc3, skc2)!=skf14(skc3, skc2))). % 63.13/54.21 tff(c_114, plain, (![V_114, U_113]: (~six(V_114, U_113) | skf18(U_113, V_114)!=skf16(U_113, V_114)))). % 63.13/54.21 tff(c_94, plain, (![V_94, U_93]: (~six(V_94, U_93) | skf22(U_93, V_94)!=skf14(U_93, V_94)))). % 63.13/54.21 tff(c_528, plain, (skf22(skc3, skc2)!=skf12(skc3, skc2))). % 63.13/54.21 tff(c_92, plain, (![V_92, U_91]: (~six(V_92, U_91) | skf22(U_91, V_92)!=skf12(U_91, V_92)))). % 63.13/54.21 tff(c_523, plain, (skf16(skc3, skc2)!=skf14(skc3, skc2))). % 63.13/54.21 tff(c_518, plain, (skf22(skc3, skc2)!=skf16(skc3, skc2))). % 63.13/54.21 tff(c_118, plain, (![V_118, U_117]: (~six(V_118, U_117) | skf16(U_117, V_118)!=skf14(U_117, V_118)))). % 63.13/54.21 tff(c_96, plain, (![V_96, U_95]: (~six(V_96, U_95) | skf22(U_95, V_96)!=skf16(U_95, V_96)))). % 63.13/54.21 tff(c_513, plain, (skf20(skc3, skc2)!=skf12(skc3, skc2))). % 63.13/54.21 tff(c_508, plain, (act(skc2, skf12(skc3, skc2)))). % 63.13/54.21 tff(c_102, plain, (![V_102, U_101]: (~six(V_102, U_101) | skf20(U_101, V_102)!=skf12(U_101, V_102)))). % 63.13/54.21 tff(c_504, plain, (action(skc2, skf12(skc3, skc2)))). % 63.13/54.21 tff(c_500, plain, (shot(skc2, skf12(skc3, skc2)))). % 63.13/54.21 tff(c_90, plain, (![U_89, V_90]: (member(U_89, skf12(V_90, U_89), V_90) | ~six(U_89, V_90)))). % 63.13/54.21 tff(c_486, plain, (![U_37, V_38]: (~act(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.13/54.22 tff(c_491, plain, (skf22(skc3, skc2)!=skf18(skc3, skc2))). % 63.13/54.22 tff(c_98, plain, (![V_98, U_97]: (~six(V_98, U_97) | skf22(U_97, V_98)!=skf18(U_97, V_98)))). % 63.13/54.22 tff(c_470, plain, (![U_7, V_8]: (~entity(U_7, V_8) | ~act(U_7, V_8)))). % 63.13/54.22 tff(c_412, plain, (![U_251, V_252]: (~eventuality(U_251, V_252) | ~group(U_251, V_252)))). % 63.13/54.22 tff(c_476, plain, (skf20(skc3, skc2)!=skf18(skc3, skc2))). % 63.13/54.22 tff(c_108, plain, (![V_108, U_107]: (~six(V_108, U_107) | skf20(U_107, V_108)!=skf18(U_107, V_108)))). % 63.13/54.22 tff(c_397, plain, (![U_55, V_56]: (~artifact(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.13/54.22 tff(c_402, plain, (![U_9, V_10]: (~entity(U_9, V_10) | ~event(U_9, V_10)))). % 63.13/54.22 tff(c_465, plain, (act(skc2, skf16(skc3, skc2)))). % 63.13/54.22 tff(c_461, plain, (action(skc2, skf16(skc3, skc2)))). % 63.13/54.22 tff(c_457, plain, (shot(skc2, skf16(skc3, skc2)))). % 63.31/54.22 tff(c_86, plain, (![U_85, V_86]: (member(U_85, skf16(V_86, U_85), V_86) | ~six(U_85, V_86)))). % 63.31/54.22 tff(c_417, plain, (![U_356, V_357]: (artifact(U_356, V_357) | ~cannon(U_356, V_357)))). % 63.31/54.22 tff(c_444, plain, (skf16(skc3, skc2)!=skf12(skc3, skc2))). % 63.31/54.22 tff(c_439, plain, (~entity(skc2, skc3))). % 63.31/54.22 tff(c_116, plain, (![V_116, U_115]: (~six(V_116, U_115) | skf16(U_115, V_116)!=skf12(U_115, V_116)))). % 63.31/54.22 tff(c_366, plain, (![U_251, V_252]: (~entity(U_251, V_252) | ~group(U_251, V_252)))). % 63.31/54.22 tff(c_355, plain, (![U_334, V_335]: (~animate(U_334, V_335) | ~artifact(U_334, V_335)))). % 63.31/54.22 tff(c_433, plain, (act(skc2, skf18(skc3, skc2)))). % 63.31/54.22 tff(c_429, plain, (action(skc2, skf18(skc3, skc2)))). % 63.31/54.22 tff(c_425, plain, (shot(skc2, skf18(skc3, skc2)))). % 63.31/54.22 tff(c_84, plain, (![U_83, V_84]: (member(U_83, skf18(V_84, U_83), V_84) | ~six(U_83, V_84)))). % 63.31/54.22 tff(c_360, plain, (![U_29, V_30]: (instrumentality(U_29, V_30) | ~cannon(U_29, V_30)))). % 63.31/54.22 tff(c_268, plain, (![U_308, V_309]: (~multiple(U_308, V_309) | ~eventuality(U_308, V_309)))). % 63.31/54.22 tff(c_407, plain, (skf14(skc3, skc2)!=skf12(skc3, skc2))). % 63.31/54.22 tff(c_120, plain, (![V_120, U_119]: (~six(V_120, U_119) | skf14(U_119, V_120)!=skf12(U_119, V_120)))). % 63.31/54.22 tff(c_330, plain, (![U_45, V_46]: (~eventuality(U_45, V_46) | ~entity(U_45, V_46)))). % 63.31/54.22 tff(c_354, plain, (![U_334, V_335]: (~living(U_334, V_335) | ~artifact(U_334, V_335)))). % 63.31/54.22 tff(c_392, plain, (act(skc2, skf22(skc3, skc2)))). % 63.31/54.22 tff(c_388, plain, (action(skc2, skf22(skc3, skc2)))). % 63.31/54.22 tff(c_384, plain, (shot(skc2, skf22(skc3, skc2)))). % 63.31/54.22 tff(c_80, plain, (![U_79, V_80]: (member(U_79, skf22(V_80, U_79), V_80) | ~six(U_79, V_80)))). % 63.31/54.22 tff(c_376, plain, (~artifact(skc2, skc3))). % 63.31/54.22 tff(c_274, plain, (![U_37, V_38]: (~male(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.31/54.22 tff(c_371, plain, (skf22(skc3, skc2)!=skf20(skc3, skc2))). % 63.31/54.22 tff(c_100, plain, (![V_100, U_99]: (~six(V_100, U_99) | skf22(U_99, V_100)!=skf20(U_99, V_100)))). % 63.31/54.22 tff(c_341, plain, (![U_330, V_331]: (~multiple(U_330, V_331) | ~entity(U_330, V_331)))). % 63.31/54.22 tff(c_346, plain, (skf20(skc3, skc2)!=skf16(skc3, skc2))). % 63.31/54.22 tff(c_185, plain, (![U_37, V_38]: (entity(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.31/54.22 tff(c_179, plain, (![U_245, V_246]: (instrumentality(U_245, V_246) | ~weapon(U_245, V_246)))). % 63.31/54.22 tff(c_214, plain, (![U_37, V_38]: (nonliving(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.31/54.22 tff(c_106, plain, (![V_106, U_105]: (~six(V_106, U_105) | skf20(U_105, V_106)!=skf16(U_105, V_106)))). % 63.31/54.22 tff(c_279, plain, (skf18(skc3, skc2)!=skf12(skc3, skc2))). % 63.31/54.22 tff(c_336, plain, (skf18(skc3, skc2)!=skf14(skc3, skc2))). % 63.31/54.22 tff(c_208, plain, (![U_261, V_262]: (singleton(U_261, V_262) | ~entity(U_261, V_262)))). % 63.31/54.22 tff(c_112, plain, (![V_112, U_111]: (~six(V_112, U_111) | skf18(U_111, V_112)!=skf14(U_111, V_112)))). % 63.31/54.22 tff(c_224, plain, (![U_37, V_38]: (impartial(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.31/54.22 tff(c_229, plain, (![U_17, V_18]: (~existent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 63.31/54.22 tff(c_325, plain, (act(skc2, skf14(skc3, skc2)))). % 63.31/54.22 tff(c_321, plain, (action(skc2, skf14(skc3, skc2)))). % 63.31/54.22 tff(c_317, plain, (shot(skc2, skf14(skc3, skc2)))). % 63.31/54.22 tff(c_88, plain, (![U_87, V_88]: (member(U_87, skf14(V_88, U_87), V_88) | ~six(U_87, V_88)))). % 63.31/54.22 tff(c_309, plain, (act(skc2, skf20(skc3, skc2)))). % 63.31/54.22 tff(c_305, plain, (action(skc2, skf20(skc3, skc2)))). % 63.31/54.22 tff(c_301, plain, (shot(skc2, skf20(skc3, skc2)))). % 63.31/54.22 tff(c_82, plain, (![U_81, V_82]: (member(U_81, skf20(V_82, U_81), V_82) | ~six(U_81, V_82)))). % 63.31/54.22 tff(c_190, plain, (![U_251, V_252]: (multiple(U_251, V_252) | ~group(U_251, V_252)))). % 63.31/54.22 tff(c_292, plain, (~act(skc2, skc3))). % 63.31/54.22 tff(c_288, plain, (~event(skc2, skc3))). % 63.31/54.22 tff(c_284, plain, (~eventuality(skc2, skc3))). % 63.31/54.22 tff(c_240, plain, (![U_19, V_20]: (~male(U_19, V_20) | ~eventuality(U_19, V_20)))). % 63.31/54.22 tff(c_110, plain, (![V_110, U_109]: (~six(V_110, U_109) | skf18(U_109, V_110)!=skf12(U_109, V_110)))). % 63.31/54.22 tff(c_239, plain, (![U_51, V_52]: (~male(U_51, V_52) | ~object(U_51, V_52)))). % 63.31/54.22 tff(c_257, plain, (![U_55, V_56]: (living(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.31/54.22 tff(c_203, plain, (![U_259, V_260]: (singleton(U_259, V_260) | ~eventuality(U_259, V_260)))). % 63.31/54.22 tff(c_148, plain, (![U_210]: (shot(skc2, U_210) | ~member(skc2, U_210, skc3)))). % 63.31/54.22 tff(c_252, plain, (![U_55, V_56]: (impartial(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.31/54.22 tff(c_246, plain, (![U_55, V_56]: (entity(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.31/54.22 tff(c_72, plain, (![U_71, V_72]: (~singleton(U_71, V_72) | ~multiple(U_71, V_72)))). % 63.31/54.22 tff(c_64, plain, (![U_63, V_64]: (human(U_63, V_64) | ~human_person(U_63, V_64)))). % 63.31/54.22 tff(c_66, plain, (![U_65, V_66]: (animate(U_65, V_66) | ~human_person(U_65, V_66)))). % 63.31/54.22 tff(c_62, plain, (![U_61, V_62]: (living(U_61, V_62) | ~organism(U_61, V_62)))). % 63.31/54.22 tff(c_60, plain, (![U_59, V_60]: (impartial(U_59, V_60) | ~organism(U_59, V_60)))). % 63.31/54.22 tff(c_74, plain, (![U_73, V_74]: (~nonliving(U_73, V_74) | ~living(U_73, V_74)))). % 63.31/54.22 tff(c_58, plain, (![U_57, V_58]: (entity(U_57, V_58) | ~organism(U_57, V_58)))). % 63.31/54.22 tff(c_68, plain, (![U_67, V_68]: (male(U_67, V_68) | ~man(U_67, V_68)))). % 63.31/54.22 tff(c_70, plain, (![U_69, V_70]: (~unisex(U_69, V_70) | ~male(U_69, V_70)))). % 63.31/54.22 tff(c_54, plain, (![U_53, V_54]: (human_person(U_53, V_54) | ~man(U_53, V_54)))). % 63.31/54.22 tff(c_56, plain, (![U_55, V_56]: (organism(U_55, V_56) | ~human_person(U_55, V_56)))). % 63.31/54.22 tff(c_76, plain, (![U_75, V_76]: (~existent(U_75, V_76) | ~nonexistent(U_75, V_76)))). % 63.31/54.22 tff(c_50, plain, (![U_49, V_50]: (impartial(U_49, V_50) | ~object(U_49, V_50)))). % 63.31/54.22 tff(c_4, plain, (![U_3, V_4]: (action(U_3, V_4) | ~shot(U_3, V_4)))). % 63.31/54.22 tff(c_52, plain, (![U_51, V_52]: (unisex(U_51, V_52) | ~object(U_51, V_52)))). % 63.31/54.22 tff(c_6, plain, (![U_5, V_6]: (act(U_5, V_6) | ~action(U_5, V_6)))). % 63.31/54.22 tff(c_10, plain, (![U_9, V_10]: (eventuality(U_9, V_10) | ~event(U_9, V_10)))). % 63.31/54.22 tff(c_46, plain, (![U_45, V_46]: (existent(U_45, V_46) | ~entity(U_45, V_46)))). % 63.31/54.22 tff(c_48, plain, (![U_47, V_48]: (nonliving(U_47, V_48) | ~object(U_47, V_48)))). % 63.31/54.22 tff(c_78, plain, (![U_77, V_78]: (~animate(U_77, V_78) | ~nonliving(U_77, V_78)))). % 63.31/54.22 tff(c_42, plain, (![U_41, V_42]: (thing(U_41, V_42) | ~entity(U_41, V_42)))). % 63.31/54.22 tff(c_12, plain, (![U_11, V_12]: (thing(U_11, V_12) | ~eventuality(U_11, V_12)))). % 63.31/54.22 tff(c_44, plain, (![U_43, V_44]: (specific(U_43, V_44) | ~entity(U_43, V_44)))). % 63.31/54.23 tff(c_28, plain, (![U_27, V_28]: (event(U_27, V_28) | ~fire(U_27, V_28)))). % 63.31/54.23 tff(c_26, plain, (![U_25, V_26]: (group(U_25, V_26) | ~six(U_25, V_26)))). % 63.31/54.23 tff(c_22, plain, (![U_21, V_22]: (set(U_21, V_22) | ~group(U_21, V_22)))). % 63.31/54.23 tff(c_40, plain, (![U_39, V_40]: (entity(U_39, V_40) | ~object(U_39, V_40)))). % 63.31/54.23 tff(c_30, plain, (![U_29, V_30]: (weapon(U_29, V_30) | ~cannon(U_29, V_30)))). % 63.31/54.23 tff(c_32, plain, (![U_31, V_32]: (weaponry(U_31, V_32) | ~weapon(U_31, V_32)))). % 63.31/54.23 tff(c_34, plain, (![U_33, V_34]: (instrumentality(U_33, V_34) | ~weaponry(U_33, V_34)))). % 63.31/54.23 tff(c_24, plain, (![U_23, V_24]: (multiple(U_23, V_24) | ~set(U_23, V_24)))). % 63.31/54.23 tff(c_16, plain, (![U_15, V_16]: (specific(U_15, V_16) | ~eventuality(U_15, V_16)))). % 63.31/54.23 tff(c_38, plain, (![U_37, V_38]: (object(U_37, V_38) | ~artifact(U_37, V_38)))). % 63.31/54.23 tff(c_20, plain, (![U_19, V_20]: (unisex(U_19, V_20) | ~eventuality(U_19, V_20)))). % 63.31/54.23 tff(c_36, plain, (![U_35, V_36]: (artifact(U_35, V_36) | ~instrumentality(U_35, V_36)))). % 63.31/54.23 tff(c_18, plain, (![U_17, V_18]: (nonexistent(U_17, V_18) | ~eventuality(U_17, V_18)))). % 63.31/54.23 tff(c_14, plain, (![U_13, V_14]: (singleton(U_13, V_14) | ~thing(U_13, V_14)))). % 63.31/54.23 tff(c_8, plain, (![U_7, V_8]: (event(U_7, V_8) | ~act(U_7, V_8)))). % 63.31/54.23 tff(c_2, plain, (![U_1, V_2]: (~member(U_1, V_2, V_2)))). % 63.31/54.23 tff(c_142, plain, (male(skc2, skc3))). % 63.31/54.23 tff(c_146, plain, (group(skc2, skc3))). % 63.31/54.23 tff(c_144, plain, (six(skc2, skc3))). % 63.31/54.23 tff(c_140, plain, (actual_world(skc2))). % 63.31/54.23 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 63.31/54.23 %------------------------------------------------------------------------------