PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.119981
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 15803

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        777752 kB
Buffers:         28604 kB
Cached:         206224 kB
SwapCached:        316 kB
Active:          48620 kB
Inactive:       188504 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        777500 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            14108 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:08:22 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 16653 7 1200.21 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.82 0.92 0.94 2/54 21386
Raw data (stat): 21386 (runsolver) R 21385 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484455187 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.85 0.92 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 12985 0 0 0 968 31 0 0 25 0 1 0 484455187 63586304 12627 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15524 12627 603 41 0 15483 0
vsize: 62096
[startup+20.0018 s]
Raw data (loadavg): 0.87 0.92 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 13126 0 0 0 1967 32 0 0 25 0 1 0 484455187 64122880 12768 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15655 12768 603 41 0 15614 0
vsize: 62620
[startup+30.0032 s]
Raw data (loadavg): 0.89 0.92 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 13296 0 0 0 2966 32 0 0 25 0 1 0 484455187 64794624 12938 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15819 12938 603 41 0 15778 0
vsize: 63276
[startup+40.0036 s]
Raw data (loadavg): 0.91 0.92 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 13548 0 0 0 3965 33 0 0 25 0 1 0 484455187 65875968 13190 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16083 13190 603 41 0 16042 0
vsize: 64332
[startup+50.0034 s]
Raw data (loadavg): 0.92 0.93 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 13782 0 0 0 4964 34 0 0 25 0 1 0 484455187 66822144 13424 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16314 13424 603 41 0 16273 0
vsize: 65256
[startup+60.0047 s]
Raw data (loadavg): 0.93 0.93 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 13952 0 0 0 5964 35 0 0 25 0 1 0 484455187 67497984 13594 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16479 13594 603 41 0 16438 0
vsize: 65916
[startup+70.0051 s]
Raw data (loadavg): 0.94 0.93 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 14169 0 0 0 6963 36 0 0 25 0 1 0 484455187 68440064 13811 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16709 13811 603 41 0 16668 0
vsize: 66836
[startup+80.0059 s]
Raw data (loadavg): 0.95 0.93 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 14325 0 0 0 7962 37 0 0 25 0 1 0 484455187 68980736 13967 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.0062 s]
Raw data (loadavg): 0.96 0.93 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 14635 0 0 0 8962 38 0 0 25 0 1 0 484455187 70332416 14277 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17171 14277 603 41 0 17130 0
vsize: 68684
[startup+100.006 s]
Raw data (loadavg): 0.96 0.94 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 14840 0 0 0 9961 38 0 0 25 0 1 0 484455187 71139328 14482 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17368 14482 603 41 0 17327 0
vsize: 69472
[startup+110.007 s]
Raw data (loadavg): 0.97 0.94 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 15019 0 0 0 10960 39 0 0 25 0 1 0 484455187 71815168 14661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17533 14661 603 41 0 17492 0
vsize: 70132
[startup+120.008 s]
Raw data (loadavg): 0.97 0.94 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 15313 0 0 0 11959 40 0 0 25 0 1 0 484455187 73052160 14955 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17835 14955 603 41 0 17794 0
vsize: 71340
[startup+130.008 s]
Raw data (loadavg): 0.98 0.94 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 15634 0 0 0 12959 41 0 0 25 0 1 0 484455187 74391552 15276 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18162 15276 603 41 0 18121 0
vsize: 72648
[startup+140.008 s]
Raw data (loadavg): 0.98 0.94 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 16000 0 0 0 13958 42 0 0 25 0 1 0 484455187 75874304 15642 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18524 15642 603 41 0 18483 0
vsize: 74096
[startup+150.008 s]
Raw data (loadavg): 0.98 0.94 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 16310 0 0 0 14957 43 0 0 25 0 1 0 484455187 77086720 15952 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18820 15952 603 41 0 18779 0
vsize: 75280
[startup+160.009 s]
Raw data (loadavg): 0.98 0.94 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 16588 0 0 0 15956 44 0 0 25 0 1 0 484455187 78303232 16230 4294967295 134512640 134672761 3221224544 3221223648 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19117 16230 603 41 0 19076 0
vsize: 76468
[startup+170.009 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 16932 0 0 0 16954 46 0 0 25 0 1 0 484455187 79646720 16574 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19445 16574 603 41 0 19404 0
vsize: 77780
[startup+180.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 17238 0 0 0 17953 47 0 0 25 0 1 0 484455187 80998400 16880 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19775 16880 603 41 0 19734 0
vsize: 79100
[startup+190.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 17535 0 0 0 18952 48 0 0 25 0 1 0 484455187 82210816 17177 4294967295 134512640 134672761 3221224544 3221223744 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20071 17177 603 41 0 20030 0
vsize: 80284
[startup+200.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 17766 0 0 0 19951 49 0 0 25 0 1 0 484455187 83148800 17408 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20300 17408 603 41 0 20259 0
vsize: 81200
[startup+210.012 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 17967 0 0 0 20951 49 0 0 25 0 1 0 484455187 83951616 17609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20496 17609 603 41 0 20455 0
vsize: 81984
[startup+220.012 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 18166 0 0 0 21950 50 0 0 25 0 1 0 484455187 84766720 17808 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20695 17808 603 41 0 20654 0
vsize: 82780
[startup+230.013 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 18418 0 0 0 22948 52 0 0 25 0 1 0 484455187 85708800 18060 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20925 18060 603 41 0 20884 0
vsize: 83700
[startup+240.014 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 18659 0 0 0 23947 53 0 0 25 0 1 0 484455187 86781952 18301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21187 18301 603 41 0 21146 0
vsize: 84748
[startup+250.013 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 18862 0 0 0 24946 55 0 0 25 0 1 0 484455187 87711744 18504 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21414 18504 603 41 0 21373 0
vsize: 85656
[startup+260.014 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 19192 0 0 0 25945 56 0 0 25 0 1 0 484455187 89051136 18834 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21741 18834 603 41 0 21700 0
vsize: 86964
[startup+270.014 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 19428 0 0 0 26945 56 0 0 25 0 1 0 484455187 89997312 19070 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21972 19070 603 41 0 21931 0
vsize: 87888
[startup+280.015 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 19622 0 0 0 27944 57 0 0 25 0 1 0 484455187 90804224 19264 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22169 19264 603 41 0 22128 0
vsize: 88676
[startup+290.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 19872 0 0 0 28944 58 0 0 25 0 1 0 484455187 91746304 19514 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22399 19514 603 41 0 22358 0
vsize: 89596
[startup+300.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 20145 0 0 0 29943 59 0 0 25 0 1 0 484455187 92954624 19787 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22694 19787 603 41 0 22653 0
vsize: 90776
[startup+310.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 20410 0 0 0 30942 60 0 0 25 0 1 0 484455187 94035968 20052 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22958 20052 603 41 0 22917 0
vsize: 91832
[startup+320.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 20748 0 0 0 31941 61 0 0 25 0 1 0 484455187 95367168 20390 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23283 20390 603 41 0 23242 0
vsize: 93132
[startup+330.018 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 21090 0 0 0 32940 62 0 0 25 0 1 0 484455187 96714752 20732 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23612 20732 603 41 0 23571 0
vsize: 94448
[startup+340.018 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 21535 0 0 0 33938 64 0 0 25 0 1 0 484455187 98598912 21177 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24072 21177 603 41 0 24031 0
vsize: 96288
[startup+350.018 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 21833 0 0 0 34937 65 0 0 25 0 1 0 484455187 99807232 21475 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24367 21475 603 41 0 24326 0
vsize: 97468
[startup+360.019 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 22135 0 0 0 35936 66 0 0 25 0 1 0 484455187 101023744 21777 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24664 21777 603 41 0 24623 0
vsize: 98656
[startup+370.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 22413 0 0 0 36935 67 0 0 25 0 1 0 484455187 102100992 22055 4294967295 134512640 134672761 3221224544 3221223712 134561008 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.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 22744 0 0 0 37934 69 0 0 25 0 1 0 484455187 103444480 22386 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25255 22386 603 41 0 25214 0
vsize: 101020
[startup+390.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 22962 0 0 0 38933 70 0 0 25 0 1 0 484455187 104386560 22604 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25485 22604 603 41 0 25444 0
vsize: 101940
[startup+400.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 23172 0 0 0 39932 71 0 0 25 0 1 0 484455187 105193472 22814 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25682 22814 603 41 0 25641 0
vsize: 102728
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 23529 0 0 0 40931 72 0 0 25 0 1 0 484455187 106663936 23171 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26041 23171 603 41 0 26000 0
vsize: 104164
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 23867 0 0 0 41930 73 0 0 25 0 1 0 484455187 108011520 23509 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26370 23509 603 41 0 26329 0
vsize: 105480
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 24102 0 0 0 42929 74 0 0 25 0 1 0 484455187 108957696 23744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26601 23744 603 41 0 26560 0
vsize: 106404
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 24336 0 0 0 43928 75 0 0 25 0 1 0 484455187 109907968 23978 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26833 23978 603 41 0 26792 0
vsize: 107332
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 24749 0 0 0 44927 76 0 0 25 0 1 0 484455187 111640576 24391 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27256 24391 603 41 0 27215 0
vsize: 109024
[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 24971 0 0 0 45926 78 0 0 25 0 1 0 484455187 112578560 24613 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27485 24613 603 41 0 27444 0
vsize: 109940
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 25270 0 0 0 46925 79 0 0 25 0 1 0 484455187 113803264 24912 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27784 24912 603 41 0 27743 0
vsize: 111136
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 25530 0 0 0 47924 79 0 0 25 0 1 0 484455187 114880512 25172 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28047 25172 603 41 0 28006 0
vsize: 112188
[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 25768 0 0 0 48924 80 0 0 25 0 1 0 484455187 115814400 25410 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28275 25410 603 41 0 28234 0
vsize: 113100
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 26126 0 0 0 49923 81 0 0 25 0 1 0 484455187 117555200 25768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28700 25768 603 41 0 28659 0
vsize: 114800
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 26343 0 0 0 50922 82 0 0 25 0 1 0 484455187 118366208 25985 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28898 25985 603 41 0 28857 0
vsize: 115592
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 26526 0 0 0 51922 83 0 0 25 0 1 0 484455187 119185408 26168 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29098 26168 603 41 0 29057 0
vsize: 116392
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 26752 0 0 0 52921 83 0 0 25 0 1 0 484455187 120127488 26394 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29328 26394 603 41 0 29287 0
vsize: 117312
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 27025 0 0 0 53920 84 0 0 25 0 1 0 484455187 121200640 26667 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29590 26667 603 41 0 29549 0
vsize: 118360
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 27223 0 0 0 54920 85 0 0 25 0 1 0 484455187 122003456 26865 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29786 26865 603 41 0 29745 0
vsize: 119144
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 27521 0 0 0 55919 86 0 0 25 0 1 0 484455187 123224064 27163 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30084 27163 603 41 0 30043 0
vsize: 120336
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 27779 0 0 0 56918 87 0 0 25 0 1 0 484455187 124301312 27421 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30347 27421 603 41 0 30306 0
vsize: 121388
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 28080 0 0 0 57918 88 0 0 25 0 1 0 484455187 125521920 27722 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30645 27722 603 41 0 30604 0
vsize: 122580
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 28350 0 0 0 58917 88 0 0 25 0 1 0 484455187 126603264 27992 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30909 27992 603 41 0 30868 0
vsize: 123636
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 28682 0 0 0 59917 89 0 0 25 0 1 0 484455187 127938560 28324 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31235 28324 603 41 0 31194 0
vsize: 124940
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 28962 0 0 0 60916 90 0 0 25 0 1 0 484455187 129155072 28604 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31532 28604 603 41 0 31491 0
vsize: 126128
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 29294 0 0 0 61916 90 0 0 25 0 1 0 484455187 130498560 28936 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31860 28936 603 41 0 31819 0
vsize: 127440
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 29539 0 0 0 62915 91 0 0 25 0 1 0 484455187 131440640 29181 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32090 29181 603 41 0 32049 0
vsize: 128360
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 29800 0 0 0 63914 92 0 0 25 0 1 0 484455187 132517888 29442 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32353 29442 603 41 0 32312 0
vsize: 129412
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 30021 0 0 0 64914 93 0 0 25 0 1 0 484455187 133455872 29663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32582 29663 603 41 0 32541 0
vsize: 130328
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 30316 0 0 0 65913 94 0 0 25 0 1 0 484455187 134672384 29958 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32879 29958 603 41 0 32838 0
vsize: 131516
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 30703 0 0 0 66912 95 0 0 25 0 1 0 484455187 136151040 30345 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 30345 603 41 0 33199 0
vsize: 132960
[startup+680.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 31049 0 0 0 67911 96 0 0 25 0 1 0 484455187 137650176 30691 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33606 30691 603 41 0 33565 0
vsize: 134424
[startup+690.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 31308 0 0 0 68900 97 0 0 25 0 1 0 484455187 138723328 30950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33868 30950 603 41 0 33827 0
vsize: 135472
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 21386
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 31526 0 0 0 69899 98 0 0 25 0 1 0 484455187 139513856 31168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34061 31168 603 41 0 34020 0
vsize: 136244
[startup+710.1 s]
Raw data (loadavg): 1.07 0.99 0.95 2/58 21429
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 31808 0 0 0 70905 99 0 0 25 0 1 0 484455187 140709888 31450 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34353 31450 603 41 0 34312 0
vsize: 137412
[startup+720.1 s]
Raw data (loadavg): 1.22 1.02 0.96 2/54 21439
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 32052 0 0 0 71905 99 0 0 25 0 1 0 484455187 141656064 31694 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34584 31694 603 41 0 34543 0
vsize: 138336
[startup+730.101 s]
Raw data (loadavg): 1.19 1.02 0.96 2/54 21439
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 32282 0 0 0 72904 100 0 0 25 0 1 0 484455187 142594048 31924 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34813 31924 603 41 0 34772 0
vsize: 139252
[startup+740.101 s]
Raw data (loadavg): 1.16 1.02 0.96 2/54 21439
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 32523 0 0 0 73903 101 0 0 25 0 1 0 484455187 143675392 32165 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35077 32165 603 41 0 35036 0
vsize: 140308
[startup+750.101 s]
Raw data (loadavg): 1.13 1.02 0.96 2/54 21439
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 32814 0 0 0 74903 102 0 0 25 0 1 0 484455187 144883712 32456 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35372 32456 603 41 0 35331 0
vsize: 141488
[startup+760.101 s]
Raw data (loadavg): 1.11 1.02 0.96 2/54 21439
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 33064 0 0 0 75902 103 0 0 25 0 1 0 484455187 145829888 32706 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35603 32706 603 41 0 35562 0
vsize: 142412
[startup+770.101 s]
Raw data (loadavg): 1.10 1.02 0.96 2/54 21439
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 33321 0 0 0 76902 103 0 0 25 0 1 0 484455187 146898944 32963 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35864 32963 603 41 0 35823 0
vsize: 143456
[startup+780.102 s]
Raw data (loadavg): 1.08 1.01 0.96 2/54 21439
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 33724 0 0 0 77901 104 0 0 25 0 1 0 484455187 148516864 33366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36259 33366 603 41 0 36218 0
vsize: 145036
[startup+790.102 s]
Raw data (loadavg): 1.07 1.01 0.96 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 33960 0 0 0 78900 105 0 0 25 0 1 0 484455187 149463040 33602 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36490 33602 603 41 0 36449 0
vsize: 145960
[startup+800.102 s]
Raw data (loadavg): 1.06 1.01 0.96 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 34205 0 0 0 79899 106 0 0 25 0 1 0 484455187 150544384 33847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36754 33847 603 41 0 36713 0
vsize: 147016
[startup+810.101 s]
Raw data (loadavg): 1.05 1.01 0.96 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 34479 0 0 0 80898 108 0 0 25 0 1 0 484455187 151621632 34121 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37017 34121 603 41 0 36976 0
vsize: 148068
[startup+820.101 s]
Raw data (loadavg): 1.19 1.04 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 34849 0 0 0 81897 108 0 0 25 0 1 0 484455187 153100288 34491 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37378 34491 603 41 0 37337 0
vsize: 149512
[startup+830.102 s]
Raw data (loadavg): 1.16 1.04 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 35111 0 0 0 82896 109 0 0 25 0 1 0 484455187 154177536 34753 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37641 34753 603 41 0 37600 0
vsize: 150564
[startup+840.103 s]
Raw data (loadavg): 1.14 1.04 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 35388 0 0 0 83896 110 0 0 25 0 1 0 484455187 155385856 35030 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37936 35030 603 41 0 37895 0
vsize: 151744
[startup+850.103 s]
Raw data (loadavg): 1.12 1.04 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 35681 0 0 0 84895 111 0 0 25 0 1 0 484455187 156581888 35323 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38228 35323 603 41 0 38187 0
vsize: 152912
[startup+860.103 s]
Raw data (loadavg): 1.10 1.04 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 35978 0 0 0 85895 111 0 0 25 0 1 0 484455187 157786112 35620 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38522 35620 603 41 0 38481 0
vsize: 154088
[startup+870.103 s]
Raw data (loadavg): 1.08 1.03 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 36304 0 0 0 86894 113 0 0 25 0 1 0 484455187 159055872 35946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38832 35946 603 41 0 38791 0
vsize: 155328
[startup+880.103 s]
Raw data (loadavg): 1.07 1.03 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 36605 0 0 0 87893 113 0 0 25 0 1 0 484455187 160272384 36247 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39129 36247 603 41 0 39088 0
vsize: 156516
[startup+890.106 s]
Raw data (loadavg): 1.06 1.03 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 36930 0 0 0 88893 114 0 0 25 0 1 0 484455187 161619968 36572 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39458 36572 603 41 0 39417 0
vsize: 157832
[startup+900.105 s]
Raw data (loadavg): 1.05 1.03 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 37232 0 0 0 89892 115 0 0 25 0 1 0 484455187 162824192 36874 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39752 36874 603 41 0 39711 0
vsize: 159008
[startup+910.105 s]
Raw data (loadavg): 1.04 1.03 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 37446 0 0 0 90892 115 0 0 25 0 1 0 484455187 163770368 37088 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39983 37088 603 41 0 39942 0
vsize: 159932
[startup+920.105 s]
Raw data (loadavg): 1.03 1.03 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 37674 0 0 0 91891 116 0 0 25 0 1 0 484455187 164700160 37316 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40210 37316 603 41 0 40169 0
vsize: 160840
[startup+930.106 s]
Raw data (loadavg): 1.03 1.03 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 37926 0 0 0 92891 117 0 0 25 0 1 0 484455187 165773312 37568 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40472 37568 603 41 0 40431 0
vsize: 161888
[startup+940.105 s]
Raw data (loadavg): 1.10 1.04 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 38295 0 0 0 93889 118 0 0 25 0 1 0 484455187 167256064 37937 4294967295 134512640 134672761 3221224544 3221223648 134560150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40834 37937 603 41 0 40793 0
vsize: 163336
[startup+950.106 s]
Raw data (loadavg): 1.08 1.04 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 38640 0 0 0 94889 119 0 0 25 0 1 0 484455187 168603648 38282 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 38282 603 41 0 41122 0
vsize: 164652
[startup+960.106 s]
Raw data (loadavg): 1.07 1.04 0.97 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 39043 0 0 0 95888 120 0 0 25 0 1 0 484455187 170352640 38685 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41590 38685 603 41 0 41549 0
vsize: 166360
[startup+970.106 s]
Raw data (loadavg): 1.13 1.05 0.98 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 39477 0 0 0 96887 122 0 0 25 0 1 0 484455187 172097536 39119 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42016 39119 603 41 0 41975 0
vsize: 168064
[startup+980.106 s]
Raw data (loadavg): 1.11 1.05 0.98 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 39807 0 0 0 97886 122 0 0 25 0 1 0 484455187 173445120 39449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42345 39449 603 41 0 42304 0
vsize: 169380
[startup+990.106 s]
Raw data (loadavg): 1.09 1.05 0.98 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 40108 0 0 0 98885 123 0 0 25 0 1 0 484455187 174661632 39750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42642 39750 603 41 0 42601 0
vsize: 170568
[startup+1000.11 s]
Raw data (loadavg): 1.08 1.05 0.98 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 40388 0 0 0 99885 124 0 0 25 0 1 0 484455187 175738880 40030 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42905 40030 603 41 0 42864 0
vsize: 171620
[startup+1010.11 s]
Raw data (loadavg): 1.07 1.04 0.98 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 40698 0 0 0 100883 126 0 0 25 0 1 0 484455187 177070080 40340 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43230 40340 603 41 0 43189 0
vsize: 172920
[startup+1020.11 s]
Raw data (loadavg): 1.06 1.04 0.98 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 41021 0 0 0 101883 127 0 0 25 0 1 0 484455187 178409472 40663 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43557 40663 603 41 0 43516 0
vsize: 174228
[startup+1030.11 s]
Raw data (loadavg): 1.05 1.04 0.98 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 41305 0 0 0 102882 127 0 0 25 0 1 0 484455187 179482624 40947 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43819 40947 603 41 0 43778 0
vsize: 175276
[startup+1040.11 s]
Raw data (loadavg): 1.04 1.04 0.98 2/54 21441
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 41627 0 0 0 103882 128 0 0 25 0 1 0 484455187 180830208 41269 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44148 41269 603 41 0 44107 0
vsize: 176592
[startup+1050.11 s]
Raw data (loadavg): 1.03 1.04 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 41906 0 0 0 104881 128 0 0 25 0 1 0 484455187 182042624 41548 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44444 41548 603 41 0 44403 0
vsize: 177776
[startup+1060.11 s]
Raw data (loadavg): 1.03 1.03 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 42222 0 0 0 105880 130 0 0 25 0 1 0 484455187 183238656 41864 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44736 41864 603 41 0 44695 0
vsize: 178944
[startup+1070.11 s]
Raw data (loadavg): 1.02 1.03 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 42468 0 0 0 106880 130 0 0 25 0 1 0 484455187 184320000 42110 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45000 42110 603 41 0 44959 0
vsize: 180000
[startup+1080.11 s]
Raw data (loadavg): 1.02 1.03 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 42615 0 0 0 107880 130 0 0 25 0 1 0 484455187 184856576 42257 4294967295 134512640 134672761 3221224544 3221223680 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45131 42257 603 41 0 45090 0
vsize: 180524
[startup+1090.11 s]
Raw data (loadavg): 1.02 1.03 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 42821 0 0 0 108880 131 0 0 25 0 1 0 484455187 185794560 42463 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45360 42463 603 41 0 45319 0
vsize: 181440
[startup+1100.11 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 43070 0 0 0 109879 131 0 0 25 0 1 0 484455187 186728448 42712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45588 42712 603 41 0 45547 0
vsize: 182352
[startup+1110.11 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 43313 0 0 0 110879 132 0 0 25 0 1 0 484455187 187805696 42955 4294967295 134512640 134672761 3221224544 3221223728 134559625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45851 42955 603 41 0 45810 0
vsize: 183404
[startup+1120.11 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 43499 0 0 0 111878 133 0 0 25 0 1 0 484455187 188469248 43141 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46013 43141 603 41 0 45972 0
vsize: 184052
[startup+1130.11 s]
Raw data (loadavg): 1.01 1.02 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 43815 0 0 0 112877 134 0 0 25 0 1 0 484455187 189812736 43457 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46341 43457 603 41 0 46300 0
vsize: 185364
[startup+1140.11 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 44026 0 0 0 113877 135 0 0 25 0 1 0 484455187 190623744 43668 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46539 43668 603 41 0 46498 0
vsize: 186156
[startup+1150.11 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 44354 0 0 0 114875 136 0 0 25 0 1 0 484455187 191963136 43996 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46866 43996 603 41 0 46825 0
vsize: 187464
[startup+1160.11 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 44708 0 0 0 115874 137 0 0 25 0 1 0 484455187 193966080 44350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47355 44350 603 41 0 47314 0
vsize: 189420
[startup+1170.11 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 45039 0 0 0 116874 138 0 0 25 0 1 0 484455187 195325952 44681 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47687 44681 603 41 0 47646 0
vsize: 190748
[startup+1180.11 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 45296 0 0 0 117873 138 0 0 25 0 1 0 484455187 196403200 44938 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47950 44938 603 41 0 47909 0
vsize: 191800
[startup+1190.11 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 45466 0 0 0 118873 138 0 0 25 0 1 0 484455187 197079040 45108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48115 45108 603 41 0 48074 0
vsize: 192460
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 21443
Raw data (stat): 21386 (minisat+) R 21385 25285 25284 0 -1 0 45793 0 0 0 119872 139 0 0 25 0 1 0 484455187 198430720 45435 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48445 45435 603 41 0 48404 0
vsize: 193780
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.00 1.02 0.98 1/54 21443
Raw data (stat): 21386 (minisat+) Z 21385 25285 25284 0 -1 12 45795 0 0 0 119872 148 0 0 25 0 1 0 484455187 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.19
CPU time (s): 1200.21
CPU user time (s): 1198.73
CPU system time (s): 1.48477
CPU usage (%): 100.002
Max. virtual memory (Kb): 193780
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####