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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.116981
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 16500

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-21 07:33:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13182 boxname=wulflinc4 idbench=1014 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  26490113618ae9605b5ebe6370b5910b  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-air04.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-air04.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-20-10-air04.opb
IDLAUNCH: 13182
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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		: 451.169
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:        698576 kB
Buffers:         32308 kB
Cached:         280560 kB
SwapCached:          0 kB
Active:          57308 kB
Inactive:       258352 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        698324 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14776 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 07:53:12 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 13182 7 1200.34 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.80 0.92 0.90 2/54 3871
Raw data (stat): 3871 (runsolver) R 3870 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485083261 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.83 0.93 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 12985 0 0 0 968 30 0 0 25 0 1 0 485083261 63586304 12627 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15524 12627 603 41 0 15483 0
vsize: 62096
[startup+20.0018 s]
Raw data (loadavg): 0.86 0.93 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 13123 0 0 0 1967 30 0 0 25 0 1 0 485083261 64122880 12765 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15655 12765 603 41 0 15614 0
vsize: 62620
[startup+30.0022 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 13291 0 0 0 2966 31 0 0 25 0 1 0 485083261 64794624 12933 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15819 12933 603 41 0 15778 0
vsize: 63276
[startup+40.0028 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 13546 0 0 0 3964 32 0 0 25 0 1 0 485083261 65875968 13188 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16083 13188 603 41 0 16042 0
vsize: 64332
[startup+50.0034 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 13780 0 0 0 4964 33 0 0 25 0 1 0 485083261 66822144 13422 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16314 13422 603 41 0 16273 0
vsize: 65256
[startup+60.0032 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 13945 0 0 0 5963 33 0 0 25 0 1 0 485083261 67497984 13587 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16479 13587 603 41 0 16438 0
vsize: 65916
[startup+70.0044 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 14168 0 0 0 6963 34 0 0 25 0 1 0 485083261 68440064 13810 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16709 13810 603 41 0 16668 0
vsize: 66836
[startup+80.005 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 14325 0 0 0 7962 35 0 0 25 0 1 0 485083261 68980736 13967 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16841 13967 603 41 0 16800 0
vsize: 67364
[startup+90.0052 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 14629 0 0 0 8961 36 0 0 25 0 1 0 485083261 70197248 14271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17138 14271 603 41 0 17097 0
vsize: 68552
[startup+100.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 14837 0 0 0 9961 37 0 0 25 0 1 0 485083261 71139328 14479 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17368 14479 603 41 0 17327 0
vsize: 69472
[startup+110.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 15016 0 0 0 10961 37 0 0 25 0 1 0 485083261 71815168 14658 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17533 14658 603 41 0 17492 0
vsize: 70132
[startup+120.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 15307 0 0 0 11960 38 0 0 25 0 1 0 485083261 73052160 14949 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17835 14949 603 41 0 17794 0
vsize: 71340
[startup+130.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 15631 0 0 0 12959 39 0 0 25 0 1 0 485083261 74391552 15273 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18162 15273 603 41 0 18121 0
vsize: 72648
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 15997 0 0 0 13958 40 0 0 25 0 1 0 485083261 75874304 15639 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18524 15639 603 41 0 18483 0
vsize: 74096
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 16309 0 0 0 14958 41 0 0 25 0 1 0 485083261 77086720 15951 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18820 15951 603 41 0 18779 0
vsize: 75280
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 16587 0 0 0 15957 41 0 0 25 0 1 0 485083261 78303232 16229 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19117 16229 603 41 0 19076 0
vsize: 76468
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 16930 0 0 0 16957 42 0 0 25 0 1 0 485083261 79646720 16572 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19445 16572 603 41 0 19404 0
vsize: 77780
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 17238 0 0 0 17956 43 0 0 25 0 1 0 485083261 80998400 16880 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19775 16880 603 41 0 19734 0
vsize: 79100
[startup+190.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 17535 0 0 0 18955 44 0 0 25 0 1 0 485083261 82206720 17177 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20070 17177 603 41 0 20029 0
vsize: 80280
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 17767 0 0 0 19955 45 0 0 25 0 1 0 485083261 83148800 17409 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20300 17409 603 41 0 20259 0
vsize: 81200
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 17970 0 0 0 20954 45 0 0 25 0 1 0 485083261 83951616 17612 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20496 17612 603 41 0 20455 0
vsize: 81984
[startup+220.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 18169 0 0 0 21954 46 0 0 25 0 1 0 485083261 84766720 17811 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20695 17811 603 41 0 20654 0
vsize: 82780
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 18420 0 0 0 22953 47 0 0 25 0 1 0 485083261 85708800 18062 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20925 18062 603 41 0 20884 0
vsize: 83700
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 18662 0 0 0 23953 47 0 0 25 0 1 0 485083261 86917120 18304 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21220 18304 603 41 0 21179 0
vsize: 84880
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 18868 0 0 0 24953 48 0 0 25 0 1 0 485083261 87711744 18510 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21414 18510 603 41 0 21373 0
vsize: 85656
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 19198 0 0 0 25952 49 0 0 25 0 1 0 485083261 89051136 18840 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21741 18840 603 41 0 21700 0
vsize: 86964
[startup+270.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 19434 0 0 0 26951 50 0 0 25 0 1 0 485083261 89997312 19076 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21972 19076 603 41 0 21931 0
vsize: 87888
[startup+280.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 19623 0 0 0 27951 50 0 0 25 0 1 0 485083261 90804224 19265 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22169 19265 603 41 0 22128 0
vsize: 88676
[startup+290.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 19875 0 0 0 28949 51 0 0 25 0 1 0 485083261 91746304 19517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22399 19517 603 41 0 22358 0
vsize: 89596
[startup+300.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 20145 0 0 0 29948 52 0 0 25 0 1 0 485083261 92954624 19787 4294967295 134512640 134672761 3221224544 3221223712 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22694 19787 603 41 0 22653 0
vsize: 90776
[startup+310.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 20410 0 0 0 30947 53 0 0 25 0 1 0 485083261 94035968 20052 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22958 20052 603 41 0 22917 0
vsize: 91832
[startup+320.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 20748 0 0 0 31946 54 0 0 25 0 1 0 485083261 95367168 20390 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23283 20390 603 41 0 23242 0
vsize: 93132
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 21090 0 0 0 32945 55 0 0 25 0 1 0 485083261 96714752 20732 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23612 20732 603 41 0 23571 0
vsize: 94448
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 21536 0 0 0 33944 57 0 0 25 0 1 0 485083261 98598912 21178 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24072 21178 603 41 0 24031 0
vsize: 96288
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 21837 0 0 0 34943 57 0 0 25 0 1 0 485083261 99807232 21479 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24367 21479 603 41 0 24326 0
vsize: 97468
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 22142 0 0 0 35943 58 0 0 25 0 1 0 485083261 101023744 21784 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24664 21784 603 41 0 24623 0
vsize: 98656
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 22416 0 0 0 36942 59 0 0 25 0 1 0 485083261 102100992 22058 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24927 22058 603 41 0 24886 0
vsize: 99708
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 22748 0 0 0 37941 60 0 0 25 0 1 0 485083261 103444480 22390 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25255 22390 603 41 0 25214 0
vsize: 101020
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 22966 0 0 0 38941 61 0 0 25 0 1 0 485083261 104386560 22608 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25485 22608 603 41 0 25444 0
vsize: 101940
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 23175 0 0 0 39940 61 0 0 25 0 1 0 485083261 105193472 22817 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25682 22817 603 41 0 25641 0
vsize: 102728
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 23533 0 0 0 40939 62 0 0 25 0 1 0 485083261 106663936 23175 4294967295 134512640 134672761 3221224544 3221223648 134559951 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26041 23175 603 41 0 26000 0
vsize: 104164
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 23874 0 0 0 41938 64 0 0 25 0 1 0 485083261 108011520 23516 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26370 23516 603 41 0 26329 0
vsize: 105480
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 24106 0 0 0 42937 64 0 0 25 0 1 0 485083261 108957696 23748 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26601 23748 603 41 0 26560 0
vsize: 106404
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 24337 0 0 0 43936 65 0 0 25 0 1 0 485083261 109907968 23979 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26833 23979 603 41 0 26792 0
vsize: 107332
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 24750 0 0 0 44935 66 0 0 25 0 1 0 485083261 111640576 24392 4294967295 134512640 134672761 3221224544 3221223668 134566103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27256 24392 603 41 0 27215 0
vsize: 109024
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 24975 0 0 0 45935 67 0 0 25 0 1 0 485083261 112578560 24617 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27485 24617 603 41 0 27444 0
vsize: 109940
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 25276 0 0 0 46934 68 0 0 25 0 1 0 485083261 113803264 24918 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27784 24918 603 41 0 27743 0
vsize: 111136
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 25538 0 0 0 47933 69 0 0 25 0 1 0 485083261 114880512 25180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28047 25180 603 41 0 28006 0
vsize: 112188
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 25775 0 0 0 48933 70 0 0 25 0 1 0 485083261 115814400 25417 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28275 25417 603 41 0 28234 0
vsize: 113100
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 26140 0 0 0 49932 71 0 0 25 0 1 0 485083261 117555200 25782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28700 25782 603 41 0 28659 0
vsize: 114800
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 26350 0 0 0 50931 72 0 0 25 0 1 0 485083261 118501376 25992 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28931 25992 603 41 0 28890 0
vsize: 115724
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 26534 0 0 0 51930 73 0 0 25 0 1 0 485083261 119185408 26176 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29098 26176 603 41 0 29057 0
vsize: 116392
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 26759 0 0 0 52930 73 0 0 25 0 1 0 485083261 120127488 26401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29328 26401 603 41 0 29287 0
vsize: 117312
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 27048 0 0 0 53929 74 0 0 25 0 1 0 485083261 121335808 26690 4294967295 134512640 134672761 3221224544 3221223680 134560560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29623 26690 603 41 0 29582 0
vsize: 118492
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 27254 0 0 0 54928 75 0 0 25 0 1 0 485083261 122134528 26896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29818 26896 603 41 0 29777 0
vsize: 119272
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 27543 0 0 0 55927 77 0 0 25 0 1 0 485083261 123359232 27185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30117 27185 603 41 0 30076 0
vsize: 120468
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 27807 0 0 0 56927 77 0 0 25 0 1 0 485083261 124436480 27449 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30380 27449 603 41 0 30339 0
vsize: 121520
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 28115 0 0 0 57926 78 0 0 25 0 1 0 485083261 125657088 27757 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30678 27757 603 41 0 30637 0
vsize: 122712
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 28394 0 0 0 58926 78 0 0 25 0 1 0 485083261 126734336 28036 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30941 28036 603 41 0 30900 0
vsize: 123764
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 28722 0 0 0 59925 80 0 0 25 0 1 0 485083261 128077824 28364 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31269 28364 603 41 0 31228 0
vsize: 125076
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 29003 0 0 0 60924 80 0 0 25 0 1 0 485083261 129290240 28645 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31565 28645 603 41 0 31524 0
vsize: 126260
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 29339 0 0 0 61924 81 0 0 25 0 1 0 485083261 130629632 28981 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31892 28981 603 41 0 31851 0
vsize: 127568
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 29625 0 0 0 62923 82 0 0 25 0 1 0 485083261 131846144 29267 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32189 29267 603 41 0 32148 0
vsize: 128756
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 29834 0 0 0 63922 83 0 0 25 0 1 0 485083261 132653056 29476 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32386 29476 603 41 0 32345 0
vsize: 129544
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 30059 0 0 0 64921 84 0 0 25 0 1 0 485083261 133591040 29701 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32615 29701 603 41 0 32574 0
vsize: 130460
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 30395 0 0 0 65921 85 0 0 25 0 1 0 485083261 134942720 30037 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32945 30037 603 41 0 32904 0
vsize: 131780
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 30809 0 0 0 66920 85 0 0 25 0 1 0 485083261 136691712 30451 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33372 30451 603 41 0 33331 0
vsize: 133488
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 31126 0 0 0 67919 87 0 0 25 0 1 0 485083261 137920512 30768 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33672 30768 603 41 0 33631 0
vsize: 134688
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 31369 0 0 0 68918 87 0 0 25 0 1 0 485083261 138989568 31011 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33933 31011 603 41 0 33892 0
vsize: 135732
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 31626 0 0 0 69918 87 0 0 25 0 1 0 485083261 139915264 31268 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34159 31268 603 41 0 34118 0
vsize: 136636
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 31863 0 0 0 70916 89 0 0 25 0 1 0 485083261 140980224 31505 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34419 31505 603 41 0 34378 0
vsize: 137676
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 32106 0 0 0 71915 90 0 0 25 0 1 0 485083261 141926400 31748 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34650 31748 603 41 0 34609 0
vsize: 138600
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 32368 0 0 0 72915 90 0 0 25 0 1 0 485083261 142999552 32010 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34912 32010 603 41 0 34871 0
vsize: 139648
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 32599 0 0 0 73914 90 0 0 25 0 1 0 485083261 143941632 32241 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35142 32241 603 41 0 35101 0
vsize: 140568
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 32886 0 0 0 74914 91 0 0 25 0 1 0 485083261 145154048 32528 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35438 32528 603 41 0 35397 0
vsize: 141752
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 33142 0 0 0 75913 92 0 0 25 0 1 0 485083261 146223104 32784 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35699 32784 603 41 0 35658 0
vsize: 142796
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 33492 0 0 0 76913 92 0 0 25 0 1 0 485083261 147574784 33134 4294967295 134512640 134672761 3221224544 3221223648 134560267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36029 33134 603 41 0 35988 0
vsize: 144116
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 33813 0 0 0 77912 93 0 0 25 0 1 0 485083261 148922368 33455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36358 33455 603 41 0 36317 0
vsize: 145432
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 34031 0 0 0 78912 94 0 0 25 0 1 0 485083261 149733376 33673 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36556 33673 603 41 0 36515 0
vsize: 146224
[startup+800.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 34254 0 0 0 79912 94 0 0 25 0 1 0 485083261 150679552 33896 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36787 33896 603 41 0 36746 0
vsize: 147148
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 34590 0 0 0 80911 95 0 0 25 0 1 0 485083261 152027136 34232 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37116 34232 603 41 0 37075 0
vsize: 148464
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 34957 0 0 0 81911 95 0 0 25 0 1 0 485083261 153636864 34599 4294967295 134512640 134672761 3221224544 3221223560 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37509 34599 603 41 0 37468 0
vsize: 150036
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 35239 0 0 0 82910 96 0 0 25 0 1 0 485083261 154705920 34881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37770 34881 603 41 0 37729 0
vsize: 151080
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 35508 0 0 0 83910 97 0 0 25 0 1 0 485083261 155791360 35150 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38035 35150 603 41 0 37994 0
vsize: 152140
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 35826 0 0 0 84909 97 0 0 25 0 1 0 485083261 157122560 35468 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38360 35468 603 41 0 38319 0
vsize: 153440
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 36076 0 0 0 85909 98 0 0 25 0 1 0 485083261 158117888 35718 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38603 35718 603 41 0 38562 0
vsize: 154412
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 36449 0 0 0 86908 99 0 0 25 0 1 0 485083261 159731712 36091 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38997 36091 603 41 0 38956 0
vsize: 155988
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 36763 0 0 0 87908 99 0 0 25 0 1 0 485083261 160948224 36405 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39294 36405 603 41 0 39253 0
vsize: 157176
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 37065 0 0 0 88907 100 0 0 25 0 1 0 485083261 162144256 36707 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39586 36707 603 41 0 39545 0
vsize: 158344
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 37376 0 0 0 89907 101 0 0 25 0 1 0 485083261 163504128 37018 4294967295 134512640 134672761 3221224544 3221223680 134560694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39918 37018 603 41 0 39877 0
vsize: 159672
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 37551 0 0 0 90906 102 0 0 25 0 1 0 485083261 164167680 37193 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40080 37193 603 41 0 40039 0
vsize: 160320
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 37797 0 0 0 91905 103 0 0 25 0 1 0 485083261 165232640 37439 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40340 37439 603 41 0 40299 0
vsize: 161360
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 38114 0 0 0 92904 104 0 0 25 0 1 0 485083261 166440960 37756 4294967295 134512640 134672761 3221224544 3221223648 134559943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40635 37756 603 41 0 40594 0
vsize: 162540
[startup+940.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 38501 0 0 0 93904 105 0 0 25 0 1 0 485083261 168067072 38143 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41032 38143 603 41 0 40991 0
vsize: 164128
[startup+950.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 38820 0 0 0 94903 106 0 0 25 0 1 0 485083261 169410560 38462 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41360 38462 603 41 0 41319 0
vsize: 165440
[startup+960.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 39329 0 0 0 95912 107 0 0 25 0 1 0 485083261 171429888 38971 4294967295 134512640 134672761 3221224544 3221223648 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41853 38971 603 41 0 41812 0
vsize: 167412
[startup+970.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 39661 0 0 0 96911 108 0 0 25 0 1 0 485083261 172769280 39303 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42180 39303 603 41 0 42139 0
vsize: 168720
[startup+980.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 39946 0 0 0 97911 108 0 0 25 0 1 0 485083261 173985792 39588 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42477 39588 603 41 0 42436 0
vsize: 169908
[startup+990.147 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 40319 0 0 0 98910 110 0 0 25 0 1 0 485083261 175468544 39961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42839 39961 603 41 0 42798 0
vsize: 171356
[startup+1000.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 40579 0 0 0 99910 110 0 0 25 0 1 0 485083261 176537600 40221 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43100 40221 603 41 0 43059 0
vsize: 172400
[startup+1010.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 40887 0 0 0 100910 111 0 0 25 0 1 0 485083261 177881088 40529 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43428 40529 603 41 0 43387 0
vsize: 173712
[startup+1020.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 41182 0 0 0 101909 112 0 0 25 0 1 0 485083261 179085312 40824 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43722 40824 603 41 0 43681 0
vsize: 174888
[startup+1030.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 41516 0 0 0 102909 113 0 0 25 0 1 0 485083261 180424704 41158 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44049 41158 603 41 0 44008 0
vsize: 176196
[startup+1040.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 41797 0 0 0 103909 113 0 0 25 0 1 0 485083261 181506048 41439 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44313 41439 603 41 0 44272 0
vsize: 177252
[startup+1050.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 42125 0 0 0 104908 114 0 0 25 0 1 0 485083261 182837248 41767 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44638 41767 603 41 0 44597 0
vsize: 178552
[startup+1060.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 42403 0 0 0 105907 115 0 0 25 0 1 0 485083261 184049664 42045 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44934 42045 603 41 0 44893 0
vsize: 179736
[startup+1070.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 42585 0 0 0 106907 115 0 0 25 0 1 0 485083261 184721408 42227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45098 42227 603 41 0 45057 0
vsize: 180392
[startup+1080.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 42768 0 0 0 107907 116 0 0 25 0 1 0 485083261 185528320 42410 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45295 42410 603 41 0 45254 0
vsize: 181180
[startup+1090.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 42988 0 0 0 108907 116 0 0 25 0 1 0 485083261 186458112 42630 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45522 42630 603 41 0 45481 0
vsize: 182088
[startup+1100.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 43229 0 0 0 109906 117 0 0 25 0 1 0 485083261 187404288 42871 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45753 42871 603 41 0 45712 0
vsize: 183012
[startup+1110.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 43450 0 0 0 110906 117 0 0 25 0 1 0 485083261 188334080 43092 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45980 43092 603 41 0 45939 0
vsize: 183920
[startup+1120.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 43750 0 0 0 111906 118 0 0 25 0 1 0 485083261 189538304 43392 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46274 43392 603 41 0 46233 0
vsize: 185096
[startup+1130.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 43991 0 0 0 112906 118 0 0 25 0 1 0 485083261 190488576 43633 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46506 43633 603 41 0 46465 0
vsize: 186024
[startup+1140.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 44297 0 0 0 113905 119 0 0 25 0 1 0 485083261 191700992 43939 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46802 43939 603 41 0 46761 0
vsize: 187208
[startup+1150.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 44651 0 0 0 114904 120 0 0 25 0 1 0 485083261 193171456 44293 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47161 44293 603 41 0 47120 0
vsize: 188644
[startup+1160.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 44970 0 0 0 115903 121 0 0 25 0 1 0 485083261 195051520 44612 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47620 44612 603 41 0 47579 0
vsize: 190480
[startup+1170.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 45265 0 0 0 116903 121 0 0 25 0 1 0 485083261 196268032 44907 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47917 44907 603 41 0 47876 0
vsize: 191668
[startup+1180.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 45427 0 0 0 117903 122 0 0 25 0 1 0 485083261 196943872 45069 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48082 45069 603 41 0 48041 0
vsize: 192328
[startup+1190.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 45753 0 0 0 118902 123 0 0 25 0 1 0 485083261 198295552 45395 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48412 45395 603 41 0 48371 0
vsize: 193648
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3871
Raw data (stat): 3871 (minisat+) R 3870 5897 5896 0 -1 0 45962 0 0 0 119902 123 0 0 25 0 1 0 485083261 199102464 45604 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48609 45604 603 41 0 48568 0
vsize: 194436
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3871
Raw data (stat): 3871 (minisat+) Z 3870 5897 5896 0 -1 12 45964 0 0 0 119902 132 0 0 20 0 1 0 485083261 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.35
CPU time (s): 1200.34
CPU user time (s): 1199.02
CPU system time (s): 1.3228
CPU usage (%): 99.9999
Max. virtual memory (Kb): 194436
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####