%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN908-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 : n011.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.86s 1.27s
% Output : FiniteModel 2.26s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( skc41 = "d0"
& skf95("d0") = "d1"
& skf96("d0") = "d1"
& skf96("d1") = "d0"
& skf95("d1") = "d1"
& skf98("d0") = "d0"
& skf97("d1") = "d0"
& skf98("d1") = "d0"
& skf97("d0") = "d0"
& skf99("d1") = "d0"
& skf99("d0") = "d0"
& skf104("d0") = "d0"
& skf103("d1") = "d0"
& skf104("d1") = "d0"
& skf103("d0") = "d0"
& skf102("d0") = "d0"
& skf101("d1") = "d0"
& skf102("d1") = "d0"
& skf101("d0") = "d0"
& skf100("d0") = "d0"
& skf100("d1") = "d0"
& skf109("d1") = "d0"
& skf109("d0") = "d0"
& skf108("d0") = "d0"
& skf107("d1") = "d0"
& skf108("d1") = "d0"
& skf107("d0") = "d0"
& skf106("d0") = "d0"
& skf105("d1") = "d0"
& skf106("d1") = "d0"
& skf105("d0") = "d0"
& skf115("d0") = "d0"
& skf114("d1") = "d0"
& skf115("d1") = "d0"
& skf114("d0") = "d0"
& skf113("d0") = "d0"
& skf112("d1") = "d0"
& skf113("d1") = "d0"
& skf112("d0") = "d0"
& skf111("d0") = "d0"
& skf110("d1") = "d0"
& skf111("d1") = "d0"
& skf110("d0") = "d0"
& skf119("d1") = "d1"
& skf119("d0") = "d0"
& skf118("d1") = "d1"
& skf118("d0") = "d0"
& skf117("d1") = "d1"
& skf117("d0") = "d0"
& skf116("d1") = "d1"
& skf116("d0") = "d0"
& skf126("d1") = "d1"
& skf126("d0") = "d0"
& skf125("d1") = "d1"
& skf125("d0") = "d0"
& skf124("d1") = "d1"
& skf124("d0") = "d0"
& skf123("d1") = "d1"
& skf123("d0") = "d0"
& skf122("d1") = "d1"
& skf122("d0") = "d0"
& skf121("d1") = "d1"
& skf121("d0") = "d0"
& skf120("d1") = "d1"
& skf120("d0") = "d0"
& skf129("d1") = "d1"
& skf129("d0") = "d0"
& skf128("d1") = "d1"
& skf128("d0") = "d0"
& skf127("d1") = "d1"
& skf127("d0") = "d0"
& skf140("d1") = "d1"
& skf140("d0") = "d1"
& skf137("d1") = "d1"
& skf136("d0") = "d1"
& skf137("d0") = "d1"
& skf136("d1") = "d1"
& skf135("d1") = "d1"
& skf135("d0") = "d0"
& skf134("d1") = "d1"
& skf134("d0") = "d0"
& skf133("d0") = "d0"
& skf133("d1") = "d1"
& skf132("d1") = "d1"
& skf132("d0") = "d0"
& skf131("d0") = "d0"
& skf131("d1") = "d1"
& skf130("d1") = "d1"
& skf130("d0") = "d0"
& skf139("d1") = "d1"
& skf138("d0") = "d1"
& skf139("d0") = "d1"
& skf138("d1") = "d1"
& skf151("d1") = "d1"
& skf150("d0") = "d1"
& skf151("d0") = "d1"
& skf150("d1") = "d1"
& skf148("d1") = "d1"
& skf147("d0") = "d1"
& skf148("d0") = "d1"
& skf147("d1") = "d1"
& skf146("d1") = "d1"
& skf145("d0") = "d1"
& skf146("d0") = "d1"
& skf145("d1") = "d1"
& skf144("d1") = "d1"
& skf143("d0") = "d1"
& skf144("d0") = "d1"
& skf143("d1") = "d1"
& skf142("d1") = "d1"
& skf141("d0") = "d1"
& skf142("d0") = "d1"
& skf141("d1") = "d1"
& skf149("d0") = "d1"
& skf149("d1") = "d1"
& skf162("d1") = "d1"
& skf161("d0") = "d1"
& skf162("d0") = "d1"
& skf161("d1") = "d1"
& skf160("d1") = "d1"
& skf160("d0") = "d1"
& skf159("d1") = "d1"
& skf158("d0") = "d1"
& skf159("d0") = "d1"
& skf158("d1") = "d1"
& skf157("d1") = "d1"
& skf156("d0") = "d1"
& skf157("d0") = "d1"
& skf156("d1") = "d1"
& skf155("d1") = "d1"
& skf154("d0") = "d1"
& skf155("d0") = "d1"
& skf154("d1") = "d1"
& skf153("d1") = "d1"
& skf152("d0") = "d1"
& skf153("d0") = "d1"
& skf152("d1") = "d1"
& skf173("d1") = "d1"
& skf172("d0") = "d1"
& skf173("d0") = "d1"
& skf172("d1") = "d1"
& skf171("d1") = "d1"
& skf170("d0") = "d1"
& skf171("d0") = "d1"
& skf170("d1") = "d1"
& skf169("d0") = "d1"
& skf169("d1") = "d1"
& skf168("d1") = "d1"
& skf167("d0") = "d1"
& skf168("d0") = "d1"
& skf167("d1") = "d1"
& skf166("d1") = "d1"
& skf165("d0") = "d1"
& skf166("d0") = "d1"
& skf165("d1") = "d1"
& skf164("d1") = "d1"
& skf163("d0") = "d1"
& skf164("d0") = "d1"
& skf163("d1") = "d1"
& skf184("d1") = "d1"
& skf183("d0") = "d1"
& skf184("d0") = "d1"
& skf183("d1") = "d1"
& skf182("d1") = "d1"
& skf181("d0") = "d1"
& skf182("d0") = "d1"
& skf181("d1") = "d1"
& skf180("d1") = "d1"
& skf180("d0") = "d1"
& skf179("d1") = "d1"
& skf178("d0") = "d1"
& skf179("d0") = "d1"
& skf178("d1") = "d1"
& skf177("d1") = "d1"
& skf176("d0") = "d1"
& skf177("d0") = "d1"
& skf176("d1") = "d1"
& skf175("d1") = "d1"
& skf174("d0") = "d1"
& skf175("d0") = "d1"
& skf174("d1") = "d1"
& skf189("d0") = "d1"
& skf189("d1") = "d1"
& skf188("d1") = "d1"
& skf187("d0") = "d1"
& skf188("d0") = "d1"
& skf187("d1") = "d1"
& skf186("d1") = "d1"
& skf185("d0") = "d1"
& skf186("d0") = "d1"
& skf185("d1") = "d1" ) ).
fof(predicate_mappings,interpretation-mappings,
( ~ ssPv47("d0")
& ssPv47("d1")
& ~ ssPv41("d0")
& ssPv41("d1")
& ssPv44("d1")
& ~ ssPv45("d0")
& ~ ssPv44("d0")
& ssPv45("d1")
& ssPv42("d1")
& ~ ssPv43("d0")
& ~ ssPv42("d0")
& ssPv43("d1")
& ~ ssPv27("d0")
& ssPv26("d1")
& ssPv27("d1")
& ~ ssPv26("d0")
& ~ ssPv25("d0")
& ssPv25("d1")
& ~ ssPv29("d0")
& ssPv29("d1")
& ~ ssPv30("d0")
& ssPv30("d1")
& ssPv31("d1")
& ~ ssPv32("d0")
& ~ ssPv31("d0")
& ssPv32("d1")
& ssPv15("d1")
& ~ ssPv16("d0")
& ~ ssPv15("d0")
& ssPv16("d1")
& ~ ssPv14("d0")
& ssPv13("d1")
& ssPv14("d1")
& ~ ssPv13("d0")
& ~ ssPv12("d0")
& ssPv11("d1")
& ssPv12("d1")
& ~ ssPv11("d0")
& ssPv9("d1")
& ~ ssPv9("d0")
& ssSkP999("d0")
& ssSkP999("d1")
& ssSkP1190("d0")
& ~ ssSkP1190("d1")
& ~ ssSkP1191("d1")
& ssSkP1191("d0")
& ssSkP1183("d0")
& ssSkP1182("d1")
& ssSkP1183("d1")
& ssSkP1182("d0")
& ssSkP1181("d0")
& ssSkP1180("d1")
& ssSkP1181("d1")
& ssSkP1180("d0")
& ssSkP1187("d0")
& ssSkP1186("d1")
& ssSkP1187("d1")
& ssSkP1186("d0")
& ssSkP1185("d0")
& ssSkP1184("d1")
& ssSkP1185("d1")
& ssSkP1184("d0")
& ssSkP1188("d1")
& ssSkP1189("d0")
& ssSkP1189("d1")
& ssSkP1188("d0")
& ssSkP1171("d1")
& ssSkP1172("d0")
& ssSkP1171("d0")
& ssSkP1172("d1")
& ssSkP1170("d0")
& ssSkP1170("d1")
& ssSkP1176("d0")
& ssSkP1175("d1")
& ssSkP1175("d0")
& ssSkP1176("d1")
& ssSkP1174("d0")
& ssSkP1173("d1")
& ssSkP1173("d0")
& ssSkP1174("d1")
& ssSkP1179("d1")
& ssSkP1179("d0")
& ssSkP1177("d1")
& ssSkP1178("d0")
& ssSkP1177("d0")
& ssSkP1178("d1")
& ssSkP1161("d0")
& ssSkP1160("d1")
& ssSkP1161("d1")
& ssSkP1160("d0")
& ssSkP1164("d1")
& ssSkP1165("d0")
& ssSkP1164("d0")
& ssSkP1165("d1")
& ssSkP1163("d0")
& ssSkP1162("d1")
& ssSkP1163("d1")
& ssSkP1162("d0")
& ssSkP1021("d0","d1")
& ssSkP1021("d1","d0")
& ssSkP1169("d0")
& ssSkP1168("d1")
& ssSkP1021("d1","d1")
& ssSkP1021("d0","d0")
& ssSkP1169("d1")
& ssSkP1168("d0")
& ssSkP1167("d0")
& ssSkP1166("d1")
& ssSkP1167("d1")
& ssSkP1166("d0")
& ssSkP1150("d0")
& ssSkP1150("d1")
& ssSkP1153("d1")
& ssSkP1154("d0")
& ssSkP1153("d0")
& ssSkP1154("d1")
& ssSkP1151("d1")
& ssSkP1152("d0")
& ssSkP1151("d0")
& ssSkP1152("d1")
& ssSkP1157("d1")
& ssSkP1158("d0")
& ssSkP1157("d0")
& ssSkP1158("d1")
& ssSkP1155("d1")
& ssSkP1156("d0")
& ssSkP1155("d0")
& ssSkP1156("d1")
& ssSkP1159("d1")
& ssSkP1159("d0")
& ssSkP1143("d0")
& ssSkP1142("d1")
& ssSkP1143("d1")
& ssSkP1142("d0")
& ssSkP1141("d0")
& ssSkP1140("d1")
& ssSkP1141("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")
& ssSkP1131("d1")
& ssSkP1132("d0")
& ssSkP1131("d0")
& ssSkP1132("d1")
& ssSkP1130("d0")
& ssSkP1130("d1")
& ssSkP1135("d1")
& ssSkP1136("d0")
& ssSkP1135("d0")
& ssSkP1136("d1")
& ssSkP1133("d1")
& ssSkP1134("d0")
& ssSkP1133("d0")
& ssSkP1134("d1")
& ssSkP1139("d1")
& ssSkP1139("d0")
& ssSkP1137("d1")
& ssSkP1138("d0")
& ssSkP1137("d0")
& ssSkP1138("d1")
& ssSkP1119("d1")
& ssSkP1119("d0")
& ssSkP1121("d0")
& ssSkP1120("d1")
& ssSkP1121("d1")
& ssSkP1120("d0")
& 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")
& ssSkP1117("d1")
& ssSkP1118("d0")
& ssSkP1117("d0")
& ssSkP1118("d1")
& ssSkP1115("d1")
& ssSkP1116("d0")
& ssSkP1115("d0")
& ssSkP1116("d1")
& ssSkP1000("d1","d1")
& ssSkP1000("d0","d0")
& ssSkP1103("d0")
& ssSkP1102("d1")
& ssSkP1000("d1","d0")
& ssSkP1000("d0","d1")
& ssSkP1103("d1")
& ssSkP1102("d0")
& ssSkP1101("d0")
& ssSkP1100("d1")
& ssSkP1101("d1")
& ssSkP1100("d0")
& ssSkP1107("d0")
& ssSkP1106("d1")
& ssSkP1107("d1")
& ssSkP1106("d0")
& ssSkP1105("d0")
& ssSkP1104("d1")
& ssSkP1105("d1")
& ssSkP1104("d0")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0")
& ssSkP1091("d0")
& ssSkP1090("d1")
& ssSkP1091("d1")
& ssSkP1090("d0")
& ssSkP1095("d0")
& ssSkP1094("d1")
& ssSkP1095("d1")
& ssSkP1094("d0")
& ssSkP1093("d0")
& ssSkP1092("d1")
& ssSkP1093("d1")
& ssSkP1092("d0")
& ssSkP1099("d0")
& ssSkP1098("d1")
& ssSkP1099("d1")
& ssSkP1098("d0")
& ssSkP1097("d0")
& ssSkP1096("d1")
& ssSkP1097("d1")
& ssSkP1096("d0")
& ssSkP1080("d0")
& ssSkP1080("d1")
& ssSkP1083("d1")
& ssSkP1084("d0")
& ssSkP1083("d0")
& ssSkP1084("d1")
& ssSkP1081("d1")
& ssSkP1082("d0")
& ssSkP1081("d0")
& ssSkP1082("d1")
& ssSkP1087("d1")
& ssSkP1088("d0")
& ssSkP1087("d0")
& ssSkP1088("d1")
& ssSkP1085("d1")
& ssSkP1086("d0")
& ssSkP1085("d0")
& ssSkP1086("d1")
& ssSkP1089("d1")
& ssSkP1089("d0")
& ssSkP1072("d1")
& ssSkP1073("d0")
& ssSkP1072("d0")
& ssSkP1073("d1")
& ssSkP1070("d1")
& ssSkP1071("d0")
& ssSkP1070("d0")
& ssSkP1071("d1")
& ssSkP1076("d1")
& ssSkP1077("d0")
& ssSkP1076("d0")
& ssSkP1077("d1")
& ssSkP1074("d1")
& ssSkP1075("d0")
& ssSkP1074("d0")
& ssSkP1075("d1")
& ssSkP1078("d1")
& ssSkP1079("d0")
& ssSkP1078("d0")
& ssSkP1079("d1")
& ~ ssSkP1062("d0")
& ssSkP1061("d1")
& ssSkP1062("d1")
& ~ ssSkP1061("d0")
& ~ ssSkP1060("d0")
& ssSkP1060("d1")
& ssSkP1066("d0")
& ssSkP1065("d1")
& ssSkP1065("d0")
& ssSkP1066("d1")
& ssSkP1064("d0")
& ssSkP1063("d1")
& ssSkP1064("d1")
& ssSkP1063("d0")
& ssSkP1069("d1")
& ssSkP1069("d0")
& ssSkP1067("d1")
& ssSkP1068("d0")
& ssSkP1067("d0")
& ssSkP1068("d1")
& ssSkP1050("d1")
& ssSkP1051("d0")
& ~ ssSkP1050("d0")
& ssSkP1051("d1")
& ~ ssSkP1055("d0")
& ssSkP1054("d1")
& ssSkP1055("d1")
& ~ ssSkP1054("d0")
& ~ ssSkP1053("d0")
& ssSkP1052("d1")
& ssSkP1053("d1")
& ~ ssSkP1052("d0")
& ~ ssSkP1059("d0")
& ssSkP1058("d1")
& ssSkP1059("d1")
& ~ ssSkP1058("d0")
& ~ ssSkP1057("d0")
& ssSkP1056("d1")
& ssSkP1057("d1")
& ~ ssSkP1056("d0")
& ~ ssSkP1040("d0")
& ssSkP1040("d1")
& ~ ssSkP1044("d0")
& ssSkP1043("d1")
& ~ ssSkC20
& ssSkP1044("d1")
& ~ ssSkP1043("d0")
& ~ ssSkP1042("d0")
& ssSkP1041("d1")
& ~ ssSkP1041("d0")
& ssSkP1042("d1")
& ~ ssSkP1048("d0")
& ssSkP1047("d1")
& ssSkP1048("d1")
& ~ ssSkP1047("d0")
& ~ ssSkP1046("d0")
& ssSkP1045("d1")
& ssSkP1046("d1")
& ~ ssSkP1045("d0")
& ssSkP1049("d1")
& ~ ssSkP1049("d0")
& ~ ssSkP1033("d0")
& ssSkP1032("d1")
& ssSkP1033("d1")
& ~ ssSkP1032("d0")
& ssSkP1030("d1")
& ~ ssSkP1031("d0")
& ~ ssSkP1030("d0")
& ssSkP1031("d1")
& ssSkP1036("d1")
& ~ ssSkP1037("d0")
& ~ ssSkP1036("d0")
& ssSkP1037("d1")
& ~ ssSkP1035("d0")
& ssSkP1034("d1")
& ssSkP1035("d1")
& ~ ssSkP1034("d0")
& ssSkP1038("d1")
& ~ ssSkP1039("d0")
& ~ ssSkP1038("d0")
& ssSkP1039("d1")
& ~ ssSkP1022("d0")
& ssSkP1022("d1")
& ~ ssSkP1020("d0")
& ssSkP1020("d1")
& ~ ssSkP1026("d0")
& ssSkP1025("d1")
& ssSkP1026("d1")
& ~ ssSkP1025("d0")
& ~ ssSkP1024("d0")
& ssSkP1023("d1")
& ssSkP1024("d1")
& ~ ssSkP1023("d0")
& ssSkP1029("d1")
& ~ ssSkP1029("d0")
& ssSkP1027("d1")
& ~ ssSkP1028("d0")
& ~ ssSkP1027("d0")
& ssSkP1028("d1")
& ssSkP1009("d1")
& ~ ssSkP1009("d0")
& ~ ssSkP1011("d0")
& ssSkP1010("d1")
& ssSkP1011("d1")
& ~ ssSkP1010("d0")
& ssSkP1014("d1")
& ~ ssSkP1015("d0")
& ~ ssSkP1014("d0")
& ssSkP1015("d1")
& ~ ssSkP1013("d0")
& ssSkP1012("d1")
& ssSkP1013("d1")
& ~ ssSkP1012("d0")
& ssSkP1018("d1")
& ~ ssSkP1019("d0")
& ~ ssSkP1018("d0")
& ssSkP1019("d1")
& ssSkP1016("d1")
& ~ ssSkP1017("d0")
& ~ ssSkP1016("d0")
& ssSkP1017("d1")
& ssSkP1003("d1")
& ~ ssSkP1004("d0")
& ~ ssSkP1003("d0")
& ssSkP1004("d1")
& ~ ssSkP1002("d0")
& ssSkP1001("d1")
& ssSkP1002("d1")
& ~ ssSkP1001("d0")
& ssSkP1007("d1")
& ~ ssSkP1008("d0")
& ~ ssSkP1007("d0")
& ssSkP1008("d1")
& ~ ssSkP1006("d0")
& ssSkP1005("d1")
& ssSkP1006("d1")
& ~ ssSkP1005("d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYN908-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.14/0.41 % Computer : n011.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Fri Sep 25 02:32:28 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.23/0.56 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.sJAtSGCGHf/theBenchmark.cnf 300
% 0.32/1.03 % domain size: 1
% 1.67/1.17 % domain size: 2
% 1.86/1.25 % model found for domain size 2
% 1.86/1.27 % SZS status CounterSatisfiable for theBenchmark
% 1.86/1.27 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.32/1.41 % FMB4L exiting
%------------------------------------------------------------------------------