%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN425+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:37:42 PM UTC 2026
% Result : CounterSatisfiable 1.97s 1.04s
% Output : FiniteModel 1.97s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( a1336 = "d0"
& a1216 = "d1"
& a1215 = "d0"
& a1337 = "d0"
& a1214 = "d1"
& a1213 = "d0"
& a1334 = "d0"
& a1335 = "d0"
& a1332 = "d0"
& a1212 = "d0"
& a1211 = "d1"
& a1333 = "d0"
& a1210 = "d1"
& a1331 = "d0"
& a1330 = "d1"
& a1219 = "d0"
& a1338 = "d0"
& a1217 = "d0"
& a1218 = "d1"
& a1339 = "d0"
& a1340 = "d0"
& a1204 = "d0"
& a1326 = "d0"
& a1205 = "d0"
& a1325 = "d1"
& a1323 = "d0"
& a1202 = "d0"
& a1324 = "d0"
& a1203 = "d0"
& a1321 = "d0"
& a1201 = "d1"
& a1200 = "d1"
& a1322 = "d0"
& a1320 = "d0"
& a1329 = "d0"
& a1209 = "d0"
& a1208 = "d1"
& a1206 = "d0"
& a1328 = "d0"
& a1327 = "d1"
& a1207 = "d0"
& a1314 = "d0"
& a1315 = "d0"
& a1312 = "d0"
& a1313 = "d0"
& a1310 = "d0"
& a1311 = "d0"
& a1318 = "d0"
& a1319 = "d0"
& a1316 = "d0"
& a1317 = "d0"
& a1303 = "d0"
& a1304 = "d0"
& a1301 = "d0"
& a1302 = "d0"
& a1300 = "d0"
& a1309 = "d0"
& a1308 = "d1"
& a1307 = "d1"
& a1305 = "d0"
& a1306 = "d0"
& a1199 = "d0"
& a1198 = "d1"
& a1196 = "d0"
& a1197 = "d0"
& a1194 = "d0"
& a1195 = "d1"
& a1193 = "d1"
& a1192 = "d0"
& a1190 = "d0"
& a1191 = "d0"
& a1259 = "d0"
& a1257 = "d0"
& a1258 = "d0"
& a1255 = "d0"
& a1256 = "d0"
& a1253 = "d0"
& a1254 = "d0"
& a1262 = "d0"
& a1263 = "d0"
& a1261 = "d1"
& a1260 = "d1"
& a1248 = "d0"
& a1249 = "d1"
& a1246 = "d0"
& a1247 = "d0"
& a1245 = "d1"
& a1244 = "d0"
& a1243 = "d1"
& a1242 = "d0"
& a1364 = "d0"
& a1363 = "d1"
& a1251 = "d0"
& a1252 = "d0"
& a1250 = "d1"
& a1358 = "d0"
& a1238 = "d1"
& a1237 = "d0"
& a1359 = "d0"
& a1356 = "d0"
& a1235 = "d0"
& a1357 = "d0"
& a1236 = "d0"
& a1354 = "d0"
& a1233 = "d0"
& a1355 = "d0"
& a1234 = "d0"
& a1231 = "d0"
& a1353 = "d0"
& a1352 = "d1"
& a1232 = "d0"
& a1239 = "d0"
& a1240 = "d0"
& a1361 = "d0"
& a1362 = "d0"
& a1241 = "d0"
& a1360 = "d0"
& a1347 = "d1"
& a1227 = "d0"
& a1226 = "d1"
& a1348 = "d0"
& a1346 = "d1"
& a1224 = "d0"
& a1345 = "d1"
& a1225 = "d0"
& a1222 = "d0"
& a1344 = "d0"
& a1343 = "d1"
& a1223 = "d0"
& a1341 = "d0"
& a1221 = "d0"
& a1220 = "d1"
& a1342 = "d0"
& a1228 = "d0"
& a1349 = "d0"
& a1229 = "d0"
& a1350 = "d0"
& a1351 = "d0"
& a1230 = "d0"
& a1299 = "d1"
& a1297 = "d0"
& a1298 = "d0"
& a1288 = "d0"
& a1289 = "d0"
& a1286 = "d0"
& a1287 = "d0"
& a1295 = "d0"
& a1296 = "d0"
& a1293 = "d0"
& a1294 = "d0"
& a1291 = "d0"
& a1292 = "d0"
& a1290 = "d0"
& a1279 = "d0"
& a1277 = "d0"
& a1278 = "d0"
& a1275 = "d0"
& a1276 = "d0"
& a1284 = "d0"
& a1285 = "d0"
& a1282 = "d0"
& a1283 = "d0"
& a1280 = "d0"
& a1281 = "d0"
& a1269 = "d0"
& a1268 = "d1"
& a1266 = "d0"
& a1267 = "d0"
& a1264 = "d0"
& a1265 = "d0"
& a1273 = "d0"
& a1274 = "d0"
& a1271 = "d0"
& a1272 = "d0"
& a1270 = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( ~ c5_1("d1")
& ~ c5_1("d0")
& ~ c6_0
& ~ c6_2("d0","d1")
& ~ c6_2("d1","d0")
& c6_2("d1","d1")
& c6_2("d0","d0")
& c6_1("d0")
& ~ c6_1("d1")
& c5_2("d1","d1")
& c5_2("d0","d0")
& c5_2("d0","d1")
& ~ c5_2("d1","d0")
& ~ c5_0
& c3_1("d1")
& ~ c3_1("d0")
& c4_2("d0","d1")
& c4_2("d1","d0")
& ~ c4_2("d1","d1")
& c4_2("d0","d0")
& c4_0
& ~ c4_1("d0")
& c4_1("d1")
& c3_0
& c3_2("d1","d1")
& c3_2("d0","d0")
& c3_2("d0","d1")
& c3_2("d1","d0")
& ~ c9_1("d1")
& c9_1("d0")
& ~ c9_2("d1","d1")
& c9_2("d0","d0")
& ~ c9_2("d0","d1")
& ~ c9_2("d1","d0")
& c9_0
& ~ c8_2("d0","d1")
& ~ c8_2("d1","d0")
& ~ c8_2("d1","d1")
& c8_2("d0","d0")
& c7_1("d1")
& c7_1("d0")
& c8_0
& ~ c8_1("d0")
& ~ c8_1("d1")
& ~ c7_0
& c7_2("d1","d1")
& ~ c7_2("d0","d0")
& c7_2("d0","d1")
& ~ c7_2("d1","d0")
& ~ c10_1("d0")
& c10_1("d1")
& ~ c10_0
& c10_2("d0","d1")
& c10_2("d1","d0")
& ~ c10_2("d1","d1")
& ~ c10_2("d0","d0")
& ndr1_1("d1")
& ndr1_1("d0")
& ndr1_0
& c1_1("d1")
& c1_1("d0")
& c2_0
& ~ c2_2("d0","d1")
& c2_2("d1","d0")
& ~ c2_2("d1","d1")
& ~ c2_2("d0","d0")
& c1_0
& ~ c2_1("d0")
& c2_1("d1")
& ~ c1_2("d1","d1")
& c1_2("d0","d0")
& ~ c1_2("d0","d1")
& ~ c1_2("d1","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN425+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 01:14:39 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.43 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.GjUHIfftqD/theBenchmark.cnf 300
% 0.95/0.81 % domain size: 1
% 1.41/0.93 % domain size: 2
% 1.41/1.03 % model found for domain size 2
% 1.97/1.04 % SZS status CounterSatisfiable for theBenchmark
% 1.97/1.04 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.36/1.15 % FMB4L exiting
%------------------------------------------------------------------------------