%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SET780-1 : TPTP v9.0.0. Released v2.5.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 08:39:13 PM UTC 2025 % Result : Satisfiable 8.76s 3.11s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET780-1 : TPTP v9.0.0. Released v2.5.0. % 0.03/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.13/0.34 % Computer : n016.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Apr 8 21:37:09 EDT 2025 % 0.13/0.34 % CPUTime : % 8.76/3.11 % 8.76/3.11 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.76/3.11 % 8.76/3.11 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.76/3.12 %$ difference > subset > member > equal_sets > k > member_of_1_not_of_2 > #nlpp % 8.76/3.12 % 8.76/3.12 %Foreground sorts: % 8.76/3.12 % 8.76/3.12 % 8.76/3.12 %Background operators: % 8.76/3.12 % 8.76/3.12 % 8.76/3.12 %Foreground operators: % 8.76/3.12 tff(member_of_1_not_of_2, type, member_of_1_not_of_2: ($i * $i) > $i). % 8.76/3.12 tff(k, type, k: ($i * $i * $i) > $i). % 8.76/3.12 tff(subset, type, subset: ($i * $i) > $o). % 8.76/3.12 tff(member, type, member: ($i * $i) > $o). % 8.76/3.12 tff(difference, type, difference: ($i * $i * $i) > $o). % 8.76/3.12 tff(equal_sets, type, equal_sets: ($i * $i) > $o). % 8.76/3.12 % 8.76/3.12 %Saturated clause set: % 8.76/3.12 tff(c_1906, plain, (![Set1_14, Superset_483, Set1_481, Set2_15, Set2_480, Superset_482, Difference_479]: (member(k(Set1_481, Set2_480, Difference_479), Set1_14) | ~difference(Set1_14, Set2_15, Superset_482) | member(k(Set1_481, Set2_480, Difference_479), Superset_483) | ~equal_sets(Set1_481, Superset_483) | ~equal_sets(Superset_482, Difference_479) | difference(Set1_481, Set2_480, Difference_479)))). % 8.76/3.12 tff(c_2089, plain, (![Set1_14, Set2_649, Set1_647, Superset_651, Difference_648, Set2_15, Superset_650]: (member(k(Set1_647, Set2_649, Difference_648), Set1_14) | ~difference(Set1_14, Set2_15, Superset_650) | member(k(Set1_647, Set2_649, Difference_648), Superset_651) | ~equal_sets(Set1_647, Superset_651) | ~equal_sets(Difference_648, Superset_650) | difference(Set1_647, Set2_649, Difference_648)))). % 8.76/3.12 tff(c_2407, plain, (![Set1_14, Set1_823, Difference_821, Set2_15, Superset_819, Set2_822, Superset_820]: (member(k(Set1_823, Set2_822, Difference_821), Set1_14) | ~difference(Set1_14, Set2_15, Superset_819) | member(k(Set1_823, Set2_822, Difference_821), Superset_820) | ~equal_sets(Superset_820, Difference_821) | ~equal_sets(Set1_823, Superset_819) | difference(Set1_823, Set2_822, Difference_821)))). % 8.76/3.12 tff(c_1381, plain, (![Set1_14, Difference_390, Superset_392, Set1_388, Superset_389, Set2_391, Set2_15]: (member(k(Set1_388, Set2_391, Difference_390), Set1_14) | ~difference(Set1_14, Set2_15, Superset_389) | ~equal_sets(Superset_389, Difference_390) | member(k(Set1_388, Set2_391, Difference_390), Superset_392) | ~equal_sets(Superset_392, Set1_388) | difference(Set1_388, Set2_391, Difference_390)))). % 8.76/3.12 tff(c_2084, plain, (![Set1_14, Set2_649, Set1_647, Superset_651, Difference_648, Set2_15, Superset_650]: (member(k(Set1_647, Set2_649, Difference_648), Set1_14) | ~difference(Set1_14, Set2_15, Superset_651) | ~equal_sets(Set1_647, Superset_651) | member(k(Set1_647, Set2_649, Difference_648), Superset_650) | ~equal_sets(Difference_648, Superset_650) | difference(Set1_647, Set2_649, Difference_648)))). % 8.76/3.12 tff(c_1709, plain, (![Set2_409, Set1_411, Superset_9, Superset_410, Superset_407, Difference_408]: (member(k(Set1_411, Set2_409, Difference_408), Superset_9) | ~equal_sets(Superset_407, Superset_9) | member(k(Set1_411, Set2_409, Difference_408), Superset_410) | ~equal_sets(Difference_408, Superset_410) | ~equal_sets(Set1_411, Superset_407) | difference(Set1_411, Set2_409, Difference_408)))). % 8.76/3.13 tff(c_1382, plain, (![Difference_390, Superset_10, Superset_392, Set1_388, Superset_389, Set2_391]: (member(k(Set1_388, Set2_391, Difference_390), Superset_10) | ~equal_sets(Superset_10, Superset_389) | ~equal_sets(Superset_389, Difference_390) | member(k(Set1_388, Set2_391, Difference_390), Superset_392) | ~equal_sets(Superset_392, Set1_388) | difference(Set1_388, Set2_391, Difference_390)))). % 8.76/3.13 tff(c_2179, plain, (![Superset_697, Superset_9, Difference_695, Set1_693, Set2_696, Superset_694]: (member(k(Set1_693, Set2_696, Difference_695), Superset_9) | ~equal_sets(Superset_694, Superset_9) | ~equal_sets(Superset_694, Set1_693) | member(k(Set1_693, Set2_696, Difference_695), Superset_697) | ~equal_sets(Difference_695, Superset_697) | difference(Set1_693, Set2_696, Difference_695)))). % 8.76/3.13 tff(c_1810, plain, (![Set1_14, Superset_447, Set2_446, Superset_449, Difference_445, Set1_448, Set2_15]: (member(k(Set1_448, Set2_446, Difference_445), Set1_14) | ~difference(Set1_14, Set2_15, Superset_447) | ~equal_sets(Superset_447, Set1_448) | member(k(Set1_448, Set2_446, Difference_445), Superset_449) | ~equal_sets(Superset_449, Difference_445) | difference(Set1_448, Set2_446, Difference_445)))). % 8.76/3.13 tff(c_2401, plain, (![Superset_10, Set1_823, Difference_821, Superset_819, Set2_822, Superset_820]: (member(k(Set1_823, Set2_822, Difference_821), Superset_10) | ~equal_sets(Superset_10, Superset_820) | ~equal_sets(Superset_820, Difference_821) | member(k(Set1_823, Set2_822, Difference_821), Superset_819) | ~equal_sets(Set1_823, Superset_819) | difference(Set1_823, Set2_822, Difference_821)))). % 8.76/3.13 tff(c_2402, plain, (![Superset_9, Set1_823, Difference_821, Superset_819, Set2_822, Superset_820]: (member(k(Set1_823, Set2_822, Difference_821), Superset_9) | ~equal_sets(Superset_820, Superset_9) | ~equal_sets(Superset_820, Difference_821) | member(k(Set1_823, Set2_822, Difference_821), Superset_819) | ~equal_sets(Set1_823, Superset_819) | difference(Set1_823, Set2_822, Difference_821)))). % 8.76/3.13 tff(c_1902, plain, (![Superset_10, Superset_483, Set1_481, Set2_480, Superset_482, Difference_479]: (member(k(Set1_481, Set2_480, Difference_479), Superset_10) | ~equal_sets(Superset_10, Superset_483) | ~equal_sets(Set1_481, Superset_483) | member(k(Set1_481, Set2_480, Difference_479), Superset_482) | ~equal_sets(Superset_482, Difference_479) | difference(Set1_481, Set2_480, Difference_479)))). % 8.76/3.13 tff(c_2184, plain, (![Superset_697, Superset_9, Difference_695, Set1_693, Set2_696, Superset_694]: (member(k(Set1_693, Set2_696, Difference_695), Superset_9) | ~equal_sets(Superset_697, Superset_9) | member(k(Set1_693, Set2_696, Difference_695), Superset_694) | ~equal_sets(Superset_694, Set1_693) | ~equal_sets(Difference_695, Superset_697) | difference(Set1_693, Set2_696, Difference_695)))). % 8.76/3.13 tff(c_1903, plain, (![Superset_9, Superset_483, Set1_481, Set2_480, Superset_482, Difference_479]: (member(k(Set1_481, Set2_480, Difference_479), Superset_9) | ~equal_sets(Superset_483, Superset_9) | ~equal_sets(Set1_481, Superset_483) | member(k(Set1_481, Set2_480, Difference_479), Superset_482) | ~equal_sets(Superset_482, Difference_479) | difference(Set1_481, Set2_480, Difference_479)))). % 8.76/3.13 tff(c_2276, plain, (![Set1_14, Set1_806, Set2_15, Set2_808, Superset_809, Difference_807, Superset_810]: (member(k(Set1_806, Set2_808, Difference_807), Set1_14) | ~difference(Set1_14, Set2_15, Superset_810) | ~equal_sets(Difference_807, Superset_810) | member(k(Set1_806, Set2_808, Difference_807), Superset_809) | ~equal_sets(Superset_809, Set1_806) | difference(Set1_806, Set2_808, Difference_807)))). % 8.76/3.13 tff(c_1811, plain, (![Superset_447, Set2_446, Superset_10, Superset_449, Difference_445, Set1_448]: (member(k(Set1_448, Set2_446, Difference_445), Superset_10) | ~equal_sets(Superset_10, Superset_447) | ~equal_sets(Superset_447, Set1_448) | member(k(Set1_448, Set2_446, Difference_445), Superset_449) | ~equal_sets(Superset_449, Difference_445) | difference(Set1_448, Set2_446, Difference_445)))). % 8.76/3.13 tff(c_2090, plain, (![Superset_10, Set2_649, Set1_647, Superset_651, Difference_648, Superset_650]: (member(k(Set1_647, Set2_649, Difference_648), Superset_10) | ~equal_sets(Superset_10, Superset_650) | member(k(Set1_647, Set2_649, Difference_648), Superset_651) | ~equal_sets(Set1_647, Superset_651) | ~equal_sets(Difference_648, Superset_650) | difference(Set1_647, Set2_649, Difference_648)))). % 8.76/3.13 tff(c_2085, plain, (![Superset_10, Set2_649, Set1_647, Superset_651, Difference_648, Superset_650]: (member(k(Set1_647, Set2_649, Difference_648), Superset_10) | ~equal_sets(Superset_10, Superset_651) | ~equal_sets(Set1_647, Superset_651) | member(k(Set1_647, Set2_649, Difference_648), Superset_650) | ~equal_sets(Difference_648, Superset_650) | difference(Set1_647, Set2_649, Difference_648)))). % 8.76/3.13 tff(c_1812, plain, (![Superset_447, Set2_446, Superset_9, Superset_449, Difference_445, Set1_448]: (member(k(Set1_448, Set2_446, Difference_445), Superset_9) | ~equal_sets(Superset_447, Superset_9) | ~equal_sets(Superset_447, Set1_448) | member(k(Set1_448, Set2_446, Difference_445), Superset_449) | ~equal_sets(Superset_449, Difference_445) | difference(Set1_448, Set2_446, Difference_445)))). % 8.76/3.13 tff(c_2277, plain, (![Superset_10, Set1_806, Set2_808, Superset_809, Difference_807, Superset_810]: (member(k(Set1_806, Set2_808, Difference_807), Superset_10) | ~equal_sets(Superset_10, Superset_810) | ~equal_sets(Difference_807, Superset_810) | member(k(Set1_806, Set2_808, Difference_807), Superset_809) | ~equal_sets(Superset_809, Set1_806) | difference(Set1_806, Set2_808, Difference_807)))). % 8.76/3.13 tff(c_1383, plain, (![Difference_390, Superset_9, Superset_392, Set1_388, Superset_389, Set2_391]: (member(k(Set1_388, Set2_391, Difference_390), Superset_9) | ~equal_sets(Superset_389, Superset_9) | ~equal_sets(Superset_389, Difference_390) | member(k(Set1_388, Set2_391, Difference_390), Superset_392) | ~equal_sets(Superset_392, Set1_388) | difference(Set1_388, Set2_391, Difference_390)))). % 8.76/3.13 tff(c_2178, plain, (![Superset_697, Superset_10, Difference_695, Set1_693, Set2_696, Superset_694]: (member(k(Set1_693, Set2_696, Difference_695), Superset_10) | ~equal_sets(Superset_10, Superset_694) | ~equal_sets(Superset_694, Set1_693) | member(k(Set1_693, Set2_696, Difference_695), Superset_697) | ~equal_sets(Difference_695, Superset_697) | difference(Set1_693, Set2_696, Difference_695)))). % 8.76/3.13 tff(c_2091, plain, (![Superset_9, Set2_649, Set1_647, Superset_651, Difference_648, Superset_650]: (member(k(Set1_647, Set2_649, Difference_648), Superset_9) | ~equal_sets(Superset_650, Superset_9) | member(k(Set1_647, Set2_649, Difference_648), Superset_651) | ~equal_sets(Set1_647, Superset_651) | ~equal_sets(Difference_648, Superset_650) | difference(Set1_647, Set2_649, Difference_648)))). % 8.92/3.13 tff(c_2283, plain, (![Set1_14, Set1_806, Set2_15, Set2_808, Superset_809, Difference_807, Superset_810]: (member(k(Set1_806, Set2_808, Difference_807), Set1_14) | ~difference(Set1_14, Set2_15, Superset_809) | member(k(Set1_806, Set2_808, Difference_807), Superset_810) | ~equal_sets(Difference_807, Superset_810) | ~equal_sets(Superset_809, Set1_806) | difference(Set1_806, Set2_808, Difference_807)))). % 8.92/3.13 tff(c_776, plain, (![Set1_14, Difference_269, Set1_267, Set2_268, Set2_15, Superset_270]: (member(k(Set1_267, Set2_268, Difference_269), Set1_14) | ~difference(Set1_14, Set2_15, Difference_269) | member(k(Set1_267, Set2_268, Difference_269), Superset_270) | ~equal_sets(Superset_270, Set1_267) | difference(Set1_267, Set2_268, Difference_269)))). % 8.92/3.13 tff(c_632, plain, (![Set1_14, Difference_235, Superset_236, Set2_15, Set1_233, Set2_234]: (member(k(Set1_233, Set2_234, Difference_235), Set1_14) | ~difference(Set1_14, Set2_15, Set1_233) | member(k(Set1_233, Set2_234, Difference_235), Superset_236) | ~equal_sets(Difference_235, Superset_236) | difference(Set1_233, Set2_234, Difference_235)))). % 8.92/3.13 tff(c_771, plain, (![Set1_14, Difference_269, Set1_267, Set2_268, Set2_15, Superset_270]: (member(k(Set1_267, Set2_268, Difference_269), Set1_14) | ~difference(Set1_14, Set2_15, Superset_270) | ~equal_sets(Superset_270, Set1_267) | member(k(Set1_267, Set2_268, Difference_269), Difference_269) | difference(Set1_267, Set2_268, Difference_269)))). % 8.92/3.13 tff(c_933, plain, (![Set1_14, Set1_303, Set2_304, Difference_305, Set2_15, Superset_306]: (member(k(Set1_303, Set2_304, Difference_305), Set1_14) | ~difference(Set1_14, Set2_15, Set1_303) | member(k(Set1_303, Set2_304, Difference_305), Superset_306) | ~equal_sets(Superset_306, Difference_305) | difference(Set1_303, Set2_304, Difference_305)))). % 8.92/3.13 tff(c_472, plain, (![Set1_14, Set1_198, Superset_201, Difference_200, Set2_199, Set2_15]: (member(k(Set1_198, Set2_199, Difference_200), Set1_14) | ~difference(Set1_14, Set2_15, Difference_200) | member(k(Set1_198, Set2_199, Difference_200), Superset_201) | ~equal_sets(Set1_198, Superset_201) | difference(Set1_198, Set2_199, Difference_200)))). % 8.92/3.13 tff(c_928, plain, (![Set1_14, Set1_303, Set2_304, Difference_305, Set2_15, Superset_306]: (member(k(Set1_303, Set2_304, Difference_305), Set1_14) | ~difference(Set1_14, Set2_15, Superset_306) | ~equal_sets(Superset_306, Difference_305) | member(k(Set1_303, Set2_304, Difference_305), Set1_303) | difference(Set1_303, Set2_304, Difference_305)))). % 8.92/3.13 tff(c_627, plain, (![Set1_14, Difference_235, Superset_236, Set2_15, Set1_233, Set2_234]: (member(k(Set1_233, Set2_234, Difference_235), Set1_14) | ~difference(Set1_14, Set2_15, Superset_236) | ~equal_sets(Difference_235, Superset_236) | member(k(Set1_233, Set2_234, Difference_235), Set1_233) | difference(Set1_233, Set2_234, Difference_235)))). % 8.92/3.13 tff(c_467, plain, (![Set1_14, Set1_198, Superset_201, Difference_200, Set2_199, Set2_15]: (member(k(Set1_198, Set2_199, Difference_200), Set1_14) | ~difference(Set1_14, Set2_15, Superset_201) | ~equal_sets(Set1_198, Superset_201) | member(k(Set1_198, Set2_199, Difference_200), Difference_200) | difference(Set1_198, Set2_199, Difference_200)))). % 8.92/3.13 tff(c_1905, plain, (![Set1_481, Superset_482, Difference_479, Superset_483]: (member(k(Set1_481, Superset_482, Difference_479), Difference_479) | member(k(Set1_481, Superset_482, Difference_479), Superset_483) | ~equal_sets(Set1_481, Superset_483) | ~equal_sets(Superset_482, Difference_479) | difference(Set1_481, Superset_482, Difference_479)))). % 8.92/3.14 tff(c_2088, plain, (![Set1_647, Superset_650, Difference_648, Superset_651]: (member(k(Set1_647, Superset_650, Difference_648), Difference_648) | member(k(Set1_647, Superset_650, Difference_648), Superset_651) | ~equal_sets(Set1_647, Superset_651) | ~equal_sets(Difference_648, Superset_650) | difference(Set1_647, Superset_650, Difference_648)))). % 8.92/3.14 tff(c_1380, plain, (![Set1_388, Superset_389, Difference_390, Superset_392]: (member(k(Set1_388, Superset_389, Difference_390), Difference_390) | ~equal_sets(Superset_389, Difference_390) | member(k(Set1_388, Superset_389, Difference_390), Superset_392) | ~equal_sets(Superset_392, Set1_388) | difference(Set1_388, Superset_389, Difference_390)))). % 8.92/3.14 tff(c_469, plain, (![Set1_198, Superset_201, Superset_9, Difference_200, Set2_199]: (member(k(Set1_198, Set2_199, Difference_200), Superset_9) | ~equal_sets(Superset_201, Superset_9) | ~equal_sets(Set1_198, Superset_201) | member(k(Set1_198, Set2_199, Difference_200), Difference_200) | difference(Set1_198, Set2_199, Difference_200)))). % 8.92/3.14 tff(c_629, plain, (![Superset_9, Difference_235, Superset_236, Set1_233, Set2_234]: (member(k(Set1_233, Set2_234, Difference_235), Superset_9) | ~equal_sets(Superset_236, Superset_9) | ~equal_sets(Difference_235, Superset_236) | member(k(Set1_233, Set2_234, Difference_235), Set1_233) | difference(Set1_233, Set2_234, Difference_235)))). % 8.92/3.14 tff(c_2371, plain, (![Superset_10, Difference_200, Set1_198, Set2_199]: (~equal_sets(Superset_10, Difference_200) | ~equal_sets(Set1_198, Superset_10) | difference(Set1_198, Set2_199, Difference_200) | member(k(Set1_198, Set2_199, Difference_200), Superset_10)))). % 8.92/3.14 tff(c_473, plain, (![Set1_198, Superset_201, Superset_10, Difference_200, Set2_199]: (member(k(Set1_198, Set2_199, Difference_200), Superset_10) | ~equal_sets(Superset_10, Difference_200) | member(k(Set1_198, Set2_199, Difference_200), Superset_201) | ~equal_sets(Set1_198, Superset_201) | difference(Set1_198, Set2_199, Difference_200)))). % 8.92/3.14 tff(c_2247, plain, (![Difference_269, Superset_9, Set1_267, Set2_268]: (~equal_sets(Difference_269, Superset_9) | ~equal_sets(Superset_9, Set1_267) | difference(Set1_267, Set2_268, Difference_269) | member(k(Set1_267, Set2_268, Difference_269), Superset_9)))). % 8.92/3.14 tff(c_2181, plain, (![Set1_693, Superset_697, Difference_695, Superset_694]: (member(k(Set1_693, Superset_697, Difference_695), Difference_695) | member(k(Set1_693, Superset_697, Difference_695), Superset_694) | ~equal_sets(Superset_694, Set1_693) | ~equal_sets(Difference_695, Superset_697) | difference(Set1_693, Superset_697, Difference_695)))). % 8.92/3.14 tff(c_778, plain, (![Superset_9, Difference_269, Set1_267, Set2_268, Superset_270]: (member(k(Set1_267, Set2_268, Difference_269), Superset_9) | ~equal_sets(Difference_269, Superset_9) | member(k(Set1_267, Set2_268, Difference_269), Superset_270) | ~equal_sets(Superset_270, Set1_267) | difference(Set1_267, Set2_268, Difference_269)))). % 8.92/3.14 tff(c_1317, plain, (![Set2_381, Set1_14, Set1_380, Superset_383, Set2_15, Superset_382]: (member(k(Set1_380, Set2_381, Superset_382), Set1_14) | ~difference(Set1_14, Set2_15, Superset_383) | ~equal_sets(Superset_383, Set2_381) | ~equal_sets(Superset_382, Set1_380) | difference(Set1_380, Set2_381, Superset_382)))). % 8.92/3.14 tff(c_1747, plain, (![Set1_14, Superset_419, Superset_416, Set2_15, Superset_418, Set2_417]: (member(k(Superset_416, Set2_417, Superset_418), Set1_14) | ~difference(Set1_14, Set2_15, Superset_419) | ~equal_sets(Set2_417, Superset_419) | ~equal_sets(Superset_416, Superset_418) | difference(Superset_416, Set2_417, Superset_418)))). % 8.92/3.14 tff(c_773, plain, (![Superset_9, Difference_269, Set1_267, Set2_268, Superset_270]: (member(k(Set1_267, Set2_268, Difference_269), Superset_9) | ~equal_sets(Superset_270, Superset_9) | ~equal_sets(Superset_270, Set1_267) | member(k(Set1_267, Set2_268, Difference_269), Difference_269) | difference(Set1_267, Set2_268, Difference_269)))). % 8.92/3.14 tff(c_1656, plain, (![Set1_14, Set2_404, Superset_405, Superset_403, Set2_15, Superset_406]: (member(k(Superset_403, Set2_404, Superset_405), Set1_14) | ~difference(Set1_14, Set2_15, Superset_406) | ~equal_sets(Superset_406, Set2_404) | ~equal_sets(Superset_403, Superset_405) | difference(Superset_403, Set2_404, Superset_405)))). % 8.92/3.14 tff(c_1337, plain, (![Set1_14, Set2_385, Set1_384, Superset_386, Set2_15, Superset_387]: (member(k(Set1_384, Set2_385, Superset_386), Set1_14) | ~difference(Set1_14, Set2_15, Superset_387) | ~equal_sets(Set2_385, Superset_387) | ~equal_sets(Superset_386, Set1_384) | difference(Set1_384, Set2_385, Superset_386)))). % 8.92/3.14 tff(c_851, plain, (![Set1_14, Superset_287, Superset_289, Set2_15, Difference_288, Set1_286]: (member(k(Set1_286, Superset_287, Difference_288), Set1_14) | ~difference(Set1_14, Set2_15, Superset_289) | ~equal_sets(Difference_288, Superset_289) | ~equal_sets(Superset_287, Set1_286) | difference(Set1_286, Superset_287, Difference_288)))). % 8.92/3.14 tff(c_533, plain, (![Set1_14, Superset_218, Difference_219, Set1_217, Superset_220, Set2_15]: (member(k(Set1_217, Superset_218, Difference_219), Set1_14) | ~difference(Set1_14, Set2_15, Superset_220) | ~equal_sets(Superset_220, Difference_219) | ~equal_sets(Set1_217, Superset_218) | difference(Set1_217, Superset_218, Difference_219)))). % 8.92/3.14 tff(c_551, plain, (![Set1_14, Set2_222, Set1_221, Superset_223, Set2_15, Superset_224]: (member(k(Set1_221, Set2_222, Superset_223), Set1_14) | ~difference(Set1_14, Set2_15, Superset_224) | ~equal_sets(Superset_223, Superset_224) | ~equal_sets(Set1_221, Superset_223) | difference(Set1_221, Set2_222, Superset_223)))). % 8.92/3.14 tff(c_569, plain, (![Set1_14, Superset_227, Set1_225, Set2_226, Set2_15, Superset_228]: (member(k(Set1_225, Set2_226, Superset_227), Set1_14) | ~difference(Set1_14, Set2_15, Superset_228) | ~equal_sets(Superset_228, Superset_227) | ~equal_sets(Set1_225, Superset_227) | difference(Set1_225, Set2_226, Superset_227)))). % 8.92/3.14 tff(c_833, plain, (![Set1_14, Superset_284, Set2_15, Set2_283, Set1_282, Superset_285]: (member(k(Set1_282, Set2_283, Superset_284), Set1_14) | ~difference(Set1_14, Set2_15, Superset_285) | ~equal_sets(Superset_285, Superset_284) | ~equal_sets(Superset_284, Set1_282) | difference(Set1_282, Set2_283, Superset_284)))). % 8.92/3.14 tff(c_869, plain, (![Set1_14, Superset_291, Difference_292, Set1_290, Superset_293, Set2_15]: (member(k(Set1_290, Superset_291, Difference_292), Set1_14) | ~difference(Set1_14, Set2_15, Superset_293) | ~equal_sets(Superset_293, Difference_292) | ~equal_sets(Superset_291, Set1_290) | difference(Set1_290, Superset_291, Difference_292)))). % 8.92/3.14 tff(c_468, plain, (![Set1_198, Superset_201, Superset_10, Difference_200, Set2_199]: (member(k(Set1_198, Set2_199, Difference_200), Superset_10) | ~equal_sets(Superset_10, Superset_201) | ~equal_sets(Set1_198, Superset_201) | member(k(Set1_198, Set2_199, Difference_200), Difference_200) | difference(Set1_198, Set2_199, Difference_200)))). % 8.92/3.14 tff(c_887, plain, (![Set1_14, Superset_297, Set2_295, Set1_294, Set2_15, Superset_296]: (member(k(Set1_294, Set2_295, Superset_296), Set1_14) | ~difference(Set1_14, Set2_15, Superset_297) | ~equal_sets(Superset_296, Superset_297) | ~equal_sets(Superset_296, Set1_294) | difference(Set1_294, Set2_295, Superset_296)))). % 8.92/3.14 tff(c_2202, plain, (![Set1_14, Set1_699, Set2_15, Difference_700, Superset_698, Set2_701]: (member(k(Set1_699, Set2_701, Difference_700), Set1_14) | ~difference(Set1_14, Set2_15, Superset_698) | ~equal_sets(Superset_698, Set1_699) | ~equal_sets(Difference_700, Superset_698) | difference(Set1_699, Set2_701, Difference_700)))). % 8.92/3.14 tff(c_587, plain, (![Set1_14, Difference_231, Superset_230, Superset_232, Set1_229, Set2_15]: (member(k(Set1_229, Superset_230, Difference_231), Set1_14) | ~difference(Set1_14, Set2_15, Superset_232) | ~equal_sets(Difference_231, Superset_232) | ~equal_sets(Set1_229, Superset_230) | difference(Set1_229, Superset_230, Difference_231)))). % 8.92/3.14 tff(c_2204, plain, (![Set1_699, Superset_9, Difference_700, Superset_698, Set2_701]: (member(k(Set1_699, Set2_701, Difference_700), Superset_9) | ~equal_sets(Superset_698, Superset_9) | ~equal_sets(Superset_698, Set1_699) | ~equal_sets(Difference_700, Superset_698) | difference(Set1_699, Set2_701, Difference_700)))). % 8.92/3.14 tff(c_991, plain, (![Set1_14, Superset_319, Superset_322, Set2_15, Set2_320, Difference_321]: (member(k(Superset_319, Set2_320, Difference_321), Set1_14) | ~difference(Set1_14, Set2_15, Superset_322) | ~equal_sets(Superset_319, Superset_322) | ~equal_sets(Superset_319, Difference_321) | difference(Superset_319, Set2_320, Difference_321)))). % 8.92/3.14 tff(c_2203, plain, (![Set1_699, Superset_10, Difference_700, Superset_698, Set2_701]: (member(k(Set1_699, Set2_701, Difference_700), Superset_10) | ~equal_sets(Superset_10, Superset_698) | ~equal_sets(Superset_698, Set1_699) | ~equal_sets(Difference_700, Superset_698) | difference(Set1_699, Set2_701, Difference_700)))). % 8.92/3.14 tff(c_2146, plain, (![Superset_10, Set1_233, Difference_235, Set2_234]: (~equal_sets(Superset_10, Set1_233) | ~equal_sets(Difference_235, Superset_10) | difference(Set1_233, Set2_234, Difference_235) | member(k(Set1_233, Set2_234, Difference_235), Superset_10)))). % 8.92/3.14 tff(c_633, plain, (![Superset_10, Difference_235, Superset_236, Set1_233, Set2_234]: (member(k(Set1_233, Set2_234, Difference_235), Superset_10) | ~equal_sets(Superset_10, Set1_233) | member(k(Set1_233, Set2_234, Difference_235), Superset_236) | ~equal_sets(Difference_235, Superset_236) | difference(Set1_233, Set2_234, Difference_235)))). % 8.92/3.14 tff(c_1926, plain, (![Set1_14, Difference_486, Set2_487, Set2_15, Set1_484, Superset_485]: (member(k(Set1_484, Set2_487, Difference_486), Set1_14) | ~difference(Set1_14, Set2_15, Superset_485) | ~equal_sets(Set1_484, Superset_485) | ~equal_sets(Superset_485, Difference_486) | difference(Set1_484, Set2_487, Difference_486)))). % 8.92/3.14 tff(c_1339, plain, (![Set2_385, Superset_9, Set1_384, Superset_386, Superset_387]: (member(k(Set1_384, Set2_385, Superset_386), Superset_9) | ~equal_sets(Superset_387, Superset_9) | ~equal_sets(Set2_385, Superset_387) | ~equal_sets(Superset_386, Set1_384) | difference(Set1_384, Set2_385, Superset_386)))). % 8.92/3.14 tff(c_1338, plain, (![Set2_385, Superset_10, Set1_384, Superset_386, Superset_387]: (member(k(Set1_384, Set2_385, Superset_386), Superset_10) | ~equal_sets(Superset_10, Superset_387) | ~equal_sets(Set2_385, Superset_387) | ~equal_sets(Superset_386, Set1_384) | difference(Set1_384, Set2_385, Superset_386)))). % 8.92/3.14 tff(c_1657, plain, (![Set2_404, Superset_405, Superset_10, Superset_403, Superset_406]: (member(k(Superset_403, Set2_404, Superset_405), Superset_10) | ~equal_sets(Superset_10, Superset_406) | ~equal_sets(Superset_406, Set2_404) | ~equal_sets(Superset_403, Superset_405) | difference(Superset_403, Set2_404, Superset_405)))). % 8.92/3.14 tff(c_1749, plain, (![Superset_9, Superset_419, Superset_416, Superset_418, Set2_417]: (member(k(Superset_416, Set2_417, Superset_418), Superset_9) | ~equal_sets(Superset_419, Superset_9) | ~equal_sets(Set2_417, Superset_419) | ~equal_sets(Superset_416, Superset_418) | difference(Superset_416, Set2_417, Superset_418)))). % 8.92/3.14 tff(c_669, plain, (![Set1_14, Difference_242, Set2_15, Set2_241, Superset_240, Superset_243]: (member(k(Superset_240, Set2_241, Difference_242), Set1_14) | ~difference(Set1_14, Set2_15, Superset_243) | ~equal_sets(Superset_243, Superset_240) | ~equal_sets(Difference_242, Superset_240) | difference(Superset_240, Set2_241, Difference_242)))). % 8.92/3.14 tff(c_1319, plain, (![Set2_381, Superset_9, Set1_380, Superset_383, Superset_382]: (member(k(Set1_380, Set2_381, Superset_382), Superset_9) | ~equal_sets(Superset_383, Superset_9) | ~equal_sets(Superset_383, Set2_381) | ~equal_sets(Superset_382, Set1_380) | difference(Set1_380, Set2_381, Superset_382)))). % 8.92/3.14 tff(c_2053, plain, (![Set1_233, Superset_9, Difference_235, Set2_234]: (~equal_sets(Set1_233, Superset_9) | ~equal_sets(Difference_235, Superset_9) | difference(Set1_233, Set2_234, Difference_235) | member(k(Set1_233, Set2_234, Difference_235), Superset_9)))). % 8.92/3.14 tff(c_634, plain, (![Superset_9, Difference_235, Superset_236, Set1_233, Set2_234]: (member(k(Set1_233, Set2_234, Difference_235), Superset_9) | ~equal_sets(Set1_233, Superset_9) | member(k(Set1_233, Set2_234, Difference_235), Superset_236) | ~equal_sets(Difference_235, Superset_236) | difference(Set1_233, Set2_234, Difference_235)))). % 8.92/3.14 tff(c_1748, plain, (![Superset_10, Superset_419, Superset_416, Superset_418, Set2_417]: (member(k(Superset_416, Set2_417, Superset_418), Superset_10) | ~equal_sets(Superset_10, Superset_419) | ~equal_sets(Set2_417, Superset_419) | ~equal_sets(Superset_416, Superset_418) | difference(Superset_416, Set2_417, Superset_418)))). % 8.92/3.14 tff(c_1658, plain, (![Set2_404, Superset_405, Superset_9, Superset_403, Superset_406]: (member(k(Superset_403, Set2_404, Superset_405), Superset_9) | ~equal_sets(Superset_406, Superset_9) | ~equal_sets(Superset_406, Set2_404) | ~equal_sets(Superset_403, Superset_405) | difference(Superset_403, Set2_404, Superset_405)))). % 8.92/3.14 tff(c_1318, plain, (![Set2_381, Superset_10, Set1_380, Superset_383, Superset_382]: (member(k(Set1_380, Set2_381, Superset_382), Superset_10) | ~equal_sets(Superset_10, Superset_383) | ~equal_sets(Superset_383, Set2_381) | ~equal_sets(Superset_382, Set1_380) | difference(Set1_380, Set2_381, Superset_382)))). % 8.92/3.14 tff(c_709, plain, (![Set1_14, Set2_248, Superset_250, Superset_247, Set2_15, Difference_249]: (member(k(Superset_247, Set2_248, Difference_249), Set1_14) | ~difference(Set1_14, Set2_15, Superset_250) | ~equal_sets(Superset_247, Superset_250) | ~equal_sets(Difference_249, Superset_247) | difference(Superset_247, Set2_248, Difference_249)))). % 8.92/3.14 tff(c_888, plain, (![Superset_10, Superset_297, Set2_295, Set1_294, Superset_296]: (member(k(Set1_294, Set2_295, Superset_296), Superset_10) | ~equal_sets(Superset_10, Superset_297) | ~equal_sets(Superset_296, Superset_297) | ~equal_sets(Superset_296, Set1_294) | difference(Set1_294, Set2_295, Superset_296)))). % 8.92/3.14 tff(c_670, plain, (![Superset_10, Difference_242, Set2_241, Superset_240, Superset_243]: (member(k(Superset_240, Set2_241, Difference_242), Superset_10) | ~equal_sets(Superset_10, Superset_243) | ~equal_sets(Superset_243, Superset_240) | ~equal_sets(Difference_242, Superset_240) | difference(Superset_240, Set2_241, Difference_242)))). % 8.92/3.14 tff(c_871, plain, (![Superset_9, Superset_291, Difference_292, Set1_290, Superset_293]: (member(k(Set1_290, Superset_291, Difference_292), Superset_9) | ~equal_sets(Superset_293, Superset_9) | ~equal_sets(Superset_293, Difference_292) | ~equal_sets(Superset_291, Set1_290) | difference(Set1_290, Superset_291, Difference_292)))). % 8.92/3.14 tff(c_929, plain, (![Set1_303, Superset_10, Set2_304, Difference_305, Superset_306]: (member(k(Set1_303, Set2_304, Difference_305), Superset_10) | ~equal_sets(Superset_10, Superset_306) | ~equal_sets(Superset_306, Difference_305) | member(k(Set1_303, Set2_304, Difference_305), Set1_303) | difference(Set1_303, Set2_304, Difference_305)))). % 8.92/3.14 tff(c_553, plain, (![Set2_222, Set1_221, Superset_223, Superset_9, Superset_224]: (member(k(Set1_221, Set2_222, Superset_223), Superset_9) | ~equal_sets(Superset_224, Superset_9) | ~equal_sets(Superset_223, Superset_224) | ~equal_sets(Set1_221, Superset_223) | difference(Set1_221, Set2_222, Superset_223)))). % 8.92/3.14 tff(c_870, plain, (![Superset_10, Superset_291, Difference_292, Set1_290, Superset_293]: (member(k(Set1_290, Superset_291, Difference_292), Superset_10) | ~equal_sets(Superset_10, Superset_293) | ~equal_sets(Superset_293, Difference_292) | ~equal_sets(Superset_291, Set1_290) | difference(Set1_290, Superset_291, Difference_292)))). % 8.92/3.14 tff(c_535, plain, (![Superset_218, Superset_9, Difference_219, Set1_217, Superset_220]: (member(k(Set1_217, Superset_218, Difference_219), Superset_9) | ~equal_sets(Superset_220, Superset_9) | ~equal_sets(Superset_220, Difference_219) | ~equal_sets(Set1_217, Superset_218) | difference(Set1_217, Superset_218, Difference_219)))). % 8.92/3.15 tff(c_972, plain, (![Superset_313, Superset_310, Superset_9, Difference_312, Set2_311]: (member(k(Superset_310, Set2_311, Difference_312), Superset_9) | ~equal_sets(Superset_313, Superset_9) | ~equal_sets(Superset_313, Superset_310) | ~equal_sets(Superset_310, Difference_312) | difference(Superset_310, Set2_311, Difference_312)))). % 8.92/3.15 tff(c_834, plain, (![Superset_10, Superset_284, Set2_283, Set1_282, Superset_285]: (member(k(Set1_282, Set2_283, Superset_284), Superset_10) | ~equal_sets(Superset_10, Superset_285) | ~equal_sets(Superset_285, Superset_284) | ~equal_sets(Superset_284, Set1_282) | difference(Set1_282, Set2_283, Superset_284)))). % 8.92/3.15 tff(c_1408, plain, (![Set1_14, Set1_395, Set2_396, Difference_394, Set2_15, Superset_393]: (member(k(Set1_395, Set2_396, Difference_394), Set1_14) | ~difference(Set1_14, Set2_15, Superset_393) | ~equal_sets(Superset_393, Difference_394) | ~equal_sets(Superset_393, Set1_395) | difference(Set1_395, Set2_396, Difference_394)))). % 8.92/3.15 tff(c_628, plain, (![Superset_10, Difference_235, Superset_236, Set1_233, Set2_234]: (member(k(Set1_233, Set2_234, Difference_235), Superset_10) | ~equal_sets(Superset_10, Superset_236) | ~equal_sets(Difference_235, Superset_236) | member(k(Set1_233, Set2_234, Difference_235), Set1_233) | difference(Set1_233, Set2_234, Difference_235)))). % 8.92/3.15 tff(c_992, plain, (![Superset_10, Superset_319, Superset_322, Set2_320, Difference_321]: (member(k(Superset_319, Set2_320, Difference_321), Superset_10) | ~equal_sets(Superset_10, Superset_322) | ~equal_sets(Superset_319, Superset_322) | ~equal_sets(Superset_319, Difference_321) | difference(Superset_319, Set2_320, Difference_321)))). % 8.92/3.15 tff(c_534, plain, (![Superset_218, Superset_10, Difference_219, Set1_217, Superset_220]: (member(k(Set1_217, Superset_218, Difference_219), Superset_10) | ~equal_sets(Superset_10, Superset_220) | ~equal_sets(Superset_220, Difference_219) | ~equal_sets(Set1_217, Superset_218) | difference(Set1_217, Superset_218, Difference_219)))). % 8.92/3.15 tff(c_571, plain, (![Superset_227, Superset_9, Set1_225, Set2_226, Superset_228]: (member(k(Set1_225, Set2_226, Superset_227), Superset_9) | ~equal_sets(Superset_228, Superset_9) | ~equal_sets(Superset_228, Superset_227) | ~equal_sets(Set1_225, Superset_227) | difference(Set1_225, Set2_226, Superset_227)))). % 8.92/3.15 tff(c_588, plain, (![Superset_10, Difference_231, Superset_230, Superset_232, Set1_229]: (member(k(Set1_229, Superset_230, Difference_231), Superset_10) | ~equal_sets(Superset_10, Superset_232) | ~equal_sets(Difference_231, Superset_232) | ~equal_sets(Set1_229, Superset_230) | difference(Set1_229, Superset_230, Difference_231)))). % 8.92/3.15 tff(c_589, plain, (![Superset_9, Difference_231, Superset_230, Superset_232, Set1_229]: (member(k(Set1_229, Superset_230, Difference_231), Superset_9) | ~equal_sets(Superset_232, Superset_9) | ~equal_sets(Difference_231, Superset_232) | ~equal_sets(Set1_229, Superset_230) | difference(Set1_229, Superset_230, Difference_231)))). % 8.92/3.15 tff(c_1727, plain, (![Set1_14, Set2_415, Set1_414, Superset_413, Difference_412, Set2_15]: (member(k(Set1_414, Set2_415, Difference_412), Set1_14) | ~difference(Set1_14, Set2_15, Superset_413) | ~equal_sets(Difference_412, Superset_413) | ~equal_sets(Set1_414, Superset_413) | difference(Set1_414, Set2_415, Difference_412)))). % 8.92/3.15 tff(c_835, plain, (![Superset_9, Superset_284, Set2_283, Set1_282, Superset_285]: (member(k(Set1_282, Set2_283, Superset_284), Superset_9) | ~equal_sets(Superset_285, Superset_9) | ~equal_sets(Superset_285, Superset_284) | ~equal_sets(Superset_284, Set1_282) | difference(Set1_282, Set2_283, Superset_284)))). % 8.92/3.15 tff(c_852, plain, (![Superset_10, Superset_287, Superset_289, Difference_288, Set1_286]: (member(k(Set1_286, Superset_287, Difference_288), Superset_10) | ~equal_sets(Superset_10, Superset_289) | ~equal_sets(Difference_288, Superset_289) | ~equal_sets(Superset_287, Set1_286) | difference(Set1_286, Superset_287, Difference_288)))). % 8.92/3.15 tff(c_993, plain, (![Superset_9, Superset_319, Superset_322, Set2_320, Difference_321]: (member(k(Superset_319, Set2_320, Difference_321), Superset_9) | ~equal_sets(Superset_322, Superset_9) | ~equal_sets(Superset_319, Superset_322) | ~equal_sets(Superset_319, Difference_321) | difference(Superset_319, Set2_320, Difference_321)))). % 8.92/3.15 tff(c_930, plain, (![Set1_303, Superset_9, Set2_304, Difference_305, Superset_306]: (member(k(Set1_303, Set2_304, Difference_305), Superset_9) | ~equal_sets(Superset_306, Superset_9) | ~equal_sets(Superset_306, Difference_305) | member(k(Set1_303, Set2_304, Difference_305), Set1_303) | difference(Set1_303, Set2_304, Difference_305)))). % 8.92/3.15 tff(c_711, plain, (![Superset_9, Set2_248, Superset_250, Superset_247, Difference_249]: (member(k(Superset_247, Set2_248, Difference_249), Superset_9) | ~equal_sets(Superset_250, Superset_9) | ~equal_sets(Superset_247, Superset_250) | ~equal_sets(Difference_249, Superset_247) | difference(Superset_247, Set2_248, Difference_249)))). % 8.92/3.15 tff(c_1927, plain, (![Superset_10, Difference_486, Set2_487, Set1_484, Superset_485]: (member(k(Set1_484, Set2_487, Difference_486), Superset_10) | ~equal_sets(Superset_10, Superset_485) | ~equal_sets(Set1_484, Superset_485) | ~equal_sets(Superset_485, Difference_486) | difference(Set1_484, Set2_487, Difference_486)))). % 8.92/3.15 tff(c_1928, plain, (![Superset_9, Difference_486, Set2_487, Set1_484, Superset_485]: (member(k(Set1_484, Set2_487, Difference_486), Superset_9) | ~equal_sets(Superset_485, Superset_9) | ~equal_sets(Set1_484, Superset_485) | ~equal_sets(Superset_485, Difference_486) | difference(Set1_484, Set2_487, Difference_486)))). % 8.92/3.15 tff(c_853, plain, (![Superset_9, Superset_287, Superset_289, Difference_288, Set1_286]: (member(k(Set1_286, Superset_287, Difference_288), Superset_9) | ~equal_sets(Superset_289, Superset_9) | ~equal_sets(Difference_288, Superset_289) | ~equal_sets(Superset_287, Set1_286) | difference(Set1_286, Superset_287, Difference_288)))). % 8.92/3.15 tff(c_970, plain, (![Set1_14, Superset_313, Superset_310, Difference_312, Set2_311, Set2_15]: (member(k(Superset_310, Set2_311, Difference_312), Set1_14) | ~difference(Set1_14, Set2_15, Superset_313) | ~equal_sets(Superset_313, Superset_310) | ~equal_sets(Superset_310, Difference_312) | difference(Superset_310, Set2_311, Difference_312)))). % 8.92/3.15 tff(c_570, plain, (![Superset_227, Superset_10, Set1_225, Set2_226, Superset_228]: (member(k(Set1_225, Set2_226, Superset_227), Superset_10) | ~equal_sets(Superset_10, Superset_228) | ~equal_sets(Superset_228, Superset_227) | ~equal_sets(Set1_225, Superset_227) | difference(Set1_225, Set2_226, Superset_227)))). % 8.92/3.15 tff(c_1870, plain, (![Set1_303, Superset_9, Difference_305, Set2_304]: (~equal_sets(Set1_303, Superset_9) | ~equal_sets(Superset_9, Difference_305) | difference(Set1_303, Set2_304, Difference_305) | member(k(Set1_303, Set2_304, Difference_305), Superset_9)))). % 8.92/3.15 tff(c_935, plain, (![Set1_303, Superset_9, Set2_304, Difference_305, Superset_306]: (member(k(Set1_303, Set2_304, Difference_305), Superset_9) | ~equal_sets(Set1_303, Superset_9) | member(k(Set1_303, Set2_304, Difference_305), Superset_306) | ~equal_sets(Superset_306, Difference_305) | difference(Set1_303, Set2_304, Difference_305)))). % 8.92/3.15 tff(c_971, plain, (![Superset_313, Superset_310, Superset_10, Difference_312, Set2_311]: (member(k(Superset_310, Set2_311, Difference_312), Superset_10) | ~equal_sets(Superset_10, Superset_313) | ~equal_sets(Superset_313, Superset_310) | ~equal_sets(Superset_310, Difference_312) | difference(Superset_310, Set2_311, Difference_312)))). % 8.92/3.15 tff(c_552, plain, (![Set2_222, Set1_221, Superset_223, Superset_10, Superset_224]: (member(k(Set1_221, Set2_222, Superset_223), Superset_10) | ~equal_sets(Superset_10, Superset_224) | ~equal_sets(Superset_223, Superset_224) | ~equal_sets(Set1_221, Superset_223) | difference(Set1_221, Set2_222, Superset_223)))). % 8.92/3.15 tff(c_671, plain, (![Superset_9, Difference_242, Set2_241, Superset_240, Superset_243]: (member(k(Superset_240, Set2_241, Difference_242), Superset_9) | ~equal_sets(Superset_243, Superset_9) | ~equal_sets(Superset_243, Superset_240) | ~equal_sets(Difference_242, Superset_240) | difference(Superset_240, Set2_241, Difference_242)))). % 8.92/3.15 tff(c_1836, plain, (![Superset_450, Superset_10, Set2_453, Difference_452, Set1_451]: (member(k(Set1_451, Set2_453, Difference_452), Superset_10) | ~equal_sets(Superset_10, Superset_450) | ~equal_sets(Superset_450, Set1_451) | ~equal_sets(Superset_450, Difference_452) | difference(Set1_451, Set2_453, Difference_452)))). % 8.92/3.15 tff(c_889, plain, (![Superset_9, Superset_297, Set2_295, Set1_294, Superset_296]: (member(k(Set1_294, Set2_295, Superset_296), Superset_9) | ~equal_sets(Superset_297, Superset_9) | ~equal_sets(Superset_296, Superset_297) | ~equal_sets(Superset_296, Set1_294) | difference(Set1_294, Set2_295, Superset_296)))). % 8.92/3.15 tff(c_1779, plain, (![Superset_10, Set1_303, Difference_305, Set2_304]: (~equal_sets(Superset_10, Set1_303) | ~equal_sets(Superset_10, Difference_305) | difference(Set1_303, Set2_304, Difference_305) | member(k(Set1_303, Set2_304, Difference_305), Superset_10)))). % 8.92/3.15 tff(c_934, plain, (![Set1_303, Superset_10, Set2_304, Difference_305, Superset_306]: (member(k(Set1_303, Set2_304, Difference_305), Superset_10) | ~equal_sets(Superset_10, Set1_303) | member(k(Set1_303, Set2_304, Difference_305), Superset_306) | ~equal_sets(Superset_306, Difference_305) | difference(Set1_303, Set2_304, Difference_305)))). % 8.92/3.15 tff(c_1410, plain, (![Superset_9, Set1_395, Set2_396, Difference_394, Superset_393]: (member(k(Set1_395, Set2_396, Difference_394), Superset_9) | ~equal_sets(Superset_393, Superset_9) | ~equal_sets(Superset_393, Difference_394) | ~equal_sets(Superset_393, Set1_395) | difference(Set1_395, Set2_396, Difference_394)))). % 8.92/3.15 tff(c_710, plain, (![Superset_10, Set2_248, Superset_250, Superset_247, Difference_249]: (member(k(Superset_247, Set2_248, Difference_249), Superset_10) | ~equal_sets(Superset_10, Superset_250) | ~equal_sets(Superset_247, Superset_250) | ~equal_sets(Difference_249, Superset_247) | difference(Superset_247, Set2_248, Difference_249)))). % 8.92/3.15 tff(c_1728, plain, (![Set2_415, Superset_10, Set1_414, Superset_413, Difference_412]: (member(k(Set1_414, Set2_415, Difference_412), Superset_10) | ~equal_sets(Superset_10, Superset_413) | ~equal_sets(Difference_412, Superset_413) | ~equal_sets(Set1_414, Superset_413) | difference(Set1_414, Set2_415, Difference_412)))). % 8.92/3.15 tff(c_1729, plain, (![Superset_9, Set2_415, Set1_414, Superset_413, Difference_412]: (member(k(Set1_414, Set2_415, Difference_412), Superset_9) | ~equal_sets(Superset_413, Superset_9) | ~equal_sets(Difference_412, Superset_413) | ~equal_sets(Set1_414, Superset_413) | difference(Set1_414, Set2_415, Difference_412)))). % 8.92/3.15 tff(c_1636, plain, (![Set1_14, Superset_402, Superset_400, Set2_401, Set2_15]: (member(k(Superset_400, Set2_401, Superset_402), Set1_14) | ~difference(Set1_14, Set2_15, Set2_401) | ~equal_sets(Superset_400, Superset_402) | difference(Superset_400, Set2_401, Superset_402)))). % 8.92/3.15 tff(c_1638, plain, (![Superset_400, Set2_401, Superset_402, Superset_9]: (member(k(Superset_400, Set2_401, Superset_402), Superset_9) | ~equal_sets(Set2_401, Superset_9) | ~equal_sets(Superset_400, Superset_402) | difference(Superset_400, Set2_401, Superset_402)))). % 8.92/3.15 tff(c_1671, plain, (![Difference_200, Superset_9, Set1_198, Set2_199]: (~equal_sets(Difference_200, Superset_9) | ~equal_sets(Set1_198, Superset_9) | difference(Set1_198, Set2_199, Difference_200) | member(k(Set1_198, Set2_199, Difference_200), Superset_9)))). % 8.92/3.15 tff(c_474, plain, (![Set1_198, Superset_201, Superset_9, Difference_200, Set2_199]: (member(k(Set1_198, Set2_199, Difference_200), Superset_9) | ~equal_sets(Difference_200, Superset_9) | member(k(Set1_198, Set2_199, Difference_200), Superset_201) | ~equal_sets(Set1_198, Superset_201) | difference(Set1_198, Set2_199, Difference_200)))). % 8.92/3.15 tff(c_1637, plain, (![Superset_400, Set2_401, Superset_402, Superset_10]: (member(k(Superset_400, Set2_401, Superset_402), Superset_10) | ~equal_sets(Superset_10, Set2_401) | ~equal_sets(Superset_400, Superset_402) | difference(Superset_400, Set2_401, Superset_402)))). % 8.92/3.15 tff(c_1544, plain, (![Superset_307, Set2_309, Superset_9]: (member(k(Superset_307, Set2_309, Superset_9), Set2_309) | ~equal_sets(Superset_307, Superset_9) | difference(Superset_307, Set2_309, Superset_9)))). % 8.92/3.15 tff(c_1352, plain, (![Superset_10, Difference_269, Set1_267, Set2_268]: (~equal_sets(Superset_10, Difference_269) | ~equal_sets(Superset_10, Set1_267) | difference(Set1_267, Set2_268, Difference_269) | member(k(Set1_267, Set2_268, Difference_269), Superset_10)))). % 8.92/3.15 tff(c_777, plain, (![Superset_10, Difference_269, Set1_267, Set2_268, Superset_270]: (member(k(Set1_267, Set2_268, Difference_269), Superset_10) | ~equal_sets(Superset_10, Difference_269) | member(k(Set1_267, Set2_268, Difference_269), Superset_270) | ~equal_sets(Superset_270, Set1_267) | difference(Set1_267, Set2_268, Difference_269)))). % 8.92/3.15 tff(c_1294, plain, (![Set1_367, Set2_368, Superset_369, Superset_9]: (member(k(Set1_367, Set2_368, Superset_369), Superset_9) | ~equal_sets(Set2_368, Superset_9) | ~equal_sets(Superset_369, Set1_367) | difference(Set1_367, Set2_368, Superset_369)))). % 8.92/3.15 tff(c_1293, plain, (![Set1_367, Set2_368, Superset_369, Superset_10]: (member(k(Set1_367, Set2_368, Superset_369), Superset_10) | ~equal_sets(Superset_10, Set2_368) | ~equal_sets(Superset_369, Set1_367) | difference(Set1_367, Set2_368, Superset_369)))). % 8.92/3.15 tff(c_1292, plain, (![Superset_369, Set1_14, Set2_15, Set1_367, Set2_368]: (member(k(Set1_367, Set2_368, Superset_369), Set1_14) | ~difference(Set1_14, Set2_15, Set2_368) | ~equal_sets(Superset_369, Set1_367) | difference(Set1_367, Set2_368, Superset_369)))). % 8.92/3.15 tff(c_772, plain, (![Superset_10, Difference_269, Set1_267, Set2_268, Superset_270]: (member(k(Set1_267, Set2_268, Difference_269), Superset_10) | ~equal_sets(Superset_10, Superset_270) | ~equal_sets(Superset_270, Set1_267) | member(k(Set1_267, Set2_268, Difference_269), Difference_269) | difference(Set1_267, Set2_268, Difference_269)))). % 8.92/3.15 tff(c_1213, plain, (![Set1_272, Set2_273, Superset_9]: (member(k(Set1_272, Set2_273, Superset_9), Set2_273) | ~equal_sets(Superset_9, Set1_272) | difference(Set1_272, Set2_273, Superset_9)))). % 8.92/3.15 tff(c_471, plain, (![Set1_198, Difference_200, Superset_201]: (member(k(Set1_198, Difference_200, Difference_200), Difference_200) | member(k(Set1_198, Difference_200, Difference_200), Superset_201) | ~equal_sets(Set1_198, Superset_201) | difference(Set1_198, Difference_200, Difference_200)))). % 8.92/3.16 tff(c_371, plain, (![Set1_14, Superset_154, Set2_155, Set2_15, Superset_156]: (member(k(Superset_154, Set2_155, Superset_154), Set1_14) | ~difference(Set1_14, Set2_15, Superset_156) | ~equal_sets(Set2_155, Superset_156) | difference(Superset_154, Set2_155, Superset_154)))). % 8.92/3.16 tff(c_391, plain, (![Superset_157, Set1_14, Set2_158, Superset_159, Set2_15]: (member(k(Superset_157, Set2_158, Superset_157), Set1_14) | ~difference(Set1_14, Set2_15, Superset_159) | ~equal_sets(Superset_159, Set2_158) | difference(Superset_157, Set2_158, Superset_157)))). % 8.92/3.16 tff(c_510, plain, (![Set1_14, Difference_207, Set1_205, Set2_15, Superset_206]: (member(k(Set1_205, Superset_206, Difference_207), Set1_14) | ~difference(Set1_14, Set2_15, Difference_207) | ~equal_sets(Set1_205, Superset_206) | difference(Set1_205, Superset_206, Difference_207)))). % 8.92/3.16 tff(c_775, plain, (![Set1_267, Difference_269, Superset_270]: (member(k(Set1_267, Difference_269, Difference_269), Difference_269) | member(k(Set1_267, Difference_269, Difference_269), Superset_270) | ~equal_sets(Superset_270, Set1_267) | difference(Set1_267, Difference_269, Difference_269)))). % 8.92/3.16 tff(c_814, plain, (![Set1_14, Set1_275, Set2_15, Superset_274, Difference_276]: (member(k(Set1_275, Superset_274, Difference_276), Set1_14) | ~difference(Set1_14, Set2_15, Difference_276) | ~equal_sets(Superset_274, Set1_275) | difference(Set1_275, Superset_274, Difference_276)))). % 8.92/3.16 tff(c_649, plain, (![Set1_14, Superset_238, Difference_237, Set2_239, Set2_15]: (member(k(Superset_238, Set2_239, Difference_237), Set1_14) | ~difference(Set1_14, Set2_15, Superset_238) | ~equal_sets(Difference_237, Superset_238) | difference(Superset_238, Set2_239, Difference_237)))). % 8.92/3.16 tff(c_950, plain, (![Set1_14, Difference_308, Superset_307, Set2_309, Set2_15]: (member(k(Superset_307, Set2_309, Difference_308), Set1_14) | ~difference(Set1_14, Set2_15, Superset_307) | ~equal_sets(Superset_307, Difference_308) | difference(Superset_307, Set2_309, Difference_308)))). % 8.92/3.16 tff(c_796, plain, (![Set1_14, Set1_272, Superset_271, Set2_15, Set2_273]: (member(k(Set1_272, Set2_273, Superset_271), Set1_14) | ~difference(Set1_14, Set2_15, Superset_271) | ~equal_sets(Superset_271, Set1_272) | difference(Set1_272, Set2_273, Superset_271)))). % 8.92/3.16 tff(c_952, plain, (![Superset_307, Set2_309, Difference_308, Superset_9]: (member(k(Superset_307, Set2_309, Difference_308), Superset_9) | ~equal_sets(Superset_307, Superset_9) | ~equal_sets(Superset_307, Difference_308) | difference(Superset_307, Set2_309, Difference_308)))). % 8.92/3.16 tff(c_492, plain, (![Set1_14, Set1_202, Set2_204, Set2_15, Superset_203]: (member(k(Set1_202, Set2_204, Superset_203), Set1_14) | ~difference(Set1_14, Set2_15, Superset_203) | ~equal_sets(Set1_202, Superset_203) | difference(Set1_202, Set2_204, Superset_203)))). % 8.92/3.16 tff(c_951, plain, (![Superset_307, Set2_309, Difference_308, Superset_10]: (member(k(Superset_307, Set2_309, Difference_308), Superset_10) | ~equal_sets(Superset_10, Superset_307) | ~equal_sets(Superset_307, Difference_308) | difference(Superset_307, Set2_309, Difference_308)))). % 8.92/3.16 tff(c_903, plain, (![Superset_10, Difference_88, Set2_87]: (~equal_sets(Superset_10, Difference_88) | difference(Superset_10, Set2_87, Difference_88) | member(k(Superset_10, Set2_87, Difference_88), Superset_10)))). % 8.92/3.16 tff(c_155, plain, (![Set1_86, Set2_87, Difference_88, Superset_10]: (member(k(Set1_86, Set2_87, Difference_88), Superset_10) | ~equal_sets(Superset_10, Difference_88) | member(k(Set1_86, Set2_87, Difference_88), Set1_86) | difference(Set1_86, Set2_87, Difference_88)))). % 8.92/3.16 tff(c_251, plain, (![Set1_14, Superset_111, Set2_15, Set1_109, Difference_110]: (member(k(Set1_109, Set1_109, Difference_110), Set1_14) | ~difference(Set1_14, Set2_15, Superset_111) | ~equal_sets(Difference_110, Superset_111) | difference(Set1_109, Set1_109, Difference_110)))). % 8.92/3.16 tff(c_798, plain, (![Set1_272, Set2_273, Superset_271, Superset_9]: (member(k(Set1_272, Set2_273, Superset_271), Superset_9) | ~equal_sets(Superset_271, Superset_9) | ~equal_sets(Superset_271, Set1_272) | difference(Set1_272, Set2_273, Superset_271)))). % 8.92/3.16 tff(c_815, plain, (![Set1_275, Superset_274, Difference_276, Superset_10]: (member(k(Set1_275, Superset_274, Difference_276), Superset_10) | ~equal_sets(Superset_10, Difference_276) | ~equal_sets(Superset_274, Set1_275) | difference(Set1_275, Superset_274, Difference_276)))). % 8.92/3.16 tff(c_816, plain, (![Set1_275, Superset_274, Difference_276, Superset_9]: (member(k(Set1_275, Superset_274, Difference_276), Superset_9) | ~equal_sets(Difference_276, Superset_9) | ~equal_sets(Superset_274, Set1_275) | difference(Set1_275, Superset_274, Difference_276)))). % 8.92/3.16 tff(c_797, plain, (![Set1_272, Set2_273, Superset_271, Superset_10]: (member(k(Set1_272, Set2_273, Superset_271), Superset_10) | ~equal_sets(Superset_10, Superset_271) | ~equal_sets(Superset_271, Set1_272) | difference(Set1_272, Set2_273, Superset_271)))). % 8.92/3.16 tff(c_177, plain, (![Set1_14, Superset_93, Difference_91, Set2_92, Set2_15]: (member(k(Difference_91, Set2_92, Difference_91), Set1_14) | ~difference(Set1_14, Set2_15, Superset_93) | ~equal_sets(Superset_93, Difference_91) | difference(Difference_91, Set2_92, Difference_91)))). % 8.92/3.16 tff(c_770, plain, (![Superset_270, Set1_267, Difference_269]: (~equal_sets(Superset_270, Set1_267) | member(k(Set1_267, Superset_270, Difference_269), Difference_269) | difference(Set1_267, Superset_270, Difference_269)))). % 8.92/3.16 tff(c_740, plain, (![Superset_10, Set1_86, Set2_87]: (~equal_sets(Superset_10, Set1_86) | difference(Set1_86, Set2_87, Superset_10) | member(k(Set1_86, Set2_87, Superset_10), Superset_10)))). % 8.92/3.16 tff(c_158, plain, (![Set1_86, Set2_87, Difference_88, Superset_10]: (member(k(Set1_86, Set2_87, Difference_88), Superset_10) | ~equal_sets(Superset_10, Set1_86) | member(k(Set1_86, Set2_87, Difference_88), Difference_88) | difference(Set1_86, Set2_87, Difference_88)))). % 8.92/3.16 tff(c_373, plain, (![Superset_154, Set2_155, Superset_9, Superset_156]: (member(k(Superset_154, Set2_155, Superset_154), Superset_9) | ~equal_sets(Superset_156, Superset_9) | ~equal_sets(Set2_155, Superset_156) | difference(Superset_154, Set2_155, Superset_154)))). % 8.92/3.16 tff(c_393, plain, (![Superset_157, Set2_158, Superset_9, Superset_159]: (member(k(Superset_157, Set2_158, Superset_157), Superset_9) | ~equal_sets(Superset_159, Superset_9) | ~equal_sets(Superset_159, Set2_158) | difference(Superset_157, Set2_158, Superset_157)))). % 8.92/3.16 tff(c_392, plain, (![Superset_157, Set2_158, Superset_10, Superset_159]: (member(k(Superset_157, Set2_158, Superset_157), Superset_10) | ~equal_sets(Superset_10, Superset_159) | ~equal_sets(Superset_159, Set2_158) | difference(Superset_157, Set2_158, Superset_157)))). % 8.92/3.16 tff(c_372, plain, (![Superset_154, Set2_155, Superset_10, Superset_156]: (member(k(Superset_154, Set2_155, Superset_154), Superset_10) | ~equal_sets(Superset_10, Superset_156) | ~equal_sets(Set2_155, Superset_156) | difference(Superset_154, Set2_155, Superset_154)))). % 8.92/3.16 tff(c_651, plain, (![Superset_238, Set2_239, Difference_237, Superset_9]: (member(k(Superset_238, Set2_239, Difference_237), Superset_9) | ~equal_sets(Superset_238, Superset_9) | ~equal_sets(Difference_237, Superset_238) | difference(Superset_238, Set2_239, Difference_237)))). % 8.92/3.16 tff(c_650, plain, (![Superset_238, Set2_239, Difference_237, Superset_10]: (member(k(Superset_238, Set2_239, Difference_237), Superset_10) | ~equal_sets(Superset_10, Superset_238) | ~equal_sets(Difference_237, Superset_238) | difference(Superset_238, Set2_239, Difference_237)))). % 8.92/3.16 tff(c_602, plain, (![Difference_88, Superset_9, Set2_87]: (~equal_sets(Difference_88, Superset_9) | difference(Superset_9, Set2_87, Difference_88) | member(k(Superset_9, Set2_87, Difference_88), Superset_9)))). % 8.92/3.16 tff(c_156, plain, (![Set1_86, Set2_87, Difference_88, Superset_9]: (member(k(Set1_86, Set2_87, Difference_88), Superset_9) | ~equal_sets(Difference_88, Superset_9) | member(k(Set1_86, Set2_87, Difference_88), Set1_86) | difference(Set1_86, Set2_87, Difference_88)))). % 8.92/3.16 tff(c_512, plain, (![Set1_205, Superset_206, Difference_207, Superset_9]: (member(k(Set1_205, Superset_206, Difference_207), Superset_9) | ~equal_sets(Difference_207, Superset_9) | ~equal_sets(Set1_205, Superset_206) | difference(Set1_205, Superset_206, Difference_207)))). % 8.92/3.16 tff(c_493, plain, (![Set1_202, Set2_204, Superset_203, Superset_10]: (member(k(Set1_202, Set2_204, Superset_203), Superset_10) | ~equal_sets(Superset_10, Superset_203) | ~equal_sets(Set1_202, Superset_203) | difference(Set1_202, Set2_204, Superset_203)))). % 8.92/3.16 tff(c_494, plain, (![Set1_202, Set2_204, Superset_203, Superset_9]: (member(k(Set1_202, Set2_204, Superset_203), Superset_9) | ~equal_sets(Superset_203, Superset_9) | ~equal_sets(Set1_202, Superset_203) | difference(Set1_202, Set2_204, Superset_203)))). % 8.92/3.16 tff(c_511, plain, (![Set1_205, Superset_206, Difference_207, Superset_10]: (member(k(Set1_205, Superset_206, Difference_207), Superset_10) | ~equal_sets(Superset_10, Difference_207) | ~equal_sets(Set1_205, Superset_206) | difference(Set1_205, Superset_206, Difference_207)))). % 8.92/3.16 tff(c_188, plain, (![Difference_94, Set2_95, Superset_10, Superset_96]: (member(k(Difference_94, Set2_95, Difference_94), Superset_10) | ~equal_sets(Superset_10, Superset_96) | ~equal_sets(Difference_94, Superset_96) | difference(Difference_94, Set2_95, Difference_94)))). % 8.92/3.16 tff(c_187, plain, (![Set1_14, Set2_95, Superset_96, Set2_15, Difference_94]: (member(k(Difference_94, Set2_95, Difference_94), Set1_14) | ~difference(Set1_14, Set2_15, Superset_96) | ~equal_sets(Difference_94, Superset_96) | difference(Difference_94, Set2_95, Difference_94)))). % 8.92/3.16 tff(c_466, plain, (![Set1_198, Superset_201, Difference_200]: (~equal_sets(Set1_198, Superset_201) | member(k(Set1_198, Superset_201, Difference_200), Difference_200) | difference(Set1_198, Superset_201, Difference_200)))). % 8.92/3.16 tff(c_436, plain, (![Set1_86, Superset_9, Set2_87]: (~equal_sets(Set1_86, Superset_9) | difference(Set1_86, Set2_87, Superset_9) | member(k(Set1_86, Set2_87, Superset_9), Superset_9)))). % 8.92/3.16 tff(c_159, plain, (![Set1_86, Set2_87, Difference_88, Superset_9]: (member(k(Set1_86, Set2_87, Difference_88), Superset_9) | ~equal_sets(Set1_86, Superset_9) | member(k(Set1_86, Set2_87, Difference_88), Difference_88) | difference(Set1_86, Set2_87, Difference_88)))). % 8.92/3.16 tff(c_189, plain, (![Difference_94, Set2_95, Superset_9, Superset_96]: (member(k(Difference_94, Set2_95, Difference_94), Superset_9) | ~equal_sets(Superset_96, Superset_9) | ~equal_sets(Difference_94, Superset_96) | difference(Difference_94, Set2_95, Difference_94)))). % 8.92/3.16 tff(c_178, plain, (![Difference_91, Set2_92, Superset_10, Superset_93]: (member(k(Difference_91, Set2_92, Difference_91), Superset_10) | ~equal_sets(Superset_10, Superset_93) | ~equal_sets(Superset_93, Difference_91) | difference(Difference_91, Set2_92, Difference_91)))). % 8.92/3.16 tff(c_253, plain, (![Set1_109, Difference_110, Superset_9, Superset_111]: (member(k(Set1_109, Set1_109, Difference_110), Superset_9) | ~equal_sets(Superset_111, Superset_9) | ~equal_sets(Difference_110, Superset_111) | difference(Set1_109, Set1_109, Difference_110)))). % 8.92/3.16 tff(c_237, plain, (![Set1_14, Set1_106, Superset_108, Set2_15, Difference_107]: (member(k(Set1_106, Set1_106, Difference_107), Set1_14) | ~difference(Set1_14, Set2_15, Superset_108) | ~equal_sets(Superset_108, Difference_107) | difference(Set1_106, Set1_106, Difference_107)))). % 8.92/3.16 tff(c_252, plain, (![Set1_109, Difference_110, Superset_10, Superset_111]: (member(k(Set1_109, Set1_109, Difference_110), Superset_10) | ~equal_sets(Superset_10, Superset_111) | ~equal_sets(Difference_110, Superset_111) | difference(Set1_109, Set1_109, Difference_110)))). % 8.92/3.16 tff(c_239, plain, (![Set1_106, Difference_107, Superset_9, Superset_108]: (member(k(Set1_106, Set1_106, Difference_107), Superset_9) | ~equal_sets(Superset_108, Superset_9) | ~equal_sets(Superset_108, Difference_107) | difference(Set1_106, Set1_106, Difference_107)))). % 8.92/3.16 tff(c_238, plain, (![Set1_106, Difference_107, Superset_10, Superset_108]: (member(k(Set1_106, Set1_106, Difference_107), Superset_10) | ~equal_sets(Superset_10, Superset_108) | ~equal_sets(Superset_108, Difference_107) | difference(Set1_106, Set1_106, Difference_107)))). % 8.92/3.16 tff(c_157, plain, (![Difference_88, Set1_14, Set1_86, Set2_15, Set2_87]: (member(k(Set1_86, Set2_87, Difference_88), Set1_14) | ~difference(Set1_14, Set2_15, Set1_86) | member(k(Set1_86, Set2_87, Difference_88), Difference_88) | difference(Set1_86, Set2_87, Difference_88)))). % 8.92/3.16 tff(c_179, plain, (![Difference_91, Set2_92, Superset_9, Superset_93]: (member(k(Difference_91, Set2_92, Difference_91), Superset_9) | ~equal_sets(Superset_93, Superset_9) | ~equal_sets(Superset_93, Difference_91) | difference(Difference_91, Set2_92, Difference_91)))). % 8.92/3.16 tff(c_351, plain, (![Superset_148, Set2_149, Superset_10]: (member(k(Superset_148, Set2_149, Superset_148), Superset_10) | ~equal_sets(Superset_10, Set2_149) | difference(Superset_148, Set2_149, Superset_148)))). % 8.92/3.16 tff(c_352, plain, (![Superset_148, Set2_149, Superset_9]: (member(k(Superset_148, Set2_149, Superset_148), Superset_9) | ~equal_sets(Set2_149, Superset_9) | difference(Superset_148, Set2_149, Superset_148)))). % 8.92/3.16 tff(c_350, plain, (![Superset_148, Set2_149, Set1_14, Set2_15]: (member(k(Superset_148, Set2_149, Superset_148), Set1_14) | ~difference(Set1_14, Set2_15, Set2_149) | difference(Superset_148, Set2_149, Superset_148)))). % 8.92/3.16 tff(c_331, plain, (![Superset_9, Set2_90]: (member(k(Superset_9, Set2_90, Superset_9), Set2_90) | difference(Superset_9, Set2_90, Superset_9)))). % 8.92/3.16 tff(c_102, plain, (![Set1_14, Superset_69, Subset_68, Superset_70, Set2_15]: (member(member_of_1_not_of_2(Subset_68, Superset_69), Set1_14) | ~difference(Set1_14, Set2_15, Superset_70) | ~equal_sets(Superset_70, Subset_68) | subset(Subset_68, Superset_69)))). % 8.92/3.16 tff(c_154, plain, (![Difference_88, Set1_14, Set1_86, Set2_15, Set2_87]: (member(k(Set1_86, Set2_87, Difference_88), Set1_14) | ~difference(Set1_14, Set2_15, Difference_88) | member(k(Set1_86, Set2_87, Difference_88), Set1_86) | difference(Set1_86, Set2_87, Difference_88)))). % 8.92/3.16 tff(c_118, plain, (![Set1_14, Superset_76, Subset_75, Set2_15, Superset_77]: (member(member_of_1_not_of_2(Subset_75, Superset_76), Set1_14) | ~difference(Set1_14, Set2_15, Superset_77) | ~equal_sets(Subset_75, Superset_77) | subset(Subset_75, Superset_76)))). % 8.92/3.16 tff(c_103, plain, (![Subset_68, Superset_69, Superset_10, Superset_70]: (member(member_of_1_not_of_2(Subset_68, Superset_69), Superset_10) | ~equal_sets(Superset_10, Superset_70) | ~equal_sets(Superset_70, Subset_68) | subset(Subset_68, Superset_69)))). % 8.92/3.17 tff(c_120, plain, (![Subset_75, Superset_76, Superset_9, Superset_77]: (member(member_of_1_not_of_2(Subset_75, Superset_76), Superset_9) | ~equal_sets(Superset_77, Superset_9) | ~equal_sets(Subset_75, Superset_77) | subset(Subset_75, Superset_76)))). % 8.92/3.17 tff(c_119, plain, (![Subset_75, Superset_76, Superset_10, Superset_77]: (member(member_of_1_not_of_2(Subset_75, Superset_76), Superset_10) | ~equal_sets(Superset_10, Superset_77) | ~equal_sets(Subset_75, Superset_77) | subset(Subset_75, Superset_76)))). % 8.92/3.17 tff(c_223, plain, (![Set1_104, Difference_105, Set1_14, Set2_15]: (member(k(Set1_104, Set1_104, Difference_105), Set1_14) | ~difference(Set1_14, Set2_15, Difference_105) | difference(Set1_104, Set1_104, Difference_105)))). % 8.92/3.17 tff(c_24, plain, (![Set1_32, Set2_33, Difference_34]: (difference(Set1_32, Set2_33, Difference_34) | member(k(Set1_32, Set2_33, Difference_34), Set2_33) | ~member(k(Set1_32, Set2_33, Difference_34), Set1_32) | ~member(k(Set1_32, Set2_33, Difference_34), Difference_34)))). % 8.92/3.17 tff(c_225, plain, (![Set1_104, Difference_105, Superset_9]: (member(k(Set1_104, Set1_104, Difference_105), Superset_9) | ~equal_sets(Difference_105, Superset_9) | difference(Set1_104, Set1_104, Difference_105)))). % 8.92/3.17 tff(c_224, plain, (![Set1_104, Difference_105, Superset_10]: (member(k(Set1_104, Set1_104, Difference_105), Superset_10) | ~equal_sets(Superset_10, Difference_105) | difference(Set1_104, Set1_104, Difference_105)))). % 8.92/3.17 tff(c_211, plain, (![Set1_26, Difference_28]: (member(k(Set1_26, Set1_26, Difference_28), Difference_28) | difference(Set1_26, Set1_26, Difference_28)))). % 8.92/3.17 tff(c_22, plain, (![Set1_29, Set2_30, Difference_31]: (difference(Set1_29, Set2_30, Difference_31) | member(k(Set1_29, Set2_30, Difference_31), Difference_31) | ~member(k(Set1_29, Set2_30, Difference_31), Set2_30)))). % 8.92/3.17 tff(c_167, plain, (![Difference_89, Set2_90, Set1_14, Set2_15]: (member(k(Difference_89, Set2_90, Difference_89), Set1_14) | ~difference(Set1_14, Set2_15, Difference_89) | difference(Difference_89, Set2_90, Difference_89)))). % 8.92/3.17 tff(c_169, plain, (![Difference_89, Set2_90, Superset_9]: (member(k(Difference_89, Set2_90, Difference_89), Superset_9) | ~equal_sets(Difference_89, Superset_9) | difference(Difference_89, Set2_90, Difference_89)))). % 8.92/3.17 tff(c_168, plain, (![Difference_89, Set2_90, Superset_10]: (member(k(Difference_89, Set2_90, Difference_89), Superset_10) | ~equal_sets(Superset_10, Difference_89) | difference(Difference_89, Set2_90, Difference_89)))). % 8.92/3.17 tff(c_139, plain, (![Difference_28, Set2_27]: (difference(Difference_28, Set2_27, Difference_28) | member(k(Difference_28, Set2_27, Difference_28), Difference_28)))). % 8.92/3.17 tff(c_20, plain, (![Set1_26, Set2_27, Difference_28]: (member(k(Set1_26, Set2_27, Difference_28), Difference_28) | member(k(Set1_26, Set2_27, Difference_28), Set1_26) | difference(Set1_26, Set2_27, Difference_28)))). % 8.92/3.17 tff(c_104, plain, (![Subset_68, Superset_69, Superset_9, Superset_70]: (member(member_of_1_not_of_2(Subset_68, Superset_69), Superset_9) | ~equal_sets(Superset_70, Superset_9) | ~equal_sets(Superset_70, Subset_68) | subset(Subset_68, Superset_69)))). % 8.92/3.17 tff(c_90, plain, (![Subset_4, Superset_5, Set1_65, Set2_67]: (member(member_of_1_not_of_2(Subset_4, Superset_5), Set1_65) | ~difference(Set1_65, Set2_67, Subset_4) | subset(Subset_4, Superset_5)))). % 8.92/3.17 tff(c_82, plain, (![Subset_4, Superset_5, Superset_59]: (member(member_of_1_not_of_2(Subset_4, Superset_5), Superset_59) | ~equal_sets(Subset_4, Superset_59) | subset(Subset_4, Superset_5)))). % 8.92/3.17 tff(c_18, plain, (![Element_22, Set2_24, Difference_25, Set1_23]: (member(Element_22, Set2_24) | member(Element_22, Difference_25) | ~difference(Set1_23, Set2_24, Difference_25) | ~member(Element_22, Set1_23)))). % 8.92/3.17 tff(c_86, plain, (![Subset_4, Superset_5, Superset_62]: (member(member_of_1_not_of_2(Subset_4, Superset_5), Superset_62) | ~equal_sets(Superset_62, Subset_4) | subset(Subset_4, Superset_5)))). % 8.92/3.17 tff(c_14, plain, (![Element_17, Set1_14, Difference_16, Set2_15]: (member(Element_17, Set1_14) | ~member(Element_17, Difference_16) | ~difference(Set1_14, Set2_15, Difference_16)))). % 8.92/3.17 tff(c_57, plain, (![Element_47, Superset_10, Subset_11]: (member(Element_47, Superset_10) | ~member(Element_47, Subset_11) | ~equal_sets(Superset_10, Subset_11)))). % 8.92/3.17 tff(c_56, plain, (![Element_47, Superset_9, Subset_8]: (member(Element_47, Superset_9) | ~member(Element_47, Subset_8) | ~equal_sets(Subset_8, Superset_9)))). % 8.92/3.17 tff(c_71, plain, (![Superset_9, Subset_8]: (equal_sets(Superset_9, Subset_8) | ~equal_sets(Subset_8, Superset_9)))). % 8.92/3.17 tff(c_16, plain, (![A_set_21, Set1_19, Set2_20, Element_18]: (~difference(A_set_21, Set1_19, Set2_20) | ~member(Element_18, Set2_20) | ~member(Element_18, Set1_19)))). % 8.92/3.17 tff(c_2, plain, (![Element_1, Superset_3, Subset_2]: (member(Element_1, Superset_3) | ~subset(Subset_2, Superset_3) | ~member(Element_1, Subset_2)))). % 8.92/3.17 tff(c_44, plain, (![Subset_41]: (equal_sets(Subset_41, Subset_41)))). % 8.92/3.17 tff(c_12, plain, (![Set2_13, Set1_12]: (equal_sets(Set2_13, Set1_12) | ~subset(Set2_13, Set1_12) | ~subset(Set1_12, Set2_13)))). % 8.92/3.17 tff(c_33, plain, (![Subset_41]: (subset(Subset_41, Subset_41)))). % 8.92/3.17 tff(c_4, plain, (![Subset_4, Superset_5]: (member(member_of_1_not_of_2(Subset_4, Superset_5), Subset_4) | subset(Subset_4, Superset_5)))). % 8.92/3.17 tff(c_6, plain, (![Subset_6, Superset_7]: (subset(Subset_6, Superset_7) | ~member(member_of_1_not_of_2(Subset_6, Superset_7), Superset_7)))). % 8.92/3.17 tff(c_8, plain, (![Subset_8, Superset_9]: (subset(Subset_8, Superset_9) | ~equal_sets(Subset_8, Superset_9)))). % 8.92/3.17 tff(c_10, plain, (![Subset_11, Superset_10]: (subset(Subset_11, Superset_10) | ~equal_sets(Superset_10, Subset_11)))). % 8.92/3.17 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.92/3.17 %------------------------------------------------------------------------------