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 17150

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        795076 kB
Buffers:         23904 kB
Cached:         186912 kB
SwapCached:        596 kB
Active:          83452 kB
Inactive:       130880 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        794824 kB
SwapTotal:     2097892 kB
SwapFree:      2097284 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6628 kB
Slab:            19412 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 10:05:10 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 11661 7 1200.31 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   63
c ---[1640]---> BDD-cost:   23
c ---[1638]---> BDD-cost:   29
c ---[1636]---> BDD-cost:    0
c ---[1634]---> BDD-cost:   71
c ---[1632]---> BDD-cost:   55
c ---[1628]---> BDD-cost:   23
c ---[1626]---> BDD-cost:   47
c ---[1624]---> BDD-cost:  213
c ---[1622]---> BDD-cost:   75
c ---[1620]---> BDD-cost:   75
c ---[1618]---> BDD-cost:   55
c ---[1616]---> BDD-cost:   15
c ---[1614]---> BDD-cost:   87
c ---[1612]---> BDD-cost:   51
c ---[1610]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1606]---> BDD-cost:   23
c ---[1604]---> BDD-cost:   11
c ---[1602]---> BDD-cost:   39
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:  259
c ---[1594]---> BDD-cost:  189
c ---[1592]---> BDD-cost:  101
c ---[1588]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  101
c ---[1582]---> BDD-cost:   37
c ---[1580]---> BDD-cost:  181
c ---[1578]---> BDD-cost:  283
c ---[1576]---> BDD-cost:   99
c ---[1574]---> BDD-cost:    1
c ---[1572]---> BDD-cost:  109
c ---[1570]---> BDD-cost:   75
c ---[1568]---> BDD-cost:  237
c ---[1566]---> BDD-cost:  119
c ---[1564]---> BDD-cost:  109
c ---[1562]---> BDD-cost:   83
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:  157
c ---[1556]---> BDD-cost:  155
c ---[1554]---> BDD-cost:  109
c ---[1550]---> BDD-cost:   77
c ---[1548]---> BDD-cost:  133
c ---[1546]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  115
c ---[1542]---> BDD-cost:  185
c ---[1540]---> BDD-cost:  203
c ---[1538]---> BDD-cost:  167
c ---[1536]---> BDD-cost:  135
c ---[1534]---> BDD-cost:    9
c ---[1532]---> BDD-cost:   85
c ---[1530]---> BDD-cost:  143
c ---[1528]---> BDD-cost:  135
c ---[1526]---> BDD-cost:   63
c ---[1524]---> BDD-cost:   51
c ---[1522]---> BDD-cost:  159
c ---[1520]---> BDD-cost:  155
c ---[1518]---> BDD-cost:  211
c ---[1516]---> BDD-cost:   75
c ---[1514]---> BDD-cost:   37
c ---[1512]---> BDD-cost:   87
c ---[1510]---> BDD-cost:   79
c ---[1508]---> BDD-cost:  109
c ---[1506]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  247
c ---[1502]---> BDD-cost:  105
c ---[1500]---> BDD-cost:   59
c ---[1498]---> BDD-cost:   71
c ---[1496]---> BDD-cost:   61
c ---[1494]---> BDD-cost:   89
c ---[1492]---> BDD-cost:   91
c ---[1490]---> BDD-cost:  143
c ---[1488]---> BDD-cost:  111
c ---[1486]---> BDD-cost:   95
c ---[1484]---> BDD-cost:  169
c ---[1482]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  151
c ---[1478]---> BDD-cost:   67
c ---[1476]---> BDD-cost:   45
c ---[1474]---> BDD-cost:   45
c ---[1472]---> BDD-cost:   45
c ---[1470]---> BDD-cost:   65
c ---[1468]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   47
c ---[1460]---> BDD-cost:   29
c ---[1458]---> BDD-cost:   27
c ---[1456]---> BDD-cost:   11
c ---[1452]---> BDD-cost:   81
c ---[1450]---> BDD-cost:  233
c ---[1448]---> BDD-cost:  275
c ---[1446]---> BDD-cost:  289
c ---[1444]---> BDD-cost:  119
c ---[1442]---> BDD-cost:  145
c ---[1440]---> BDD-cost:  165
c ---[1438]---> BDD-cost:  239
c ---[1436]---> BDD-cost:  223
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   35
c ---[1430]---> BDD-cost:   93
c ---[1428]---> BDD-cost:   45
c ---[1426]---> BDD-cost:   73
c ---[1424]---> BDD-cost:   75
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   99
c ---[1416]---> BDD-cost:  187
c ---[1414]---> BDD-cost:   55
c ---[1412]---> BDD-cost:  107
c ---[1410]---> BDD-cost:   69
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:    3
c ---[1404]---> BDD-cost:  149
c ---[1402]---> BDD-cost:  137
c ---[1400]---> BDD-cost:  195
c ---[1398]---> BDD-cost:   93
c ---[1396]---> BDD-cost:  157
c ---[1394]---> BDD-cost:  233
c ---[1392]---> BDD-cost:  223
c ---[1390]---> BDD-cost:  225
c ---[1388]---> BDD-cost:  247
c ---[1386]---> BDD-cost:  179
c ---[1384]---> BDD-cost:  225
c ---[1382]---> BDD-cost:  243
c ---[1380]---> BDD-cost:  199
c ---[1378]---> BDD-cost:   55
c ---[1376]---> BDD-cost:   57
c ---[1374]---> BDD-cost:   99
c ---[1372]---> BDD-cost:    9
c ---[1370]---> BDD-cost:    3
c ---[1368]---> BDD-cost:   23
c ---[1366]---> BDD-cost:   51
c ---[1364]---> BDD-cost:   25
c ---[1362]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   27
c ---[1358]---> BDD-cost:   15
c ---[1356]---> BDD-cost:   37
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   67
c ---[1350]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  211
c ---[1342]---> BDD-cost:   65
c ---[1340]---> BDD-cost:  117
c ---[1338]---> BDD-cost:   65
c ---[1336]---> BDD-cost:   65
c ---[1334]---> BDD-cost:   49
c ---[1332]---> BDD-cost:  439
c ---[1330]---> BDD-cost:  423
c ---[1328]---> BDD-cost:  287
c ---[1326]---> BDD-cost:  217
c ---[1324]---> BDD-cost:  195
c ---[1322]---> BDD-cost:   63
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:  359
c ---[1316]---> BDD-cost:  353
c ---[1312]---> BDD-cost:  169
c ---[1310]---> BDD-cost:  139
c ---[1308]---> BDD-cost:  159
c ---[1306]---> BDD-cost:  223
c ---[1304]---> BDD-cost:  107
c ---[1302]---> BDD-cost:   75
c ---[1300]---> BDD-cost:  109
c ---[1298]---> BDD-cost:   93
c ---[1296]---> BDD-cost:   87
c ---[1294]---> BDD-cost:   87
c ---[1292]---> BDD-cost:    7
c ---[1288]---> BDD-cost:   73
c ---[1286]---> BDD-cost:   71
c ---[1284]---> BDD-cost:  107
c ---[1282]---> BDD-cost:   77
c ---[1280]---> BDD-cost:    3
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  131
c ---[1274]---> BDD-cost:  135
c ---[1272]---> BDD-cost:   65
c ---[1270]---> BDD-cost:  165
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:    1
c ---[1264]---> BDD-cost:   87
c ---[1262]---> BDD-cost:  155
c ---[1260]---> BDD-cost:  167
c ---[1258]---> BDD-cost:  203
c ---[1256]---> BDD-cost:  231
c ---[1254]---> BDD-cost:  147
c ---[1252]---> BDD-cost:  135
c ---[1250]---> BDD-cost:   49
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   95
c ---[1244]---> BDD-cost:  325
c ---[1242]---> BDD-cost:  333
c ---[1240]---> BDD-cost:  173
c ---[1238]---> BDD-cost:  269
c ---[1236]---> BDD-cost:   31
c ---[1234]---> BDD-cost:  413
c ---[1232]---> BDD-cost:  313
c ---[1230]---> BDD-cost:  125
c ---[1228]---> BDD-cost:  113
c ---[1226]---> BDD-cost:  247
c ---[1224]---> BDD-cost:   57
c ---[1222]---> BDD-cost:  237
c ---[1220]---> BDD-cost:  159
c ---[1218]---> BDD-cost:  117
c ---[1216]---> BDD-cost:   43
c ---[1214]---> BDD-cost:  143
c ---[1212]---> BDD-cost:   65
c ---[1210]---> BDD-cost:  123
c ---[1208]---> BDD-cost:   61
c ---[1206]---> BDD-cost:  103
c ---[1204]---> BDD-cost:   85
c ---[1202]---> BDD-cost:   77
c ---[1200]---> BDD-cost:   57
c ---[1198]---> BDD-cost:  127
c ---[1196]---> BDD-cost:  157
c ---[1194]---> BDD-cost:  267
c ---[1192]---> BDD-cost:  223
c ---[1190]---> BDD-cost:  229
c ---[1188]---> BDD-cost:  257
c ---[1186]---> BDD-cost:  241
c ---[1184]---> BDD-cost:  195
c ---[1182]---> BDD-cost:   49
c ---[1180]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  197
c ---[1176]---> BDD-cost:  171
c ---[1174]---> BDD-cost:  287
c ---[1172]---> BDD-cost:   75
c ---[1170]---> BDD-cost:  215
c ---[1168]---> BDD-cost:  119
c ---[1166]---> BDD-cost:  245
c ---[1164]---> BDD-cost:  257
c ---[1162]---> BDD-cost:  279
c ---[1160]---> BDD-cost:  227
c ---[1158]---> BDD-cost:  201
c ---[1156]---> BDD-cost:  143
c ---[1154]---> BDD-cost:  207
c ---[1152]---> BDD-cost:  131
c ---[1150]---> BDD-cost:  245
c ---[1148]---> BDD-cost:  115
c ---[1146]---> BDD-cost:   91
c ---[1144]---> BDD-cost:   43
c ---[1142]---> BDD-cost:   39
c ---[1140]---> BDD-cost:   91
c ---[1138]---> BDD-cost:  179
c ---[1136]---> BDD-cost:   73
c ---[1134]---> BDD-cost:   29
c ---[1132]---> BDD-cost:  163
c ---[1130]---> BDD-cost:   81
c ---[1128]---> BDD-cost:   63
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  113
c ---[1122]---> BDD-cost:  115
c ---[1120]---> BDD-cost:   19
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   99
c ---[1114]---> BDD-cost:   99
c ---[1112]---> BDD-cost:  103
c ---[1110]---> BDD-cost:   67
c ---[1108]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   85
c ---[1104]---> BDD-cost:   87
c ---[1102]---> BDD-cost:    7
c ---[1100]---> BDD-cost:   45
c ---[1098]---> BDD-cost:   43
c ---[1096]---> BDD-cost:   11
c ---[1094]---> BDD-cost:   59
c ---[1092]---> BDD-cost:  185
c ---[1090]---> BDD-cost:  249
c ---[1088]---> BDD-cost:  315
c ---[1086]---> BDD-cost:  253
c ---[1084]---> BDD-cost:  161
c ---[1082]---> BDD-cost:  257
c ---[1080]---> BDD-cost:  167
c ---[1078]---> BDD-cost:  167
c ---[1076]---> BDD-cost:  141
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   95
c ---[1068]---> BDD-cost:  141
c ---[1066]---> BDD-cost:  123
c ---[1064]---> BDD-cost:   83
c ---[1062]---> BDD-cost:   55
c ---[1060]---> BDD-cost:  183
c ---[1058]---> BDD-cost:  269
c ---[1056]---> BDD-cost:   63
c ---[1054]---> BDD-cost:   45
c ---[1052]---> BDD-cost:   39
c ---[1050]---> BDD-cost:   97
c ---[1048]---> BDD-cost:   51
c ---[1046]---> BDD-cost:   45
c ---[1044]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   85
c ---[1040]---> BDD-cost:   35
c ---[1038]---> BDD-cost:   53
c ---[1036]---> BDD-cost:   21
c ---[1034]---> BDD-cost:  115
c ---[1032]---> BDD-cost:   99
c ---[1030]---> BDD-cost:   63
c ---[1028]---> BDD-cost:   77
c ---[1026]---> BDD-cost:  139
c ---[1024]---> BDD-cost:  109
c ---[1022]---> BDD-cost:  407
c ---[1020]---> BDD-cost:  323
c ---[1018]---> BDD-cost:  109
c ---[1016]---> BDD-cost:   93
c ---[1014]---> BDD-cost:   51
c ---[1012]---> BDD-cost:   79
c ---[1010]---> BDD-cost:   75
c ---[1008]---> BDD-cost:  147
c ---[1006]---> BDD-cost:  169
c ---[1004]---> BDD-cost:  209
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   51
c ---[ 998]---> BDD-cost:   85
c ---[ 994]---> BDD-cost:  103
c ---[ 992]---> BDD-cost:  127
c ---[ 990]---> BDD-cost:   77
c ---[ 988]---> BDD-cost:   77
c ---[ 986]---> BDD-cost:  141
c ---[ 984]---> BDD-cost:   89
c ---[ 982]---> BDD-cost:   85
c ---[ 980]---> BDD-cost:  119
c ---[ 978]---> BDD-cost:   69
c ---[ 976]---> BDD-cost:   57
c ---[ 974]---> BDD-cost:   65
c ---[ 972]---> BDD-cost:   47
c ---[ 970]---> BDD-cost:   61
c ---[ 968]---> BDD-cost:   31
c ---[ 964]---> BDD-cost:  183
c ---[ 962]---> BDD-cost:  121
c ---[ 960]---> BDD-cost:   89
c ---[ 958]---> BDD-cost:  225
c ---[ 956]---> BDD-cost:  267
c ---[ 952]---> BDD-cost:  159
c ---[ 950]---> BDD-cost:  209
c ---[ 948]---> BDD-cost:   71
c ---[ 946]---> BDD-cost:  237
c ---[ 944]---> BDD-cost:  129
c ---[ 942]---> BDD-cost:  365
c ---[ 940]---> BDD-cost:  369
c ---[ 938]---> BDD-cost:  129
c ---[ 936]---> BDD-cost:  101
c ---[ 934]---> BDD-cost:  289
c ---[ 932]---> BDD-cost:  279
c ---[ 930]---> BDD-cost:  345
c ---[ 928]---> BDD-cost:   81
c ---[ 926]---> BDD-cost:   69
c ---[ 924]---> BDD-cost:   83
c ---[ 922]---> BDD-cost:   53
c ---[ 920]---> BDD-cost:   67
c ---[ 918]---> BDD-cost:   55
c ---[ 916]---> BDD-cost:  145
c ---[ 914]---> BDD-cost:  149
c ---[ 912]---> BDD-cost:  105
c ---[ 910]---> BDD-cost:   19
c ---[ 908]---> BDD-cost:  105
c ---[ 906]---> BDD-cost:  101
c ---[ 904]---> BDD-cost:  147
c ---[ 902]---> BDD-cost:  231
c ---[ 900]---> BDD-cost:  191
c ---[ 898]---> BDD-cost:  157
c ---[ 896]---> BDD-cost:  249
c ---[ 894]---> BDD-cost:  385
c ---[ 892]---> BDD-cost:   67
c ---[ 890]---> BDD-cost:   71
c ---[ 888]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:  147
c ---[ 884]---> BDD-cost:  139
c ---[ 882]---> BDD-cost:  273
c ---[ 880]---> BDD-cost:  213
c ---[ 878]---> BDD-cost:  169
c ---[ 876]---> BDD-cost:  239
c ---[ 874]---> BDD-cost:  305
c ---[ 872]---> BDD-cost:  109
c ---[ 870]---> BDD-cost:  105
c ---[ 868]---> BDD-cost:  147
c ---[ 866]---> BDD-cost:  115
c ---[ 864]---> BDD-cost:  115
c ---[ 862]---> BDD-cost:   67
c ---[ 860]---> BDD-cost:  329
c ---[ 858]---> BDD-cost:  295
c ---[ 856]---> BDD-cost:   51
c ---[ 854]---> BDD-cost:   61
c ---[ 852]---> BDD-cost:  317
c ---[ 850]---> BDD-cost:   97
c ---[ 848]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:   43
c ---[ 844]---> BDD-cost:   85
c ---[ 842]---> BDD-cost:   35
c ---[ 840]---> BDD-cost:   69
c ---[ 836]---> BDD-cost:   45
c ---[ 834]---> BDD-cost:   73
c ---[ 832]---> BDD-cost:   55
c ---[ 828]---> BDD-cost:   33
c ---[ 826]---> BDD-cost:   29
c ---[ 824]---> BDD-cost:  245
c ---[ 822]---> BDD-cost:  225
c ---[ 820]---> BDD-cost:  111
c ---[ 818]---> BDD-cost:  117
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  129
c ---[ 812]---> BDD-cost:  259
c ---[ 810]---> BDD-cost:  221
c ---[ 808]---> BDD-cost:  275
c ---[ 806]---> BDD-cost:  209
c ---[ 804]---> BDD-cost:  267
c ---[ 802]---> BDD-cost:  171
c ---[ 800]---> BDD-cost:   57
c ---[ 796]---> BDD-cost:  133
c ---[ 794]---> BDD-cost:  185
c ---[ 792]---> BDD-cost:  169
c ---[ 790]---> BDD-cost:  287
c ---[ 788]---> BDD-cost:   81
c ---[ 786]---> BDD-cost:  335
c ---[ 784]---> BDD-cost:  365
c ---[ 782]---> BDD-cost:  255
c ---[ 780]---> BDD-cost:  111
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  101
c ---[ 774]---> BDD-cost:  197
c ---[ 772]---> BDD-cost:  383
c ---[ 770]---> BDD-cost:  329
c ---[ 768]---> BDD-cost:  241
c ---[ 766]---> BDD-cost:  129
c ---[ 764]---> BDD-cost:   85
c ---[ 762]---> BDD-cost:   71
c ---[ 760]---> BDD-cost:   37
c ---[ 758]---> BDD-cost:   77
c ---[ 756]---> BDD-cost:   49
c ---[ 754]---> BDD-cost:  133
c ---[ 752]---> BDD-cost:  133
c ---[ 750]---> BDD-cost:  377
c ---[ 748]---> BDD-cost:  117
c ---[ 744]---> BDD-cost:  119
c ---[ 742]---> BDD-cost:  119
c ---[ 740]---> BDD-cost:  151
c ---[ 738]---> BDD-cost:  221
c ---[ 736]---> BDD-cost:  181
c ---[ 732]---> BDD-cost:   87
c ---[ 730]---> BDD-cost:  127
c ---[ 728]---> BDD-cost:  299
c ---[ 726]---> BDD-cost:  331
c ---[ 722]---> BDD-cost:   21
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  217
c ---[ 716]---> BDD-cost:  349
c ---[ 714]---> BDD-cost:  291
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  161
c ---[ 708]---> BDD-cost:   61
c ---[ 706]---> BDD-cost:   55
c ---[ 704]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:  189
c ---[ 698]---> BDD-cost:  157
c ---[ 696]---> BDD-cost:  149
c ---[ 694]---> BDD-cost:  139
c ---[ 692]---> BDD-cost:  165
c ---[ 690]---> BDD-cost:  181
c ---[ 688]---> BDD-cost:  253
c ---[ 686]---> BDD-cost:   43
c ---[ 684]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  141
c ---[ 680]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:   95
c ---[ 676]---> BDD-cost:   75
c ---[ 674]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  149
c ---[ 670]---> BDD-cost:  137
c ---[ 668]---> BDD-cost:   59
c ---[ 666]---> BDD-cost:    5
c ---[ 664]---> BDD-cost:   35
c ---[ 662]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   47
c ---[ 654]---> BDD-cost:   55
c ---[ 652]---> BDD-cost:  197
c ---[ 650]---> BDD-cost:  191
c ---[ 648]---> BDD-cost:  125
c ---[ 646]---> BDD-cost:  173
c ---[ 642]---> BDD-cost:   93
c ---[ 640]---> BDD-cost:   29
c ---[ 638]---> BDD-cost:  321
c ---[ 636]---> BDD-cost:  195
c ---[ 634]---> BDD-cost:  163
c ---[ 628]---> BDD-cost:  151
c ---[ 626]---> BDD-cost:  253
c ---[ 624]---> BDD-cost:  381
c ---[ 622]---> BDD-cost:  345
c ---[ 620]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:   83
c ---[ 614]---> BDD-cost:   69
c ---[ 612]---> BDD-cost:   51
c ---[ 610]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   59
c ---[ 606]---> BDD-cost:   83
c ---[ 604]---> BDD-cost:  107
c ---[ 602]---> BDD-cost:  363
c ---[ 600]---> BDD-cost:  103
c ---[ 598]---> BDD-cost:  277
c ---[ 596]---> BDD-cost:  341
c ---[ 594]---> BDD-cost:  213
c ---[ 592]---> BDD-cost:  315
c ---[ 590]---> BDD-cost:  275
c ---[ 588]---> BDD-cost:  151
c ---[ 586]---> BDD-cost:  111
c ---[ 584]---> BDD-cost:  103
c ---[ 582]---> BDD-cost:   75
c ---[ 580]---> BDD-cost:   27
c ---[ 578]---> BDD-cost:   21
c ---[ 576]---> BDD-cost:   11
c ---[ 574]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:  149
c ---[ 564]---> BDD-cost:   97
c ---[ 562]---> BDD-cost:  149
c ---[ 560]---> BDD-cost:  395
c ---[ 558]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:  389
c ---[ 554]---> BDD-cost:  251
c ---[ 552]---> BDD-cost:  375
c ---[ 550]---> BDD-cost:  343
c ---[ 548]---> BDD-cost:  267
c ---[ 546]---> BDD-cost:  135
c ---[ 544]---> BDD-cost:  263
c ---[ 542]---> BDD-cost:  259
c ---[ 540]---> BDD-cost:  245
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:   41
c ---[ 534]---> BDD-cost:  127
c ---[ 532]---> BDD-cost:  117
c ---[ 530]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:  149
c ---[ 526]---> BDD-cost:  103
c ---[ 524]---> BDD-cost:  215
c ---[ 522]---> BDD-cost:   89
c ---[ 520]---> BDD-cost:  177
c ---[ 518]---> BDD-cost:  343
c ---[ 516]---> BDD-cost:  237
c ---[ 514]---> BDD-cost:  177
c ---[ 512]---> BDD-cost:   85
c ---[ 510]---> BDD-cost:  267
c ---[ 508]---> BDD-cost:  225
c ---[ 506]---> BDD-cost:  109
c ---[ 504]---> BDD-cost:  105
c ---[ 502]---> BDD-cost:  113
c ---[ 500]---> BDD-cost:   55
c ---[ 498]---> BDD-cost:  117
c ---[ 496]---> BDD-cost:   83
c ---[ 494]---> BDD-cost:   79
c ---[ 492]---> BDD-cost:   81
c ---[ 490]---> BDD-cost:  263
c ---[ 488]---> BDD-cost:  179
c ---[ 486]---> BDD-cost:  281
c ---[ 484]---> BDD-cost:  389
c ---[ 482]---> BDD-cost:  333
c ---[ 480]---> BDD-cost:  357
c ---[ 478]---> BDD-cost:  345
c ---[ 476]---> BDD-cost:  263
c ---[ 474]---> BDD-cost:   89
c ---[ 472]---> BDD-cost:  285
c ---[ 468]---> BDD-cost:  419
c ---[ 466]---> BDD-cost:  357
c ---[ 464]---> BDD-cost:  473
c ---[ 462]---> BDD-cost:  455
c ---[ 460]---> BDD-cost:  405
c ---[ 458]---> BDD-cost:  241
c ---[ 456]---> BDD-cost:  211
c ---[ 454]---> BDD-cost:  313
c ---[ 452]---> BDD-cost:  371
c ---[ 450]---> BDD-cost:  389
c ---[ 448]---> BDD-cost:  223
c ---[ 446]---> BDD-cost:  221
c ---[ 444]---> BDD-cost:  147
c ---[ 442]---> BDD-cost:  131
c ---[ 440]---> BDD-cost:  185
c ---[ 438]---> BDD-cost:  141
c ---[ 436]---> BDD-cost:  249
c ---[ 434]---> BDD-cost:  261
c ---[ 432]---> BDD-cost:  311
c ---[ 430]---> BDD-cost:  261
c ---[ 428]---> BDD-cost:  387
c ---[ 426]---> BDD-cost:  247
c ---[ 424]---> BDD-cost:  295
c ---[ 422]---> BDD-cost:   31
c ---[ 420]---> BDD-cost:  355
c ---[ 418]---> BDD-cost:  135
c ---[ 416]---> BDD-cost:  443
c ---[ 414]---> BDD-cost:  653
c ---[ 412]---> BDD-cost:  703
c ---[ 410]---> BDD-cost:  517
c ---[ 408]---> BDD-cost:  441
c ---[ 406]---> BDD-cost:  411
c ---[ 404]---> BDD-cost:  289
c ---[ 402]---> BDD-cost:  277
c ---[ 400]---> BDD-cost:  239
c ---[ 398]---> BDD-cost:  201
c ---[ 396]---> BDD-cost:  309
c ---[ 394]---> BDD-cost:  287
c ---[ 392]---> BDD-cost:  177
c ---[ 390]---> BDD-cost:  143
c ---[ 388]---> BDD-cost:  131
c ---[ 386]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:  189
c ---[ 382]---> BDD-cost:  219
c ---[ 378]---> BDD-cost:  267
c ---[ 376]---> BDD-cost:  135
c ---[ 374]---> BDD-cost:   69
c ---[ 372]---> BDD-cost:   75
c ---[ 370]---> BDD-cost:   51
c ---[ 368]---> BDD-cost:  117
c ---[ 366]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:  189
c ---[ 358]---> BDD-cost:   73
c ---[ 356]---> BDD-cost:   55
c ---[ 354]---> BDD-cost:   57
c ---[ 352]---> BDD-cost:   91
c ---[ 350]---> BDD-cost:  325
c ---[ 348]---> BDD-cost:  223
c ---[ 346]---> BDD-cost:   57
c ---[ 344]---> BDD-cost:   43
c ---[ 342]---> BDD-cost:  255
c ---[ 340]---> BDD-cost:  285
c ---[ 338]---> BDD-cost:  187
c ---[ 336]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   91
c ---[ 332]---> BDD-cost:  211
c ---[ 330]---> BDD-cost:  159
c ---[ 328]---> BDD-cost:   97
c ---[ 326]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:  101
c ---[ 322]---> BDD-cost:  141
c ---[ 318]---> BDD-cost:  109
c ---[ 316]---> BDD-cost:  321
c ---[ 314]---> BDD-cost:  305
c ---[ 312]---> BDD-cost:  603
c ---[ 310]---> BDD-cost:  441
c ---[ 308]---> BDD-cost:  391
c ---[ 306]---> BDD-cost:  387
c ---[ 304]---> BDD-cost:  289
c ---[ 302]---> BDD-cost:  219
c ---[ 300]---> BDD-cost:  309
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  197
c ---[ 294]---> BDD-cost:  279
c ---[ 292]---> BDD-cost:  167
c ---[ 290]---> BDD-cost:  151
c ---[ 288]---> BDD-cost:   49
c ---[ 286]---> BDD-cost:   31
c ---[ 284]---> BDD-cost:  107
c ---[ 282]---> BDD-cost:   55
c ---[ 278]---> BDD-cost:  177
c ---[ 276]---> BDD-cost:  223
c ---[ 274]---> BDD-cost:  119
c ---[ 272]---> BDD-cost:  137
c ---[ 270]---> BDD-cost:  105
c ---[ 268]---> BDD-cost:  183
c ---[ 266]---> BDD-cost:  179
c ---[ 264]---> BDD-cost:  285
c ---[ 262]---> BDD-cost:  191
c ---[ 260]---> BDD-cost:  177
c ---[ 258]---> BDD-cost:  145
c ---[ 254]---> BDD-cost:  153
c ---[ 252]---> BDD-cost:  121
c ---[ 250]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:  111
c ---[ 244]---> BDD-cost:  281
c ---[ 242]---> BDD-cost:  265
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  151
c ---[ 236]---> BDD-cost:  167
c ---[ 234]---> BDD-cost:  137
c ---[ 230]---> BDD-cost:  375
c ---[ 228]---> BDD-cost:  287
c ---[ 226]---> BDD-cost:  249
c ---[ 224]---> BDD-cost:  131
c ---[ 222]---> BDD-cost:  187
c ---[ 220]---> BDD-cost:  135
c ---[ 218]---> BDD-cost:  129
c ---[ 216]---> BDD-cost:  317
c ---[ 214]---> BDD-cost:  365
c ---[ 212]---> BDD-cost:  235
c ---[ 210]---> BDD-cost:  249
c ---[ 208]---> BDD-cost:  283
c ---[ 206]---> BDD-cost:  233
c ---[ 204]---> BDD-cost:  259
c ---[ 202]---> BDD-cost:  287
c ---[ 200]---> BDD-cost:  175
c ---[ 198]---> BDD-cost:  233
c ---[ 196]---> BDD-cost:  167
c ---[ 194]---> BDD-cost:  159
c ---[ 192]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:  135
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:  167
c ---[ 182]---> BDD-cost:  203
c ---[ 180]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  263
c ---[ 176]---> BDD-cost:   31
c ---[ 174]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   31
c ---[ 170]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:  225
c ---[ 166]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  385
c ---[ 162]---> BDD-cost:  361
c ---[ 160]---> BDD-cost:   73
c ---[ 158]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:  131
c ---[ 152]---> BDD-cost:  145
c ---[ 150]---> BDD-cost:  121
c ---[ 148]---> BDD-cost:  117
c ---[ 146]---> BDD-cost:  111
c ---[ 144]---> BDD-cost:  123
c ---[ 142]---> BDD-cost:  125
c ---[ 140]---> BDD-cost:  243
c ---[ 138]---> BDD-cost:  143
c ---[ 136]---> BDD-cost:  149
c ---[ 134]---> BDD-cost:  103
c ---[ 132]---> BDD-cost:  155
c ---[ 130]---> BDD-cost:  247
c ---[ 128]---> BDD-cost:  143
c ---[ 126]---> BDD-cost:   91
c ---[ 124]---> BDD-cost:   81
c ---[ 122]---> BDD-cost:   79
c ---[ 120]---> BDD-cost:  117
c ---[ 118]---> BDD-cost:   89
c ---[ 116]---> BDD-cost:   61
c ---[ 114]---> BDD-cost:  127
c ---[ 112]---> BDD-cost:  135
c ---[ 110]---> BDD-cost:  161
c ---[ 108]---> BDD-cost:  141
c ---[ 106]---> BDD-cost:  437
c ---[ 104]---> BDD-cost:  309
c ---[ 102]---> BDD-cost:  173
c ---[ 100]---> BDD-cost:  441
c ---[  98]---> BDD-cost:  489
c ---[  96]---> BDD-cost:  299
c ---[  94]---> BDD-cost:  455
c ---[  92]---> BDD-cost:  333
c ---[  90]---> BDD-cost:  421
c ---[  88]---> BDD-cost:  375
c ---[  86]---> BDD-cost:  433
c ---[  84]---> BDD-cost:  405
c ---[  82]---> BDD-cost:  333
c ---[  80]---> BDD-cost:  673
c ---[  78]---> BDD-cost:  685
c ---[  76]---> BDD-cost:  385
c ---[  74]---> BDD-cost:  267
c ---[  72]---> BDD-cost:  345
c ---[  70]---> BDD-cost:  365
c ---[  68]---> BDD-cost:  391
c ---[  66]---> BDD-cost:  313
c ---[  64]---> BDD-cost:  275
c ---[  62]---> BDD-cost:  257
c ---[  60]---> BDD-cost:  203
c ---[  58]---> BDD-cost:  311
c ---[  56]---> BDD-cost:  227
c ---[  54]---> BDD-cost:  295
c ---[  52]---> BDD-cost:  233
c ---[  50]---> BDD-cost:  247
c ---[  46]---> BDD-cost:  237
c ---[  44]---> BDD-cost:  149
c ---[  40]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   85
c ---[  36]---> BDD-cost:  109
c ---[  34]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:   71
c ---[  28]---> BDD-cost:   67
c ---[  26]---> BDD-cost:  151
c ---[  24]---> BDD-cost:  147
c ---[  22]---> BDD-cost:  177
c ---[  20]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  147
c ---[  14]---> BDD-cost:  215
c ---[  12]---> BDD-cost:  181
c ---[  10]---> BDD-cost:  235
c ---[   8]---> BDD-cost:  163
c ---[   6]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   59
c ---[   2]---> BDD-cost:  139
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  556705  1546773 |  185568       0        0     nan |  0.000 % |
c |       100 |  556705  1546773 |  204124     100     5588    55.9 |  0.588 % |
c |       250 |  556666  1546664 |  224537     224    12453    55.6 |  0.591 % |
c |       475 |  556616  1546515 |  246991     444    20776    46.8 |  0.598 % |
c |       812 |  556565  1546377 |  271690     777    73035    94.0 |  0.600 % |
c |      1320 |  556565  1546377 |  298859    1285   151800   118.1 |  0.600 % |
c |      2080 |  556078  1545030 |  328745    2010   196008    97.5 |  0.640 % |
c |      3219 |  555916  1544566 |  361619    3142   321129   102.2 |  0.661 % |
c |      4928 |  553857  1538932 |  397781    4711   534915   113.5 |  0.862 % |
c |      7491 |  553675  1538424 |  437559    7252   896739   123.7 |  0.883 % |
c |     11336 |  553504  1537943 |  481315   11064  1318064   119.1 |  0.898 % |
c |     17102 |  552763  1535895 |  529447   16749  2072031   123.7 |  0.964 % |
c |     25752 |  552698  1535712 |  582391   25386  4197786   165.4 |  0.971 % |
c |     38726 |  552330  1534708 |  640631   38106  6393123   167.8 |  0.994 % |
c |     58188 |  552049  1533955 |  704694   57514 10479307   182.2 |  1.004 % |
c |     87380 |  551731  1533099 |  775163   86644 17582579   202.9 |  1.019 % |
c |    131169 |  551531  1532560 |  852679  130381 30406338   233.2 |  1.028 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.95 0.97 0.91 2/55 26396
Raw data (stat): 26396 (runsolver) R 26395 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544109196 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 12985 0 0 0 966 32 0 0 25 0 1 0 544109196 63586304 12627 4294967295 134512640 134672761 3221224544 3221223696 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15524 12627 603 41 0 15483 0
vsize: 62096
[startup+20.0009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 13123 0 0 0 1965 32 0 0 25 0 1 0 544109196 64122880 12765 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15655 12765 603 41 0 15614 0
vsize: 62620
[startup+30.002 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 13291 0 0 0 2964 33 0 0 25 0 1 0 544109196 64794624 12933 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15819 12933 603 41 0 15778 0
vsize: 63276
[startup+40.0014 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 13546 0 0 0 3963 34 0 0 25 0 1 0 544109196 65875968 13188 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16083 13188 603 41 0 16042 0
vsize: 64332
[startup+50.0017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 13780 0 0 0 4962 35 0 0 25 0 1 0 544109196 66822144 13422 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16314 13422 603 41 0 16273 0
vsize: 65256
[startup+60.0016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 13942 0 0 0 5962 35 0 0 25 0 1 0 544109196 67497984 13584 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16479 13584 603 41 0 16438 0
vsize: 65916
[startup+70.0012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 14165 0 0 0 6962 36 0 0 25 0 1 0 544109196 68440064 13807 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16709 13807 603 41 0 16668 0
vsize: 66836
[startup+80.0015 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 14325 0 0 0 7962 36 0 0 25 0 1 0 544109196 68980736 13967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16841 13967 603 41 0 16800 0
vsize: 67364
[startup+90.0014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 14628 0 0 0 8960 37 0 0 25 0 1 0 544109196 70197248 14270 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17138 14270 603 41 0 17097 0
vsize: 68552
[startup+100.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 14835 0 0 0 9960 38 0 0 25 0 1 0 544109196 71139328 14477 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17368 14477 603 41 0 17327 0
vsize: 69472
[startup+110.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 15013 0 0 0 10959 39 0 0 25 0 1 0 544109196 71815168 14655 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17533 14655 603 41 0 17492 0
vsize: 70132
[startup+120.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 15295 0 0 0 11959 40 0 0 25 0 1 0 544109196 73052160 14937 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17835 14937 603 41 0 17794 0
vsize: 71340
[startup+130.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 15626 0 0 0 12958 41 0 0 25 0 1 0 544109196 74391552 15268 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18162 15268 603 41 0 18121 0
vsize: 72648
[startup+140.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 15984 0 0 0 13957 42 0 0 25 0 1 0 544109196 75874304 15626 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18524 15626 603 41 0 18483 0
vsize: 74096
[startup+150.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 16296 0 0 0 14956 43 0 0 25 0 1 0 544109196 77086720 15938 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18820 15938 603 41 0 18779 0
vsize: 75280
[startup+160.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 16580 0 0 0 15956 43 0 0 25 0 1 0 544109196 78303232 16222 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19117 16222 603 41 0 19076 0
vsize: 76468
[startup+170.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 16920 0 0 0 16955 45 0 0 25 0 1 0 544109196 79646720 16562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19445 16562 603 41 0 19404 0
vsize: 77780
[startup+180.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 17227 0 0 0 17954 45 0 0 25 0 1 0 544109196 80863232 16869 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19742 16869 603 41 0 19701 0
vsize: 78968
[startup+190.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 17525 0 0 0 18953 46 0 0 25 0 1 0 544109196 82075648 17167 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20038 17167 603 41 0 19997 0
vsize: 80152
[startup+200.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 17761 0 0 0 19953 47 0 0 25 0 1 0 544109196 83013632 17403 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20267 17403 603 41 0 20226 0
vsize: 81068
[startup+210.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 17964 0 0 0 20953 48 0 0 25 0 1 0 544109196 83951616 17606 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20496 17606 603 41 0 20455 0
vsize: 81984
[startup+220.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 18157 0 0 0 21952 48 0 0 25 0 1 0 544109196 84631552 17799 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20662 17799 603 41 0 20621 0
vsize: 82648
[startup+230.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 18406 0 0 0 22952 48 0 0 25 0 1 0 544109196 85708800 18048 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20925 18048 603 41 0 20884 0
vsize: 83700
[startup+240.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26396
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 18658 0 0 0 23951 49 0 0 25 0 1 0 544109196 86781952 18300 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21187 18300 603 41 0 21146 0
vsize: 84748
[startup+250.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 18854 0 0 0 24951 50 0 0 25 0 1 0 544109196 87576576 18496 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21381 18496 603 41 0 21340 0
vsize: 85524
[startup+260.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 19175 0 0 0 25950 51 0 0 25 0 1 0 544109196 88915968 18817 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21708 18817 603 41 0 21667 0
vsize: 86832
[startup+270.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 19407 0 0 0 26950 51 0 0 25 0 1 0 544109196 89862144 19049 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21939 19049 603 41 0 21898 0
vsize: 87756
[startup+280.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 19612 0 0 0 27949 52 0 0 25 0 1 0 544109196 90669056 19254 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22136 19254 603 41 0 22095 0
vsize: 88544
[startup+290.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 19853 0 0 0 28948 53 0 0 25 0 1 0 544109196 91746304 19495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22399 19495 603 41 0 22358 0
vsize: 89596
[startup+300.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 20138 0 0 0 29948 54 0 0 25 0 1 0 544109196 92819456 19780 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22661 19780 603 41 0 22620 0
vsize: 90644
[startup+310.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 20402 0 0 0 30947 54 0 0 25 0 1 0 544109196 93900800 20044 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22925 20044 603 41 0 22884 0
vsize: 91700
[startup+320.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 20740 0 0 0 31946 55 0 0 25 0 1 0 544109196 95232000 20382 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23250 20382 603 41 0 23209 0
vsize: 93000
[startup+330.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 21062 0 0 0 32945 57 0 0 25 0 1 0 544109196 96579584 20704 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23579 20704 603 41 0 23538 0
vsize: 94316
[startup+340.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 21511 0 0 0 33944 58 0 0 25 0 1 0 544109196 98463744 21153 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24039 21153 603 41 0 23998 0
vsize: 96156
[startup+350.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 21815 0 0 0 34944 58 0 0 25 0 1 0 544109196 99672064 21457 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24334 21457 603 41 0 24293 0
vsize: 97336
[startup+360.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 22118 0 0 0 35944 59 0 0 25 0 1 0 544109196 100888576 21760 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24631 21760 603 41 0 24590 0
vsize: 98524
[startup+370.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 22413 0 0 0 36943 60 0 0 25 0 1 0 544109196 102100992 22055 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24927 22055 603 41 0 24886 0
vsize: 99708
[startup+380.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 22727 0 0 0 37942 60 0 0 25 0 1 0 544109196 103444480 22369 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25255 22369 603 41 0 25214 0
vsize: 101020
[startup+390.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 22959 0 0 0 38942 61 0 0 25 0 1 0 544109196 104386560 22601 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25485 22601 603 41 0 25444 0
vsize: 101940
[startup+400.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 23158 0 0 0 39941 62 0 0 25 0 1 0 544109196 105193472 22800 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25682 22800 603 41 0 25641 0
vsize: 102728
[startup+410.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 23519 0 0 0 40941 63 0 0 25 0 1 0 544109196 106663936 23161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26041 23161 603 41 0 26000 0
vsize: 104164
[startup+420.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 23838 0 0 0 41940 63 0 0 25 0 1 0 544109196 107876352 23480 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26337 23480 603 41 0 26296 0
vsize: 105348
[startup+430.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 24085 0 0 0 42939 64 0 0 25 0 1 0 544109196 108957696 23727 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26601 23727 603 41 0 26560 0
vsize: 106404
[startup+440.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 24322 0 0 0 43939 65 0 0 25 0 1 0 544109196 109907968 23964 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26833 23964 603 41 0 26792 0
vsize: 107332
[startup+450.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 24721 0 0 0 44938 66 0 0 25 0 1 0 544109196 111505408 24363 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27223 24363 603 41 0 27182 0
vsize: 108892
[startup+460.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 24952 0 0 0 45938 66 0 0 25 0 1 0 544109196 112443392 24594 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27452 24594 603 41 0 27411 0
vsize: 109808
[startup+470.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 25248 0 0 0 46937 67 0 0 25 0 1 0 544109196 113668096 24890 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27751 24890 603 41 0 27710 0
vsize: 111004
[startup+480.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 25513 0 0 0 47937 67 0 0 25 0 1 0 544109196 114745344 25155 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25155 603 41 0 27973 0
vsize: 112056
[startup+490.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 25749 0 0 0 48936 68 0 0 25 0 1 0 544109196 115679232 25391 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28242 25391 603 41 0 28201 0
vsize: 112968
[startup+500.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 26098 0 0 0 49936 69 0 0 25 0 1 0 544109196 117420032 25740 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28667 25740 603 41 0 28626 0
vsize: 114668
[startup+510.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 26332 0 0 0 50935 70 0 0 25 0 1 0 544109196 118366208 25974 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28898 25974 603 41 0 28857 0
vsize: 115592
[startup+520.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 26521 0 0 0 51935 70 0 0 25 0 1 0 544109196 119185408 26163 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29098 26163 603 41 0 29057 0
vsize: 116392
[startup+530.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 26752 0 0 0 52934 71 0 0 25 0 1 0 544109196 120127488 26394 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29328 26394 603 41 0 29287 0
vsize: 117312
[startup+540.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26398
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 27017 0 0 0 53933 72 0 0 25 0 1 0 544109196 121200640 26659 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29590 26659 603 41 0 29549 0
vsize: 118360
[startup+550.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 27218 0 0 0 54933 73 0 0 25 0 1 0 544109196 122003456 26860 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29786 26860 603 41 0 29745 0
vsize: 119144
[startup+560.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 27518 0 0 0 55933 73 0 0 25 0 1 0 544109196 123224064 27160 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30084 27160 603 41 0 30043 0
vsize: 120336
[startup+570.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 27780 0 0 0 56932 74 0 0 25 0 1 0 544109196 124301312 27422 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30347 27422 603 41 0 30306 0
vsize: 121388
[startup+580.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 28085 0 0 0 57931 75 0 0 25 0 1 0 544109196 125521920 27727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30645 27727 603 41 0 30604 0
vsize: 122580
[startup+590.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 28356 0 0 0 58931 75 0 0 25 0 1 0 544109196 126603264 27998 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30909 27998 603 41 0 30868 0
vsize: 123636
[startup+600.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 28693 0 0 0 59930 76 0 0 25 0 1 0 544109196 128077824 28335 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31269 28335 603 41 0 31228 0
vsize: 125076
[startup+610.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 28977 0 0 0 60930 77 0 0 25 0 1 0 544109196 129155072 28619 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31532 28619 603 41 0 31491 0
vsize: 126128
[startup+620.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 29314 0 0 0 61929 78 0 0 25 0 1 0 544109196 130498560 28956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31860 28956 603 41 0 31819 0
vsize: 127440
[startup+630.005 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 29566 0 0 0 62929 78 0 0 25 0 1 0 544109196 131575808 29208 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32123 29208 603 41 0 32082 0
vsize: 128492
[startup+640.004 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 29802 0 0 0 63928 79 0 0 25 0 1 0 544109196 132517888 29444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32353 29444 603 41 0 32312 0
vsize: 129412
[startup+650.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 30031 0 0 0 64928 79 0 0 25 0 1 0 544109196 133455872 29673 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32582 29673 603 41 0 32541 0
vsize: 130328
[startup+660.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 30346 0 0 0 65928 80 0 0 25 0 1 0 544109196 134807552 29988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32912 29988 603 41 0 32871 0
vsize: 131648
[startup+670.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 30753 0 0 0 66927 81 0 0 25 0 1 0 544109196 136421376 30395 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33306 30395 603 41 0 33265 0
vsize: 133224
[startup+680.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 31067 0 0 0 67927 82 0 0 25 0 1 0 544109196 137650176 30709 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33606 30709 603 41 0 33565 0
vsize: 134424
[startup+690.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 31337 0 0 0 68926 82 0 0 25 0 1 0 544109196 138858496 30979 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33901 30979 603 41 0 33860 0
vsize: 135604
[startup+700.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 31571 0 0 0 69926 83 0 0 25 0 1 0 544109196 139784192 31213 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34127 31213 603 41 0 34086 0
vsize: 136508
[startup+710.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 31841 0 0 0 70926 83 0 0 25 0 1 0 544109196 140845056 31483 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34386 31483 603 41 0 34345 0
vsize: 137544
[startup+720.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 32087 0 0 0 71925 85 0 0 25 0 1 0 544109196 141791232 31729 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34617 31729 603 41 0 34576 0
vsize: 138468
[startup+730.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 32341 0 0 0 72924 85 0 0 25 0 1 0 544109196 142864384 31983 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34879 31983 603 41 0 34838 0
vsize: 139516
[startup+740.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 32566 0 0 0 73924 86 0 0 25 0 1 0 544109196 143806464 32208 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35109 32208 603 41 0 35068 0
vsize: 140436
[startup+750.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 32863 0 0 0 74923 87 0 0 25 0 1 0 544109196 145018880 32505 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35405 32505 603 41 0 35364 0
vsize: 141620
[startup+760.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 33104 0 0 0 75922 88 0 0 25 0 1 0 544109196 145960960 32746 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35635 32746 603 41 0 35594 0
vsize: 142540
[startup+770.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 33411 0 0 0 76922 89 0 0 25 0 1 0 544109196 147304448 33053 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35963 33053 603 41 0 35922 0
vsize: 143852
[startup+780.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 33774 0 0 0 77921 90 0 0 25 0 1 0 544109196 148787200 33416 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36325 33416 603 41 0 36284 0
vsize: 145300
[startup+790.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 33995 0 0 0 78921 90 0 0 25 0 1 0 544109196 149598208 33637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36523 33637 603 41 0 36482 0
vsize: 146092
[startup+800.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 34253 0 0 0 79920 91 0 0 25 0 1 0 544109196 150679552 33895 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36787 33895 603 41 0 36746 0
vsize: 147148
[startup+810.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 34543 0 0 0 80919 92 0 0 25 0 1 0 544109196 151891968 34185 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37083 34185 603 41 0 37042 0
vsize: 148332
[startup+820.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 34914 0 0 0 81919 93 0 0 25 0 1 0 544109196 153366528 34556 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37443 34556 603 41 0 37402 0
vsize: 149772
[startup+830.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 35194 0 0 0 82917 95 0 0 25 0 1 0 544109196 154578944 34836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37739 34836 603 41 0 37698 0
vsize: 150956
[startup+840.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 26400
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 35463 0 0 0 83918 95 0 0 25 0 1 0 544109196 155656192 35105 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38002 35105 603 41 0 37961 0
vsize: 152008
[startup+850.034 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 26402
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 35787 0 0 0 84917 96 0 0 25 0 1 0 544109196 156987392 35429 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38327 35429 603 41 0 38286 0
vsize: 153308
[startup+860.034 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 26402
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 36049 0 0 0 85917 97 0 0 25 0 1 0 544109196 158117888 35691 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38603 35691 603 41 0 38562 0
vsize: 154412
[startup+870.039 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 26402
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 36416 0 0 0 86917 97 0 0 25 0 1 0 544109196 159596544 36058 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38964 36058 603 41 0 38923 0
vsize: 155856
[startup+880.042 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 26402
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 36714 0 0 0 87917 98 0 0 25 0 1 0 544109196 160813056 36356 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39261 36356 603 41 0 39220 0
vsize: 157044
[startup+890.041 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 26402
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 37022 0 0 0 88917 98 0 0 25 0 1 0 544109196 162009088 36664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39553 36664 603 41 0 39512 0
vsize: 158212
[startup+900.043 s]
Raw data (loadavg): 1.03 1.00 0.92 3/59 26448
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 37349 0 0 0 89916 99 0 0 25 0 1 0 544109196 163368960 36991 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39885 36991 603 41 0 39844 0
vsize: 159540
[startup+910.043 s]
Raw data (loadavg): 1.10 1.02 0.93 2/55 26455
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 37522 0 0 0 90915 99 0 0 25 0 1 0 544109196 164032512 37164 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40047 37164 603 41 0 40006 0
vsize: 160188
[startup+920.042 s]
Raw data (loadavg): 1.08 1.02 0.93 2/55 26455
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 37755 0 0 0 91915 100 0 0 25 0 1 0 544109196 165101568 37397 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40308 37397 603 41 0 40267 0
vsize: 161232
[startup+930.043 s]
Raw data (loadavg): 1.07 1.01 0.93 2/55 26455
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 38026 0 0 0 92914 101 0 0 25 0 1 0 544109196 166178816 37668 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40571 37668 603 41 0 40530 0
vsize: 162284
[startup+940.043 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 26455
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 38433 0 0 0 93913 102 0 0 25 0 1 0 544109196 167796736 38075 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40966 38075 603 41 0 40925 0
vsize: 163864
[startup+950.043 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 26455
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 38740 0 0 0 94912 103 0 0 25 0 1 0 544109196 169005056 38382 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41261 38382 603 41 0 41220 0
vsize: 165044
[startup+960.043 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 26455
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 39257 0 0 0 95911 105 0 0 25 0 1 0 544109196 171155456 38899 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41786 38899 603 41 0 41745 0
vsize: 167144
[startup+970.043 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 26455
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 39605 0 0 0 96909 106 0 0 25 0 1 0 544109196 172634112 39247 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42147 39247 603 41 0 42106 0
vsize: 168588
[startup+980.043 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 39887 0 0 0 97909 107 0 0 25 0 1 0 544109196 173715456 39529 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42411 39529 603 41 0 42370 0
vsize: 169644
[startup+990.042 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 40248 0 0 0 98908 108 0 0 25 0 1 0 544109196 175198208 39890 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42773 39890 603 41 0 42732 0
vsize: 171092
[startup+1000.04 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 40525 0 0 0 99909 108 0 0 25 0 1 0 544109196 176402432 40167 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43067 40167 603 41 0 43026 0
vsize: 172268
[startup+1010.04 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 40812 0 0 0 100908 109 0 0 25 0 1 0 544109196 177475584 40454 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43329 40454 603 41 0 43288 0
vsize: 173316
[startup+1020.04 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 41134 0 0 0 101907 110 0 0 25 0 1 0 544109196 178814976 40776 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43656 40776 603 41 0 43615 0
vsize: 174624
[startup+1030.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 41460 0 0 0 102907 110 0 0 25 0 1 0 544109196 180154368 41102 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43983 41102 603 41 0 43942 0
vsize: 175932
[startup+1040.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 41746 0 0 0 103906 111 0 0 25 0 1 0 544109196 181370880 41388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44280 41388 603 41 0 44239 0
vsize: 177120
[startup+1050.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 42055 0 0 0 104905 112 0 0 25 0 1 0 544109196 182571008 41697 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44573 41698 603 41 0 44532 0
vsize: 178292
[startup+1060.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 42346 0 0 0 105905 112 0 0 25 0 1 0 544109196 183779328 41988 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44868 41988 603 41 0 44827 0
vsize: 179472
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 42539 0 0 0 106905 113 0 0 25 0 1 0 544109196 184590336 42181 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45066 42181 603 41 0 45025 0
vsize: 180264
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 42720 0 0 0 107905 113 0 0 25 0 1 0 544109196 185257984 42362 4294967295 134512640 134672761 3221224544 3221223728 134558658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45229 42362 603 41 0 45188 0
vsize: 180916
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 42935 0 0 0 108904 114 0 0 25 0 1 0 544109196 186191872 42577 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45457 42577 603 41 0 45416 0
vsize: 181828
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 43180 0 0 0 109904 115 0 0 25 0 1 0 544109196 187269120 42822 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45720 42822 603 41 0 45679 0
vsize: 182880
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 43404 0 0 0 110904 116 0 0 25 0 1 0 544109196 188071936 43046 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45916 43046 603 41 0 45875 0
vsize: 183664
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 43661 0 0 0 111904 116 0 0 25 0 1 0 544109196 189149184 43303 4294967295 134512640 134672761 3221224544 3221223728 134559609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46179 43303 603 41 0 46138 0
vsize: 184716
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 43915 0 0 0 112903 117 0 0 25 0 1 0 544109196 190218240 43557 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46440 43557 603 41 0 46399 0
vsize: 185760
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26457
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 44222 0 0 0 113902 118 0 0 25 0 1 0 544109196 191430656 43864 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46736 43864 603 41 0 46695 0
vsize: 186944
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26459
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 44569 0 0 0 114900 120 0 0 25 0 1 0 544109196 192901120 44211 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47095 44211 603 41 0 47054 0
vsize: 188380
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26459
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 44851 0 0 0 115899 121 0 0 25 0 1 0 544109196 194506752 44493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47487 44493 603 41 0 47446 0
vsize: 189948
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26459
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 45198 0 0 0 116898 122 0 0 25 0 1 0 544109196 195993600 44840 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47850 44840 603 41 0 47809 0
vsize: 191400
[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26459
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 45319 0 0 0 117898 123 0 0 25 0 1 0 544109196 196403200 44961 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47950 44961 603 41 0 47909 0
vsize: 191800
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26459
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 45665 0 0 0 118896 124 0 0 25 0 1 0 544109196 197890048 45307 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48313 45307 603 41 0 48272 0
vsize: 193252
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 26459
Raw data (stat): 26396 (minisat+) R 26395 20838 20837 0 -1 0 45919 0 0 0 119896 125 0 0 25 0 1 0 544109196 198971392 45561 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48577 45561 603 41 0 48536 0
vsize: 194308
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 26459
Raw data (stat): 26396 (minisat+) Z 26395 20838 20837 0 -1 12 45921 0 0 0 119896 134 0 0 25 0 1 0 544109196 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.16
CPU time (s): 1200.31
CPU user time (s): 1198.97
CPU system time (s): 1.3448
CPU usage (%): 100.013
Max. virtual memory (Kb): 194308
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####