%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SET779-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n022.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 03:37:09 EDT 2022 % Result : Satisfiable 0.19s 0.39s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET779-1 : TPTP v8.1.0. Released v2.5.0. % 0.03/0.13 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n022.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.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jul 10 22:45:55 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.19/0.39 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.39 % 0.19/0.39 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.39 |- ~member $Element $Subset \/ ~subset $Subset $Superset \/ % 0.19/0.39 member $Element $Superset % 0.19/0.39 |- member (member_of_1_not_of_2 $Subset $Superset) $Subset \/ % 0.19/0.39 subset $Subset $Superset % 0.19/0.39 |- ~member (member_of_1_not_of_2 $Subset $Superset) $Superset \/ % 0.19/0.39 subset $Subset $Superset % 0.19/0.39 |- ~equal_sets $Subset $Superset \/ subset $Subset $Superset % 0.19/0.39 |- ~equal_sets $Superset $Subset \/ subset $Subset $Superset % 0.19/0.39 |- ~subset $Set1 $Set2 \/ ~subset $Set2 $Set1 \/ equal_sets $Set2 $Set1 % 0.19/0.39 |- ~intersection $Set1 $Set2 $Intersection \/ % 0.19/0.39 ~member $Element $Intersection \/ member $Element $Set1 % 0.19/0.39 |- ~intersection $Set1 $Set2 $Intersection \/ % 0.19/0.39 ~member $Element $Intersection \/ member $Element $Set2 % 0.19/0.39 |- ~intersection $Set1 $Set2 $Intersection \/ ~member $Element $Set1 \/ % 0.19/0.39 ~member $Element $Set2 \/ member $Element $Intersection % 0.19/0.39 |- intersection $Set1 $Set2 $Intersection \/ % 0.19/0.39 member (h $Set1 $Set2 $Intersection) $Intersection \/ % 0.19/0.39 member (h $Set1 $Set2 $Intersection) $Set1 % 0.19/0.39 |- intersection $Set1 $Set2 $Intersection \/ % 0.19/0.39 member (h $Set1 $Set2 $Intersection) $Intersection \/ % 0.19/0.39 member (h $Set1 $Set2 $Intersection) $Set2 % 0.19/0.40 |- ~member (h $Set1 $Set2 $Intersection) $Intersection \/ % 0.19/0.40 ~member (h $Set1 $Set2 $Intersection) $Set1 \/ % 0.19/0.40 ~member (h $Set1 $Set2 $Intersection) $Set2 \/ % 0.19/0.40 intersection $Set1 $Set2 $Intersection % 0.19/0.40 |- intersection $Set1 $Set2 $Set1 \/ member (h $Set1 $Set2 $Set1) $Set1 % 0.19/0.40 |- intersection $Set1 $Set2 $Set2 \/ member (h $Set1 $Set2 $Set2) $Set2 % 0.19/0.40 |- ~intersection $Set2 $Set2 $Intersection \/ ~member $Element $Set2 \/ % 0.19/0.40 member $Element $Intersection % 0.19/0.40 |- ~member (h $Set2 $Set2 $Intersection) $Intersection \/ % 0.19/0.40 ~member (h $Set2 $Set2 $Intersection) $Set2 \/ % 0.19/0.40 intersection $Set2 $Set2 $Intersection % 0.19/0.40 |- subset $_9 $_9 % 0.19/0.40 |- equal_sets $_10 $_10 % 0.19/0.40 |- intersection $_13 $_13 $_13 % 0.19/0.40 |- ~subset $_20 $_21 \/ intersection $Set1 $_20 $_20 \/ % 0.19/0.40 member (h $Set1 $_20 $_20) $_21 % 0.19/0.40 |- ~subset $_20 $_21 \/ intersection $_20 $Set2 $_20 \/ % 0.19/0.40 member (h $_20 $Set2 $_20) $_21 % 0.19/0.40 |- ~subset $_20 $_21 \/ % 0.19/0.40 member (member_of_1_not_of_2 $_20 $Superset) $_21 \/ % 0.19/0.40 subset $_20 $Superset % 0.19/0.40 |- ~intersection $_24 $_24 $_23 \/ intersection $Set1 $_24 $_24 \/ % 0.19/0.40 member (h $Set1 $_24 $_24) $_23 % 0.19/0.40 |- ~intersection $_24 $_24 $_23 \/ intersection $_24 $Set2 $_24 \/ % 0.19/0.40 member (h $_24 $Set2 $_24) $_23 % 0.19/0.40 |- ~intersection $_24 $_24 $_23 \/ % 0.19/0.40 member (member_of_1_not_of_2 $_24 $Superset) $_23 \/ % 0.19/0.40 subset $_24 $Superset % 0.19/0.40 |- ~member (h $_25 $_26 $_25) $_26 \/ intersection $_25 $_26 $_25 % 0.19/0.40 |- ~member (h $_29 $_30 $_30) $_29 \/ intersection $_29 $_30 $_30 % 0.19/0.40 |- ~intersection $_37 $_38 $_36 \/ intersection $Set1 $_36 $_36 \/ % 0.19/0.40 member (h $Set1 $_36 $_36) $_37 % 0.19/0.40 |- ~intersection $_37 $_38 $_36 \/ intersection $_36 $Set2 $_36 \/ % 0.19/0.40 member (h $_36 $Set2 $_36) $_37 % 0.19/0.40 |- ~intersection $_37 $_38 $_36 \/ % 0.19/0.40 member (member_of_1_not_of_2 $_36 $Superset) $_37 \/ % 0.19/0.40 subset $_36 $Superset % 0.19/0.40 |- ~intersection $_45 $_46 $_44 \/ intersection $Set1 $_44 $_44 \/ % 0.19/0.40 member (h $Set1 $_44 $_44) $_46 % 0.19/0.40 |- ~intersection $_45 $_46 $_44 \/ intersection $_44 $Set2 $_44 \/ % 0.19/0.40 member (h $_44 $Set2 $_44) $_46 % 0.19/0.40 |- ~intersection $_45 $_46 $_44 \/ % 0.19/0.40 member (member_of_1_not_of_2 $_44 $Superset) $_46 \/ % 0.19/0.40 subset $_44 $Superset % 0.19/0.40 |- ~intersection $Set1 $Set2 $_53 \/ intersection $_54 $_55 $_53 \/ % 0.19/0.40 member (h $_54 $_55 $_53) $Set2 \/ member (h $_54 $_55 $_53) $_54 % 0.19/0.40 |- ~intersection $Set1 $Set2 $_53 \/ intersection $_54 $_55 $_53 \/ % 0.19/0.40 member (h $_54 $_55 $_53) $Set1 \/ member (h $_54 $_55 $_53) $_54 % 0.19/0.40 |- ~intersection $_53 $_53 $Intersection \/ intersection $_54 $_55 $_53 \/ % 0.19/0.40 member (h $_54 $_55 $_53) $Intersection \/ % 0.19/0.40 member (h $_54 $_55 $_53) $_54 % 0.19/0.40 |- ~subset $_53 $Superset \/ intersection $_54 $_55 $_53 \/ % 0.19/0.40 member (h $_54 $_55 $_53) $Superset \/ member (h $_54 $_55 $_53) $_54 % 0.19/0.40 |- ~intersection $Set1 $Set2 $_54 \/ intersection $_54 $_55 $_53 \/ % 0.19/0.40 member (h $_54 $_55 $_53) $Set2 \/ member (h $_54 $_55 $_53) $_53 % 0.19/0.40 |- ~intersection $Set1 $Set2 $_54 \/ intersection $_54 $_55 $_53 \/ % 0.19/0.40 member (h $_54 $_55 $_53) $Set1 \/ member (h $_54 $_55 $_53) $_53 % 0.19/0.40 |- ~intersection $_54 $_54 $Intersection \/ intersection $_54 $_55 $_53 \/ % 0.19/0.40 member (h $_54 $_55 $_53) $Intersection \/ % 0.19/0.40 member (h $_54 $_55 $_53) $_53 % 0.19/0.40 |- ~subset $_54 $Superset \/ intersection $_54 $_55 $_53 \/ % 0.19/0.40 member (h $_54 $_55 $_53) $Superset \/ member (h $_54 $_55 $_53) $_53 % 0.19/0.40 |- ~intersection $Set1 $Set2 $_56 \/ intersection $_57 $_58 $_56 \/ % 0.19/0.40 member (h $_57 $_58 $_56) $Set2 \/ member (h $_57 $_58 $_56) $_58 % 0.19/0.40 |- ~intersection $Set1 $Set2 $_56 \/ intersection $_57 $_58 $_56 \/ % 0.19/0.40 member (h $_57 $_58 $_56) $Set1 \/ member (h $_57 $_58 $_56) $_58 % 0.19/0.40 |- ~intersection $_56 $_56 $Intersection \/ intersection $_57 $_58 $_56 \/ % 0.19/0.40 member (h $_57 $_58 $_56) $Intersection \/ % 0.19/0.40 member (h $_57 $_58 $_56) $_58 % 0.19/0.40 |- ~subset $_56 $Superset \/ intersection $_57 $_58 $_56 \/ % 0.19/0.40 member (h $_57 $_58 $_56) $Superset \/ member (h $_57 $_58 $_56) $_58 % 0.19/0.40 |- ~intersection $Set1 $Set2 $_58 \/ intersection $_57 $_58 $_56 \/ % 0.19/0.40 member (h $_57 $_58 $_56) $Set2 \/ member (h $_57 $_58 $_56) $_56 % 0.19/0.40 |- ~intersection $Set1 $Set2 $_58 \/ intersection $_57 $_58 $_56 \/ % 0.19/0.40 member (h $_57 $_58 $_56) $Set1 \/ member (h $_57 $_58 $_56) $_56 % 0.19/0.40 |- ~intersection $_58 $_58 $Intersection \/ intersection $_57 $_58 $_56 \/ % 0.19/0.40 member (h $_57 $_58 $_56) $Intersection \/ % 0.19/0.40 member (h $_57 $_58 $_56) $_56 % 0.19/0.40 |- ~subset $_58 $Superset \/ intersection $_57 $_58 $_56 \/ % 0.19/0.40 member (h $_57 $_58 $_56) $Superset \/ member (h $_57 $_58 $_56) $_56 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ % 0.19/0.40 ~member (h $Set1 $_81 $Intersection) $_82 \/ % 0.19/0.40 intersection $Set1 $_81 $Intersection \/ % 0.19/0.40 member (h $Set1 $_81 $Intersection) $Intersection \/ % 0.19/0.40 member (h $Set1 $_81 $Intersection) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ ~member (h $Set1 $Set2 $_81) $_82 \/ % 0.19/0.40 intersection $Set1 $Set2 $_81 \/ member (h $Set1 $Set2 $_81) $Set2 \/ % 0.19/0.40 member (h $Set1 $Set2 $_81) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ % 0.19/0.40 ~member (h $_81 $Set2 $Intersection) $_82 \/ % 0.19/0.40 intersection $_81 $Set2 $Intersection \/ % 0.19/0.40 member (h $_81 $Set2 $Intersection) $Intersection \/ % 0.19/0.40 member (h $_81 $Set2 $Intersection) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ ~member (h $Set1 $Set2 $_81) $_82 \/ % 0.19/0.40 intersection $Set1 $Set2 $_81 \/ member (h $Set1 $Set2 $_81) $Set1 \/ % 0.19/0.40 member (h $Set1 $Set2 $_81) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ ~member (h $Set1 $_81 $_81) $_82 \/ % 0.19/0.40 intersection $Set1 $_81 $_81 \/ member (h $Set1 $_81 $_81) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ ~member (h $_81 $Set2 $_81) $_82 \/ % 0.19/0.40 intersection $_81 $Set2 $_81 \/ member (h $_81 $Set2 $_81) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ % 0.19/0.40 ~member (member_of_1_not_of_2 $_81 $Superset) $_82 \/ % 0.19/0.40 member (member_of_1_not_of_2 $_81 $Superset) $_80 \/ % 0.19/0.40 subset $_81 $Superset % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ % 0.19/0.40 ~member (h $Set1 $_82 $Intersection) $_81 \/ % 0.19/0.40 intersection $Set1 $_82 $Intersection \/ % 0.19/0.40 member (h $Set1 $_82 $Intersection) $Intersection \/ % 0.19/0.40 member (h $Set1 $_82 $Intersection) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ ~member (h $Set1 $Set2 $_82) $_81 \/ % 0.19/0.40 intersection $Set1 $Set2 $_82 \/ member (h $Set1 $Set2 $_82) $Set2 \/ % 0.19/0.40 member (h $Set1 $Set2 $_82) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ % 0.19/0.40 ~member (h $_82 $Set2 $Intersection) $_81 \/ % 0.19/0.40 intersection $_82 $Set2 $Intersection \/ % 0.19/0.40 member (h $_82 $Set2 $Intersection) $Intersection \/ % 0.19/0.40 member (h $_82 $Set2 $Intersection) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ ~member (h $Set1 $Set2 $_82) $_81 \/ % 0.19/0.40 intersection $Set1 $Set2 $_82 \/ member (h $Set1 $Set2 $_82) $Set1 \/ % 0.19/0.40 member (h $Set1 $Set2 $_82) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ ~member (h $Set1 $_82 $_82) $_81 \/ % 0.19/0.40 intersection $Set1 $_82 $_82 \/ member (h $Set1 $_82 $_82) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ ~member (h $_82 $Set2 $_82) $_81 \/ % 0.19/0.40 intersection $_82 $Set2 $_82 \/ member (h $_82 $Set2 $_82) $_80 % 0.19/0.40 |- ~intersection $_81 $_82 $_80 \/ % 0.19/0.40 ~member (member_of_1_not_of_2 $_82 $Superset) $_81 \/ % 0.19/0.40 member (member_of_1_not_of_2 $_82 $Superset) $_80 \/ % 0.19/0.40 subset $_82 $Superset % 0.19/0.40 |- ~intersection $_207 $_208 $_206 \/ intersection $_208 $_207 $_204 \/ % 0.19/0.40 member (h $_208 $_207 $_204) $_204 \/ member (h $_208 $_207 $_204) $_206 % 0.19/0.40 |- ~intersection $_216 $_217 $_215 \/ intersection $_216 $_217 $_213 \/ % 0.19/0.40 member (h $_216 $_217 $_213) $_213 \/ member (h $_216 $_217 $_213) $_215 % 0.19/0.40 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.40 %------------------------------------------------------------------------------