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-air04.opb
MD5SUM	eb0734273e24196dd14c6f237b52fa81
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	8904
Biggest coefficient in the objective function	2258
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	5135151
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	2258
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	5135151
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.12098
Number of variables	8904
Total number of constraints	9727
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9727
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	368
Trace number 22347

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        482728 kB
Buffers:         34864 kB
Cached:         494108 kB
SwapCached:          0 kB
Active:          64672 kB
Inactive:       467100 kB
HighTotal:      131008 kB
HighFree:        19124 kB
LowTotal:       903652 kB
LowFree:        463604 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            14424 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:20:21 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 11660 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   63
c ---[1640]---> BDD-cost:   23
c ---[1638]---> BDD-cost:   29
c ---[1636]---> BDD-cost:    0
c ---[1634]---> BDD-cost:   71
c ---[1632]---> BDD-cost:   55
c ---[1628]---> BDD-cost:   23
c ---[1626]---> BDD-cost:   47
c ---[1624]---> BDD-cost:  213
c ---[1622]---> BDD-cost:   75
c ---[1620]---> BDD-cost:   75
c ---[1618]---> BDD-cost:   55
c ---[1616]---> BDD-cost:   15
c ---[1614]---> BDD-cost:   87
c ---[1612]---> BDD-cost:   51
c ---[1610]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1606]---> BDD-cost:   23
c ---[1604]---> BDD-cost:   11
c ---[1602]---> BDD-cost:   39
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:  259
c ---[1594]---> BDD-cost:  189
c ---[1592]---> BDD-cost:  101
c ---[1588]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  101
c ---[1582]---> BDD-cost:   37
c ---[1580]---> BDD-cost:  181
c ---[1578]---> BDD-cost:  283
c ---[1576]---> BDD-cost:   99
c ---[1574]---> BDD-cost:    1
c ---[1572]---> BDD-cost:  109
c ---[1570]---> BDD-cost:   75
c ---[1568]---> BDD-cost:  237
c ---[1566]---> BDD-cost:  119
c ---[1564]---> BDD-cost:  109
c ---[1562]---> BDD-cost:   83
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:  157
c ---[1556]---> BDD-cost:  155
c ---[1554]---> BDD-cost:  109
c ---[1550]---> BDD-cost:   77
c ---[1548]---> BDD-cost:  133
c ---[1546]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  115
c ---[1542]---> BDD-cost:  185
c ---[1540]---> BDD-cost:  203
c ---[1538]---> BDD-cost:  167
c ---[1536]---> BDD-cost:  135
c ---[1534]---> BDD-cost:    9
c ---[1532]---> BDD-cost:   85
c ---[1530]---> BDD-cost:  143
c ---[1528]---> BDD-cost:  135
c ---[1526]---> BDD-cost:   63
c ---[1524]---> BDD-cost:   51
c ---[1522]---> BDD-cost:  159
c ---[1520]---> BDD-cost:  155
c ---[1518]---> BDD-cost:  211
c ---[1516]---> BDD-cost:   75
c ---[1514]---> BDD-cost:   37
c ---[1512]---> BDD-cost:   87
c ---[1510]---> BDD-cost:   79
c ---[1508]---> BDD-cost:  109
c ---[1506]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  247
c ---[1502]---> BDD-cost:  105
c ---[1500]---> BDD-cost:   59
c ---[1498]---> BDD-cost:   71
c ---[1496]---> BDD-cost:   61
c ---[1494]---> BDD-cost:   89
c ---[1492]---> BDD-cost:   91
c ---[1490]---> BDD-cost:  143
c ---[1488]---> BDD-cost:  111
c ---[1486]---> BDD-cost:   95
c ---[1484]---> BDD-cost:  169
c ---[1482]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  151
c ---[1478]---> BDD-cost:   67
c ---[1476]---> BDD-cost:   45
c ---[1474]---> BDD-cost:   45
c ---[1472]---> BDD-cost:   45
c ---[1470]---> BDD-cost:   65
c ---[1468]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   47
c ---[1460]---> BDD-cost:   29
c ---[1458]---> BDD-cost:   27
c ---[1456]---> BDD-cost:   11
c ---[1452]---> BDD-cost:   81
c ---[1450]---> BDD-cost:  233
c ---[1448]---> BDD-cost:  275
c ---[1446]---> BDD-cost:  289
c ---[1444]---> BDD-cost:  119
c ---[1442]---> BDD-cost:  145
c ---[1440]---> BDD-cost:  165
c ---[1438]---> BDD-cost:  239
c ---[1436]---> BDD-cost:  223
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   35
c ---[1430]---> BDD-cost:   93
c ---[1428]---> BDD-cost:   45
c ---[1426]---> BDD-cost:   73
c ---[1424]---> BDD-cost:   75
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   99
c ---[1416]---> BDD-cost:  187
c ---[1414]---> BDD-cost:   55
c ---[1412]---> BDD-cost:  107
c ---[1410]---> BDD-cost:   69
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:    3
c ---[1404]---> BDD-cost:  149
c ---[1402]---> BDD-cost:  137
c ---[1400]---> BDD-cost:  195
c ---[1398]---> BDD-cost:   93
c ---[1396]---> BDD-cost:  157
c ---[1394]---> BDD-cost:  233
c ---[1392]---> BDD-cost:  223
c ---[1390]---> BDD-cost:  225
c ---[1388]---> BDD-cost:  247
c ---[1386]---> BDD-cost:  179
c ---[1384]---> BDD-cost:  225
c ---[1382]---> BDD-cost:  243
c ---[1380]---> BDD-cost:  199
c ---[1378]---> BDD-cost:   55
c ---[1376]---> BDD-cost:   57
c ---[1374]---> BDD-cost:   99
c ---[1372]---> BDD-cost:    9
c ---[1370]---> BDD-cost:    3
c ---[1368]---> BDD-cost:   23
c ---[1366]---> BDD-cost:   51
c ---[1364]---> BDD-cost:   25
c ---[1362]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   27
c ---[1358]---> BDD-cost:   15
c ---[1356]---> BDD-cost:   37
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   67
c ---[1350]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  211
c ---[1342]---> BDD-cost:   65
c ---[1340]---> BDD-cost:  117
c ---[1338]---> BDD-cost:   65
c ---[1336]---> BDD-cost:   65
c ---[1334]---> BDD-cost:   49
c ---[1332]---> BDD-cost:  439
c ---[1330]---> BDD-cost:  423
c ---[1328]---> BDD-cost:  287
c ---[1326]---> BDD-cost:  217
c ---[1324]---> BDD-cost:  195
c ---[1322]---> BDD-cost:   63
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:  359
c ---[1316]---> BDD-cost:  353
c ---[1312]---> BDD-cost:  169
c ---[1310]---> BDD-cost:  139
c ---[1308]---> BDD-cost:  159
c ---[1306]---> BDD-cost:  223
c ---[1304]---> BDD-cost:  107
c ---[1302]---> BDD-cost:   75
c ---[1300]---> BDD-cost:  109
c ---[1298]---> BDD-cost:   93
c ---[1296]---> BDD-cost:   87
c ---[1294]---> BDD-cost:   87
c ---[1292]---> BDD-cost:    7
c ---[1288]---> BDD-cost:   73
c ---[1286]---> BDD-cost:   71
c ---[1284]---> BDD-cost:  107
c ---[1282]---> BDD-cost:   77
c ---[1280]---> BDD-cost:    3
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  131
c ---[1274]---> BDD-cost:  135
c ---[1272]---> BDD-cost:   65
c ---[1270]---> BDD-cost:  165
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:    1
c ---[1264]---> BDD-cost:   87
c ---[1262]---> BDD-cost:  155
c ---[1260]---> BDD-cost:  167
c ---[1258]---> BDD-cost:  203
c ---[1256]---> BDD-cost:  231
c ---[1254]---> BDD-cost:  147
c ---[1252]---> BDD-cost:  135
c ---[1250]---> BDD-cost:   49
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   95
c ---[1244]---> BDD-cost:  325
c ---[1242]---> BDD-cost:  333
c ---[1240]---> BDD-cost:  173
c ---[1238]---> BDD-cost:  269
c ---[1236]---> BDD-cost:   31
c ---[1234]---> BDD-cost:  413
c ---[1232]---> BDD-cost:  313
c ---[1230]---> BDD-cost:  125
c ---[1228]---> BDD-cost:  113
c ---[1226]---> BDD-cost:  247
c ---[1224]---> BDD-cost:   57
c ---[1222]---> BDD-cost:  237
c ---[1220]---> BDD-cost:  159
c ---[1218]---> BDD-cost:  117
c ---[1216]---> BDD-cost:   43
c ---[1214]---> BDD-cost:  143
c ---[1212]---> BDD-cost:   65
c ---[1210]---> BDD-cost:  123
c ---[1208]---> BDD-cost:   61
c ---[1206]---> BDD-cost:  103
c ---[1204]---> BDD-cost:   85
c ---[1202]---> BDD-cost:   77
c ---[1200]---> BDD-cost:   57
c ---[1198]---> BDD-cost:  127
c ---[1196]---> BDD-cost:  157
c ---[1194]---> BDD-cost:  267
c ---[1192]---> BDD-cost:  223
c ---[1190]---> BDD-cost:  229
c ---[1188]---> BDD-cost:  257
c ---[1186]---> BDD-cost:  241
c ---[1184]---> BDD-cost:  195
c ---[1182]---> BDD-cost:   49
c ---[1180]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  197
c ---[1176]---> BDD-cost:  171
c ---[1174]---> BDD-cost:  287
c ---[1172]---> BDD-cost:   75
c ---[1170]---> BDD-cost:  215
c ---[1168]---> BDD-cost:  119
c ---[1166]---> BDD-cost:  245
c ---[1164]---> BDD-cost:  257
c ---[1162]---> BDD-cost:  279
c ---[1160]---> BDD-cost:  227
c ---[1158]---> BDD-cost:  201
c ---[1156]---> BDD-cost:  143
c ---[1154]---> BDD-cost:  207
c ---[1152]---> BDD-cost:  131
c ---[1150]---> BDD-cost:  245
c ---[1148]---> BDD-cost:  115
c ---[1146]---> BDD-cost:   91
c ---[1144]---> BDD-cost:   43
c ---[1142]---> BDD-cost:   39
c ---[1140]---> BDD-cost:   91
c ---[1138]---> BDD-cost:  179
c ---[1136]---> BDD-cost:   73
c ---[1134]---> BDD-cost:   29
c ---[1132]---> BDD-cost:  163
c ---[1130]---> BDD-cost:   81
c ---[1128]---> BDD-cost:   63
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  113
c ---[1122]---> BDD-cost:  115
c ---[1120]---> BDD-cost:   19
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   99
c ---[1114]---> BDD-cost:   99
c ---[1112]---> BDD-cost:  103
c ---[1110]---> BDD-cost:   67
c ---[1108]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   85
c ---[1104]---> BDD-cost:   87
c ---[1102]---> BDD-cost:    7
c ---[1100]---> BDD-cost:   45
c ---[1098]---> BDD-cost:   43
c ---[1096]---> BDD-cost:   11
c ---[1094]---> BDD-cost:   59
c ---[1092]---> BDD-cost:  185
c ---[1090]---> BDD-cost:  249
c ---[1088]---> BDD-cost:  315
c ---[1086]---> BDD-cost:  253
c ---[1084]---> BDD-cost:  161
c ---[1082]---> BDD-cost:  257
c ---[1080]---> BDD-cost:  167
c ---[1078]---> BDD-cost:  167
c ---[1076]---> BDD-cost:  141
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   95
c ---[1068]---> BDD-cost:  141
c ---[1066]---> BDD-cost:  123
c ---[1064]---> BDD-cost:   83
c ---[1062]---> BDD-cost:   55
c ---[1060]---> BDD-cost:  183
c ---[1058]---> BDD-cost:  269
c ---[1056]---> BDD-cost:   63
c ---[1054]---> BDD-cost:   45
c ---[1052]---> BDD-cost:   39
c ---[1050]---> BDD-cost:   97
c ---[1048]---> BDD-cost:   51
c ---[1046]---> BDD-cost:   45
c ---[1044]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   85
c ---[1040]---> BDD-cost:   35
c ---[1038]---> BDD-cost:   53
c ---[1036]---> BDD-cost:   21
c ---[1034]---> BDD-cost:  115
c ---[1032]---> BDD-cost:   99
c ---[1030]---> BDD-cost:   63
c ---[1028]---> BDD-cost:   77
c ---[1026]---> BDD-cost:  139
c ---[1024]---> BDD-cost:  109
c ---[1022]---> BDD-cost:  407
c ---[1020]---> BDD-cost:  323
c ---[1018]---> BDD-cost:  109
c ---[1016]---> BDD-cost:   93
c ---[1014]---> BDD-cost:   51
c ---[1012]---> BDD-cost:   79
c ---[1010]---> BDD-cost:   75
c ---[1008]---> BDD-cost:  147
c ---[1006]---> BDD-cost:  169
c ---[1004]---> BDD-cost:  209
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   51
c ---[ 998]---> BDD-cost:   85
c ---[ 994]---> BDD-cost:  103
c ---[ 992]---> BDD-cost:  127
c ---[ 990]---> BDD-cost:   77
c ---[ 988]---> BDD-cost:   77
c ---[ 986]---> BDD-cost:  141
c ---[ 984]---> BDD-cost:   89
c ---[ 982]---> BDD-cost:   85
c ---[ 980]---> BDD-cost:  119
c ---[ 978]---> BDD-cost:   69
c ---[ 976]---> BDD-cost:   57
c ---[ 974]---> BDD-cost:   65
c ---[ 972]---> BDD-cost:   47
c ---[ 970]---> BDD-cost:   61
c ---[ 968]---> BDD-cost:   31
c ---[ 964]---> BDD-cost:  183
c ---[ 962]---> BDD-cost:  121
c ---[ 960]---> BDD-cost:   89
c ---[ 958]---> BDD-cost:  225
c ---[ 956]---> BDD-cost:  267
c ---[ 952]---> BDD-cost:  159
c ---[ 950]---> BDD-cost:  209
c ---[ 948]---> BDD-cost:   71
c ---[ 946]---> BDD-cost:  237
c ---[ 944]---> BDD-cost:  129
c ---[ 942]---> BDD-cost:  365
c ---[ 940]---> BDD-cost:  369
c ---[ 938]---> BDD-cost:  129
c ---[ 936]---> BDD-cost:  101
c ---[ 934]---> BDD-cost:  289
c ---[ 932]---> BDD-cost:  279
c ---[ 930]---> BDD-cost:  345
c ---[ 928]---> BDD-cost:   81
c ---[ 926]---> BDD-cost:   69
c ---[ 924]---> BDD-cost:   83
c ---[ 922]---> BDD-cost:   53
c ---[ 920]---> BDD-cost:   67
c ---[ 918]---> BDD-cost:   55
c ---[ 916]---> BDD-cost:  145
c ---[ 914]---> BDD-cost:  149
c ---[ 912]---> BDD-cost:  105
c ---[ 910]---> BDD-cost:   19
c ---[ 908]---> BDD-cost:  105
c ---[ 906]---> BDD-cost:  101
c ---[ 904]---> BDD-cost:  147
c ---[ 902]---> BDD-cost:  231
c ---[ 900]---> BDD-cost:  191
c ---[ 898]---> BDD-cost:  157
c ---[ 896]---> BDD-cost:  249
c ---[ 894]---> BDD-cost:  385
c ---[ 892]---> BDD-cost:   67
c ---[ 890]---> BDD-cost:   71
c ---[ 888]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:  147
c ---[ 884]---> BDD-cost:  139
c ---[ 882]---> BDD-cost:  273
c ---[ 880]---> BDD-cost:  213
c ---[ 878]---> BDD-cost:  169
c ---[ 876]---> BDD-cost:  239
c ---[ 874]---> BDD-cost:  305
c ---[ 872]---> BDD-cost:  109
c ---[ 870]---> BDD-cost:  105
c ---[ 868]---> BDD-cost:  147
c ---[ 866]---> BDD-cost:  115
c ---[ 864]---> BDD-cost:  115
c ---[ 862]---> BDD-cost:   67
c ---[ 860]---> BDD-cost:  329
c ---[ 858]---> BDD-cost:  295
c ---[ 856]---> BDD-cost:   51
c ---[ 854]---> BDD-cost:   61
c ---[ 852]---> BDD-cost:  317
c ---[ 850]---> BDD-cost:   97
c ---[ 848]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:   43
c ---[ 844]---> BDD-cost:   85
c ---[ 842]---> BDD-cost:   35
c ---[ 840]---> BDD-cost:   69
c ---[ 836]---> BDD-cost:   45
c ---[ 834]---> BDD-cost:   73
c ---[ 832]---> BDD-cost:   55
c ---[ 828]---> BDD-cost:   33
c ---[ 826]---> BDD-cost:   29
c ---[ 824]---> BDD-cost:  245
c ---[ 822]---> BDD-cost:  225
c ---[ 820]---> BDD-cost:  111
c ---[ 818]---> BDD-cost:  117
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  129
c ---[ 812]---> BDD-cost:  259
c ---[ 810]---> BDD-cost:  221
c ---[ 808]---> BDD-cost:  275
c ---[ 806]---> BDD-cost:  209
c ---[ 804]---> BDD-cost:  267
c ---[ 802]---> BDD-cost:  171
c ---[ 800]---> BDD-cost:   57
c ---[ 796]---> BDD-cost:  133
c ---[ 794]---> BDD-cost:  185
c ---[ 792]---> BDD-cost:  169
c ---[ 790]---> BDD-cost:  287
c ---[ 788]---> BDD-cost:   81
c ---[ 786]---> BDD-cost:  335
c ---[ 784]---> BDD-cost:  365
c ---[ 782]---> BDD-cost:  255
c ---[ 780]---> BDD-cost:  111
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  101
c ---[ 774]---> BDD-cost:  197
c ---[ 772]---> BDD-cost:  383
c ---[ 770]---> BDD-cost:  329
c ---[ 768]---> BDD-cost:  241
c ---[ 766]---> BDD-cost:  129
c ---[ 764]---> BDD-cost:   85
c ---[ 762]---> BDD-cost:   71
c ---[ 760]---> BDD-cost:   37
c ---[ 758]---> BDD-cost:   77
c ---[ 756]---> BDD-cost:   49
c ---[ 754]---> BDD-cost:  133
c ---[ 752]---> BDD-cost:  133
c ---[ 750]---> BDD-cost:  377
c ---[ 748]---> BDD-cost:  117
c ---[ 744]---> BDD-cost:  119
c ---[ 742]---> BDD-cost:  119
c ---[ 740]---> BDD-cost:  151
c ---[ 738]---> BDD-cost:  221
c ---[ 736]---> BDD-cost:  181
c ---[ 732]---> BDD-cost:   87
c ---[ 730]---> BDD-cost:  127
c ---[ 728]---> BDD-cost:  299
c ---[ 726]---> BDD-cost:  331
c ---[ 722]---> BDD-cost:   21
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  217
c ---[ 716]---> BDD-cost:  349
c ---[ 714]---> BDD-cost:  291
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  161
c ---[ 708]---> BDD-cost:   61
c ---[ 706]---> BDD-cost:   55
c ---[ 704]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:  189
c ---[ 698]---> BDD-cost:  157
c ---[ 696]---> BDD-cost:  149
c ---[ 694]---> BDD-cost:  139
c ---[ 692]---> BDD-cost:  165
c ---[ 690]---> BDD-cost:  181
c ---[ 688]---> BDD-cost:  253
c ---[ 686]---> BDD-cost:   43
c ---[ 684]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  141
c ---[ 680]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:   95
c ---[ 676]---> BDD-cost:   75
c ---[ 674]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  149
c ---[ 670]---> BDD-cost:  137
c ---[ 668]---> BDD-cost:   59
c ---[ 666]---> BDD-cost:    5
c ---[ 664]---> BDD-cost:   35
c ---[ 662]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   47
c ---[ 654]---> BDD-cost:   55
c ---[ 652]---> BDD-cost:  197
c ---[ 650]---> BDD-cost:  191
c ---[ 648]---> BDD-cost:  125
c ---[ 646]---> BDD-cost:  173
c ---[ 642]---> BDD-cost:   93
c ---[ 640]---> BDD-cost:   29
c ---[ 638]---> BDD-cost:  321
c ---[ 636]---> BDD-cost:  195
c ---[ 634]---> BDD-cost:  163
c ---[ 628]---> BDD-cost:  151
c ---[ 626]---> BDD-cost:  253
c ---[ 624]---> BDD-cost:  381
c ---[ 622]---> BDD-cost:  345
c ---[ 620]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:   83
c ---[ 614]---> BDD-cost:   69
c ---[ 612]---> BDD-cost:   51
c ---[ 610]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   59
c ---[ 606]---> BDD-cost:   83
c ---[ 604]---> BDD-cost:  107
c ---[ 602]---> BDD-cost:  363
c ---[ 600]---> BDD-cost:  103
c ---[ 598]---> BDD-cost:  277
c ---[ 596]---> BDD-cost:  341
c ---[ 594]---> BDD-cost:  213
c ---[ 592]---> BDD-cost:  315
c ---[ 590]---> BDD-cost:  275
c ---[ 588]---> BDD-cost:  151
c ---[ 586]---> BDD-cost:  111
c ---[ 584]---> BDD-cost:  103
c ---[ 582]---> BDD-cost:   75
c ---[ 580]---> BDD-cost:   27
c ---[ 578]---> BDD-cost:   21
c ---[ 576]---> BDD-cost:   11
c ---[ 574]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:  149
c ---[ 564]---> BDD-cost:   97
c ---[ 562]---> BDD-cost:  149
c ---[ 560]---> BDD-cost:  395
c ---[ 558]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:  389
c ---[ 554]---> BDD-cost:  251
c ---[ 552]---> BDD-cost:  375
c ---[ 550]---> BDD-cost:  343
c ---[ 548]---> BDD-cost:  267
c ---[ 546]---> BDD-cost:  135
c ---[ 544]---> BDD-cost:  263
c ---[ 542]---> BDD-cost:  259
c ---[ 540]---> BDD-cost:  245
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:   41
c ---[ 534]---> BDD-cost:  127
c ---[ 532]---> BDD-cost:  117
c ---[ 530]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:  149
c ---[ 526]---> BDD-cost:  103
c ---[ 524]---> BDD-cost:  215
c ---[ 522]---> BDD-cost:   89
c ---[ 520]---> BDD-cost:  177
c ---[ 518]---> BDD-cost:  343
c ---[ 516]---> BDD-cost:  237
c ---[ 514]---> BDD-cost:  177
c ---[ 512]---> BDD-cost:   85
c ---[ 510]---> BDD-cost:  267
c ---[ 508]---> BDD-cost:  225
c ---[ 506]---> BDD-cost:  109
c ---[ 504]---> BDD-cost:  105
c ---[ 502]---> BDD-cost:  113
c ---[ 500]---> BDD-cost:   55
c ---[ 498]---> BDD-cost:  117
c ---[ 496]---> BDD-cost:   83
c ---[ 494]---> BDD-cost:   79
c ---[ 492]---> BDD-cost:   81
c ---[ 490]---> BDD-cost:  263
c ---[ 488]---> BDD-cost:  179
c ---[ 486]---> BDD-cost:  281
c ---[ 484]---> BDD-cost:  389
c ---[ 482]---> BDD-cost:  333
c ---[ 480]---> BDD-cost:  357
c ---[ 478]---> BDD-cost:  345
c ---[ 476]---> BDD-cost:  263
c ---[ 474]---> BDD-cost:   89
c ---[ 472]---> BDD-cost:  285
c ---[ 468]---> BDD-cost:  419
c ---[ 466]---> BDD-cost:  357
c ---[ 464]---> BDD-cost:  473
c ---[ 462]---> BDD-cost:  455
c ---[ 460]---> BDD-cost:  405
c ---[ 458]---> BDD-cost:  241
c ---[ 456]---> BDD-cost:  211
c ---[ 454]---> BDD-cost:  313
c ---[ 452]---> BDD-cost:  371
c ---[ 450]---> BDD-cost:  389
c ---[ 448]---> BDD-cost:  223
c ---[ 446]---> BDD-cost:  221
c ---[ 444]---> BDD-cost:  147
c ---[ 442]---> BDD-cost:  131
c ---[ 440]---> BDD-cost:  185
c ---[ 438]---> BDD-cost:  141
c ---[ 436]---> BDD-cost:  249
c ---[ 434]---> BDD-cost:  261
c ---[ 432]---> BDD-cost:  311
c ---[ 430]---> BDD-cost:  261
c ---[ 428]---> BDD-cost:  387
c ---[ 426]---> BDD-cost:  247
c ---[ 424]---> BDD-cost:  295
c ---[ 422]---> BDD-cost:   31
c ---[ 420]---> BDD-cost:  355
c ---[ 418]---> BDD-cost:  135
c ---[ 416]---> BDD-cost:  443
c ---[ 414]---> BDD-cost:  653
c ---[ 412]---> BDD-cost:  703
c ---[ 410]---> BDD-cost:  517
c ---[ 408]---> BDD-cost:  441
c ---[ 406]---> BDD-cost:  411
c ---[ 404]---> BDD-cost:  289
c ---[ 402]---> BDD-cost:  277
c ---[ 400]---> BDD-cost:  239
c ---[ 398]---> BDD-cost:  201
c ---[ 396]---> BDD-cost:  309
c ---[ 394]---> BDD-cost:  287
c ---[ 392]---> BDD-cost:  177
c ---[ 390]---> BDD-cost:  143
c ---[ 388]---> BDD-cost:  131
c ---[ 386]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:  189
c ---[ 382]---> BDD-cost:  219
c ---[ 378]---> BDD-cost:  267
c ---[ 376]---> BDD-cost:  135
c ---[ 374]---> BDD-cost:   69
c ---[ 372]---> BDD-cost:   75
c ---[ 370]---> BDD-cost:   51
c ---[ 368]---> BDD-cost:  117
c ---[ 366]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:  189
c ---[ 358]---> BDD-cost:   73
c ---[ 356]---> BDD-cost:   55
c ---[ 354]---> BDD-cost:   57
c ---[ 352]---> BDD-cost:   91
c ---[ 350]---> BDD-cost:  325
c ---[ 348]---> BDD-cost:  223
c ---[ 346]---> BDD-cost:   57
c ---[ 344]---> BDD-cost:   43
c ---[ 342]---> BDD-cost:  255
c ---[ 340]---> BDD-cost:  285
c ---[ 338]---> BDD-cost:  187
c ---[ 336]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   91
c ---[ 332]---> BDD-cost:  211
c ---[ 330]---> BDD-cost:  159
c ---[ 328]---> BDD-cost:   97
c ---[ 326]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:  101
c ---[ 322]---> BDD-cost:  141
c ---[ 318]---> BDD-cost:  109
c ---[ 316]---> BDD-cost:  321
c ---[ 314]---> BDD-cost:  305
c ---[ 312]---> BDD-cost:  603
c ---[ 310]---> BDD-cost:  441
c ---[ 308]---> BDD-cost:  391
c ---[ 306]---> BDD-cost:  387
c ---[ 304]---> BDD-cost:  289
c ---[ 302]---> BDD-cost:  219
c ---[ 300]---> BDD-cost:  309
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  197
c ---[ 294]---> BDD-cost:  279
c ---[ 292]---> BDD-cost:  167
c ---[ 290]---> BDD-cost:  151
c ---[ 288]---> BDD-cost:   49
c ---[ 286]---> BDD-cost:   31
c ---[ 284]---> BDD-cost:  107
c ---[ 282]---> BDD-cost:   55
c ---[ 278]---> BDD-cost:  177
c ---[ 276]---> BDD-cost:  223
c ---[ 274]---> BDD-cost:  119
c ---[ 272]---> BDD-cost:  137
c ---[ 270]---> BDD-cost:  105
c ---[ 268]---> BDD-cost:  183
c ---[ 266]---> BDD-cost:  179
c ---[ 264]---> BDD-cost:  285
c ---[ 262]---> BDD-cost:  191
c ---[ 260]---> BDD-cost:  177
c ---[ 258]---> BDD-cost:  145
c ---[ 254]---> BDD-cost:  153
c ---[ 252]---> BDD-cost:  121
c ---[ 250]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:  111
c ---[ 244]---> BDD-cost:  281
c ---[ 242]---> BDD-cost:  265
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  151
c ---[ 236]---> BDD-cost:  167
c ---[ 234]---> BDD-cost:  137
c ---[ 230]---> BDD-cost:  375
c ---[ 228]---> BDD-cost:  287
c ---[ 226]---> BDD-cost:  249
c ---[ 224]---> BDD-cost:  131
c ---[ 222]---> BDD-cost:  187
c ---[ 220]---> BDD-cost:  135
c ---[ 218]---> BDD-cost:  129
c ---[ 216]---> BDD-cost:  317
c ---[ 214]---> BDD-cost:  365
c ---[ 212]---> BDD-cost:  235
c ---[ 210]---> BDD-cost:  249
c ---[ 208]---> BDD-cost:  283
c ---[ 206]---> BDD-cost:  233
c ---[ 204]---> BDD-cost:  259
c ---[ 202]---> BDD-cost:  287
c ---[ 200]---> BDD-cost:  175
c ---[ 198]---> BDD-cost:  233
c ---[ 196]---> BDD-cost:  167
c ---[ 194]---> BDD-cost:  159
c ---[ 192]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:  135
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:  167
c ---[ 182]---> BDD-cost:  203
c ---[ 180]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  263
c ---[ 176]---> BDD-cost:   31
c ---[ 174]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   31
c ---[ 170]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:  225
c ---[ 166]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  385
c ---[ 162]---> BDD-cost:  361
c ---[ 160]---> BDD-cost:   73
c ---[ 158]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:  131
c ---[ 152]---> BDD-cost:  145
c ---[ 150]---> BDD-cost:  121
c ---[ 148]---> BDD-cost:  117
c ---[ 146]---> BDD-cost:  111
c ---[ 144]---> BDD-cost:  123
c ---[ 142]---> BDD-cost:  125
c ---[ 140]---> BDD-cost:  243
c ---[ 138]---> BDD-cost:  143
c ---[ 136]---> BDD-cost:  149
c ---[ 134]---> BDD-cost:  103
c ---[ 132]---> BDD-cost:  155
c ---[ 130]---> BDD-cost:  247
c ---[ 128]---> BDD-cost:  143
c ---[ 126]---> BDD-cost:   91
c ---[ 124]---> BDD-cost:   81
c ---[ 122]---> BDD-cost:   79
c ---[ 120]---> BDD-cost:  117
c ---[ 118]---> BDD-cost:   89
c ---[ 116]---> BDD-cost:   61
c ---[ 114]---> BDD-cost:  127
c ---[ 112]---> BDD-cost:  135
c ---[ 110]---> BDD-cost:  161
c ---[ 108]---> BDD-cost:  141
c ---[ 106]---> BDD-cost:  437
c ---[ 104]---> BDD-cost:  309
c ---[ 102]---> BDD-cost:  173
c ---[ 100]---> BDD-cost:  441
c ---[  98]---> BDD-cost:  489
c ---[  96]---> BDD-cost:  299
c ---[  94]---> BDD-cost:  455
c ---[  92]---> BDD-cost:  333
c ---[  90]---> BDD-cost:  421
c ---[  88]---> BDD-cost:  375
c ---[  86]---> BDD-cost:  433
c ---[  84]---> BDD-cost:  405
c ---[  82]---> BDD-cost:  333
c ---[  80]---> BDD-cost:  673
c ---[  78]---> BDD-cost:  685
c ---[  76]---> BDD-cost:  385
c ---[  74]---> BDD-cost:  267
c ---[  72]---> BDD-cost:  345
c ---[  70]---> BDD-cost:  365
c ---[  68]---> BDD-cost:  391
c ---[  66]---> BDD-cost:  313
c ---[  64]---> BDD-cost:  275
c ---[  62]---> BDD-cost:  257
c ---[  60]---> BDD-cost:  203
c ---[  58]---> BDD-cost:  311
c ---[  56]---> BDD-cost:  227
c ---[  54]---> BDD-cost:  295
c ---[  52]---> BDD-cost:  233
c ---[  50]---> BDD-cost:  247
c ---[  46]---> BDD-cost:  237
c ---[  44]---> BDD-cost:  149
c ---[  40]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   85
c ---[  36]---> BDD-cost:  109
c ---[  34]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:   71
c ---[  28]---> BDD-cost:   67
c ---[  26]---> BDD-cost:  151
c ---[  24]---> BDD-cost:  147
c ---[  22]---> BDD-cost:  177
c ---[  20]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  147
c ---[  14]---> BDD-cost:  215
c ---[  12]---> BDD-cost:  181
c ---[  10]---> BDD-cost:  235
c ---[   8]---> BDD-cost:  163
c ---[   6]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   59
c ---[   2]---> BDD-cost:  139
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  310358   807732 |  103452       0        0     nan |  0.000 % |
c |       100 |  310358   807732 |  113797     100     2792    27.9 |  0.588 % |
c |       250 |  310331   807657 |  125176     249    12761    51.2 |  0.592 % |
c |       475 |  310198   807286 |  137694     459    35376    77.1 |  0.620 % |
c |       812 |  310052   806901 |  151464     787    48598    61.8 |  0.642 % |
c |      1319 |  309884   806468 |  166610    1289    73251    56.8 |  0.667 % |
c |      2078 |  309785   806192 |  183271    2043   141139    69.1 |  0.692 % |
c |      3217 |  309724   806017 |  201598    3171   279873    88.3 |  0.705 % |
c |      4927 |  309614   805741 |  221758    4872   562380   115.4 |  0.716 % |
c |      7490 |  309614   805741 |  243934    7435  1259451   169.4 |  0.716 % |
c |     11334 |  309475   805377 |  268327   11239  1793736   159.6 |  0.732 % |
c |     17101 |  309226   804713 |  295160   16957  2478519   146.2 |  0.776 % |
c |     25752 |  307768   801003 |  324676   25505  3930547   154.1 |  0.987 % |
c |     38728 |  307515   800363 |  357144   38421  6348349   165.2 |  1.003 % |
c |     58191 |  307356   799958 |  392858   57785 10148314   175.6 |  1.017 % |
c |     87385 |  306886   798753 |  432144   86840 17512694   201.7 |  1.062 % |
c |    131176 |  306715   798313 |  475359  130557 31984227   245.0 |  1.079 % |
#### 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.85 0.94 0.90 2/54 25906
Raw data (stat): 25906 (runsolver) R 25905 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 492087084 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.0009 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 25906
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 11064 0 0 0 970 29 0 0 25 0 1 0 492087084 54525952 10706 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13312 10706 603 41 0 13271 0
vsize: 53248
[startup+20.0022 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 25906
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 11312 0 0 0 1969 30 0 0 25 0 1 0 492087084 55472128 10954 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13543 10954 603 41 0 13502 0
vsize: 54172
[startup+30.003 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 25906
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 11716 0 0 0 2967 31 0 0 25 0 1 0 492087084 57085952 11358 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13937 11358 603 41 0 13896 0
vsize: 55748
[startup+40.0034 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 25906
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 12360 0 0 0 3965 34 0 0 25 0 1 0 492087084 59777024 12002 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14594 12002 603 41 0 14553 0
vsize: 58376
[startup+50.0047 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 25906
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 12746 0 0 0 4963 36 0 0 25 0 1 0 492087084 61390848 12388 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 12388 603 41 0 14947 0
vsize: 59952
[startup+60.0056 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 13037 0 0 0 5962 37 0 0 25 0 1 0 492087084 62607360 12679 4294967295 134512640 134672761 3221224544 3221223680 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15285 12679 603 41 0 15244 0
vsize: 61140
[startup+70.0059 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 13317 0 0 0 6960 39 0 0 25 0 1 0 492087084 63684608 12959 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15548 12959 603 41 0 15507 0
vsize: 62192
[startup+80.0058 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 13563 0 0 0 7959 40 0 0 25 0 1 0 492087084 64761856 13205 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15811 13205 603 41 0 15770 0
vsize: 63244
[startup+90.006 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 13897 0 0 0 8957 42 0 0 25 0 1 0 492087084 66187264 13539 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16159 13539 603 41 0 16118 0
vsize: 64636
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 14223 0 0 0 9956 43 0 0 25 0 1 0 492087084 67399680 13865 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16455 13865 603 41 0 16414 0
vsize: 65820
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 14627 0 0 0 10955 44 0 0 25 0 1 0 492087084 69152768 14269 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16883 14269 603 41 0 16842 0
vsize: 67532
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 14993 0 0 0 11954 45 0 0 25 0 1 0 492087084 70631424 14635 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17244 14635 603 41 0 17203 0
vsize: 68976
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 15238 0 0 0 12953 47 0 0 25 0 1 0 492087084 71577600 14880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 14880 603 41 0 17434 0
vsize: 69900
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 15556 0 0 0 13951 49 0 0 25 0 1 0 492087084 72921088 15198 4294967295 134512640 134672761 3221224544 3221223712 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17803 15198 603 41 0 17762 0
vsize: 71212
[startup+150.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 15919 0 0 0 14950 50 0 0 25 0 1 0 492087084 74407936 15561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18166 15561 603 41 0 18125 0
vsize: 72664
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 16269 0 0 0 15949 51 0 0 25 0 1 0 492087084 75751424 15911 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18494 15911 603 41 0 18453 0
vsize: 73976
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 16542 0 0 0 16948 52 0 0 25 0 1 0 492087084 76832768 16184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18758 16184 603 41 0 18717 0
vsize: 75032
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 16876 0 0 0 17947 53 0 0 25 0 1 0 492087084 78311424 16518 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19119 16518 603 41 0 19078 0
vsize: 76476
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 17231 0 0 0 18945 55 0 0 25 0 1 0 492087084 79798272 16873 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19482 16873 603 41 0 19441 0
vsize: 77928
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 17547 0 0 0 19944 56 0 0 25 0 1 0 492087084 81133568 17189 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19808 17189 603 41 0 19767 0
vsize: 79232
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 17936 0 0 0 20943 57 0 0 25 0 1 0 492087084 82743296 17578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 17578 603 41 0 20160 0
vsize: 80804
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 18157 0 0 0 21942 59 0 0 25 0 1 0 492087084 83554304 17799 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20399 17799 603 41 0 20358 0
vsize: 81596
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 18374 0 0 0 22941 60 0 0 25 0 1 0 492087084 84492288 18016 4294967295 134512640 134672761 3221224544 3221223696 134565143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20628 18016 603 41 0 20587 0
vsize: 82512
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 18797 0 0 0 23939 61 0 0 25 0 1 0 492087084 86118400 18439 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21025 18439 603 41 0 20984 0
vsize: 84100
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 19113 0 0 0 24938 62 0 0 25 0 1 0 492087084 87474176 18755 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21356 18755 603 41 0 21315 0
vsize: 85424
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 19548 0 0 0 25937 64 0 0 25 0 1 0 492087084 89223168 19190 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21783 19190 603 41 0 21742 0
vsize: 87132
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 19908 0 0 0 26936 65 0 0 25 0 1 0 492087084 90710016 19550 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22146 19550 603 41 0 22105 0
vsize: 88584
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 20063 0 0 0 27935 66 0 0 25 0 1 0 492087084 91381760 19705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22310 19705 603 41 0 22269 0
vsize: 89240
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 20339 0 0 0 28934 67 0 0 25 0 1 0 492087084 92463104 19981 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22574 19981 603 41 0 22533 0
vsize: 90296
[startup+300.014 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 20625 0 0 0 29933 68 0 0 25 0 1 0 492087084 93683712 20267 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22872 20267 603 41 0 22831 0
vsize: 91488
[startup+310.014 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 21000 0 0 0 30932 69 0 0 25 0 1 0 492087084 95170560 20642 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23235 20642 603 41 0 23194 0
vsize: 92940
[startup+320.014 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 21288 0 0 0 31931 70 0 0 25 0 1 0 492087084 96387072 20930 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23532 20930 603 41 0 23491 0
vsize: 94128
[startup+330.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 21553 0 0 0 32930 72 0 0 25 0 1 0 492087084 97456128 21195 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23793 21195 603 41 0 23752 0
vsize: 95172
[startup+340.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 21866 0 0 0 33929 73 0 0 25 0 1 0 492087084 98648064 21508 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24084 21508 603 41 0 24043 0
vsize: 96336
[startup+350.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 22136 0 0 0 34927 74 0 0 25 0 1 0 492087084 99860480 21778 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24380 21778 603 41 0 24339 0
vsize: 97520
[startup+360.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 25908
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 22416 0 0 0 35926 75 0 0 25 0 1 0 492087084 100941824 22058 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24644 22058 603 41 0 24603 0
vsize: 98576
[startup+370.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 23050 0 0 0 36925 76 0 0 25 0 1 0 492087084 103526400 22692 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25275 22692 603 41 0 25234 0
vsize: 101100
[startup+380.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 23422 0 0 0 37924 78 0 0 25 0 1 0 492087084 105009152 23064 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25637 23064 603 41 0 25596 0
vsize: 102548
[startup+390.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 23658 0 0 0 38923 78 0 0 25 0 1 0 492087084 105951232 23300 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25867 23300 603 41 0 25826 0
vsize: 103468
[startup+400.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 23968 0 0 0 39923 79 0 0 25 0 1 0 492087084 107298816 23610 4294967295 134512640 134672761 3221224544 3221223680 134565143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26196 23610 603 41 0 26155 0
vsize: 104784
[startup+410.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 24299 0 0 0 40922 80 0 0 25 0 1 0 492087084 108896256 23941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26586 23941 603 41 0 26545 0
vsize: 106344
[startup+420.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 24734 0 0 0 41921 81 0 0 25 0 1 0 492087084 110641152 24376 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27012 24376 603 41 0 26971 0
vsize: 108048
[startup+430.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 25106 0 0 0 42920 82 0 0 25 0 1 0 492087084 112119808 24748 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27373 24748 603 41 0 27332 0
vsize: 109492
[startup+440.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 25460 0 0 0 43920 83 0 0 25 0 1 0 492087084 113598464 25102 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27734 25102 603 41 0 27693 0
vsize: 110936
[startup+450.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 25747 0 0 0 44919 83 0 0 25 0 1 0 492087084 114827264 25389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28034 25389 603 41 0 27993 0
vsize: 112136
[startup+460.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 25967 0 0 0 45919 84 0 0 25 0 1 0 492087084 115638272 25609 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28232 25609 603 41 0 28191 0
vsize: 112928
[startup+470.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 26215 0 0 0 46918 84 0 0 25 0 1 0 492087084 116715520 25857 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28495 25857 603 41 0 28454 0
vsize: 113980
[startup+480.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 26527 0 0 0 47917 86 0 0 25 0 1 0 492087084 117919744 26169 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28789 26169 603 41 0 28748 0
vsize: 115156
[startup+490.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 26867 0 0 0 48917 86 0 0 25 0 1 0 492087084 119394304 26509 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29149 26509 603 41 0 29108 0
vsize: 116596
[startup+500.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 27116 0 0 0 49916 87 0 0 25 0 1 0 492087084 120336384 26758 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29379 26758 603 41 0 29338 0
vsize: 117516
[startup+510.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 27437 0 0 0 50915 88 0 0 25 0 1 0 492087084 121671680 27079 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29705 27079 603 41 0 29664 0
vsize: 118820
[startup+520.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 27791 0 0 0 51914 89 0 0 25 0 1 0 492087084 123162624 27433 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30069 27433 603 41 0 30028 0
vsize: 120276
[startup+530.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 28073 0 0 0 52914 90 0 0 25 0 1 0 492087084 124227584 27715 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30329 27715 603 41 0 30288 0
vsize: 121316
[startup+540.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 28421 0 0 0 53913 91 0 0 25 0 1 0 492087084 125714432 28063 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30692 28063 603 41 0 30651 0
vsize: 122768
[startup+550.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 28658 0 0 0 54913 92 0 0 25 0 1 0 492087084 126636032 28300 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30917 28300 603 41 0 30876 0
vsize: 123668
[startup+560.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 28944 0 0 0 55912 92 0 0 25 0 1 0 492087084 127848448 28586 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31213 28586 603 41 0 31172 0
vsize: 124852
[startup+570.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 29201 0 0 0 56912 93 0 0 25 0 1 0 492087084 128933888 28843 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31478 28843 603 41 0 31437 0
vsize: 125912
[startup+580.019 s]
Raw data (loadavg): 1.00 0.99 0.91 3/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 29484 0 0 0 57911 93 0 0 25 0 1 0 492087084 130007040 29126 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31740 29126 603 41 0 31699 0
vsize: 126960
[startup+590.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 29844 0 0 0 58910 94 0 0 25 0 1 0 492087084 131477504 29486 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32099 29486 603 41 0 32058 0
vsize: 128396
[startup+600.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 30108 0 0 0 59909 95 0 0 25 0 1 0 492087084 132558848 29750 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32363 29750 603 41 0 32322 0
vsize: 129452
[startup+610.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 30530 0 0 0 60908 97 0 0 25 0 1 0 492087084 134303744 30172 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32789 30172 603 41 0 32748 0
vsize: 131156
[startup+620.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 30871 0 0 0 61907 98 0 0 25 0 1 0 492087084 135647232 30513 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33117 30513 603 41 0 33076 0
vsize: 132468
[startup+630.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 31195 0 0 0 62906 99 0 0 25 0 1 0 492087084 137003008 30837 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33448 30837 603 41 0 33407 0
vsize: 133792
[startup+640.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 31586 0 0 0 63905 100 0 0 25 0 1 0 492087084 138604544 31228 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33839 31228 603 41 0 33798 0
vsize: 135356
[startup+650.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 31902 0 0 0 64904 101 0 0 25 0 1 0 492087084 139943936 31544 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34166 31544 603 41 0 34125 0
vsize: 136664
[startup+660.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 32121 0 0 0 65904 102 0 0 25 0 1 0 492087084 140746752 31763 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34362 31763 603 41 0 34321 0
vsize: 137448
[startup+670.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 32468 0 0 0 66903 103 0 0 25 0 1 0 492087084 142229504 32110 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34724 32110 603 41 0 34683 0
vsize: 138896
[startup+680.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 32768 0 0 0 67902 103 0 0 25 0 1 0 492087084 143429632 32410 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35017 32410 603 41 0 34976 0
vsize: 140068
[startup+690.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 33009 0 0 0 68902 104 0 0 25 0 1 0 492087084 144502784 32651 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35279 32651 603 41 0 35238 0
vsize: 141116
[startup+700.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 33246 0 0 0 69902 105 0 0 25 0 1 0 492087084 145436672 32888 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35507 32888 603 41 0 35466 0
vsize: 142028
[startup+710.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 33542 0 0 0 70901 105 0 0 25 0 1 0 492087084 146653184 33184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35804 33184 603 41 0 35763 0
vsize: 143216
[startup+720.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 33827 0 0 0 71900 106 0 0 25 0 1 0 492087084 147730432 33469 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36067 33469 603 41 0 36026 0
vsize: 144268
[startup+730.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 34154 0 0 0 72900 107 0 0 25 0 1 0 492087084 149061632 33796 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36392 33796 603 41 0 36351 0
vsize: 145568
[startup+740.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 34464 0 0 0 73900 107 0 0 25 0 1 0 492087084 150409216 34106 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36721 34106 603 41 0 36680 0
vsize: 146884
[startup+750.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 34748 0 0 0 74900 108 0 0 25 0 1 0 492087084 151605248 34390 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37013 34390 603 41 0 36972 0
vsize: 148052
[startup+760.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 35115 0 0 0 75899 109 0 0 25 0 1 0 492087084 153079808 34757 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37373 34757 603 41 0 37332 0
vsize: 149492
[startup+770.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 35359 0 0 0 76898 109 0 0 25 0 1 0 492087084 154021888 35001 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37603 35001 603 41 0 37562 0
vsize: 150412
[startup+780.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 35694 0 0 0 77897 110 0 0 25 0 1 0 492087084 155369472 35336 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37932 35336 603 41 0 37891 0
vsize: 151728
[startup+790.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 36068 0 0 0 78896 112 0 0 25 0 1 0 492087084 156975104 35710 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38324 35710 603 41 0 38283 0
vsize: 153296
[startup+800.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 36326 0 0 0 79895 113 0 0 25 0 1 0 492087084 158044160 35968 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38585 35968 603 41 0 38544 0
vsize: 154340
[startup+810.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 36607 0 0 0 80894 114 0 0 25 0 1 0 492087084 159121408 36249 4294967295 134512640 134672761 3221224544 3221223680 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38848 36249 603 41 0 38807 0
vsize: 155392
[startup+820.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 36885 0 0 0 81893 115 0 0 25 0 1 0 492087084 160346112 36527 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39147 36527 603 41 0 39106 0
vsize: 156588
[startup+830.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 37250 0 0 0 82892 116 0 0 25 0 1 0 492087084 161800192 36892 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39502 36892 603 41 0 39461 0
vsize: 158008
[startup+840.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 37713 0 0 0 83892 117 0 0 25 0 1 0 492087084 163676160 37355 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39960 37355 603 41 0 39919 0
vsize: 159840
[startup+850.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 38109 0 0 0 84891 118 0 0 25 0 1 0 492087084 165302272 37751 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40357 37751 603 41 0 40316 0
vsize: 161428
[startup+860.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 38434 0 0 0 85890 119 0 0 25 0 1 0 492087084 166649856 38076 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40686 38076 603 41 0 40645 0
vsize: 162744
[startup+870.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 38719 0 0 0 86890 119 0 0 25 0 1 0 492087084 167727104 38361 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40949 38361 603 41 0 40908 0
vsize: 163796
[startup+880.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 39036 0 0 0 87889 120 0 0 25 0 1 0 492087084 169078784 38678 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41279 38678 603 41 0 41238 0
vsize: 165116
[startup+890.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 39302 0 0 0 88889 121 0 0 25 0 1 0 492087084 170160128 38944 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41543 38944 603 41 0 41502 0
vsize: 166172
[startup+900.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 39669 0 0 0 89889 121 0 0 25 0 1 0 492087084 171634688 39311 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41903 39311 603 41 0 41862 0
vsize: 167612
[startup+910.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 40074 0 0 0 90888 122 0 0 25 0 1 0 492087084 173252608 39716 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42298 39716 603 41 0 42257 0
vsize: 169192
[startup+920.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 40493 0 0 0 91888 123 0 0 25 0 1 0 492087084 175013888 40135 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42728 40135 603 41 0 42687 0
vsize: 170912
[startup+930.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 40885 0 0 0 92887 124 0 0 25 0 1 0 492087084 176619520 40527 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43120 40527 603 41 0 43079 0
vsize: 172480
[startup+940.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 41334 0 0 0 93886 125 0 0 25 0 1 0 492087084 178511872 40976 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43582 40976 603 41 0 43541 0
vsize: 174328
[startup+950.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 41738 0 0 0 94885 126 0 0 25 0 1 0 492087084 180113408 41380 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43973 41380 603 41 0 43932 0
vsize: 175892
[startup+960.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 42146 0 0 0 95885 126 0 0 25 0 1 0 492087084 181837824 41788 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44394 41788 603 41 0 44353 0
vsize: 177576
[startup+970.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 42446 0 0 0 96885 127 0 0 25 0 1 0 492087084 183050240 42088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44690 42088 603 41 0 44649 0
vsize: 178760
[startup+980.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 42687 0 0 0 97884 127 0 0 25 0 1 0 492087084 183975936 42329 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44916 42329 603 41 0 44875 0
vsize: 179664
[startup+990.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 43000 0 0 0 98883 129 0 0 25 0 1 0 492087084 185192448 42642 4294967295 134512640 134672761 3221224544 3221223648 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45213 42642 603 41 0 45172 0
vsize: 180852
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 43331 0 0 0 99883 129 0 0 25 0 1 0 492087084 186675200 42973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45575 42973 603 41 0 45534 0
vsize: 182300
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 43684 0 0 0 100882 130 0 0 25 0 1 0 492087084 188026880 43326 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45905 43326 603 41 0 45864 0
vsize: 183620
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 44034 0 0 0 101882 131 0 0 25 0 1 0 492087084 189497344 43676 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46264 43676 603 41 0 46223 0
vsize: 185056
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 44429 0 0 0 102880 132 0 0 25 0 1 0 492087084 191107072 44071 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46657 44071 603 41 0 46616 0
vsize: 186628
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 44691 0 0 0 103879 133 0 0 25 0 1 0 492087084 192716800 44333 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47050 44333 603 41 0 47009 0
vsize: 188200
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 44977 0 0 0 104878 134 0 0 25 0 1 0 492087084 193921024 44619 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47344 44619 603 41 0 47303 0
vsize: 189376
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 45248 0 0 0 105878 134 0 0 25 0 1 0 492087084 194985984 44890 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47604 44890 603 41 0 47563 0
vsize: 190416
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 45527 0 0 0 106877 135 0 0 25 0 1 0 492087084 196067328 45169 4294967295 134512640 134672761 3221224544 3221223668 134566125 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47868 45169 603 41 0 47827 0
vsize: 191472
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 45820 0 0 0 107877 135 0 0 25 0 1 0 492087084 197283840 45462 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48165 45462 603 41 0 48124 0
vsize: 192660
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 46171 0 0 0 108876 136 0 0 25 0 1 0 492087084 198750208 45813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48523 45813 603 41 0 48482 0
vsize: 194092
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 46524 0 0 0 109876 137 0 0 25 0 1 0 492087084 200228864 46166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48884 46166 603 41 0 48843 0
vsize: 195536
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 46859 0 0 0 110875 138 0 0 25 0 1 0 492087084 201568256 46501 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49211 46501 603 41 0 49170 0
vsize: 196844
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 47109 0 0 0 111875 138 0 0 25 0 1 0 492087084 202645504 46751 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49474 46751 603 41 0 49433 0
vsize: 197896
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 47329 0 0 0 112874 139 0 0 25 0 1 0 492087084 203448320 46971 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49670 46971 603 41 0 49629 0
vsize: 198680
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 47616 0 0 0 113874 140 0 0 25 0 1 0 492087084 204652544 47258 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49964 47258 603 41 0 49923 0
vsize: 199856
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 47959 0 0 0 114873 140 0 0 25 0 1 0 492087084 206000128 47601 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50293 47601 603 41 0 50252 0
vsize: 201172
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 48319 0 0 0 115873 142 0 0 25 0 1 0 492087084 207462400 47961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50650 47961 603 41 0 50609 0
vsize: 202600
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 48614 0 0 0 116873 143 0 0 25 0 1 0 492087084 208674816 48256 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50946 48256 603 41 0 50905 0
vsize: 203784
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 48905 0 0 0 117873 144 0 0 25 0 1 0 492087084 209891328 48547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51243 48547 603 41 0 51202 0
vsize: 204972
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 49218 0 0 0 118872 144 0 0 25 0 1 0 492087084 211238912 48860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51572 48860 603 41 0 51531 0
vsize: 206288
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 25910
Raw data (stat): 25906 (minisat+) R 25905 10720 10719 0 -1 0 49521 0 0 0 119871 146 0 0 25 0 1 0 492087084 212434944 49163 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51864 49163 603 41 0 51823 0
vsize: 207456
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 25910
Raw data (stat): 25906 (minisat+) Z 25905 10720 10719 0 -1 12 49523 0 0 0 119871 155 0 0 23 0 1 0 492087084 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.27
CPU user time (s): 1198.72
CPU system time (s): 1.55176
CPU usage (%): 100.008
Max. virtual memory (Kb): 207456
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####