%------------------------------------------------------------------------------
% 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 : n018.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:43 PM UTC 2026
% Result : Satisfiable 1.79s 1.08s
% Output : FiniteModel 2.28s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( a1216 = "d0"
& a1336 = "d1"
& a1215 = "d1"
& a1335 = "d1"
& a1214 = "d0"
& a1334 = "d1"
& a1332 = "d0"
& a1211 = "d0"
& a1212 = "d0"
& a1333 = "d0"
& a1210 = "d0"
& a1331 = "d0"
& a1330 = "d1"
& a1219 = "d0"
& a1338 = "d0"
& a1339 = "d0"
& a1218 = "d0"
& a1340 = "d0"
& a1325 = "d0"
& a1326 = "d0"
& a1202 = "d0"
& a1203 = "d0"
& a1324 = "d0"
& a1323 = "d1"
& a1200 = "d0"
& a1201 = "d0"
& a1208 = "d0"
& a1207 = "d1"
& a1328 = "d0"
& a1327 = "d1"
& a1314 = "d0"
& a1315 = "d1"
& a1312 = "d0"
& a1313 = "d1"
& a1310 = "d0"
& a1311 = "d0"
& a1318 = "d0"
& a1319 = "d1"
& a1316 = "d0"
& a1317 = "d0"
& a1303 = "d0"
& a1304 = "d0"
& a1301 = "d0"
& a1302 = "d0"
& a1300 = "d0"
& a1309 = "d0"
& a1308 = "d1"
& a1307 = "d0"
& a1306 = "d1"
& a1305 = "d0"
& a1199 = "d0"
& a1195 = "d1"
& a1194 = "d1"
& a1193 = "d0"
& a1255 = "d0"
& a1256 = "d0"
& a1253 = "d0"
& a1254 = "d0"
& a1262 = "d0"
& a1263 = "d0"
& a1260 = "d0"
& a1261 = "d0"
& a1249 = "d1"
& a1246 = "d0"
& a1247 = "d0"
& a1244 = "d0"
& a1245 = "d0"
& a1363 = "d0"
& a1243 = "d0"
& a1364 = "d0"
& a1242 = "d1"
& a1251 = "d0"
& a1252 = "d0"
& a1250 = "d0"
& a1237 = "d0"
& a1358 = "d0"
& a1238 = "d0"
& a1359 = "d0"
& a1356 = "d0"
& a1236 = "d0"
& a1235 = "d1"
& a1357 = "d0"
& a1234 = "d0"
& a1233 = "d1"
& a1355 = "d0"
& a1354 = "d1"
& a1231 = "d0"
& a1352 = "d0"
& a1353 = "d1"
& a1239 = "d0"
& a1361 = "d0"
& a1362 = "d0"
& a1241 = "d0"
& a1240 = "d1"
& a1360 = "d0"
& a1226 = "d0"
& a1348 = "d0"
& a1227 = "d0"
& a1347 = "d1"
& a1224 = "d0"
& a1345 = "d0"
& a1346 = "d0"
& a1222 = "d0"
& a1223 = "d1"
& a1343 = "d0"
& a1344 = "d0"
& a1220 = "d0"
& a1221 = "d0"
& a1342 = "d0"
& a1341 = "d1"
& a1349 = "d0"
& a1229 = "d0"
& a1230 = "d1"
& a1350 = "d1"
& a1351 = "d0"
& a1299 = "d1"
& a1298 = "d1"
& a1288 = "d0"
& a1286 = "d0"
& a1287 = "d0"
& a1293 = "d0"
& a1294 = "d0"
& a1292 = "d0"
& a1279 = "d0"
& a1277 = "d0"
& a1278 = "d0"
& a1275 = "d0"
& a1276 = "d1"
& a1284 = "d0"
& a1285 = "d0"
& a1282 = "d0"
& a1283 = "d0"
& a1280 = "d0"
& a1281 = "d0"
& a1268 = "d0"
& a1269 = "d0"
& a1264 = "d0"
& a1273 = "d0"
& a1274 = "d0"
& a1272 = "d0"
& a1271 = "d1"
& a1270 = "d1" ) ).
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")
& ssSkP8("d1")
& ssSkP9("d0")
& ssSkP8("d0")
& ssSkP9("d1")
& c9_1("d1")
& ~ c9_1("d0")
& ssSkC34
& ssSkC31
& ssSkC30
& ssSkC33
& ~ ssSkC32
& c9_2("d1","d1")
& ~ c9_2("d0","d0")
& c9_2("d0","d1")
& ~ c9_2("d1","d0")
& ssSkP4("d1")
& ssSkP5("d0")
& ssSkP4("d0")
& ssSkP5("d1")
& c9_0
& ssSkP7("d0")
& ssSkP6("d1")
& ~ ssSkP7("d1")
& ssSkP6("d0")
& ssSkP1("d0")
& ssSkP1("d1")
& ssSkP2("d1")
& ssSkP2("d0")
& ssSkP10("d0")
& ssSkP10("d1")
& ssSkP11("d1")
& ssSkP11("d0")
& ~ 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")
& ssSkC17
& ~ ssSkC16
& ~ ssSkC19
& ~ ssSkC18
& ssSkC15
& ~ ssSkC14
& ssSkC11
& ssSkC10
& ssSkC4
& ~ ssSkC3
& ssSkC6
& ssSkC5
& ~ ssSkC8
& ~ ssSkC7
& ssSkC9
& ~ ssSkC28
& ssSkC27
& ssSkC29
& ssSkC1
& ssSkC24
& ndr1_1("d1")
& ssSkC23
& ndr1_1("d0")
& ssSkC26
& ssSkC25
& ~ ssSkC20
& ~ ssSkC22
& ~ ssSkC21
& 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.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 01:10:49 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.45 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.BosMzI41HO/theBenchmark.cnf 300
% 0.76/0.85 % domain size: 1
% 1.23/0.96 % domain size: 2
% 1.79/1.06 % model found for domain size 2
% 1.79/1.08 % SZS status CounterSatisfiable for theBenchmark
% 1.79/1.08 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.28/1.16 % FMB4L exiting
%------------------------------------------------------------------------------