%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SYN518+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n025.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:03:14 EDT 2022 % Result : CounterSatisfiable 5.42s 5.67s % Output : FiniteModel 5.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYN518+1 : TPTP v8.1.0. Released v2.1.0. % 0.03/0.12 % Command : do_Crossbow---0.1 %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jul 12 05:15:48 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.33 /export/starexec/sandbox/solver/bin % 0.12/0.34 crossbow.opt % 0.12/0.34 do_Crossbow---0.1 % 0.12/0.34 eprover % 0.12/0.34 runsolver % 0.12/0.34 starexec_run_Crossbow---0.1 % 5.42/5.67 % SZS status CounterSatisfiable for theBenchmark.p % 5.42/5.67 % SZS output start FiniteModel for theBenchmark.p % 5.42/5.67 % domain size: 3 % 5.42/5.67 fof(interp, fi_domain, ![X] : (X = 0 | X = 1 | X = 2)). % 5.42/5.67 fof(interp, fi_functors, a1000 = 2). % 5.42/5.67 fof(interp, fi_functors, a1001 = 0). % 5.42/5.67 fof(interp, fi_functors, a1002 = 0). % 5.42/5.67 fof(interp, fi_functors, a1003 = 0). % 5.42/5.67 fof(interp, fi_functors, a1004 = 0). % 5.42/5.67 fof(interp, fi_functors, a1005 = 0). % 5.42/5.67 fof(interp, fi_functors, a1006 = 0). % 5.42/5.67 fof(interp, fi_functors, a1007 = 1). % 5.42/5.67 fof(interp, fi_functors, a1008 = 0). % 5.42/5.67 fof(interp, fi_functors, a1009 = 1). % 5.42/5.67 fof(interp, fi_functors, a1010 = 1). % 5.42/5.67 fof(interp, fi_functors, a1011 = 2). % 5.42/5.67 fof(interp, fi_functors, a1012 = 2). % 5.42/5.67 fof(interp, fi_functors, a1013 = 0). % 5.42/5.67 fof(interp, fi_functors, a1014 = 0). % 5.42/5.67 fof(interp, fi_functors, a1015 = 2). % 5.42/5.67 fof(interp, fi_functors, a1016 = 0). % 5.42/5.67 fof(interp, fi_functors, a1017 = 0). % 5.42/5.67 fof(interp, fi_functors, a1018 = 0). % 5.42/5.67 fof(interp, fi_functors, a1019 = 0). % 5.42/5.67 fof(interp, fi_functors, a1020 = 0). % 5.42/5.67 fof(interp, fi_functors, a1021 = 0). % 5.42/5.67 fof(interp, fi_functors, a1022 = 0). % 5.42/5.67 fof(interp, fi_functors, a1023 = 1). % 5.42/5.67 fof(interp, fi_functors, a1024 = 0). % 5.42/5.67 fof(interp, fi_functors, a1025 = 2). % 5.42/5.67 fof(interp, fi_functors, a1026 = 0). % 5.42/5.67 fof(interp, fi_functors, a1027 = 1). % 5.42/5.67 fof(interp, fi_functors, a1028 = 1). % 5.42/5.67 fof(interp, fi_functors, a1029 = 0). % 5.42/5.67 fof(interp, fi_functors, a1030 = 0). % 5.42/5.67 fof(interp, fi_functors, a1031 = 1). % 5.42/5.67 fof(interp, fi_functors, a1032 = 2). % 5.42/5.67 fof(interp, fi_functors, a1033 = 0). % 5.42/5.67 fof(interp, fi_functors, a1034 = 2). % 5.42/5.67 fof(interp, fi_functors, a1035 = 0). % 5.42/5.67 fof(interp, fi_functors, a1036 = 0). % 5.42/5.67 fof(interp, fi_functors, a1037 = 2). % 5.42/5.67 fof(interp, fi_functors, a1038 = 1). % 5.42/5.67 fof(interp, fi_functors, a1039 = 1). % 5.42/5.67 fof(interp, fi_functors, a1040 = 1). % 5.42/5.67 fof(interp, fi_functors, a1041 = 1). % 5.42/5.67 fof(interp, fi_functors, a1042 = 2). % 5.42/5.67 fof(interp, fi_functors, a1043 = 1). % 5.42/5.67 fof(interp, fi_functors, a1044 = 2). % 5.42/5.67 fof(interp, fi_functors, a1045 = 1). % 5.42/5.67 fof(interp, fi_functors, a1046 = 0). % 5.42/5.67 fof(interp, fi_functors, a1047 = 0). % 5.42/5.67 fof(interp, fi_functors, a1048 = 0). % 5.42/5.67 fof(interp, fi_functors, a1049 = 1). % 5.42/5.67 fof(interp, fi_functors, a1050 = 0). % 5.42/5.67 fof(interp, fi_functors, a1051 = 2). % 5.42/5.67 fof(interp, fi_functors, a1052 = 1). % 5.42/5.67 fof(interp, fi_functors, a1053 = 1). % 5.42/5.67 fof(interp, fi_functors, a1054 = 1). % 5.42/5.67 fof(interp, fi_functors, a1055 = 1). % 5.42/5.67 fof(interp, fi_functors, a1056 = 2). % 5.42/5.67 fof(interp, fi_functors, a1057 = 0). % 5.42/5.67 fof(interp, fi_functors, a1058 = 1). % 5.42/5.67 fof(interp, fi_functors, a1059 = 0). % 5.42/5.67 fof(interp, fi_functors, a1060 = 0). % 5.42/5.67 fof(interp, fi_functors, a1061 = 0). % 5.42/5.67 fof(interp, fi_functors, a1062 = 2). % 5.42/5.67 fof(interp, fi_functors, a1063 = 2). % 5.42/5.67 fof(interp, fi_functors, a1064 = 0). % 5.42/5.67 fof(interp, fi_functors, a1065 = 1). % 5.42/5.67 fof(interp, fi_functors, a1066 = 1). % 5.42/5.67 fof(interp, fi_functors, a1067 = 2). % 5.42/5.67 fof(interp, fi_functors, a1068 = 0). % 5.42/5.67 fof(interp, fi_functors, a1069 = 0). % 5.42/5.67 fof(interp, fi_functors, a1070 = 0). % 5.42/5.67 fof(interp, fi_functors, a1071 = 0). % 5.42/5.67 fof(interp, fi_functors, a1072 = 1). % 5.42/5.67 fof(interp, fi_functors, a1073 = 2). % 5.42/5.67 fof(interp, fi_functors, a1074 = 1). % 5.42/5.67 fof(interp, fi_functors, a1075 = 2). % 5.42/5.67 fof(interp, fi_functors, a1076 = 2). % 5.42/5.67 fof(interp, fi_functors, a1077 = 1). % 5.42/5.67 fof(interp, fi_functors, a1078 = 0). % 5.42/5.67 fof(interp, fi_functors, a1079 = 0). % 5.42/5.67 fof(interp, fi_functors, a1080 = 1). % 5.42/5.67 fof(interp, fi_functors, a1081 = 0). % 5.42/5.67 fof(interp, fi_functors, a1082 = 1). % 5.42/5.67 fof(interp, fi_functors, a1083 = 2). % 5.42/5.67 fof(interp, fi_functors, a1084 = 0). % 5.42/5.67 fof(interp, fi_functors, a1085 = 2). % 5.42/5.67 fof(interp, fi_functors, a1086 = 1). % 5.42/5.67 fof(interp, fi_functors, a1087 = 0). % 5.42/5.67 fof(interp, fi_functors, a1088 = 0). % 5.42/5.67 fof(interp, fi_functors, a1089 = 1). % 5.42/5.67 fof(interp, fi_functors, a1090 = 0). % 5.42/5.67 fof(interp, fi_functors, a1091 = 0). % 5.42/5.67 fof(interp, fi_functors, a1092 = 0). % 5.42/5.67 fof(interp, fi_functors, a1093 = 0). % 5.42/5.67 fof(interp, fi_functors, a1094 = 2). % 5.42/5.67 fof(interp, fi_functors, a1095 = 0). % 5.42/5.67 fof(interp, fi_functors, a1096 = 0). % 5.42/5.67 fof(interp, fi_functors, a1097 = 0). % 5.42/5.67 fof(interp, fi_functors, a1098 = 1). % 5.42/5.67 fof(interp, fi_functors, a1099 = 1). % 5.42/5.67 fof(interp, fi_functors, a1100 = 0). % 5.42/5.67 fof(interp, fi_functors, a1101 = 2). % 5.42/5.67 fof(interp, fi_functors, a1102 = 0). % 5.42/5.67 fof(interp, fi_functors, a1103 = 1). % 5.42/5.67 fof(interp, fi_functors, a1104 = 2). % 5.42/5.67 fof(interp, fi_functors, a1105 = 0). % 5.42/5.67 fof(interp, fi_functors, a1106 = 2). % 5.42/5.67 fof(interp, fi_functors, a1107 = 2). % 5.42/5.67 fof(interp, fi_functors, a1108 = 2). % 5.42/5.67 fof(interp, fi_functors, a1109 = 0). % 5.42/5.67 fof(interp, fi_functors, a1110 = 0). % 5.42/5.67 fof(interp, fi_functors, a1111 = 2). % 5.42/5.67 fof(interp, fi_functors, a1112 = 1). % 5.42/5.67 fof(interp, fi_functors, a1113 = 1). % 5.42/5.67 fof(interp, fi_functors, a1114 = 0). % 5.42/5.67 fof(interp, fi_functors, a1115 = 0). % 5.42/5.67 fof(interp, fi_functors, a1116 = 0). % 5.42/5.67 fof(interp, fi_functors, a1117 = 0). % 5.42/5.67 fof(interp, fi_functors, a1118 = 0). % 5.42/5.67 fof(interp, fi_functors, a1119 = 0). % 5.42/5.67 fof(interp, fi_functors, a1120 = 2). % 5.42/5.67 fof(interp, fi_functors, a1121 = 0). % 5.42/5.67 fof(interp, fi_functors, a1122 = 1). % 5.42/5.67 fof(interp, fi_functors, a1123 = 2). % 5.42/5.67 fof(interp, fi_functors, a1124 = 2). % 5.42/5.67 fof(interp, fi_functors, a1125 = 0). % 5.42/5.67 fof(interp, fi_functors, a1126 = 0). % 5.42/5.67 fof(interp, fi_functors, a1127 = 1). % 5.42/5.67 fof(interp, fi_functors, a1128 = 0). % 5.42/5.67 fof(interp, fi_functors, a1129 = 0). % 5.42/5.67 fof(interp, fi_functors, a1130 = 1). % 5.42/5.67 fof(interp, fi_functors, a1131 = 1). % 5.42/5.67 fof(interp, fi_functors, a1132 = 0). % 5.42/5.67 fof(interp, fi_functors, a1133 = 0). % 5.42/5.67 fof(interp, fi_functors, a1134 = 0). % 5.42/5.67 fof(interp, fi_functors, a1135 = 1). % 5.42/5.67 fof(interp, fi_functors, a1136 = 1). % 5.42/5.67 fof(interp, fi_functors, a1137 = 0). % 5.42/5.67 fof(interp, fi_functors, a1138 = 1). % 5.42/5.67 fof(interp, fi_functors, a1139 = 0). % 5.42/5.67 fof(interp, fi_functors, a1140 = 0). % 5.42/5.67 fof(interp, fi_functors, a1141 = 0). % 5.42/5.67 fof(interp, fi_functors, a1142 = 0). % 5.42/5.67 fof(interp, fi_functors, a1143 = 0). % 5.42/5.67 fof(interp, fi_functors, a1144 = 1). % 5.42/5.67 fof(interp, fi_functors, a1145 = 1). % 5.42/5.67 fof(interp, fi_functors, a1146 = 0). % 5.42/5.67 fof(interp, fi_functors, a1147 = 0). % 5.42/5.67 fof(interp, fi_functors, a1148 = 2). % 5.42/5.67 fof(interp, fi_functors, a1149 = 1). % 5.42/5.67 fof(interp, fi_functors, a1150 = 0). % 5.42/5.67 fof(interp, fi_functors, a1151 = 2). % 5.42/5.67 fof(interp, fi_functors, a1152 = 0). % 5.42/5.67 fof(interp, fi_functors, a1153 = 1). % 5.42/5.67 fof(interp, fi_functors, a1154 = 0). % 5.42/5.67 fof(interp, fi_functors, a1155 = 0). % 5.42/5.67 fof(interp, fi_functors, a1156 = 0). % 5.42/5.67 fof(interp, fi_functors, a1157 = 1). % 5.42/5.67 fof(interp, fi_functors, a999 = 0). % 5.42/5.67 fof(interp, fi_predicates, c1_0). % 5.42/5.67 fof(interp, fi_predicates, ~c1_1(0) & c1_1(1) & ~c1_1(2)). % 5.42/5.67 fof(interp, fi_predicates, c1_2(0, 0) & c1_2(0, 1) & c1_2(0, 2) & c1_2(1, 0) & % 5.42/5.67 c1_2(1, 1) & % 5.42/5.67 c1_2(1, 2) & % 5.42/5.67 ~c1_2(2, 0) & % 5.42/5.67 c1_2(2, 1) & % 5.42/5.67 ~c1_2(2, 2)). % 5.42/5.67 fof(interp, fi_predicates, ~c2_0). % 5.42/5.67 fof(interp, fi_predicates, ~c2_1(0) & c2_1(1) & ~c2_1(2)). % 5.42/5.67 fof(interp, fi_predicates, ~c2_2(0, 0) & ~c2_2(0, 1) & c2_2(0, 2) & c2_2(1, 0) & % 5.42/5.67 c2_2(1, 1) & % 5.42/5.67 c2_2(1, 2) & % 5.42/5.67 c2_2(2, 0) & % 5.42/5.67 ~c2_2(2, 1) & % 5.42/5.67 ~c2_2(2, 2)). % 5.42/5.67 fof(interp, fi_predicates, ~c3_0). % 5.42/5.67 fof(interp, fi_predicates, c3_1(0) & ~c3_1(1) & ~c3_1(2)). % 5.42/5.67 fof(interp, fi_predicates, ~c3_2(0, 0) & c3_2(0, 1) & c3_2(0, 2) & ~c3_2(1, 0) & % 5.42/5.67 ~c3_2(1, 1) & % 5.42/5.67 ~c3_2(1, 2) & % 5.42/5.67 c3_2(2, 0) & % 5.42/5.67 ~c3_2(2, 1) & % 5.42/5.67 ~c3_2(2, 2)). % 5.42/5.67 fof(interp, fi_predicates, ~c4_0). % 5.42/5.67 fof(interp, fi_predicates, ~c4_1(0) & c4_1(1) & ~c4_1(2)). % 5.42/5.67 fof(interp, fi_predicates, c4_2(0, 0) & ~c4_2(0, 1) & c4_2(0, 2) & c4_2(1, 0) & % 5.42/5.67 ~c4_2(1, 1) & % 5.42/5.67 c4_2(1, 2) & % 5.42/5.67 ~c4_2(2, 0) & % 5.42/5.67 ~c4_2(2, 1) & % 5.42/5.67 ~c4_2(2, 2)). % 5.42/5.67 fof(interp, fi_predicates, ~c5_0). % 5.42/5.67 fof(interp, fi_predicates, ~c5_1(0) & c5_1(1) & c5_1(2)). % 5.42/5.67 fof(interp, fi_predicates, ~c5_2(0, 0) & c5_2(0, 1) & c5_2(0, 2) & c5_2(1, 0) & % 5.42/5.67 ~c5_2(1, 1) & % 5.42/5.67 c5_2(1, 2) & % 5.42/5.67 ~c5_2(2, 0) & % 5.42/5.67 c5_2(2, 1) & % 5.42/5.67 ~c5_2(2, 2)). % 5.42/5.67 fof(interp, fi_predicates, ~epred1_0). % 5.42/5.67 fof(interp, fi_predicates, epred2_0). % 5.42/5.67 fof(interp, fi_predicates, epred3_0). % 5.42/5.67 fof(interp, fi_predicates, ~epred4_0). % 5.42/5.67 fof(interp, fi_predicates, ~epred5_0). % 5.42/5.67 fof(interp, fi_predicates, epred6_0). % 5.42/5.67 fof(interp, fi_predicates, epred7_0). % 5.42/5.67 fof(interp, fi_predicates, ndr1_0). % 5.42/5.67 fof(interp, fi_predicates, ndr1_1(0) & ndr1_1(1) & ndr1_1(2)). % 5.42/5.67 % SZS output end FiniteModel for theBenchmark.p % 5.42/5.67 % 20 lemma(s) from E % 5.42/5.67 % cnf(cl, axiom, ndr1_0). % 5.42/5.67 % cnf(cl, axiom, c1_0). % 5.42/5.67 % cnf(cl, axiom, epred7_0). % 5.42/5.67 % cnf(cl, axiom, epred6_0). % 5.42/5.67 % cnf(cl, axiom, epred3_0). % 5.42/5.67 % cnf(cl, axiom, ~c5_0). % 5.42/5.67 % cnf(cl, axiom, ~c4_0). % 5.42/5.67 % cnf(cl, axiom, ~c2_0). % 5.42/5.67 % cnf(cl, axiom, ~c3_0). % 5.42/5.67 % cnf(cl, axiom, ndr1_1(a1097)). % 5.42/5.67 % cnf(cl, axiom, c5_1(a1049)). % 5.42/5.67 % cnf(cl, axiom, c5_1(a1103)). % 5.42/5.67 % cnf(cl, axiom, ndr1_1(a1141)). % 5.42/5.67 % cnf(cl, axiom, c1_1(a1113)). % 5.42/5.67 % cnf(cl, axiom, c3_1(a1121)). % 5.42/5.67 % cnf(cl, axiom, c2_1(a1113)). % 5.42/5.67 % cnf(cl, axiom, ndr1_1(a1000)). % 5.42/5.67 % cnf(cl, axiom, ndr1_1(a1104)). % 5.42/5.67 % cnf(cl, axiom, ndr1_1(a1067)). % 5.42/5.67 % cnf(cl, axiom, ndr1_1(a1051)). % 5.42/5.67 % 734 pred(s) % 5.42/5.67 % 159 func(s) % 5.42/5.67 % 2 sort(s) % 5.42/5.67 % 1775 clause(s) % 5.42/5.67 % Instantiating 1 (5224 ms) % 5.42/5.67 % Solving (5226 ms) % 5.42/5.67 % Instantiating 2 (5227 ms) % 5.42/5.67 % Solving (5231 ms) % 5.42/5.67 % Instantiating 3 (5231 ms) % 5.42/5.67 % Solving (5241 ms) % 5.42/5.67 % % 5.42/5.67 % 1 model found (5253 ms) %------------------------------------------------------------------------------