%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN910-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.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:38:38 PM UTC 2026
% Result : Satisfiable 1.53s 0.99s
% Output : FiniteModel 2.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( skc48 = "d0"
& skc41 = "d0"
& skc43 = "d1"
& skc60 = "d0"
& skc61 = "d0"
& skf104("d1") = "d1"
& skf103("d0") = "d1"
& skf104("d0") = "d1"
& skf103("d1") = "d1"
& skf102("d1") = "d1"
& skf101("d0") = "d1"
& skf102("d0") = "d1"
& skf101("d1") = "d1"
& skf100("d1") = "d1"
& skf100("d0") = "d1"
& skf109("d0") = "d1"
& skf109("d1") = "d1"
& skf108("d1") = "d1"
& skf107("d0") = "d1"
& skf108("d0") = "d1"
& skf107("d1") = "d1"
& skf106("d1") = "d1"
& skf105("d0") = "d1"
& skf106("d0") = "d1"
& skf105("d1") = "d1"
& skf115("d1") = "d1"
& skf114("d0") = "d1"
& skf115("d0") = "d1"
& skf114("d1") = "d1"
& skf113("d1") = "d1"
& skf112("d0") = "d1"
& skf113("d0") = "d1"
& skf112("d1") = "d1"
& skf111("d1") = "d1"
& skf110("d0") = "d1"
& skf111("d0") = "d1"
& skf110("d1") = "d1"
& skf119("d1") = "d1"
& skf118("d0") = "d1"
& skf119("d0") = "d1"
& skf118("d1") = "d1"
& skf117("d1") = "d1"
& skf116("d0") = "d1"
& skf117("d0") = "d1"
& skf116("d1") = "d1"
& skf126("d1") = "d1"
& skf125("d0") = "d1"
& skf126("d0") = "d1"
& skf125("d1") = "d1"
& skf124("d1") = "d1"
& skf123("d0") = "d1"
& skf124("d0") = "d1"
& skf123("d1") = "d1"
& skf122("d1") = "d1"
& skf121("d0") = "d1"
& skf122("d0") = "d1"
& skf121("d1") = "d1"
& skf120("d1") = "d1"
& skf120("d0") = "d1"
& skf129("d0") = "d1"
& skf129("d1") = "d1"
& skf128("d1") = "d1"
& skf127("d0") = "d1"
& skf128("d0") = "d1"
& skf127("d1") = "d1"
& skf133("d1") = "d1"
& skf132("d0") = "d1"
& skf133("d0") = "d1"
& skf132("d1") = "d1"
& skf131("d1") = "d1"
& skf130("d0") = "d1"
& skf131("d0") = "d1"
& skf130("d1") = "d1"
& skf81("d0") = "d0"
& skf80("d1") = "d0"
& skf81("d1") = "d0"
& skf80("d0") = "d0"
& skf83("d1") = "d1"
& skf83("d0") = "d0"
& skf82("d1") = "d1"
& skf82("d0") = "d0"
& skf85("d1") = "d1"
& skf85("d0") = "d0"
& skf84("d1") = "d1"
& skf84("d0") = "d0"
& skf87("d1") = "d1"
& skf87("d0") = "d0"
& skf86("d1") = "d1"
& skf86("d0") = "d0"
& skf89("d1") = "d1"
& skf89("d0") = "d0"
& skf88("d1") = "d1"
& skf88("d0") = "d0"
& skf90("d1") = "d1"
& skf90("d0") = "d0"
& skf92("d1") = "d1"
& skf92("d0") = "d0"
& skf91("d1") = "d1"
& skf91("d0") = "d0"
& skf94("d1") = "d1"
& skf94("d0") = "d0"
& skf93("d1") = "d1"
& skf93("d0") = "d0"
& skf96("d1") = "d1"
& skf96("d0") = "d1"
& skf95("d1") = "d1"
& skf95("d0") = "d0"
& skf98("d1") = "d1"
& skf97("d0") = "d1"
& skf98("d0") = "d1"
& skf97("d1") = "d1"
& skf99("d0") = "d1"
& skf99("d1") = "d1"
& skf67("d1") = "d1"
& skf67("d0") = "d1"
& skf69("d0") = "d0"
& skf68("d0") = "d1"
& skf68("d1") = "d0"
& skf69("d1") = "d0"
& skf70("d0") = "d0"
& skf70("d1") = "d0"
& skf72("d0") = "d0"
& skf71("d1") = "d0"
& skf72("d1") = "d0"
& skf71("d0") = "d0"
& skf74("d0") = "d0"
& skf73("d1") = "d0"
& skf74("d1") = "d0"
& skf73("d0") = "d0"
& skf76("d0") = "d0"
& skf75("d1") = "d0"
& skf76("d1") = "d0"
& skf75("d0") = "d0"
& skf78("d0") = "d0"
& skf77("d1") = "d0"
& skf78("d1") = "d0"
& skf77("d0") = "d0"
& skf79("d1") = "d0"
& skf79("d0") = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssPv26("d1")
& ~ ssPv27("d0")
& ~ ssPv26("d0")
& ssPv27("d1")
& ~ ssPv25("d0")
& ssPv25("d1")
& ssPv28("d1")
& ~ ssPv28("d0")
& ssPv22("d1")
& ssPv22("d0")
& ~ ssPv35("d1")
& ~ ssPv35("d0")
& ~ ssPv30("d0")
& ssPv30("d1")
& ssPv31("d1")
& ~ ssPv32("d0")
& ~ ssPv31("d0")
& ssPv32("d1")
& ~ ssPv16("d0")
& ssPv15("d1")
& ssPv16("d1")
& ~ ssPv15("d0")
& ssPv13("d1")
& ~ ssPv14("d0")
& ~ ssPv13("d0")
& ssPv14("d1")
& ssPv11("d1")
& ~ ssPv12("d0")
& ~ ssPv11("d0")
& ssPv12("d1")
& ~ ssPv10("d0")
& ssPv10("d1")
& ssPv7("d1")
& ssPv6("d0")
& ssPv7("d0")
& ssPv6("d1")
& ssSkP1190("d0")
& ssSkP1190("d1")
& ssSkP1193("d1")
& ssSkP1194("d0")
& ssSkP1193("d0")
& ssSkP1194("d1")
& ssSkP1191("d1")
& ssSkP1192("d0")
& ssSkP1191("d0")
& ssSkP1192("d1")
& ssSkP1197("d1")
& ssSkP1198("d0")
& ssSkP1197("d0")
& ssSkP1198("d1")
& ssSkP1195("d1")
& ssSkP1196("d0")
& ssSkP1195("d0")
& ssSkP1196("d1")
& ssSkP1199("d1")
& ssSkP1199("d0")
& ssSkP347("d1","d1")
& ssSkP347("d0","d0")
& ~ ssSkP1183("d0")
& ssSkP1182("d1")
& ssSkP347("d0","d1")
& ssSkP347("d1","d0")
& ssSkP1183("d1")
& ~ ssSkP1182("d0")
& ssSkP346("d1","d0")
& ssSkP346("d0","d1")
& ~ ssSkP1181("d0")
& ssSkP1180("d1")
& ssSkP346("d1","d1")
& ssSkP346("d0","d0")
& ssSkP1181("d1")
& ~ ssSkP1180("d0")
& ssSkP1187("d0")
& ssSkP1186("d1")
& ssSkP1187("d1")
& ssSkP1186("d0")
& ~ ssSkP1185("d0")
& ssSkP1184("d1")
& ssSkP1185("d1")
& ssSkP1184("d0")
& ssSkP1188("d1")
& ssSkP1189("d0")
& ssSkP1188("d0")
& ssSkP1189("d1")
& ~ ssSkP1172("d0")
& ssSkP1171("d1")
& ssSkP1172("d1")
& ~ ssSkP1171("d0")
& ~ ssSkP1170("d0")
& ssSkP1170("d1")
& ~ ssSkP1176("d0")
& ssSkP1175("d1")
& ssSkP1176("d1")
& ~ ssSkP1175("d0")
& ~ ssSkP1174("d0")
& ssSkP1173("d1")
& ssSkP1174("d1")
& ~ ssSkP1173("d0")
& ssSkP1179("d1")
& ~ ssSkP1179("d0")
& ~ ssSkP1178("d0")
& ssSkP1177("d1")
& ssSkP1178("d1")
& ~ ssSkP1177("d0")
& ~ ssSkP1161("d0")
& ssSkP1160("d1")
& ssSkP1161("d1")
& ~ ssSkP1160("d0")
& ssSkP1164("d1")
& ~ ssSkP1165("d0")
& ~ ssSkP1164("d0")
& ssSkP1165("d1")
& ssSkP1162("d1")
& ~ ssSkP1163("d0")
& ~ ssSkP1162("d0")
& ssSkP1163("d1")
& ssSkP1168("d1")
& ~ ssSkP1169("d0")
& ~ ssSkP1168("d0")
& ssSkP1169("d1")
& ~ ssSkP1167("d0")
& ssSkP1166("d1")
& ssSkP1167("d1")
& ~ ssSkP1166("d0")
& ~ ssSkP1150("d0")
& ssSkP1150("d1")
& ssSkP1153("d1")
& ~ ssSkP1154("d0")
& ~ ssSkP1153("d0")
& ssSkP1154("d1")
& ~ ssSkP1152("d0")
& ssSkP1151("d1")
& ssSkP1152("d1")
& ~ ssSkP1151("d0")
& ~ ssSkP1158("d0")
& ssSkP1157("d1")
& ssSkP1158("d1")
& ~ ssSkP1157("d0")
& ssSkP1155("d1")
& ~ ssSkP1155("d0")
& ssSkP1159("d1")
& ~ ssSkP1159("d0")
& ~ ssSkP1143("d0")
& ssSkP1142("d1")
& ssSkP1143("d1")
& ~ ssSkP1142("d0")
& ssSkP1140("d1")
& ssSkP1140("d0")
& ~ ssSkP1147("d0")
& ssSkP1146("d1")
& ssSkP1147("d1")
& ~ ssSkP1146("d0")
& ~ ssSkP1145("d0")
& ssSkP1144("d1")
& ssSkP1145("d1")
& ~ ssSkP1144("d0")
& ~ ssSkP1149("d0")
& ssSkP1148("d1")
& ssSkP1149("d1")
& ~ ssSkP1148("d0")
& ssSkP1132("d0")
& ssSkP1131("d1")
& ssSkP1132("d1")
& ssSkP1131("d0")
& ssSkP1130("d0")
& ssSkP1130("d1")
& ssSkP1136("d0")
& ssSkP1135("d1")
& ssSkP1136("d1")
& ssSkP1135("d0")
& ssSkP1134("d0")
& ssSkP1133("d1")
& ssSkP1134("d1")
& ssSkP1133("d0")
& ~ ssSkP1139("d1")
& ssSkP1139("d0")
& ssSkP1138("d0")
& ssSkP1137("d1")
& ssSkP1138("d1")
& ssSkP1137("d0")
& ~ ssSkP1119("d1")
& ~ ssSkP1119("d0")
& ssSkP1120("d1")
& ssSkP1121("d0")
& ssSkP1120("d0")
& ssSkP1121("d1")
& ssSkP1125("d0")
& ssSkP1124("d1")
& ssSkP1125("d1")
& ssSkP1124("d0")
& ssSkP1123("d0")
& ssSkP1122("d1")
& ssSkP1123("d1")
& ssSkP1122("d0")
& ssSkP1129("d0")
& ssSkP1128("d1")
& ssSkP1129("d1")
& ssSkP1128("d0")
& ssSkP1127("d0")
& ssSkP1126("d1")
& ssSkP1127("d1")
& ssSkP1126("d0")
& ~ ssSkP1109("d0")
& ~ ssSkP1108("d1")
& ~ ssSkP1109("d1")
& ~ ssSkP1108("d0")
& ~ ssSkP1110("d0")
& ~ ssSkP1110("d1")
& ~ ssSkP1113("d1")
& ~ ssSkP1114("d0")
& ssSkP1113("d0")
& ~ ssSkP1114("d1")
& ssSkP1111("d1")
& ~ ssSkP1112("d0")
& ~ ssSkP1111("d0")
& ~ ssSkP1112("d1")
& ~ ssSkP1118("d0")
& ~ ssSkP1117("d1")
& ~ ssSkP1118("d1")
& ~ ssSkP1117("d0")
& ~ ssSkP1116("d0")
& ~ ssSkP1115("d1")
& ~ ssSkP1116("d1")
& ~ ssSkP1115("d0")
& ~ ssSkP1103("d0")
& ~ ssSkP1103("d1")
& ~ ssSkP1107("d0")
& ~ ssSkP1106("d1")
& ~ ssSkP1107("d1")
& ~ ssSkP1106("d0")
& ~ ssSkP1105("d0")
& ~ ssSkP1104("d1")
& ~ ssSkP1105("d1")
& ~ ssSkP1104("d0")
& ssSkP619("d1")
& ~ ssSkP619("d0")
& ssSkP618("d0")
& ssSkP617("d1")
& ssSkP618("d1")
& ssSkP617("d0")
& ssSkP623("d0")
& ssSkP622("d1")
& ssSkP623("d1")
& ssSkP622("d0")
& ssSkP620("d1")
& ssSkP621("d0")
& ssSkP620("d0")
& ssSkP621("d1")
& ~ ssSkC30
& ssSkP649("d0")
& ssSkP648("d1")
& ssSkP649("d1")
& ssSkP648("d0")
& ssSkP647("d0")
& ssSkP646("d1")
& ssSkP647("d1")
& ssSkP646("d0")
& ssSkP652("d0")
& ssSkP651("d1")
& ssSkP652("d1")
& ssSkP651("d0")
& ssSkP650("d0")
& ssSkP650("d1")
& ~ ssSkP653("d1")
& ssSkP653("d0")
& ssSkP627("d0")
& ssSkP626("d1")
& ssSkP627("d1")
& ssSkP626("d0")
& ssSkP625("d0")
& ssSkP624("d1")
& ssSkP625("d1")
& ssSkP624("d0")
& ssSkP629("d0")
& ssSkP628("d1")
& ssSkP629("d1")
& ssSkP628("d0")
& ssSkP630("d0")
& ssSkP630("d1")
& ssSkP633("d1")
& ssSkP634("d0")
& ssSkP633("d0")
& ssSkP634("d1")
& ssSkP632("d0")
& ssSkP631("d1")
& ssSkP632("d1")
& ssSkP631("d0")
& ssSkP638("d0")
& ssSkP637("d1")
& ssSkP638("d1")
& ssSkP637("d0")
& ssSkP636("d0")
& ssSkP635("d1")
& ssSkP636("d1")
& ssSkP635("d0")
& ssSkP639("d1")
& ssSkP639("d0")
& ssSkP641("d0")
& ssSkP640("d1")
& ssSkP641("d1")
& ssSkP640("d0")
& ssSkP644("d1")
& ssSkP645("d0")
& ssSkP644("d0")
& ssSkP645("d1")
& ssSkP643("d0")
& ssSkP642("d1")
& ~ ssSkP643("d1")
& ssSkP642("d0")
& ssSkP428("d1","d1")
& ssSkP428("d0","d0")
& ssSkP428("d0","d1")
& ssSkP428("d1","d0")
& ssSkP427("d1","d0")
& ssSkP427("d0","d1")
& ssSkP427("d1","d1")
& ssSkP427("d0","d0")
& ~ ssSkC17
& ~ ssSkC12
& ~ ssSkC10
& ~ ssSkC29
& ssSkP1270("d1")
& ssSkP1271("d0")
& ssSkP1270("d0")
& ssSkP1271("d1")
& ssSkP1275("d0")
& ssSkP1274("d1")
& ~ ssSkP1275("d1")
& ssSkP1274("d0")
& ssSkP1273("d0")
& ssSkP1272("d1")
& ssSkP1273("d1")
& ssSkP1272("d0")
& ~ ssSkP1276("d1")
& ssSkP1276("d0")
& ssSkP1260("d0")
& ssSkP1260("d1")
& ssSkP1264("d0")
& ssSkP1263("d1")
& ssSkP1264("d1")
& ssSkP1263("d0")
& ssSkP1262("d0")
& ssSkP1261("d1")
& ssSkP1262("d1")
& ssSkP1261("d0")
& ssSkP1268("d0")
& ssSkP1267("d1")
& ssSkP1268("d1")
& ssSkP1267("d0")
& ssSkP1266("d0")
& ssSkP1265("d1")
& ssSkP1266("d1")
& ssSkP1265("d0")
& ssSkP1269("d1")
& ssSkP1269("d0")
& ssSkP1252("d1")
& ssSkP1253("d0")
& ssSkP1252("d0")
& ssSkP1253("d1")
& ssSkP1250("d1")
& ssSkP1251("d0")
& ssSkP1250("d0")
& ssSkP1251("d1")
& ssSkP1256("d1")
& ssSkP1257("d0")
& ssSkP1256("d0")
& ssSkP1257("d1")
& ssSkP1254("d1")
& ssSkP1255("d0")
& ssSkP1254("d0")
& ssSkP1255("d1")
& ssSkP1258("d1")
& ssSkP1259("d0")
& ssSkP1258("d0")
& ssSkP1259("d1")
& ssSkP1242("d0")
& ssSkP1241("d1")
& ssSkP1242("d1")
& ssSkP1241("d0")
& ssSkP1240("d0")
& ssSkP1240("d1")
& ssSkP1246("d0")
& ssSkP1245("d1")
& ssSkP1246("d1")
& ssSkP1245("d0")
& ssSkP1244("d0")
& ssSkP1243("d1")
& ssSkP1244("d1")
& ssSkP1243("d0")
& ssSkP1249("d1")
& ssSkP1249("d0")
& ssSkP1248("d0")
& ssSkP1247("d1")
& ssSkP1248("d1")
& ssSkP1247("d0")
& ssSkP1229("d1")
& ssSkP1229("d0")
& ssSkP1230("d1")
& ssSkP1231("d0")
& ssSkP1230("d0")
& ssSkP1231("d1")
& ssSkP1234("d1")
& ssSkP1235("d0")
& ssSkP1234("d0")
& ssSkP1235("d1")
& ssSkP1232("d1")
& ssSkP1233("d0")
& ssSkP1232("d0")
& ssSkP1233("d1")
& ssSkP1238("d1")
& ssSkP1239("d0")
& ssSkP1238("d0")
& ssSkP1239("d1")
& ssSkP1236("d1")
& ssSkP1237("d0")
& ssSkP1236("d0")
& ssSkP1237("d1")
& ssSkP1218("d1")
& ssSkP1219("d0")
& ssSkP1218("d0")
& ssSkP1219("d1")
& ssSkP1220("d0")
& ssSkP1220("d1")
& ssSkP1224("d0")
& ssSkP1223("d1")
& ssSkP1224("d1")
& ssSkP1223("d0")
& ssSkP1222("d0")
& ssSkP1221("d1")
& ssSkP1222("d1")
& ssSkP1221("d0")
& ssSkP1228("d0")
& ssSkP1227("d1")
& ssSkP1228("d1")
& ssSkP1227("d0")
& ssSkP1226("d0")
& ssSkP1225("d1")
& ssSkP1226("d1")
& ssSkP1225("d0")
& ssSkP1209("d1")
& ssSkP1209("d0")
& ssSkP1208("d0")
& ssSkP1207("d1")
& ssSkP1208("d1")
& ssSkP1207("d0")
& ssSkP1212("d1")
& ssSkP1213("d0")
& ssSkP1212("d0")
& ssSkP1213("d1")
& ssSkP1210("d1")
& ssSkP1211("d0")
& ssSkP1210("d0")
& ssSkP1211("d1")
& ssSkP1216("d1")
& ssSkP1217("d0")
& ssSkP1216("d0")
& ssSkP1217("d1")
& ssSkP1214("d1")
& ssSkP1215("d0")
& ssSkP1214("d0")
& ssSkP1215("d1")
& ssSkP1202("d0")
& ssSkP1201("d1")
& ssSkP1202("d1")
& ssSkP1201("d0")
& ssSkP1200("d0")
& ssSkP1200("d1")
& ssSkP1206("d0")
& ssSkP1205("d1")
& ssSkP1206("d1")
& ssSkP1205("d0")
& ssSkP1204("d0")
& ssSkP1203("d1")
& ssSkP1204("d1")
& ssSkP1203("d0")
& ssSkP615("d1","d0")
& ssSkP615("d0","d1")
& ssSkP616("d1","d1")
& ssSkP616("d0","d0")
& ssSkP615("d1","d1")
& ssSkP615("d0","d0")
& ssSkP616("d0","d1")
& ssSkP616("d1","d0")
& ~ ssSkP449("d1")
& ~ ssSkP448("d0")
& ~ ssSkP449("d0")
& ~ ssSkP448("d1")
& ~ ssSkP450("d1")
& ~ ssSkP450("d0")
& ~ ssSkP454("d1")
& ~ ssSkP453("d0")
& ~ ssSkP454("d0")
& ~ ssSkP453("d1")
& ~ ssSkP452("d1")
& ~ ssSkP451("d0")
& ~ ssSkP452("d0")
& ~ ssSkP451("d1")
& ~ ssSkP458("d1")
& ~ ssSkP457("d0")
& ~ ssSkP458("d0")
& ~ ssSkP457("d1")
& ~ ssSkP455("d0")
& ~ ssSkP456("d1")
& ~ ssSkP455("d1")
& ~ ssSkP456("d0")
& ~ ssSkP459("d0")
& ~ ssSkP459("d1")
& ssSkP460("d0")
& ssSkP461("d1")
& ssSkP460("d1")
& ssSkP461("d0")
& ssSkP465("d1")
& ssSkP464("d0")
& ssSkP465("d0")
& ssSkP464("d1")
& ssSkP463("d1")
& ssSkP462("d0")
& ssSkP463("d0")
& ssSkP462("d1")
& ~ ssSkP466("d0")
& ssSkP466("d1")
& ~ ssSkP429("d1")
& ~ ssSkP429("d0")
& ~ ssSkP432("d1")
& ~ ssSkP431("d0")
& ~ ssSkP432("d0")
& ~ ssSkP431("d1")
& ~ ssSkP430("d1")
& ~ ssSkP430("d0")
& ~ ssSkP436("d1")
& ~ ssSkP435("d0")
& ~ ssSkP436("d0")
& ~ ssSkP435("d1")
& ~ ssSkP434("d1")
& ~ ssSkP433("d0")
& ~ ssSkP434("d0")
& ~ ssSkP433("d1")
& ~ ssSkP439("d0")
& ~ ssSkP439("d1")
& ssSkP438("d1")
& ~ ssSkP437("d0")
& ~ ssSkP438("d0")
& ~ ssSkP437("d1")
& ~ ssSkP443("d1")
& ~ ssSkP442("d0")
& ~ ssSkP443("d0")
& ~ ssSkP442("d1")
& ~ ssSkP441("d1")
& ~ ssSkP440("d0")
& ~ ssSkP441("d0")
& ~ ssSkP440("d1")
& ~ ssSkP447("d1")
& ~ ssSkP446("d0")
& ~ ssSkP447("d0")
& ~ ssSkP446("d1")
& ~ ssSkP445("d1")
& ~ ssSkP444("d0")
& ~ ssSkP445("d0")
& ~ ssSkP444("d1")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0")
& ssSkP348("d1")
& ssSkP348("d0")
& ssSkP373("d1")
& ssSkP372("d0")
& ssSkP373("d0")
& ssSkP372("d1")
& ssSkP1156("d1","d1")
& ssSkP1156("d0","d0")
& ssSkP371("d1")
& ssSkP370("d0")
& ssSkP1156("d0","d1")
& ssSkP1156("d1","d0")
& ssSkP371("d0")
& ssSkP370("d1")
& ssSkP377("d1")
& ssSkP376("d0")
& ssSkP377("d0")
& ssSkP376("d1")
& ssSkP375("d1")
& ssSkP374("d0")
& ssSkP375("d0")
& ssSkP374("d1")
& ssSkP379("d1")
& ssSkP378("d0")
& ssSkP379("d0")
& ssSkP378("d1")
& ssSkP380("d1")
& ssSkP380("d0")
& ssSkP384("d1")
& ssSkP383("d0")
& ssSkP384("d0")
& ssSkP383("d1")
& ssSkP382("d1")
& ssSkP381("d0")
& ssSkP382("d0")
& ssSkP381("d1")
& ssSkP1141("d1","d1")
& ssSkP1141("d0","d0")
& ssSkP385("d0")
& ssSkP1141("d1","d0")
& ssSkP1141("d0","d1")
& ~ ssSkP385("d1")
& ssSkP349("d0")
& ssSkP349("d1")
& ssSkP351("d1")
& ssSkP350("d0")
& ssSkP351("d0")
& ssSkP350("d1")
& ssSkP355("d1")
& ~ ssSkP354("d0")
& ssSkP355("d0")
& ssSkP354("d1")
& ssSkP353("d1")
& ssSkP352("d0")
& ssSkP353("d0")
& ssSkP352("d1")
& ssSkP359("d1")
& ssSkP358("d0")
& ssSkP359("d0")
& ssSkP358("d1")
& ssSkP357("d1")
& ssSkP356("d0")
& ssSkP357("d0")
& ~ ssSkP356("d1")
& ssSkP362("d1")
& ssSkP361("d0")
& ssSkP362("d0")
& ssSkP361("d1")
& ssSkP360("d1")
& ssSkP360("d0")
& ssSkP366("d1")
& ssSkP365("d0")
& ssSkP366("d0")
& ssSkP365("d1")
& ssSkP364("d1")
& ssSkP363("d0")
& ssSkP364("d0")
& ssSkP363("d1")
& ssSkP369("d0")
& ssSkP369("d1")
& ssSkP368("d1")
& ssSkP367("d0")
& ssSkP368("d0")
& ssSkP367("d1")
& ssSkP1102("d0","d1")
& ssSkP1102("d1","d0")
& ssSkP1102("d1","d1")
& ssSkP1102("d0","d0")
& ssSkP1101("d1","d1")
& ssSkP1101("d0","d0")
& ssSkP1101("d1","d0")
& ssSkP1101("d0","d1") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN910-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 02:34:37 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.45 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.WxRrAxXf4p/theBenchmark.cnf 300
% 0.63/0.79 % domain size: 1
% 1.53/0.91 % domain size: 2
% 1.53/0.98 % model found for domain size 2
% 1.53/0.99 % SZS status CounterSatisfiable for theBenchmark
% 1.53/1.00 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.14/1.12 % FMB4L exiting
%------------------------------------------------------------------------------