%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SEV436-1 : TPTP v8.1.0. Released v6.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n019.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 : 600s % DateTime : Tue Jul 19 17:45:11 EDT 2022 % Result : Satisfiable 0.46s 0.61s % Output : Saturation 0.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SEV436-1 : TPTP v8.1.0. Released v6.4.0. % 0.10/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n019.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jun 28 09:34:24 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.46/0.61 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.46/0.61 % 0.46/0.61 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.46/0.61 |- ~member $Element $Subset \/ ~subset $Subset $Superset \/ % 0.46/0.61 member $Element $Superset % 0.46/0.61 |- member (member_of_1_not_of_2 $Subset $Superset) $Subset \/ % 0.46/0.61 subset $Subset $Superset % 0.46/0.61 |- ~member (member_of_1_not_of_2 $Subset $Superset) $Superset \/ % 0.46/0.61 subset $Subset $Superset % 0.46/0.61 |- ~equal_sets $Subset $Superset \/ subset $Subset $Superset % 0.46/0.61 |- ~equal_sets $Superset $Subset \/ subset $Subset $Superset % 0.46/0.61 |- ~subset $Set1 $Set2 \/ ~subset $Set2 $Set1 \/ equal_sets $Set2 $Set1 % 0.46/0.61 |- ~member $Element $Union \/ ~union $Set1 $Set2 $Union \/ % 0.46/0.61 member $Element $Set1 \/ member $Element $Set2 % 0.46/0.61 |- ~member $Element $Set1 \/ ~union $Set1 $Set2 $Union \/ % 0.46/0.61 member $Element $Union % 0.46/0.61 |- ~member $Element $Set2 \/ ~union $Set1 $Set2 $Union \/ % 0.46/0.61 member $Element $Union % 0.46/0.61 |- member (g $Set1 $Set2 $Union) $Set1 \/ % 0.46/0.61 member (g $Set1 $Set2 $Union) $Set2 \/ % 0.46/0.61 member (g $Set1 $Set2 $Union) $Union \/ union $Set1 $Set2 $Union % 0.46/0.61 |- ~member (g $Set1 $Set2 $Union) $Set1 \/ % 0.46/0.61 ~member (g $Set1 $Set2 $Union) $Union \/ union $Set1 $Set2 $Union % 0.46/0.61 |- ~member (g $Set1 $Set2 $Union) $Set2 \/ % 0.46/0.61 ~member (g $Set1 $Set2 $Union) $Union \/ union $Set1 $Set2 $Union % 0.46/0.61 |- ~intersection $Set1 $Set2 $Intersection \/ % 0.46/0.61 ~member $Element $Intersection \/ member $Element $Set1 % 0.46/0.61 |- ~intersection $Set1 $Set2 $Intersection \/ % 0.46/0.61 ~member $Element $Intersection \/ member $Element $Set2 % 0.46/0.61 |- ~intersection $Set1 $Set2 $Intersection \/ ~member $Element $Set1 \/ % 0.46/0.61 ~member $Element $Set2 \/ member $Element $Intersection % 0.46/0.61 |- intersection $Set1 $Set2 $Intersection \/ % 0.46/0.61 member (h $Set1 $Set2 $Intersection) $Intersection \/ % 0.46/0.61 member (h $Set1 $Set2 $Intersection) $Set1 % 0.46/0.61 |- intersection $Set1 $Set2 $Intersection \/ % 0.46/0.61 member (h $Set1 $Set2 $Intersection) $Intersection \/ % 0.46/0.61 member (h $Set1 $Set2 $Intersection) $Set2 % 0.46/0.61 |- ~member (h $Set1 $Set2 $Intersection) $Intersection \/ % 0.46/0.61 ~member (h $Set1 $Set2 $Intersection) $Set1 \/ % 0.46/0.61 ~member (h $Set1 $Set2 $Intersection) $Set2 \/ % 0.46/0.61 intersection $Set1 $Set2 $Intersection % 0.46/0.61 |- ~difference $Set1 $Set2 $Difference \/ ~member $Element $Difference \/ % 0.46/0.61 member $Element $Set1 % 0.46/0.61 |- ~difference $A_set $Set1 $Set2 \/ ~member $Element $Set1 \/ % 0.46/0.61 ~member $Element $Set2 % 0.46/0.61 |- ~difference $Set1 $Set2 $Difference \/ ~member $Element $Set1 \/ % 0.46/0.61 member $Element $Difference \/ member $Element $Set2 % 0.46/0.61 |- difference $Set1 $Set2 $Difference \/ % 0.46/0.61 member (k $Set1 $Set2 $Difference) $Difference \/ % 0.46/0.61 member (k $Set1 $Set2 $Difference) $Set1 % 0.46/0.61 |- ~member (k $Set1 $Set2 $Difference) $Set2 \/ % 0.46/0.61 difference $Set1 $Set2 $Difference \/ % 0.46/0.61 member (k $Set1 $Set2 $Difference) $Difference % 0.46/0.61 |- ~member (k $Set1 $Set2 $Difference) $Difference \/ % 0.46/0.61 ~member (k $Set1 $Set2 $Difference) $Set1 \/ % 0.46/0.61 difference $Set1 $Set2 $Difference \/ % 0.46/0.61 member (k $Set1 $Set2 $Difference) $Set2 % 0.46/0.61 |- ~member (g $Union $Set2 $Union) $Union \/ union $Union $Set2 $Union % 0.46/0.61 |- ~member (g $Set1 $Union $Union) $Union \/ union $Set1 $Union $Union % 0.46/0.61 |- intersection $Set1 $Set2 $Set1 \/ member (h $Set1 $Set2 $Set1) $Set1 % 0.46/0.61 |- intersection $Set1 $Set2 $Set2 \/ member (h $Set1 $Set2 $Set2) $Set2 % 0.46/0.61 |- ~difference $A_set $Set2 $Set2 \/ ~member $Element $Set2 % 0.46/0.61 |- difference $Set1 $Set2 $Set1 \/ member (k $Set1 $Set2 $Set1) $Set1 % 0.46/0.61 |- member (g $Set2 $Set2 $Union) $Set2 \/ % 0.46/0.61 member (g $Set2 $Set2 $Union) $Union \/ union $Set2 $Set2 $Union % 0.46/0.61 |- ~intersection $Set2 $Set2 $Intersection \/ ~member $Element $Set2 \/ % 0.46/0.61 member $Element $Intersection % 0.46/0.61 |- ~member (h $Set2 $Set2 $Intersection) $Intersection \/ % 0.46/0.61 ~member (h $Set2 $Set2 $Intersection) $Set2 \/ % 0.46/0.61 intersection $Set2 $Set2 $Intersection % 0.46/0.61 |- subset $_10 $_10 % 0.46/0.61 |- equal_sets $_11 $_11 % 0.46/0.61 |- ~difference $_13 $_15 $_15 \/ subset $_15 $Superset % 0.46/0.61 |- union $_18 $_18 $_18 % 0.46/0.61 |- ~difference $A_set $_23 $_23 \/ intersection $_23 $_24 $_23 % 0.46/0.61 |- intersection $_24 $_24 $_24 % 0.46/0.61 |- ~difference $A_set $_27 $_27 \/ intersection $_26 $_27 $_27 % 0.46/0.61 |- ~difference $A_set $_28 $_28 \/ difference $_28 $_29 $_28 % 0.46/0.61 |- ~subset $_45 $_46 \/ intersection $Set1 $_45 $_45 \/ % 0.46/0.61 member (h $Set1 $_45 $_45) $_46 % 0.46/0.61 |- ~subset $_45 $_46 \/ intersection $_45 $Set2 $_45 \/ % 0.46/0.61 member (h $_45 $Set2 $_45) $_46 % 0.46/0.61 |- ~subset $_45 $_46 \/ difference $_45 $Set2 $_45 \/ % 0.46/0.61 member (k $_45 $Set2 $_45) $_46 % 0.46/0.61 |- ~subset $_45 $_46 \/ % 0.46/0.61 member (member_of_1_not_of_2 $_45 $Superset) $_46 \/ % 0.46/0.61 subset $_45 $Superset % 0.46/0.61 |- difference $_47 $_48 $_47 \/ member (k $_47 $_48 $_47) $_48 % 0.46/0.61 |- ~subset $_50 $Superset \/ difference $_49 $_50 $_49 \/ % 0.46/0.61 member (k $_49 $_50 $_49) $Superset % 0.46/0.61 |- ~difference $A_set $_50 $_50 \/ difference $_49 $_50 $_49 % 0.46/0.61 |- ~intersection $_56 $_56 $_55 \/ intersection $Set1 $_56 $_56 \/ % 0.46/0.61 member (h $Set1 $_56 $_56) $_55 % 0.46/0.61 |- ~intersection $_56 $_56 $_55 \/ intersection $_56 $Set2 $_56 \/ % 0.46/0.61 member (h $_56 $Set2 $_56) $_55 % 0.46/0.61 |- ~intersection $_56 $_56 $_55 \/ difference $_47 $_56 $_47 \/ % 0.46/0.61 member (k $_47 $_56 $_47) $_55 % 0.46/0.61 |- ~intersection $_56 $_56 $_55 \/ difference $_56 $Set2 $_56 \/ % 0.46/0.61 member (k $_56 $Set2 $_56) $_55 % 0.46/0.61 |- ~intersection $_56 $_56 $_55 \/ % 0.46/0.61 member (member_of_1_not_of_2 $_56 $Superset) $_55 \/ % 0.46/0.61 subset $_56 $Superset % 0.46/0.61 |- ~intersection $_57 $_57 $Intersection \/ % 0.46/0.61 member (g $_57 $_57 $_58) $Intersection \/ % 0.46/0.61 member (g $_57 $_57 $_58) $_58 \/ union $_57 $_57 $_58 % 0.46/0.61 |- ~subset $_57 $Superset \/ member (g $_57 $_57 $_58) $Superset \/ % 0.46/0.61 member (g $_57 $_57 $_58) $_58 \/ union $_57 $_57 $_58 % 0.46/0.61 |- ~difference $A_set $_57 $_57 \/ member (g $_57 $_57 $_58) $_58 \/ % 0.46/0.61 union $_57 $_57 $_58 % 0.46/0.61 |- ~intersection $_58 $_58 $Intersection \/ % 0.46/0.61 member (g $_57 $_57 $_58) $Intersection \/ % 0.46/0.61 member (g $_57 $_57 $_58) $_57 \/ union $_57 $_57 $_58 % 0.46/0.61 |- ~subset $_58 $Superset \/ member (g $_57 $_57 $_58) $Superset \/ % 0.46/0.61 member (g $_57 $_57 $_58) $_57 \/ union $_57 $_57 $_58 % 0.46/0.61 |- ~difference $A_set $_58 $_58 \/ member (g $_57 $_57 $_58) $_57 \/ % 0.46/0.61 union $_57 $_57 $_58 % 0.46/0.61 |- member (g $_60 $_59 $_60) $_59 \/ union $_60 $_59 $_60 % 0.46/0.61 |- ~intersection $_61 $_61 $Intersection \/ % 0.46/0.61 member (g $_62 $_61 $_62) $Intersection \/ union $_62 $_61 $_62 % 0.46/0.61 |- ~subset $_61 $Superset \/ member (g $_62 $_61 $_62) $Superset \/ % 0.46/0.61 union $_62 $_61 $_62 % 0.46/0.61 |- ~difference $A_set $_61 $_61 \/ union $_62 $_61 $_62 % 0.46/0.61 |- member (g $_66 $_67 $_67) $_66 \/ union $_66 $_67 $_67 % 0.46/0.61 |- ~intersection $_68 $_68 $Intersection \/ % 0.46/0.61 member (g $_68 $_69 $_69) $Intersection \/ union $_68 $_69 $_69 % 0.46/0.61 |- ~subset $_68 $Superset \/ member (g $_68 $_69 $_69) $Superset \/ % 0.46/0.61 union $_68 $_69 $_69 % 0.46/0.61 |- ~difference $A_set $_68 $_68 \/ union $_68 $_69 $_69 % 0.46/0.61 |- ~member (h $_73 $_74 $_73) $_74 \/ intersection $_73 $_74 $_73 % 0.46/0.61 |- ~member (h $_77 $_78 $_78) $_77 \/ intersection $_77 $_78 $_78 % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ member (g $_84 $_67 $_67) $_86 \/ % 0.46/0.61 union $_84 $_67 $_67 % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ member (g $_60 $_84 $_60) $_86 \/ % 0.46/0.61 union $_60 $_84 $_60 % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ member (g $Set2 $Set2 $_84) $Set2 \/ % 0.46/0.61 member (g $Set2 $Set2 $_84) $_86 \/ union $Set2 $Set2 $_84 % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ member (g $_84 $_84 $Union) $Union \/ % 0.46/0.61 member (g $_84 $_84 $Union) $_86 \/ union $_84 $_84 $Union % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ intersection $Set1 $_84 $_84 \/ % 0.46/0.61 member (h $Set1 $_84 $_84) $_86 % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ intersection $_84 $Set2 $_84 \/ % 0.46/0.61 member (h $_84 $Set2 $_84) $_86 % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ difference $_47 $_84 $_47 \/ % 0.46/0.61 member (k $_47 $_84 $_47) $_86 % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ difference $_84 $Set2 $_84 \/ % 0.46/0.61 member (k $_84 $Set2 $_84) $_86 % 0.46/0.61 |- ~union $_84 $_85 $_86 \/ % 0.46/0.61 member (member_of_1_not_of_2 $_84 $Superset) $_86 \/ % 0.46/0.61 subset $_84 $Superset % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ member (g $_89 $_67 $_67) $_90 \/ % 0.46/0.61 union $_89 $_67 $_67 % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ member (g $_60 $_89 $_60) $_90 \/ % 0.46/0.61 union $_60 $_89 $_60 % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ member (g $Set2 $Set2 $_89) $Set2 \/ % 0.46/0.61 member (g $Set2 $Set2 $_89) $_90 \/ union $Set2 $Set2 $_89 % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ member (g $_89 $_89 $Union) $Union \/ % 0.46/0.61 member (g $_89 $_89 $Union) $_90 \/ union $_89 $_89 $Union % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ intersection $Set1 $_89 $_89 \/ % 0.46/0.61 member (h $Set1 $_89 $_89) $_90 % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ intersection $_89 $Set2 $_89 \/ % 0.46/0.61 member (h $_89 $Set2 $_89) $_90 % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ difference $_47 $_89 $_47 \/ % 0.46/0.61 member (k $_47 $_89 $_47) $_90 % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ difference $_89 $Set2 $_89 \/ % 0.46/0.61 member (k $_89 $Set2 $_89) $_90 % 0.46/0.61 |- ~union $_88 $_89 $_90 \/ % 0.46/0.61 member (member_of_1_not_of_2 $_89 $Superset) $_90 \/ % 0.46/0.61 subset $_89 $Superset % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ member (g $_92 $_67 $_67) $_93 \/ % 0.46/0.61 union $_92 $_67 $_67 % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ member (g $_60 $_92 $_60) $_93 \/ % 0.46/0.61 union $_60 $_92 $_60 % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ member (g $Set2 $Set2 $_92) $Set2 \/ % 0.46/0.61 member (g $Set2 $Set2 $_92) $_93 \/ union $Set2 $Set2 $_92 % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ member (g $_92 $_92 $Union) $Union \/ % 0.46/0.61 member (g $_92 $_92 $Union) $_93 \/ union $_92 $_92 $Union % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ intersection $Set1 $_92 $_92 \/ % 0.46/0.61 member (h $Set1 $_92 $_92) $_93 % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ intersection $_92 $Set2 $_92 \/ % 0.46/0.61 member (h $_92 $Set2 $_92) $_93 % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ difference $_47 $_92 $_47 \/ % 0.46/0.61 member (k $_47 $_92 $_47) $_93 % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ difference $_92 $Set2 $_92 \/ % 0.46/0.61 member (k $_92 $Set2 $_92) $_93 % 0.46/0.61 |- ~intersection $_93 $_94 $_92 \/ % 0.46/0.61 member (member_of_1_not_of_2 $_92 $Superset) $_93 \/ % 0.46/0.61 subset $_92 $Superset % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ member (g $_96 $_67 $_67) $_98 \/ % 0.46/0.61 union $_96 $_67 $_67 % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ member (g $_60 $_96 $_60) $_98 \/ % 0.46/0.61 union $_60 $_96 $_60 % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ member (g $Set2 $Set2 $_96) $Set2 \/ % 0.46/0.61 member (g $Set2 $Set2 $_96) $_98 \/ union $Set2 $Set2 $_96 % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ member (g $_96 $_96 $Union) $Union \/ % 0.46/0.61 member (g $_96 $_96 $Union) $_98 \/ union $_96 $_96 $Union % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ intersection $Set1 $_96 $_96 \/ % 0.46/0.61 member (h $Set1 $_96 $_96) $_98 % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ intersection $_96 $Set2 $_96 \/ % 0.46/0.61 member (h $_96 $Set2 $_96) $_98 % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ difference $_47 $_96 $_47 \/ % 0.46/0.61 member (k $_47 $_96 $_47) $_98 % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ difference $_96 $Set2 $_96 \/ % 0.46/0.61 member (k $_96 $Set2 $_96) $_98 % 0.46/0.61 |- ~intersection $_97 $_98 $_96 \/ % 0.46/0.61 member (member_of_1_not_of_2 $_96 $Superset) $_98 \/ % 0.46/0.61 subset $_96 $Superset % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ member (g $_103 $_67 $_67) $_105 \/ % 0.46/0.61 union $_103 $_67 $_67 % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ member (g $_60 $_103 $_60) $_105 \/ % 0.46/0.61 union $_60 $_103 $_60 % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ member (g $Set2 $Set2 $_103) $Set2 \/ % 0.46/0.61 member (g $Set2 $Set2 $_103) $_105 \/ union $Set2 $Set2 $_103 % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ member (g $_103 $_103 $Union) $Union \/ % 0.46/0.61 member (g $_103 $_103 $Union) $_105 \/ union $_103 $_103 $Union % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ intersection $Set1 $_103 $_103 \/ % 0.46/0.61 member (h $Set1 $_103 $_103) $_105 % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ intersection $_103 $Set2 $_103 \/ % 0.46/0.61 member (h $_103 $Set2 $_103) $_105 % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ difference $_47 $_103 $_47 \/ % 0.46/0.61 member (k $_47 $_103 $_47) $_105 % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ difference $_103 $Set2 $_103 \/ % 0.46/0.61 member (k $_103 $Set2 $_103) $_105 % 0.46/0.61 |- ~difference $_105 $_106 $_103 \/ % 0.46/0.61 member (member_of_1_not_of_2 $_103 $Superset) $_105 \/ % 0.46/0.61 subset $_103 $Superset % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (g $_109 $_67 $_67) $_110 \/ % 0.46/0.61 union $_109 $_67 $_67 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (g $_60 $_109 $_60) $_110 \/ % 0.46/0.61 union $_60 $_109 $_60 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (g $Set2 $Set2 $_109) $_110 \/ % 0.46/0.61 member (g $Set2 $Set2 $_109) $Set2 \/ union $Set2 $Set2 $_109 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (g $_109 $_109 $Union) $_110 \/ % 0.46/0.61 member (g $_109 $_109 $Union) $Union \/ union $_109 $_109 $Union % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (h $Set1 $_109 $_109) $_110 \/ % 0.46/0.61 intersection $Set1 $_109 $_109 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (h $_109 $Set2 $_109) $_110 \/ % 0.46/0.61 intersection $_109 $Set2 $_109 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (k $_47 $_109 $_47) $_110 \/ % 0.46/0.61 difference $_47 $_109 $_47 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (k $_109 $Set2 $_109) $_110 \/ % 0.46/0.61 difference $_109 $Set2 $_109 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ % 0.46/0.61 ~member (member_of_1_not_of_2 $_109 $Superset) $_110 \/ % 0.46/0.61 subset $_109 $Superset % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (g $_110 $_67 $_67) $_109 \/ % 0.46/0.61 union $_110 $_67 $_67 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (g $_60 $_110 $_60) $_109 \/ % 0.46/0.61 union $_60 $_110 $_60 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (g $Set2 $Set2 $_110) $_109 \/ % 0.46/0.61 member (g $Set2 $Set2 $_110) $Set2 \/ union $Set2 $Set2 $_110 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (g $_110 $_110 $Union) $_109 \/ % 0.46/0.61 member (g $_110 $_110 $Union) $Union \/ union $_110 $_110 $Union % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (h $Set1 $_110 $_110) $_109 \/ % 0.46/0.61 intersection $Set1 $_110 $_110 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (h $_110 $Set2 $_110) $_109 \/ % 0.46/0.61 intersection $_110 $Set2 $_110 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (k $_47 $_110 $_47) $_109 \/ % 0.46/0.61 difference $_47 $_110 $_47 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ ~member (k $_110 $Set2 $_110) $_109 \/ % 0.46/0.61 difference $_110 $Set2 $_110 % 0.46/0.61 |- ~difference $_107 $_109 $_110 \/ % 0.46/0.61 ~member (member_of_1_not_of_2 $_110 $Superset) $_109 \/ % 0.46/0.61 subset $_110 $Superset % 0.46/0.61 |- ~difference $_125 $_126 $_127 \/ difference $_127 $_126 $_127 % 0.46/0.61 |- ~difference $A_set $Set1 $_138 \/ ~member (h $_139 $_140 $_138) $Set1 \/ % 0.46/0.61 intersection $_139 $_140 $_138 \/ member (h $_139 $_140 $_138) $_139 % 0.46/0.61 |- ~difference $A_set $_138 $Set2 \/ ~member (h $_139 $_140 $_138) $Set2 \/ % 0.46/0.61 intersection $_139 $_140 $_138 \/ member (h $_139 $_140 $_138) $_139 % 0.46/0.61 |- ~difference $Set1 $Set2 $_138 \/ intersection $_139 $_140 $_138 \/ % 0.46/0.61 member (h $_139 $_140 $_138) $Set1 \/ member (h $_139 $_140 $_138) $_139 % 0.46/0.61 |- ~intersection $Set1 $Set2 $_138 \/ intersection $_139 $_140 $_138 \/ % 0.46/0.61 member (h $_139 $_140 $_138) $Set2 \/ member (h $_139 $_140 $_138) $_139 % 0.46/0.61 |- ~intersection $Set1 $Set2 $_138 \/ intersection $_139 $_140 $_138 \/ % 0.46/0.61 member (h $_139 $_140 $_138) $Set1 \/ member (h $_139 $_140 $_138) $_139 % 0.46/0.61 |- ~union $Set1 $_138 $Union \/ intersection $_139 $_140 $_138 \/ % 0.46/0.61 member (h $_139 $_140 $_138) $Union \/ % 0.46/0.61 member (h $_139 $_140 $_138) $_139 % 0.46/0.62 |- ~union $_138 $Set2 $Union \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Union \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_139 % 0.46/0.62 |- ~intersection $_138 $_138 $Intersection \/ % 0.46/0.62 intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Intersection \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_139 % 0.46/0.62 |- ~subset $_138 $Superset \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Superset \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_139 % 0.46/0.62 |- ~difference $A_set $_138 $_138 \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_139 % 0.46/0.62 |- ~difference $A_set $Set1 $_139 \/ ~member (h $_139 $_140 $_138) $Set1 \/ % 0.46/0.62 intersection $_139 $_140 $_138 \/ member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~difference $A_set $_139 $Set2 \/ ~member (h $_139 $_140 $_138) $Set2 \/ % 0.46/0.62 intersection $_139 $_140 $_138 \/ member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~difference $Set1 $Set2 $_139 \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Set1 \/ member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_139 \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Set2 \/ member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_139 \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Set1 \/ member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~union $Set1 $_139 $Union \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Union \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~union $_139 $Set2 $Union \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Union \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~intersection $_139 $_139 $Intersection \/ % 0.46/0.62 intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Intersection \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~subset $_139 $Superset \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $Superset \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~difference $A_set $_139 $_139 \/ intersection $_139 $_140 $_138 \/ % 0.46/0.62 member (h $_139 $_140 $_138) $_138 % 0.46/0.62 |- ~difference $A_set $Set1 $_141 \/ ~member (h $_142 $_143 $_141) $Set1 \/ % 0.46/0.62 intersection $_142 $_143 $_141 \/ member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~difference $A_set $_141 $Set2 \/ ~member (h $_142 $_143 $_141) $Set2 \/ % 0.46/0.62 intersection $_142 $_143 $_141 \/ member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~difference $Set1 $Set2 $_141 \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Set1 \/ member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_141 \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Set2 \/ member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_141 \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Set1 \/ member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~union $Set1 $_141 $Union \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Union \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~union $_141 $Set2 $Union \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Union \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~intersection $_141 $_141 $Intersection \/ % 0.46/0.62 intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Intersection \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~subset $_141 $Superset \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Superset \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~difference $A_set $_141 $_141 \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_143 % 0.46/0.62 |- ~difference $A_set $Set1 $_143 \/ ~member (h $_142 $_143 $_141) $Set1 \/ % 0.46/0.62 intersection $_142 $_143 $_141 \/ member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~difference $A_set $_143 $Set2 \/ ~member (h $_142 $_143 $_141) $Set2 \/ % 0.46/0.62 intersection $_142 $_143 $_141 \/ member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~difference $Set1 $Set2 $_143 \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Set1 \/ member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_143 \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Set2 \/ member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_143 \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Set1 \/ member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~union $Set1 $_143 $Union \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Union \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~union $_143 $Set2 $Union \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Union \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~intersection $_143 $_143 $Intersection \/ % 0.46/0.62 intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Intersection \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~subset $_143 $Superset \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $Superset \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~difference $A_set $_143 $_143 \/ intersection $_142 $_143 $_141 \/ % 0.46/0.62 member (h $_142 $_143 $_141) $_141 % 0.46/0.62 |- ~difference $A_set $Set1 $_144 \/ ~member (k $_145 $_146 $_144) $Set1 \/ % 0.46/0.62 difference $_145 $_146 $_144 \/ member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~difference $A_set $_144 $Set2 \/ ~member (k $_145 $_146 $_144) $Set2 \/ % 0.46/0.62 difference $_145 $_146 $_144 \/ member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~difference $Set1 $Set2 $_144 \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Set1 \/ member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_144 \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Set2 \/ member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_144 \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Set1 \/ member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~union $Set1 $_144 $Union \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Union \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~union $_144 $Set2 $Union \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Union \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~intersection $_144 $_144 $Intersection \/ % 0.46/0.62 difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Intersection \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~subset $_144 $Superset \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Superset \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~difference $A_set $_144 $_144 \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_145 % 0.46/0.62 |- ~difference $A_set $Set1 $_145 \/ ~member (k $_145 $_146 $_144) $Set1 \/ % 0.46/0.62 difference $_145 $_146 $_144 \/ member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~difference $A_set $_145 $Set2 \/ ~member (k $_145 $_146 $_144) $Set2 \/ % 0.46/0.62 difference $_145 $_146 $_144 \/ member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~difference $Set1 $Set2 $_145 \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Set1 \/ member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_145 \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Set2 \/ member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_145 \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Set1 \/ member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~union $Set1 $_145 $Union \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Union \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~union $_145 $Set2 $Union \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Union \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~intersection $_145 $_145 $Intersection \/ % 0.46/0.62 difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Intersection \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~subset $_145 $Superset \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $Superset \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- ~difference $A_set $_145 $_145 \/ difference $_145 $_146 $_144 \/ % 0.46/0.62 member (k $_145 $_146 $_144) $_144 % 0.46/0.62 |- difference $_149 $_149 $_147 \/ member (k $_149 $_149 $_147) $_147 % 0.46/0.62 |- ~difference $A_set $Set1 $_150 \/ ~member (k $_151 $_151 $_150) $Set1 \/ % 0.46/0.62 difference $_151 $_151 $_150 % 0.46/0.62 |- ~difference $A_set $_150 $Set2 \/ ~member (k $_151 $_151 $_150) $Set2 \/ % 0.46/0.62 difference $_151 $_151 $_150 % 0.46/0.62 |- ~difference $Set1 $Set2 $_150 \/ difference $_151 $_151 $_150 \/ % 0.46/0.62 member (k $_151 $_151 $_150) $Set1 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_150 \/ difference $_151 $_151 $_150 \/ % 0.46/0.62 member (k $_151 $_151 $_150) $Set2 % 0.46/0.62 |- ~intersection $Set1 $Set2 $_150 \/ difference $_151 $_151 $_150 \/ % 0.46/0.62 member (k $_151 $_151 $_150) $Set1 % 0.46/0.62 |- ~union $Set1 $_150 $Union \/ difference $_151 $_151 $_150 \/ % 0.46/0.62 member (k $_151 $_151 $_150) $Union % 0.46/0.62 |- ~union $_150 $Set2 $Union \/ difference $_151 $_151 $_150 \/ % 0.46/0.62 member (k $_151 $_151 $_150) $Union % 0.46/0.62 |- ~intersection $_150 $_150 $Intersection \/ % 0.46/0.62 difference $_151 $_151 $_150 \/ % 0.46/0.62 member (k $_151 $_151 $_150) $Intersection % 0.46/0.62 |- ~subset $_150 $Superset \/ difference $_151 $_151 $_150 \/ % 0.46/0.62 member (k $_151 $_151 $_150) $Superset % 0.46/0.62 |- ~difference $A_set $_150 $_150 \/ difference $_151 $_151 $_150 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ member (g $_205 $_67 $_67) $_203 \/ % 0.46/0.62 member (g $_205 $_67 $_67) $_204 \/ union $_205 $_67 $_67 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ member (g $_60 $_205 $_60) $_203 \/ % 0.46/0.62 member (g $_60 $_205 $_60) $_204 \/ union $_60 $_205 $_60 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ member (g $Set2 $Set2 $_205) $Set2 \/ % 0.46/0.62 member (g $Set2 $Set2 $_205) $_203 \/ % 0.46/0.62 member (g $Set2 $Set2 $_205) $_204 \/ union $Set2 $Set2 $_205 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ member (g $_205 $_205 $Union) $Union \/ % 0.46/0.62 member (g $_205 $_205 $Union) $_203 \/ % 0.46/0.62 member (g $_205 $_205 $Union) $_204 \/ union $_205 $_205 $Union % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ intersection $Set1 $_205 $Intersection \/ % 0.46/0.62 member (h $Set1 $_205 $Intersection) $Intersection \/ % 0.46/0.62 member (h $Set1 $_205 $Intersection) $_203 \/ % 0.46/0.62 member (h $Set1 $_205 $Intersection) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ intersection $Set1 $Set2 $_205 \/ % 0.46/0.62 member (h $Set1 $Set2 $_205) $Set2 \/ % 0.46/0.62 member (h $Set1 $Set2 $_205) $_203 \/ member (h $Set1 $Set2 $_205) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ intersection $_205 $Set2 $Intersection \/ % 0.46/0.62 member (h $_205 $Set2 $Intersection) $Intersection \/ % 0.46/0.62 member (h $_205 $Set2 $Intersection) $_203 \/ % 0.46/0.62 member (h $_205 $Set2 $Intersection) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ intersection $Set1 $Set2 $_205 \/ % 0.46/0.62 member (h $Set1 $Set2 $_205) $Set1 \/ % 0.46/0.62 member (h $Set1 $Set2 $_205) $_203 \/ member (h $Set1 $Set2 $_205) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ intersection $Set1 $_205 $_205 \/ % 0.46/0.62 member (h $Set1 $_205 $_205) $_203 \/ member (h $Set1 $_205 $_205) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ intersection $_205 $Set2 $_205 \/ % 0.46/0.62 member (h $_205 $Set2 $_205) $_203 \/ member (h $_205 $Set2 $_205) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ difference $_149 $_149 $_205 \/ % 0.46/0.62 member (k $_149 $_149 $_205) $_203 \/ member (k $_149 $_149 $_205) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ difference $_205 $Set2 $Difference \/ % 0.46/0.62 member (k $_205 $Set2 $Difference) $Difference \/ % 0.46/0.62 member (k $_205 $Set2 $Difference) $_203 \/ % 0.46/0.62 member (k $_205 $Set2 $Difference) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ difference $Set1 $Set2 $_205 \/ % 0.46/0.62 member (k $Set1 $Set2 $_205) $Set1 \/ % 0.46/0.62 member (k $Set1 $Set2 $_205) $_203 \/ member (k $Set1 $Set2 $_205) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ difference $_47 $_205 $_47 \/ % 0.46/0.62 member (k $_47 $_205 $_47) $_203 \/ member (k $_47 $_205 $_47) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ difference $_205 $Set2 $_205 \/ % 0.46/0.62 member (k $_205 $Set2 $_205) $_203 \/ member (k $_205 $Set2 $_205) $_204 % 0.46/0.62 |- ~union $_203 $_204 $_205 \/ % 0.46/0.62 member (member_of_1_not_of_2 $_205 $Superset) $_203 \/ % 0.46/0.62 member (member_of_1_not_of_2 $_205 $Superset) $_204 \/ % 0.46/0.62 subset $_205 $Superset % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ ~member (g $_208 $_67 $_67) $_209 \/ % 0.46/0.62 member (g $_208 $_67 $_67) $_207 \/ union $_208 $_67 $_67 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ ~member (g $_60 $_208 $_60) $_209 \/ % 0.46/0.62 member (g $_60 $_208 $_60) $_207 \/ union $_60 $_208 $_60 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (g $Set2 $Set2 $_208) $_209 \/ % 0.46/0.62 member (g $Set2 $Set2 $_208) $Set2 \/ % 0.46/0.62 member (g $Set2 $Set2 $_208) $_207 \/ union $Set2 $Set2 $_208 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (g $_208 $_208 $Union) $_209 \/ % 0.46/0.62 member (g $_208 $_208 $Union) $Union \/ % 0.46/0.62 member (g $_208 $_208 $Union) $_207 \/ union $_208 $_208 $Union % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $Set1 $_208 $Intersection) $_209 \/ % 0.46/0.62 intersection $Set1 $_208 $Intersection \/ % 0.46/0.62 member (h $Set1 $_208 $Intersection) $Intersection \/ % 0.46/0.62 member (h $Set1 $_208 $Intersection) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $Set1 $Set2 $_208) $_209 \/ intersection $Set1 $Set2 $_208 \/ % 0.46/0.62 member (h $Set1 $Set2 $_208) $Set2 \/ member (h $Set1 $Set2 $_208) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $_208 $Set2 $Intersection) $_209 \/ % 0.46/0.62 intersection $_208 $Set2 $Intersection \/ % 0.46/0.62 member (h $_208 $Set2 $Intersection) $Intersection \/ % 0.46/0.62 member (h $_208 $Set2 $Intersection) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $Set1 $Set2 $_208) $_209 \/ intersection $Set1 $Set2 $_208 \/ % 0.46/0.62 member (h $Set1 $Set2 $_208) $Set1 \/ member (h $Set1 $Set2 $_208) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $Set1 $_208 $_208) $_209 \/ intersection $Set1 $_208 $_208 \/ % 0.46/0.62 member (h $Set1 $_208 $_208) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $_208 $Set2 $_208) $_209 \/ intersection $_208 $Set2 $_208 \/ % 0.46/0.62 member (h $_208 $Set2 $_208) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (k $_149 $_149 $_208) $_209 \/ difference $_149 $_149 $_208 \/ % 0.46/0.62 member (k $_149 $_149 $_208) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (k $_208 $Set2 $Difference) $_209 \/ % 0.46/0.62 difference $_208 $Set2 $Difference \/ % 0.46/0.62 member (k $_208 $Set2 $Difference) $Difference \/ % 0.46/0.62 member (k $_208 $Set2 $Difference) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (k $Set1 $Set2 $_208) $_209 \/ difference $Set1 $Set2 $_208 \/ % 0.46/0.62 member (k $Set1 $Set2 $_208) $Set1 \/ member (k $Set1 $Set2 $_208) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ ~member (k $_47 $_208 $_47) $_209 \/ % 0.46/0.62 difference $_47 $_208 $_47 \/ member (k $_47 $_208 $_47) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (k $_208 $Set2 $_208) $_209 \/ difference $_208 $Set2 $_208 \/ % 0.46/0.62 member (k $_208 $Set2 $_208) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (member_of_1_not_of_2 $_208 $Superset) $_209 \/ % 0.46/0.62 member (member_of_1_not_of_2 $_208 $Superset) $_207 \/ % 0.46/0.62 subset $_208 $Superset % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ ~member (g $_209 $_67 $_67) $_208 \/ % 0.46/0.62 member (g $_209 $_67 $_67) $_207 \/ union $_209 $_67 $_67 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ ~member (g $_60 $_209 $_60) $_208 \/ % 0.46/0.62 member (g $_60 $_209 $_60) $_207 \/ union $_60 $_209 $_60 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (g $Set2 $Set2 $_209) $_208 \/ % 0.46/0.62 member (g $Set2 $Set2 $_209) $Set2 \/ % 0.46/0.62 member (g $Set2 $Set2 $_209) $_207 \/ union $Set2 $Set2 $_209 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (g $_209 $_209 $Union) $_208 \/ % 0.46/0.62 member (g $_209 $_209 $Union) $Union \/ % 0.46/0.62 member (g $_209 $_209 $Union) $_207 \/ union $_209 $_209 $Union % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $Set1 $_209 $Intersection) $_208 \/ % 0.46/0.62 intersection $Set1 $_209 $Intersection \/ % 0.46/0.62 member (h $Set1 $_209 $Intersection) $Intersection \/ % 0.46/0.62 member (h $Set1 $_209 $Intersection) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $Set1 $Set2 $_209) $_208 \/ intersection $Set1 $Set2 $_209 \/ % 0.46/0.62 member (h $Set1 $Set2 $_209) $Set2 \/ member (h $Set1 $Set2 $_209) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $_209 $Set2 $Intersection) $_208 \/ % 0.46/0.62 intersection $_209 $Set2 $Intersection \/ % 0.46/0.62 member (h $_209 $Set2 $Intersection) $Intersection \/ % 0.46/0.62 member (h $_209 $Set2 $Intersection) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $Set1 $Set2 $_209) $_208 \/ intersection $Set1 $Set2 $_209 \/ % 0.46/0.62 member (h $Set1 $Set2 $_209) $Set1 \/ member (h $Set1 $Set2 $_209) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $Set1 $_209 $_209) $_208 \/ intersection $Set1 $_209 $_209 \/ % 0.46/0.62 member (h $Set1 $_209 $_209) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (h $_209 $Set2 $_209) $_208 \/ intersection $_209 $Set2 $_209 \/ % 0.46/0.62 member (h $_209 $Set2 $_209) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (k $_149 $_149 $_209) $_208 \/ difference $_149 $_149 $_209 \/ % 0.46/0.62 member (k $_149 $_149 $_209) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (k $_209 $Set2 $Difference) $_208 \/ % 0.46/0.62 difference $_209 $Set2 $Difference \/ % 0.46/0.62 member (k $_209 $Set2 $Difference) $Difference \/ % 0.46/0.62 member (k $_209 $Set2 $Difference) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (k $Set1 $Set2 $_209) $_208 \/ difference $Set1 $Set2 $_209 \/ % 0.46/0.62 member (k $Set1 $Set2 $_209) $Set1 \/ member (k $Set1 $Set2 $_209) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ ~member (k $_47 $_209 $_47) $_208 \/ % 0.46/0.62 difference $_47 $_209 $_47 \/ member (k $_47 $_209 $_47) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (k $_209 $Set2 $_209) $_208 \/ difference $_209 $Set2 $_209 \/ % 0.46/0.62 member (k $_209 $Set2 $_209) $_207 % 0.46/0.62 |- ~intersection $_208 $_209 $_207 \/ % 0.46/0.62 ~member (member_of_1_not_of_2 $_209 $Superset) $_208 \/ % 0.46/0.62 member (member_of_1_not_of_2 $_209 $Superset) $_207 \/ % 0.46/0.62 subset $_209 $Superset % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ member (g $_212 $_67 $_67) $_210 \/ % 0.46/0.62 member (g $_212 $_67 $_67) $_213 \/ union $_212 $_67 $_67 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ member (g $_60 $_212 $_60) $_210 \/ % 0.46/0.62 member (g $_60 $_212 $_60) $_213 \/ union $_60 $_212 $_60 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ member (g $Set2 $Set2 $_212) $Set2 \/ % 0.46/0.62 member (g $Set2 $Set2 $_212) $_210 \/ % 0.46/0.62 member (g $Set2 $Set2 $_212) $_213 \/ union $Set2 $Set2 $_212 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ member (g $_212 $_212 $Union) $Union \/ % 0.46/0.62 member (g $_212 $_212 $Union) $_210 \/ % 0.46/0.62 member (g $_212 $_212 $Union) $_213 \/ union $_212 $_212 $Union % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ % 0.46/0.62 intersection $Set1 $_212 $Intersection \/ % 0.46/0.62 member (h $Set1 $_212 $Intersection) $Intersection \/ % 0.46/0.62 member (h $Set1 $_212 $Intersection) $_210 \/ % 0.46/0.62 member (h $Set1 $_212 $Intersection) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ intersection $Set1 $Set2 $_212 \/ % 0.46/0.62 member (h $Set1 $Set2 $_212) $Set2 \/ % 0.46/0.62 member (h $Set1 $Set2 $_212) $_210 \/ member (h $Set1 $Set2 $_212) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ % 0.46/0.62 intersection $_212 $Set2 $Intersection \/ % 0.46/0.62 member (h $_212 $Set2 $Intersection) $Intersection \/ % 0.46/0.62 member (h $_212 $Set2 $Intersection) $_210 \/ % 0.46/0.62 member (h $_212 $Set2 $Intersection) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ intersection $Set1 $Set2 $_212 \/ % 0.46/0.62 member (h $Set1 $Set2 $_212) $Set1 \/ % 0.46/0.62 member (h $Set1 $Set2 $_212) $_210 \/ member (h $Set1 $Set2 $_212) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ intersection $Set1 $_212 $_212 \/ % 0.46/0.62 member (h $Set1 $_212 $_212) $_210 \/ member (h $Set1 $_212 $_212) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ intersection $_212 $Set2 $_212 \/ % 0.46/0.62 member (h $_212 $Set2 $_212) $_210 \/ member (h $_212 $Set2 $_212) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ difference $_149 $_149 $_212 \/ % 0.46/0.62 member (k $_149 $_149 $_212) $_210 \/ member (k $_149 $_149 $_212) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ difference $_212 $Set2 $Difference \/ % 0.46/0.62 member (k $_212 $Set2 $Difference) $Difference \/ % 0.46/0.62 member (k $_212 $Set2 $Difference) $_210 \/ % 0.46/0.62 member (k $_212 $Set2 $Difference) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ difference $Set1 $Set2 $_212 \/ % 0.46/0.62 member (k $Set1 $Set2 $_212) $Set1 \/ % 0.46/0.62 member (k $Set1 $Set2 $_212) $_210 \/ member (k $Set1 $Set2 $_212) $_213 % 0.46/0.62 |- ~difference $_212 $_213 $_210 \/ difference $_47 $_212 $_47 \/ % 0.46/0.62 member (k $_47 $_212 $_47) $_210 \/ member (k $_47 $_212 $_47) $_213 % 0.46/0.63 |- ~difference $_212 $_213 $_210 \/ difference $_212 $Set2 $_212 \/ % 0.46/0.63 member (k $_212 $Set2 $_212) $_210 \/ member (k $_212 $Set2 $_212) $_213 % 0.46/0.63 |- ~difference $_212 $_213 $_210 \/ % 0.46/0.63 member (member_of_1_not_of_2 $_212 $Superset) $_210 \/ % 0.46/0.63 member (member_of_1_not_of_2 $_212 $Superset) $_213 \/ % 0.46/0.63 subset $_212 $Superset % 0.46/0.63 |- ~difference $_391 $Set2 $Difference \/ % 0.46/0.63 member (g $_391 $_392 $_393) $Difference \/ % 0.46/0.63 member (g $_391 $_392 $_393) $Set2 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.46/0.63 |- ~intersection $Set1 $_391 $Intersection \/ % 0.46/0.63 ~member (g $_391 $_392 $_393) $Set1 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.46/0.63 |- ~intersection $_391 $Set2 $Intersection \/ % 0.46/0.63 ~member (g $_391 $_392 $_393) $Set2 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.46/0.63 |- ~union $Set1 $Set2 $_391 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $Set2 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.46/0.63 |- ~difference $A_set $Set1 $_391 \/ ~member (g $_391 $_392 $_393) $Set1 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.46/0.63 |- ~difference $A_set $_391 $Set2 \/ ~member (g $_391 $_392 $_393) $Set2 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.46/0.63 |- ~difference $Set1 $Set2 $_391 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.46/0.63 |- ~intersection $Set1 $Set2 $_391 \/ member (g $_391 $_392 $_393) $Set2 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.46/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $Set1 $Set2 $_391 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~union $Set1 $_391 $Union \/ member (g $_391 $_392 $_393) $Union \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~union $_391 $Set2 $Union \/ member (g $_391 $_392 $_393) $Union \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $_391 $_391 $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~subset $_391 $Superset \/ member (g $_391 $_392 $_393) $Superset \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $A_set $_391 $_391 \/ member (g $_391 $_392 $_393) $_392 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $_392 $Set2 $Difference \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Difference \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $Set1 $_392 $Intersection \/ % 0.49/0.63 ~member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $_392 $Set2 $Intersection \/ % 0.49/0.63 ~member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~union $Set1 $Set2 $_392 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $A_set $Set1 $_392 \/ ~member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $A_set $_392 $Set2 \/ ~member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $Set1 $Set2 $_392 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $Set1 $Set2 $_392 \/ member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $Set1 $Set2 $_392 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~union $Set1 $_392 $Union \/ member (g $_391 $_392 $_393) $Union \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~union $_392 $Set2 $Union \/ member (g $_391 $_392 $_393) $Union \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $_392 $_392 $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~subset $_392 $Superset \/ member (g $_391 $_392 $_393) $Superset \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $A_set $_392 $_392 \/ member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_393 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $_393 $Set2 $Difference \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Difference \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $Set1 $_393 $Intersection \/ % 0.49/0.63 ~member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $_393 $Set2 $Intersection \/ % 0.49/0.63 ~member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~union $Set1 $Set2 $_393 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $A_set $Set1 $_393 \/ ~member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $A_set $_393 $Set2 \/ ~member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $Set1 $Set2 $_393 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $Set1 $Set2 $_393 \/ member (g $_391 $_392 $_393) $Set2 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $Set1 $Set2 $_393 \/ member (g $_391 $_392 $_393) $Set1 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~union $Set1 $_393 $Union \/ member (g $_391 $_392 $_393) $Union \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~union $_393 $Set2 $Union \/ member (g $_391 $_392 $_393) $Union \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~intersection $_393 $_393 $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $Intersection \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~subset $_393 $Superset \/ member (g $_391 $_392 $_393) $Superset \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $A_set $_393 $_393 \/ member (g $_391 $_392 $_393) $_391 \/ % 0.49/0.63 member (g $_391 $_392 $_393) $_392 \/ union $_391 $_392 $_393 % 0.49/0.63 |- ~difference $_408 $_409 $_410 \/ difference $_409 $_410 $_409 % 0.49/0.63 |- ~intersection $_707 $_708 $_706 \/ difference $_708 $_707 $_708 \/ % 0.49/0.63 member (k $_708 $_707 $_708) $_706 % 0.49/0.63 |- ~intersection $_715 $_716 $_714 \/ difference $_715 $_716 $_715 \/ % 0.49/0.63 member (k $_715 $_716 $_715) $_714 % 0.49/0.63 |- ~difference $_796 $_797 $_799 \/ intersection $_799 $_797 $_798 \/ % 0.49/0.63 member (h $_799 $_797 $_798) $_798 % 0.49/0.63 |- ~difference $_805 $_808 $_806 \/ intersection $_808 $_806 $_807 \/ % 0.49/0.63 member (h $_808 $_806 $_807) $_807 % 0.49/0.63 |- ~intersection $_1078 $_1079 $_1077 \/ % 0.49/0.63 intersection $_1079 $_1078 $_1075 \/ % 0.49/0.63 member (h $_1079 $_1078 $_1075) $_1075 \/ % 0.49/0.63 member (h $_1079 $_1078 $_1075) $_1077 % 0.49/0.63 |- ~intersection $_1092 $_1093 $_1091 \/ % 0.49/0.63 intersection $_1092 $_1093 $_1089 \/ % 0.49/0.63 member (h $_1092 $_1093 $_1089) $_1089 \/ % 0.49/0.63 member (h $_1092 $_1093 $_1089) $_1091 % 0.49/0.63 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.49/0.63 %------------------------------------------------------------------------------