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 22350

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-22 03:00:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11653 boxname=wulflinc11 idbench=897 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  eb0734273e24196dd14c6f237b52fa81  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-air04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-air04.opb
IDLAUNCH: 11653
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        323848 kB
Buffers:         34968 kB
Cached:         653464 kB
SwapCached:          0 kB
Active:         242920 kB
Inactive:       448328 kB
HighTotal:      131008 kB
HighFree:        25956 kB
LowTotal:       903652 kB
LowFree:        297892 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            13660 kB
Committed_AS:    63636 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:20:29 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 11653 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   63
c ---[1640]---> BDD-cost:   23
c ---[1638]---> BDD-cost:   29
c ---[1636]---> BDD-cost:    0
c ---[1634]---> BDD-cost:   71
c ---[1632]---> BDD-cost:   55
c ---[1628]---> BDD-cost:   23
c ---[1626]---> BDD-cost:   47
c ---[1624]---> BDD-cost:  213
c ---[1622]---> BDD-cost:   75
c ---[1620]---> BDD-cost:   75
c ---[1618]---> BDD-cost:   55
c ---[1616]---> BDD-cost:   15
c ---[1614]---> BDD-cost:   87
c ---[1612]---> BDD-cost:   51
c ---[1610]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1606]---> BDD-cost:   23
c ---[1604]---> BDD-cost:   11
c ---[1602]---> BDD-cost:   39
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:  259
c ---[1594]---> BDD-cost:  189
c ---[1592]---> BDD-cost:  101
c ---[1588]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  101
c ---[1582]---> BDD-cost:   37
c ---[1580]---> BDD-cost:  181
c ---[1578]---> BDD-cost:  283
c ---[1576]---> BDD-cost:   99
c ---[1574]---> BDD-cost:    1
c ---[1572]---> BDD-cost:  109
c ---[1570]---> BDD-cost:   75
c ---[1568]---> BDD-cost:  237
c ---[1566]---> BDD-cost:  119
c ---[1564]---> BDD-cost:  109
c ---[1562]---> BDD-cost:   83
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:  157
c ---[1556]---> BDD-cost:  155
c ---[1554]---> BDD-cost:  109
c ---[1550]---> BDD-cost:   77
c ---[1548]---> BDD-cost:  133
c ---[1546]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  115
c ---[1542]---> BDD-cost:  185
c ---[1540]---> BDD-cost:  203
c ---[1538]---> BDD-cost:  167
c ---[1536]---> BDD-cost:  135
c ---[1534]---> BDD-cost:    9
c ---[1532]---> BDD-cost:   85
c ---[1530]---> BDD-cost:  143
c ---[1528]---> BDD-cost:  135
c ---[1526]---> BDD-cost:   63
c ---[1524]---> BDD-cost:   51
c ---[1522]---> BDD-cost:  159
c ---[1520]---> BDD-cost:  155
c ---[1518]---> BDD-cost:  211
c ---[1516]---> BDD-cost:   75
c ---[1514]---> BDD-cost:   37
c ---[1512]---> BDD-cost:   87
c ---[1510]---> BDD-cost:   79
c ---[1508]---> BDD-cost:  109
c ---[1506]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  247
c ---[1502]---> BDD-cost:  105
c ---[1500]---> BDD-cost:   59
c ---[1498]---> BDD-cost:   71
c ---[1496]---> BDD-cost:   61
c ---[1494]---> BDD-cost:   89
c ---[1492]---> BDD-cost:   91
c ---[1490]---> BDD-cost:  143
c ---[1488]---> BDD-cost:  111
c ---[1486]---> BDD-cost:   95
c ---[1484]---> BDD-cost:  169
c ---[1482]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  151
c ---[1478]---> BDD-cost:   67
c ---[1476]---> BDD-cost:   45
c ---[1474]---> BDD-cost:   45
c ---[1472]---> BDD-cost:   45
c ---[1470]---> BDD-cost:   65
c ---[1468]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   47
c ---[1460]---> BDD-cost:   29
c ---[1458]---> BDD-cost:   27
c ---[1456]---> BDD-cost:   11
c ---[1452]---> BDD-cost:   81
c ---[1450]---> BDD-cost:  233
c ---[1448]---> BDD-cost:  275
c ---[1446]---> BDD-cost:  289
c ---[1444]---> BDD-cost:  119
c ---[1442]---> BDD-cost:  145
c ---[1440]---> BDD-cost:  165
c ---[1438]---> BDD-cost:  239
c ---[1436]---> BDD-cost:  223
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   35
c ---[1430]---> BDD-cost:   93
c ---[1428]---> BDD-cost:   45
c ---[1426]---> BDD-cost:   73
c ---[1424]---> BDD-cost:   75
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   99
c ---[1416]---> BDD-cost:  187
c ---[1414]---> BDD-cost:   55
c ---[1412]---> BDD-cost:  107
c ---[1410]---> BDD-cost:   69
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:    3
c ---[1404]---> BDD-cost:  149
c ---[1402]---> BDD-cost:  137
c ---[1400]---> BDD-cost:  195
c ---[1398]---> BDD-cost:   93
c ---[1396]---> BDD-cost:  157
c ---[1394]---> BDD-cost:  233
c ---[1392]---> BDD-cost:  223
c ---[1390]---> BDD-cost:  225
c ---[1388]---> BDD-cost:  247
c ---[1386]---> BDD-cost:  179
c ---[1384]---> BDD-cost:  225
c ---[1382]---> BDD-cost:  243
c ---[1380]---> BDD-cost:  199
c ---[1378]---> BDD-cost:   55
c ---[1376]---> BDD-cost:   57
c ---[1374]---> BDD-cost:   99
c ---[1372]---> BDD-cost:    9
c ---[1370]---> BDD-cost:    3
c ---[1368]---> BDD-cost:   23
c ---[1366]---> BDD-cost:   51
c ---[1364]---> BDD-cost:   25
c ---[1362]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   27
c ---[1358]---> BDD-cost:   15
c ---[1356]---> BDD-cost:   37
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   67
c ---[1350]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  211
c ---[1342]---> BDD-cost:   65
c ---[1340]---> BDD-cost:  117
c ---[1338]---> BDD-cost:   65
c ---[1336]---> BDD-cost:   65
c ---[1334]---> BDD-cost:   49
c ---[1332]---> BDD-cost:  439
c ---[1330]---> BDD-cost:  423
c ---[1328]---> BDD-cost:  287
c ---[1326]---> BDD-cost:  217
c ---[1324]---> BDD-cost:  195
c ---[1322]---> BDD-cost:   63
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:  359
c ---[1316]---> BDD-cost:  353
c ---[1312]---> BDD-cost:  169
c ---[1310]---> BDD-cost:  139
c ---[1308]---> BDD-cost:  159
c ---[1306]---> BDD-cost:  223
c ---[1304]---> BDD-cost:  107
c ---[1302]---> BDD-cost:   75
c ---[1300]---> BDD-cost:  109
c ---[1298]---> BDD-cost:   93
c ---[1296]---> BDD-cost:   87
c ---[1294]---> BDD-cost:   87
c ---[1292]---> BDD-cost:    7
c ---[1288]---> BDD-cost:   73
c ---[1286]---> BDD-cost:   71
c ---[1284]---> BDD-cost:  107
c ---[1282]---> BDD-cost:   77
c ---[1280]---> BDD-cost:    3
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  131
c ---[1274]---> BDD-cost:  135
c ---[1272]---> BDD-cost:   65
c ---[1270]---> BDD-cost:  165
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:    1
c ---[1264]---> BDD-cost:   87
c ---[1262]---> BDD-cost:  155
c ---[1260]---> BDD-cost:  167
c ---[1258]---> BDD-cost:  203
c ---[1256]---> BDD-cost:  231
c ---[1254]---> BDD-cost:  147
c ---[1252]---> BDD-cost:  135
c ---[1250]---> BDD-cost:   49
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   95
c ---[1244]---> BDD-cost:  325
c ---[1242]---> BDD-cost:  333
c ---[1240]---> BDD-cost:  173
c ---[1238]---> BDD-cost:  269
c ---[1236]---> BDD-cost:   31
c ---[1234]---> BDD-cost:  413
c ---[1232]---> BDD-cost:  313
c ---[1230]---> BDD-cost:  125
c ---[1228]---> BDD-cost:  113
c ---[1226]---> BDD-cost:  247
c ---[1224]---> BDD-cost:   57
c ---[1222]---> BDD-cost:  237
c ---[1220]---> BDD-cost:  159
c ---[1218]---> BDD-cost:  117
c ---[1216]---> BDD-cost:   43
c ---[1214]---> BDD-cost:  143
c ---[1212]---> BDD-cost:   65
c ---[1210]---> BDD-cost:  123
c ---[1208]---> BDD-cost:   61
c ---[1206]---> BDD-cost:  103
c ---[1204]---> BDD-cost:   85
c ---[1202]---> BDD-cost:   77
c ---[1200]---> BDD-cost:   57
c ---[1198]---> BDD-cost:  127
c ---[1196]---> BDD-cost:  157
c ---[1194]---> BDD-cost:  267
c ---[1192]---> BDD-cost:  223
c ---[1190]---> BDD-cost:  229
c ---[1188]---> BDD-cost:  257
c ---[1186]---> BDD-cost:  241
c ---[1184]---> BDD-cost:  195
c ---[1182]---> BDD-cost:   49
c ---[1180]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  197
c ---[1176]---> BDD-cost:  171
c ---[1174]---> BDD-cost:  287
c ---[1172]---> BDD-cost:   75
c ---[1170]---> BDD-cost:  215
c ---[1168]---> BDD-cost:  119
c ---[1166]---> BDD-cost:  245
c ---[1164]---> BDD-cost:  257
c ---[1162]---> BDD-cost:  279
c ---[1160]---> BDD-cost:  227
c ---[1158]---> BDD-cost:  201
c ---[1156]---> BDD-cost:  143
c ---[1154]---> BDD-cost:  207
c ---[1152]---> BDD-cost:  131
c ---[1150]---> BDD-cost:  245
c ---[1148]---> BDD-cost:  115
c ---[1146]---> BDD-cost:   91
c ---[1144]---> BDD-cost:   43
c ---[1142]---> BDD-cost:   39
c ---[1140]---> BDD-cost:   91
c ---[1138]---> BDD-cost:  179
c ---[1136]---> BDD-cost:   73
c ---[1134]---> BDD-cost:   29
c ---[1132]---> BDD-cost:  163
c ---[1130]---> BDD-cost:   81
c ---[1128]---> BDD-cost:   63
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  113
c ---[1122]---> BDD-cost:  115
c ---[1120]---> BDD-cost:   19
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   99
c ---[1114]---> BDD-cost:   99
c ---[1112]---> BDD-cost:  103
c ---[1110]---> BDD-cost:   67
c ---[1108]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   85
c ---[1104]---> BDD-cost:   87
c ---[1102]---> BDD-cost:    7
c ---[1100]---> BDD-cost:   45
c ---[1098]---> BDD-cost:   43
c ---[1096]---> BDD-cost:   11
c ---[1094]---> BDD-cost:   59
c ---[1092]---> BDD-cost:  185
c ---[1090]---> BDD-cost:  249
c ---[1088]---> BDD-cost:  315
c ---[1086]---> BDD-cost:  253
c ---[1084]---> BDD-cost:  161
c ---[1082]---> BDD-cost:  257
c ---[1080]---> BDD-cost:  167
c ---[1078]---> BDD-cost:  167
c ---[1076]---> BDD-cost:  141
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   95
c ---[1068]---> BDD-cost:  141
c ---[1066]---> BDD-cost:  123
c ---[1064]---> BDD-cost:   83
c ---[1062]---> BDD-cost:   55
c ---[1060]---> BDD-cost:  183
c ---[1058]---> BDD-cost:  269
c ---[1056]---> BDD-cost:   63
c ---[1054]---> BDD-cost:   45
c ---[1052]---> BDD-cost:   39
c ---[1050]---> BDD-cost:   97
c ---[1048]---> BDD-cost:   51
c ---[1046]---> BDD-cost:   45
c ---[1044]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   85
c ---[1040]---> BDD-cost:   35
c ---[1038]---> BDD-cost:   53
c ---[1036]---> BDD-cost:   21
c ---[1034]---> BDD-cost:  115
c ---[1032]---> BDD-cost:   99
c ---[1030]---> BDD-cost:   63
c ---[1028]---> BDD-cost:   77
c ---[1026]---> BDD-cost:  139
c ---[1024]---> BDD-cost:  109
c ---[1022]---> BDD-cost:  407
c ---[1020]---> BDD-cost:  323
c ---[1018]---> BDD-cost:  109
c ---[1016]---> BDD-cost:   93
c ---[1014]---> BDD-cost:   51
c ---[1012]---> BDD-cost:   79
c ---[1010]---> BDD-cost:   75
c ---[1008]---> BDD-cost:  147
c ---[1006]---> BDD-cost:  169
c ---[1004]---> BDD-cost:  209
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   51
c ---[ 998]---> BDD-cost:   85
c ---[ 994]---> BDD-cost:  103
c ---[ 992]---> BDD-cost:  127
c ---[ 990]---> BDD-cost:   77
c ---[ 988]---> BDD-cost:   77
c ---[ 986]---> BDD-cost:  141
c ---[ 984]---> BDD-cost:   89
c ---[ 982]---> BDD-cost:   85
c ---[ 980]---> BDD-cost:  119
c ---[ 978]---> BDD-cost:   69
c ---[ 976]---> BDD-cost:   57
c ---[ 974]---> BDD-cost:   65
c ---[ 972]---> BDD-cost:   47
c ---[ 970]---> BDD-cost:   61
c ---[ 968]---> BDD-cost:   31
c ---[ 964]---> BDD-cost:  183
c ---[ 962]---> BDD-cost:  121
c ---[ 960]---> BDD-cost:   89
c ---[ 958]---> BDD-cost:  225
c ---[ 956]---> BDD-cost:  267
c ---[ 952]---> BDD-cost:  159
c ---[ 950]---> BDD-cost:  209
c ---[ 948]---> BDD-cost:   71
c ---[ 946]---> BDD-cost:  237
c ---[ 944]---> BDD-cost:  129
c ---[ 942]---> BDD-cost:  365
c ---[ 940]---> BDD-cost:  369
c ---[ 938]---> BDD-cost:  129
c ---[ 936]---> BDD-cost:  101
c ---[ 934]---> BDD-cost:  289
c ---[ 932]---> BDD-cost:  279
c ---[ 930]---> BDD-cost:  345
c ---[ 928]---> BDD-cost:   81
c ---[ 926]---> BDD-cost:   69
c ---[ 924]---> BDD-cost:   83
c ---[ 922]---> BDD-cost:   53
c ---[ 920]---> BDD-cost:   67
c ---[ 918]---> BDD-cost:   55
c ---[ 916]---> BDD-cost:  145
c ---[ 914]---> BDD-cost:  149
c ---[ 912]---> BDD-cost:  105
c ---[ 910]---> BDD-cost:   19
c ---[ 908]---> BDD-cost:  105
c ---[ 906]---> BDD-cost:  101
c ---[ 904]---> BDD-cost:  147
c ---[ 902]---> BDD-cost:  231
c ---[ 900]---> BDD-cost:  191
c ---[ 898]---> BDD-cost:  157
c ---[ 896]---> BDD-cost:  249
c ---[ 894]---> BDD-cost:  385
c ---[ 892]---> BDD-cost:   67
c ---[ 890]---> BDD-cost:   71
c ---[ 888]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:  147
c ---[ 884]---> BDD-cost:  139
c ---[ 882]---> BDD-cost:  273
c ---[ 880]---> BDD-cost:  213
c ---[ 878]---> BDD-cost:  169
c ---[ 876]---> BDD-cost:  239
c ---[ 874]---> BDD-cost:  305
c ---[ 872]---> BDD-cost:  109
c ---[ 870]---> BDD-cost:  105
c ---[ 868]---> BDD-cost:  147
c ---[ 866]---> BDD-cost:  115
c ---[ 864]---> BDD-cost:  115
c ---[ 862]---> BDD-cost:   67
c ---[ 860]---> BDD-cost:  329
c ---[ 858]---> BDD-cost:  295
c ---[ 856]---> BDD-cost:   51
c ---[ 854]---> BDD-cost:   61
c ---[ 852]---> BDD-cost:  317
c ---[ 850]---> BDD-cost:   97
c ---[ 848]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:   43
c ---[ 844]---> BDD-cost:   85
c ---[ 842]---> BDD-cost:   35
c ---[ 840]---> BDD-cost:   69
c ---[ 836]---> BDD-cost:   45
c ---[ 834]---> BDD-cost:   73
c ---[ 832]---> BDD-cost:   55
c ---[ 828]---> BDD-cost:   33
c ---[ 826]---> BDD-cost:   29
c ---[ 824]---> BDD-cost:  245
c ---[ 822]---> BDD-cost:  225
c ---[ 820]---> BDD-cost:  111
c ---[ 818]---> BDD-cost:  117
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  129
c ---[ 812]---> BDD-cost:  259
c ---[ 810]---> BDD-cost:  221
c ---[ 808]---> BDD-cost:  275
c ---[ 806]---> BDD-cost:  209
c ---[ 804]---> BDD-cost:  267
c ---[ 802]---> BDD-cost:  171
c ---[ 800]---> BDD-cost:   57
c ---[ 796]---> BDD-cost:  133
c ---[ 794]---> BDD-cost:  185
c ---[ 792]---> BDD-cost:  169
c ---[ 790]---> BDD-cost:  287
c ---[ 788]---> BDD-cost:   81
c ---[ 786]---> BDD-cost:  335
c ---[ 784]---> BDD-cost:  365
c ---[ 782]---> BDD-cost:  255
c ---[ 780]---> BDD-cost:  111
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  101
c ---[ 774]---> BDD-cost:  197
c ---[ 772]---> BDD-cost:  383
c ---[ 770]---> BDD-cost:  329
c ---[ 768]---> BDD-cost:  241
c ---[ 766]---> BDD-cost:  129
c ---[ 764]---> BDD-cost:   85
c ---[ 762]---> BDD-cost:   71
c ---[ 760]---> BDD-cost:   37
c ---[ 758]---> BDD-cost:   77
c ---[ 756]---> BDD-cost:   49
c ---[ 754]---> BDD-cost:  133
c ---[ 752]---> BDD-cost:  133
c ---[ 750]---> BDD-cost:  377
c ---[ 748]---> BDD-cost:  117
c ---[ 744]---> BDD-cost:  119
c ---[ 742]---> BDD-cost:  119
c ---[ 740]---> BDD-cost:  151
c ---[ 738]---> BDD-cost:  221
c ---[ 736]---> BDD-cost:  181
c ---[ 732]---> BDD-cost:   87
c ---[ 730]---> BDD-cost:  127
c ---[ 728]---> BDD-cost:  299
c ---[ 726]---> BDD-cost:  331
c ---[ 722]---> BDD-cost:   21
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  217
c ---[ 716]---> BDD-cost:  349
c ---[ 714]---> BDD-cost:  291
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  161
c ---[ 708]---> BDD-cost:   61
c ---[ 706]---> BDD-cost:   55
c ---[ 704]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:  189
c ---[ 698]---> BDD-cost:  157
c ---[ 696]---> BDD-cost:  149
c ---[ 694]---> BDD-cost:  139
c ---[ 692]---> BDD-cost:  165
c ---[ 690]---> BDD-cost:  181
c ---[ 688]---> BDD-cost:  253
c ---[ 686]---> BDD-cost:   43
c ---[ 684]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  141
c ---[ 680]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:   95
c ---[ 676]---> BDD-cost:   75
c ---[ 674]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  149
c ---[ 670]---> BDD-cost:  137
c ---[ 668]---> BDD-cost:   59
c ---[ 666]---> BDD-cost:    5
c ---[ 664]---> BDD-cost:   35
c ---[ 662]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   47
c ---[ 654]---> BDD-cost:   55
c ---[ 652]---> BDD-cost:  197
c ---[ 650]---> BDD-cost:  191
c ---[ 648]---> BDD-cost:  125
c ---[ 646]---> BDD-cost:  173
c ---[ 642]---> BDD-cost:   93
c ---[ 640]---> BDD-cost:   29
c ---[ 638]---> BDD-cost:  321
c ---[ 636]---> BDD-cost:  195
c ---[ 634]---> BDD-cost:  163
c ---[ 628]---> BDD-cost:  151
c ---[ 626]---> BDD-cost:  253
c ---[ 624]---> BDD-cost:  381
c ---[ 622]---> BDD-cost:  345
c ---[ 620]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:   83
c ---[ 614]---> BDD-cost:   69
c ---[ 612]---> BDD-cost:   51
c ---[ 610]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   59
c ---[ 606]---> BDD-cost:   83
c ---[ 604]---> BDD-cost:  107
c ---[ 602]---> BDD-cost:  363
c ---[ 600]---> BDD-cost:  103
c ---[ 598]---> BDD-cost:  277
c ---[ 596]---> BDD-cost:  341
c ---[ 594]---> BDD-cost:  213
c ---[ 592]---> BDD-cost:  315
c ---[ 590]---> BDD-cost:  275
c ---[ 588]---> BDD-cost:  151
c ---[ 586]---> BDD-cost:  111
c ---[ 584]---> BDD-cost:  103
c ---[ 582]---> BDD-cost:   75
c ---[ 580]---> BDD-cost:   27
c ---[ 578]---> BDD-cost:   21
c ---[ 576]---> BDD-cost:   11
c ---[ 574]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:  149
c ---[ 564]---> BDD-cost:   97
c ---[ 562]---> BDD-cost:  149
c ---[ 560]---> BDD-cost:  395
c ---[ 558]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:  389
c ---[ 554]---> BDD-cost:  251
c ---[ 552]---> BDD-cost:  375
c ---[ 550]---> BDD-cost:  343
c ---[ 548]---> BDD-cost:  267
c ---[ 546]---> BDD-cost:  135
c ---[ 544]---> BDD-cost:  263
c ---[ 542]---> BDD-cost:  259
c ---[ 540]---> BDD-cost:  245
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:   41
c ---[ 534]---> BDD-cost:  127
c ---[ 532]---> BDD-cost:  117
c ---[ 530]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:  149
c ---[ 526]---> BDD-cost:  103
c ---[ 524]---> BDD-cost:  215
c ---[ 522]---> BDD-cost:   89
c ---[ 520]---> BDD-cost:  177
c ---[ 518]---> BDD-cost:  343
c ---[ 516]---> BDD-cost:  237
c ---[ 514]---> BDD-cost:  177
c ---[ 512]---> BDD-cost:   85
c ---[ 510]---> BDD-cost:  267
c ---[ 508]---> BDD-cost:  225
c ---[ 506]---> BDD-cost:  109
c ---[ 504]---> BDD-cost:  105
c ---[ 502]---> BDD-cost:  113
c ---[ 500]---> BDD-cost:   55
c ---[ 498]---> BDD-cost:  117
c ---[ 496]---> BDD-cost:   83
c ---[ 494]---> BDD-cost:   79
c ---[ 492]---> BDD-cost:   81
c ---[ 490]---> BDD-cost:  263
c ---[ 488]---> BDD-cost:  179
c ---[ 486]---> BDD-cost:  281
c ---[ 484]---> BDD-cost:  389
c ---[ 482]---> BDD-cost:  333
c ---[ 480]---> BDD-cost:  357
c ---[ 478]---> BDD-cost:  345
c ---[ 476]---> BDD-cost:  263
c ---[ 474]---> BDD-cost:   89
c ---[ 472]---> BDD-cost:  285
c ---[ 468]---> BDD-cost:  419
c ---[ 466]---> BDD-cost:  357
c ---[ 464]---> BDD-cost:  473
c ---[ 462]---> BDD-cost:  455
c ---[ 460]---> BDD-cost:  405
c ---[ 458]---> BDD-cost:  241
c ---[ 456]---> BDD-cost:  211
c ---[ 454]---> BDD-cost:  313
c ---[ 452]---> BDD-cost:  371
c ---[ 450]---> BDD-cost:  389
c ---[ 448]---> BDD-cost:  223
c ---[ 446]---> BDD-cost:  221
c ---[ 444]---> BDD-cost:  147
c ---[ 442]---> BDD-cost:  131
c ---[ 440]---> BDD-cost:  185
c ---[ 438]---> BDD-cost:  141
c ---[ 436]---> BDD-cost:  249
c ---[ 434]---> BDD-cost:  261
c ---[ 432]---> BDD-cost:  311
c ---[ 430]---> BDD-cost:  261
c ---[ 428]---> BDD-cost:  387
c ---[ 426]---> BDD-cost:  247
c ---[ 424]---> BDD-cost:  295
c ---[ 422]---> BDD-cost:   31
c ---[ 420]---> BDD-cost:  355
c ---[ 418]---> BDD-cost:  135
c ---[ 416]---> BDD-cost:  443
c ---[ 414]---> BDD-cost:  653
c ---[ 412]---> BDD-cost:  703
c ---[ 410]---> BDD-cost:  517
c ---[ 408]---> BDD-cost:  441
c ---[ 406]---> BDD-cost:  411
c ---[ 404]---> BDD-cost:  289
c ---[ 402]---> BDD-cost:  277
c ---[ 400]---> BDD-cost:  239
c ---[ 398]---> BDD-cost:  201
c ---[ 396]---> BDD-cost:  309
c ---[ 394]---> BDD-cost:  287
c ---[ 392]---> BDD-cost:  177
c ---[ 390]---> BDD-cost:  143
c ---[ 388]---> BDD-cost:  131
c ---[ 386]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:  189
c ---[ 382]---> BDD-cost:  219
c ---[ 378]---> BDD-cost:  267
c ---[ 376]---> BDD-cost:  135
c ---[ 374]---> BDD-cost:   69
c ---[ 372]---> BDD-cost:   75
c ---[ 370]---> BDD-cost:   51
c ---[ 368]---> BDD-cost:  117
c ---[ 366]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:  189
c ---[ 358]---> BDD-cost:   73
c ---[ 356]---> BDD-cost:   55
c ---[ 354]---> BDD-cost:   57
c ---[ 352]---> BDD-cost:   91
c ---[ 350]---> BDD-cost:  325
c ---[ 348]---> BDD-cost:  223
c ---[ 346]---> BDD-cost:   57
c ---[ 344]---> BDD-cost:   43
c ---[ 342]---> BDD-cost:  255
c ---[ 340]---> BDD-cost:  285
c ---[ 338]---> BDD-cost:  187
c ---[ 336]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   91
c ---[ 332]---> BDD-cost:  211
c ---[ 330]---> BDD-cost:  159
c ---[ 328]---> BDD-cost:   97
c ---[ 326]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:  101
c ---[ 322]---> BDD-cost:  141
c ---[ 318]---> BDD-cost:  109
c ---[ 316]---> BDD-cost:  321
c ---[ 314]---> BDD-cost:  305
c ---[ 312]---> BDD-cost:  603
c ---[ 310]---> BDD-cost:  441
c ---[ 308]---> BDD-cost:  391
c ---[ 306]---> BDD-cost:  387
c ---[ 304]---> BDD-cost:  289
c ---[ 302]---> BDD-cost:  219
c ---[ 300]---> BDD-cost:  309
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  197
c ---[ 294]---> BDD-cost:  279
c ---[ 292]---> BDD-cost:  167
c ---[ 290]---> BDD-cost:  151
c ---[ 288]---> BDD-cost:   49
c ---[ 286]---> BDD-cost:   31
c ---[ 284]---> BDD-cost:  107
c ---[ 282]---> BDD-cost:   55
c ---[ 278]---> BDD-cost:  177
c ---[ 276]---> BDD-cost:  223
c ---[ 274]---> BDD-cost:  119
c ---[ 272]---> BDD-cost:  137
c ---[ 270]---> BDD-cost:  105
c ---[ 268]---> BDD-cost:  183
c ---[ 266]---> BDD-cost:  179
c ---[ 264]---> BDD-cost:  285
c ---[ 262]---> BDD-cost:  191
c ---[ 260]---> BDD-cost:  177
c ---[ 258]---> BDD-cost:  145
c ---[ 254]---> BDD-cost:  153
c ---[ 252]---> BDD-cost:  121
c ---[ 250]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:  111
c ---[ 244]---> BDD-cost:  281
c ---[ 242]---> BDD-cost:  265
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  151
c ---[ 236]---> BDD-cost:  167
c ---[ 234]---> BDD-cost:  137
c ---[ 230]---> BDD-cost:  375
c ---[ 228]---> BDD-cost:  287
c ---[ 226]---> BDD-cost:  249
c ---[ 224]---> BDD-cost:  131
c ---[ 222]---> BDD-cost:  187
c ---[ 220]---> BDD-cost:  135
c ---[ 218]---> BDD-cost:  129
c ---[ 216]---> BDD-cost:  317
c ---[ 214]---> BDD-cost:  365
c ---[ 212]---> BDD-cost:  235
c ---[ 210]---> BDD-cost:  249
c ---[ 208]---> BDD-cost:  283
c ---[ 206]---> BDD-cost:  233
c ---[ 204]---> BDD-cost:  259
c ---[ 202]---> BDD-cost:  287
c ---[ 200]---> BDD-cost:  175
c ---[ 198]---> BDD-cost:  233
c ---[ 196]---> BDD-cost:  167
c ---[ 194]---> BDD-cost:  159
c ---[ 192]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:  135
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:  167
c ---[ 182]---> BDD-cost:  203
c ---[ 180]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  263
c ---[ 176]---> BDD-cost:   31
c ---[ 174]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   31
c ---[ 170]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:  225
c ---[ 166]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  385
c ---[ 162]---> BDD-cost:  361
c ---[ 160]---> BDD-cost:   73
c ---[ 158]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:  131
c ---[ 152]---> BDD-cost:  145
c ---[ 150]---> BDD-cost:  121
c ---[ 148]---> BDD-cost:  117
c ---[ 146]---> BDD-cost:  111
c ---[ 144]---> BDD-cost:  123
c ---[ 142]---> BDD-cost:  125
c ---[ 140]---> BDD-cost:  243
c ---[ 138]---> BDD-cost:  143
c ---[ 136]---> BDD-cost:  149
c ---[ 134]---> BDD-cost:  103
c ---[ 132]---> BDD-cost:  155
c ---[ 130]---> BDD-cost:  247
c ---[ 128]---> BDD-cost:  143
c ---[ 126]---> BDD-cost:   91
c ---[ 124]---> BDD-cost:   81
c ---[ 122]---> BDD-cost:   79
c ---[ 120]---> BDD-cost:  117
c ---[ 118]---> BDD-cost:   89
c ---[ 116]---> BDD-cost:   61
c ---[ 114]---> BDD-cost:  127
c ---[ 112]---> BDD-cost:  135
c ---[ 110]---> BDD-cost:  161
c ---[ 108]---> BDD-cost:  141
c ---[ 106]---> BDD-cost:  437
c ---[ 104]---> BDD-cost:  309
c ---[ 102]---> BDD-cost:  173
c ---[ 100]---> BDD-cost:  441
c ---[  98]---> BDD-cost:  489
c ---[  96]---> BDD-cost:  299
c ---[  94]---> BDD-cost:  455
c ---[  92]---> BDD-cost:  333
c ---[  90]---> BDD-cost:  421
c ---[  88]---> BDD-cost:  375
c ---[  86]---> BDD-cost:  433
c ---[  84]---> BDD-cost:  405
c ---[  82]---> BDD-cost:  333
c ---[  80]---> BDD-cost:  673
c ---[  78]---> BDD-cost:  685
c ---[  76]---> BDD-cost:  385
c ---[  74]---> BDD-cost:  267
c ---[  72]---> BDD-cost:  345
c ---[  70]---> BDD-cost:  365
c ---[  68]---> BDD-cost:  391
c ---[  66]---> BDD-cost:  313
c ---[  64]---> BDD-cost:  275
c ---[  62]---> BDD-cost:  257
c ---[  60]---> BDD-cost:  203
c ---[  58]---> BDD-cost:  311
c ---[  56]---> BDD-cost:  227
c ---[  54]---> BDD-cost:  295
c ---[  52]---> BDD-cost:  233
c ---[  50]---> BDD-cost:  247
c ---[  46]---> BDD-cost:  237
c ---[  44]---> BDD-cost:  149
c ---[  40]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   85
c ---[  36]---> BDD-cost:  109
c ---[  34]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:   71
c ---[  28]---> BDD-cost:   67
c ---[  26]---> BDD-cost:  151
c ---[  24]---> BDD-cost:  147
c ---[  22]---> BDD-cost:  177
c ---[  20]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  147
c ---[  14]---> BDD-cost:  215
c ---[  12]---> BDD-cost:  181
c ---[  10]---> BDD-cost:  235
c ---[   8]---> BDD-cost:  163
c ---[   6]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   59
c ---[   2]---> BDD-cost:  139
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  310358   807732 |  103452       0        0     nan |  0.000 % |
c |       100 |  310358   807732 |  113797     100     2792    27.9 |  0.588 % |
c |       250 |  310331   807657 |  125176     249    12761    51.2 |  0.592 % |
c |       475 |  310198   807286 |  137694     459    35376    77.1 |  0.620 % |
c |       812 |  310052   806901 |  151464     787    48598    61.8 |  0.642 % |
c |      1319 |  309884   806468 |  166610    1289    73251    56.8 |  0.667 % |
c |      2078 |  309785   806192 |  183271    2043   141139    69.1 |  0.692 % |
c |      3217 |  309724   806017 |  201598    3171   279873    88.3 |  0.705 % |
c |      4927 |  309614   805741 |  221758    4872   562380   115.4 |  0.716 % |
c |      7490 |  309614   805741 |  243934    7435  1259451   169.4 |  0.716 % |
c |     11334 |  309475   805377 |  268327   11239  1793736   159.6 |  0.732 % |
c |     17101 |  309226   804713 |  295160   16957  2478519   146.2 |  0.776 % |
c |     25752 |  307768   801003 |  324676   25505  3930547   154.1 |  0.987 % |
c |     38728 |  307515   800363 |  357144   38421  6348349   165.2 |  1.003 % |
c |     58191 |  307356   799958 |  392858   57785 10148314   175.6 |  1.017 % |
c |     87385 |  306886   798753 |  432144   86840 17512694   201.7 |  1.062 % |
c |    131176 |  306715   798313 |  475359  130557 31984227   245.0 |  1.079 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.92 2/54 16561
Raw data (stat): 16561 (runsolver) R 16560 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 492089861 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0011 s]
Raw data (loadavg): 0.87 0.97 0.92 2/54 16561
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 11064 0 0 0 970 28 0 0 25 0 1 0 492089861 54525952 10706 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13312 10706 603 41 0 13271 0
vsize: 53248
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 16561
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 11313 0 0 0 1969 29 0 0 25 0 1 0 492089861 55472128 10955 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13543 10955 603 41 0 13502 0
vsize: 54172
[startup+30.0031 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 16561
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 11716 0 0 0 2968 30 0 0 25 0 1 0 492089861 57085952 11358 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13937 11358 603 41 0 13896 0
vsize: 55748
[startup+40.0034 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 16561
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 12357 0 0 0 3965 32 0 0 25 0 1 0 492089861 59777024 11999 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14594 11999 603 41 0 14553 0
vsize: 58376
[startup+50.0048 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 12745 0 0 0 4963 34 0 0 25 0 1 0 492089861 61390848 12387 4294967295 134512640 134672761 3221224624 3221223840 134557688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 12387 603 41 0 14947 0
vsize: 59952
[startup+60.0049 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 13035 0 0 0 5963 35 0 0 25 0 1 0 492089861 62607360 12677 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15285 12677 603 41 0 15244 0
vsize: 61140
[startup+70.0046 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 13316 0 0 0 6962 35 0 0 25 0 1 0 492089861 63684608 12958 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15548 12958 603 41 0 15507 0
vsize: 62192
[startup+80.0054 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 13563 0 0 0 7962 36 0 0 25 0 1 0 492089861 64761856 13205 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15811 13205 603 41 0 15770 0
vsize: 63244
[startup+90.0052 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 13901 0 0 0 8961 37 0 0 25 0 1 0 492089861 66187264 13543 4294967295 134512640 134672761 3221224624 3221223728 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16159 13543 603 41 0 16118 0
vsize: 64636
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 14226 0 0 0 9959 39 0 0 25 0 1 0 492089861 67399680 13868 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16455 13868 603 41 0 16414 0
vsize: 65820
[startup+110.006 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 14636 0 0 0 10959 40 0 0 25 0 1 0 492089861 69152768 14278 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16883 14278 603 41 0 16842 0
vsize: 67532
[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 14993 0 0 0 11958 41 0 0 25 0 1 0 492089861 70631424 14635 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17244 14635 603 41 0 17203 0
vsize: 68976
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 15259 0 0 0 12957 42 0 0 25 0 1 0 492089861 71708672 14901 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17507 14901 603 41 0 17466 0
vsize: 70028
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 15564 0 0 0 13955 43 0 0 25 0 1 0 492089861 72921088 15206 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17803 15206 603 41 0 17762 0
vsize: 71212
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 15941 0 0 0 14954 44 0 0 25 0 1 0 492089861 74407936 15583 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18166 15583 603 41 0 18125 0
vsize: 72664
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 16282 0 0 0 15953 45 0 0 25 0 1 0 492089861 75886592 15924 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18527 15924 603 41 0 18486 0
vsize: 74108
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 16569 0 0 0 16953 46 0 0 25 0 1 0 492089861 76967936 16211 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18791 16211 603 41 0 18750 0
vsize: 75164
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 16882 0 0 0 17952 47 0 0 25 0 1 0 492089861 78446592 16524 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19152 16524 603 41 0 19111 0
vsize: 76608
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 17243 0 0 0 18951 48 0 0 25 0 1 0 492089861 79929344 16885 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19514 16886 603 41 0 19473 0
vsize: 78056
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 17585 0 0 0 19950 49 0 0 25 0 1 0 492089861 81268736 17227 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19841 17227 603 41 0 19800 0
vsize: 79364
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 17952 0 0 0 20949 50 0 0 25 0 1 0 492089861 82743296 17594 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20201 17594 603 41 0 20160 0
vsize: 80804
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 18176 0 0 0 21949 51 0 0 25 0 1 0 492089861 83689472 17818 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20432 17818 603 41 0 20391 0
vsize: 81728
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 18396 0 0 0 22949 51 0 0 25 0 1 0 492089861 84492288 18038 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20628 18038 603 41 0 20587 0
vsize: 82512
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 18825 0 0 0 23948 52 0 0 25 0 1 0 492089861 86253568 18467 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21058 18467 603 41 0 21017 0
vsize: 84232
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 19169 0 0 0 24947 53 0 0 25 0 1 0 492089861 87744512 18811 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21422 18811 603 41 0 21381 0
vsize: 85688
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 19611 0 0 0 25946 55 0 0 25 0 1 0 492089861 89493504 19253 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21849 19253 603 41 0 21808 0
vsize: 87396
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 19912 0 0 0 26945 56 0 0 25 0 1 0 492089861 90710016 19554 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22146 19554 603 41 0 22105 0
vsize: 88584
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 20086 0 0 0 27945 56 0 0 25 0 1 0 492089861 91381760 19728 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22310 19728 603 41 0 22269 0
vsize: 89240
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 20375 0 0 0 28944 57 0 0 25 0 1 0 492089861 92606464 20017 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22609 20017 603 41 0 22568 0
vsize: 90436
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 16563
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 20671 0 0 0 29944 58 0 0 25 0 1 0 492089861 93818880 20313 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22905 20313 603 41 0 22864 0
vsize: 91620
[startup+310.01 s]
Raw data (loadavg): 1.15 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 21045 0 0 0 30943 59 0 0 25 0 1 0 492089861 95305728 20687 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23268 20687 603 41 0 23227 0
vsize: 93072
[startup+320.009 s]
Raw data (loadavg): 1.13 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 21330 0 0 0 31942 60 0 0 25 0 1 0 492089861 96522240 20972 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23565 20972 603 41 0 23524 0
vsize: 94260
[startup+330.01 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 21574 0 0 0 32941 60 0 0 25 0 1 0 492089861 97456128 21216 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23793 21216 603 41 0 23752 0
vsize: 95172
[startup+340.01 s]
Raw data (loadavg): 1.09 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 21901 0 0 0 33941 61 0 0 25 0 1 0 492089861 98783232 21543 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24117 21543 603 41 0 24076 0
vsize: 96468
[startup+350.01 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 22166 0 0 0 34939 62 0 0 25 0 1 0 492089861 99860480 21808 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24380 21808 603 41 0 24339 0
vsize: 97520
[startup+360.01 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 22492 0 0 0 35939 63 0 0 25 0 1 0 492089861 101212160 22134 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24710 22134 603 41 0 24669 0
vsize: 98840
[startup+370.01 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 23146 0 0 0 36937 65 0 0 25 0 1 0 492089861 103936000 22788 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25375 22788 603 41 0 25334 0
vsize: 101500
[startup+380.011 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 23469 0 0 0 37936 66 0 0 25 0 1 0 492089861 105275392 23111 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25702 23111 603 41 0 25661 0
vsize: 102808
[startup+390.011 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 23685 0 0 0 38935 67 0 0 25 0 1 0 492089861 106086400 23327 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25900 23327 603 41 0 25859 0
vsize: 103600
[startup+400.011 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 24025 0 0 0 39935 68 0 0 25 0 1 0 492089861 107433984 23667 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26229 23667 603 41 0 26188 0
vsize: 104916
[startup+410.011 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 24351 0 0 0 40934 68 0 0 25 0 1 0 492089861 109023232 23993 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26617 23993 603 41 0 26576 0
vsize: 106468
[startup+420.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 24799 0 0 0 41933 70 0 0 25 0 1 0 492089861 110911488 24441 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27078 24441 603 41 0 27037 0
vsize: 108312
[startup+430.011 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 25147 0 0 0 42932 71 0 0 25 0 1 0 492089861 112381952 24789 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27437 24789 603 41 0 27396 0
vsize: 109748
[startup+440.011 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 25471 0 0 0 43932 71 0 0 25 0 1 0 492089861 113598464 25113 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27734 25113 603 41 0 27693 0
vsize: 110936
[startup+450.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 25778 0 0 0 44931 72 0 0 25 0 1 0 492089861 114970624 25420 4294967295 134512640 134672761 3221224624 3221223728 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28069 25420 603 41 0 28028 0
vsize: 112276
[startup+460.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 25989 0 0 0 45931 73 0 0 25 0 1 0 492089861 115773440 25631 4294967295 134512640 134672761 3221224624 3221223792 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28265 25631 603 41 0 28224 0
vsize: 113060
[startup+470.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 26238 0 0 0 46930 73 0 0 25 0 1 0 492089861 116715520 25880 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28495 25880 603 41 0 28454 0
vsize: 113980
[startup+480.014 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 26559 0 0 0 47930 74 0 0 25 0 1 0 492089861 118050816 26201 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28821 26201 603 41 0 28780 0
vsize: 115284
[startup+490.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 26870 0 0 0 48930 75 0 0 25 0 1 0 492089861 119394304 26512 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29149 26512 603 41 0 29108 0
vsize: 116596
[startup+500.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 27129 0 0 0 49929 75 0 0 25 0 1 0 492089861 120471552 26771 4294967295 134512640 134672761 3221224624 3221223792 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29412 26771 603 41 0 29371 0
vsize: 117648
[startup+510.015 s]
Raw data (loadavg): 1.00 1.00 0.93 3/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 27472 0 0 0 50928 76 0 0 25 0 1 0 492089861 121802752 27114 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29737 27114 603 41 0 29696 0
vsize: 118948
[startup+520.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 27820 0 0 0 51928 77 0 0 25 0 1 0 492089861 123297792 27462 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30102 27462 603 41 0 30061 0
vsize: 120408
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 28096 0 0 0 52927 78 0 0 25 0 1 0 492089861 124358656 27738 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30361 27738 603 41 0 30320 0
vsize: 121444
[startup+540.016 s]
Raw data (loadavg): 1.00 1.00 0.93 3/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 28423 0 0 0 53927 79 0 0 25 0 1 0 492089861 125714432 28065 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30692 28065 603 41 0 30651 0
vsize: 122768
[startup+550.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 28660 0 0 0 54926 79 0 0 25 0 1 0 492089861 126636032 28302 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30917 28302 603 41 0 30876 0
vsize: 123668
[startup+560.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 28948 0 0 0 55925 80 0 0 25 0 1 0 492089861 127848448 28590 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31213 28590 603 41 0 31172 0
vsize: 124852
[startup+570.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 29211 0 0 0 56925 81 0 0 25 0 1 0 492089861 128933888 28853 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31478 28853 603 41 0 31437 0
vsize: 125912
[startup+580.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 29491 0 0 0 57924 82 0 0 25 0 1 0 492089861 130007040 29133 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31740 29133 603 41 0 31699 0
vsize: 126960
[startup+590.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 29856 0 0 0 58923 82 0 0 25 0 1 0 492089861 131612672 29498 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32132 29498 603 41 0 32091 0
vsize: 128528
[startup+600.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 30116 0 0 0 59923 83 0 0 25 0 1 0 492089861 132558848 29758 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32363 29758 603 41 0 32322 0
vsize: 129452
[startup+610.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 30540 0 0 0 60922 84 0 0 25 0 1 0 492089861 134303744 30182 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32789 30182 603 41 0 32748 0
vsize: 131156
[startup+620.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 30875 0 0 0 61921 85 0 0 25 0 1 0 492089861 135647232 30517 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33117 30517 603 41 0 33076 0
vsize: 132468
[startup+630.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 31205 0 0 0 62920 86 0 0 25 0 1 0 492089861 137003008 30847 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33448 30847 603 41 0 33407 0
vsize: 133792
[startup+640.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 31596 0 0 0 63920 87 0 0 25 0 1 0 492089861 138604544 31238 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33839 31238 603 41 0 33798 0
vsize: 135356
[startup+650.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 31906 0 0 0 64919 88 0 0 25 0 1 0 492089861 139943936 31548 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34166 31548 603 41 0 34125 0
vsize: 136664
[startup+660.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 32124 0 0 0 65918 89 0 0 25 0 1 0 492089861 140746752 31766 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34362 31766 603 41 0 34321 0
vsize: 137448
[startup+670.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 32471 0 0 0 66918 89 0 0 25 0 1 0 492089861 142229504 32113 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34724 32113 603 41 0 34683 0
vsize: 138896
[startup+680.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 32768 0 0 0 67918 90 0 0 25 0 1 0 492089861 143429632 32410 4294967295 134512640 134672761 3221224624 3221223760 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35017 32410 603 41 0 34976 0
vsize: 140068
[startup+690.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 33009 0 0 0 68918 90 0 0 25 0 1 0 492089861 144502784 32651 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35279 32651 603 41 0 35238 0
vsize: 141116
[startup+700.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 33246 0 0 0 69917 91 0 0 25 0 1 0 492089861 145436672 32888 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35507 32888 603 41 0 35466 0
vsize: 142028
[startup+710.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 33538 0 0 0 70916 92 0 0 25 0 1 0 492089861 146653184 33180 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35804 33180 603 41 0 35763 0
vsize: 143216
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 33820 0 0 0 71916 93 0 0 25 0 1 0 492089861 147730432 33462 4294967295 134512640 134672761 3221224624 3221223728 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36067 33462 603 41 0 36026 0
vsize: 144268
[startup+730.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 34150 0 0 0 72915 93 0 0 25 0 1 0 492089861 149061632 33792 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36392 33792 603 41 0 36351 0
vsize: 145568
[startup+740.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 34450 0 0 0 73914 94 0 0 25 0 1 0 492089861 150274048 34092 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36688 34092 603 41 0 36647 0
vsize: 146752
[startup+750.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 34736 0 0 0 74914 95 0 0 25 0 1 0 492089861 151470080 34378 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36980 34378 603 41 0 36939 0
vsize: 147920
[startup+760.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 35106 0 0 0 75914 95 0 0 25 0 1 0 492089861 152948736 34748 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37341 34748 603 41 0 37300 0
vsize: 149364
[startup+770.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 35353 0 0 0 76913 96 0 0 25 0 1 0 492089861 154021888 34995 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37603 34995 603 41 0 37562 0
vsize: 150412
[startup+780.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 35673 0 0 0 77912 97 0 0 25 0 1 0 492089861 155369472 35315 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37932 35315 603 41 0 37891 0
vsize: 151728
[startup+790.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 36068 0 0 0 78911 98 0 0 25 0 1 0 492089861 156975104 35710 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38324 35710 603 41 0 38283 0
vsize: 153296
[startup+800.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 36303 0 0 0 79911 99 0 0 25 0 1 0 492089861 157908992 35945 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38552 35945 603 41 0 38511 0
vsize: 154208
[startup+810.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 36588 0 0 0 80911 99 0 0 25 0 1 0 492089861 159121408 36230 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38848 36230 603 41 0 38807 0
vsize: 155392
[startup+820.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 36873 0 0 0 81910 100 0 0 25 0 1 0 492089861 160210944 36515 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39114 36515 603 41 0 39073 0
vsize: 156456
[startup+830.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 37224 0 0 0 82909 101 0 0 25 0 1 0 492089861 161681408 36866 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39473 36866 603 41 0 39432 0
vsize: 157892
[startup+840.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 37674 0 0 0 83908 102 0 0 25 0 1 0 492089861 163549184 37316 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39929 37316 603 41 0 39888 0
vsize: 159716
[startup+850.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 38069 0 0 0 84907 103 0 0 25 0 1 0 492089861 165167104 37711 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40324 37711 603 41 0 40283 0
vsize: 161296
[startup+860.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 38406 0 0 0 85907 104 0 0 25 0 1 0 492089861 166510592 38048 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40652 38048 603 41 0 40611 0
vsize: 162608
[startup+870.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 38693 0 0 0 86906 105 0 0 25 0 1 0 492089861 167727104 38335 4294967295 134512640 134672761 3221224624 3221223760 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40949 38335 603 41 0 40908 0
vsize: 163796
[startup+880.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 39005 0 0 0 87905 106 0 0 25 0 1 0 492089861 168943616 38647 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41246 38647 603 41 0 41205 0
vsize: 164984
[startup+890.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 39283 0 0 0 88904 107 0 0 25 0 1 0 492089861 170024960 38925 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41510 38925 603 41 0 41469 0
vsize: 166040
[startup+900.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 39606 0 0 0 89904 108 0 0 25 0 1 0 492089861 171364352 39248 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41837 39248 603 41 0 41796 0
vsize: 167348
[startup+910.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 40025 0 0 0 90903 108 0 0 25 0 1 0 492089861 173117440 39667 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42265 39667 603 41 0 42224 0
vsize: 169060
[startup+920.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 40431 0 0 0 91903 109 0 0 25 0 1 0 492089861 174743552 40073 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42662 40073 603 41 0 42621 0
vsize: 170648
[startup+930.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 40839 0 0 0 92902 110 0 0 25 0 1 0 492089861 176484352 40481 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43087 40481 603 41 0 43046 0
vsize: 172348
[startup+940.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 41278 0 0 0 93902 110 0 0 25 0 1 0 492089861 178241536 40920 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43516 40920 603 41 0 43475 0
vsize: 174064
[startup+950.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 41673 0 0 0 94900 112 0 0 25 0 1 0 492089861 179855360 41315 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43910 41315 603 41 0 43869 0
vsize: 175640
[startup+960.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 42083 0 0 0 95900 113 0 0 25 0 1 0 492089861 181563392 41725 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44327 41725 603 41 0 44286 0
vsize: 177308
[startup+970.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 42440 0 0 0 96899 114 0 0 25 0 1 0 492089861 182915072 42082 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44657 42082 603 41 0 44616 0
vsize: 178628
[startup+980.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 42649 0 0 0 97899 114 0 0 25 0 1 0 492089861 183840768 42291 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44883 42291 603 41 0 44842 0
vsize: 179532
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 42947 0 0 0 98898 115 0 0 25 0 1 0 492089861 185057280 42589 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45180 42589 603 41 0 45139 0
vsize: 180720
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 43283 0 0 0 99897 116 0 0 25 0 1 0 492089861 186404864 42925 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45509 42925 603 41 0 45468 0
vsize: 182036
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 43595 0 0 0 100897 117 0 0 25 0 1 0 492089861 187625472 43237 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45807 43237 603 41 0 45766 0
vsize: 183228
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 43961 0 0 0 101896 117 0 0 25 0 1 0 492089861 189235200 43603 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46200 43603 603 41 0 46159 0
vsize: 184800
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 44379 0 0 0 102896 118 0 0 25 0 1 0 492089861 190840832 44021 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46592 44021 603 41 0 46551 0
vsize: 186368
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 44639 0 0 0 103895 119 0 0 25 0 1 0 492089861 192446464 44281 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46984 44281 603 41 0 46943 0
vsize: 187936
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 44916 0 0 0 104894 120 0 0 25 0 1 0 492089861 193658880 44558 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47280 44560 603 41 0 47239 0
vsize: 189120
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 45188 0 0 0 105893 121 0 0 25 0 1 0 492089861 194715648 44830 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47538 44830 603 41 0 47497 0
vsize: 190152
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 45480 0 0 0 106893 121 0 0 25 0 1 0 492089861 195932160 45122 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47835 45122 603 41 0 47794 0
vsize: 191340
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 45738 0 0 0 107892 122 0 0 25 0 1 0 492089861 197013504 45380 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48099 45380 603 41 0 48058 0
vsize: 192396
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 46086 0 0 0 108891 123 0 0 25 0 1 0 492089861 198348800 45728 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48425 45728 603 41 0 48384 0
vsize: 193700
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 46435 0 0 0 109891 124 0 0 25 0 1 0 492089861 199823360 46077 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48785 46077 603 41 0 48744 0
vsize: 195140
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 46779 0 0 0 110890 125 0 0 25 0 1 0 492089861 201170944 46421 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49114 46421 603 41 0 49073 0
vsize: 196456
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 47078 0 0 0 111890 125 0 0 25 0 1 0 492089861 202514432 46720 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49442 46720 603 41 0 49401 0
vsize: 197768
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 47281 0 0 0 112889 126 0 0 25 0 1 0 492089861 203313152 46923 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49637 46923 603 41 0 49596 0
vsize: 198548
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 47545 0 0 0 113890 126 0 0 25 0 1 0 492089861 204382208 47187 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49898 47187 603 41 0 49857 0
vsize: 199592
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 47871 0 0 0 114889 127 0 0 25 0 1 0 492089861 205737984 47513 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50229 47513 603 41 0 50188 0
vsize: 200916
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 48226 0 0 0 115889 128 0 0 25 0 1 0 492089861 207204352 47868 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50587 47868 603 41 0 50546 0
vsize: 202348
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 48552 0 0 0 116889 129 0 0 25 0 1 0 492089861 208539648 48194 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50913 48194 603 41 0 50872 0
vsize: 203652
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 48833 0 0 0 117888 129 0 0 25 0 1 0 492089861 209616896 48475 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51176 48475 603 41 0 51135 0
vsize: 204704
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 49145 0 0 0 118888 131 0 0 25 0 1 0 492089861 210968576 48787 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51506 48787 603 41 0 51465 0
vsize: 206024
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16565
Raw data (stat): 16561 (minisat+) R 16560 32461 32460 0 -1 0 49436 0 0 0 119888 131 0 0 25 0 1 0 492089861 212037632 49078 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51767 49078 603 41 0 51726 0
vsize: 207068
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 16565
Raw data (stat): 16561 (minisat+) Z 16560 32461 32460 0 -1 12 49438 0 0 0 119888 140 0 0 25 0 1 0 492089861 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.15
CPU time (s): 1200.29
CPU user time (s): 1198.89
CPU system time (s): 1.40679
CPU usage (%): 100.012
Max. virtual memory (Kb): 207068
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####