PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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	1175.81
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 15786

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 05:47:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16678 boxname=wulflinc23 idbench=1283 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f85d0079133f298b06c25764b03ff228  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-air06.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-air06.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-air06.opb
IDLAUNCH: 16678
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        621520 kB
Buffers:         24608 kB
Cached:         358800 kB
SwapCached:        520 kB
Active:          63108 kB
Inactive:       322432 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        621268 kB
SwapTotal:     2097136 kB
SwapFree:      2095824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            21920 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:07:29 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 16678 7 1200.3 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.73 0.91 0.90 2/54 29839
Raw data (stat): 29839 (runsolver) R 29838 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542674276 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0007 s]
Raw data (loadavg): 0.77 0.91 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 10675 0 0 0 972 26 0 0 25 0 1 0 542674276 45465600 10320 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11100 10320 603 41 0 11059 0
vsize: 44400
[startup+20.0009 s]
Raw data (loadavg): 0.80 0.91 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 10824 0 0 0 1971 27 0 0 25 0 1 0 542674276 46137344 10469 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11264 10469 603 41 0 11223 0
vsize: 45056
[startup+30.0011 s]
Raw data (loadavg): 0.83 0.91 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 10999 0 0 0 2970 27 0 0 25 0 1 0 542674276 46837760 10644 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11435 10644 603 41 0 11394 0
vsize: 45740
[startup+40.0016 s]
Raw data (loadavg): 0.86 0.92 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 11152 0 0 0 3969 28 0 0 25 0 1 0 542674276 47378432 10797 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11567 10797 603 41 0 11526 0
vsize: 46268
[startup+50.0018 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 11329 0 0 0 4969 29 0 0 25 0 1 0 542674276 48189440 10974 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11765 10974 603 41 0 11724 0
vsize: 47060
[startup+60.0028 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 11519 0 0 0 5968 30 0 0 25 0 1 0 542674276 48996352 11164 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11962 11164 603 41 0 11921 0
vsize: 47848
[startup+70.0035 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 11704 0 0 0 6968 30 0 0 25 0 1 0 542674276 49672192 11349 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12127 11349 603 41 0 12086 0
vsize: 48508
[startup+80.0037 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 11915 0 0 0 7967 31 0 0 25 0 1 0 542674276 50483200 11560 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12325 11560 603 41 0 12284 0
vsize: 49300
[startup+90.0048 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 12073 0 0 0 8966 32 0 0 25 0 1 0 542674276 51150848 11718 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12488 11718 603 41 0 12447 0
vsize: 49952
[startup+100.005 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 12260 0 0 0 9966 33 0 0 25 0 1 0 542674276 51961856 11905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12686 11905 603 41 0 12645 0
vsize: 50744
[startup+110.006 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 12395 0 0 0 10965 34 0 0 25 0 1 0 542674276 52527104 12040 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12824 12040 603 41 0 12783 0
vsize: 51296
[startup+120.007 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 12613 0 0 0 11964 34 0 0 25 0 1 0 542674276 53338112 12258 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13022 12258 603 41 0 12981 0
vsize: 52088
[startup+130.006 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 12747 0 0 0 12964 35 0 0 25 0 1 0 542674276 53878784 12392 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13154 12392 603 41 0 13113 0
vsize: 52616
[startup+140.007 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 12950 0 0 0 13963 36 0 0 25 0 1 0 542674276 54829056 12595 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13386 12595 603 41 0 13345 0
vsize: 53544
[startup+150.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 13114 0 0 0 14962 37 0 0 25 0 1 0 542674276 55500800 12759 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13550 12759 603 41 0 13509 0
vsize: 54200
[startup+160.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 13321 0 0 0 15961 37 0 0 25 0 1 0 542674276 56311808 12966 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13748 12966 603 41 0 13707 0
vsize: 54992
[startup+170.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 13559 0 0 0 16961 39 0 0 25 0 1 0 542674276 57253888 13204 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13978 13204 603 41 0 13937 0
vsize: 55912
[startup+180.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 13823 0 0 0 17959 40 0 0 25 0 1 0 542674276 58327040 13468 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14240 13468 603 41 0 14199 0
vsize: 56960
[startup+190.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 13989 0 0 0 18959 41 0 0 25 0 1 0 542674276 58998784 13634 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14404 13634 603 41 0 14363 0
vsize: 57616
[startup+200.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 14226 0 0 0 19958 41 0 0 25 0 1 0 542674276 59944960 13871 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14635 13871 603 41 0 14594 0
vsize: 58540
[startup+210.011 s]
Raw data (loadavg): 1.07 0.96 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 14446 0 0 0 20957 42 0 0 25 0 1 0 542674276 60887040 14091 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14865 14091 603 41 0 14824 0
vsize: 59460
[startup+220.011 s]
Raw data (loadavg): 1.06 0.96 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 14643 0 0 0 21956 43 0 0 25 0 1 0 542674276 61685760 14288 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15060 14288 603 41 0 15019 0
vsize: 60240
[startup+230.011 s]
Raw data (loadavg): 1.05 0.96 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 14804 0 0 0 22956 44 0 0 25 0 1 0 542674276 62488576 14449 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15256 14449 603 41 0 15215 0
vsize: 61024
[startup+240.011 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 15023 0 0 0 23955 44 0 0 25 0 1 0 542674276 63295488 14668 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15453 14668 603 41 0 15412 0
vsize: 61812
[startup+250.011 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 15336 0 0 0 24955 45 0 0 25 0 1 0 542674276 64651264 14981 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15784 14981 603 41 0 15743 0
vsize: 63136
[startup+260.012 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 15579 0 0 0 25954 46 0 0 25 0 1 0 542674276 65593344 15224 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16014 15224 603 41 0 15973 0
vsize: 64056
[startup+270.012 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 15750 0 0 0 26953 47 0 0 25 0 1 0 542674276 66269184 15395 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16179 15395 603 41 0 16138 0
vsize: 64716
[startup+280.012 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 15985 0 0 0 27952 48 0 0 25 0 1 0 542674276 67207168 15630 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16408 15630 603 41 0 16367 0
vsize: 65632
[startup+290.013 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 16189 0 0 0 28951 49 0 0 25 0 1 0 542674276 68153344 15834 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16639 15834 603 41 0 16598 0
vsize: 66556
[startup+300.013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 16428 0 0 0 29951 50 0 0 25 0 1 0 542674276 69099520 16073 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 16073 603 41 0 16829 0
vsize: 67480
[startup+310.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 16647 0 0 0 30950 51 0 0 25 0 1 0 542674276 69906432 16292 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17067 16292 603 41 0 17026 0
vsize: 68268
[startup+320.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 16945 0 0 0 31949 52 0 0 25 0 1 0 542674276 71135232 16590 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17367 16590 603 41 0 17326 0
vsize: 69468
[startup+330.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 17203 0 0 0 32948 54 0 0 25 0 1 0 542674276 72212480 16848 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17630 16848 603 41 0 17589 0
vsize: 70520
[startup+340.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 17451 0 0 0 33947 54 0 0 25 0 1 0 542674276 73297920 17096 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17895 17096 603 41 0 17854 0
vsize: 71580
[startup+350.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 17694 0 0 0 34946 55 0 0 25 0 1 0 542674276 74235904 17339 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18124 17339 603 41 0 18083 0
vsize: 72496
[startup+360.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 17922 0 0 0 35946 56 0 0 25 0 1 0 542674276 75173888 17567 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18353 17567 603 41 0 18312 0
vsize: 73412
[startup+370.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 18127 0 0 0 36945 56 0 0 25 0 1 0 542674276 75984896 17772 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18551 17772 603 41 0 18510 0
vsize: 74204
[startup+380.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 18367 0 0 0 37945 57 0 0 25 0 1 0 542674276 76931072 18012 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18782 18012 603 41 0 18741 0
vsize: 75128
[startup+390.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 18742 0 0 0 38944 58 0 0 25 0 1 0 542674276 78548992 18387 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19177 18387 603 41 0 19136 0
vsize: 76708
[startup+400.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 18993 0 0 0 39943 59 0 0 25 0 1 0 542674276 79495168 18638 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19408 18638 603 41 0 19367 0
vsize: 77632
[startup+410.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 19231 0 0 0 40943 59 0 0 25 0 1 0 542674276 80441344 18876 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19639 18876 603 41 0 19598 0
vsize: 78556
[startup+420.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 19433 0 0 0 41943 60 0 0 25 0 1 0 542674276 81383424 19078 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19869 19078 603 41 0 19828 0
vsize: 79476
[startup+430.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 19645 0 0 0 42942 61 0 0 25 0 1 0 542674276 82190336 19290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20066 19290 603 41 0 20025 0
vsize: 80264
[startup+440.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 19890 0 0 0 43942 62 0 0 25 0 1 0 542674276 83128320 19535 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20295 19535 603 41 0 20254 0
vsize: 81180
[startup+450.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 20243 0 0 0 44940 63 0 0 25 0 1 0 542674276 84611072 19888 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20657 19888 603 41 0 20616 0
vsize: 82628
[startup+460.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 20533 0 0 0 45940 63 0 0 25 0 1 0 542674276 85831680 20178 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20955 20178 603 41 0 20914 0
vsize: 83820
[startup+470.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 20774 0 0 0 46939 64 0 0 25 0 1 0 542674276 86777856 20419 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21186 20419 603 41 0 21145 0
vsize: 84744
[startup+480.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 21006 0 0 0 47938 65 0 0 25 0 1 0 542674276 87732224 20651 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21419 20651 603 41 0 21378 0
vsize: 85676
[startup+490.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 21230 0 0 0 48938 66 0 0 25 0 1 0 542674276 88670208 20875 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21648 20875 603 41 0 21607 0
vsize: 86592
[startup+500.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 21451 0 0 0 49938 66 0 0 25 0 1 0 542674276 89616384 21096 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21879 21096 603 41 0 21838 0
vsize: 87516
[startup+510.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 21720 0 0 0 50936 68 0 0 25 0 1 0 542674276 90701824 21365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22144 21365 603 41 0 22103 0
vsize: 88576
[startup+520.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 21936 0 0 0 51935 69 0 0 25 0 1 0 542674276 91512832 21581 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22342 21581 603 41 0 22301 0
vsize: 89368
[startup+530.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 22158 0 0 0 52935 70 0 0 25 0 1 0 542674276 92463104 21803 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22574 21803 603 41 0 22533 0
vsize: 90296
[startup+540.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 22372 0 0 0 53934 70 0 0 25 0 1 0 542674276 93532160 22017 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22835 22017 603 41 0 22794 0
vsize: 91340
[startup+550.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 22576 0 0 0 54934 71 0 0 25 0 1 0 542674276 94470144 22221 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23064 22221 603 41 0 23023 0
vsize: 92256
[startup+560.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 22845 0 0 0 55933 72 0 0 25 0 1 0 542674276 95547392 22490 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23327 22490 603 41 0 23286 0
vsize: 93308
[startup+570.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 23137 0 0 0 56932 73 0 0 25 0 1 0 542674276 96743424 22782 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23619 22782 603 41 0 23578 0
vsize: 94476
[startup+580.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 23373 0 0 0 57931 74 0 0 25 0 1 0 542674276 97685504 23018 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23849 23018 603 41 0 23808 0
vsize: 95396
[startup+590.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 23623 0 0 0 58930 75 0 0 25 0 1 0 542674276 98623488 23268 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24078 23268 603 41 0 24037 0
vsize: 96312
[startup+600.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 23930 0 0 0 59930 76 0 0 25 0 1 0 542674276 99979264 23575 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24409 23575 603 41 0 24368 0
vsize: 97636
[startup+610.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 24212 0 0 0 60930 76 0 0 25 0 1 0 542674276 101060608 23857 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24673 23857 603 41 0 24632 0
vsize: 98692
[startup+620.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 24483 0 0 0 61929 77 0 0 25 0 1 0 542674276 102277120 24128 4294967295 134512640 134672761 3221224544 3221223648 134559814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24970 24128 603 41 0 24929 0
vsize: 99880
[startup+630.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 24813 0 0 0 62928 78 0 0 25 0 1 0 542674276 103477248 24458 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25263 24458 603 41 0 25222 0
vsize: 101052
[startup+640.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 25190 0 0 0 63928 79 0 0 25 0 1 0 542674276 105099264 24835 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25659 24835 603 41 0 25618 0
vsize: 102636
[startup+650.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 25535 0 0 0 64927 80 0 0 25 0 1 0 542674276 106459136 25180 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25991 25180 603 41 0 25950 0
vsize: 103964
[startup+660.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 25843 0 0 0 65926 80 0 0 25 0 1 0 542674276 107802624 25488 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26319 25488 603 41 0 26278 0
vsize: 105276
[startup+670.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 26146 0 0 0 66926 81 0 0 25 0 1 0 542674276 109010944 25791 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26614 25791 603 41 0 26573 0
vsize: 106456
[startup+680.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 26469 0 0 0 67925 82 0 0 25 0 1 0 542674276 110346240 26114 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26940 26114 603 41 0 26899 0
vsize: 107760
[startup+690.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 26818 0 0 0 68924 83 0 0 25 0 1 0 542674276 111697920 26463 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27270 26463 603 41 0 27229 0
vsize: 109080
[startup+700.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 27078 0 0 0 69924 84 0 0 25 0 1 0 542674276 112783360 26723 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27535 26723 603 41 0 27494 0
vsize: 110140
[startup+710.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 27400 0 0 0 70924 84 0 0 25 0 1 0 542674276 114147328 27045 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27868 27045 603 41 0 27827 0
vsize: 111472
[startup+720.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 27581 0 0 0 71923 85 0 0 25 0 1 0 542674276 114827264 27226 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28034 27226 603 41 0 27993 0
vsize: 112136
[startup+730.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 27884 0 0 0 72923 85 0 0 25 0 1 0 542674276 116035584 27529 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28329 27529 603 41 0 28288 0
vsize: 113316
[startup+740.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 28229 0 0 0 73922 87 0 0 25 0 1 0 542674276 117514240 27874 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28690 27874 603 41 0 28649 0
vsize: 114760
[startup+750.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29839
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 28467 0 0 0 74921 87 0 0 25 0 1 0 542674276 118452224 28112 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28919 28112 603 41 0 28878 0
vsize: 115676
[startup+760.018 s]
Raw data (loadavg): 1.00 0.97 0.91 3/57 29878
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 28754 0 0 0 75918 90 0 0 25 0 1 0 542674276 119676928 28399 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29218 28399 603 41 0 29177 0
vsize: 116872
[startup+770.079 s]
Raw data (loadavg): 1.08 0.99 0.92 3/58 29892
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 29039 0 0 0 76924 91 0 0 25 0 1 0 542674276 120762368 28684 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29483 28684 603 41 0 29442 0
vsize: 117932
[startup+780.079 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 29892
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 29267 0 0 0 77923 92 0 0 25 0 1 0 542674276 121708544 28912 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29714 28912 603 41 0 29673 0
vsize: 118856
[startup+790.08 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 29892
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 29554 0 0 0 78922 93 0 0 25 0 1 0 542674276 122929152 29199 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30012 29199 603 41 0 29971 0
vsize: 120048
[startup+800.088 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 29892
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 29830 0 0 0 79922 94 0 0 25 0 1 0 542674276 124006400 29475 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30275 29475 603 41 0 30234 0
vsize: 121100
[startup+810.088 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 29892
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 30212 0 0 0 80921 95 0 0 25 0 1 0 542674276 125628416 29857 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30671 29857 603 41 0 30630 0
vsize: 122684
[startup+820.09 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 29892
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 30610 0 0 0 81920 96 0 0 25 0 1 0 542674276 127217664 30255 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31059 30255 603 41 0 31018 0
vsize: 124236
[startup+830.09 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 29892
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 30813 0 0 0 82919 97 0 0 25 0 1 0 542674276 128020480 30458 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31255 30458 603 41 0 31214 0
vsize: 125020
[startup+840.091 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 31046 0 0 0 83918 98 0 0 25 0 1 0 542674276 128966656 30691 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31486 30691 603 41 0 31445 0
vsize: 125944
[startup+850.091 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 31297 0 0 0 84918 99 0 0 25 0 1 0 542674276 130043904 30942 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31749 30942 603 41 0 31708 0
vsize: 126996
[startup+860.092 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 31664 0 0 0 85917 99 0 0 25 0 1 0 542674276 131530752 31309 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32112 31309 603 41 0 32071 0
vsize: 128448
[startup+870.092 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 31970 0 0 0 86916 100 0 0 25 0 1 0 542674276 132714496 31615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32401 31615 603 41 0 32360 0
vsize: 129604
[startup+880.091 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 32251 0 0 0 87916 101 0 0 25 0 1 0 542674276 133918720 31896 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32695 31896 603 41 0 32654 0
vsize: 130780
[startup+890.092 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 32535 0 0 0 88915 102 0 0 25 0 1 0 542674276 135000064 32180 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32959 32180 603 41 0 32918 0
vsize: 131836
[startup+900.093 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 32802 0 0 0 89914 103 0 0 25 0 1 0 542674276 136200192 32447 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33252 32447 603 41 0 33211 0
vsize: 133008
[startup+910.093 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 33093 0 0 0 90914 104 0 0 25 0 1 0 542674276 137293824 32738 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33519 32738 603 41 0 33478 0
vsize: 134076
[startup+920.093 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 33354 0 0 0 91913 104 0 0 25 0 1 0 542674276 138354688 32999 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33778 32999 603 41 0 33737 0
vsize: 135112
[startup+930.094 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 33523 0 0 0 92913 105 0 0 25 0 1 0 542674276 139034624 33168 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33944 33168 603 41 0 33903 0
vsize: 135776
[startup+940.094 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 33839 0 0 0 93912 105 0 0 25 0 1 0 542674276 140382208 33484 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34273 33484 603 41 0 34232 0
vsize: 137092
[startup+950.095 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 34197 0 0 0 94911 107 0 0 25 0 1 0 542674276 141860864 33842 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34634 33842 603 41 0 34593 0
vsize: 138536
[startup+960.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 34479 0 0 0 95910 108 0 0 25 0 1 0 542674276 142934016 34124 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34896 34124 603 41 0 34855 0
vsize: 139584
[startup+970.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 34866 0 0 0 96909 109 0 0 25 0 1 0 542674276 144543744 34511 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35289 34511 603 41 0 35248 0
vsize: 141156
[startup+980.095 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 35291 0 0 0 97907 111 0 0 25 0 1 0 542674276 146309120 34936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35720 34936 603 41 0 35679 0
vsize: 142880
[startup+990.096 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 35523 0 0 0 98906 112 0 0 25 0 1 0 542674276 147247104 35168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35949 35168 603 41 0 35908 0
vsize: 143796
[startup+1000.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 35762 0 0 0 99905 113 0 0 25 0 1 0 542674276 148189184 35407 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36179 35407 603 41 0 36138 0
vsize: 144716
[startup+1010.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 35970 0 0 0 100905 114 0 0 25 0 1 0 542674276 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+1020.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 36125 0 0 0 101905 114 0 0 25 0 1 0 542674276 149680128 35770 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36543 35770 603 41 0 36502 0
vsize: 146172
[startup+1030.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 36356 0 0 0 102903 115 0 0 25 0 1 0 542674276 150622208 36001 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36773 36001 603 41 0 36732 0
vsize: 147092
[startup+1040.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 36628 0 0 0 103903 116 0 0 25 0 1 0 542674276 151818240 36273 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37065 36273 603 41 0 37024 0
vsize: 148260
[startup+1050.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 36989 0 0 0 104902 117 0 0 25 0 1 0 542674276 153153536 36634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37391 36634 603 41 0 37350 0
vsize: 149564
[startup+1060.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 37116 0 0 0 105902 118 0 0 25 0 1 0 542674276 153690112 36761 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37522 36761 603 41 0 37481 0
vsize: 150088
[startup+1070.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 37382 0 0 0 106901 118 0 0 25 0 1 0 542674276 154775552 37027 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37787 37027 603 41 0 37746 0
vsize: 151148
[startup+1080.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 37634 0 0 0 107900 119 0 0 25 0 1 0 542674276 155844608 37279 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38048 37279 603 41 0 38007 0
vsize: 152192
[startup+1090.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 37932 0 0 0 108899 121 0 0 25 0 1 0 542674276 157061120 37577 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38345 37577 603 41 0 38304 0
vsize: 153380
[startup+1100.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 38172 0 0 0 109898 122 0 0 25 0 1 0 542674276 158015488 37817 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38578 37817 603 41 0 38537 0
vsize: 154312
[startup+1110.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 38404 0 0 0 110898 122 0 0 25 0 1 0 542674276 158965760 38049 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38810 38049 603 41 0 38769 0
vsize: 155240
[startup+1120.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 38729 0 0 0 111897 123 0 0 25 0 1 0 542674276 160329728 38374 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39143 38374 603 41 0 39102 0
vsize: 156572
[startup+1130.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 39050 0 0 0 112896 124 0 0 25 0 1 0 542674276 161550336 38695 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39441 38695 603 41 0 39400 0
vsize: 157764
[startup+1140.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29894
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 39414 0 0 0 113895 125 0 0 25 0 1 0 542674276 163168256 39059 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39836 39059 603 41 0 39795 0
vsize: 159344
[startup+1150.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29896
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 39775 0 0 0 114894 126 0 0 25 0 1 0 542674276 164528128 39420 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40168 39420 603 41 0 40127 0
vsize: 160672
[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29896
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 40100 0 0 0 115893 128 0 0 25 0 1 0 542674276 165928960 39745 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40510 39745 603 41 0 40469 0
vsize: 162040
[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29896
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 40314 0 0 0 116893 128 0 0 25 0 1 0 542674276 166866944 39959 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40739 39959 603 41 0 40698 0
vsize: 162956
[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29896
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 40517 0 0 0 117892 129 0 0 25 0 1 0 542674276 167673856 40162 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40936 40162 603 41 0 40895 0
vsize: 163744
[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29896
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 40816 0 0 0 118891 130 0 0 25 0 1 0 542674276 168886272 40461 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41232 40461 603 41 0 41191 0
vsize: 164928
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 29896
Raw data (stat): 29839 (minisat+) R 29838 3260 3259 0 -1 0 40993 0 0 0 119890 131 0 0 25 0 1 0 542674276 169558016 40638 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41396 40638 603 41 0 41355 0
vsize: 165584
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 29896
Raw data (stat): 29839 (minisat+) Z 29838 3260 3259 0 -1 12 40995 0 0 0 119890 138 0 0 25 0 1 0 542674276 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.18
CPU time (s): 1200.3
CPU user time (s): 1198.91
CPU system time (s): 1.38979
CPU usage (%): 100.01
Max. virtual memory (Kb): 165584
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####