%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SET780-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n023.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.12s 0.36s % Output : Saturation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SET780-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n023.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 : Sun Jul 10 16:28:10 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.12/0.36 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.36 % 0.12/0.36 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.36 |- ~member $Element $Subset \/ ~subset $Subset $Superset \/ % 0.12/0.36 member $Element $Superset % 0.12/0.36 |- member (member_of_1_not_of_2 $Subset $Superset) $Subset \/ % 0.12/0.36 subset $Subset $Superset % 0.12/0.36 |- ~member (member_of_1_not_of_2 $Subset $Superset) $Superset \/ % 0.12/0.36 subset $Subset $Superset % 0.12/0.36 |- ~equal_sets $Subset $Superset \/ subset $Subset $Superset % 0.12/0.37 |- ~equal_sets $Superset $Subset \/ subset $Subset $Superset % 0.12/0.37 |- ~subset $Set1 $Set2 \/ ~subset $Set2 $Set1 \/ equal_sets $Set2 $Set1 % 0.12/0.37 |- ~difference $Set1 $Set2 $Difference \/ ~member $Element $Difference \/ % 0.12/0.37 member $Element $Set1 % 0.12/0.37 |- ~difference $A_set $Set1 $Set2 \/ ~member $Element $Set1 \/ % 0.12/0.37 ~member $Element $Set2 % 0.12/0.37 |- ~difference $Set1 $Set2 $Difference \/ ~member $Element $Set1 \/ % 0.12/0.37 member $Element $Difference \/ member $Element $Set2 % 0.12/0.37 |- difference $Set1 $Set2 $Difference \/ % 0.12/0.37 member (k $Set1 $Set2 $Difference) $Difference \/ % 0.12/0.37 member (k $Set1 $Set2 $Difference) $Set1 % 0.12/0.37 |- ~member (k $Set1 $Set2 $Difference) $Set2 \/ % 0.12/0.37 difference $Set1 $Set2 $Difference \/ % 0.12/0.37 member (k $Set1 $Set2 $Difference) $Difference % 0.12/0.37 |- ~member (k $Set1 $Set2 $Difference) $Difference \/ % 0.12/0.37 ~member (k $Set1 $Set2 $Difference) $Set1 \/ % 0.12/0.37 difference $Set1 $Set2 $Difference \/ % 0.12/0.37 member (k $Set1 $Set2 $Difference) $Set2 % 0.12/0.37 |- ~difference $A_set $Set2 $Set2 \/ ~member $Element $Set2 % 0.12/0.37 |- difference $Set1 $Set2 $Set1 \/ member (k $Set1 $Set2 $Set1) $Set1 % 0.12/0.37 |- subset $_8 $_8 % 0.12/0.37 |- equal_sets $_9 $_9 % 0.12/0.37 |- ~difference $_11 $_13 $_13 \/ subset $_13 $Superset % 0.12/0.37 |- ~difference $A_set $_17 $_17 \/ difference $_17 $_18 $_17 % 0.12/0.37 |- difference $_22 $_23 $_22 \/ member (k $_22 $_23 $_22) $_23 % 0.12/0.37 |- ~difference $A_set $_25 $_25 \/ difference $_24 $_25 $_24 % 0.12/0.37 |- ~subset $_32 $_33 \/ difference $_22 $_32 $_22 \/ % 0.12/0.37 member (k $_22 $_32 $_22) $_33 % 0.12/0.37 |- ~subset $_32 $_33 \/ difference $_32 $Set2 $_32 \/ % 0.12/0.37 member (k $_32 $Set2 $_32) $_33 % 0.12/0.37 |- ~subset $_32 $_33 \/ % 0.12/0.37 member (member_of_1_not_of_2 $_32 $Superset) $_33 \/ % 0.12/0.37 subset $_32 $Superset % 0.12/0.37 |- ~difference $_36 $_37 $_34 \/ difference $_22 $_34 $_22 \/ % 0.12/0.37 member (k $_22 $_34 $_22) $_36 % 0.12/0.37 |- ~difference $_36 $_37 $_34 \/ difference $_34 $Set2 $_34 \/ % 0.12/0.37 member (k $_34 $Set2 $_34) $_36 % 0.12/0.37 |- ~difference $_36 $_37 $_34 \/ % 0.12/0.37 member (member_of_1_not_of_2 $_34 $Superset) $_36 \/ % 0.12/0.37 subset $_34 $Superset % 0.12/0.37 |- ~difference $_38 $_40 $_41 \/ ~member (k $_22 $_40 $_22) $_41 \/ % 0.12/0.37 difference $_22 $_40 $_22 % 0.12/0.37 |- ~difference $_38 $_40 $_41 \/ ~member (k $_40 $Set2 $_40) $_41 \/ % 0.12/0.37 difference $_40 $Set2 $_40 % 0.12/0.37 |- ~difference $_38 $_40 $_41 \/ % 0.12/0.37 ~member (member_of_1_not_of_2 $_40 $Superset) $_41 \/ % 0.12/0.37 subset $_40 $Superset % 0.12/0.37 |- ~difference $_38 $_40 $_41 \/ ~member (k $_22 $_41 $_22) $_40 \/ % 0.12/0.37 difference $_22 $_41 $_22 % 0.12/0.37 |- ~difference $_38 $_40 $_41 \/ ~member (k $_41 $Set2 $_41) $_40 \/ % 0.12/0.37 difference $_41 $Set2 $_41 % 0.12/0.37 |- ~difference $_38 $_40 $_41 \/ % 0.12/0.37 ~member (member_of_1_not_of_2 $_41 $Superset) $_40 \/ % 0.12/0.37 subset $_41 $Superset % 0.12/0.37 |- ~difference $A_set $Set1 $_48 \/ ~member (k $_49 $_50 $_48) $Set1 \/ % 0.12/0.37 difference $_49 $_50 $_48 \/ member (k $_49 $_50 $_48) $_49 % 0.12/0.37 |- ~difference $A_set $_48 $Set2 \/ ~member (k $_49 $_50 $_48) $Set2 \/ % 0.12/0.37 difference $_49 $_50 $_48 \/ member (k $_49 $_50 $_48) $_49 % 0.12/0.37 |- ~difference $Set1 $Set2 $_48 \/ difference $_49 $_50 $_48 \/ % 0.12/0.37 member (k $_49 $_50 $_48) $Set1 \/ member (k $_49 $_50 $_48) $_49 % 0.12/0.37 |- ~subset $_48 $Superset \/ difference $_49 $_50 $_48 \/ % 0.12/0.37 member (k $_49 $_50 $_48) $Superset \/ member (k $_49 $_50 $_48) $_49 % 0.12/0.37 |- ~difference $A_set $_48 $_48 \/ difference $_49 $_50 $_48 \/ % 0.12/0.37 member (k $_49 $_50 $_48) $_49 % 0.12/0.37 |- ~difference $A_set $Set1 $_49 \/ ~member (k $_49 $_50 $_48) $Set1 \/ % 0.12/0.37 difference $_49 $_50 $_48 \/ member (k $_49 $_50 $_48) $_48 % 0.12/0.37 |- ~difference $A_set $_49 $Set2 \/ ~member (k $_49 $_50 $_48) $Set2 \/ % 0.12/0.37 difference $_49 $_50 $_48 \/ member (k $_49 $_50 $_48) $_48 % 0.12/0.37 |- ~difference $Set1 $Set2 $_49 \/ difference $_49 $_50 $_48 \/ % 0.12/0.37 member (k $_49 $_50 $_48) $Set1 \/ member (k $_49 $_50 $_48) $_48 % 0.12/0.37 |- ~subset $_49 $Superset \/ difference $_49 $_50 $_48 \/ % 0.12/0.37 member (k $_49 $_50 $_48) $Superset \/ member (k $_49 $_50 $_48) $_48 % 0.12/0.37 |- ~difference $A_set $_49 $_49 \/ difference $_49 $_50 $_48 \/ % 0.12/0.37 member (k $_49 $_50 $_48) $_48 % 0.12/0.37 |- difference $_53 $_53 $_51 \/ member (k $_53 $_53 $_51) $_51 % 0.12/0.37 |- ~difference $A_set $Set1 $_54 \/ ~member (k $_55 $_55 $_54) $Set1 \/ % 0.12/0.37 difference $_55 $_55 $_54 % 0.12/0.37 |- ~difference $A_set $_54 $Set2 \/ ~member (k $_55 $_55 $_54) $Set2 \/ % 0.12/0.37 difference $_55 $_55 $_54 % 0.12/0.37 |- ~difference $Set1 $Set2 $_54 \/ difference $_55 $_55 $_54 \/ % 0.12/0.37 member (k $_55 $_55 $_54) $Set1 % 0.12/0.37 |- ~subset $_54 $Superset \/ difference $_55 $_55 $_54 \/ % 0.12/0.37 member (k $_55 $_55 $_54) $Superset % 0.12/0.37 |- ~difference $A_set $_54 $_54 \/ difference $_55 $_55 $_54 % 0.12/0.37 |- ~difference $_71 $_72 $_69 \/ difference $_53 $_53 $_71 \/ % 0.12/0.37 member (k $_53 $_53 $_71) $_69 \/ member (k $_53 $_53 $_71) $_72 % 0.12/0.37 |- ~difference $_71 $_72 $_69 \/ difference $_71 $Set2 $Difference \/ % 0.12/0.37 member (k $_71 $Set2 $Difference) $Difference \/ % 0.12/0.37 member (k $_71 $Set2 $Difference) $_69 \/ % 0.12/0.37 member (k $_71 $Set2 $Difference) $_72 % 0.12/0.37 |- ~difference $_71 $_72 $_69 \/ difference $Set1 $Set2 $_71 \/ % 0.12/0.37 member (k $Set1 $Set2 $_71) $Set1 \/ member (k $Set1 $Set2 $_71) $_69 \/ % 0.12/0.37 member (k $Set1 $Set2 $_71) $_72 % 0.12/0.37 |- ~difference $_71 $_72 $_69 \/ difference $_22 $_71 $_22 \/ % 0.12/0.37 member (k $_22 $_71 $_22) $_69 \/ member (k $_22 $_71 $_22) $_72 % 0.12/0.37 |- ~difference $_71 $_72 $_69 \/ difference $_71 $Set2 $_71 \/ % 0.12/0.37 member (k $_71 $Set2 $_71) $_69 \/ member (k $_71 $Set2 $_71) $_72 % 0.12/0.37 |- ~difference $_71 $_72 $_69 \/ % 0.12/0.37 member (member_of_1_not_of_2 $_71 $Superset) $_69 \/ % 0.12/0.37 member (member_of_1_not_of_2 $_71 $Superset) $_72 \/ % 0.12/0.37 subset $_71 $Superset % 0.12/0.37 |- ~difference $_102 $_103 $_104 \/ difference $_104 $_103 $_104 % 0.12/0.37 |- ~difference $_109 $_110 $_111 \/ difference $_110 $_111 $_110 % 0.12/0.37 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.37 %------------------------------------------------------------------------------