%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SYN424+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n014.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 : 600s % DateTime : Thu Jul 21 03:02:11 EDT 2022 % Result : CounterSatisfiable 5.57s 5.77s % Output : FiniteModel 5.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SYN424+1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.12 % Command : do_Crossbow---0.1 %s % 0.12/0.32 % Computer : n014.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 600 % 0.12/0.32 % DateTime : Tue Jul 12 06:54:04 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 /export/starexec/sandbox/solver/bin % 0.12/0.33 crossbow.opt % 0.12/0.33 do_Crossbow---0.1 % 0.12/0.33 eprover % 0.12/0.33 runsolver % 0.12/0.33 starexec_run_Crossbow---0.1 % 5.57/5.77 % SZS status CounterSatisfiable for theBenchmark.p % 5.57/5.77 % SZS output start FiniteModel for theBenchmark.p % 5.57/5.77 % domain size: 2 % 5.57/5.77 fof(interp, fi_domain, ![X] : (X = 0 | X = 1)). % 5.57/5.77 fof(interp, fi_functors, a1000 = 0). % 5.57/5.77 fof(interp, fi_functors, a1001 = 0). % 5.57/5.77 fof(interp, fi_functors, a1002 = 0). % 5.57/5.77 fof(interp, fi_functors, a1003 = 0). % 5.57/5.77 fof(interp, fi_functors, a1004 = 0). % 5.57/5.77 fof(interp, fi_functors, a1005 = 0). % 5.57/5.77 fof(interp, fi_functors, a1006 = 0). % 5.57/5.77 fof(interp, fi_functors, a1007 = 0). % 5.57/5.77 fof(interp, fi_functors, a1008 = 1). % 5.57/5.77 fof(interp, fi_functors, a1009 = 1). % 5.57/5.77 fof(interp, fi_functors, a1010 = 1). % 5.57/5.77 fof(interp, fi_functors, a1011 = 1). % 5.57/5.77 fof(interp, fi_functors, a1012 = 0). % 5.57/5.77 fof(interp, fi_functors, a1013 = 0). % 5.57/5.77 fof(interp, fi_functors, a1014 = 0). % 5.57/5.77 fof(interp, fi_functors, a1015 = 0). % 5.57/5.77 fof(interp, fi_functors, a1016 = 0). % 5.57/5.77 fof(interp, fi_functors, a1017 = 0). % 5.57/5.77 fof(interp, fi_functors, a1018 = 1). % 5.57/5.77 fof(interp, fi_functors, a1019 = 0). % 5.57/5.77 fof(interp, fi_functors, a1020 = 0). % 5.57/5.77 fof(interp, fi_functors, a1021 = 0). % 5.57/5.77 fof(interp, fi_functors, a1022 = 0). % 5.57/5.77 fof(interp, fi_functors, a1023 = 0). % 5.57/5.77 fof(interp, fi_functors, a1024 = 0). % 5.57/5.77 fof(interp, fi_functors, a1025 = 0). % 5.57/5.77 fof(interp, fi_functors, a1026 = 0). % 5.57/5.77 fof(interp, fi_functors, a1027 = 0). % 5.57/5.77 fof(interp, fi_functors, a1028 = 0). % 5.57/5.77 fof(interp, fi_functors, a1029 = 0). % 5.57/5.77 fof(interp, fi_functors, a1030 = 1). % 5.57/5.77 fof(interp, fi_functors, a1031 = 1). % 5.57/5.77 fof(interp, fi_functors, a1032 = 0). % 5.57/5.77 fof(interp, fi_functors, a1033 = 1). % 5.57/5.77 fof(interp, fi_functors, a1034 = 1). % 5.57/5.77 fof(interp, fi_functors, a1035 = 1). % 5.57/5.77 fof(interp, fi_functors, a1036 = 0). % 5.57/5.77 fof(interp, fi_functors, a1037 = 1). % 5.57/5.77 fof(interp, fi_functors, a1038 = 0). % 5.57/5.77 fof(interp, fi_functors, a1039 = 1). % 5.57/5.77 fof(interp, fi_functors, a1040 = 1). % 5.57/5.77 fof(interp, fi_functors, a1041 = 0). % 5.57/5.77 fof(interp, fi_functors, a1042 = 0). % 5.57/5.77 fof(interp, fi_functors, a1043 = 1). % 5.57/5.77 fof(interp, fi_functors, a1044 = 0). % 5.57/5.77 fof(interp, fi_functors, a1045 = 0). % 5.57/5.77 fof(interp, fi_functors, a1046 = 1). % 5.57/5.77 fof(interp, fi_functors, a1047 = 0). % 5.57/5.77 fof(interp, fi_functors, a1048 = 1). % 5.57/5.77 fof(interp, fi_functors, a1049 = 1). % 5.57/5.77 fof(interp, fi_functors, a1050 = 0). % 5.57/5.77 fof(interp, fi_functors, a1051 = 0). % 5.57/5.77 fof(interp, fi_functors, a1052 = 0). % 5.57/5.77 fof(interp, fi_functors, a1053 = 0). % 5.57/5.77 fof(interp, fi_functors, a1054 = 0). % 5.57/5.77 fof(interp, fi_functors, a1055 = 0). % 5.57/5.77 fof(interp, fi_functors, a1056 = 0). % 5.57/5.77 fof(interp, fi_functors, a1057 = 0). % 5.57/5.77 fof(interp, fi_functors, a1058 = 1). % 5.57/5.77 fof(interp, fi_functors, a1059 = 1). % 5.57/5.77 fof(interp, fi_functors, a1060 = 0). % 5.57/5.77 fof(interp, fi_functors, a1061 = 0). % 5.57/5.77 fof(interp, fi_functors, a1062 = 1). % 5.57/5.77 fof(interp, fi_functors, a1063 = 1). % 5.57/5.77 fof(interp, fi_functors, a1064 = 0). % 5.57/5.77 fof(interp, fi_functors, a1065 = 0). % 5.57/5.77 fof(interp, fi_functors, a1066 = 0). % 5.57/5.77 fof(interp, fi_functors, a1067 = 1). % 5.57/5.77 fof(interp, fi_functors, a1068 = 0). % 5.57/5.77 fof(interp, fi_functors, a1069 = 0). % 5.57/5.77 fof(interp, fi_functors, a1070 = 0). % 5.57/5.77 fof(interp, fi_functors, a1071 = 0). % 5.57/5.77 fof(interp, fi_functors, a1072 = 0). % 5.57/5.77 fof(interp, fi_functors, a1073 = 0). % 5.57/5.77 fof(interp, fi_functors, a1074 = 0). % 5.57/5.77 fof(interp, fi_functors, a1075 = 0). % 5.57/5.77 fof(interp, fi_functors, a1076 = 0). % 5.57/5.77 fof(interp, fi_functors, a1077 = 1). % 5.57/5.77 fof(interp, fi_functors, a1078 = 1). % 5.57/5.77 fof(interp, fi_functors, a1079 = 0). % 5.57/5.77 fof(interp, fi_functors, a1080 = 0). % 5.57/5.77 fof(interp, fi_functors, a1081 = 0). % 5.57/5.77 fof(interp, fi_functors, a1082 = 0). % 5.57/5.77 fof(interp, fi_functors, a1083 = 0). % 5.57/5.77 fof(interp, fi_functors, a1084 = 1). % 5.57/5.77 fof(interp, fi_functors, a1085 = 1). % 5.57/5.77 fof(interp, fi_functors, a1086 = 0). % 5.57/5.77 fof(interp, fi_functors, a1087 = 0). % 5.57/5.77 fof(interp, fi_functors, a1088 = 1). % 5.57/5.77 fof(interp, fi_functors, a1089 = 0). % 5.57/5.77 fof(interp, fi_functors, a1090 = 0). % 5.57/5.77 fof(interp, fi_functors, a1091 = 0). % 5.57/5.77 fof(interp, fi_functors, a1092 = 1). % 5.57/5.77 fof(interp, fi_functors, a1093 = 1). % 5.57/5.77 fof(interp, fi_functors, a1094 = 0). % 5.57/5.77 fof(interp, fi_functors, a1095 = 0). % 5.57/5.77 fof(interp, fi_functors, a1096 = 0). % 5.57/5.77 fof(interp, fi_functors, a1097 = 0). % 5.57/5.77 fof(interp, fi_functors, a1098 = 0). % 5.57/5.77 fof(interp, fi_functors, a1099 = 1). % 5.57/5.77 fof(interp, fi_functors, a1100 = 1). % 5.57/5.77 fof(interp, fi_functors, a1101 = 0). % 5.57/5.77 fof(interp, fi_functors, a1102 = 0). % 5.57/5.77 fof(interp, fi_functors, a1103 = 1). % 5.57/5.77 fof(interp, fi_functors, a1104 = 0). % 5.57/5.77 fof(interp, fi_functors, a1105 = 0). % 5.57/5.77 fof(interp, fi_functors, a1106 = 0). % 5.57/5.77 fof(interp, fi_functors, a1107 = 0). % 5.57/5.77 fof(interp, fi_functors, a1108 = 1). % 5.57/5.77 fof(interp, fi_functors, a1109 = 1). % 5.57/5.77 fof(interp, fi_functors, a1110 = 1). % 5.57/5.77 fof(interp, fi_functors, a1111 = 1). % 5.57/5.77 fof(interp, fi_functors, a1112 = 0). % 5.57/5.77 fof(interp, fi_functors, a1113 = 0). % 5.57/5.77 fof(interp, fi_functors, a1114 = 0). % 5.57/5.77 fof(interp, fi_functors, a1115 = 0). % 5.57/5.77 fof(interp, fi_functors, a1116 = 0). % 5.57/5.77 fof(interp, fi_functors, a1117 = 0). % 5.57/5.77 fof(interp, fi_functors, a1118 = 1). % 5.57/5.77 fof(interp, fi_functors, a1119 = 0). % 5.57/5.77 fof(interp, fi_functors, a1120 = 0). % 5.57/5.77 fof(interp, fi_functors, a1121 = 1). % 5.57/5.77 fof(interp, fi_functors, a1122 = 1). % 5.57/5.77 fof(interp, fi_functors, a1123 = 1). % 5.57/5.77 fof(interp, fi_functors, a1124 = 0). % 5.57/5.77 fof(interp, fi_functors, a1125 = 1). % 5.57/5.77 fof(interp, fi_functors, a1126 = 0). % 5.57/5.77 fof(interp, fi_functors, a1127 = 1). % 5.57/5.77 fof(interp, fi_functors, a1128 = 1). % 5.57/5.77 fof(interp, fi_functors, a1129 = 1). % 5.57/5.77 fof(interp, fi_functors, a1130 = 1). % 5.57/5.77 fof(interp, fi_functors, a1131 = 1). % 5.57/5.77 fof(interp, fi_functors, a1132 = 0). % 5.57/5.77 fof(interp, fi_functors, a1133 = 0). % 5.57/5.77 fof(interp, fi_functors, a1134 = 1). % 5.57/5.77 fof(interp, fi_functors, a1135 = 1). % 5.57/5.77 fof(interp, fi_functors, a1136 = 0). % 5.57/5.77 fof(interp, fi_functors, a1137 = 1). % 5.57/5.77 fof(interp, fi_functors, a1138 = 1). % 5.57/5.77 fof(interp, fi_functors, a1139 = 1). % 5.57/5.77 fof(interp, fi_functors, a1140 = 0). % 5.57/5.77 fof(interp, fi_functors, a1141 = 1). % 5.57/5.77 fof(interp, fi_functors, a1142 = 0). % 5.57/5.77 fof(interp, fi_functors, a1143 = 1). % 5.57/5.77 fof(interp, fi_functors, a1144 = 1). % 5.57/5.77 fof(interp, fi_functors, a1145 = 1). % 5.57/5.77 fof(interp, fi_functors, a1146 = 0). % 5.57/5.77 fof(interp, fi_functors, a1147 = 0). % 5.57/5.77 fof(interp, fi_functors, a1148 = 0). % 5.57/5.77 fof(interp, fi_functors, a1149 = 0). % 5.57/5.77 fof(interp, fi_functors, a1150 = 0). % 5.57/5.77 fof(interp, fi_functors, a1151 = 0). % 5.57/5.77 fof(interp, fi_functors, a1152 = 0). % 5.57/5.77 fof(interp, fi_functors, a1153 = 0). % 5.57/5.77 fof(interp, fi_functors, a1154 = 0). % 5.57/5.77 fof(interp, fi_functors, a1155 = 1). % 5.57/5.77 fof(interp, fi_functors, a1156 = 0). % 5.57/5.77 fof(interp, fi_functors, a1157 = 0). % 5.57/5.77 fof(interp, fi_functors, a1158 = 0). % 5.57/5.77 fof(interp, fi_functors, a1159 = 0). % 5.57/5.77 fof(interp, fi_functors, a1160 = 1). % 5.57/5.77 fof(interp, fi_functors, a1161 = 1). % 5.57/5.77 fof(interp, fi_functors, a1162 = 0). % 5.57/5.77 fof(interp, fi_functors, a1163 = 1). % 5.57/5.77 fof(interp, fi_functors, a1164 = 0). % 5.57/5.77 fof(interp, fi_functors, a1165 = 0). % 5.57/5.77 fof(interp, fi_functors, a1166 = 0). % 5.57/5.77 fof(interp, fi_functors, a1167 = 0). % 5.57/5.77 fof(interp, fi_functors, a1168 = 0). % 5.57/5.77 fof(interp, fi_functors, a1169 = 0). % 5.57/5.77 fof(interp, fi_functors, a1170 = 1). % 5.57/5.77 fof(interp, fi_functors, a1171 = 0). % 5.57/5.77 fof(interp, fi_functors, a1172 = 0). % 5.57/5.77 fof(interp, fi_functors, a1173 = 0). % 5.57/5.77 fof(interp, fi_functors, a1174 = 0). % 5.57/5.77 fof(interp, fi_functors, a1175 = 0). % 5.57/5.77 fof(interp, fi_functors, a1176 = 0). % 5.57/5.77 fof(interp, fi_functors, a1177 = 1). % 5.57/5.77 fof(interp, fi_functors, a1178 = 0). % 5.57/5.77 fof(interp, fi_functors, a1179 = 0). % 5.57/5.77 fof(interp, fi_functors, a1180 = 0). % 5.57/5.77 fof(interp, fi_functors, a1181 = 1). % 5.57/5.77 fof(interp, fi_functors, a1182 = 0). % 5.57/5.77 fof(interp, fi_functors, a1183 = 0). % 5.57/5.77 fof(interp, fi_functors, a1184 = 0). % 5.57/5.77 fof(interp, fi_functors, a1185 = 0). % 5.57/5.77 fof(interp, fi_functors, a1186 = 0). % 5.57/5.77 fof(interp, fi_functors, a1187 = 0). % 5.57/5.77 fof(interp, fi_functors, a1188 = 0). % 5.57/5.77 fof(interp, fi_functors, a1189 = 0). % 5.57/5.77 fof(interp, fi_functors, a960 = 1). % 5.57/5.77 fof(interp, fi_functors, a961 = 0). % 5.57/5.77 fof(interp, fi_functors, a962 = 0). % 5.57/5.77 fof(interp, fi_functors, a963 = 0). % 5.57/5.77 fof(interp, fi_functors, a964 = 0). % 5.57/5.77 fof(interp, fi_functors, a965 = 0). % 5.57/5.77 fof(interp, fi_functors, a966 = 0). % 5.57/5.77 fof(interp, fi_functors, a967 = 0). % 5.57/5.77 fof(interp, fi_functors, a968 = 0). % 5.57/5.77 fof(interp, fi_functors, a969 = 0). % 5.57/5.77 fof(interp, fi_functors, a970 = 1). % 5.57/5.77 fof(interp, fi_functors, a971 = 1). % 5.57/5.77 fof(interp, fi_functors, a972 = 0). % 5.57/5.77 fof(interp, fi_functors, a973 = 0). % 5.57/5.77 fof(interp, fi_functors, a974 = 0). % 5.57/5.77 fof(interp, fi_functors, a975 = 0). % 5.57/5.77 fof(interp, fi_functors, a976 = 1). % 5.57/5.77 fof(interp, fi_functors, a977 = 0). % 5.57/5.77 fof(interp, fi_functors, a978 = 0). % 5.57/5.77 fof(interp, fi_functors, a979 = 1). % 5.57/5.77 fof(interp, fi_functors, a980 = 0). % 5.57/5.77 fof(interp, fi_functors, a981 = 1). % 5.57/5.77 fof(interp, fi_functors, a982 = 0). % 5.57/5.77 fof(interp, fi_functors, a983 = 1). % 5.57/5.77 fof(interp, fi_functors, a984 = 0). % 5.57/5.77 fof(interp, fi_functors, a985 = 0). % 5.57/5.77 fof(interp, fi_functors, a986 = 1). % 5.57/5.77 fof(interp, fi_functors, a987 = 0). % 5.57/5.77 fof(interp, fi_functors, a988 = 0). % 5.57/5.77 fof(interp, fi_functors, a989 = 0). % 5.57/5.77 fof(interp, fi_functors, a990 = 0). % 5.57/5.77 fof(interp, fi_functors, a991 = 0). % 5.57/5.77 fof(interp, fi_functors, a992 = 1). % 5.57/5.77 fof(interp, fi_functors, a993 = 1). % 5.57/5.77 fof(interp, fi_functors, a994 = 1). % 5.57/5.77 fof(interp, fi_functors, a995 = 0). % 5.57/5.77 fof(interp, fi_functors, a996 = 0). % 5.57/5.77 fof(interp, fi_functors, a997 = 0). % 5.57/5.77 fof(interp, fi_functors, a998 = 0). % 5.57/5.77 fof(interp, fi_functors, a999 = 0). % 5.57/5.77 fof(interp, fi_predicates, ~c10_0). % 5.57/5.77 fof(interp, fi_predicates, c10_1(0) & ~c10_1(1)). % 5.57/5.77 fof(interp, fi_predicates, c10_2(0, 0) & ~c10_2(0, 1) & ~c10_2(1, 0) & % 5.57/5.77 c10_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, c1_0). % 5.57/5.77 fof(interp, fi_predicates, ~c1_1(0) & ~c1_1(1)). % 5.57/5.77 fof(interp, fi_predicates, c1_2(0, 0) & c1_2(0, 1) & c1_2(1, 0) & ~c1_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, c2_0). % 5.57/5.77 fof(interp, fi_predicates, ~c2_1(0) & ~c2_1(1)). % 5.57/5.77 fof(interp, fi_predicates, ~c2_2(0, 0) & c2_2(0, 1) & c2_2(1, 0) & ~c2_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, c3_0). % 5.57/5.77 fof(interp, fi_predicates, c3_1(0) & c3_1(1)). % 5.57/5.77 fof(interp, fi_predicates, c3_2(0, 0) & ~c3_2(0, 1) & ~c3_2(1, 0) & c3_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, c4_0). % 5.57/5.77 fof(interp, fi_predicates, c4_1(0) & ~c4_1(1)). % 5.57/5.77 fof(interp, fi_predicates, c4_2(0, 0) & ~c4_2(0, 1) & ~c4_2(1, 0) & c4_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, ~c5_0). % 5.57/5.77 fof(interp, fi_predicates, c5_1(0) & ~c5_1(1)). % 5.57/5.77 fof(interp, fi_predicates, ~c5_2(0, 0) & ~c5_2(0, 1) & ~c5_2(1, 0) & c5_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, c6_0). % 5.57/5.77 fof(interp, fi_predicates, ~c6_1(0) & ~c6_1(1)). % 5.57/5.77 fof(interp, fi_predicates, ~c6_2(0, 0) & c6_2(0, 1) & ~c6_2(1, 0) & ~c6_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, c7_0). % 5.57/5.77 fof(interp, fi_predicates, c7_1(0) & ~c7_1(1)). % 5.57/5.77 fof(interp, fi_predicates, c7_2(0, 0) & ~c7_2(0, 1) & ~c7_2(1, 0) & ~c7_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, ~c8_0). % 5.57/5.77 fof(interp, fi_predicates, ~c8_1(0) & c8_1(1)). % 5.57/5.77 fof(interp, fi_predicates, ~c8_2(0, 0) & ~c8_2(0, 1) & c8_2(1, 0) & c8_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, ~c9_0). % 5.57/5.77 fof(interp, fi_predicates, c9_1(0) & ~c9_1(1)). % 5.57/5.77 fof(interp, fi_predicates, c9_2(0, 0) & c9_2(0, 1) & ~c9_2(1, 0) & c9_2(1, 1)). % 5.57/5.77 fof(interp, fi_predicates, ~epred10_0). % 5.57/5.77 fof(interp, fi_predicates, ~epred11_0). % 5.57/5.77 fof(interp, fi_predicates, epred12_0). % 5.57/5.77 fof(interp, fi_predicates, epred13_0). % 5.57/5.77 fof(interp, fi_predicates, epred14_0). % 5.57/5.77 fof(interp, fi_predicates, ~epred1_0). % 5.57/5.77 fof(interp, fi_predicates, ~epred2_0). % 5.57/5.77 fof(interp, fi_predicates, epred3_0). % 5.57/5.77 fof(interp, fi_predicates, epred4_0). % 5.57/5.77 fof(interp, fi_predicates, epred5_0). % 5.57/5.77 fof(interp, fi_predicates, epred6_0). % 5.57/5.77 fof(interp, fi_predicates, epred7_0). % 5.57/5.77 fof(interp, fi_predicates, epred8_0). % 5.57/5.77 fof(interp, fi_predicates, epred9_0). % 5.57/5.77 fof(interp, fi_predicates, ndr1_0). % 5.57/5.77 fof(interp, fi_predicates, ndr1_1(0) & ndr1_1(1)). % 5.57/5.77 % SZS output end FiniteModel for theBenchmark.p % 5.57/5.77 % 1 lemma(s) from E % 5.57/5.77 % cnf(cl, axiom, ndr1_0). % 5.57/5.77 % 1145 pred(s) % 5.57/5.77 % 230 func(s) % 5.57/5.77 % 2 sort(s) % 5.57/5.77 % 2791 clause(s) % 5.57/5.77 % Instantiating 1 (5298 ms) % 5.57/5.77 % Solving (5301 ms) % 5.57/5.77 % Instantiating 2 (5301 ms) % 5.57/5.77 % Solving (5309 ms) % 5.57/5.77 % % 5.57/5.77 % 1 model found (5321 ms) %------------------------------------------------------------------------------