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/miplib2003/normalized-mps-v2-20-10-air04.opb
MD5SUM	ee388359e66788d310d5d5b34d6465c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63236
Optimality of the best value was proved	NO
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	SAT
Best CPU time to get the best result obtained on this benchmark	1185.16
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 16846

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        813732 kB
Buffers:         22192 kB
Cached:         169924 kB
SwapCached:        596 kB
Active:          79620 kB
Inactive:       116052 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        813480 kB
SwapTotal:     2097892 kB
SwapFree:      2097284 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6628 kB
Slab:            19548 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 09:02:38 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 12441 7 1200.18 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:   67
c ---[1640]---> BDD-cost:  303
c ---[1638]---> BDD-cost:  119
c ---[1636]---> BDD-cost:  145
c ---[1634]---> BDD-cost:  165
c ---[1632]---> BDD-cost:  239
c ---[1630]---> BDD-cost:  223
c ---[1628]---> BDD-cost:   59
c ---[1626]---> BDD-cost:   35
c ---[1624]---> BDD-cost:   93
c ---[1622]---> BDD-cost:   45
c ---[1620]---> BDD-cost:  213
c ---[1618]---> BDD-cost:   73
c ---[1616]---> BDD-cost:   75
c ---[1614]---> BDD-cost:   63
c ---[1612]---> BDD-cost:   99
c ---[1608]---> BDD-cost:  187
c ---[1606]---> BDD-cost:   55
c ---[1604]---> BDD-cost:  107
c ---[1602]---> BDD-cost:   69
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   75
c ---[1596]---> BDD-cost:    3
c ---[1594]---> BDD-cost:  149
c ---[1592]---> BDD-cost:  137
c ---[1590]---> BDD-cost:  195
c ---[1588]---> BDD-cost:   93
c ---[1586]---> BDD-cost:  157
c ---[1584]---> BDD-cost:  233
c ---[1582]---> BDD-cost:  223
c ---[1580]---> BDD-cost:  225
c ---[1578]---> BDD-cost:  247
c ---[1576]---> BDD-cost:   75
c ---[1574]---> BDD-cost:  179
c ---[1572]---> BDD-cost:  225
c ---[1570]---> BDD-cost:  243
c ---[1568]---> BDD-cost:  199
c ---[1566]---> BDD-cost:   55
c ---[1564]---> BDD-cost:   57
c ---[1562]---> BDD-cost:   99
c ---[1560]---> BDD-cost:    9
c ---[1558]---> BDD-cost:    3
c ---[1556]---> BDD-cost:   23
c ---[1554]---> BDD-cost:   55
c ---[1552]---> BDD-cost:   51
c ---[1550]---> BDD-cost:   25
c ---[1548]---> BDD-cost:   23
c ---[1546]---> BDD-cost:   27
c ---[1544]---> BDD-cost:   15
c ---[1542]---> BDD-cost:   37
c ---[1540]---> BDD-cost:   67
c ---[1538]---> BDD-cost:   67
c ---[1536]---> BDD-cost:  109
c ---[1534]---> BDD-cost:  211
c ---[1532]---> BDD-cost:   15
c ---[1530]---> BDD-cost:    0
c ---[1526]---> BDD-cost:   65
c ---[1524]---> BDD-cost:  117
c ---[1522]---> BDD-cost:   65
c ---[1520]---> BDD-cost:   65
c ---[1518]---> BDD-cost:   49
c ---[1516]---> BDD-cost:  439
c ---[1514]---> BDD-cost:  423
c ---[1512]---> BDD-cost:  287
c ---[1510]---> BDD-cost:   87
c ---[1508]---> BDD-cost:  217
c ---[1506]---> BDD-cost:  195
c ---[1504]---> BDD-cost:   63
c ---[1502]---> BDD-cost:   53
c ---[1500]---> BDD-cost:  359
c ---[1498]---> BDD-cost:  353
c ---[1494]---> BDD-cost:  169
c ---[1492]---> BDD-cost:  139
c ---[1490]---> BDD-cost:  159
c ---[1488]---> BDD-cost:   51
c ---[1486]---> BDD-cost:  223
c ---[1484]---> BDD-cost:  107
c ---[1482]---> BDD-cost:   75
c ---[1480]---> BDD-cost:  109
c ---[1478]---> BDD-cost:   93
c ---[1476]---> BDD-cost:   87
c ---[1474]---> BDD-cost:   87
c ---[1472]---> BDD-cost:    7
c ---[1468]---> BDD-cost:   73
c ---[1466]---> BDD-cost:    1
c ---[1464]---> BDD-cost:   71
c ---[1462]---> BDD-cost:  107
c ---[1460]---> BDD-cost:   77
c ---[1458]---> BDD-cost:    3
c ---[1456]---> BDD-cost:  107
c ---[1454]---> BDD-cost:  131
c ---[1452]---> BDD-cost:  135
c ---[1450]---> BDD-cost:   65
c ---[1448]---> BDD-cost:  165
c ---[1446]---> BDD-cost:  123
c ---[1444]---> BDD-cost:    1
c ---[1442]---> BDD-cost:    1
c ---[1440]---> BDD-cost:   87
c ---[1438]---> BDD-cost:  155
c ---[1436]---> BDD-cost:  167
c ---[1434]---> BDD-cost:  203
c ---[1432]---> BDD-cost:  231
c ---[1430]---> BDD-cost:  147
c ---[1428]---> BDD-cost:  135
c ---[1426]---> BDD-cost:   49
c ---[1424]---> BDD-cost:   31
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   23
c ---[1418]---> BDD-cost:   95
c ---[1416]---> BDD-cost:  325
c ---[1414]---> BDD-cost:  333
c ---[1412]---> BDD-cost:  173
c ---[1410]---> BDD-cost:  269
c ---[1408]---> BDD-cost:   31
c ---[1406]---> BDD-cost:  413
c ---[1404]---> BDD-cost:  313
c ---[1402]---> BDD-cost:  125
c ---[1400]---> BDD-cost:  113
c ---[1398]---> BDD-cost:   11
c ---[1396]---> BDD-cost:  247
c ---[1394]---> BDD-cost:   57
c ---[1392]---> BDD-cost:  237
c ---[1390]---> BDD-cost:  159
c ---[1388]---> BDD-cost:  117
c ---[1386]---> BDD-cost:   43
c ---[1384]---> BDD-cost:  143
c ---[1382]---> BDD-cost:   65
c ---[1380]---> BDD-cost:  123
c ---[1378]---> BDD-cost:   61
c ---[1376]---> BDD-cost:   39
c ---[1374]---> BDD-cost:  103
c ---[1372]---> BDD-cost:   85
c ---[1370]---> BDD-cost:   77
c ---[1368]---> BDD-cost:   57
c ---[1366]---> BDD-cost:  127
c ---[1364]---> BDD-cost:  157
c ---[1362]---> BDD-cost:  267
c ---[1360]---> BDD-cost:  223
c ---[1358]---> BDD-cost:  229
c ---[1356]---> BDD-cost:  257
c ---[1354]---> BDD-cost:   13
c ---[1352]---> BDD-cost:  241
c ---[1350]---> BDD-cost:  195
c ---[1348]---> BDD-cost:   49
c ---[1346]---> BDD-cost:  117
c ---[1344]---> BDD-cost:  197
c ---[1342]---> BDD-cost:  171
c ---[1340]---> BDD-cost:  287
c ---[1338]---> BDD-cost:   75
c ---[1336]---> BDD-cost:  215
c ---[1334]---> BDD-cost:  119
c ---[1332]---> BDD-cost:   57
c ---[1330]---> BDD-cost:  245
c ---[1328]---> BDD-cost:  257
c ---[1326]---> BDD-cost:  279
c ---[1324]---> BDD-cost:  227
c ---[1322]---> BDD-cost:  201
c ---[1320]---> BDD-cost:  143
c ---[1318]---> BDD-cost:  207
c ---[1316]---> BDD-cost:  131
c ---[1314]---> BDD-cost:  245
c ---[1312]---> BDD-cost:  115
c ---[1310]---> BDD-cost:  259
c ---[1308]---> BDD-cost:   91
c ---[1306]---> BDD-cost:   43
c ---[1304]---> BDD-cost:   39
c ---[1302]---> BDD-cost:   91
c ---[1300]---> BDD-cost:  179
c ---[1298]---> BDD-cost:   73
c ---[1296]---> BDD-cost:   29
c ---[1294]---> BDD-cost:  163
c ---[1292]---> BDD-cost:   81
c ---[1290]---> BDD-cost:   63
c ---[1288]---> BDD-cost:  189
c ---[1286]---> BDD-cost:  103
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  115
c ---[1280]---> BDD-cost:   19
c ---[1278]---> BDD-cost:   93
c ---[1276]---> BDD-cost:   99
c ---[1274]---> BDD-cost:   99
c ---[1272]---> BDD-cost:  103
c ---[1270]---> BDD-cost:   67
c ---[1268]---> BDD-cost:   23
c ---[1266]---> BDD-cost:  101
c ---[1264]---> BDD-cost:   85
c ---[1262]---> BDD-cost:   87
c ---[1260]---> BDD-cost:    7
c ---[1258]---> BDD-cost:   45
c ---[1256]---> BDD-cost:   43
c ---[1254]---> BDD-cost:   11
c ---[1252]---> BDD-cost:   59
c ---[1250]---> BDD-cost:  185
c ---[1248]---> BDD-cost:  249
c ---[1246]---> BDD-cost:  315
c ---[1244]---> BDD-cost:  137
c ---[1242]---> BDD-cost:  253
c ---[1240]---> BDD-cost:  161
c ---[1238]---> BDD-cost:  257
c ---[1236]---> BDD-cost:  167
c ---[1234]---> BDD-cost:  167
c ---[1232]---> BDD-cost:  141
c ---[1230]---> BDD-cost:   21
c ---[1228]---> BDD-cost:   10
c ---[1226]---> BDD-cost:   95
c ---[1224]---> BDD-cost:  141
c ---[1222]---> BDD-cost:    0
c ---[1220]---> BDD-cost:  123
c ---[1218]---> BDD-cost:   83
c ---[1216]---> BDD-cost:   55
c ---[1214]---> BDD-cost:  183
c ---[1212]---> BDD-cost:  269
c ---[1210]---> BDD-cost:   63
c ---[1208]---> BDD-cost:   45
c ---[1206]---> BDD-cost:   39
c ---[1204]---> BDD-cost:   97
c ---[1202]---> BDD-cost:   51
c ---[1200]---> BDD-cost:   23
c ---[1198]---> BDD-cost:  101
c ---[1196]---> BDD-cost:   45
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   85
c ---[1190]---> BDD-cost:   35
c ---[1188]---> BDD-cost:   53
c ---[1186]---> BDD-cost:   21
c ---[1184]---> BDD-cost:  115
c ---[1182]---> BDD-cost:   99
c ---[1180]---> BDD-cost:   63
c ---[1178]---> BDD-cost:   77
c ---[1176]---> BDD-cost:   37
c ---[1174]---> BDD-cost:  139
c ---[1172]---> BDD-cost:  109
c ---[1170]---> BDD-cost:  407
c ---[1168]---> BDD-cost:  323
c ---[1166]---> BDD-cost:  109
c ---[1164]---> BDD-cost:   93
c ---[1162]---> BDD-cost:   51
c ---[1160]---> BDD-cost:   79
c ---[1158]---> BDD-cost:   75
c ---[1156]---> BDD-cost:  147
c ---[1154]---> BDD-cost:    0
c ---[1152]---> BDD-cost:  169
c ---[1150]---> BDD-cost:  209
c ---[1148]---> BDD-cost:   69
c ---[1146]---> BDD-cost:   51
c ---[1144]---> BDD-cost:   85
c ---[1140]---> BDD-cost:  103
c ---[1138]---> BDD-cost:  127
c ---[1136]---> BDD-cost:   77
c ---[1134]---> BDD-cost:   77
c ---[1132]---> BDD-cost:  181
c ---[1130]---> BDD-cost:  141
c ---[1128]---> BDD-cost:   89
c ---[1126]---> BDD-cost:   85
c ---[1124]---> BDD-cost:  119
c ---[1122]---> BDD-cost:   69
c ---[1120]---> BDD-cost:   57
c ---[1118]---> BDD-cost:   65
c ---[1116]---> BDD-cost:   47
c ---[1114]---> BDD-cost:   61
c ---[1112]---> BDD-cost:   31
c ---[1110]---> BDD-cost:  283
c ---[1106]---> BDD-cost:  183
c ---[1104]---> BDD-cost:  121
c ---[1102]---> BDD-cost:   89
c ---[1100]---> BDD-cost:  225
c ---[1098]---> BDD-cost:  267
c ---[1094]---> BDD-cost:  159
c ---[1092]---> BDD-cost:  209
c ---[1090]---> BDD-cost:   71
c ---[1088]---> BDD-cost:   99
c ---[1086]---> BDD-cost:  237
c ---[1084]---> BDD-cost:  129
c ---[1082]---> BDD-cost:  365
c ---[1080]---> BDD-cost:  369
c ---[1078]---> BDD-cost:  129
c ---[1076]---> BDD-cost:  101
c ---[1074]---> BDD-cost:  289
c ---[1072]---> BDD-cost:  279
c ---[1070]---> BDD-cost:  345
c ---[1068]---> BDD-cost:   81
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:   69
c ---[1062]---> BDD-cost:   83
c ---[1060]---> BDD-cost:   53
c ---[1058]---> BDD-cost:   67
c ---[1056]---> BDD-cost:   55
c ---[1054]---> BDD-cost:  145
c ---[1052]---> BDD-cost:  149
c ---[1050]---> BDD-cost:  105
c ---[1048]---> BDD-cost:   19
c ---[1046]---> BDD-cost:  105
c ---[1044]---> BDD-cost:  109
c ---[1042]---> BDD-cost:  101
c ---[1040]---> BDD-cost:  147
c ---[1038]---> BDD-cost:  231
c ---[1036]---> BDD-cost:  191
c ---[1034]---> BDD-cost:  157
c ---[1032]---> BDD-cost:  249
c ---[1030]---> BDD-cost:  385
c ---[1028]---> BDD-cost:   67
c ---[1026]---> BDD-cost:   71
c ---[1024]---> BDD-cost:   47
c ---[1022]---> BDD-cost:   75
c ---[1020]---> BDD-cost:  147
c ---[1018]---> BDD-cost:  139
c ---[1016]---> BDD-cost:  273
c ---[1014]---> BDD-cost:  213
c ---[1012]---> BDD-cost:  169
c ---[1010]---> BDD-cost:  239
c ---[1008]---> BDD-cost:  305
c ---[1006]---> BDD-cost:  109
c ---[1004]---> BDD-cost:  105
c ---[1002]---> BDD-cost:  147
c ---[1000]---> BDD-cost:  237
c ---[ 998]---> BDD-cost:  115
c ---[ 996]---> BDD-cost:  115
c ---[ 994]---> BDD-cost:   67
c ---[ 992]---> BDD-cost:  329
c ---[ 990]---> BDD-cost:  295
c ---[ 988]---> BDD-cost:   51
c ---[ 986]---> BDD-cost:   61
c ---[ 984]---> BDD-cost:  317
c ---[ 982]---> BDD-cost:   97
c ---[ 980]---> BDD-cost:   79
c ---[ 978]---> BDD-cost:   29
c ---[ 976]---> BDD-cost:  119
c ---[ 974]---> BDD-cost:   43
c ---[ 972]---> BDD-cost:   85
c ---[ 970]---> BDD-cost:   35
c ---[ 968]---> BDD-cost:   69
c ---[ 964]---> BDD-cost:   45
c ---[ 962]---> BDD-cost:   73
c ---[ 960]---> BDD-cost:   55
c ---[ 956]---> BDD-cost:   33
c ---[ 954]---> BDD-cost:  109
c ---[ 952]---> BDD-cost:   29
c ---[ 950]---> BDD-cost:  245
c ---[ 948]---> BDD-cost:  225
c ---[ 946]---> BDD-cost:  111
c ---[ 944]---> BDD-cost:  117
c ---[ 942]---> BDD-cost:  127
c ---[ 940]---> BDD-cost:  129
c ---[ 938]---> BDD-cost:  259
c ---[ 936]---> BDD-cost:  221
c ---[ 934]---> BDD-cost:  275
c ---[ 932]---> BDD-cost:   83
c ---[ 930]---> BDD-cost:  209
c ---[ 928]---> BDD-cost:  267
c ---[ 926]---> BDD-cost:  171
c ---[ 924]---> BDD-cost:   57
c ---[ 920]---> BDD-cost:  133
c ---[ 918]---> BDD-cost:  185
c ---[ 916]---> BDD-cost:  169
c ---[ 914]---> BDD-cost:  287
c ---[ 912]---> BDD-cost:   81
c ---[ 910]---> BDD-cost:   13
c ---[ 908]---> BDD-cost:  335
c ---[ 906]---> BDD-cost:  365
c ---[ 904]---> BDD-cost:  255
c ---[ 902]---> BDD-cost:  111
c ---[ 900]---> BDD-cost:   57
c ---[ 898]---> BDD-cost:  101
c ---[ 896]---> BDD-cost:  197
c ---[ 894]---> BDD-cost:  383
c ---[ 892]---> BDD-cost:  329
c ---[ 890]---> BDD-cost:  241
c ---[ 888]---> BDD-cost:  157
c ---[ 886]---> BDD-cost:  129
c ---[ 884]---> BDD-cost:   85
c ---[ 882]---> BDD-cost:   71
c ---[ 880]---> BDD-cost:   37
c ---[ 878]---> BDD-cost:   77
c ---[ 876]---> BDD-cost:   49
c ---[ 874]---> BDD-cost:  133
c ---[ 872]---> BDD-cost:  133
c ---[ 870]---> BDD-cost:  377
c ---[ 868]---> BDD-cost:  117
c ---[ 866]---> BDD-cost:  155
c ---[ 862]---> BDD-cost:  119
c ---[ 860]---> BDD-cost:  119
c ---[ 858]---> BDD-cost:  151
c ---[ 856]---> BDD-cost:  221
c ---[ 854]---> BDD-cost:  181
c ---[ 850]---> BDD-cost:   87
c ---[ 848]---> BDD-cost:  127
c ---[ 846]---> BDD-cost:  299
c ---[ 844]---> BDD-cost:  109
c ---[ 842]---> BDD-cost:  331
c ---[ 838]---> BDD-cost:   21
c ---[ 836]---> BDD-cost:  205
c ---[ 834]---> BDD-cost:  217
c ---[ 832]---> BDD-cost:  349
c ---[ 830]---> BDD-cost:  291
c ---[ 828]---> BDD-cost:  165
c ---[ 826]---> BDD-cost:  161
c ---[ 824]---> BDD-cost:   61
c ---[ 822]---> BDD-cost:   77
c ---[ 820]---> BDD-cost:   55
c ---[ 818]---> BDD-cost:  113
c ---[ 816]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:  189
c ---[ 812]---> BDD-cost:  157
c ---[ 810]---> BDD-cost:  149
c ---[ 808]---> BDD-cost:  139
c ---[ 806]---> BDD-cost:  165
c ---[ 804]---> BDD-cost:  181
c ---[ 802]---> BDD-cost:  253
c ---[ 800]---> BDD-cost:    0
c ---[ 798]---> BDD-cost:   43
c ---[ 796]---> BDD-cost:  145
c ---[ 794]---> BDD-cost:  141
c ---[ 792]---> BDD-cost:  105
c ---[ 790]---> BDD-cost:   95
c ---[ 788]---> BDD-cost:   75
c ---[ 786]---> BDD-cost:  103
c ---[ 784]---> BDD-cost:  149
c ---[ 782]---> BDD-cost:  137
c ---[ 780]---> BDD-cost:   59
c ---[ 778]---> BDD-cost:  133
c ---[ 776]---> BDD-cost:    5
c ---[ 774]---> BDD-cost:   35
c ---[ 772]---> BDD-cost:    9
c ---[ 770]---> BDD-cost:   35
c ---[ 768]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   55
c ---[ 762]---> BDD-cost:  197
c ---[ 760]---> BDD-cost:  191
c ---[ 758]---> BDD-cost:  125
c ---[ 756]---> BDD-cost:    0
c ---[ 754]---> BDD-cost:  103
c ---[ 752]---> BDD-cost:  173
c ---[ 748]---> BDD-cost:   93
c ---[ 746]---> BDD-cost:   29
c ---[ 744]---> BDD-cost:  321
c ---[ 742]---> BDD-cost:  195
c ---[ 740]---> BDD-cost:  163
c ---[ 734]---> BDD-cost:  151
c ---[ 732]---> BDD-cost:  115
c ---[ 730]---> BDD-cost:  253
c ---[ 728]---> BDD-cost:  381
c ---[ 726]---> BDD-cost:  345
c ---[ 724]---> BDD-cost:  185
c ---[ 720]---> BDD-cost:   83
c ---[ 718]---> BDD-cost:   69
c ---[ 716]---> BDD-cost:   51
c ---[ 714]---> BDD-cost:   47
c ---[ 712]---> BDD-cost:   59
c ---[ 710]---> BDD-cost:  185
c ---[ 708]---> BDD-cost:   83
c ---[ 706]---> BDD-cost:  107
c ---[ 704]---> BDD-cost:  363
c ---[ 702]---> BDD-cost:  103
c ---[ 700]---> BDD-cost:  277
c ---[ 698]---> BDD-cost:  341
c ---[ 696]---> BDD-cost:  213
c ---[ 694]---> BDD-cost:  315
c ---[ 692]---> BDD-cost:  275
c ---[ 690]---> BDD-cost:  151
c ---[ 688]---> BDD-cost:  203
c ---[ 686]---> BDD-cost:  111
c ---[ 684]---> BDD-cost:  103
c ---[ 682]---> BDD-cost:   75
c ---[ 680]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   21
c ---[ 676]---> BDD-cost:   11
c ---[ 674]---> BDD-cost:   31
c ---[ 670]---> BDD-cost:   19
c ---[ 668]---> BDD-cost:  149
c ---[ 666]---> BDD-cost:  167
c ---[ 664]---> BDD-cost:    0
c ---[ 662]---> BDD-cost:   97
c ---[ 660]---> BDD-cost:  149
c ---[ 658]---> BDD-cost:  395
c ---[ 656]---> BDD-cost:   25
c ---[ 654]---> BDD-cost:  389
c ---[ 652]---> BDD-cost:  251
c ---[ 650]---> BDD-cost:  375
c ---[ 648]---> BDD-cost:  343
c ---[ 646]---> BDD-cost:  267
c ---[ 644]---> BDD-cost:  135
c ---[ 642]---> BDD-cost:  135
c ---[ 640]---> BDD-cost:  263
c ---[ 638]---> BDD-cost:  259
c ---[ 636]---> BDD-cost:  245
c ---[ 634]---> BDD-cost:   45
c ---[ 632]---> BDD-cost:   41
c ---[ 630]---> BDD-cost:  127
c ---[ 628]---> BDD-cost:  117
c ---[ 626]---> BDD-cost:   53
c ---[ 624]---> BDD-cost:  149
c ---[ 622]---> BDD-cost:    9
c ---[ 620]---> BDD-cost:  103
c ---[ 618]---> BDD-cost:  215
c ---[ 616]---> BDD-cost:   89
c ---[ 614]---> BDD-cost:  177
c ---[ 612]---> BDD-cost:  343
c ---[ 610]---> BDD-cost:  237
c ---[ 608]---> BDD-cost:  177
c ---[ 606]---> BDD-cost:   85
c ---[ 604]---> BDD-cost:  267
c ---[ 602]---> BDD-cost:  225
c ---[ 600]---> BDD-cost:   85
c ---[ 598]---> BDD-cost:  109
c ---[ 596]---> BDD-cost:  105
c ---[ 594]---> BDD-cost:  113
c ---[ 592]---> BDD-cost:   55
c ---[ 590]---> BDD-cost:  117
c ---[ 588]---> BDD-cost:   83
c ---[ 586]---> BDD-cost:   79
c ---[ 584]---> BDD-cost:   81
c ---[ 582]---> BDD-cost:  263
c ---[ 580]---> BDD-cost:  179
c ---[ 578]---> BDD-cost:  143
c ---[ 576]---> BDD-cost:  281
c ---[ 574]---> BDD-cost:  389
c ---[ 572]---> BDD-cost:  333
c ---[ 570]---> BDD-cost:  357
c ---[ 568]---> BDD-cost:  345
c ---[ 566]---> BDD-cost:  263
c ---[ 564]---> BDD-cost:   89
c ---[ 562]---> BDD-cost:  285
c ---[ 558]---> BDD-cost:  419
c ---[ 556]---> BDD-cost:  135
c ---[ 554]---> BDD-cost:  357
c ---[ 552]---> BDD-cost:  473
c ---[ 550]---> BDD-cost:  455
c ---[ 548]---> BDD-cost:  405
c ---[ 546]---> BDD-cost:  241
c ---[ 544]---> BDD-cost:  211
c ---[ 542]---> BDD-cost:  313
c ---[ 540]---> BDD-cost:  371
c ---[ 538]---> BDD-cost:  389
c ---[ 536]---> BDD-cost:  223
c ---[ 534]---> BDD-cost:   71
c ---[ 532]---> BDD-cost:   63
c ---[ 530]---> BDD-cost:  221
c ---[ 528]---> BDD-cost:  147
c ---[ 526]---> BDD-cost:  131
c ---[ 524]---> BDD-cost:  185
c ---[ 522]---> BDD-cost:  141
c ---[ 520]---> BDD-cost:  249
c ---[ 518]---> BDD-cost:  261
c ---[ 516]---> BDD-cost:  311
c ---[ 514]---> BDD-cost:  261
c ---[ 512]---> BDD-cost:  387
c ---[ 510]---> BDD-cost:   51
c ---[ 508]---> BDD-cost:  247
c ---[ 506]---> BDD-cost:  295
c ---[ 504]---> BDD-cost:   31
c ---[ 502]---> BDD-cost:  355
c ---[ 500]---> BDD-cost:  135
c ---[ 498]---> BDD-cost:  443
c ---[ 496]---> BDD-cost:  653
c ---[ 494]---> BDD-cost:  703
c ---[ 492]---> BDD-cost:  517
c ---[ 490]---> BDD-cost:  441
c ---[ 488]---> BDD-cost:  159
c ---[ 486]---> BDD-cost:  411
c ---[ 484]---> BDD-cost:  289
c ---[ 482]---> BDD-cost:  277
c ---[ 480]---> BDD-cost:  239
c ---[ 478]---> BDD-cost:  201
c ---[ 476]---> BDD-cost:  309
c ---[ 474]---> BDD-cost:  287
c ---[ 472]---> BDD-cost:  177
c ---[ 470]---> BDD-cost:  143
c ---[ 468]---> BDD-cost:  131
c ---[ 466]---> BDD-cost:  155
c ---[ 464]---> BDD-cost:   35
c ---[ 462]---> BDD-cost:  189
c ---[ 460]---> BDD-cost:  219
c ---[ 456]---> BDD-cost:  267
c ---[ 454]---> BDD-cost:  135
c ---[ 452]---> BDD-cost:   69
c ---[ 450]---> BDD-cost:   75
c ---[ 448]---> BDD-cost:   51
c ---[ 446]---> BDD-cost:  117
c ---[ 444]---> BDD-cost:  211
c ---[ 442]---> BDD-cost:  117
c ---[ 436]---> BDD-cost:  189
c ---[ 434]---> BDD-cost:   73
c ---[ 432]---> BDD-cost:   55
c ---[ 430]---> BDD-cost:   57
c ---[ 428]---> BDD-cost:   91
c ---[ 426]---> BDD-cost:  325
c ---[ 424]---> BDD-cost:  223
c ---[ 422]---> BDD-cost:   75
c ---[ 420]---> BDD-cost:   57
c ---[ 418]---> BDD-cost:   43
c ---[ 416]---> BDD-cost:  255
c ---[ 414]---> BDD-cost:  285
c ---[ 412]---> BDD-cost:  187
c ---[ 410]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   91
c ---[ 406]---> BDD-cost:  211
c ---[ 404]---> BDD-cost:  159
c ---[ 402]---> BDD-cost:   97
c ---[ 400]---> BDD-cost:   37
c ---[ 398]---> BDD-cost:   27
c ---[ 396]---> BDD-cost:  101
c ---[ 394]---> BDD-cost:  141
c ---[ 390]---> BDD-cost:  109
c ---[ 388]---> BDD-cost:  321
c ---[ 386]---> BDD-cost:  305
c ---[ 384]---> BDD-cost:  603
c ---[ 382]---> BDD-cost:  441
c ---[ 380]---> BDD-cost:  391
c ---[ 378]---> BDD-cost:   87
c ---[ 376]---> BDD-cost:  387
c ---[ 374]---> BDD-cost:  289
c ---[ 372]---> BDD-cost:  219
c ---[ 370]---> BDD-cost:  309
c ---[ 368]---> BDD-cost:  241
c ---[ 366]---> BDD-cost:  197
c ---[ 364]---> BDD-cost:  279
c ---[ 362]---> BDD-cost:  167
c ---[ 360]---> BDD-cost:  151
c ---[ 358]---> BDD-cost:   49
c ---[ 356]---> BDD-cost:   79
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> BDD-cost:  107
c ---[ 350]---> BDD-cost:   55
c ---[ 346]---> BDD-cost:  177
c ---[ 344]---> BDD-cost:  223
c ---[ 342]---> BDD-cost:  119
c ---[ 340]---> BDD-cost:  137
c ---[ 338]---> BDD-cost:  105
c ---[ 336]---> BDD-cost:  183
c ---[ 334]---> BDD-cost:  109
c ---[ 332]---> BDD-cost:  179
c ---[ 330]---> BDD-cost:  285
c ---[ 328]---> BDD-cost:  191
c ---[ 326]---> BDD-cost:  177
c ---[ 324]---> BDD-cost:  145
c ---[ 320]---> BDD-cost:  153
c ---[ 318]---> BDD-cost:  121
c ---[ 316]---> BDD-cost:   95
c ---[ 314]---> BDD-cost:  111
c ---[ 312]---> BDD-cost:   35
c ---[ 310]---> BDD-cost:  115
c ---[ 308]---> BDD-cost:    0
c ---[ 306]---> BDD-cost:  281
c ---[ 304]---> BDD-cost:  265
c ---[ 302]---> BDD-cost:  167
c ---[ 300]---> BDD-cost:  151
c ---[ 298]---> BDD-cost:  167
c ---[ 296]---> BDD-cost:  137
c ---[ 292]---> BDD-cost:  375
c ---[ 290]---> BDD-cost:  287
c ---[ 288]---> BDD-cost:  247
c ---[ 286]---> BDD-cost:  249
c ---[ 284]---> BDD-cost:  131
c ---[ 282]---> BDD-cost:  187
c ---[ 280]---> BDD-cost:  135
c ---[ 278]---> BDD-cost:  129
c ---[ 276]---> BDD-cost:  317
c ---[ 274]---> BDD-cost:  365
c ---[ 272]---> BDD-cost:  235
c ---[ 270]---> BDD-cost:  249
c ---[ 268]---> BDD-cost:  283
c ---[ 266]---> BDD-cost:  105
c ---[ 264]---> BDD-cost:  233
c ---[ 262]---> BDD-cost:  259
c ---[ 260]---> BDD-cost:  287
c ---[ 258]---> BDD-cost:  175
c ---[ 256]---> BDD-cost:  233
c ---[ 254]---> BDD-cost:  167
c ---[ 252]---> BDD-cost:  159
c ---[ 250]---> BDD-cost:   47
c ---[ 246]---> BDD-cost:  135
c ---[ 244]---> BDD-cost:   59
c ---[ 242]---> BDD-cost:  147
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  203
c ---[ 236]---> BDD-cost:  275
c ---[ 234]---> BDD-cost:  263
c ---[ 232]---> BDD-cost:   31
c ---[ 230]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   31
c ---[ 226]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:  225
c ---[ 222]---> BDD-cost:   71
c ---[ 220]---> BDD-cost:   65
c ---[ 218]---> BDD-cost:  385
c ---[ 216]---> BDD-cost:  361
c ---[ 214]---> BDD-cost:   73
c ---[ 212]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:  131
c ---[ 206]---> BDD-cost:  145
c ---[ 204]---> BDD-cost:  121
c ---[ 202]---> BDD-cost:  117
c ---[ 200]---> BDD-cost:   61
c ---[ 198]---> BDD-cost:  111
c ---[ 196]---> BDD-cost:  123
c ---[ 194]---> BDD-cost:  125
c ---[ 192]---> BDD-cost:  243
c ---[ 190]---> BDD-cost:  143
c ---[ 188]---> BDD-cost:  149
c ---[ 186]---> BDD-cost:  103
c ---[ 184]---> BDD-cost:  155
c ---[ 182]---> BDD-cost:  247
c ---[ 180]---> BDD-cost:  143
c ---[ 178]---> BDD-cost:   89
c ---[ 176]---> BDD-cost:   91
c ---[ 174]---> BDD-cost:   81
c ---[ 172]---> BDD-cost:   79
c ---[ 170]---> BDD-cost:  117
c ---[ 168]---> BDD-cost:   89
c ---[ 166]---> BDD-cost:   61
c ---[ 164]---> BDD-cost:  127
c ---[ 162]---> BDD-cost:  135
c ---[ 160]---> BDD-cost:  161
c ---[ 158]---> BDD-cost:  141
c ---[ 156]---> BDD-cost:   91
c ---[ 154]---> BDD-cost:  437
c ---[ 152]---> BDD-cost:  309
c ---[ 150]---> BDD-cost:  173
c ---[ 148]---> BDD-cost:  441
c ---[ 146]---> BDD-cost:  489
c ---[ 144]---> BDD-cost:  299
c ---[ 142]---> BDD-cost:  455
c ---[ 140]---> BDD-cost:  333
c ---[ 138]---> BDD-cost:  421
c ---[ 136]---> BDD-cost:  375
c ---[ 134]---> BDD-cost:  143
c ---[ 132]---> BDD-cost:  433
c ---[ 130]---> BDD-cost:  405
c ---[ 128]---> BDD-cost:  333
c ---[ 126]---> BDD-cost:  673
c ---[ 124]---> BDD-cost:  685
c ---[ 122]---> BDD-cost:  385
c ---[ 120]---> BDD-cost:  267
c ---[ 118]---> BDD-cost:  345
c ---[ 116]---> BDD-cost:  365
c ---[ 114]---> BDD-cost:  391
c ---[ 112]---> BDD-cost:  111
c ---[ 110]---> BDD-cost:  313
c ---[ 108]---> BDD-cost:  275
c ---[ 106]---> BDD-cost:  257
c ---[ 104]---> BDD-cost:  203
c ---[ 102]---> BDD-cost:  311
c ---[ 100]---> BDD-cost:  227
c ---[  98]---> BDD-cost:  295
c ---[  96]---> BDD-cost:  233
c ---[  94]---> BDD-cost:  247
c ---[  92]---> BDD-cost:  237
c ---[  90]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   95
c ---[  86]---> BDD-cost:    0
c ---[  84]---> BDD-cost:  149
c ---[  80]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   85
c ---[  76]---> BDD-cost:  109
c ---[  74]---> BDD-cost:   43
c ---[  72]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   71
c ---[  68]---> BDD-cost:   67
c ---[  66]---> BDD-cost:  169
c ---[  64]---> BDD-cost:  151
c ---[  62]---> BDD-cost:  147
c ---[  60]---> BDD-cost:  177
c ---[  58]---> BDD-cost:  127
c ---[  56]---> BDD-cost:  131
c ---[  54]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  215
c ---[  50]---> BDD-cost:  181
c ---[  48]---> BDD-cost:  235
c ---[  46]---> BDD-cost:  163
c ---[  44]---> BDD-cost:  101
c ---[  42]---> BDD-cost:   57
c ---[  40]---> BDD-cost:   59
c ---[  38]---> BDD-cost:  139
c ---[  36]---> BDD-cost:   39
c ---[  34]---> BDD-cost:  151
c ---[  32]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   45
c ---[  28]---> BDD-cost:   45
c ---[  26]---> BDD-cost:   45
c ---[  24]---> BDD-cost:   65
c ---[  22]---> BDD-cost:   95
c ---[  20]---> BDD-cost:    0
c ---[  16]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   81
c ---[   2]---> BDD-cost:  223
c ---[   0]---> BDD-cost:  271
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 |       101 |  556583  1546438 |  204124      97     3860    39.8 |  0.597 % |
c |       253 |  556583  1546438 |  224537     249     8590    34.5 |  0.597 % |
c |       480 |  556583  1546438 |  246991     476    27255    57.3 |  0.597 % |
c |       817 |  556460  1546082 |  271690     807    57537    71.3 |  0.613 % |
c |      1324 |  556460  1546082 |  298859    1314    96333    73.3 |  0.613 % |
c |      2083 |  556435  1546014 |  328745    2072   169245    81.7 |  0.614 % |
c |      3222 |  556306  1545644 |  361619    3193   235735    73.8 |  0.628 % |
c |      4933 |  556143  1545187 |  397781    4887   374517    76.6 |  0.645 % |
c |      7496 |  555762  1544105 |  437559    7324   683691    93.3 |  0.680 % |
c |     11341 |  553381  1537592 |  481315   11000  1016992    92.5 |  0.890 % |
c |     17108 |  553168  1537017 |  529447   16736  2141343   127.9 |  0.905 % |
c |     25760 |  552999  1536551 |  582391   25355  4410378   173.9 |  0.916 % |
c |     38734 |  552412  1534942 |  640631   38256  6250267   163.4 |  0.963 % |
c |     58195 |  551755  1533149 |  704694   57618 10540545   182.9 |  1.002 % |
c |     87388 |  551111  1531403 |  775163   86624 18470644   213.2 |  1.038 % |
#### 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): 1.01 1.00 0.95 2/55 25314
Raw data (stat): 25314 (runsolver) R 25313 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543733906 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+9.99966 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 12968 0 0 0 967 31 0 0 25 0 1 0 543733906 63373312 12600 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15472 12600 603 41 0 15431 0
vsize: 61888
[startup+20.0004 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 13105 0 0 0 1965 32 0 0 25 0 1 0 543733906 63913984 12737 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15604 12737 603 41 0 15563 0
vsize: 62416
[startup+30.0007 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 13243 0 0 0 2965 33 0 0 25 0 1 0 543733906 64602112 12875 4294967295 134512640 134672761 3221224544 3221223728 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15772 12875 603 41 0 15731 0
vsize: 63088
[startup+40.0003 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 13518 0 0 0 3953 34 0 0 25 0 1 0 543733906 65683456 13150 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16036 13150 603 41 0 15995 0
vsize: 64144
[startup+50.0013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 13720 0 0 0 4953 35 0 0 25 0 1 0 543733906 66547712 13352 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16247 13352 603 41 0 16206 0
vsize: 64988
[startup+60.0005 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 13863 0 0 0 5952 36 0 0 25 0 1 0 543733906 67088384 13495 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16379 13495 603 41 0 16338 0
vsize: 65516
[startup+70.0012 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 14174 0 0 0 6951 37 0 0 25 0 1 0 543733906 68300800 13806 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16675 13806 603 41 0 16634 0
vsize: 66700
[startup+80.002 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 14374 0 0 0 7950 37 0 0 25 0 1 0 543733906 69111808 14006 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16873 14006 603 41 0 16832 0
vsize: 67492
[startup+90.0013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25314
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 14730 0 0 0 8950 38 0 0 25 0 1 0 543733906 70586368 14362 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17233 14362 603 41 0 17192 0
vsize: 68932
[startup+100.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 15045 0 0 0 9949 39 0 0 25 0 1 0 543733906 71933952 14677 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17562 14677 603 41 0 17521 0
vsize: 70248
[startup+110.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 15331 0 0 0 10948 40 0 0 25 0 1 0 543733906 73158656 14963 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17861 14963 603 41 0 17820 0
vsize: 71444
[startup+120.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 15473 0 0 0 11948 40 0 0 25 0 1 0 543733906 73691136 15105 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17991 15105 603 41 0 17950 0
vsize: 71964
[startup+130.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 15693 0 0 0 12947 41 0 0 25 0 1 0 543733906 74637312 15325 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18222 15325 603 41 0 18181 0
vsize: 72888
[startup+140.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 15906 0 0 0 13947 42 0 0 25 0 1 0 543733906 75448320 15538 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18420 15538 603 41 0 18379 0
vsize: 73680
[startup+150.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 16099 0 0 0 14947 42 0 0 25 0 1 0 543733906 76251136 15731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18616 15731 603 41 0 18575 0
vsize: 74464
[startup+160.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 16528 0 0 0 15945 44 0 0 25 0 1 0 543733906 77987840 16160 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19040 16160 603 41 0 18999 0
vsize: 76160
[startup+170 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 16996 0 0 0 16944 45 0 0 25 0 1 0 543733906 79896576 16628 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19506 16628 603 41 0 19465 0
vsize: 78024
[startup+180.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 17412 0 0 0 17943 46 0 0 25 0 1 0 543733906 81514496 17044 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19901 17044 603 41 0 19860 0
vsize: 79604
[startup+190 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 17682 0 0 0 18943 47 0 0 25 0 1 0 543733906 82726912 17314 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20197 17314 603 41 0 20156 0
vsize: 80788
[startup+200 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 18101 0 0 0 19941 48 0 0 25 0 1 0 543733906 84340736 17733 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20591 17733 603 41 0 20550 0
vsize: 82364
[startup+210.001 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 18456 0 0 0 20940 50 0 0 25 0 1 0 543733906 85819392 18088 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20952 18088 603 41 0 20911 0
vsize: 83808
[startup+220 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 18685 0 0 0 21939 51 0 0 25 0 1 0 543733906 86761472 18317 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21182 18317 603 41 0 21141 0
vsize: 84728
[startup+230 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 18874 0 0 0 22939 51 0 0 25 0 1 0 543733906 87695360 18506 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21410 18506 603 41 0 21369 0
vsize: 85640
[startup+239.999 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 19089 0 0 0 23939 52 0 0 25 0 1 0 543733906 88506368 18721 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21608 18721 603 41 0 21567 0
vsize: 86432
[startup+250 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 19305 0 0 0 24938 52 0 0 25 0 1 0 543733906 89452544 18937 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21839 18937 603 41 0 21798 0
vsize: 87356
[startup+260 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 19525 0 0 0 25938 53 0 0 25 0 1 0 543733906 90255360 19157 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22035 19157 603 41 0 21994 0
vsize: 88140
[startup+270 s]
Raw data (loadavg): 1.00 1.00 0.95 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 19765 0 0 0 26937 54 0 0 25 0 1 0 543733906 91332608 19397 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22298 19397 603 41 0 22257 0
vsize: 89192
[startup+280 s]
Raw data (loadavg): 1.15 1.03 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 19998 0 0 0 27936 55 0 0 25 0 1 0 543733906 92278784 19630 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22529 19630 603 41 0 22488 0
vsize: 90116
[startup+290 s]
Raw data (loadavg): 1.13 1.03 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 20230 0 0 0 28936 55 0 0 25 0 1 0 543733906 93216768 19862 4294967295 134512640 134672761 3221224544 3221223728 134558756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22758 19862 603 41 0 22717 0
vsize: 91032
[startup+300 s]
Raw data (loadavg): 1.11 1.03 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 20483 0 0 0 29935 56 0 0 25 0 1 0 543733906 94285824 20115 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23019 20115 603 41 0 22978 0
vsize: 92076
[startup+310 s]
Raw data (loadavg): 1.09 1.03 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 20731 0 0 0 30935 57 0 0 25 0 1 0 543733906 95227904 20363 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23249 20363 603 41 0 23208 0
vsize: 92996
[startup+320 s]
Raw data (loadavg): 1.08 1.03 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 20935 0 0 0 31935 57 0 0 25 0 1 0 543733906 96030720 20567 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23445 20567 603 41 0 23404 0
vsize: 93780
[startup+330 s]
Raw data (loadavg): 1.06 1.03 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 21240 0 0 0 32934 58 0 0 25 0 1 0 543733906 97251328 20872 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23743 20872 603 41 0 23702 0
vsize: 94972
[startup+339.999 s]
Raw data (loadavg): 1.05 1.02 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 21535 0 0 0 33933 59 0 0 25 0 1 0 543733906 98463744 21167 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24039 21167 603 41 0 23998 0
vsize: 96156
[startup+350 s]
Raw data (loadavg): 1.05 1.02 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 21780 0 0 0 34933 60 0 0 25 0 1 0 543733906 99536896 21412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24301 21412 603 41 0 24260 0
vsize: 97204
[startup+360 s]
Raw data (loadavg): 1.04 1.02 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 21997 0 0 0 35933 60 0 0 25 0 1 0 543733906 100335616 21629 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24496 21629 603 41 0 24455 0
vsize: 97984
[startup+370 s]
Raw data (loadavg): 1.03 1.02 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 22241 0 0 0 36932 61 0 0 25 0 1 0 543733906 101416960 21873 4294967295 134512640 134672761 3221224544 3221223728 134558857 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24760 21873 603 41 0 24719 0
vsize: 99040
[startup+380 s]
Raw data (loadavg): 1.03 1.02 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 22486 0 0 0 37932 62 0 0 25 0 1 0 543733906 102359040 22118 4294967295 134512640 134672761 3221224544 3221223560 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24990 22118 603 41 0 24949 0
vsize: 99960
[startup+389.999 s]
Raw data (loadavg): 1.02 1.02 0.96 2/55 25316
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 22702 0 0 0 38931 62 0 0 25 0 1 0 543733906 103301120 22334 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25220 22334 603 41 0 25179 0
vsize: 100880
[startup+399.999 s]
Raw data (loadavg): 1.02 1.02 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 22994 0 0 0 39930 63 0 0 25 0 1 0 543733906 104509440 22626 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25515 22626 603 41 0 25474 0
vsize: 102060
[startup+409.999 s]
Raw data (loadavg): 1.02 1.02 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 23393 0 0 0 40929 64 0 0 25 0 1 0 543733906 106106880 23025 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25905 23025 603 41 0 25864 0
vsize: 103620
[startup+419.999 s]
Raw data (loadavg): 1.01 1.02 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 23780 0 0 0 41928 66 0 0 25 0 1 0 543733906 107704320 23412 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26295 23412 603 41 0 26254 0
vsize: 105180
[startup+429.999 s]
Raw data (loadavg): 1.01 1.02 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 24081 0 0 0 42927 67 0 0 25 0 1 0 543733906 108912640 23713 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26590 23713 603 41 0 26549 0
vsize: 106360
[startup+439.999 s]
Raw data (loadavg): 1.01 1.02 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 24343 0 0 0 43926 68 0 0 25 0 1 0 543733906 109854720 23975 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26820 23975 603 41 0 26779 0
vsize: 107280
[startup+449.999 s]
Raw data (loadavg): 1.01 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 24540 0 0 0 44926 69 0 0 25 0 1 0 543733906 110661632 24172 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27017 24172 603 41 0 26976 0
vsize: 108068
[startup+459.999 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 24765 0 0 0 45925 69 0 0 25 0 1 0 543733906 111603712 24397 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27247 24397 603 41 0 27206 0
vsize: 108988
[startup+470 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 24969 0 0 0 46925 70 0 0 25 0 1 0 543733906 112410624 24601 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27444 24601 603 41 0 27403 0
vsize: 109776
[startup+479.999 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 25217 0 0 0 47924 71 0 0 25 0 1 0 543733906 113479680 24849 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27705 24849 603 41 0 27664 0
vsize: 110820
[startup+489.998 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 25389 0 0 0 48924 71 0 0 25 0 1 0 543733906 114151424 25021 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27869 25021 603 41 0 27828 0
vsize: 111476
[startup+499.998 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 25581 0 0 0 49923 72 0 0 25 0 1 0 543733906 114958336 25213 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28066 25213 603 41 0 28025 0
vsize: 112264
[startup+509.998 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 25806 0 0 0 50923 73 0 0 25 0 1 0 543733906 116166656 25438 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28361 25438 603 41 0 28320 0
vsize: 113444
[startup+519.998 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 26048 0 0 0 51922 74 0 0 25 0 1 0 543733906 117108736 25680 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28591 25680 603 41 0 28550 0
vsize: 114364
[startup+529.998 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 26326 0 0 0 52921 75 0 0 25 0 1 0 543733906 118329344 25958 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28889 25958 603 41 0 28848 0
vsize: 115556
[startup+539.998 s]
Raw data (loadavg): 1.00 1.01 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 26649 0 0 0 53921 75 0 0 25 0 1 0 543733906 119566336 26281 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29191 26281 603 41 0 29150 0
vsize: 116764
[startup+549.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 26922 0 0 0 54921 75 0 0 25 0 1 0 543733906 120664064 26554 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29459 26554 603 41 0 29418 0
vsize: 117836
[startup+559.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 27214 0 0 0 55920 76 0 0 25 0 1 0 543733906 121876480 26846 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29755 26846 603 41 0 29714 0
vsize: 119020
[startup+569.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 27478 0 0 0 56919 77 0 0 25 0 1 0 543733906 122961920 27110 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30020 27110 603 41 0 29979 0
vsize: 120080
[startup+579.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 27754 0 0 0 57918 78 0 0 25 0 1 0 543733906 124030976 27386 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30281 27386 603 41 0 30240 0
vsize: 121124
[startup+589.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 28047 0 0 0 58918 79 0 0 25 0 1 0 543733906 125251584 27679 4294967295 134512640 134672761 3221224544 3221223648 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30579 27679 603 41 0 30538 0
vsize: 122316
[startup+599.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 28353 0 0 0 59917 79 0 0 25 0 1 0 543733906 126590976 27985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30906 27985 603 41 0 30865 0
vsize: 123624
[startup+609.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 28597 0 0 0 60916 81 0 0 25 0 1 0 543733906 127537152 28229 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31137 28229 603 41 0 31096 0
vsize: 124548
[startup+619.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 28911 0 0 0 61915 82 0 0 25 0 1 0 543733906 128868352 28543 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 28543 603 41 0 31421 0
vsize: 125848
[startup+629.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 29210 0 0 0 62915 83 0 0 25 0 1 0 543733906 130076672 28842 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31757 28842 603 41 0 31716 0
vsize: 127028
[startup+639.997 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 29504 0 0 0 63914 84 0 0 25 0 1 0 543733906 131284992 29136 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32052 29136 603 41 0 32011 0
vsize: 128208
[startup+649.997 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 29765 0 0 0 64913 85 0 0 25 0 1 0 543733906 132354048 29397 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32313 29397 603 41 0 32272 0
vsize: 129252
[startup+659.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 29996 0 0 0 65912 86 0 0 25 0 1 0 543733906 133300224 29628 4294967295 134512640 134672761 3221224544 3221223648 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32544 29628 603 41 0 32503 0
vsize: 130176
[startup+669.998 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 30222 0 0 0 66912 86 0 0 25 0 1 0 543733906 134246400 29854 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32775 29854 603 41 0 32734 0
vsize: 131100
[startup+679.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 30390 0 0 0 67912 87 0 0 25 0 1 0 543733906 134918144 30022 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32939 30022 603 41 0 32898 0
vsize: 131756
[startup+689.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25318
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 30642 0 0 0 68911 87 0 0 25 0 1 0 543733906 135864320 30274 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33170 30274 603 41 0 33129 0
vsize: 132680
[startup+699.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 30905 0 0 0 69911 88 0 0 25 0 1 0 543733906 136949760 30537 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33435 30537 603 41 0 33394 0
vsize: 133740
[startup+709.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 31099 0 0 0 70911 88 0 0 25 0 1 0 543733906 137760768 30731 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33633 30731 603 41 0 33592 0
vsize: 134532
[startup+720 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 31403 0 0 0 71910 89 0 0 25 0 1 0 543733906 138993664 31035 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33934 31035 603 41 0 33893 0
vsize: 135736
[startup+729.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 31699 0 0 0 72910 90 0 0 25 0 1 0 543733906 140197888 31331 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34228 31331 603 41 0 34187 0
vsize: 136912
[startup+739.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 32075 0 0 0 73909 91 0 0 25 0 1 0 543733906 141680640 31707 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34590 31707 603 41 0 34549 0
vsize: 138360
[startup+750 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 32301 0 0 0 74908 91 0 0 25 0 1 0 543733906 142626816 31933 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34821 31933 603 41 0 34780 0
vsize: 139284
[startup+760 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 32559 0 0 0 75907 92 0 0 25 0 1 0 543733906 143699968 32191 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35083 32191 603 41 0 35042 0
vsize: 140332
[startup+770.001 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 32808 0 0 0 76907 93 0 0 25 0 1 0 543733906 144773120 32440 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35345 32440 603 41 0 35304 0
vsize: 141380
[startup+780 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 33107 0 0 0 77906 94 0 0 25 0 1 0 543733906 145989632 32739 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35642 32739 603 41 0 35601 0
vsize: 142568
[startup+790 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 33400 0 0 0 78905 94 0 0 25 0 1 0 543733906 147206144 33032 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35939 33032 603 41 0 35898 0
vsize: 143756
[startup+800 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 33682 0 0 0 79905 95 0 0 25 0 1 0 543733906 148262912 33314 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36197 33314 603 41 0 36156 0
vsize: 144788
[startup+809.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 33993 0 0 0 80904 96 0 0 25 0 1 0 543733906 149594112 33625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36522 33625 603 41 0 36481 0
vsize: 146088
[startup+819.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 34276 0 0 0 81903 97 0 0 25 0 1 0 543733906 150654976 33908 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36781 33908 603 41 0 36740 0
vsize: 147124
[startup+829.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 34553 0 0 0 82902 98 0 0 25 0 1 0 543733906 151855104 34185 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37074 34185 603 41 0 37033 0
vsize: 148296
[startup+839.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 34806 0 0 0 83901 99 0 0 25 0 1 0 543733906 152936448 34438 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37338 34438 603 41 0 37297 0
vsize: 149352
[startup+849.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 35028 0 0 0 84901 100 0 0 25 0 1 0 543733906 153751552 34660 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37537 34660 603 41 0 37496 0
vsize: 150148
[startup+859.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 35242 0 0 0 85900 101 0 0 25 0 1 0 543733906 154677248 34874 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37763 34874 603 41 0 37722 0
vsize: 151052
[startup+870 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 35455 0 0 0 86900 102 0 0 25 0 1 0 543733906 155480064 35087 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37959 35087 603 41 0 37918 0
vsize: 151836
[startup+879.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 35685 0 0 0 87899 102 0 0 25 0 1 0 543733906 156413952 35317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38187 35317 603 41 0 38146 0
vsize: 152748
[startup+889.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 35930 0 0 0 88898 103 0 0 25 0 1 0 543733906 157495296 35562 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38451 35562 603 41 0 38410 0
vsize: 153804
[startup+900 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 36200 0 0 0 89898 104 0 0 25 0 1 0 543733906 158576640 35832 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38715 35832 603 41 0 38674 0
vsize: 154860
[startup+909.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 36480 0 0 0 90898 104 0 0 25 0 1 0 543733906 159780864 36112 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39009 36112 603 41 0 38968 0
vsize: 156036
[startup+919.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 36758 0 0 0 91897 105 0 0 25 0 1 0 543733906 160845824 36390 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39269 36390 603 41 0 39228 0
vsize: 157076
[startup+929.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 36894 0 0 0 92897 106 0 0 25 0 1 0 543733906 161386496 36526 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39401 36526 603 41 0 39360 0
vsize: 157604
[startup+939.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 37103 0 0 0 93896 106 0 0 25 0 1 0 543733906 162193408 36735 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39598 36735 603 41 0 39557 0
vsize: 158392
[startup+949.999 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 37403 0 0 0 94896 106 0 0 25 0 1 0 543733906 163532800 37035 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39925 37035 603 41 0 39884 0
vsize: 159700
[startup+960 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 37631 0 0 0 95896 107 0 0 25 0 1 0 543733906 164343808 37263 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40123 37263 603 41 0 40082 0
vsize: 160492
[startup+970 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 37957 0 0 0 96896 107 0 0 25 0 1 0 543733906 165691392 37589 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40452 37589 603 41 0 40411 0
vsize: 161808
[startup+980.001 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 38172 0 0 0 97896 108 0 0 25 0 1 0 543733906 166629376 37804 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40681 37804 603 41 0 40640 0
vsize: 162724
[startup+990 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25320
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 38477 0 0 0 98896 108 0 0 25 0 1 0 543733906 167849984 38109 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40979 38109 603 41 0 40938 0
vsize: 163916
[startup+1000 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 38757 0 0 0 99895 109 0 0 25 0 1 0 543733906 169070592 38389 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41277 38389 603 41 0 41236 0
vsize: 165108
[startup+1010 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 38969 0 0 0 100894 110 0 0 25 0 1 0 543733906 169877504 38601 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41474 38601 603 41 0 41433 0
vsize: 165896
[startup+1020 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 39213 0 0 0 101894 110 0 0 25 0 1 0 543733906 170823680 38845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41705 38845 603 41 0 41664 0
vsize: 166820
[startup+1030 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 39389 0 0 0 102893 111 0 0 25 0 1 0 543733906 171634688 39021 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41903 39021 603 41 0 41862 0
vsize: 167612
[startup+1040 s]
Raw data (loadavg): 1.00 1.00 0.96 2/55 25322
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 39566 0 0 0 103893 111 0 0 25 0 1 0 543733906 172302336 39198 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42066 39198 603 41 0 42025 0
vsize: 168264
[startup+1050 s]
Raw data (loadavg): 1.08 1.02 0.97 3/58 25336
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 39847 0 0 0 104893 112 0 0 25 0 1 0 543733906 173514752 39479 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42362 39479 603 41 0 42321 0
vsize: 169448
[startup+1060 s]
Raw data (loadavg): 1.14 1.03 0.97 2/55 25375
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 40066 0 0 0 105892 113 0 0 25 0 1 0 543733906 174325760 39698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42560 39698 603 41 0 42519 0
vsize: 170240
[startup+1070.01 s]
Raw data (loadavg): 1.12 1.03 0.97 2/55 25375
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 40392 0 0 0 106893 113 0 0 25 0 1 0 543733906 175681536 40024 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42891 40024 603 41 0 42850 0
vsize: 171564
[startup+1080.01 s]
Raw data (loadavg): 1.10 1.03 0.97 2/55 25375
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 40636 0 0 0 107892 114 0 0 25 0 1 0 543733906 176631808 40268 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43123 40268 603 41 0 43082 0
vsize: 172492
[startup+1090.01 s]
Raw data (loadavg): 1.08 1.03 0.97 2/55 25375
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 40940 0 0 0 108892 115 0 0 25 0 1 0 543733906 177979392 40572 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43452 40572 603 41 0 43411 0
vsize: 173808
[startup+1100.01 s]
Raw data (loadavg): 1.07 1.03 0.97 2/55 25375
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 41250 0 0 0 109891 116 0 0 25 0 1 0 543733906 179187712 40882 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43747 40882 603 41 0 43706 0
vsize: 174988
[startup+1110.01 s]
Raw data (loadavg): 1.06 1.03 0.97 2/55 25375
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 41597 0 0 0 110890 117 0 0 25 0 1 0 543733906 180666368 41229 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44108 41229 603 41 0 44067 0
vsize: 176432
[startup+1120.01 s]
Raw data (loadavg): 1.05 1.02 0.97 2/55 25375
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 41853 0 0 0 111890 117 0 0 25 0 1 0 543733906 181616640 41485 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44340 41485 603 41 0 44299 0
vsize: 177360
[startup+1130.01 s]
Raw data (loadavg): 1.04 1.02 0.97 2/55 25377
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 42190 0 0 0 112888 119 0 0 25 0 1 0 543733906 183099392 41822 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44702 41822 603 41 0 44661 0
vsize: 178808
[startup+1140.01 s]
Raw data (loadavg): 1.04 1.02 0.97 2/55 25377
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 42408 0 0 0 113887 121 0 0 25 0 1 0 543733906 183910400 42040 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44900 42040 603 41 0 44859 0
vsize: 179600
[startup+1150.01 s]
Raw data (loadavg): 1.03 1.02 0.97 2/55 25377
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 42717 0 0 0 114886 121 0 0 25 0 1 0 543733906 185249792 42349 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45227 42349 603 41 0 45186 0
vsize: 180908
[startup+1160.01 s]
Raw data (loadavg): 1.02 1.02 0.97 2/55 25377
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 43024 0 0 0 115885 122 0 0 25 0 1 0 543733906 186458112 42656 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45522 42656 603 41 0 45481 0
vsize: 182088
[startup+1170.01 s]
Raw data (loadavg): 1.02 1.02 0.97 2/55 25377
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 43371 0 0 0 116884 124 0 0 25 0 1 0 543733906 187940864 43003 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45884 43003 603 41 0 45843 0
vsize: 183536
[startup+1180.01 s]
Raw data (loadavg): 1.02 1.02 0.97 2/55 25377
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 43594 0 0 0 117884 124 0 0 25 0 1 0 543733906 188760064 43226 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46084 43226 603 41 0 46043 0
vsize: 184336
[startup+1190.01 s]
Raw data (loadavg): 1.01 1.02 0.97 2/55 25377
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 43831 0 0 0 118883 125 0 0 25 0 1 0 543733906 189693952 43463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46312 43463 603 41 0 46271 0
vsize: 185248
[startup+1200.01 s]
Raw data (loadavg): 1.01 1.02 0.97 2/55 25377
Raw data (stat): 25314 (minisat+) R 25313 20838 20837 0 -1 0 44086 0 0 0 119883 126 0 0 25 0 1 0 543733906 190775296 43718 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46576 43718 603 41 0 46535 0
vsize: 186304
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.01 1.02 0.97 1/55 25377
Raw data (stat): 25314 (minisat+) Z 25313 20838 20837 0 -1 12 44088 0 0 0 119883 134 0 0 25 0 1 0 543733906 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.1
CPU time (s): 1200.18
CPU user time (s): 1198.83
CPU system time (s): 1.3418
CPU usage (%): 100.007
Max. virtual memory (Kb): 186304
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####