%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : GEO661+1 : TPTP v9.3.0. Released v9.3.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 : 300s % DateTime : Tue May 5 06:23:58 PM UTC 2026 % Result : Satisfiable 0.21s 0.45s % Output : Saturation 0.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GEO661+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.14 % Command : metis --show proof --show saturation %s % 0.19/0.35 % Computer : n022.cluster.edu % 0.19/0.35 % Model : x86_64 x86_64 % 0.19/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.35 % Memory : 8042.1875MB % 0.19/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.35 % CPULimit : 300 % 0.19/0.35 % WCLimit : 300 % 0.19/0.35 % DateTime : Mon May 4 21:02:05 EDT 2026 % 0.19/0.35 % CPUTime : % 0.21/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.21/0.45 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.45 % 0.21/0.45 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.45 |- equidistant $X $Y $Y $X % 0.21/0.45 |- ~equidistant $X $Y $V2 $W \/ ~equidistant $X $Y $Z $V \/ % 0.21/0.45 equidistant $Z $V $V2 $W % 0.21/0.45 |- ~equidistant $X $Y $Z $Z \/ $X = $Y % 0.21/0.45 |- ~between $X $Y (skolemFOFtoCNF_Z $X $Y) \/ % 0.21/0.45 equidistant $Y (skolemFOFtoCNF_Z_1 $A $B $Y) $A $B % 0.21/0.45 |- ~between $X $Y $Z \/ ~between $X1 $Y1 $Z1 \/ % 0.21/0.45 ~equidistant $X $V $X1 $V1 \/ ~equidistant $X $Y $X1 $Y1 \/ % 0.21/0.45 ~equidistant $Y $V $Y1 $V1 \/ ~equidistant $Y $Z $Y1 $Z1 \/ $X = $Y \/ % 0.21/0.45 equidistant $Z $V $Z1 $V1 % 0.21/0.45 |- ~between $X $Y $X \/ $X = $Y % 0.21/0.45 |- ~between $X $U $Z \/ ~between $Y $V $Z \/ % 0.21/0.45 between $U (skolemFOFtoCNF_A $U $V $X $Y) $Y % 0.21/0.45 |- ~between $X $U $Z \/ ~between $Y $V $Z \/ % 0.21/0.45 between $V (skolemFOFtoCNF_A $U $V $X $Y) $X % 0.21/0.45 |- ~between skolemFOFtoCNF_A_1 skolemFOFtoCNF_B skolemFOFtoCNF_C % 0.21/0.45 |- ~between skolemFOFtoCNF_B skolemFOFtoCNF_C skolemFOFtoCNF_A_1 % 0.21/0.45 |- ~between skolemFOFtoCNF_C skolemFOFtoCNF_A_1 skolemFOFtoCNF_B % 0.21/0.45 |- ~equidistant $X $W $X $V \/ ~equidistant $Y $W $Y $V \/ % 0.21/0.45 ~equidistant $Z $W $Z $V \/ $W = $V \/ between $X $Y $Z \/ % 0.21/0.45 between $Y $Z $X \/ between $Z $X $Y % 0.21/0.45 |- ~between $X $U $V \/ ~between $Y $U $Z \/ $X = $U \/ % 0.21/0.45 between $X $Y (skolemFOFtoCNF_A_2 $V $X $Y $Z) % 0.21/0.45 |- ~between $X $U $V \/ ~between $Y $U $Z \/ $X = $U \/ % 0.21/0.45 between $X $Z (skolemFOFtoCNF_B_1 $V $X $Y $Z) % 0.21/0.45 |- ~between $X $U $V \/ ~between $Y $U $Z \/ $X = $U \/ % 0.21/0.45 between (skolemFOFtoCNF_A_2 $V $X $Y $Z) $V % 0.21/0.45 (skolemFOFtoCNF_B_1 $V $X $Y $Z) % 0.21/0.45 |- ~between $U $V $X \/ ~between $V $W $X \/ ~equidistant $U $V $U $V1 \/ % 0.21/0.45 ~equidistant $U $X $U $X1 \/ % 0.21/0.45 between $V1 (skolemFOFtoCNF_A_3 $U $V1 $W $X1) $X1 % 0.21/0.45 |- ~between $U $V $X \/ ~between $V $W $X \/ ~equidistant $U $V $U $V1 \/ % 0.21/0.45 ~equidistant $U $X $U $X1 \/ % 0.21/0.45 equidistant $U $W $U (skolemFOFtoCNF_A_3 $U $V1 $W $X1) % 0.21/0.45 |- ~between $Y $V $Z \/ between $V (skolemFOFtoCNF_A $V $V $Y $Y) $Y % 0.21/0.45 |- ~between $Y $U $Z \/ $Y = $U \/ % 0.21/0.45 between $Y $Y (skolemFOFtoCNF_A_2 $Z $Y $Y $Z) % 0.21/0.45 |- ~between $Y $U $Z \/ $Y = $U \/ % 0.21/0.45 between $Y $Z (skolemFOFtoCNF_B_1 $Z $Y $Y $Z) % 0.21/0.45 |- ~between $Y $U $Z \/ $Y = $U \/ % 0.21/0.45 between (skolemFOFtoCNF_A_2 $Z $Y $Y $Z) $Z % 0.21/0.45 (skolemFOFtoCNF_B_1 $Z $Y $Y $Z) % 0.21/0.45 |- ~between $W $W $X \/ ~equidistant $W $W $W $V1 \/ % 0.21/0.45 ~equidistant $W $X $W $X1 \/ % 0.21/0.45 between $V1 (skolemFOFtoCNF_A_3 $W $V1 $W $X1) $X1 % 0.21/0.45 |- ~between $U $X $X \/ ~between $X $W $X \/ ~equidistant $U $X $U $X1 \/ % 0.21/0.45 between $X1 (skolemFOFtoCNF_A_3 $U $X1 $W $X1) $X1 % 0.21/0.45 |- ~between $W $W $W \/ ~equidistant $W $W $W $X1 \/ % 0.21/0.45 between $X1 (skolemFOFtoCNF_A_3 $W $X1 $W $X1) $X1 % 0.21/0.45 |- ~between $W $W $X \/ ~equidistant $W $W $W $V1 \/ % 0.21/0.45 ~equidistant $W $X $W $X1 \/ % 0.21/0.45 equidistant $W $W $W (skolemFOFtoCNF_A_3 $W $V1 $W $X1) % 0.21/0.45 |- ~between $U $X $X \/ ~between $X $W $X \/ ~equidistant $U $X $U $X1 \/ % 0.21/0.45 equidistant $U $W $U (skolemFOFtoCNF_A_3 $U $X1 $W $X1) % 0.21/0.45 |- ~between $W $W $W \/ ~equidistant $W $W $W $X1 \/ % 0.21/0.45 equidistant $W $W $W (skolemFOFtoCNF_A_3 $W $X1 $W $X1) % 0.21/0.45 |- ~equidistant $Y $W $Y $V \/ ~equidistant $Z $W $Z $V \/ $W = $V \/ % 0.21/0.45 between $Y $Y $Z \/ between $Y $Z $Y \/ between $Z $Y $Y % 0.21/0.45 |- ~equidistant $Z $W $Z $V \/ $W = $V \/ between $Z $Z $Z % 0.21/0.45 |- ~between $X1 $Y1 $Z1 \/ ~equidistant $X1 $V $X1 $V1 \/ % 0.21/0.45 ~equidistant $Y1 $V $Y1 $V1 \/ $X1 = $Y1 \/ equidistant $Z1 $V $Z1 $V1 % 0.21/0.45 |- ~between $X $Y $Z \/ ~between $X1 $Y1 $Z1 \/ % 0.21/0.45 ~equidistant $X $Y $X1 $Y1 \/ ~equidistant $Y $Y $Y1 $Y1 \/ % 0.21/0.45 ~equidistant $Y $Z $Y1 $Z1 \/ $X = $Y \/ equidistant $Z $Y $Z1 $Y1 % 0.21/0.45 |- ~between $X $Y $Z \/ ~between $X1 $Y1 $Z1 \/ % 0.21/0.45 ~equidistant $X $Y $X1 $Y1 \/ ~equidistant $X $Z $X1 $Z1 \/ % 0.21/0.45 ~equidistant $Y $Z $Y1 $Z1 \/ $X = $Y \/ equidistant $Z $Z $Z1 $Z1 % 0.21/0.45 |- equidistant $_10 $_7 $_10 $_7 % 0.21/0.45 |- ~equidistant $_49 $_50 $_53 $_48 \/ equidistant $_53 $_48 $_49 $_50 % 0.21/0.45 |- ~equidistant $_50 $_49 $_53 $_48 \/ equidistant $_53 $_48 $_49 $_50 % 0.21/0.45 |- ~equidistant $_48 $_53 $_49 $_50 \/ equidistant $_53 $_48 $_49 $_50 % 0.21/0.45 |- ~between $_73 $_73 $_75 \/ ~equidistant $_73 $_75 $_73 $_76 \/ % 0.21/0.45 between $_73 (skolemFOFtoCNF_A_3 $_73 $_73 $_73 $_76) $_76 % 0.21/0.45 |- ~between $_74 $_74 $_76 \/ ~equidistant $_74 $_74 $_74 $_73 \/ % 0.21/0.45 between $_73 (skolemFOFtoCNF_A_3 $_74 $_73 $_74 $_76) $_76 % 0.21/0.45 |- ~between $_77 $_77 $_79 \/ % 0.21/0.45 between $_77 (skolemFOFtoCNF_A_3 $_77 $_77 $_77 $_79) $_79 % 0.21/0.45 |- ~between $_102 $_102 $_104 \/ ~equidistant $_102 $_104 $_102 $_105 \/ % 0.21/0.45 equidistant $_102 $_102 $_102 % 0.21/0.45 (skolemFOFtoCNF_A_3 $_102 $_102 $_102 $_105) % 0.21/0.45 |- ~between $_103 $_103 $_105 \/ ~equidistant $_103 $_103 $_103 $_102 \/ % 0.21/0.45 equidistant $_103 $_103 $_103 % 0.21/0.45 (skolemFOFtoCNF_A_3 $_103 $_102 $_103 $_105) % 0.21/0.45 |- ~between $_106 $_106 $_108 \/ % 0.21/0.45 equidistant $_106 $_106 $_106 % 0.21/0.45 (skolemFOFtoCNF_A_3 $_106 $_106 $_106 $_108) % 0.21/0.45 |- ~between $_123 $_125 $_127 \/ ~between $_125 $_126 $_127 \/ % 0.21/0.45 ~equidistant $_123 $_127 $_123 $_128 \/ % 0.21/0.45 between $_125 (skolemFOFtoCNF_A_3 $_123 $_125 $_126 $_128) $_128 % 0.21/0.45 |- ~between $_123 $_124 $_128 \/ ~between $_124 $_126 $_128 \/ % 0.21/0.45 ~equidistant $_123 $_124 $_123 $_125 \/ % 0.21/0.45 between $_125 (skolemFOFtoCNF_A_3 $_123 $_125 $_126 $_128) $_128 % 0.21/0.45 |- ~between $_129 $_130 $_133 \/ ~between $_130 $_131 $_133 \/ % 0.21/0.45 between $_130 (skolemFOFtoCNF_A_3 $_129 $_130 $_131 $_133) $_133 % 0.21/0.45 |- ~between $_143 $_145 $_147 \/ ~between $_145 $_146 $_147 \/ % 0.21/0.45 ~equidistant $_143 $_147 $_143 $_148 \/ % 0.21/0.45 equidistant $_143 $_146 $_143 % 0.21/0.45 (skolemFOFtoCNF_A_3 $_143 $_145 $_146 $_148) % 0.21/0.45 |- ~between $_143 $_144 $_148 \/ ~between $_144 $_146 $_148 \/ % 0.21/0.45 ~equidistant $_143 $_144 $_143 $_145 \/ % 0.21/0.45 equidistant $_143 $_146 $_143 % 0.21/0.45 (skolemFOFtoCNF_A_3 $_143 $_145 $_146 $_148) % 0.21/0.45 |- ~between $_149 $_150 $_153 \/ ~between $_150 $_151 $_153 \/ % 0.21/0.45 equidistant $_149 $_151 $_149 % 0.21/0.45 (skolemFOFtoCNF_A_3 $_149 $_150 $_151 $_153) % 0.21/0.45 |- ~between $_174 $_176 $_178 \/ ~between $_176 $_174 $_177 \/ % 0.21/0.45 ~equidistant $_174 $_174 $_176 $_176 \/ % 0.21/0.45 ~equidistant $_174 $_177 $_176 $_178 \/ $_176 = $_174 \/ % 0.21/0.45 equidistant $_177 $_174 $_178 $_176 % 0.21/0.45 |- ~between $_173 $_176 $_177 \/ ~between $_174 $_176 $_178 \/ % 0.21/0.45 ~equidistant $_173 $_176 $_174 $_176 \/ % 0.21/0.45 ~equidistant $_176 $_177 $_176 $_178 \/ $_173 = $_176 \/ % 0.21/0.45 equidistant $_177 $_176 $_178 $_176 % 0.21/0.45 |- ~between $_193 $_195 $_196 \/ ~between $_193 $_195 $_197 \/ % 0.21/0.45 ~equidistant $_193 $_196 $_193 $_197 \/ % 0.21/0.45 ~equidistant $_195 $_196 $_195 $_197 \/ $_193 = $_195 \/ % 0.21/0.45 equidistant $_196 $_196 $_197 $_197 % 0.21/0.45 |- ~between $_193 $_195 $_197 \/ ~between $_195 $_193 $_196 \/ % 0.21/0.45 ~equidistant $_193 $_196 $_195 $_197 \/ % 0.21/0.45 ~equidistant $_195 $_196 $_193 $_197 \/ $_195 = $_193 \/ % 0.21/0.45 equidistant $_196 $_196 $_197 $_197 % 0.21/0.45 |- ~between $_193 $_195 $_197 \/ ~between $_197 $_194 $_193 \/ % 0.21/0.45 ~equidistant $_194 $_193 $_195 $_197 \/ % 0.21/0.45 ~equidistant $_197 $_194 $_193 $_195 \/ $_197 = $_194 \/ % 0.21/0.45 equidistant $_193 $_193 $_197 $_197 % 0.21/0.45 |- ~between $_192 $_197 $_195 \/ ~between $_193 $_195 $_197 \/ % 0.21/0.45 ~equidistant $_192 $_195 $_193 $_197 \/ % 0.21/0.45 ~equidistant $_192 $_197 $_193 $_195 \/ $_192 = $_197 \/ % 0.21/0.45 equidistant $_195 $_195 $_197 $_197 % 0.21/0.45 |- ~between $_217 $_218 $_220 \/ ~between $_217 $_219 $_221 \/ % 0.21/0.45 ~equidistant $_217 $_218 $_217 $_219 \/ % 0.21/0.45 ~equidistant $_218 $_215 $_219 $_215 \/ % 0.21/0.45 ~equidistant $_218 $_220 $_219 $_221 \/ $_217 = $_218 \/ % 0.21/0.45 equidistant $_220 $_215 $_221 $_215 % 0.21/0.45 |- ~between $_215 $_218 $_220 \/ ~between $_217 $_219 $_221 \/ % 0.21/0.45 ~equidistant $_215 $_218 $_217 $_219 \/ % 0.21/0.45 ~equidistant $_218 $_217 $_219 $_215 \/ % 0.21/0.45 ~equidistant $_218 $_220 $_219 $_221 \/ $_215 = $_218 \/ % 0.21/0.45 equidistant $_220 $_217 $_221 $_215 % 0.21/0.45 |- ~between $_217 $_219 $_220 \/ ~between $_217 $_219 $_221 \/ % 0.21/0.45 ~equidistant $_217 $_214 $_217 $_215 \/ % 0.21/0.45 ~equidistant $_219 $_214 $_219 $_215 \/ % 0.21/0.45 ~equidistant $_219 $_220 $_219 $_221 \/ $_217 = $_219 \/ % 0.21/0.45 equidistant $_220 $_214 $_221 $_215 % 0.21/0.45 |- ~between $_217 $_219 $_221 \/ ~between $_219 $_217 $_220 \/ % 0.21/0.45 ~equidistant $_217 $_214 $_219 $_215 \/ % 0.21/0.45 ~equidistant $_217 $_220 $_219 $_221 \/ % 0.21/0.45 ~equidistant $_219 $_214 $_217 $_215 \/ $_219 = $_217 \/ % 0.21/0.45 equidistant $_220 $_214 $_221 $_215 % 0.21/0.45 |- ~between $_216 $_219 $_220 \/ ~between $_217 $_219 $_221 \/ % 0.21/0.45 ~equidistant $_216 $_215 $_217 $_215 \/ % 0.21/0.45 ~equidistant $_216 $_219 $_217 $_219 \/ % 0.21/0.45 ~equidistant $_219 $_220 $_219 $_221 \/ $_216 = $_219 \/ % 0.21/0.45 equidistant $_220 $_215 $_221 $_215 % 0.21/0.45 |- ~between $_216 $_215 $_220 \/ ~between $_217 $_219 $_221 \/ % 0.21/0.45 ~equidistant $_215 $_220 $_219 $_221 \/ % 0.21/0.45 ~equidistant $_216 $_215 $_217 $_219 \/ % 0.21/0.45 ~equidistant $_216 $_219 $_217 $_215 \/ $_216 = $_215 \/ % 0.21/0.45 equidistant $_220 $_219 $_221 $_215 % 0.21/0.46 |- ~between $_216 $_219 $_221 \/ ~between $_217 $_219 $_221 \/ % 0.21/0.46 ~equidistant $_216 $_214 $_217 $_215 \/ % 0.21/0.46 ~equidistant $_216 $_219 $_217 $_219 \/ % 0.21/0.46 ~equidistant $_219 $_214 $_219 $_215 \/ $_216 = $_219 \/ % 0.21/0.46 equidistant $_221 $_214 $_221 $_215 % 0.21/0.46 |- ~between $_216 $_221 $_219 \/ ~between $_217 $_219 $_221 \/ % 0.21/0.46 ~equidistant $_216 $_214 $_217 $_215 \/ % 0.21/0.46 ~equidistant $_216 $_221 $_217 $_219 \/ % 0.21/0.46 ~equidistant $_221 $_214 $_219 $_215 \/ $_216 = $_221 \/ % 0.21/0.46 equidistant $_219 $_214 $_221 $_215 % 0.21/0.46 |- ~between $_224 $_225 $_226 \/ ~between $_224 $_225 $_227 \/ % 0.21/0.46 ~equidistant $_225 $_226 $_225 $_227 \/ $_224 = $_225 \/ % 0.21/0.46 equidistant $_226 $_223 $_227 $_223 % 0.21/0.46 |- ~between $_233 $_236 $_238 \/ ~between $_234 $_236 $_238 \/ % 0.21/0.46 ~equidistant $_233 $_236 $_234 $_236 \/ % 0.21/0.46 ~equidistant $_236 $_234 $_236 $_233 \/ $_233 = $_236 \/ % 0.21/0.46 equidistant $_238 $_234 $_238 $_233 % 0.30/0.46 |- ~between $_233 $_238 $_236 \/ ~between $_234 $_236 $_238 \/ % 0.30/0.46 ~equidistant $_233 $_238 $_234 $_236 \/ % 0.30/0.46 ~equidistant $_238 $_234 $_236 $_233 \/ $_233 = $_238 \/ % 0.30/0.46 equidistant $_236 $_234 $_238 $_233 % 0.30/0.46 |- ~between $_255 $_256 $_258 \/ ~between $_256 $_255 $_257 \/ % 0.30/0.46 ~equidistant $_255 $_257 $_256 $_258 \/ % 0.30/0.46 ~equidistant $_256 $_256 $_255 $_255 \/ $_256 = $_255 \/ % 0.30/0.46 equidistant $_257 $_256 $_258 $_255 % 0.30/0.46 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.30/0.46 %------------------------------------------------------------------------------