PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-air04.opb
MD5SUM	26490113618ae9605b5ebe6370b5910b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	8904
Biggest coefficient in the objective function	2258
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	5135151
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	2258
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	5135151
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.120981
Number of variables	8904
Total number of constraints	9727
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9727
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	368
Trace number 18358

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 14:30:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18174 boxname=wulflinc15 idbench=1398 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  26490113618ae9605b5ebe6370b5910b  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-air04.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-air04.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-air04.opb
IDLAUNCH: 18174
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        785144 kB
Buffers:         29808 kB
Cached:         197620 kB
SwapCached:        440 kB
Active:          22676 kB
Inactive:       206920 kB
HighTotal:      131008 kB
HighFree:        43260 kB
LowTotal:       903652 kB
LowFree:        741884 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14260 kB
Committed_AS:    63468 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:50:25 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 18174 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   63
c ---[1640]---> BDD-cost:   23
c ---[1638]---> BDD-cost:   29
c ---[1636]---> BDD-cost:    0
c ---[1634]---> BDD-cost:   71
c ---[1632]---> BDD-cost:   55
c ---[1628]---> BDD-cost:   23
c ---[1626]---> BDD-cost:   47
c ---[1624]---> BDD-cost:  213
c ---[1622]---> BDD-cost:   75
c ---[1620]---> BDD-cost:   75
c ---[1618]---> BDD-cost:   55
c ---[1616]---> BDD-cost:   15
c ---[1614]---> BDD-cost:   87
c ---[1612]---> BDD-cost:   51
c ---[1610]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1606]---> BDD-cost:   23
c ---[1604]---> BDD-cost:   11
c ---[1602]---> BDD-cost:   39
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:  259
c ---[1594]---> BDD-cost:  189
c ---[1592]---> BDD-cost:  101
c ---[1588]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  101
c ---[1582]---> BDD-cost:   37
c ---[1580]---> BDD-cost:  181
c ---[1578]---> BDD-cost:  283
c ---[1576]---> BDD-cost:   99
c ---[1574]---> BDD-cost:    1
c ---[1572]---> BDD-cost:  109
c ---[1570]---> BDD-cost:   75
c ---[1568]---> BDD-cost:  237
c ---[1566]---> BDD-cost:  119
c ---[1564]---> BDD-cost:  109
c ---[1562]---> BDD-cost:   83
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:  157
c ---[1556]---> BDD-cost:  155
c ---[1554]---> BDD-cost:  109
c ---[1550]---> BDD-cost:   77
c ---[1548]---> BDD-cost:  133
c ---[1546]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  115
c ---[1542]---> BDD-cost:  185
c ---[1540]---> BDD-cost:  203
c ---[1538]---> BDD-cost:  167
c ---[1536]---> BDD-cost:  135
c ---[1534]---> BDD-cost:    9
c ---[1532]---> BDD-cost:   85
c ---[1530]---> BDD-cost:  143
c ---[1528]---> BDD-cost:  135
c ---[1526]---> BDD-cost:   63
c ---[1524]---> BDD-cost:   51
c ---[1522]---> BDD-cost:  159
c ---[1520]---> BDD-cost:  155
c ---[1518]---> BDD-cost:  211
c ---[1516]---> BDD-cost:   75
c ---[1514]---> BDD-cost:   37
c ---[1512]---> BDD-cost:   87
c ---[1510]---> BDD-cost:   79
c ---[1508]---> BDD-cost:  109
c ---[1506]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  247
c ---[1502]---> BDD-cost:  105
c ---[1500]---> BDD-cost:   59
c ---[1498]---> BDD-cost:   71
c ---[1496]---> BDD-cost:   61
c ---[1494]---> BDD-cost:   89
c ---[1492]---> BDD-cost:   91
c ---[1490]---> BDD-cost:  143
c ---[1488]---> BDD-cost:  111
c ---[1486]---> BDD-cost:   95
c ---[1484]---> BDD-cost:  169
c ---[1482]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  151
c ---[1478]---> BDD-cost:   67
c ---[1476]---> BDD-cost:   45
c ---[1474]---> BDD-cost:   45
c ---[1472]---> BDD-cost:   45
c ---[1470]---> BDD-cost:   65
c ---[1468]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   47
c ---[1460]---> BDD-cost:   29
c ---[1458]---> BDD-cost:   27
c ---[1456]---> BDD-cost:   11
c ---[1452]---> BDD-cost:   81
c ---[1450]---> BDD-cost:  233
c ---[1448]---> BDD-cost:  275
c ---[1446]---> BDD-cost:  289
c ---[1444]---> BDD-cost:  119
c ---[1442]---> BDD-cost:  145
c ---[1440]---> BDD-cost:  165
c ---[1438]---> BDD-cost:  239
c ---[1436]---> BDD-cost:  223
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   35
c ---[1430]---> BDD-cost:   93
c ---[1428]---> BDD-cost:   45
c ---[1426]---> BDD-cost:   73
c ---[1424]---> BDD-cost:   75
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   99
c ---[1416]---> BDD-cost:  187
c ---[1414]---> BDD-cost:   55
c ---[1412]---> BDD-cost:  107
c ---[1410]---> BDD-cost:   69
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:    3
c ---[1404]---> BDD-cost:  149
c ---[1402]---> BDD-cost:  137
c ---[1400]---> BDD-cost:  195
c ---[1398]---> BDD-cost:   93
c ---[1396]---> BDD-cost:  157
c ---[1394]---> BDD-cost:  233
c ---[1392]---> BDD-cost:  223
c ---[1390]---> BDD-cost:  225
c ---[1388]---> BDD-cost:  247
c ---[1386]---> BDD-cost:  179
c ---[1384]---> BDD-cost:  225
c ---[1382]---> BDD-cost:  243
c ---[1380]---> BDD-cost:  199
c ---[1378]---> BDD-cost:   55
c ---[1376]---> BDD-cost:   57
c ---[1374]---> BDD-cost:   99
c ---[1372]---> BDD-cost:    9
c ---[1370]---> BDD-cost:    3
c ---[1368]---> BDD-cost:   23
c ---[1366]---> BDD-cost:   51
c ---[1364]---> BDD-cost:   25
c ---[1362]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   27
c ---[1358]---> BDD-cost:   15
c ---[1356]---> BDD-cost:   37
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   67
c ---[1350]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  211
c ---[1342]---> BDD-cost:   65
c ---[1340]---> BDD-cost:  117
c ---[1338]---> BDD-cost:   65
c ---[1336]---> BDD-cost:   65
c ---[1334]---> BDD-cost:   49
c ---[1332]---> BDD-cost:  439
c ---[1330]---> BDD-cost:  423
c ---[1328]---> BDD-cost:  287
c ---[1326]---> BDD-cost:  217
c ---[1324]---> BDD-cost:  195
c ---[1322]---> BDD-cost:   63
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:  359
c ---[1316]---> BDD-cost:  353
c ---[1312]---> BDD-cost:  169
c ---[1310]---> BDD-cost:  139
c ---[1308]---> BDD-cost:  159
c ---[1306]---> BDD-cost:  223
c ---[1304]---> BDD-cost:  107
c ---[1302]---> BDD-cost:   75
c ---[1300]---> BDD-cost:  109
c ---[1298]---> BDD-cost:   93
c ---[1296]---> BDD-cost:   87
c ---[1294]---> BDD-cost:   87
c ---[1292]---> BDD-cost:    7
c ---[1288]---> BDD-cost:   73
c ---[1286]---> BDD-cost:   71
c ---[1284]---> BDD-cost:  107
c ---[1282]---> BDD-cost:   77
c ---[1280]---> BDD-cost:    3
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  131
c ---[1274]---> BDD-cost:  135
c ---[1272]---> BDD-cost:   65
c ---[1270]---> BDD-cost:  165
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:    1
c ---[1264]---> BDD-cost:   87
c ---[1262]---> BDD-cost:  155
c ---[1260]---> BDD-cost:  167
c ---[1258]---> BDD-cost:  203
c ---[1256]---> BDD-cost:  231
c ---[1254]---> BDD-cost:  147
c ---[1252]---> BDD-cost:  135
c ---[1250]---> BDD-cost:   49
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   95
c ---[1244]---> BDD-cost:  325
c ---[1242]---> BDD-cost:  333
c ---[1240]---> BDD-cost:  173
c ---[1238]---> BDD-cost:  269
c ---[1236]---> BDD-cost:   31
c ---[1234]---> BDD-cost:  413
c ---[1232]---> BDD-cost:  313
c ---[1230]---> BDD-cost:  125
c ---[1228]---> BDD-cost:  113
c ---[1226]---> BDD-cost:  247
c ---[1224]---> BDD-cost:   57
c ---[1222]---> BDD-cost:  237
c ---[1220]---> BDD-cost:  159
c ---[1218]---> BDD-cost:  117
c ---[1216]---> BDD-cost:   43
c ---[1214]---> BDD-cost:  143
c ---[1212]---> BDD-cost:   65
c ---[1210]---> BDD-cost:  123
c ---[1208]---> BDD-cost:   61
c ---[1206]---> BDD-cost:  103
c ---[1204]---> BDD-cost:   85
c ---[1202]---> BDD-cost:   77
c ---[1200]---> BDD-cost:   57
c ---[1198]---> BDD-cost:  127
c ---[1196]---> BDD-cost:  157
c ---[1194]---> BDD-cost:  267
c ---[1192]---> BDD-cost:  223
c ---[1190]---> BDD-cost:  229
c ---[1188]---> BDD-cost:  257
c ---[1186]---> BDD-cost:  241
c ---[1184]---> BDD-cost:  195
c ---[1182]---> BDD-cost:   49
c ---[1180]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  197
c ---[1176]---> BDD-cost:  171
c ---[1174]---> BDD-cost:  287
c ---[1172]---> BDD-cost:   75
c ---[1170]---> BDD-cost:  215
c ---[1168]---> BDD-cost:  119
c ---[1166]---> BDD-cost:  245
c ---[1164]---> BDD-cost:  257
c ---[1162]---> BDD-cost:  279
c ---[1160]---> BDD-cost:  227
c ---[1158]---> BDD-cost:  201
c ---[1156]---> BDD-cost:  143
c ---[1154]---> BDD-cost:  207
c ---[1152]---> BDD-cost:  131
c ---[1150]---> BDD-cost:  245
c ---[1148]---> BDD-cost:  115
c ---[1146]---> BDD-cost:   91
c ---[1144]---> BDD-cost:   43
c ---[1142]---> BDD-cost:   39
c ---[1140]---> BDD-cost:   91
c ---[1138]---> BDD-cost:  179
c ---[1136]---> BDD-cost:   73
c ---[1134]---> BDD-cost:   29
c ---[1132]---> BDD-cost:  163
c ---[1130]---> BDD-cost:   81
c ---[1128]---> BDD-cost:   63
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  113
c ---[1122]---> BDD-cost:  115
c ---[1120]---> BDD-cost:   19
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   99
c ---[1114]---> BDD-cost:   99
c ---[1112]---> BDD-cost:  103
c ---[1110]---> BDD-cost:   67
c ---[1108]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   85
c ---[1104]---> BDD-cost:   87
c ---[1102]---> BDD-cost:    7
c ---[1100]---> BDD-cost:   45
c ---[1098]---> BDD-cost:   43
c ---[1096]---> BDD-cost:   11
c ---[1094]---> BDD-cost:   59
c ---[1092]---> BDD-cost:  185
c ---[1090]---> BDD-cost:  249
c ---[1088]---> BDD-cost:  315
c ---[1086]---> BDD-cost:  253
c ---[1084]---> BDD-cost:  161
c ---[1082]---> BDD-cost:  257
c ---[1080]---> BDD-cost:  167
c ---[1078]---> BDD-cost:  167
c ---[1076]---> BDD-cost:  141
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   95
c ---[1068]---> BDD-cost:  141
c ---[1066]---> BDD-cost:  123
c ---[1064]---> BDD-cost:   83
c ---[1062]---> BDD-cost:   55
c ---[1060]---> BDD-cost:  183
c ---[1058]---> BDD-cost:  269
c ---[1056]---> BDD-cost:   63
c ---[1054]---> BDD-cost:   45
c ---[1052]---> BDD-cost:   39
c ---[1050]---> BDD-cost:   97
c ---[1048]---> BDD-cost:   51
c ---[1046]---> BDD-cost:   45
c ---[1044]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   85
c ---[1040]---> BDD-cost:   35
c ---[1038]---> BDD-cost:   53
c ---[1036]---> BDD-cost:   21
c ---[1034]---> BDD-cost:  115
c ---[1032]---> BDD-cost:   99
c ---[1030]---> BDD-cost:   63
c ---[1028]---> BDD-cost:   77
c ---[1026]---> BDD-cost:  139
c ---[1024]---> BDD-cost:  109
c ---[1022]---> BDD-cost:  407
c ---[1020]---> BDD-cost:  323
c ---[1018]---> BDD-cost:  109
c ---[1016]---> BDD-cost:   93
c ---[1014]---> BDD-cost:   51
c ---[1012]---> BDD-cost:   79
c ---[1010]---> BDD-cost:   75
c ---[1008]---> BDD-cost:  147
c ---[1006]---> BDD-cost:  169
c ---[1004]---> BDD-cost:  209
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   51
c ---[ 998]---> BDD-cost:   85
c ---[ 994]---> BDD-cost:  103
c ---[ 992]---> BDD-cost:  127
c ---[ 990]---> BDD-cost:   77
c ---[ 988]---> BDD-cost:   77
c ---[ 986]---> BDD-cost:  141
c ---[ 984]---> BDD-cost:   89
c ---[ 982]---> BDD-cost:   85
c ---[ 980]---> BDD-cost:  119
c ---[ 978]---> BDD-cost:   69
c ---[ 976]---> BDD-cost:   57
c ---[ 974]---> BDD-cost:   65
c ---[ 972]---> BDD-cost:   47
c ---[ 970]---> BDD-cost:   61
c ---[ 968]---> BDD-cost:   31
c ---[ 964]---> BDD-cost:  183
c ---[ 962]---> BDD-cost:  121
c ---[ 960]---> BDD-cost:   89
c ---[ 958]---> BDD-cost:  225
c ---[ 956]---> BDD-cost:  267
c ---[ 952]---> BDD-cost:  159
c ---[ 950]---> BDD-cost:  209
c ---[ 948]---> BDD-cost:   71
c ---[ 946]---> BDD-cost:  237
c ---[ 944]---> BDD-cost:  129
c ---[ 942]---> BDD-cost:  365
c ---[ 940]---> BDD-cost:  369
c ---[ 938]---> BDD-cost:  129
c ---[ 936]---> BDD-cost:  101
c ---[ 934]---> BDD-cost:  289
c ---[ 932]---> BDD-cost:  279
c ---[ 930]---> BDD-cost:  345
c ---[ 928]---> BDD-cost:   81
c ---[ 926]---> BDD-cost:   69
c ---[ 924]---> BDD-cost:   83
c ---[ 922]---> BDD-cost:   53
c ---[ 920]---> BDD-cost:   67
c ---[ 918]---> BDD-cost:   55
c ---[ 916]---> BDD-cost:  145
c ---[ 914]---> BDD-cost:  149
c ---[ 912]---> BDD-cost:  105
c ---[ 910]---> BDD-cost:   19
c ---[ 908]---> BDD-cost:  105
c ---[ 906]---> BDD-cost:  101
c ---[ 904]---> BDD-cost:  147
c ---[ 902]---> BDD-cost:  231
c ---[ 900]---> BDD-cost:  191
c ---[ 898]---> BDD-cost:  157
c ---[ 896]---> BDD-cost:  249
c ---[ 894]---> BDD-cost:  385
c ---[ 892]---> BDD-cost:   67
c ---[ 890]---> BDD-cost:   71
c ---[ 888]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:  147
c ---[ 884]---> BDD-cost:  139
c ---[ 882]---> BDD-cost:  273
c ---[ 880]---> BDD-cost:  213
c ---[ 878]---> BDD-cost:  169
c ---[ 876]---> BDD-cost:  239
c ---[ 874]---> BDD-cost:  305
c ---[ 872]---> BDD-cost:  109
c ---[ 870]---> BDD-cost:  105
c ---[ 868]---> BDD-cost:  147
c ---[ 866]---> BDD-cost:  115
c ---[ 864]---> BDD-cost:  115
c ---[ 862]---> BDD-cost:   67
c ---[ 860]---> BDD-cost:  329
c ---[ 858]---> BDD-cost:  295
c ---[ 856]---> BDD-cost:   51
c ---[ 854]---> BDD-cost:   61
c ---[ 852]---> BDD-cost:  317
c ---[ 850]---> BDD-cost:   97
c ---[ 848]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:   43
c ---[ 844]---> BDD-cost:   85
c ---[ 842]---> BDD-cost:   35
c ---[ 840]---> BDD-cost:   69
c ---[ 836]---> BDD-cost:   45
c ---[ 834]---> BDD-cost:   73
c ---[ 832]---> BDD-cost:   55
c ---[ 828]---> BDD-cost:   33
c ---[ 826]---> BDD-cost:   29
c ---[ 824]---> BDD-cost:  245
c ---[ 822]---> BDD-cost:  225
c ---[ 820]---> BDD-cost:  111
c ---[ 818]---> BDD-cost:  117
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  129
c ---[ 812]---> BDD-cost:  259
c ---[ 810]---> BDD-cost:  221
c ---[ 808]---> BDD-cost:  275
c ---[ 806]---> BDD-cost:  209
c ---[ 804]---> BDD-cost:  267
c ---[ 802]---> BDD-cost:  171
c ---[ 800]---> BDD-cost:   57
c ---[ 796]---> BDD-cost:  133
c ---[ 794]---> BDD-cost:  185
c ---[ 792]---> BDD-cost:  169
c ---[ 790]---> BDD-cost:  287
c ---[ 788]---> BDD-cost:   81
c ---[ 786]---> BDD-cost:  335
c ---[ 784]---> BDD-cost:  365
c ---[ 782]---> BDD-cost:  255
c ---[ 780]---> BDD-cost:  111
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  101
c ---[ 774]---> BDD-cost:  197
c ---[ 772]---> BDD-cost:  383
c ---[ 770]---> BDD-cost:  329
c ---[ 768]---> BDD-cost:  241
c ---[ 766]---> BDD-cost:  129
c ---[ 764]---> BDD-cost:   85
c ---[ 762]---> BDD-cost:   71
c ---[ 760]---> BDD-cost:   37
c ---[ 758]---> BDD-cost:   77
c ---[ 756]---> BDD-cost:   49
c ---[ 754]---> BDD-cost:  133
c ---[ 752]---> BDD-cost:  133
c ---[ 750]---> BDD-cost:  377
c ---[ 748]---> BDD-cost:  117
c ---[ 744]---> BDD-cost:  119
c ---[ 742]---> BDD-cost:  119
c ---[ 740]---> BDD-cost:  151
c ---[ 738]---> BDD-cost:  221
c ---[ 736]---> BDD-cost:  181
c ---[ 732]---> BDD-cost:   87
c ---[ 730]---> BDD-cost:  127
c ---[ 728]---> BDD-cost:  299
c ---[ 726]---> BDD-cost:  331
c ---[ 722]---> BDD-cost:   21
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  217
c ---[ 716]---> BDD-cost:  349
c ---[ 714]---> BDD-cost:  291
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  161
c ---[ 708]---> BDD-cost:   61
c ---[ 706]---> BDD-cost:   55
c ---[ 704]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:  189
c ---[ 698]---> BDD-cost:  157
c ---[ 696]---> BDD-cost:  149
c ---[ 694]---> BDD-cost:  139
c ---[ 692]---> BDD-cost:  165
c ---[ 690]---> BDD-cost:  181
c ---[ 688]---> BDD-cost:  253
c ---[ 686]---> BDD-cost:   43
c ---[ 684]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  141
c ---[ 680]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:   95
c ---[ 676]---> BDD-cost:   75
c ---[ 674]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  149
c ---[ 670]---> BDD-cost:  137
c ---[ 668]---> BDD-cost:   59
c ---[ 666]---> BDD-cost:    5
c ---[ 664]---> BDD-cost:   35
c ---[ 662]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   47
c ---[ 654]---> BDD-cost:   55
c ---[ 652]---> BDD-cost:  197
c ---[ 650]---> BDD-cost:  191
c ---[ 648]---> BDD-cost:  125
c ---[ 646]---> BDD-cost:  173
c ---[ 642]---> BDD-cost:   93
c ---[ 640]---> BDD-cost:   29
c ---[ 638]---> BDD-cost:  321
c ---[ 636]---> BDD-cost:  195
c ---[ 634]---> BDD-cost:  163
c ---[ 628]---> BDD-cost:  151
c ---[ 626]---> BDD-cost:  253
c ---[ 624]---> BDD-cost:  381
c ---[ 622]---> BDD-cost:  345
c ---[ 620]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:   83
c ---[ 614]---> BDD-cost:   69
c ---[ 612]---> BDD-cost:   51
c ---[ 610]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   59
c ---[ 606]---> BDD-cost:   83
c ---[ 604]---> BDD-cost:  107
c ---[ 602]---> BDD-cost:  363
c ---[ 600]---> BDD-cost:  103
c ---[ 598]---> BDD-cost:  277
c ---[ 596]---> BDD-cost:  341
c ---[ 594]---> BDD-cost:  213
c ---[ 592]---> BDD-cost:  315
c ---[ 590]---> BDD-cost:  275
c ---[ 588]---> BDD-cost:  151
c ---[ 586]---> BDD-cost:  111
c ---[ 584]---> BDD-cost:  103
c ---[ 582]---> BDD-cost:   75
c ---[ 580]---> BDD-cost:   27
c ---[ 578]---> BDD-cost:   21
c ---[ 576]---> BDD-cost:   11
c ---[ 574]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:  149
c ---[ 564]---> BDD-cost:   97
c ---[ 562]---> BDD-cost:  149
c ---[ 560]---> BDD-cost:  395
c ---[ 558]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:  389
c ---[ 554]---> BDD-cost:  251
c ---[ 552]---> BDD-cost:  375
c ---[ 550]---> BDD-cost:  343
c ---[ 548]---> BDD-cost:  267
c ---[ 546]---> BDD-cost:  135
c ---[ 544]---> BDD-cost:  263
c ---[ 542]---> BDD-cost:  259
c ---[ 540]---> BDD-cost:  245
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:   41
c ---[ 534]---> BDD-cost:  127
c ---[ 532]---> BDD-cost:  117
c ---[ 530]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:  149
c ---[ 526]---> BDD-cost:  103
c ---[ 524]---> BDD-cost:  215
c ---[ 522]---> BDD-cost:   89
c ---[ 520]---> BDD-cost:  177
c ---[ 518]---> BDD-cost:  343
c ---[ 516]---> BDD-cost:  237
c ---[ 514]---> BDD-cost:  177
c ---[ 512]---> BDD-cost:   85
c ---[ 510]---> BDD-cost:  267
c ---[ 508]---> BDD-cost:  225
c ---[ 506]---> BDD-cost:  109
c ---[ 504]---> BDD-cost:  105
c ---[ 502]---> BDD-cost:  113
c ---[ 500]---> BDD-cost:   55
c ---[ 498]---> BDD-cost:  117
c ---[ 496]---> BDD-cost:   83
c ---[ 494]---> BDD-cost:   79
c ---[ 492]---> BDD-cost:   81
c ---[ 490]---> BDD-cost:  263
c ---[ 488]---> BDD-cost:  179
c ---[ 486]---> BDD-cost:  281
c ---[ 484]---> BDD-cost:  389
c ---[ 482]---> BDD-cost:  333
c ---[ 480]---> BDD-cost:  357
c ---[ 478]---> BDD-cost:  345
c ---[ 476]---> BDD-cost:  263
c ---[ 474]---> BDD-cost:   89
c ---[ 472]---> BDD-cost:  285
c ---[ 468]---> BDD-cost:  419
c ---[ 466]---> BDD-cost:  357
c ---[ 464]---> BDD-cost:  473
c ---[ 462]---> BDD-cost:  455
c ---[ 460]---> BDD-cost:  405
c ---[ 458]---> BDD-cost:  241
c ---[ 456]---> BDD-cost:  211
c ---[ 454]---> BDD-cost:  313
c ---[ 452]---> BDD-cost:  371
c ---[ 450]---> BDD-cost:  389
c ---[ 448]---> BDD-cost:  223
c ---[ 446]---> BDD-cost:  221
c ---[ 444]---> BDD-cost:  147
c ---[ 442]---> BDD-cost:  131
c ---[ 440]---> BDD-cost:  185
c ---[ 438]---> BDD-cost:  141
c ---[ 436]---> BDD-cost:  249
c ---[ 434]---> BDD-cost:  261
c ---[ 432]---> BDD-cost:  311
c ---[ 430]---> BDD-cost:  261
c ---[ 428]---> BDD-cost:  387
c ---[ 426]---> BDD-cost:  247
c ---[ 424]---> BDD-cost:  295
c ---[ 422]---> BDD-cost:   31
c ---[ 420]---> BDD-cost:  355
c ---[ 418]---> BDD-cost:  135
c ---[ 416]---> BDD-cost:  443
c ---[ 414]---> BDD-cost:  653
c ---[ 412]---> BDD-cost:  703
c ---[ 410]---> BDD-cost:  517
c ---[ 408]---> BDD-cost:  441
c ---[ 406]---> BDD-cost:  411
c ---[ 404]---> BDD-cost:  289
c ---[ 402]---> BDD-cost:  277
c ---[ 400]---> BDD-cost:  239
c ---[ 398]---> BDD-cost:  201
c ---[ 396]---> BDD-cost:  309
c ---[ 394]---> BDD-cost:  287
c ---[ 392]---> BDD-cost:  177
c ---[ 390]---> BDD-cost:  143
c ---[ 388]---> BDD-cost:  131
c ---[ 386]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:  189
c ---[ 382]---> BDD-cost:  219
c ---[ 378]---> BDD-cost:  267
c ---[ 376]---> BDD-cost:  135
c ---[ 374]---> BDD-cost:   69
c ---[ 372]---> BDD-cost:   75
c ---[ 370]---> BDD-cost:   51
c ---[ 368]---> BDD-cost:  117
c ---[ 366]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:  189
c ---[ 358]---> BDD-cost:   73
c ---[ 356]---> BDD-cost:   55
c ---[ 354]---> BDD-cost:   57
c ---[ 352]---> BDD-cost:   91
c ---[ 350]---> BDD-cost:  325
c ---[ 348]---> BDD-cost:  223
c ---[ 346]---> BDD-cost:   57
c ---[ 344]---> BDD-cost:   43
c ---[ 342]---> BDD-cost:  255
c ---[ 340]---> BDD-cost:  285
c ---[ 338]---> BDD-cost:  187
c ---[ 336]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   91
c ---[ 332]---> BDD-cost:  211
c ---[ 330]---> BDD-cost:  159
c ---[ 328]---> BDD-cost:   97
c ---[ 326]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:  101
c ---[ 322]---> BDD-cost:  141
c ---[ 318]---> BDD-cost:  109
c ---[ 316]---> BDD-cost:  321
c ---[ 314]---> BDD-cost:  305
c ---[ 312]---> BDD-cost:  603
c ---[ 310]---> BDD-cost:  441
c ---[ 308]---> BDD-cost:  391
c ---[ 306]---> BDD-cost:  387
c ---[ 304]---> BDD-cost:  289
c ---[ 302]---> BDD-cost:  219
c ---[ 300]---> BDD-cost:  309
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  197
c ---[ 294]---> BDD-cost:  279
c ---[ 292]---> BDD-cost:  167
c ---[ 290]---> BDD-cost:  151
c ---[ 288]---> BDD-cost:   49
c ---[ 286]---> BDD-cost:   31
c ---[ 284]---> BDD-cost:  107
c ---[ 282]---> BDD-cost:   55
c ---[ 278]---> BDD-cost:  177
c ---[ 276]---> BDD-cost:  223
c ---[ 274]---> BDD-cost:  119
c ---[ 272]---> BDD-cost:  137
c ---[ 270]---> BDD-cost:  105
c ---[ 268]---> BDD-cost:  183
c ---[ 266]---> BDD-cost:  179
c ---[ 264]---> BDD-cost:  285
c ---[ 262]---> BDD-cost:  191
c ---[ 260]---> BDD-cost:  177
c ---[ 258]---> BDD-cost:  145
c ---[ 254]---> BDD-cost:  153
c ---[ 252]---> BDD-cost:  121
c ---[ 250]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:  111
c ---[ 244]---> BDD-cost:  281
c ---[ 242]---> BDD-cost:  265
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  151
c ---[ 236]---> BDD-cost:  167
c ---[ 234]---> BDD-cost:  137
c ---[ 230]---> BDD-cost:  375
c ---[ 228]---> BDD-cost:  287
c ---[ 226]---> BDD-cost:  249
c ---[ 224]---> BDD-cost:  131
c ---[ 222]---> BDD-cost:  187
c ---[ 220]---> BDD-cost:  135
c ---[ 218]---> BDD-cost:  129
c ---[ 216]---> BDD-cost:  317
c ---[ 214]---> BDD-cost:  365
c ---[ 212]---> BDD-cost:  235
c ---[ 210]---> BDD-cost:  249
c ---[ 208]---> BDD-cost:  283
c ---[ 206]---> BDD-cost:  233
c ---[ 204]---> BDD-cost:  259
c ---[ 202]---> BDD-cost:  287
c ---[ 200]---> BDD-cost:  175
c ---[ 198]---> BDD-cost:  233
c ---[ 196]---> BDD-cost:  167
c ---[ 194]---> BDD-cost:  159
c ---[ 192]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:  135
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:  167
c ---[ 182]---> BDD-cost:  203
c ---[ 180]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  263
c ---[ 176]---> BDD-cost:   31
c ---[ 174]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   31
c ---[ 170]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:  225
c ---[ 166]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  385
c ---[ 162]---> BDD-cost:  361
c ---[ 160]---> BDD-cost:   73
c ---[ 158]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:  131
c ---[ 152]---> BDD-cost:  145
c ---[ 150]---> BDD-cost:  121
c ---[ 148]---> BDD-cost:  117
c ---[ 146]---> BDD-cost:  111
c ---[ 144]---> BDD-cost:  123
c ---[ 142]---> BDD-cost:  125
c ---[ 140]---> BDD-cost:  243
c ---[ 138]---> BDD-cost:  143
c ---[ 136]---> BDD-cost:  149
c ---[ 134]---> BDD-cost:  103
c ---[ 132]---> BDD-cost:  155
c ---[ 130]---> BDD-cost:  247
c ---[ 128]---> BDD-cost:  143
c ---[ 126]---> BDD-cost:   91
c ---[ 124]---> BDD-cost:   81
c ---[ 122]---> BDD-cost:   79
c ---[ 120]---> BDD-cost:  117
c ---[ 118]---> BDD-cost:   89
c ---[ 116]---> BDD-cost:   61
c ---[ 114]---> BDD-cost:  127
c ---[ 112]---> BDD-cost:  135
c ---[ 110]---> BDD-cost:  161
c ---[ 108]---> BDD-cost:  141
c ---[ 106]---> BDD-cost:  437
c ---[ 104]---> BDD-cost:  309
c ---[ 102]---> BDD-cost:  173
c ---[ 100]---> BDD-cost:  441
c ---[  98]---> BDD-cost:  489
c ---[  96]---> BDD-cost:  299
c ---[  94]---> BDD-cost:  455
c ---[  92]---> BDD-cost:  333
c ---[  90]---> BDD-cost:  421
c ---[  88]---> BDD-cost:  375
c ---[  86]---> BDD-cost:  433
c ---[  84]---> BDD-cost:  405
c ---[  82]---> BDD-cost:  333
c ---[  80]---> BDD-cost:  673
c ---[  78]---> BDD-cost:  685
c ---[  76]---> BDD-cost:  385
c ---[  74]---> BDD-cost:  267
c ---[  72]---> BDD-cost:  345
c ---[  70]---> BDD-cost:  365
c ---[  68]---> BDD-cost:  391
c ---[  66]---> BDD-cost:  313
c ---[  64]---> BDD-cost:  275
c ---[  62]---> BDD-cost:  257
c ---[  60]---> BDD-cost:  203
c ---[  58]---> BDD-cost:  311
c ---[  56]---> BDD-cost:  227
c ---[  54]---> BDD-cost:  295
c ---[  52]---> BDD-cost:  233
c ---[  50]---> BDD-cost:  247
c ---[  46]---> BDD-cost:  237
c ---[  44]---> BDD-cost:  149
c ---[  40]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   85
c ---[  36]---> BDD-cost:  109
c ---[  34]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:   71
c ---[  28]---> BDD-cost:   67
c ---[  26]---> BDD-cost:  151
c ---[  24]---> BDD-cost:  147
c ---[  22]---> BDD-cost:  177
c ---[  20]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  147
c ---[  14]---> BDD-cost:  215
c ---[  12]---> BDD-cost:  181
c ---[  10]---> BDD-cost:  235
c ---[   8]---> BDD-cost:  163
c ---[   6]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   59
c ---[   2]---> BDD-cost:  139
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  556705  1546773 |  185568       0        0     nan |  0.000 % |
c |       100 |  556705  1546773 |  204124     100     5588    55.9 |  0.588 % |
c |       250 |  556666  1546664 |  224537     224    12453    55.6 |  0.591 % |
c |       475 |  556616  1546515 |  246991     444    20776    46.8 |  0.598 % |
c |       812 |  556565  1546377 |  271690     777    73035    94.0 |  0.600 % |
c |      1320 |  556565  1546377 |  298859    1285   151800   118.1 |  0.600 % |
c |      2080 |  556078  1545030 |  328745    2010   196008    97.5 |  0.640 % |
c |      3219 |  555916  1544566 |  361619    3142   321129   102.2 |  0.661 % |
c |      4928 |  553857  1538932 |  397781    4711   534915   113.5 |  0.862 % |
c |      7491 |  553675  1538424 |  437559    7252   896739   123.7 |  0.883 % |
c |     11336 |  553504  1537943 |  481315   11064  1318064   119.1 |  0.898 % |
c |     17102 |  552763  1535895 |  529447   16749  2072031   123.7 |  0.964 % |
c |     25752 |  552698  1535712 |  582391   25386  4197786   165.4 |  0.971 % |
c |     38726 |  552330  1534708 |  640631   38106  6393123   167.8 |  0.994 % |
c |     58188 |  552049  1533955 |  704694   57514 10479307   182.2 |  1.004 % |
c |     87380 |  551731  1533099 |  775163   86644 17582579   202.9 |  1.019 % |
c |    131169 |  551531  1532560 |  852679  130381 30406338   233.2 |  1.028 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.90 0.90 2/54 9570
Raw data (stat): 9570 (runsolver) R 9569 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487587910 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.90 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 12985 0 0 0 959 39 0 0 25 0 1 0 487587910 63586304 12627 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15524 12627 603 41 0 15483 0
vsize: 62096
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.90 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 13122 0 0 0 1958 40 0 0 25 0 1 0 487587910 64122880 12764 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15655 12764 603 41 0 15614 0
vsize: 62620
[startup+30.0017 s]
Raw data (loadavg): 0.90 0.91 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 13288 0 0 0 2958 41 0 0 25 0 1 0 487587910 64794624 12930 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15819 12930 603 41 0 15778 0
vsize: 63276
[startup+40.0025 s]
Raw data (loadavg): 0.92 0.91 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 13545 0 0 0 3957 42 0 0 25 0 1 0 487587910 65875968 13187 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16083 13187 603 41 0 16042 0
vsize: 64332
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.91 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 13779 0 0 0 4956 43 0 0 25 0 1 0 487587910 66822144 13421 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16314 13421 603 41 0 16273 0
vsize: 65256
[startup+60.0028 s]
Raw data (loadavg): 0.94 0.91 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 13933 0 0 0 5955 44 0 0 25 0 1 0 487587910 67497984 13575 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16479 13575 603 41 0 16438 0
vsize: 65916
[startup+70.004 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 14161 0 0 0 6955 44 0 0 25 0 1 0 487587910 68304896 13803 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16676 13803 603 41 0 16635 0
vsize: 66704
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.92 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 14313 0 0 0 7954 45 0 0 25 0 1 0 487587910 68980736 13955 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16841 13955 603 41 0 16800 0
vsize: 67364
[startup+90.0057 s]
Raw data (loadavg): 0.96 0.92 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 14612 0 0 0 8953 46 0 0 25 0 1 0 487587910 70197248 14254 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17138 14254 603 41 0 17097 0
vsize: 68552
[startup+100.006 s]
Raw data (loadavg): 0.97 0.92 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 14804 0 0 0 9953 47 0 0 25 0 1 0 487587910 71004160 14446 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17335 14446 603 41 0 17294 0
vsize: 69340
[startup+110.007 s]
Raw data (loadavg): 0.97 0.92 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 14992 0 0 0 10952 47 0 0 25 0 1 0 487587910 71680000 14634 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17500 14634 603 41 0 17459 0
vsize: 70000
[startup+120.008 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 15245 0 0 0 11951 48 0 0 25 0 1 0 487587910 72781824 14887 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17769 14887 603 41 0 17728 0
vsize: 71076
[startup+130.008 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 15568 0 0 0 12951 49 0 0 25 0 1 0 487587910 74121216 15210 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18096 15210 603 41 0 18055 0
vsize: 72384
[startup+140.008 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 15947 0 0 0 13950 50 0 0 25 0 1 0 487587910 75739136 15589 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18491 15589 603 41 0 18450 0
vsize: 73964
[startup+150.01 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 16253 0 0 0 14950 50 0 0 25 0 1 0 487587910 76951552 15895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18787 15895 603 41 0 18746 0
vsize: 75148
[startup+160.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 16537 0 0 0 15949 51 0 0 25 0 1 0 487587910 78032896 16179 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19051 16179 603 41 0 19010 0
vsize: 76204
[startup+170.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 16867 0 0 0 16948 52 0 0 25 0 1 0 487587910 79376384 16509 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19379 16509 603 41 0 19338 0
vsize: 77516
[startup+180.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 17147 0 0 0 17947 53 0 0 25 0 1 0 487587910 80592896 16789 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19676 16789 603 41 0 19635 0
vsize: 78704
[startup+190.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 17489 0 0 0 18946 54 0 0 25 0 1 0 487587910 81940480 17131 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20005 17131 603 41 0 19964 0
vsize: 80020
[startup+200.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 17715 0 0 0 19946 55 0 0 25 0 1 0 487587910 82882560 17357 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20235 17357 603 41 0 20194 0
vsize: 80940
[startup+210.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 17924 0 0 0 20944 57 0 0 25 0 1 0 487587910 83685376 17566 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20431 17566 603 41 0 20390 0
vsize: 81724
[startup+220.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 18141 0 0 0 21943 57 0 0 25 0 1 0 487587910 84631552 17783 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20662 17783 603 41 0 20621 0
vsize: 82648
[startup+230.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 18356 0 0 0 22943 58 0 0 25 0 1 0 487587910 85438464 17998 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20859 17998 603 41 0 20818 0
vsize: 83436
[startup+240.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 18599 0 0 0 23942 59 0 0 25 0 1 0 487587910 86519808 18241 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21123 18241 603 41 0 21082 0
vsize: 84492
[startup+250.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 18804 0 0 0 24942 60 0 0 25 0 1 0 487587910 87445504 18446 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21349 18446 603 41 0 21308 0
vsize: 85396
[startup+260.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 19075 0 0 0 25941 61 0 0 25 0 1 0 487587910 88514560 18717 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21610 18717 603 41 0 21569 0
vsize: 86440
[startup+270.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 19338 0 0 0 26940 62 0 0 25 0 1 0 487587910 89591808 18980 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21873 18980 603 41 0 21832 0
vsize: 87492
[startup+280.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 19562 0 0 0 27939 63 0 0 25 0 1 0 487587910 90533888 19204 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22103 19204 603 41 0 22062 0
vsize: 88412
[startup+290.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 19785 0 0 0 28938 64 0 0 25 0 1 0 487587910 91475968 19427 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22333 19427 603 41 0 22292 0
vsize: 89332
[startup+300.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 20060 0 0 0 29937 65 0 0 25 0 1 0 487587910 92549120 19702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22595 19702 603 41 0 22554 0
vsize: 90380
[startup+310.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 20294 0 0 0 30937 66 0 0 25 0 1 0 487587910 93495296 19936 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22826 19936 603 41 0 22785 0
vsize: 91304
[startup+320.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 20673 0 0 0 31935 67 0 0 25 0 1 0 487587910 95100928 20315 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23218 20315 603 41 0 23177 0
vsize: 92872
[startup+330.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 20922 0 0 0 32934 68 0 0 25 0 1 0 487587910 96038912 20564 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23447 20564 603 41 0 23406 0
vsize: 93788
[startup+340.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 21359 0 0 0 33932 70 0 0 25 0 1 0 487587910 97787904 21001 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23874 21001 603 41 0 23833 0
vsize: 95496
[startup+350.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 21725 0 0 0 34932 71 0 0 25 0 1 0 487587910 99266560 21367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24235 21367 603 41 0 24194 0
vsize: 96940
[startup+360.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 21998 0 0 0 35931 72 0 0 25 0 1 0 487587910 100483072 21640 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24532 21640 603 41 0 24491 0
vsize: 98128
[startup+370.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 22299 0 0 0 36929 73 0 0 25 0 1 0 487587910 101699584 21941 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24829 21941 603 41 0 24788 0
vsize: 99316
[startup+380.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 22615 0 0 0 37929 74 0 0 25 0 1 0 487587910 102907904 22257 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25124 22257 603 41 0 25083 0
vsize: 100496
[startup+390.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 22895 0 0 0 38928 75 0 0 25 0 1 0 487587910 104116224 22537 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25419 22537 603 41 0 25378 0
vsize: 101676
[startup+400.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 23069 0 0 0 39928 75 0 0 25 0 1 0 487587910 104792064 22711 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25584 22711 603 41 0 25543 0
vsize: 102336
[startup+410.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 23400 0 0 0 40927 77 0 0 25 0 1 0 487587910 106127360 23042 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25910 23042 603 41 0 25869 0
vsize: 103640
[startup+420.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 23696 0 0 0 41926 78 0 0 25 0 1 0 487587910 107339776 23338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26206 23338 603 41 0 26165 0
vsize: 104824
[startup+430.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 24027 0 0 0 42924 79 0 0 25 0 1 0 487587910 108687360 23669 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26535 23669 603 41 0 26494 0
vsize: 106140
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 24227 0 0 0 43923 80 0 0 25 0 1 0 487587910 109502464 23869 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26734 23869 603 41 0 26693 0
vsize: 106936
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 24558 0 0 0 44922 82 0 0 25 0 1 0 487587910 110845952 24200 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27062 24200 603 41 0 27021 0
vsize: 108248
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 24879 0 0 0 45920 83 0 0 25 0 1 0 487587910 112181248 24521 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27388 24521 603 41 0 27347 0
vsize: 109552
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 25110 0 0 0 46920 84 0 0 25 0 1 0 487587910 113123328 24752 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27618 24752 603 41 0 27577 0
vsize: 110472
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 25411 0 0 0 47919 85 0 0 25 0 1 0 487587910 114343936 25053 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27916 25053 603 41 0 27875 0
vsize: 111664
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 25657 0 0 0 48919 86 0 0 25 0 1 0 487587910 115412992 25299 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28177 25299 603 41 0 28136 0
vsize: 112708
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 25927 0 0 0 49918 87 0 0 25 0 1 0 487587910 116748288 25569 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28503 25569 603 41 0 28462 0
vsize: 114012
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 26248 0 0 0 50916 89 0 0 25 0 1 0 487587910 118095872 25890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28832 25890 603 41 0 28791 0
vsize: 115328
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 26436 0 0 0 51916 89 0 0 25 0 1 0 487587910 118771712 26078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28997 26078 603 41 0 28956 0
vsize: 115988
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 26661 0 0 0 52914 91 0 0 25 0 1 0 487587910 119726080 26303 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29230 26303 603 41 0 29189 0
vsize: 116920
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 26903 0 0 0 53914 92 0 0 25 0 1 0 487587910 120664064 26545 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29459 26545 603 41 0 29418 0
vsize: 117836
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 27128 0 0 0 54913 92 0 0 25 0 1 0 487587910 121606144 26770 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29689 26770 603 41 0 29648 0
vsize: 118756
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 27367 0 0 0 55912 94 0 0 25 0 1 0 487587910 122540032 27009 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29917 27009 603 41 0 29876 0
vsize: 119668
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 27637 0 0 0 56911 95 0 0 25 0 1 0 487587910 123764736 27279 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30216 27279 603 41 0 30175 0
vsize: 120864
[startup+580.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 27906 0 0 0 57910 96 0 0 25 0 1 0 487587910 124846080 27548 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30480 27548 603 41 0 30439 0
vsize: 121920
[startup+590.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 28202 0 0 0 58909 97 0 0 25 0 1 0 487587910 126062592 27844 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30777 27844 603 41 0 30736 0
vsize: 123108
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 28485 0 0 0 59908 98 0 0 25 0 1 0 487587910 127135744 28127 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31039 28127 603 41 0 30998 0
vsize: 124156
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 28814 0 0 0 60907 99 0 0 25 0 1 0 487587910 128483328 28456 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31368 28456 603 41 0 31327 0
vsize: 125472
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 29122 0 0 0 61906 100 0 0 25 0 1 0 487587910 129826816 28764 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31696 28764 603 41 0 31655 0
vsize: 126784
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 29426 0 0 0 62906 100 0 0 25 0 1 0 487587910 131035136 29068 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31991 29068 603 41 0 31950 0
vsize: 127964
[startup+640.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 29711 0 0 0 63905 101 0 0 25 0 1 0 487587910 132112384 29353 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32254 29353 603 41 0 32213 0
vsize: 129016
[startup+650.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 29939 0 0 0 64904 102 0 0 25 0 1 0 487587910 133054464 29581 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32484 29581 603 41 0 32443 0
vsize: 129936
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 30131 0 0 0 65904 103 0 0 25 0 1 0 487587910 133857280 29773 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32680 29773 603 41 0 32639 0
vsize: 130720
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 30476 0 0 0 66902 104 0 0 25 0 1 0 487587910 135344128 30118 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33043 30118 603 41 0 33002 0
vsize: 132172
[startup+680.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 30912 0 0 0 67901 106 0 0 25 0 1 0 487587910 137109504 30554 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33474 30554 603 41 0 33433 0
vsize: 133896
[startup+690.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 31209 0 0 0 68900 107 0 0 25 0 1 0 487587910 138326016 30851 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33771 30851 603 41 0 33730 0
vsize: 135084
[startup+700.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 31440 0 0 0 69899 108 0 0 25 0 1 0 487587910 139251712 31082 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33997 31082 603 41 0 33956 0
vsize: 135988
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 31702 0 0 0 70899 109 0 0 25 0 1 0 487587910 140308480 31344 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34255 31344 603 41 0 34214 0
vsize: 137020
[startup+720.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 31937 0 0 0 71898 110 0 0 25 0 1 0 487587910 141250560 31579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34485 31579 603 41 0 34444 0
vsize: 137940
[startup+730.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 32176 0 0 0 72897 111 0 0 25 0 1 0 487587910 142196736 31818 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34716 31818 603 41 0 34675 0
vsize: 138864
[startup+740.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 32448 0 0 0 73896 112 0 0 25 0 1 0 487587910 143269888 32090 4294967295 134512640 134672761 3221224544 3221223728 134558697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34978 32090 603 41 0 34937 0
vsize: 139912
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 32671 0 0 0 74896 113 0 0 25 0 1 0 487587910 144207872 32313 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35207 32313 603 41 0 35166 0
vsize: 140828
[startup+760.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 32941 0 0 0 75895 114 0 0 25 0 1 0 487587910 145289216 32583 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35471 32583 603 41 0 35430 0
vsize: 141884
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 33202 0 0 0 76894 114 0 0 25 0 1 0 487587910 146358272 32844 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35732 32844 603 41 0 35691 0
vsize: 142928
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 33596 0 0 0 77893 115 0 0 25 0 1 0 487587910 147980288 33238 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36128 33238 603 41 0 36087 0
vsize: 144512
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 33875 0 0 0 78892 116 0 0 25 0 1 0 487587910 149192704 33517 4294967295 134512640 134672761 3221224544 3221223648 134560150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36424 33517 603 41 0 36383 0
vsize: 145696
[startup+800.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 34093 0 0 0 79892 117 0 0 25 0 1 0 487587910 150003712 33735 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36622 33735 603 41 0 36581 0
vsize: 146488
[startup+810.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 34316 0 0 0 80891 118 0 0 25 0 1 0 487587910 150949888 33958 4294967295 134512640 134672761 3221224544 3221223728 134558775 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36853 33958 603 41 0 36812 0
vsize: 147412
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 34669 0 0 0 81890 119 0 0 25 0 1 0 487587910 152432640 34311 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37215 34311 603 41 0 37174 0
vsize: 148860
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 35000 0 0 0 82888 120 0 0 25 0 1 0 487587910 153772032 34642 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37542 34642 603 41 0 37501 0
vsize: 150168
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 35301 0 0 0 83887 121 0 0 25 0 1 0 487587910 154980352 34943 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37837 34943 603 41 0 37796 0
vsize: 151348
[startup+850.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 35552 0 0 0 84889 122 0 0 25 0 1 0 487587910 156053504 35194 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38099 35194 603 41 0 38058 0
vsize: 152396
[startup+860.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 35877 0 0 0 85888 124 0 0 25 0 1 0 487587910 157392896 35519 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38426 35519 603 41 0 38385 0
vsize: 153704
[startup+870.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 36142 0 0 0 86888 124 0 0 25 0 1 0 487587910 158388224 35784 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38669 35784 603 41 0 38628 0
vsize: 154676
[startup+880.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 36477 0 0 0 87887 126 0 0 25 0 1 0 487587910 159866880 36119 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39030 36119 603 41 0 38989 0
vsize: 156120
[startup+890.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 36810 0 0 0 88886 127 0 0 25 0 1 0 487587910 161218560 36452 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39360 36452 603 41 0 39319 0
vsize: 157440
[startup+900.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 37111 0 0 0 89886 128 0 0 25 0 1 0 487587910 162414592 36753 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39652 36753 603 41 0 39611 0
vsize: 158608
[startup+910.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 37406 0 0 0 90885 128 0 0 25 0 1 0 487587910 163635200 37048 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39950 37048 603 41 0 39909 0
vsize: 159800
[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 37570 0 0 0 91885 129 0 0 25 0 1 0 487587910 164302848 37212 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40113 37212 603 41 0 40072 0
vsize: 160452
[startup+930.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 37816 0 0 0 92884 130 0 0 25 0 1 0 487587910 165232640 37458 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40340 37458 603 41 0 40299 0
vsize: 161360
[startup+940.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 38152 0 0 0 93883 131 0 0 25 0 1 0 487587910 166711296 37794 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40701 37794 603 41 0 40660 0
vsize: 162804
[startup+950.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 38546 0 0 0 94881 133 0 0 25 0 1 0 487587910 168333312 38188 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41097 38188 603 41 0 41056 0
vsize: 164388
[startup+960.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 38874 0 0 0 95880 134 0 0 25 0 1 0 487587910 169545728 38516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41393 38516 603 41 0 41352 0
vsize: 165572
[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 39348 0 0 0 96879 135 0 0 25 0 1 0 487587910 171565056 38990 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41886 38990 603 41 0 41845 0
vsize: 167544
[startup+980.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 39681 0 0 0 97878 136 0 0 25 0 1 0 487587910 172904448 39323 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42213 39323 603 41 0 42172 0
vsize: 168852
[startup+990.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 39980 0 0 0 98878 137 0 0 25 0 1 0 487587910 174120960 39622 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42510 39622 603 41 0 42469 0
vsize: 170040
[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 40341 0 0 0 99877 138 0 0 25 0 1 0 487587910 175603712 39983 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42872 39983 603 41 0 42831 0
vsize: 171488
[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 40600 0 0 0 100876 139 0 0 25 0 1 0 487587910 176672768 40242 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43133 40242 603 41 0 43092 0
vsize: 172532
[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 40903 0 0 0 101876 140 0 0 25 0 1 0 487587910 177881088 40545 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43428 40545 603 41 0 43387 0
vsize: 173712
[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 41193 0 0 0 102874 142 0 0 25 0 1 0 487587910 179085312 40835 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43722 40835 603 41 0 43681 0
vsize: 174888
[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 41529 0 0 0 103874 142 0 0 25 0 1 0 487587910 180424704 41171 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44049 41171 603 41 0 44008 0
vsize: 176196
[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 41805 0 0 0 104873 143 0 0 25 0 1 0 487587910 181637120 41447 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44345 41447 603 41 0 44304 0
vsize: 177380
[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 42130 0 0 0 105872 144 0 0 25 0 1 0 487587910 182968320 41772 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44670 41772 603 41 0 44629 0
vsize: 178680
[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 42408 0 0 0 106870 146 0 0 25 0 1 0 487587910 184049664 42050 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44934 42050 603 41 0 44893 0
vsize: 179736
[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 42587 0 0 0 107870 147 0 0 25 0 1 0 487587910 184721408 42229 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45098 42229 603 41 0 45057 0
vsize: 180392
[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 42768 0 0 0 108870 147 0 0 25 0 1 0 487587910 185528320 42410 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45295 42410 603 41 0 45254 0
vsize: 181180
[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 42984 0 0 0 109869 148 0 0 25 0 1 0 487587910 186458112 42626 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45522 42626 603 41 0 45481 0
vsize: 182088
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 43217 0 0 0 110869 149 0 0 25 0 1 0 487587910 187404288 42859 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45753 42859 603 41 0 45712 0
vsize: 183012
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 43435 0 0 0 111868 150 0 0 25 0 1 0 487587910 188203008 43077 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45948 43077 603 41 0 45907 0
vsize: 183792
[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 43722 0 0 0 112867 151 0 0 25 0 1 0 487587910 189415424 43364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46244 43364 603 41 0 46203 0
vsize: 184976
[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 43957 0 0 0 113867 152 0 0 25 0 1 0 487587910 190353408 43599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46473 43599 603 41 0 46432 0
vsize: 185892
[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 44266 0 0 0 114866 152 0 0 25 0 1 0 487587910 191700992 43908 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46802 43908 603 41 0 46761 0
vsize: 187208
[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 44604 0 0 0 115865 153 0 0 25 0 1 0 487587910 193036288 44246 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47128 44246 603 41 0 47087 0
vsize: 188512
[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 44918 0 0 0 116865 153 0 0 25 0 1 0 487587910 194781184 44560 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47554 44560 603 41 0 47513 0
vsize: 190216
[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 45218 0 0 0 117864 154 0 0 25 0 1 0 487587910 195993600 44860 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47850 44860 603 41 0 47809 0
vsize: 191400
[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 45359 0 0 0 118864 154 0 0 25 0 1 0 487587910 196673536 45001 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48016 45001 603 41 0 47975 0
vsize: 192064
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9570
Raw data (stat): 9570 (minisat+) R 9569 29151 29150 0 -1 0 45687 0 0 0 119865 155 0 0 25 0 1 0 487587910 198025216 45329 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48346 45329 603 41 0 48305 0
vsize: 193384
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.2 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 9570
Raw data (stat): 9570 (minisat+) Z 9569 29151 29150 0 -1 12 45689 0 0 0 119865 163 0 0 25 0 1 0 487587910 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.2
CPU time (s): 1200.29
CPU user time (s): 1198.65
CPU system time (s): 1.63875
CPU usage (%): 100.008
Max. virtual memory (Kb): 193384
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####