%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : GRP395-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n015.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 : Sat Jul 16 10:38:35 EDT 2022 % Result : Satisfiable 23.33s 23.53s % Output : Saturation 23.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP395-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.13 % Command : metis --show proof --show saturation %s % 0.12/0.34 % Computer : n015.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 13 06:41:07 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 23.33/23.53 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.33/23.53 % 23.33/23.53 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.33/23.53 |- group_member (identity_for $Xg) $Xg % 23.33/23.53 |- product $Xg (identity_for $Xg) $X $X % 23.33/23.53 |- product $Xg $X (identity_for $Xg) $X % 23.33/23.53 |- ~group_member $X $Xg \/ group_member (inverse $Xg $X) $Xg % 23.33/23.53 |- product $Xg (inverse $Xg $X) $X (identity_for $Xg) % 23.33/23.53 |- product $Xg $X (inverse $Xg $X) (identity_for $Xg) % 23.33/23.53 |- ~group_member $X $Xg \/ ~group_member $Y $Xg \/ % 23.33/23.53 product $Xg $X $Y (multiply $Xg $X $Y) % 23.33/23.53 |- ~group_member $X $Xg \/ ~group_member $Y $Xg \/ % 23.33/23.53 group_member (multiply $Xg $X $Y) $Xg % 23.33/23.53 |- ~product $Xg $X $Y $W \/ ~product $Xg $X $Y $Z \/ $W = $Z % 23.33/23.53 |- ~product $Xg $X $Y $Xy \/ ~product $Xg $Xy $Z $Xyz \/ % 23.33/23.53 ~product $Xg $Y $Z $Yz \/ product $Xg $X $Yz $Xyz % 23.33/23.53 |- ~product $Xg $X $Y $Xy \/ ~product $Xg $X $Yz $Xyz \/ % 23.33/23.53 ~product $Xg $Y $Z $Yz \/ product $Xg $Xy $Z $Xyz % 23.33/23.53 |- ~group_member $Y $Xg \/ product $Xg $Y $Y (multiply $Xg $Y $Y) % 23.33/23.53 |- ~group_member $Y $Xg \/ group_member (multiply $Xg $Y $Y) $Xg % 23.33/23.53 |- ~product $Xg $Xyz $Z $Xyz \/ ~product $Xg $Z $Z $Yz \/ % 23.33/23.53 product $Xg $Xyz $Yz $Xyz % 23.33/23.53 |- ~product $Xg $Yz $Z $Xyz \/ ~product $Xg $Z $Z $Yz \/ % 23.33/23.53 product $Xg $Z $Yz $Xyz % 23.33/23.53 |- ~product $Xg $X $Y $Y \/ ~product $Xg $Y $Z $Yz \/ % 23.33/23.53 product $Xg $X $Yz $Yz % 23.33/23.53 |- ~product $Xg $X $Yz $Xyz \/ ~product $Xg $Yz $Z $Yz \/ % 23.33/23.53 product $Xg $Xyz $Z $Xyz % 23.33/23.53 |- ~product $Xg $Z $Yz $Xyz \/ ~product $Xg $Z $Z $Yz \/ % 23.33/23.53 product $Xg $Yz $Z $Xyz % 23.33/23.53 |- ~product $Xg $Y $Y $Xy \/ ~product $Xg $Y $Z $Z \/ product $Xg $Xy $Z $Z % 23.33/23.53 |- ~group_member $_107 $_106 \/ % 23.33/23.53 group_member (multiply $_106 (identity_for $_106) $_107) $_106 % 23.33/23.53 |- ~group_member $_105 $_106 \/ % 23.33/23.53 group_member (multiply $_106 $_105 (identity_for $_106)) $_106 % 23.33/23.53 |- ~group_member $_486 $_485 \/ % 23.33/23.53 product $_485 (identity_for $_485) $_486 % 23.33/23.53 (multiply $_485 (identity_for $_485) $_486) % 23.33/23.53 |- ~group_member $_484 $_485 \/ % 23.33/23.53 product $_485 $_484 (identity_for $_485) % 23.33/23.53 (multiply $_485 $_484 (identity_for $_485)) % 23.33/23.53 |- ~product $_3936 (identity_for $_3936) (identity_for $_3936) $_3938 \/ % 23.33/23.53 product $_3936 $_3937 $_3938 $_3937 % 23.33/23.53 |- ~product $_3986 (identity_for $_3986) (identity_for $_3986) $_3987 \/ % 23.33/23.53 product $_3986 $_3987 $_3989 $_3989 % 23.33/23.53 |- ~product $_5979 (identity_for $_5979) $_5977 $_5981 \/ $_5977 = $_5981 % 23.33/23.53 |- ~product $_5979 (inverse $_5979 $_5980) $_5980 $_5981 \/ % 23.33/23.53 identity_for $_5979 = $_5981 % 23.33/23.53 |- ~product $_5979 $_5977 (identity_for $_5979) $_5981 \/ $_5977 = $_5981 % 23.33/23.53 |- ~product $_5979 $_5978 (inverse $_5979 $_5978) $_5981 \/ % 23.33/23.53 identity_for $_5979 = $_5981 % 23.33/23.53 |- inverse $_5983 (identity_for $_5983) = identity_for $_5983 % 23.33/23.53 |- multiply $_5983 (identity_for $_5983) (identity_for $_5983) = % 23.33/23.53 identity_for $_5983 % 23.33/23.53 |- ~product $_6001 $_6000 (identity_for $_6001) (identity_for $_6001) \/ % 23.33/23.53 product $_6001 $_6000 $_6003 $_6003 % 23.33/23.53 |- ~product $_6001 $_6000 $_6002 $_6002 \/ % 23.33/23.53 product $_6001 $_6000 (identity_for $_6001) (identity_for $_6001) % 23.33/23.53 |- ~product $_6012 $_6014 $_6015 $_6014 \/ % 23.33/23.53 product $_6012 (identity_for $_6012) $_6015 (identity_for $_6012) % 23.33/23.53 |- ~product $_6012 (identity_for $_6012) $_6015 (identity_for $_6012) \/ % 23.33/23.53 product $_6012 $_6013 $_6015 $_6013 % 23.33/23.53 |- ~product $_6023 $_6024 $_6028 $_6025 \/ % 23.33/23.53 ~product $_6023 $_6024 $_6028 $_6027 \/ % 23.33/23.53 product $_6023 (identity_for $_6023) $_6027 $_6025 % 23.33/23.53 |- ~product $_6023 $_6026 $_6028 $_6027 \/ % 23.33/23.53 ~product $_6023 (identity_for $_6023) $_6028 $_6025 \/ % 23.33/23.53 product $_6023 (inverse $_6023 $_6026) $_6027 $_6025 % 23.33/23.53 |- ~product $_6023 $_6024 $_6028 $_6025 \/ % 23.33/23.53 ~product $_6023 (identity_for $_6023) $_6028 $_6027 \/ % 23.33/23.53 product $_6023 $_6024 $_6027 $_6025 % 23.33/23.53 |- ~product $_6023 (identity_for $_6023) $_6028 $_6025 \/ % 23.33/23.53 ~product $_6023 (inverse $_6023 $_6022) $_6028 $_6027 \/ % 23.33/23.53 product $_6023 $_6022 $_6027 $_6025 % 23.33/23.53 |- ~product $_6023 $_6022 $_6026 (identity_for $_6023) \/ % 23.33/23.53 ~product $_6023 $_6026 $_6025 $_6027 \/ % 23.33/23.53 product $_6023 $_6022 $_6027 $_6025 % 23.33/23.53 |- ~product $_6023 $_6022 $_6026 (inverse $_6023 $_6028) \/ % 23.33/23.53 ~product $_6023 $_6026 $_6028 $_6027 \/ % 23.33/23.53 product $_6023 $_6022 $_6027 (identity_for $_6023) % 23.33/23.53 |- ~product $_6023 $_6022 $_6026 $_6025 \/ % 23.33/23.53 ~product $_6023 $_6026 (identity_for $_6023) $_6027 \/ % 23.33/23.53 product $_6023 $_6022 $_6027 $_6025 % 23.33/23.53 |- ~product $_6023 $_6022 $_6026 $_6024 \/ % 23.33/23.53 ~product $_6023 $_6026 (inverse $_6023 $_6024) $_6027 \/ % 23.33/23.53 product $_6023 $_6022 $_6027 (identity_for $_6023) % 23.33/23.53 |- ~product $_6023 $_6022 (identity_for $_6023) $_6024 \/ % 23.33/23.53 ~product $_6023 $_6024 $_6027 $_6025 \/ % 23.33/23.53 product $_6023 $_6022 $_6027 $_6025 % 23.33/23.53 |- ~product $_6023 $_6022 (inverse $_6023 $_6028) $_6024 \/ % 23.33/23.53 ~product $_6023 $_6024 $_6028 $_6025 \/ % 23.33/23.53 product $_6023 $_6022 (identity_for $_6023) $_6025 % 23.33/23.53 |- ~product $_6023 $_6022 $_6027 $_6024 \/ % 23.33/23.53 ~product $_6023 $_6024 (identity_for $_6023) $_6025 \/ % 23.33/23.53 product $_6023 $_6022 $_6027 $_6025 % 23.33/23.53 |- ~product $_6023 $_6022 $_6026 $_6024 \/ % 23.33/23.53 ~product $_6023 $_6024 (inverse $_6023 $_6026) $_6025 \/ % 23.33/23.53 product $_6023 $_6022 (identity_for $_6023) $_6025 % 23.33/23.53 |- ~product $_6029 (identity_for $_6029) $_6031 $_6032 \/ % 23.33/23.53 product $_6029 (identity_for $_6029) $_6032 $_6031 % 23.33/23.53 |- ~product $_6029 (inverse $_6029 $_6033) $_6033 $_6032 \/ % 23.33/23.53 product $_6029 (identity_for $_6029) $_6032 (identity_for $_6029) % 23.33/23.53 |- ~product $_6029 $_6031 (identity_for $_6029) $_6032 \/ % 23.33/23.53 product $_6029 (identity_for $_6029) $_6032 $_6031 % 23.33/23.53 |- ~product $_6029 $_6030 (inverse $_6029 $_6030) $_6032 \/ % 23.33/23.53 product $_6029 (identity_for $_6029) $_6032 (identity_for $_6029) % 23.33/23.53 |- ~product $_6029 (inverse $_6029 $_6033) $_6033 $_6031 \/ % 23.33/23.53 product $_6029 (identity_for $_6029) (identity_for $_6029) $_6031 % 23.33/23.53 |- ~product $_6029 $_6032 (identity_for $_6029) $_6031 \/ % 23.33/23.53 product $_6029 (identity_for $_6029) $_6032 $_6031 % 23.33/23.53 |- ~product $_6029 $_6030 (inverse $_6029 $_6030) $_6031 \/ % 23.33/23.53 product $_6029 (identity_for $_6029) (identity_for $_6029) $_6031 % 23.33/23.54 |- ~product $_6055 (identity_for $_6055) $_6059 $_6058 \/ % 23.33/23.54 product $_6055 (inverse $_6055 $_6059) $_6058 (identity_for $_6055) % 23.33/23.54 |- ~product $_6055 (identity_for $_6055) (inverse $_6055 $_6056) $_6058 \/ % 23.33/23.54 product $_6055 $_6056 $_6058 (identity_for $_6055) % 23.33/23.54 |- ~product $_6067 $_6069 $_6068 $_6070 \/ % 23.33/23.54 product $_6067 (inverse $_6067 $_6069) $_6070 $_6068 % 23.33/23.54 |- ~product $_6067 (inverse $_6067 $_6066) $_6068 $_6070 \/ % 23.33/23.54 product $_6067 $_6066 $_6070 $_6068 % 23.33/23.54 |- ~product $_6067 $_6066 (inverse $_6067 $_6068) (identity_for $_6067) \/ % 23.33/23.54 product $_6067 $_6066 (identity_for $_6067) $_6068 % 23.33/23.54 |- ~product $_6067 $_6066 $_6069 (identity_for $_6067) \/ % 23.33/23.54 product $_6067 $_6066 (identity_for $_6067) (inverse $_6067 $_6069) % 23.33/23.54 |- inverse $_6074 (inverse $_6074 $_6075) = $_6075 % 23.33/23.54 |- ~product $_6095 $_6094 (identity_for $_6095) (inverse $_6095 $_6098) \/ % 23.33/23.54 product $_6095 $_6094 $_6098 (identity_for $_6095) % 23.33/23.54 |- ~product $_6095 $_6094 (identity_for $_6095) $_6096 \/ % 23.33/23.54 product $_6095 $_6094 (inverse $_6095 $_6096) (identity_for $_6095) % 23.33/23.54 |- ~product $_6106 (identity_for $_6106) (identity_for $_6106) $_6108 \/ % 23.33/23.54 product $_6106 (inverse $_6106 $_6109) $_6109 $_6108 % 23.33/23.54 |- ~product $_6106 (identity_for $_6106) (identity_for $_6106) $_6108 \/ % 23.33/23.54 product $_6106 $_6105 (inverse $_6106 $_6105) $_6108 % 23.33/23.54 |- ~product $_6116 (identity_for $_6116) $_6120 $_6117 \/ % 23.33/23.54 product $_6116 $_6120 (identity_for $_6116) $_6117 % 23.33/23.54 |- ~product $_6150 $_6151 $_6155 $_6154 \/ % 23.33/23.54 ~product $_6150 (identity_for $_6150) $_6154 $_6152 \/ % 23.33/23.54 product $_6150 $_6151 $_6155 $_6152 % 23.33/23.54 |- ~product $_6150 $_6153 $_6155 $_6154 \/ % 23.33/23.54 ~product $_6150 (inverse $_6150 $_6153) $_6154 $_6152 \/ % 23.33/23.54 product $_6150 (identity_for $_6150) $_6155 $_6152 % 23.33/23.54 |- ~product $_6150 $_6151 $_6154 $_6152 \/ % 23.33/23.54 ~product $_6150 (identity_for $_6150) $_6155 $_6154 \/ % 23.33/23.54 product $_6150 $_6151 $_6155 $_6152 % 23.33/23.54 |- ~product $_6150 $_6149 $_6154 $_6152 \/ % 23.33/23.54 ~product $_6150 (inverse $_6150 $_6149) $_6155 $_6154 \/ % 23.33/23.54 product $_6150 (identity_for $_6150) $_6155 $_6152 % 23.33/23.54 |- ~product $_6150 $_6153 $_6155 $_6152 \/ % 23.33/23.54 ~product $_6150 (identity_for $_6150) $_6153 $_6151 \/ % 23.33/23.54 product $_6150 $_6151 $_6155 $_6152 % 23.33/23.54 |- ~product $_6150 $_6153 $_6155 $_6154 \/ % 23.33/23.54 ~product $_6150 (inverse $_6150 $_6154) $_6153 $_6151 \/ % 23.33/23.54 product $_6150 $_6151 $_6155 (identity_for $_6150) % 23.33/23.54 |- ~product $_6150 $_6152 $_6153 $_6151 \/ % 23.33/23.54 ~product $_6150 $_6153 $_6155 (identity_for $_6150) \/ % 23.33/23.54 product $_6150 $_6151 $_6155 $_6152 % 23.33/23.54 |- ~product $_6150 $_6149 $_6153 $_6151 \/ % 23.33/23.54 ~product $_6150 $_6153 $_6155 (inverse $_6150 $_6149) \/ % 23.33/23.54 product $_6150 $_6151 $_6155 (identity_for $_6150) % 23.33/23.54 |- ~product $_6150 $_6149 $_6154 $_6152 \/ % 23.33/23.54 ~product $_6150 $_6149 (identity_for $_6150) $_6151 \/ % 23.33/23.54 product $_6150 $_6151 $_6154 $_6152 % 23.33/23.54 |- ~product $_6150 $_6149 (identity_for $_6150) $_6152 \/ % 23.33/23.54 ~product $_6150 $_6149 (inverse $_6150 $_6155) $_6151 \/ % 23.33/23.54 product $_6150 $_6151 $_6155 $_6152 % 23.33/23.54 |- ~product $_6150 $_6149 $_6154 $_6151 \/ % 23.33/23.54 ~product $_6150 $_6149 $_6154 $_6152 \/ % 23.33/23.54 product $_6150 $_6151 (identity_for $_6150) $_6152 % 23.33/23.54 |- ~product $_6150 $_6149 $_6153 $_6151 \/ % 23.33/23.54 ~product $_6150 $_6149 (identity_for $_6150) $_6152 \/ % 23.33/23.54 product $_6150 $_6151 (inverse $_6150 $_6153) $_6152 % 23.33/23.54 |- ~product $_6161 (identity_for $_6161) $_6165 $_6164 \/ % 23.33/23.54 product $_6161 (inverse $_6161 $_6164) $_6165 (identity_for $_6161) % 23.33/23.54 |- ~product $_6161 (identity_for $_6161) $_6165 (inverse $_6161 $_6162) \/ % 23.33/23.54 product $_6161 $_6162 $_6165 (identity_for $_6161) % 23.33/23.54 |- ~product $_6172 (identity_for $_6172) $_6174 $_6173 \/ % 23.33/23.54 product $_6172 $_6173 (identity_for $_6172) $_6174 % 23.33/23.54 |- ~product $_6186 $_6189 $_6190 (identity_for $_6186) \/ % 23.33/23.54 product $_6186 (identity_for $_6186) $_6190 (inverse $_6186 $_6189) % 23.33/23.54 |- ~product $_6186 (inverse $_6186 $_6188) $_6190 (identity_for $_6186) \/ % 23.33/23.54 product $_6186 (identity_for $_6186) $_6190 $_6188 % 23.33/23.54 |- ~product $_6186 $_6188 (identity_for $_6186) $_6187 \/ % 23.33/23.54 product $_6186 $_6187 (identity_for $_6186) $_6188 % 23.33/23.54 |- ~product $_6186 $_6188 (inverse $_6186 $_6190) $_6187 \/ % 23.33/23.54 product $_6186 $_6187 $_6190 $_6188 % 23.33/23.54 |- ~product $_6186 $_6188 $_6189 $_6187 \/ % 23.33/23.54 product $_6186 $_6187 (inverse $_6186 $_6189) $_6188 % 23.33/23.54 |- ~product $_6209 (inverse $_6209 $_6212) (identity_for $_6209) $_6210 \/ % 23.33/23.54 product $_6209 $_6210 $_6212 (identity_for $_6209) % 23.33/23.54 |- ~product $_6213 $_6075 (identity_for $_6213) $_6214 \/ % 23.33/23.54 product $_6213 $_6214 (inverse $_6213 $_6075) (identity_for $_6213) % 23.33/23.54 |- ~product $_6220 (inverse $_6220 $_6223) $_6223 $_6221 \/ % 23.33/23.54 product $_6220 $_6221 (identity_for $_6220) (identity_for $_6220) % 23.33/23.54 |- ~product $_6224 $_6075 (inverse $_6224 $_6075) $_6225 \/ % 23.33/23.54 product $_6224 $_6225 (identity_for $_6224) (identity_for $_6224) % 23.33/23.54 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.33/23.54 %------------------------------------------------------------------------------