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/miplib/normalized-mps-v2-20-10-air06.opb
MD5SUM	f85d0079133f298b06c25764b03ff228
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50233
Optimality of the best value was proved	NO
Number of terms in the objective function	8627
Biggest coefficient in the objective function	1859
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	4587852
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	1859
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	4587852
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1182.3
Number of variables	8627
Total number of constraints	9452
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9452
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	461
Trace number 17112

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 09:43:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11686 boxname=wulflinc13 idbench=899 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f85d0079133f298b06c25764b03ff228  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-air06.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-air06.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-air06.opb
IDLAUNCH: 11686
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        592144 kB
Buffers:         34528 kB
Cached:         385196 kB
SwapCached:        176 kB
Active:         188040 kB
Inactive:       234476 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        591892 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            14268 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 10:03:24 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 11686 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1628 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1626]---> BDD-cost:  103
c ---[1622]---> BDD-cost:   43
c ---[1618]---> BDD-cost:   59
c ---[1616]---> BDD-cost:   33
c ---[1614]---> BDD-cost:  109
c ---[1612]---> BDD-cost:  113
c ---[1610]---> BDD-cost:   79
c ---[1608]---> BDD-cost:    3
c ---[1604]---> BDD-cost:   41
c ---[1602]---> BDD-cost:   51
c ---[1600]---> BDD-cost:  147
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:   23
c ---[1594]---> BDD-cost:  135
c ---[1592]---> BDD-cost:   81
c ---[1590]---> BDD-cost:   41
c ---[1588]---> BDD-cost:   27
c ---[1586]---> BDD-cost:   25
c ---[1584]---> BDD-cost:    8
c ---[1582]---> BDD-cost:   71
c ---[1580]---> BDD-cost:  137
c ---[1578]---> BDD-cost:   25
c ---[1576]---> BDD-cost:   13
c ---[1574]---> BDD-cost:   27
c ---[1572]---> BDD-cost:    9
c ---[1570]---> BDD-cost:  131
c ---[1566]---> BDD-cost:   47
c ---[1564]---> BDD-cost:   41
c ---[1562]---> BDD-cost:   27
c ---[1560]---> BDD-cost:   35
c ---[1558]---> BDD-cost:  133
c ---[1556]---> BDD-cost:  303
c ---[1554]---> BDD-cost:  231
c ---[1552]---> BDD-cost:  175
c ---[1550]---> BDD-cost:  131
c ---[1548]---> BDD-cost:   89
c ---[1546]---> BDD-cost:   53
c ---[1544]---> BDD-cost:   65
c ---[1542]---> BDD-cost:  141
c ---[1540]---> BDD-cost:  129
c ---[1538]---> BDD-cost:   21
c ---[1536]---> BDD-cost:   13
c ---[1534]---> BDD-cost:   83
c ---[1532]---> BDD-cost:   63
c ---[1530]---> BDD-cost:    7
c ---[1528]---> BDD-cost:    9
c ---[1526]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   41
c ---[1522]---> BDD-cost:   93
c ---[1520]---> BDD-cost:   55
c ---[1518]---> BDD-cost:   27
c ---[1516]---> BDD-cost:  253
c ---[1514]---> BDD-cost:  189
c ---[1512]---> BDD-cost:  131
c ---[1510]---> BDD-cost:  143
c ---[1508]---> BDD-cost:   55
c ---[1506]---> BDD-cost:  105
c ---[1504]---> BDD-cost:  357
c ---[1502]---> BDD-cost:  355
c ---[1500]---> BDD-cost:  361
c ---[1498]---> BDD-cost:  257
c ---[1496]---> BDD-cost:  263
c ---[1494]---> BDD-cost:  271
c ---[1492]---> BDD-cost:   91
c ---[1488]---> BDD-cost:   15
c ---[1486]---> BDD-cost:    7
c ---[1484]---> BDD-cost:   37
c ---[1478]---> BDD-cost:    1
c ---[1476]---> BDD-cost:   14
c ---[1474]---> BDD-cost:    7
c ---[1472]---> BDD-cost:    1
c ---[1470]---> BDD-cost:    1
c ---[1468]---> BDD-cost:    5
c ---[1466]---> BDD-cost:  103
c ---[1464]---> BDD-cost:  203
c ---[1462]---> BDD-cost:   91
c ---[1460]---> BDD-cost:   49
c ---[1458]---> BDD-cost:    7
c ---[1456]---> BDD-cost:   77
c ---[1452]---> BDD-cost:   55
c ---[1450]---> BDD-cost:   19
c ---[1448]---> BDD-cost:   95
c ---[1446]---> BDD-cost:  101
c ---[1444]---> BDD-cost:  115
c ---[1442]---> BDD-cost:   67
c ---[1440]---> BDD-cost:   33
c ---[1438]---> BDD-cost:   29
c ---[1436]---> BDD-cost:   91
c ---[1434]---> BDD-cost:   25
c ---[1428]---> BDD-cost:   11
c ---[1426]---> BDD-cost:   15
c ---[1424]---> BDD-cost:   29
c ---[1422]---> BDD-cost:  127
c ---[1420]---> BDD-cost:  195
c ---[1418]---> BDD-cost:  143
c ---[1416]---> BDD-cost:  111
c ---[1414]---> BDD-cost:  169
c ---[1412]---> BDD-cost:  169
c ---[1410]---> BDD-cost:  171
c ---[1408]---> BDD-cost:  135
c ---[1406]---> BDD-cost:   43
c ---[1404]---> BDD-cost:  257
c ---[1402]---> BDD-cost:  261
c ---[1400]---> BDD-cost:  167
c ---[1398]---> BDD-cost:  125
c ---[1396]---> BDD-cost:  125
c ---[1394]---> BDD-cost:   39
c ---[1392]---> BDD-cost:   37
c ---[1390]---> BDD-cost:   43
c ---[1386]---> BDD-cost:   29
c ---[1384]---> BDD-cost:   33
c ---[1382]---> BDD-cost:  107
c ---[1380]---> BDD-cost:   57
c ---[1378]---> BDD-cost:  169
c ---[1376]---> BDD-cost:   79
c ---[1374]---> BDD-cost:   81
c ---[1372]---> BDD-cost:  219
c ---[1370]---> BDD-cost:  229
c ---[1368]---> BDD-cost:  111
c ---[1366]---> BDD-cost:    5
c ---[1364]---> BDD-cost:   89
c ---[1362]---> BDD-cost:  389
c ---[1360]---> BDD-cost:  335
c ---[1358]---> BDD-cost:  191
c ---[1356]---> BDD-cost:  121
c ---[1354]---> BDD-cost:  137
c ---[1352]---> BDD-cost:   83
c ---[1350]---> BDD-cost:  199
c ---[1348]---> BDD-cost:   15
c ---[1346]---> BDD-cost:  109
c ---[1344]---> BDD-cost:   55
c ---[1342]---> BDD-cost:  181
c ---[1340]---> BDD-cost:  133
c ---[1338]---> BDD-cost:   81
c ---[1336]---> BDD-cost:   33
c ---[1334]---> BDD-cost:  131
c ---[1332]---> BDD-cost:   75
c ---[1330]---> BDD-cost:   49
c ---[1328]---> BDD-cost:   17
c ---[1326]---> BDD-cost:   97
c ---[1324]---> BDD-cost:  129
c ---[1322]---> BDD-cost:   69
c ---[1320]---> BDD-cost:  273
c ---[1318]---> BDD-cost:  261
c ---[1316]---> BDD-cost:   89
c ---[1314]---> BDD-cost:  119
c ---[1312]---> BDD-cost:   53
c ---[1310]---> BDD-cost:   43
c ---[1308]---> BDD-cost:   61
c ---[1306]---> BDD-cost:   99
c ---[1304]---> BDD-cost:   81
c ---[1302]---> BDD-cost:  165
c ---[1300]---> BDD-cost:  231
c ---[1298]---> BDD-cost:  121
c ---[1296]---> BDD-cost:  135
c ---[1294]---> BDD-cost:  227
c ---[1292]---> BDD-cost:   35
c ---[1290]---> BDD-cost:   55
c ---[1288]---> BDD-cost:  143
c ---[1286]---> BDD-cost:  135
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  177
c ---[1280]---> BDD-cost:  151
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  179
c ---[1274]---> BDD-cost:   61
c ---[1272]---> BDD-cost:  167
c ---[1270]---> BDD-cost:  145
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:  243
c ---[1264]---> BDD-cost:   15
c ---[1262]---> BDD-cost:  137
c ---[1260]---> BDD-cost:   85
c ---[1258]---> BDD-cost:   37
c ---[1254]---> BDD-cost:   43
c ---[1252]---> BDD-cost:   19
c ---[1250]---> BDD-cost:   23
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   91
c ---[1244]---> BDD-cost:   95
c ---[1242]---> BDD-cost:   61
c ---[1240]---> BDD-cost:   79
c ---[1238]---> BDD-cost:   89
c ---[1236]---> BDD-cost:  105
c ---[1234]---> BDD-cost:   97
c ---[1232]---> BDD-cost:  105
c ---[1230]---> BDD-cost:   81
c ---[1228]---> BDD-cost:   19
c ---[1226]---> BDD-cost:   13
c ---[1224]---> BDD-cost:    3
c ---[1222]---> BDD-cost:   21
c ---[1220]---> BDD-cost:   65
c ---[1218]---> BDD-cost:   35
c ---[1216]---> BDD-cost:   69
c ---[1214]---> BDD-cost:   45
c ---[1212]---> BDD-cost:   59
c ---[1210]---> BDD-cost:   89
c ---[1208]---> BDD-cost:   65
c ---[1206]---> BDD-cost:  101
c ---[1204]---> BDD-cost:   87
c ---[1202]---> BDD-cost:   95
c ---[1200]---> BDD-cost:   69
c ---[1198]---> BDD-cost:  119
c ---[1196]---> BDD-cost:   53
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   27
c ---[1190]---> BDD-cost:  273
c ---[1188]---> BDD-cost:  231
c ---[1186]---> BDD-cost:  243
c ---[1184]---> BDD-cost:  121
c ---[1182]---> BDD-cost:  295
c ---[1180]---> BDD-cost:  175
c ---[1178]---> BDD-cost:  115
c ---[1176]---> BDD-cost:  175
c ---[1174]---> BDD-cost:  249
c ---[1172]---> BDD-cost:  233
c ---[1170]---> BDD-cost:  123
c ---[1168]---> BDD-cost:   81
c ---[1166]---> BDD-cost:    5
c ---[1164]---> BDD-cost:   75
c ---[1162]---> BDD-cost:   71
c ---[1160]---> BDD-cost:   39
c ---[1156]---> BDD-cost:   65
c ---[1154]---> BDD-cost:   51
c ---[1152]---> BDD-cost:   21
c ---[1150]---> BDD-cost:   15
c ---[1148]---> BDD-cost:    3
c ---[1146]---> BDD-cost:   21
c ---[1144]---> BDD-cost:   17
c ---[1142]---> BDD-cost:   33
c ---[1140]---> BDD-cost:   11
c ---[1138]---> BDD-cost:   29
c ---[1136]---> BDD-cost:   95
c ---[1134]---> BDD-cost:   79
c ---[1132]---> BDD-cost:   37
c ---[1130]---> BDD-cost:  273
c ---[1128]---> BDD-cost:  221
c ---[1126]---> BDD-cost:  189
c ---[1124]---> BDD-cost:   81
c ---[1122]---> BDD-cost:   35
c ---[1120]---> BDD-cost:  185
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   59
c ---[1114]---> BDD-cost:   59
c ---[1112]---> BDD-cost:  125
c ---[1110]---> BDD-cost:  135
c ---[1108]---> BDD-cost:  117
c ---[1096]---> BDD-cost:   73
c ---[1094]---> BDD-cost:   95
c ---[1092]---> BDD-cost:   53
c ---[1090]---> BDD-cost:  117
c ---[1088]---> BDD-cost:  117
c ---[1086]---> BDD-cost:  199
c ---[1084]---> BDD-cost:  189
c ---[1082]---> BDD-cost:   25
c ---[1080]---> BDD-cost:  173
c ---[1078]---> BDD-cost:   45
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:  219
c ---[1070]---> BDD-cost:  167
c ---[1068]---> BDD-cost:  121
c ---[1066]---> BDD-cost:  203
c ---[1064]---> BDD-cost:   27
c ---[1062]---> BDD-cost:   17
c ---[1060]---> BDD-cost:   87
c ---[1058]---> BDD-cost:  111
c ---[1056]---> BDD-cost:  169
c ---[1054]---> BDD-cost:  251
c ---[1052]---> BDD-cost:  155
c ---[1048]---> BDD-cost:   93
c ---[1044]---> BDD-cost:  141
c ---[1042]---> BDD-cost:  103
c ---[1040]---> BDD-cost:  173
c ---[1038]---> BDD-cost:  221
c ---[1036]---> BDD-cost:  199
c ---[1034]---> BDD-cost:  185
c ---[1032]---> BDD-cost:  259
c ---[1030]---> BDD-cost:  129
c ---[1028]---> BDD-cost:  283
c ---[1026]---> BDD-cost:  187
c ---[1024]---> BDD-cost:  187
c ---[1022]---> BDD-cost:  173
c ---[1018]---> BDD-cost:   55
c ---[1014]---> BDD-cost:   37
c ---[1012]---> BDD-cost:   59
c ---[1010]---> BDD-cost:   57
c ---[1008]---> BDD-cost:   49
c ---[1004]---> BDD-cost:    1
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   91
c ---[ 998]---> BDD-cost:  137
c ---[ 996]---> BDD-cost:   77
c ---[ 994]---> BDD-cost:  125
c ---[ 992]---> BDD-cost:   49
c ---[ 990]---> BDD-cost:  103
c ---[ 988]---> BDD-cost:  119
c ---[ 986]---> BDD-cost:   81
c ---[ 984]---> BDD-cost:  121
c ---[ 982]---> BDD-cost:  127
c ---[ 980]---> BDD-cost:   25
c ---[ 978]---> BDD-cost:  139
c ---[ 976]---> BDD-cost:   73
c ---[ 974]---> BDD-cost:  113
c ---[ 972]---> BDD-cost:   77
c ---[ 970]---> BDD-cost:   69
c ---[ 968]---> BDD-cost:   53
c ---[ 966]---> BDD-cost:   33
c ---[ 962]---> BDD-cost:   65
c ---[ 960]---> BDD-cost:   65
c ---[ 958]---> BDD-cost:  213
c ---[ 956]---> BDD-cost:  247
c ---[ 954]---> BDD-cost:  273
c ---[ 952]---> BDD-cost:  145
c ---[ 950]---> BDD-cost:  535
c ---[ 948]---> BDD-cost:  659
c ---[ 946]---> BDD-cost:  259
c ---[ 944]---> BDD-cost:  213
c ---[ 942]---> BDD-cost:  157
c ---[ 940]---> BDD-cost:   65
c ---[ 938]---> BDD-cost:  561
c ---[ 936]---> BDD-cost:  117
c ---[ 932]---> BDD-cost:  153
c ---[ 930]---> BDD-cost:  113
c ---[ 928]---> BDD-cost:  119
c ---[ 926]---> BDD-cost:   99
c ---[ 922]---> BDD-cost:    6
c ---[ 920]---> BDD-cost:  113
c ---[ 918]---> BDD-cost:   75
c ---[ 914]---> BDD-cost:   17
c ---[ 912]---> BDD-cost:  149
c ---[ 910]---> BDD-cost:   63
c ---[ 908]---> BDD-cost:   41
c ---[ 906]---> BDD-cost:  135
c ---[ 904]---> BDD-cost:   99
c ---[ 902]---> BDD-cost:   99
c ---[ 900]---> BDD-cost:   65
c ---[ 898]---> BDD-cost:  333
c ---[ 896]---> BDD-cost:   93
c ---[ 894]---> BDD-cost:  407
c ---[ 892]---> BDD-cost:  393
c ---[ 890]---> BDD-cost:  349
c ---[ 888]---> BDD-cost:  189
c ---[ 886]---> BDD-cost:  225
c ---[ 884]---> BDD-cost:  115
c ---[ 882]---> BDD-cost:  117
c ---[ 880]---> BDD-cost:   57
c ---[ 878]---> BDD-cost:  109
c ---[ 876]---> BDD-cost:  219
c ---[ 874]---> BDD-cost:  139
c ---[ 872]---> BDD-cost:  239
c ---[ 870]---> BDD-cost:   65
c ---[ 868]---> BDD-cost:   39
c ---[ 866]---> BDD-cost:   59
c ---[ 862]---> BDD-cost:    9
c ---[ 860]---> BDD-cost:  239
c ---[ 858]---> BDD-cost:  165
c ---[ 856]---> BDD-cost:  207
c ---[ 854]---> BDD-cost:  219
c ---[ 852]---> BDD-cost:  391
c ---[ 850]---> BDD-cost:  315
c ---[ 848]---> BDD-cost:  147
c ---[ 846]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:  187
c ---[ 842]---> BDD-cost:  311
c ---[ 840]---> BDD-cost:  187
c ---[ 838]---> BDD-cost:  195
c ---[ 836]---> BDD-cost:  117
c ---[ 834]---> BDD-cost:  111
c ---[ 830]---> BDD-cost:   91
c ---[ 828]---> BDD-cost:  333
c ---[ 826]---> BDD-cost:  207
c ---[ 822]---> BDD-cost:  253
c ---[ 820]---> BDD-cost:   77
c ---[ 818]---> BDD-cost:   77
c ---[ 816]---> BDD-cost:  191
c ---[ 814]---> BDD-cost:  153
c ---[ 812]---> BDD-cost:  255
c ---[ 810]---> BDD-cost:  189
c ---[ 808]---> BDD-cost:   17
c ---[ 806]---> BDD-cost:   39
c ---[ 802]---> BDD-cost:  187
c ---[ 800]---> BDD-cost:  117
c ---[ 798]---> BDD-cost:   49
c ---[ 796]---> BDD-cost:   37
c ---[ 794]---> BDD-cost:   61
c ---[ 792]---> BDD-cost:   33
c ---[ 790]---> BDD-cost:    0
c ---[ 788]---> BDD-cost:   83
c ---[ 786]---> BDD-cost:   73
c ---[ 784]---> BDD-cost:   91
c ---[ 782]---> BDD-cost:   55
c ---[ 780]---> BDD-cost:  105
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  345
c ---[ 774]---> BDD-cost:  295
c ---[ 772]---> BDD-cost:  101
c ---[ 770]---> BDD-cost:   21
c ---[ 768]---> BDD-cost:   71
c ---[ 766]---> BDD-cost:   77
c ---[ 764]---> BDD-cost:   61
c ---[ 762]---> BDD-cost:   53
c ---[ 760]---> BDD-cost:  199
c ---[ 758]---> BDD-cost:  195
c ---[ 756]---> BDD-cost:  155
c ---[ 754]---> BDD-cost:   29
c ---[ 752]---> BDD-cost:   13
c ---[ 750]---> BDD-cost:  133
c ---[ 748]---> BDD-cost:   65
c ---[ 746]---> BDD-cost:   57
c ---[ 744]---> BDD-cost:  157
c ---[ 742]---> BDD-cost:  345
c ---[ 740]---> BDD-cost:  201
c ---[ 738]---> BDD-cost:  205
c ---[ 736]---> BDD-cost:  151
c ---[ 734]---> BDD-cost:  135
c ---[ 732]---> BDD-cost:   73
c ---[ 730]---> BDD-cost:  161
c ---[ 728]---> BDD-cost:  181
c ---[ 726]---> BDD-cost:  177
c ---[ 724]---> BDD-cost:  293
c ---[ 722]---> BDD-cost:  279
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  145
c ---[ 716]---> BDD-cost:  289
c ---[ 714]---> BDD-cost:  163
c ---[ 712]---> BDD-cost:  181
c ---[ 710]---> BDD-cost:  141
c ---[ 708]---> BDD-cost:  115
c ---[ 706]---> BDD-cost:  123
c ---[ 704]---> BDD-cost:  189
c ---[ 702]---> BDD-cost:  139
c ---[ 700]---> BDD-cost:   63
c ---[ 698]---> BDD-cost:  473
c ---[ 696]---> BDD-cost:  429
c ---[ 694]---> BDD-cost:  285
c ---[ 692]---> BDD-cost:    9
c ---[ 690]---> BDD-cost:    5
c ---[ 688]---> BDD-cost:    0
c ---[ 686]---> BDD-cost:    3
c ---[ 684]---> BDD-cost:    4
c ---[ 680]---> BDD-cost:  155
c ---[ 678]---> BDD-cost:  127
c ---[ 676]---> BDD-cost:  109
c ---[ 674]---> BDD-cost:  273
c ---[ 672]---> BDD-cost:   63
c ---[ 670]---> BDD-cost:   45
c ---[ 668]---> BDD-cost:   23
c ---[ 666]---> BDD-cost:   29
c ---[ 664]---> BDD-cost:  245
c ---[ 662]---> BDD-cost:  227
c ---[ 660]---> BDD-cost:   49
c ---[ 658]---> BDD-cost:    9
c ---[ 656]---> BDD-cost:    0
c ---[ 654]---> BDD-cost:  149
c ---[ 652]---> BDD-cost:  183
c ---[ 650]---> BDD-cost:  119
c ---[ 648]---> BDD-cost:  107
c ---[ 646]---> BDD-cost:  235
c ---[ 644]---> BDD-cost:  227
c ---[ 642]---> BDD-cost:  239
c ---[ 640]---> BDD-cost:  269
c ---[ 638]---> BDD-cost:  615
c ---[ 636]---> BDD-cost:  441
c ---[ 634]---> BDD-cost:  231
c ---[ 632]---> BDD-cost:  123
c ---[ 630]---> BDD-cost:  547
c ---[ 628]---> BDD-cost:  543
c ---[ 626]---> BDD-cost:  357
c ---[ 624]---> BDD-cost:  237
c ---[ 620]---> BDD-cost:  327
c ---[ 618]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:  287
c ---[ 614]---> BDD-cost:  205
c ---[ 612]---> BDD-cost:  177
c ---[ 610]---> BDD-cost:  313
c ---[ 608]---> BDD-cost:   57
c ---[ 606]---> BDD-cost:   61
c ---[ 604]---> BDD-cost:   45
c ---[ 602]---> BDD-cost:   35
c ---[ 600]---> BDD-cost:  133
c ---[ 598]---> BDD-cost:  107
c ---[ 596]---> BDD-cost:   91
c ---[ 594]---> BDD-cost:   93
c ---[ 592]---> BDD-cost:   35
c ---[ 590]---> BDD-cost:  187
c ---[ 588]---> BDD-cost:  573
c ---[ 586]---> BDD-cost:  305
c ---[ 584]---> BDD-cost:  607
c ---[ 582]---> BDD-cost:  443
c ---[ 580]---> BDD-cost:  213
c ---[ 578]---> BDD-cost:  213
c ---[ 576]---> BDD-cost:  167
c ---[ 574]---> BDD-cost:    4
c ---[ 572]---> BDD-cost:  283
c ---[ 570]---> BDD-cost:  277
c ---[ 568]---> BDD-cost:  125
c ---[ 566]---> BDD-cost:   85
c ---[ 564]---> BDD-cost:   81
c ---[ 562]---> BDD-cost:  403
c ---[ 560]---> BDD-cost:  391
c ---[ 558]---> BDD-cost:  175
c ---[ 556]---> BDD-cost:  159
c ---[ 554]---> BDD-cost:  155
c ---[ 552]---> BDD-cost:  101
c ---[ 550]---> BDD-cost:  155
c ---[ 548]---> BDD-cost:  165
c ---[ 546]---> BDD-cost:  153
c ---[ 544]---> BDD-cost:  135
c ---[ 542]---> BDD-cost:   81
c ---[ 540]---> BDD-cost:  167
c ---[ 538]---> BDD-cost:   27
c ---[ 536]---> BDD-cost:  147
c ---[ 534]---> BDD-cost:  155
c ---[ 532]---> BDD-cost:  173
c ---[ 530]---> BDD-cost:  267
c ---[ 528]---> BDD-cost:  157
c ---[ 526]---> BDD-cost:   91
c ---[ 524]---> BDD-cost:  259
c ---[ 522]---> BDD-cost:  117
c ---[ 520]---> BDD-cost:  121
c ---[ 518]---> BDD-cost:  323
c ---[ 516]---> BDD-cost:  325
c ---[ 514]---> BDD-cost:  311
c ---[ 512]---> BDD-cost:  313
c ---[ 510]---> BDD-cost:  247
c ---[ 508]---> BDD-cost:  297
c ---[ 506]---> BDD-cost:  211
c ---[ 504]---> BDD-cost:  369
c ---[ 500]---> BDD-cost:  305
c ---[ 498]---> BDD-cost:  341
c ---[ 496]---> BDD-cost:  285
c ---[ 494]---> BDD-cost:   77
c ---[ 492]---> BDD-cost:  317
c ---[ 490]---> BDD-cost:  275
c ---[ 488]---> BDD-cost:  423
c ---[ 486]---> BDD-cost:  403
c ---[ 484]---> BDD-cost:  307
c ---[ 482]---> BDD-cost:  327
c ---[ 480]---> BDD-cost:  307
c ---[ 478]---> BDD-cost:  315
c ---[ 476]---> BDD-cost:  297
c ---[ 474]---> BDD-cost:  273
c ---[ 472]---> BDD-cost:  701
c ---[ 470]---> BDD-cost:  289
c ---[ 468]---> BDD-cost:  245
c ---[ 466]---> BDD-cost:  385
c ---[ 464]---> BDD-cost:  363
c ---[ 462]---> BDD-cost:   27
c ---[ 458]---> BDD-cost:  145
c ---[ 456]---> BDD-cost:  147
c ---[ 454]---> BDD-cost:  149
c ---[ 452]---> BDD-cost:  125
c ---[ 450]---> BDD-cost:  147
c ---[ 448]---> BDD-cost:  111
c ---[ 446]---> BDD-cost:  319
c ---[ 444]---> BDD-cost:  309
c ---[ 438]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:    7
c ---[ 434]---> BDD-cost:  399
c ---[ 432]---> BDD-cost:  401
c ---[ 430]---> BDD-cost:  371
c ---[ 426]---> BDD-cost:   65
c ---[ 422]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:   15
c ---[ 416]---> BDD-cost:  453
c ---[ 414]---> BDD-cost:  457
c ---[ 412]---> BDD-cost:  197
c ---[ 410]---> BDD-cost:  123
c ---[ 408]---> BDD-cost:  165
c ---[ 404]---> BDD-cost:  335
c ---[ 402]---> BDD-cost:  169
c ---[ 400]---> BDD-cost:  209
c ---[ 398]---> BDD-cost:   61
c ---[ 396]---> BDD-cost:   17
c ---[ 394]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:   41
c ---[ 388]---> BDD-cost:  229
c ---[ 386]---> BDD-cost:  231
c ---[ 384]---> BDD-cost:  223
c ---[ 378]---> BDD-cost:  319
c ---[ 376]---> BDD-cost:  223
c ---[ 374]---> BDD-cost:  241
c ---[ 372]---> BDD-cost:  245
c ---[ 370]---> BDD-cost:  229
c ---[ 368]---> BDD-cost:  109
c ---[ 366]---> BDD-cost:   73
c ---[ 364]---> BDD-cost:   85
c ---[ 362]---> BDD-cost:   99
c ---[ 360]---> BDD-cost:  103
c ---[ 358]---> BDD-cost:    5
c ---[ 356]---> BDD-cost:  201
c ---[ 354]---> BDD-cost:  215
c ---[ 352]---> BDD-cost:  197
c ---[ 348]---> BDD-cost:  139
c ---[ 344]---> BDD-cost:   83
c ---[ 340]---> BDD-cost:  125
c ---[ 338]---> BDD-cost:  225
c ---[ 336]---> BDD-cost:  181
c ---[ 334]---> BDD-cost:  151
c ---[ 332]---> BDD-cost:  243
c ---[ 330]---> BDD-cost:  179
c ---[ 328]---> BDD-cost:  207
c ---[ 326]---> BDD-cost:  145
c ---[ 324]---> BDD-cost:   21
c ---[ 322]---> BDD-cost:  235
c ---[ 320]---> BDD-cost:  209
c ---[ 318]---> BDD-cost:   55
c ---[ 316]---> BDD-cost:  223
c ---[ 314]---> BDD-cost:  193
c ---[ 312]---> BDD-cost:  173
c ---[ 310]---> BDD-cost:   63
c ---[ 308]---> BDD-cost:   87
c ---[ 306]---> BDD-cost:   87
c ---[ 304]---> BDD-cost:   33
c ---[ 302]---> BDD-cost:  135
c ---[ 300]---> BDD-cost:   75
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  233
c ---[ 294]---> BDD-cost:  211
c ---[ 292]---> BDD-cost:  119
c ---[ 290]---> BDD-cost:  269
c ---[ 288]---> BDD-cost:   51
c ---[ 286]---> BDD-cost:  205
c ---[ 284]---> BDD-cost:  233
c ---[ 282]---> BDD-cost:  207
c ---[ 280]---> BDD-cost:  243
c ---[ 278]---> BDD-cost:  453
c ---[ 276]---> BDD-cost:  465
c ---[ 274]---> BDD-cost:  259
c ---[ 272]---> BDD-cost:  227
c ---[ 270]---> BDD-cost:  359
c ---[ 268]---> BDD-cost:  209
c ---[ 266]---> BDD-cost:  319
c ---[ 264]---> BDD-cost:  287
c ---[ 262]---> BDD-cost:  225
c ---[ 260]---> BDD-cost:  227
c ---[ 258]---> BDD-cost:  445
c ---[ 256]---> BDD-cost:  339
c ---[ 254]---> BDD-cost:  343
c ---[ 252]---> BDD-cost:  105
c ---[ 250]---> BDD-cost:   73
c ---[ 248]---> BDD-cost:   89
c ---[ 246]---> BDD-cost:  109
c ---[ 242]---> BDD-cost:  597
c ---[ 240]---> BDD-cost:  303
c ---[ 238]---> BDD-cost:  253
c ---[ 236]---> BDD-cost:  133
c ---[ 234]---> BDD-cost:  119
c ---[ 232]---> BDD-cost:   99
c ---[ 230]---> BDD-cost:  119
c ---[ 228]---> BDD-cost:   67
c ---[ 226]---> BDD-cost:  145
c ---[ 224]---> BDD-cost:  135
c ---[ 222]---> BDD-cost:  217
c ---[ 220]---> BDD-cost:  211
c ---[ 218]---> BDD-cost:  141
c ---[ 214]---> BDD-cost:  167
c ---[ 212]---> BDD-cost:  191
c ---[ 210]---> BDD-cost:  125
c ---[ 208]---> BDD-cost:  175
c ---[ 206]---> BDD-cost:  147
c ---[ 204]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:  389
c ---[ 200]---> BDD-cost:  349
c ---[ 198]---> BDD-cost:  151
c ---[ 196]---> BDD-cost:  151
c ---[ 194]---> BDD-cost:  307
c ---[ 192]---> BDD-cost:  355
c ---[ 190]---> BDD-cost:  269
c ---[ 188]---> BDD-cost:  267
c ---[ 186]---> BDD-cost:  327
c ---[ 184]---> BDD-cost:  347
c ---[ 182]---> BDD-cost:  187
c ---[ 180]---> BDD-cost:  117
c ---[ 178]---> BDD-cost:   37
c ---[ 176]---> BDD-cost:   17
c ---[ 174]---> BDD-cost:  171
c ---[ 170]---> BDD-cost:  339
c ---[ 168]---> BDD-cost:  429
c ---[ 166]---> BDD-cost:  443
c ---[ 164]---> BDD-cost:  419
c ---[ 162]---> BDD-cost:  465
c ---[ 160]---> BDD-cost:  379
c ---[ 158]---> BDD-cost:  307
c ---[ 156]---> BDD-cost:  907
c ---[ 154]---> BDD-cost:  439
c ---[ 152]---> BDD-cost:  303
c ---[ 150]---> BDD-cost:  239
c ---[ 148]---> BDD-cost:  219
c ---[ 146]---> BDD-cost:  261
c ---[ 144]---> BDD-cost:  247
c ---[ 142]---> BDD-cost:  265
c ---[ 140]---> BDD-cost:  273
c ---[ 138]---> BDD-cost:  673
c ---[ 136]---> BDD-cost:  433
c ---[ 134]---> BDD-cost:  317
c ---[ 132]---> BDD-cost:  187
c ---[ 130]---> BDD-cost:  199
c ---[ 128]---> BDD-cost:  155
c ---[ 126]---> BDD-cost:  105
c ---[ 124]---> BDD-cost:   31
c ---[ 122]---> BDD-cost:  117
c ---[ 120]---> BDD-cost:  107
c ---[ 118]---> BDD-cost:  141
c ---[ 116]---> BDD-cost:  165
c ---[ 114]---> BDD-cost:  221
c ---[ 110]---> BDD-cost:  163
c ---[ 108]---> BDD-cost:  179
c ---[ 106]---> BDD-cost:  139
c ---[ 104]---> BDD-cost:   83
c ---[ 102]---> BDD-cost:   67
c ---[ 100]---> BDD-cost:   87
c ---[  98]---> BDD-cost:   31
c ---[  96]---> BDD-cost:   23
c ---[  94]---> BDD-cost:   31
c ---[  92]---> BDD-cost:   91
c ---[  90]---> BDD-cost:  431
c ---[  88]---> BDD-cost:  203
c ---[  86]---> BDD-cost:  565
c ---[  84]---> BDD-cost:  611
c ---[  82]---> BDD-cost:  347
c ---[  80]---> BDD-cost:  175
c ---[  78]---> BDD-cost:  525
c ---[  76]---> BDD-cost:  505
c ---[  74]---> BDD-cost:   57
c ---[  72]---> BDD-cost:   45
c ---[  70]---> BDD-cost:   57
c ---[  68]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   55
c ---[  64]---> BDD-cost:   57
c ---[  62]---> BDD-cost:   57
c ---[  60]---> BDD-cost:  159
c ---[  58]---> BDD-cost:   71
c ---[  56]---> BDD-cost:  199
c ---[  54]---> BDD-cost:  191
c ---[  52]---> BDD-cost:  225
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:  509
c ---[  46]---> BDD-cost:  321
c ---[  44]---> BDD-cost:  333
c ---[  42]---> BDD-cost:  407
c ---[  40]---> BDD-cost:  191
c ---[  38]---> BDD-cost:  135
c ---[  36]---> BDD-cost:  379
c ---[  34]---> BDD-cost:  365
c ---[  32]---> BDD-cost:   63
c ---[  30]---> BDD-cost:   31
c ---[  28]---> BDD-cost:   33
c ---[  26]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   31
c ---[  18]---> BDD-cost:   47
c ---[  16]---> BDD-cost:  139
c ---[  14]---> BDD-cost:    9
c ---[  12]---> BDD-cost:  135
c ---[  10]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   53
c ---[   6]---> BDD-cost:  129
c ---[   4]---> BDD-cost:    7
c ---[   2]---> BDD-cost:  119
c ---[   0]---> BDD-cost:   85
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  297923   775365 |   99307       0        0     nan |  0.000 % |
c |       101 |  297806   775070 |  109237     100     2794    27.9 |  0.656 % |
c |       251 |  297804   775064 |  120161     248    14520    58.5 |  0.657 % |
c |       476 |  297507   774267 |  132177     467    22948    49.1 |  0.710 % |
c |       813 |  297152   773365 |  145395     797    35416    44.4 |  0.754 % |
c |      1319 |  296676   772113 |  159934    1277    64842    50.8 |  0.837 % |
c |      2078 |  296505   771647 |  175928    2025   118379    58.5 |  0.874 % |
c |      3217 |  296041   770425 |  193521    3109   207452    66.7 |  0.949 % |
c |      4927 |  295699   769540 |  212873    4779   350269    73.3 |  0.998 % |
c |      7492 |  295396   768750 |  234160    7275   566032    77.8 |  1.037 % |
c |     11337 |  294904   767451 |  257576   10971   954090    87.0 |  1.105 % |
c |     17103 |  294446   766278 |  283334   16577  1527497    92.1 |  1.145 % |
c |     25754 |  293444   763687 |  311667   24858  2532372   101.9 |  1.262 % |
c |     38729 |  292783   762005 |  342834   37493  4503970   120.1 |  1.316 % |
c |     58190 |  291850   759627 |  377118   56625  8594924   151.8 |  1.423 % |
c |     87385 |  291219   758027 |  414829   85473 17541788   205.2 |  1.468 % |
#### 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.62 0.87 0.88 2/54 4650
Raw data (stat): 4650 (runsolver) R 4649 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485873299 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0009 s]
Raw data (loadavg): 0.68 0.87 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 10675 0 0 0 973 25 0 0 25 0 1 0 485873299 45465600 10320 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11100 10320 603 41 0 11059 0
vsize: 44400
[startup+20.0012 s]
Raw data (loadavg): 0.73 0.87 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 10825 0 0 0 1972 25 0 0 25 0 1 0 485873299 46137344 10470 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11264 10470 603 41 0 11223 0
vsize: 45056
[startup+30.0019 s]
Raw data (loadavg): 0.77 0.88 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 11009 0 0 0 2971 27 0 0 25 0 1 0 485873299 46837760 10654 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11435 10654 603 41 0 11394 0
vsize: 45740
[startup+40.002 s]
Raw data (loadavg): 0.81 0.88 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 11161 0 0 0 3971 27 0 0 25 0 1 0 485873299 47513600 10806 4294967295 134512640 134672761 3221224544 3221223792 134562135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11600 10806 603 41 0 11559 0
vsize: 46400
[startup+50.0032 s]
Raw data (loadavg): 0.83 0.89 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 11350 0 0 0 4970 28 0 0 25 0 1 0 485873299 48189440 10995 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11765 10995 603 41 0 11724 0
vsize: 47060
[startup+60.0029 s]
Raw data (loadavg): 0.86 0.89 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 11550 0 0 0 5969 30 0 0 25 0 1 0 485873299 49131520 11195 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11995 11195 603 41 0 11954 0
vsize: 47980
[startup+70.003 s]
Raw data (loadavg): 0.88 0.89 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 11727 0 0 0 6968 30 0 0 25 0 1 0 485873299 49672192 11372 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12127 11372 603 41 0 12086 0
vsize: 48508
[startup+80.0031 s]
Raw data (loadavg): 0.90 0.89 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 11928 0 0 0 7968 31 0 0 25 0 1 0 485873299 50618368 11573 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12358 11573 603 41 0 12317 0
vsize: 49432
[startup+90.0028 s]
Raw data (loadavg): 0.91 0.90 0.88 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 12106 0 0 0 8967 31 0 0 25 0 1 0 485873299 51286016 11751 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12521 11751 603 41 0 12480 0
vsize: 50084
[startup+100.004 s]
Raw data (loadavg): 0.93 0.90 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 12292 0 0 0 9967 32 0 0 25 0 1 0 485873299 52097024 11937 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12719 11937 603 41 0 12678 0
vsize: 50876
[startup+110.004 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 12438 0 0 0 10967 32 0 0 25 0 1 0 485873299 52662272 12083 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12857 12083 603 41 0 12816 0
vsize: 51428
[startup+120.004 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 12654 0 0 0 11966 33 0 0 25 0 1 0 485873299 53608448 12299 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13088 12299 603 41 0 13047 0
vsize: 52352
[startup+130.005 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 12796 0 0 0 12965 35 0 0 25 0 1 0 485873299 54149120 12441 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13220 12441 603 41 0 13179 0
vsize: 52880
[startup+140.005 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 13007 0 0 0 13964 36 0 0 25 0 1 0 485873299 54960128 12652 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13418 12652 603 41 0 13377 0
vsize: 53672
[startup+150.006 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 13188 0 0 0 14963 37 0 0 25 0 1 0 485873299 55771136 12833 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13616 12833 603 41 0 13575 0
vsize: 54464
[startup+160.006 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 13407 0 0 0 15963 37 0 0 25 0 1 0 485873299 56582144 13052 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13814 13052 603 41 0 13773 0
vsize: 55256
[startup+170.005 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 13673 0 0 0 16962 38 0 0 25 0 1 0 485873299 57659392 13318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14077 13318 603 41 0 14036 0
vsize: 56308
[startup+180.006 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 13918 0 0 0 17961 39 0 0 25 0 1 0 485873299 58728448 13563 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14338 13563 603 41 0 14297 0
vsize: 57352
[startup+190.007 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 14081 0 0 0 18961 39 0 0 25 0 1 0 485873299 59404288 13726 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14503 13726 603 41 0 14462 0
vsize: 58012
[startup+200.006 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 14325 0 0 0 19960 41 0 0 25 0 1 0 485873299 60346368 13970 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14733 13970 603 41 0 14692 0
vsize: 58932
[startup+210.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 14523 0 0 0 20958 42 0 0 25 0 1 0 485873299 61149184 14168 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14929 14168 603 41 0 14888 0
vsize: 59716
[startup+220.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 14741 0 0 0 21958 43 0 0 25 0 1 0 485873299 62218240 14386 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15190 14386 603 41 0 15149 0
vsize: 60760
[startup+230.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 14903 0 0 0 22957 44 0 0 25 0 1 0 485873299 62894080 14548 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15355 14548 603 41 0 15314 0
vsize: 61420
[startup+240.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 15162 0 0 0 23956 45 0 0 25 0 1 0 485873299 63836160 14807 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15585 14807 603 41 0 15544 0
vsize: 62340
[startup+250.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 15508 0 0 0 24955 46 0 0 25 0 1 0 485873299 65318912 15153 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15947 15153 603 41 0 15906 0
vsize: 63788
[startup+260.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 15674 0 0 0 25954 47 0 0 25 0 1 0 485873299 65998848 15319 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16113 15319 603 41 0 16072 0
vsize: 64452
[startup+270.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 15918 0 0 0 26954 48 0 0 25 0 1 0 485873299 66940928 15563 4294967295 134512640 134672761 3221224544 3221223720 134559059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16343 15563 603 41 0 16302 0
vsize: 65372
[startup+280.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 16100 0 0 0 27953 48 0 0 25 0 1 0 485873299 67743744 15745 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16539 15745 603 41 0 16498 0
vsize: 66156
[startup+290.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 16346 0 0 0 28952 49 0 0 25 0 1 0 485873299 68694016 15991 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16771 15991 603 41 0 16730 0
vsize: 67084
[startup+300.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 16575 0 0 0 29952 50 0 0 25 0 1 0 485873299 69640192 16220 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17002 16220 603 41 0 16961 0
vsize: 68008
[startup+310.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 16868 0 0 0 30951 51 0 0 25 0 1 0 485873299 70860800 16513 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17300 16513 603 41 0 17259 0
vsize: 69200
[startup+320.006 s]
Raw data (loadavg): 0.99 0.94 0.91 3/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 17124 0 0 0 31950 52 0 0 25 0 1 0 485873299 71942144 16769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17564 16769 603 41 0 17523 0
vsize: 70256
[startup+330.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 17397 0 0 0 32949 53 0 0 25 0 1 0 485873299 73027584 17042 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17829 17042 603 41 0 17788 0
vsize: 71316
[startup+340.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 17645 0 0 0 33948 54 0 0 25 0 1 0 485873299 73965568 17290 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18058 17290 603 41 0 18017 0
vsize: 72232
[startup+350.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 17880 0 0 0 34948 54 0 0 25 0 1 0 485873299 75038720 17525 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18320 17525 603 41 0 18279 0
vsize: 73280
[startup+360.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 18097 0 0 0 35948 55 0 0 25 0 1 0 485873299 75849728 17742 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18518 17742 603 41 0 18477 0
vsize: 74072
[startup+370.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 18322 0 0 0 36947 56 0 0 25 0 1 0 485873299 76795904 17967 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18749 17967 603 41 0 18708 0
vsize: 74996
[startup+380.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 18702 0 0 0 37946 56 0 0 25 0 1 0 485873299 78278656 18347 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19111 18347 603 41 0 19070 0
vsize: 76444
[startup+390.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 18958 0 0 0 38946 57 0 0 25 0 1 0 485873299 79360000 18603 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19375 18603 603 41 0 19334 0
vsize: 77500
[startup+400.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 19215 0 0 0 39945 58 0 0 25 0 1 0 485873299 80441344 18860 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19639 18860 603 41 0 19598 0
vsize: 78556
[startup+410.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 19422 0 0 0 40945 59 0 0 25 0 1 0 485873299 81248256 19067 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19836 19067 603 41 0 19795 0
vsize: 79344
[startup+420.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 19636 0 0 0 41944 59 0 0 25 0 1 0 485873299 82190336 19281 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20066 19281 603 41 0 20025 0
vsize: 80264
[startup+430.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 19886 0 0 0 42944 60 0 0 25 0 1 0 485873299 83128320 19531 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20295 19531 603 41 0 20254 0
vsize: 81180
[startup+440.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 20246 0 0 0 43943 61 0 0 25 0 1 0 485873299 84611072 19891 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20657 19891 603 41 0 20616 0
vsize: 82628
[startup+450.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 20539 0 0 0 44941 62 0 0 25 0 1 0 485873299 85831680 20184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20955 20184 603 41 0 20914 0
vsize: 83820
[startup+460.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 20798 0 0 0 45940 63 0 0 25 0 1 0 485873299 86913024 20443 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21219 20443 603 41 0 21178 0
vsize: 84876
[startup+470.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 21039 0 0 0 46939 64 0 0 25 0 1 0 485873299 87871488 20684 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21453 20684 603 41 0 21412 0
vsize: 85812
[startup+480.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 21264 0 0 0 47938 65 0 0 25 0 1 0 485873299 88805376 20909 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21681 20909 603 41 0 21640 0
vsize: 86724
[startup+490.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 21500 0 0 0 48937 66 0 0 25 0 1 0 485873299 89751552 21145 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21912 21145 603 41 0 21871 0
vsize: 87648
[startup+500.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 21770 0 0 0 49937 66 0 0 25 0 1 0 485873299 90836992 21415 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22177 21415 603 41 0 22136 0
vsize: 88708
[startup+510.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 21965 0 0 0 50936 67 0 0 25 0 1 0 485873299 91648000 21610 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22375 21610 603 41 0 22334 0
vsize: 89500
[startup+520.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 22218 0 0 0 51936 68 0 0 25 0 1 0 485873299 92733440 21863 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22640 21863 603 41 0 22599 0
vsize: 90560
[startup+530.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 22419 0 0 0 52935 68 0 0 25 0 1 0 485873299 93794304 22064 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22899 22064 603 41 0 22858 0
vsize: 91596
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 22643 0 0 0 53935 69 0 0 25 0 1 0 485873299 94740480 22288 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23130 22288 603 41 0 23089 0
vsize: 92520
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 22928 0 0 0 54934 69 0 0 25 0 1 0 485873299 95801344 22573 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23389 22573 603 41 0 23348 0
vsize: 93556
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 23261 0 0 0 55934 70 0 0 25 0 1 0 485873299 97148928 22906 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23718 22906 603 41 0 23677 0
vsize: 94872
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 23435 0 0 0 56934 70 0 0 25 0 1 0 485873299 97947648 23080 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23913 23080 603 41 0 23872 0
vsize: 95652
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 23731 0 0 0 57934 71 0 0 25 0 1 0 485873299 99168256 23376 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24211 23376 603 41 0 24170 0
vsize: 96844
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 24039 0 0 0 58933 71 0 0 25 0 1 0 485873299 100388864 23684 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24509 23684 603 41 0 24468 0
vsize: 98036
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 24323 0 0 0 59933 72 0 0 25 0 1 0 485873299 101601280 23968 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24805 23968 603 41 0 24764 0
vsize: 99220
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 24626 0 0 0 60932 73 0 0 25 0 1 0 485873299 102805504 24271 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25099 24271 603 41 0 25058 0
vsize: 100396
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 24958 0 0 0 61931 74 0 0 25 0 1 0 485873299 104140800 24603 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25425 24603 603 41 0 25384 0
vsize: 101700
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 25322 0 0 0 62930 75 0 0 25 0 1 0 485873299 105652224 24967 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25794 24967 603 41 0 25753 0
vsize: 103176
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 25700 0 0 0 63929 76 0 0 25 0 1 0 485873299 107126784 25345 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26154 25345 603 41 0 26113 0
vsize: 104616
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 26034 0 0 0 64929 76 0 0 25 0 1 0 485873299 108470272 25679 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26482 25679 603 41 0 26441 0
vsize: 105928
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 26324 0 0 0 65929 77 0 0 25 0 1 0 485873299 109678592 25969 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26777 25969 603 41 0 26736 0
vsize: 107108
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 26638 0 0 0 66928 78 0 0 25 0 1 0 485873299 111022080 26283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27105 26283 603 41 0 27064 0
vsize: 108420
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 26961 0 0 0 67928 78 0 0 25 0 1 0 485873299 112373760 26606 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26606 603 41 0 27394 0
vsize: 109740
[startup+690.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 27291 0 0 0 68927 79 0 0 25 0 1 0 485873299 113606656 26936 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27736 26936 603 41 0 27695 0
vsize: 110944
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 27530 0 0 0 69926 80 0 0 25 0 1 0 485873299 114692096 27175 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28001 27175 603 41 0 27960 0
vsize: 112004
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 27749 0 0 0 70926 81 0 0 25 0 1 0 485873299 115503104 27394 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28199 27394 603 41 0 28158 0
vsize: 112796
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 28087 0 0 0 71925 82 0 0 25 0 1 0 485873299 116977664 27732 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28559 27732 603 41 0 28518 0
vsize: 114236
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 28394 0 0 0 72924 83 0 0 25 0 1 0 485873299 118185984 28039 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28854 28039 603 41 0 28813 0
vsize: 115416
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 28661 0 0 0 73924 83 0 0 25 0 1 0 485873299 119267328 28306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29118 28306 603 41 0 29077 0
vsize: 116472
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 28972 0 0 0 74923 84 0 0 25 0 1 0 485873299 120492032 28617 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29417 28617 603 41 0 29376 0
vsize: 117668
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 29224 0 0 0 75923 85 0 0 25 0 1 0 485873299 121569280 28869 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29680 28869 603 41 0 29639 0
vsize: 118720
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 29473 0 0 0 76922 86 0 0 25 0 1 0 485873299 122523648 29118 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29913 29118 603 41 0 29872 0
vsize: 119652
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 29800 0 0 0 77923 86 0 0 25 0 1 0 485873299 123867136 29445 4294967295 134512640 134672761 3221224544 3221223648 134560180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30241 29445 603 41 0 30200 0
vsize: 120964
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 30115 0 0 0 78923 86 0 0 25 0 1 0 485873299 125218816 29760 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30571 29760 603 41 0 30530 0
vsize: 122284
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 30551 0 0 0 79922 88 0 0 25 0 1 0 485873299 126947328 30196 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30993 30196 603 41 0 30952 0
vsize: 123972
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 30761 0 0 0 80921 88 0 0 25 0 1 0 485873299 127885312 30406 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31222 30406 603 41 0 31181 0
vsize: 124888
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 31017 0 0 0 81921 89 0 0 25 0 1 0 485873299 128831488 30662 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31453 30662 603 41 0 31412 0
vsize: 125812
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 31259 0 0 0 82921 89 0 0 25 0 1 0 485873299 129908736 30904 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31716 30904 603 41 0 31675 0
vsize: 126864
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 31598 0 0 0 83920 90 0 0 25 0 1 0 485873299 131256320 31243 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32045 31243 603 41 0 32004 0
vsize: 128180
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 31949 0 0 0 84919 91 0 0 25 0 1 0 485873299 132714496 31594 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32401 31594 603 41 0 32360 0
vsize: 129604
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 32223 0 0 0 85918 92 0 0 25 0 1 0 485873299 133791744 31868 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32664 31868 603 41 0 32623 0
vsize: 130656
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 32500 0 0 0 86917 93 0 0 25 0 1 0 485873299 134864896 32145 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32926 32145 603 41 0 32885 0
vsize: 131704
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 32774 0 0 0 87917 94 0 0 25 0 1 0 485873299 136065024 32419 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33219 32419 603 41 0 33178 0
vsize: 132876
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 33085 0 0 0 88916 94 0 0 25 0 1 0 485873299 137293824 32730 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33519 32730 603 41 0 33478 0
vsize: 134076
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 33320 0 0 0 89916 95 0 0 25 0 1 0 485873299 138219520 32965 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33745 32965 603 41 0 33704 0
vsize: 134980
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 33510 0 0 0 90915 96 0 0 25 0 1 0 485873299 139034624 33155 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33944 33155 603 41 0 33903 0
vsize: 135776
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 33804 0 0 0 91915 96 0 0 25 0 1 0 485873299 140247040 33449 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34240 33449 603 41 0 34199 0
vsize: 136960
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 34180 0 0 0 92913 98 0 0 25 0 1 0 485873299 141729792 33825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34602 33825 603 41 0 34561 0
vsize: 138408
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 34471 0 0 0 93912 99 0 0 25 0 1 0 485873299 142934016 34116 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34896 34116 603 41 0 34855 0
vsize: 139584
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 34856 0 0 0 94911 100 0 0 25 0 1 0 485873299 144543744 34501 4294967295 134512640 134672761 3221224544 3221223648 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35289 34501 603 41 0 35248 0
vsize: 141156
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 35285 0 0 0 95910 102 0 0 25 0 1 0 485873299 146309120 34930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35720 34930 603 41 0 35679 0
vsize: 142880
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 35523 0 0 0 96910 102 0 0 25 0 1 0 485873299 147247104 35168 4294967295 134512640 134672761 3221224544 3221223680 134560658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35949 35168 603 41 0 35908 0
vsize: 143796
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 35767 0 0 0 97910 103 0 0 25 0 1 0 485873299 148189184 35412 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36179 35412 603 41 0 36138 0
vsize: 144716
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 35970 0 0 0 98909 103 0 0 25 0 1 0 485873299 149139456 35615 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36411 35615 603 41 0 36370 0
vsize: 145644
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4650
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 36136 0 0 0 99909 104 0 0 25 0 1 0 485873299 149815296 35781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36576 35781 603 41 0 36535 0
vsize: 146304
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4703
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 36373 0 0 0 100902 109 0 0 25 0 1 0 485873299 150757376 36018 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36806 36018 603 41 0 36765 0
vsize: 147224
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4703
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 36649 0 0 0 101901 110 0 0 25 0 1 0 485873299 151818240 36294 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37065 36294 603 41 0 37024 0
vsize: 148260
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4703
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 37005 0 0 0 102900 111 0 0 25 0 1 0 485873299 153288704 36650 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37424 36650 603 41 0 37383 0
vsize: 149696
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4703
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 37152 0 0 0 103900 112 0 0 25 0 1 0 485873299 153829376 36797 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37556 36797 603 41 0 37515 0
vsize: 150224
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4703
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 37404 0 0 0 104899 113 0 0 25 0 1 0 485873299 154910720 37049 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37820 37049 603 41 0 37779 0
vsize: 151280
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4703
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 37666 0 0 0 105899 113 0 0 25 0 1 0 485873299 155979776 37311 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38081 37311 603 41 0 38040 0
vsize: 152324
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4703
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 37956 0 0 0 106898 114 0 0 25 0 1 0 485873299 157196288 37601 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38378 37601 603 41 0 38337 0
vsize: 153512
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 38208 0 0 0 107898 115 0 0 25 0 1 0 485873299 158150656 37853 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38611 37853 603 41 0 38570 0
vsize: 154444
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 38450 0 0 0 108898 115 0 0 25 0 1 0 485873299 159100928 38095 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38843 38095 603 41 0 38802 0
vsize: 155372
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 38778 0 0 0 109896 117 0 0 25 0 1 0 485873299 160464896 38423 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39176 38423 603 41 0 39135 0
vsize: 156704
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 39085 0 0 0 110895 118 0 0 25 0 1 0 485873299 161820672 38730 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39507 38730 603 41 0 39466 0
vsize: 158028
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 39475 0 0 0 111894 119 0 0 25 0 1 0 485873299 163303424 39120 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39869 39120 603 41 0 39828 0
vsize: 159476
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 39834 0 0 0 112894 119 0 0 25 0 1 0 485873299 164835328 39479 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40243 39479 603 41 0 40202 0
vsize: 160972
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 40121 0 0 0 113893 120 0 0 25 0 1 0 485873299 166060032 39766 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40542 39766 603 41 0 40501 0
vsize: 162168
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 40377 0 0 0 114893 121 0 0 25 0 1 0 485873299 167137280 40022 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40805 40022 603 41 0 40764 0
vsize: 163220
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 40582 0 0 0 115892 122 0 0 25 0 1 0 485873299 167940096 40227 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41001 40227 603 41 0 40960 0
vsize: 164004
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 40884 0 0 0 116891 123 0 0 25 0 1 0 485873299 169156608 40529 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41298 40529 603 41 0 41257 0
vsize: 165192
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 41031 0 0 0 117891 123 0 0 25 0 1 0 485873299 169828352 40676 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41462 40676 603 41 0 41421 0
vsize: 165848
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 41264 0 0 0 118890 124 0 0 25 0 1 0 485873299 170762240 40909 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41690 40909 603 41 0 41649 0
vsize: 166760
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4705
Raw data (stat): 4650 (minisat+) R 4649 30701 30700 0 -1 0 41582 0 0 0 119889 125 0 0 25 0 1 0 485873299 172085248 41227 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42013 41227 603 41 0 41972 0
vsize: 168052
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4705
Raw data (stat): 4650 (minisat+) Z 4649 30701 30700 0 -1 12 41584 0 0 0 119889 133 0 0 25 0 1 0 485873299 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.1
CPU time (s): 1200.23
CPU user time (s): 1198.9
CPU system time (s): 1.3348
CPU usage (%): 100.011
Max. virtual memory (Kb): 168052
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####