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-air06.opb
MD5SUM	f85d0079133f298b06c25764b03ff228
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50233
Optimality of the best value was proved	NO
Number of terms in the objective function	8627
Biggest coefficient in the objective function	1859
Number of bits for the biggest coefficient in the objective function	11
Sum of the numbers in the objective function	4587852
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	1859
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	4587852
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	1182.3
Number of variables	8627
Total number of constraints	9452
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9452
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	461
Trace number 17113

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 09:43:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11679 boxname=wulflinc28 idbench=899 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  f85d0079133f298b06c25764b03ff228  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-air06.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-air06.opb
IDLAUNCH: 11679
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        588736 kB
Buffers:         27700 kB
Cached:         390532 kB
SwapCached:        104 kB
Active:         142176 kB
Inactive:       278444 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        588484 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19460 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 10:03:26 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 11679 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1628 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1626]---> BDD-cost:  103
c ---[1622]---> BDD-cost:   43
c ---[1618]---> BDD-cost:   59
c ---[1616]---> BDD-cost:   33
c ---[1614]---> BDD-cost:  109
c ---[1612]---> BDD-cost:  113
c ---[1610]---> BDD-cost:   79
c ---[1608]---> BDD-cost:    3
c ---[1604]---> BDD-cost:   41
c ---[1602]---> BDD-cost:   51
c ---[1600]---> BDD-cost:  147
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:   23
c ---[1594]---> BDD-cost:  135
c ---[1592]---> BDD-cost:   81
c ---[1590]---> BDD-cost:   41
c ---[1588]---> BDD-cost:   27
c ---[1586]---> BDD-cost:   25
c ---[1584]---> BDD-cost:    8
c ---[1582]---> BDD-cost:   71
c ---[1580]---> BDD-cost:  137
c ---[1578]---> BDD-cost:   25
c ---[1576]---> BDD-cost:   13
c ---[1574]---> BDD-cost:   27
c ---[1572]---> BDD-cost:    9
c ---[1570]---> BDD-cost:  131
c ---[1566]---> BDD-cost:   47
c ---[1564]---> BDD-cost:   41
c ---[1562]---> BDD-cost:   27
c ---[1560]---> BDD-cost:   35
c ---[1558]---> BDD-cost:  133
c ---[1556]---> BDD-cost:  303
c ---[1554]---> BDD-cost:  231
c ---[1552]---> BDD-cost:  175
c ---[1550]---> BDD-cost:  131
c ---[1548]---> BDD-cost:   89
c ---[1546]---> BDD-cost:   53
c ---[1544]---> BDD-cost:   65
c ---[1542]---> BDD-cost:  141
c ---[1540]---> BDD-cost:  129
c ---[1538]---> BDD-cost:   21
c ---[1536]---> BDD-cost:   13
c ---[1534]---> BDD-cost:   83
c ---[1532]---> BDD-cost:   63
c ---[1530]---> BDD-cost:    7
c ---[1528]---> BDD-cost:    9
c ---[1526]---> BDD-cost:    7
c ---[1524]---> BDD-cost:   41
c ---[1522]---> BDD-cost:   93
c ---[1520]---> BDD-cost:   55
c ---[1518]---> BDD-cost:   27
c ---[1516]---> BDD-cost:  253
c ---[1514]---> BDD-cost:  189
c ---[1512]---> BDD-cost:  131
c ---[1510]---> BDD-cost:  143
c ---[1508]---> BDD-cost:   55
c ---[1506]---> BDD-cost:  105
c ---[1504]---> BDD-cost:  357
c ---[1502]---> BDD-cost:  355
c ---[1500]---> BDD-cost:  361
c ---[1498]---> BDD-cost:  257
c ---[1496]---> BDD-cost:  263
c ---[1494]---> BDD-cost:  271
c ---[1492]---> BDD-cost:   91
c ---[1488]---> BDD-cost:   15
c ---[1486]---> BDD-cost:    7
c ---[1484]---> BDD-cost:   37
c ---[1478]---> BDD-cost:    1
c ---[1476]---> BDD-cost:   14
c ---[1474]---> BDD-cost:    7
c ---[1472]---> BDD-cost:    1
c ---[1470]---> BDD-cost:    1
c ---[1468]---> BDD-cost:    5
c ---[1466]---> BDD-cost:  103
c ---[1464]---> BDD-cost:  203
c ---[1462]---> BDD-cost:   91
c ---[1460]---> BDD-cost:   49
c ---[1458]---> BDD-cost:    7
c ---[1456]---> BDD-cost:   77
c ---[1452]---> BDD-cost:   55
c ---[1450]---> BDD-cost:   19
c ---[1448]---> BDD-cost:   95
c ---[1446]---> BDD-cost:  101
c ---[1444]---> BDD-cost:  115
c ---[1442]---> BDD-cost:   67
c ---[1440]---> BDD-cost:   33
c ---[1438]---> BDD-cost:   29
c ---[1436]---> BDD-cost:   91
c ---[1434]---> BDD-cost:   25
c ---[1428]---> BDD-cost:   11
c ---[1426]---> BDD-cost:   15
c ---[1424]---> BDD-cost:   29
c ---[1422]---> BDD-cost:  127
c ---[1420]---> BDD-cost:  195
c ---[1418]---> BDD-cost:  143
c ---[1416]---> BDD-cost:  111
c ---[1414]---> BDD-cost:  169
c ---[1412]---> BDD-cost:  169
c ---[1410]---> BDD-cost:  171
c ---[1408]---> BDD-cost:  135
c ---[1406]---> BDD-cost:   43
c ---[1404]---> BDD-cost:  257
c ---[1402]---> BDD-cost:  261
c ---[1400]---> BDD-cost:  167
c ---[1398]---> BDD-cost:  125
c ---[1396]---> BDD-cost:  125
c ---[1394]---> BDD-cost:   39
c ---[1392]---> BDD-cost:   37
c ---[1390]---> BDD-cost:   43
c ---[1386]---> BDD-cost:   29
c ---[1384]---> BDD-cost:   33
c ---[1382]---> BDD-cost:  107
c ---[1380]---> BDD-cost:   57
c ---[1378]---> BDD-cost:  169
c ---[1376]---> BDD-cost:   79
c ---[1374]---> BDD-cost:   81
c ---[1372]---> BDD-cost:  219
c ---[1370]---> BDD-cost:  229
c ---[1368]---> BDD-cost:  111
c ---[1366]---> BDD-cost:    5
c ---[1364]---> BDD-cost:   89
c ---[1362]---> BDD-cost:  389
c ---[1360]---> BDD-cost:  335
c ---[1358]---> BDD-cost:  191
c ---[1356]---> BDD-cost:  121
c ---[1354]---> BDD-cost:  137
c ---[1352]---> BDD-cost:   83
c ---[1350]---> BDD-cost:  199
c ---[1348]---> BDD-cost:   15
c ---[1346]---> BDD-cost:  109
c ---[1344]---> BDD-cost:   55
c ---[1342]---> BDD-cost:  181
c ---[1340]---> BDD-cost:  133
c ---[1338]---> BDD-cost:   81
c ---[1336]---> BDD-cost:   33
c ---[1334]---> BDD-cost:  131
c ---[1332]---> BDD-cost:   75
c ---[1330]---> BDD-cost:   49
c ---[1328]---> BDD-cost:   17
c ---[1326]---> BDD-cost:   97
c ---[1324]---> BDD-cost:  129
c ---[1322]---> BDD-cost:   69
c ---[1320]---> BDD-cost:  273
c ---[1318]---> BDD-cost:  261
c ---[1316]---> BDD-cost:   89
c ---[1314]---> BDD-cost:  119
c ---[1312]---> BDD-cost:   53
c ---[1310]---> BDD-cost:   43
c ---[1308]---> BDD-cost:   61
c ---[1306]---> BDD-cost:   99
c ---[1304]---> BDD-cost:   81
c ---[1302]---> BDD-cost:  165
c ---[1300]---> BDD-cost:  231
c ---[1298]---> BDD-cost:  121
c ---[1296]---> BDD-cost:  135
c ---[1294]---> BDD-cost:  227
c ---[1292]---> BDD-cost:   35
c ---[1290]---> BDD-cost:   55
c ---[1288]---> BDD-cost:  143
c ---[1286]---> BDD-cost:  135
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  177
c ---[1280]---> BDD-cost:  151
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  179
c ---[1274]---> BDD-cost:   61
c ---[1272]---> BDD-cost:  167
c ---[1270]---> BDD-cost:  145
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:  243
c ---[1264]---> BDD-cost:   15
c ---[1262]---> BDD-cost:  137
c ---[1260]---> BDD-cost:   85
c ---[1258]---> BDD-cost:   37
c ---[1254]---> BDD-cost:   43
c ---[1252]---> BDD-cost:   19
c ---[1250]---> BDD-cost:   23
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   91
c ---[1244]---> BDD-cost:   95
c ---[1242]---> BDD-cost:   61
c ---[1240]---> BDD-cost:   79
c ---[1238]---> BDD-cost:   89
c ---[1236]---> BDD-cost:  105
c ---[1234]---> BDD-cost:   97
c ---[1232]---> BDD-cost:  105
c ---[1230]---> BDD-cost:   81
c ---[1228]---> BDD-cost:   19
c ---[1226]---> BDD-cost:   13
c ---[1224]---> BDD-cost:    3
c ---[1222]---> BDD-cost:   21
c ---[1220]---> BDD-cost:   65
c ---[1218]---> BDD-cost:   35
c ---[1216]---> BDD-cost:   69
c ---[1214]---> BDD-cost:   45
c ---[1212]---> BDD-cost:   59
c ---[1210]---> BDD-cost:   89
c ---[1208]---> BDD-cost:   65
c ---[1206]---> BDD-cost:  101
c ---[1204]---> BDD-cost:   87
c ---[1202]---> BDD-cost:   95
c ---[1200]---> BDD-cost:   69
c ---[1198]---> BDD-cost:  119
c ---[1196]---> BDD-cost:   53
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   27
c ---[1190]---> BDD-cost:  273
c ---[1188]---> BDD-cost:  231
c ---[1186]---> BDD-cost:  243
c ---[1184]---> BDD-cost:  121
c ---[1182]---> BDD-cost:  295
c ---[1180]---> BDD-cost:  175
c ---[1178]---> BDD-cost:  115
c ---[1176]---> BDD-cost:  175
c ---[1174]---> BDD-cost:  249
c ---[1172]---> BDD-cost:  233
c ---[1170]---> BDD-cost:  123
c ---[1168]---> BDD-cost:   81
c ---[1166]---> BDD-cost:    5
c ---[1164]---> BDD-cost:   75
c ---[1162]---> BDD-cost:   71
c ---[1160]---> BDD-cost:   39
c ---[1156]---> BDD-cost:   65
c ---[1154]---> BDD-cost:   51
c ---[1152]---> BDD-cost:   21
c ---[1150]---> BDD-cost:   15
c ---[1148]---> BDD-cost:    3
c ---[1146]---> BDD-cost:   21
c ---[1144]---> BDD-cost:   17
c ---[1142]---> BDD-cost:   33
c ---[1140]---> BDD-cost:   11
c ---[1138]---> BDD-cost:   29
c ---[1136]---> BDD-cost:   95
c ---[1134]---> BDD-cost:   79
c ---[1132]---> BDD-cost:   37
c ---[1130]---> BDD-cost:  273
c ---[1128]---> BDD-cost:  221
c ---[1126]---> BDD-cost:  189
c ---[1124]---> BDD-cost:   81
c ---[1122]---> BDD-cost:   35
c ---[1120]---> BDD-cost:  185
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   59
c ---[1114]---> BDD-cost:   59
c ---[1112]---> BDD-cost:  125
c ---[1110]---> BDD-cost:  135
c ---[1108]---> BDD-cost:  117
c ---[1096]---> BDD-cost:   73
c ---[1094]---> BDD-cost:   95
c ---[1092]---> BDD-cost:   53
c ---[1090]---> BDD-cost:  117
c ---[1088]---> BDD-cost:  117
c ---[1086]---> BDD-cost:  199
c ---[1084]---> BDD-cost:  189
c ---[1082]---> BDD-cost:   25
c ---[1080]---> BDD-cost:  173
c ---[1078]---> BDD-cost:   45
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:  219
c ---[1070]---> BDD-cost:  167
c ---[1068]---> BDD-cost:  121
c ---[1066]---> BDD-cost:  203
c ---[1064]---> BDD-cost:   27
c ---[1062]---> BDD-cost:   17
c ---[1060]---> BDD-cost:   87
c ---[1058]---> BDD-cost:  111
c ---[1056]---> BDD-cost:  169
c ---[1054]---> BDD-cost:  251
c ---[1052]---> BDD-cost:  155
c ---[1048]---> BDD-cost:   93
c ---[1044]---> BDD-cost:  141
c ---[1042]---> BDD-cost:  103
c ---[1040]---> BDD-cost:  173
c ---[1038]---> BDD-cost:  221
c ---[1036]---> BDD-cost:  199
c ---[1034]---> BDD-cost:  185
c ---[1032]---> BDD-cost:  259
c ---[1030]---> BDD-cost:  129
c ---[1028]---> BDD-cost:  283
c ---[1026]---> BDD-cost:  187
c ---[1024]---> BDD-cost:  187
c ---[1022]---> BDD-cost:  173
c ---[1018]---> BDD-cost:   55
c ---[1014]---> BDD-cost:   37
c ---[1012]---> BDD-cost:   59
c ---[1010]---> BDD-cost:   57
c ---[1008]---> BDD-cost:   49
c ---[1004]---> BDD-cost:    1
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   91
c ---[ 998]---> BDD-cost:  137
c ---[ 996]---> BDD-cost:   77
c ---[ 994]---> BDD-cost:  125
c ---[ 992]---> BDD-cost:   49
c ---[ 990]---> BDD-cost:  103
c ---[ 988]---> BDD-cost:  119
c ---[ 986]---> BDD-cost:   81
c ---[ 984]---> BDD-cost:  121
c ---[ 982]---> BDD-cost:  127
c ---[ 980]---> BDD-cost:   25
c ---[ 978]---> BDD-cost:  139
c ---[ 976]---> BDD-cost:   73
c ---[ 974]---> BDD-cost:  113
c ---[ 972]---> BDD-cost:   77
c ---[ 970]---> BDD-cost:   69
c ---[ 968]---> BDD-cost:   53
c ---[ 966]---> BDD-cost:   33
c ---[ 962]---> BDD-cost:   65
c ---[ 960]---> BDD-cost:   65
c ---[ 958]---> BDD-cost:  213
c ---[ 956]---> BDD-cost:  247
c ---[ 954]---> BDD-cost:  273
c ---[ 952]---> BDD-cost:  145
c ---[ 950]---> BDD-cost:  535
c ---[ 948]---> BDD-cost:  659
c ---[ 946]---> BDD-cost:  259
c ---[ 944]---> BDD-cost:  213
c ---[ 942]---> BDD-cost:  157
c ---[ 940]---> BDD-cost:   65
c ---[ 938]---> BDD-cost:  561
c ---[ 936]---> BDD-cost:  117
c ---[ 932]---> BDD-cost:  153
c ---[ 930]---> BDD-cost:  113
c ---[ 928]---> BDD-cost:  119
c ---[ 926]---> BDD-cost:   99
c ---[ 922]---> BDD-cost:    6
c ---[ 920]---> BDD-cost:  113
c ---[ 918]---> BDD-cost:   75
c ---[ 914]---> BDD-cost:   17
c ---[ 912]---> BDD-cost:  149
c ---[ 910]---> BDD-cost:   63
c ---[ 908]---> BDD-cost:   41
c ---[ 906]---> BDD-cost:  135
c ---[ 904]---> BDD-cost:   99
c ---[ 902]---> BDD-cost:   99
c ---[ 900]---> BDD-cost:   65
c ---[ 898]---> BDD-cost:  333
c ---[ 896]---> BDD-cost:   93
c ---[ 894]---> BDD-cost:  407
c ---[ 892]---> BDD-cost:  393
c ---[ 890]---> BDD-cost:  349
c ---[ 888]---> BDD-cost:  189
c ---[ 886]---> BDD-cost:  225
c ---[ 884]---> BDD-cost:  115
c ---[ 882]---> BDD-cost:  117
c ---[ 880]---> BDD-cost:   57
c ---[ 878]---> BDD-cost:  109
c ---[ 876]---> BDD-cost:  219
c ---[ 874]---> BDD-cost:  139
c ---[ 872]---> BDD-cost:  239
c ---[ 870]---> BDD-cost:   65
c ---[ 868]---> BDD-cost:   39
c ---[ 866]---> BDD-cost:   59
c ---[ 862]---> BDD-cost:    9
c ---[ 860]---> BDD-cost:  239
c ---[ 858]---> BDD-cost:  165
c ---[ 856]---> BDD-cost:  207
c ---[ 854]---> BDD-cost:  219
c ---[ 852]---> BDD-cost:  391
c ---[ 850]---> BDD-cost:  315
c ---[ 848]---> BDD-cost:  147
c ---[ 846]---> BDD-cost:    7
c ---[ 844]---> BDD-cost:  187
c ---[ 842]---> BDD-cost:  311
c ---[ 840]---> BDD-cost:  187
c ---[ 838]---> BDD-cost:  195
c ---[ 836]---> BDD-cost:  117
c ---[ 834]---> BDD-cost:  111
c ---[ 830]---> BDD-cost:   91
c ---[ 828]---> BDD-cost:  333
c ---[ 826]---> BDD-cost:  207
c ---[ 822]---> BDD-cost:  253
c ---[ 820]---> BDD-cost:   77
c ---[ 818]---> BDD-cost:   77
c ---[ 816]---> BDD-cost:  191
c ---[ 814]---> BDD-cost:  153
c ---[ 812]---> BDD-cost:  255
c ---[ 810]---> BDD-cost:  189
c ---[ 808]---> BDD-cost:   17
c ---[ 806]---> BDD-cost:   39
c ---[ 802]---> BDD-cost:  187
c ---[ 800]---> BDD-cost:  117
c ---[ 798]---> BDD-cost:   49
c ---[ 796]---> BDD-cost:   37
c ---[ 794]---> BDD-cost:   61
c ---[ 792]---> BDD-cost:   33
c ---[ 790]---> BDD-cost:    0
c ---[ 788]---> BDD-cost:   83
c ---[ 786]---> BDD-cost:   73
c ---[ 784]---> BDD-cost:   91
c ---[ 782]---> BDD-cost:   55
c ---[ 780]---> BDD-cost:  105
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  345
c ---[ 774]---> BDD-cost:  295
c ---[ 772]---> BDD-cost:  101
c ---[ 770]---> BDD-cost:   21
c ---[ 768]---> BDD-cost:   71
c ---[ 766]---> BDD-cost:   77
c ---[ 764]---> BDD-cost:   61
c ---[ 762]---> BDD-cost:   53
c ---[ 760]---> BDD-cost:  199
c ---[ 758]---> BDD-cost:  195
c ---[ 756]---> BDD-cost:  155
c ---[ 754]---> BDD-cost:   29
c ---[ 752]---> BDD-cost:   13
c ---[ 750]---> BDD-cost:  133
c ---[ 748]---> BDD-cost:   65
c ---[ 746]---> BDD-cost:   57
c ---[ 744]---> BDD-cost:  157
c ---[ 742]---> BDD-cost:  345
c ---[ 740]---> BDD-cost:  201
c ---[ 738]---> BDD-cost:  205
c ---[ 736]---> BDD-cost:  151
c ---[ 734]---> BDD-cost:  135
c ---[ 732]---> BDD-cost:   73
c ---[ 730]---> BDD-cost:  161
c ---[ 728]---> BDD-cost:  181
c ---[ 726]---> BDD-cost:  177
c ---[ 724]---> BDD-cost:  293
c ---[ 722]---> BDD-cost:  279
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  145
c ---[ 716]---> BDD-cost:  289
c ---[ 714]---> BDD-cost:  163
c ---[ 712]---> BDD-cost:  181
c ---[ 710]---> BDD-cost:  141
c ---[ 708]---> BDD-cost:  115
c ---[ 706]---> BDD-cost:  123
c ---[ 704]---> BDD-cost:  189
c ---[ 702]---> BDD-cost:  139
c ---[ 700]---> BDD-cost:   63
c ---[ 698]---> BDD-cost:  473
c ---[ 696]---> BDD-cost:  429
c ---[ 694]---> BDD-cost:  285
c ---[ 692]---> BDD-cost:    9
c ---[ 690]---> BDD-cost:    5
c ---[ 688]---> BDD-cost:    0
c ---[ 686]---> BDD-cost:    3
c ---[ 684]---> BDD-cost:    4
c ---[ 680]---> BDD-cost:  155
c ---[ 678]---> BDD-cost:  127
c ---[ 676]---> BDD-cost:  109
c ---[ 674]---> BDD-cost:  273
c ---[ 672]---> BDD-cost:   63
c ---[ 670]---> BDD-cost:   45
c ---[ 668]---> BDD-cost:   23
c ---[ 666]---> BDD-cost:   29
c ---[ 664]---> BDD-cost:  245
c ---[ 662]---> BDD-cost:  227
c ---[ 660]---> BDD-cost:   49
c ---[ 658]---> BDD-cost:    9
c ---[ 656]---> BDD-cost:    0
c ---[ 654]---> BDD-cost:  149
c ---[ 652]---> BDD-cost:  183
c ---[ 650]---> BDD-cost:  119
c ---[ 648]---> BDD-cost:  107
c ---[ 646]---> BDD-cost:  235
c ---[ 644]---> BDD-cost:  227
c ---[ 642]---> BDD-cost:  239
c ---[ 640]---> BDD-cost:  269
c ---[ 638]---> BDD-cost:  615
c ---[ 636]---> BDD-cost:  441
c ---[ 634]---> BDD-cost:  231
c ---[ 632]---> BDD-cost:  123
c ---[ 630]---> BDD-cost:  547
c ---[ 628]---> BDD-cost:  543
c ---[ 626]---> BDD-cost:  357
c ---[ 624]---> BDD-cost:  237
c ---[ 620]---> BDD-cost:  327
c ---[ 618]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:  287
c ---[ 614]---> BDD-cost:  205
c ---[ 612]---> BDD-cost:  177
c ---[ 610]---> BDD-cost:  313
c ---[ 608]---> BDD-cost:   57
c ---[ 606]---> BDD-cost:   61
c ---[ 604]---> BDD-cost:   45
c ---[ 602]---> BDD-cost:   35
c ---[ 600]---> BDD-cost:  133
c ---[ 598]---> BDD-cost:  107
c ---[ 596]---> BDD-cost:   91
c ---[ 594]---> BDD-cost:   93
c ---[ 592]---> BDD-cost:   35
c ---[ 590]---> BDD-cost:  187
c ---[ 588]---> BDD-cost:  573
c ---[ 586]---> BDD-cost:  305
c ---[ 584]---> BDD-cost:  607
c ---[ 582]---> BDD-cost:  443
c ---[ 580]---> BDD-cost:  213
c ---[ 578]---> BDD-cost:  213
c ---[ 576]---> BDD-cost:  167
c ---[ 574]---> BDD-cost:    4
c ---[ 572]---> BDD-cost:  283
c ---[ 570]---> BDD-cost:  277
c ---[ 568]---> BDD-cost:  125
c ---[ 566]---> BDD-cost:   85
c ---[ 564]---> BDD-cost:   81
c ---[ 562]---> BDD-cost:  403
c ---[ 560]---> BDD-cost:  391
c ---[ 558]---> BDD-cost:  175
c ---[ 556]---> BDD-cost:  159
c ---[ 554]---> BDD-cost:  155
c ---[ 552]---> BDD-cost:  101
c ---[ 550]---> BDD-cost:  155
c ---[ 548]---> BDD-cost:  165
c ---[ 546]---> BDD-cost:  153
c ---[ 544]---> BDD-cost:  135
c ---[ 542]---> BDD-cost:   81
c ---[ 540]---> BDD-cost:  167
c ---[ 538]---> BDD-cost:   27
c ---[ 536]---> BDD-cost:  147
c ---[ 534]---> BDD-cost:  155
c ---[ 532]---> BDD-cost:  173
c ---[ 530]---> BDD-cost:  267
c ---[ 528]---> BDD-cost:  157
c ---[ 526]---> BDD-cost:   91
c ---[ 524]---> BDD-cost:  259
c ---[ 522]---> BDD-cost:  117
c ---[ 520]---> BDD-cost:  121
c ---[ 518]---> BDD-cost:  323
c ---[ 516]---> BDD-cost:  325
c ---[ 514]---> BDD-cost:  311
c ---[ 512]---> BDD-cost:  313
c ---[ 510]---> BDD-cost:  247
c ---[ 508]---> BDD-cost:  297
c ---[ 506]---> BDD-cost:  211
c ---[ 504]---> BDD-cost:  369
c ---[ 500]---> BDD-cost:  305
c ---[ 498]---> BDD-cost:  341
c ---[ 496]---> BDD-cost:  285
c ---[ 494]---> BDD-cost:   77
c ---[ 492]---> BDD-cost:  317
c ---[ 490]---> BDD-cost:  275
c ---[ 488]---> BDD-cost:  423
c ---[ 486]---> BDD-cost:  403
c ---[ 484]---> BDD-cost:  307
c ---[ 482]---> BDD-cost:  327
c ---[ 480]---> BDD-cost:  307
c ---[ 478]---> BDD-cost:  315
c ---[ 476]---> BDD-cost:  297
c ---[ 474]---> BDD-cost:  273
c ---[ 472]---> BDD-cost:  701
c ---[ 470]---> BDD-cost:  289
c ---[ 468]---> BDD-cost:  245
c ---[ 466]---> BDD-cost:  385
c ---[ 464]---> BDD-cost:  363
c ---[ 462]---> BDD-cost:   27
c ---[ 458]---> BDD-cost:  145
c ---[ 456]---> BDD-cost:  147
c ---[ 454]---> BDD-cost:  149
c ---[ 452]---> BDD-cost:  125
c ---[ 450]---> BDD-cost:  147
c ---[ 448]---> BDD-cost:  111
c ---[ 446]---> BDD-cost:  319
c ---[ 444]---> BDD-cost:  309
c ---[ 438]---> BDD-cost:   19
c ---[ 436]---> BDD-cost:    7
c ---[ 434]---> BDD-cost:  399
c ---[ 432]---> BDD-cost:  401
c ---[ 430]---> BDD-cost:  371
c ---[ 426]---> BDD-cost:   65
c ---[ 422]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:   15
c ---[ 416]---> BDD-cost:  453
c ---[ 414]---> BDD-cost:  457
c ---[ 412]---> BDD-cost:  197
c ---[ 410]---> BDD-cost:  123
c ---[ 408]---> BDD-cost:  165
c ---[ 404]---> BDD-cost:  335
c ---[ 402]---> BDD-cost:  169
c ---[ 400]---> BDD-cost:  209
c ---[ 398]---> BDD-cost:   61
c ---[ 396]---> BDD-cost:   17
c ---[ 394]---> BDD-cost:    7
c ---[ 392]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:   41
c ---[ 388]---> BDD-cost:  229
c ---[ 386]---> BDD-cost:  231
c ---[ 384]---> BDD-cost:  223
c ---[ 378]---> BDD-cost:  319
c ---[ 376]---> BDD-cost:  223
c ---[ 374]---> BDD-cost:  241
c ---[ 372]---> BDD-cost:  245
c ---[ 370]---> BDD-cost:  229
c ---[ 368]---> BDD-cost:  109
c ---[ 366]---> BDD-cost:   73
c ---[ 364]---> BDD-cost:   85
c ---[ 362]---> BDD-cost:   99
c ---[ 360]---> BDD-cost:  103
c ---[ 358]---> BDD-cost:    5
c ---[ 356]---> BDD-cost:  201
c ---[ 354]---> BDD-cost:  215
c ---[ 352]---> BDD-cost:  197
c ---[ 348]---> BDD-cost:  139
c ---[ 344]---> BDD-cost:   83
c ---[ 340]---> BDD-cost:  125
c ---[ 338]---> BDD-cost:  225
c ---[ 336]---> BDD-cost:  181
c ---[ 334]---> BDD-cost:  151
c ---[ 332]---> BDD-cost:  243
c ---[ 330]---> BDD-cost:  179
c ---[ 328]---> BDD-cost:  207
c ---[ 326]---> BDD-cost:  145
c ---[ 324]---> BDD-cost:   21
c ---[ 322]---> BDD-cost:  235
c ---[ 320]---> BDD-cost:  209
c ---[ 318]---> BDD-cost:   55
c ---[ 316]---> BDD-cost:  223
c ---[ 314]---> BDD-cost:  193
c ---[ 312]---> BDD-cost:  173
c ---[ 310]---> BDD-cost:   63
c ---[ 308]---> BDD-cost:   87
c ---[ 306]---> BDD-cost:   87
c ---[ 304]---> BDD-cost:   33
c ---[ 302]---> BDD-cost:  135
c ---[ 300]---> BDD-cost:   75
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  233
c ---[ 294]---> BDD-cost:  211
c ---[ 292]---> BDD-cost:  119
c ---[ 290]---> BDD-cost:  269
c ---[ 288]---> BDD-cost:   51
c ---[ 286]---> BDD-cost:  205
c ---[ 284]---> BDD-cost:  233
c ---[ 282]---> BDD-cost:  207
c ---[ 280]---> BDD-cost:  243
c ---[ 278]---> BDD-cost:  453
c ---[ 276]---> BDD-cost:  465
c ---[ 274]---> BDD-cost:  259
c ---[ 272]---> BDD-cost:  227
c ---[ 270]---> BDD-cost:  359
c ---[ 268]---> BDD-cost:  209
c ---[ 266]---> BDD-cost:  319
c ---[ 264]---> BDD-cost:  287
c ---[ 262]---> BDD-cost:  225
c ---[ 260]---> BDD-cost:  227
c ---[ 258]---> BDD-cost:  445
c ---[ 256]---> BDD-cost:  339
c ---[ 254]---> BDD-cost:  343
c ---[ 252]---> BDD-cost:  105
c ---[ 250]---> BDD-cost:   73
c ---[ 248]---> BDD-cost:   89
c ---[ 246]---> BDD-cost:  109
c ---[ 242]---> BDD-cost:  597
c ---[ 240]---> BDD-cost:  303
c ---[ 238]---> BDD-cost:  253
c ---[ 236]---> BDD-cost:  133
c ---[ 234]---> BDD-cost:  119
c ---[ 232]---> BDD-cost:   99
c ---[ 230]---> BDD-cost:  119
c ---[ 228]---> BDD-cost:   67
c ---[ 226]---> BDD-cost:  145
c ---[ 224]---> BDD-cost:  135
c ---[ 222]---> BDD-cost:  217
c ---[ 220]---> BDD-cost:  211
c ---[ 218]---> BDD-cost:  141
c ---[ 214]---> BDD-cost:  167
c ---[ 212]---> BDD-cost:  191
c ---[ 210]---> BDD-cost:  125
c ---[ 208]---> BDD-cost:  175
c ---[ 206]---> BDD-cost:  147
c ---[ 204]---> BDD-cost:   43
c ---[ 202]---> BDD-cost:  389
c ---[ 200]---> BDD-cost:  349
c ---[ 198]---> BDD-cost:  151
c ---[ 196]---> BDD-cost:  151
c ---[ 194]---> BDD-cost:  307
c ---[ 192]---> BDD-cost:  355
c ---[ 190]---> BDD-cost:  269
c ---[ 188]---> BDD-cost:  267
c ---[ 186]---> BDD-cost:  327
c ---[ 184]---> BDD-cost:  347
c ---[ 182]---> BDD-cost:  187
c ---[ 180]---> BDD-cost:  117
c ---[ 178]---> BDD-cost:   37
c ---[ 176]---> BDD-cost:   17
c ---[ 174]---> BDD-cost:  171
c ---[ 170]---> BDD-cost:  339
c ---[ 168]---> BDD-cost:  429
c ---[ 166]---> BDD-cost:  443
c ---[ 164]---> BDD-cost:  419
c ---[ 162]---> BDD-cost:  465
c ---[ 160]---> BDD-cost:  379
c ---[ 158]---> BDD-cost:  307
c ---[ 156]---> BDD-cost:  907
c ---[ 154]---> BDD-cost:  439
c ---[ 152]---> BDD-cost:  303
c ---[ 150]---> BDD-cost:  239
c ---[ 148]---> BDD-cost:  219
c ---[ 146]---> BDD-cost:  261
c ---[ 144]---> BDD-cost:  247
c ---[ 142]---> BDD-cost:  265
c ---[ 140]---> BDD-cost:  273
c ---[ 138]---> BDD-cost:  673
c ---[ 136]---> BDD-cost:  433
c ---[ 134]---> BDD-cost:  317
c ---[ 132]---> BDD-cost:  187
c ---[ 130]---> BDD-cost:  199
c ---[ 128]---> BDD-cost:  155
c ---[ 126]---> BDD-cost:  105
c ---[ 124]---> BDD-cost:   31
c ---[ 122]---> BDD-cost:  117
c ---[ 120]---> BDD-cost:  107
c ---[ 118]---> BDD-cost:  141
c ---[ 116]---> BDD-cost:  165
c ---[ 114]---> BDD-cost:  221
c ---[ 110]---> BDD-cost:  163
c ---[ 108]---> BDD-cost:  179
c ---[ 106]---> BDD-cost:  139
c ---[ 104]---> BDD-cost:   83
c ---[ 102]---> BDD-cost:   67
c ---[ 100]---> BDD-cost:   87
c ---[  98]---> BDD-cost:   31
c ---[  96]---> BDD-cost:   23
c ---[  94]---> BDD-cost:   31
c ---[  92]---> BDD-cost:   91
c ---[  90]---> BDD-cost:  431
c ---[  88]---> BDD-cost:  203
c ---[  86]---> BDD-cost:  565
c ---[  84]---> BDD-cost:  611
c ---[  82]---> BDD-cost:  347
c ---[  80]---> BDD-cost:  175
c ---[  78]---> BDD-cost:  525
c ---[  76]---> BDD-cost:  505
c ---[  74]---> BDD-cost:   57
c ---[  72]---> BDD-cost:   45
c ---[  70]---> BDD-cost:   57
c ---[  68]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   55
c ---[  64]---> BDD-cost:   57
c ---[  62]---> BDD-cost:   57
c ---[  60]---> BDD-cost:  159
c ---[  58]---> BDD-cost:   71
c ---[  56]---> BDD-cost:  199
c ---[  54]---> BDD-cost:  191
c ---[  52]---> BDD-cost:  225
c ---[  50]---> BDD-cost:  209
c ---[  48]---> BDD-cost:  509
c ---[  46]---> BDD-cost:  321
c ---[  44]---> BDD-cost:  333
c ---[  42]---> BDD-cost:  407
c ---[  40]---> BDD-cost:  191
c ---[  38]---> BDD-cost:  135
c ---[  36]---> BDD-cost:  379
c ---[  34]---> BDD-cost:  365
c ---[  32]---> BDD-cost:   63
c ---[  30]---> BDD-cost:   31
c ---[  28]---> BDD-cost:   33
c ---[  26]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   15
c ---[  22]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   31
c ---[  18]---> BDD-cost:   47
c ---[  16]---> BDD-cost:  139
c ---[  14]---> BDD-cost:    9
c ---[  12]---> BDD-cost:  135
c ---[  10]---> BDD-cost:   99
c ---[   8]---> BDD-cost:   53
c ---[   6]---> BDD-cost:  129
c ---[   4]---> BDD-cost:    7
c ---[   2]---> BDD-cost:  119
c ---[   0]---> BDD-cost:   85
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  297923   775365 |   99307       0        0     nan |  0.000 % |
c |       101 |  297806   775070 |  109237     100     2794    27.9 |  0.656 % |
c |       251 |  297804   775064 |  120161     248    14520    58.5 |  0.657 % |
c |       476 |  297507   774267 |  132177     467    22948    49.1 |  0.710 % |
c |       813 |  297152   773365 |  145395     797    35416    44.4 |  0.754 % |
c |      1319 |  296676   772113 |  159934    1277    64842    50.8 |  0.837 % |
c |      2078 |  296505   771647 |  175928    2025   118379    58.5 |  0.874 % |
c |      3217 |  296041   770425 |  193521    3109   207452    66.7 |  0.949 % |
c |      4927 |  295699   769540 |  212873    4779   350269    73.3 |  0.998 % |
c |      7492 |  295396   768750 |  234160    7275   566032    77.8 |  1.037 % |
c |     11337 |  294904   767451 |  257576   10971   954090    87.0 |  1.105 % |
c |     17103 |  294446   766278 |  283334   16577  1527497    92.1 |  1.145 % |
c |     25754 |  293444   763687 |  311667   24858  2532372   101.9 |  1.262 % |
c |     38729 |  292783   762005 |  342834   37493  4503970   120.1 |  1.316 % |
c |     58190 |  291850   759627 |  377118   56625  8594924   151.8 |  1.423 % |
c |     87385 |  291219   758027 |  414829   85473 17541788   205.2 |  1.468 % |
#### 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.60 0.86 0.88 2/54 23793
Raw data (stat): 23793 (runsolver) R 23792 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544095477 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.66 0.87 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 10676 0 0 0 972 27 0 0 25 0 1 0 544095477 45465600 10321 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11100 10321 603 41 0 11059 0
vsize: 44400
[startup+20.002 s]
Raw data (loadavg): 0.71 0.87 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 10826 0 0 0 1972 27 0 0 25 0 1 0 544095477 46137344 10471 4294967295 134512640 134672761 3221224624 3221223824 134557967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11264 10471 603 41 0 11223 0
vsize: 45056
[startup+30.0019 s]
Raw data (loadavg): 0.75 0.88 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 11008 0 0 0 2971 28 0 0 25 0 1 0 544095477 46833664 10653 4294967295 134512640 134672761 3221224624 3221223760 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11434 10653 603 41 0 11393 0
vsize: 45736
[startup+40.0022 s]
Raw data (loadavg): 0.79 0.88 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 11158 0 0 0 3970 29 0 0 25 0 1 0 544095477 47509504 10803 4294967295 134512640 134672761 3221224624 3221223776 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11599 10803 603 41 0 11558 0
vsize: 46396
[startup+50.0033 s]
Raw data (loadavg): 0.82 0.88 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 11343 0 0 0 4969 30 0 0 25 0 1 0 544095477 48189440 10988 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11765 10988 603 41 0 11724 0
vsize: 47060
[startup+60.004 s]
Raw data (loadavg): 0.85 0.89 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 11540 0 0 0 5968 31 0 0 25 0 1 0 544095477 48996352 11185 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11962 11185 603 41 0 11921 0
vsize: 47848
[startup+70.0042 s]
Raw data (loadavg): 0.87 0.89 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 11721 0 0 0 6967 32 0 0 25 0 1 0 544095477 49672192 11366 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12127 11366 603 41 0 12086 0
vsize: 48508
[startup+80.0042 s]
Raw data (loadavg): 0.89 0.89 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 11929 0 0 0 7967 33 0 0 25 0 1 0 544095477 50483200 11574 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12325 11574 603 41 0 12284 0
vsize: 49300
[startup+90.005 s]
Raw data (loadavg): 0.91 0.90 0.88 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 12083 0 0 0 8966 34 0 0 25 0 1 0 544095477 51159040 11728 4294967295 134512640 134672761 3221224624 3221223760 134565036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12490 11728 603 41 0 12449 0
vsize: 49960
[startup+100.004 s]
Raw data (loadavg): 0.92 0.90 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 12273 0 0 0 9966 34 0 0 25 0 1 0 544095477 51970048 11918 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12688 11918 603 41 0 12647 0
vsize: 50752
[startup+110.005 s]
Raw data (loadavg): 0.93 0.90 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 12412 0 0 0 10965 35 0 0 25 0 1 0 544095477 52527104 12057 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12824 12057 603 41 0 12783 0
vsize: 51296
[startup+120.006 s]
Raw data (loadavg): 0.94 0.90 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 12640 0 0 0 11964 36 0 0 25 0 1 0 544095477 53473280 12285 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13055 12285 603 41 0 13014 0
vsize: 52220
[startup+130.005 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 12760 0 0 0 12964 36 0 0 25 0 1 0 544095477 54013952 12405 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13187 12405 603 41 0 13146 0
vsize: 52748
[startup+140.006 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 12970 0 0 0 13963 38 0 0 25 0 1 0 544095477 54824960 12615 4294967295 134512640 134672761 3221224624 3221223808 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13385 12615 603 41 0 13344 0
vsize: 53540
[startup+150.007 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 13156 0 0 0 14962 39 0 0 25 0 1 0 544095477 55631872 12801 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13582 12801 603 41 0 13541 0
vsize: 54328
[startup+160.008 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 13363 0 0 0 15960 40 0 0 25 0 1 0 544095477 56442880 13008 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13780 13008 603 41 0 13739 0
vsize: 55120
[startup+170.008 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 13605 0 0 0 16960 41 0 0 25 0 1 0 544095477 57384960 13250 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14010 13250 603 41 0 13969 0
vsize: 56040
[startup+180.008 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 13857 0 0 0 17958 42 0 0 25 0 1 0 544095477 58462208 13502 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14273 13502 603 41 0 14232 0
vsize: 57092
[startup+190.008 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 14013 0 0 0 18957 43 0 0 25 0 1 0 544095477 59133952 13658 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14437 13658 603 41 0 14396 0
vsize: 57748
[startup+200.009 s]
Raw data (loadavg): 0.98 0.92 0.89 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 14259 0 0 0 19957 44 0 0 25 0 1 0 544095477 60080128 13904 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13904 603 41 0 14627 0
vsize: 58672
[startup+210.009 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 14470 0 0 0 20956 45 0 0 25 0 1 0 544095477 60887040 14115 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14865 14115 603 41 0 14824 0
vsize: 59460
[startup+220.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 14698 0 0 0 21955 46 0 0 25 0 1 0 544095477 61956096 14343 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15126 14343 603 41 0 15085 0
vsize: 60504
[startup+230.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 14849 0 0 0 22954 47 0 0 25 0 1 0 544095477 62631936 14494 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15291 14494 603 41 0 15250 0
vsize: 61164
[startup+240.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 15065 0 0 0 23953 48 0 0 25 0 1 0 544095477 63447040 14710 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15490 14710 603 41 0 15449 0
vsize: 61960
[startup+250.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 15420 0 0 0 24952 49 0 0 25 0 1 0 544095477 64917504 15065 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15849 15065 603 41 0 15808 0
vsize: 63396
[startup+260.012 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 15600 0 0 0 25952 50 0 0 25 0 1 0 544095477 65728512 15245 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16047 15245 603 41 0 16006 0
vsize: 64188
[startup+270.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 15802 0 0 0 26951 51 0 0 25 0 1 0 544095477 66543616 15447 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16246 15447 603 41 0 16205 0
vsize: 64984
[startup+280.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 16031 0 0 0 27950 52 0 0 25 0 1 0 544095477 67485696 15676 4294967295 134512640 134672761 3221224624 3221223728 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16476 15676 603 41 0 16435 0
vsize: 65904
[startup+290.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 16269 0 0 0 28949 53 0 0 25 0 1 0 544095477 68435968 15914 4294967295 134512640 134672761 3221224624 3221223788 134565024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16708 15914 603 41 0 16667 0
vsize: 66832
[startup+300.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 16449 0 0 0 29948 54 0 0 25 0 1 0 544095477 69103616 16094 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16871 16094 603 41 0 16830 0
vsize: 67484
[startup+310.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 16734 0 0 0 30947 55 0 0 25 0 1 0 544095477 70320128 16379 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17168 16379 603 41 0 17127 0
vsize: 68672
[startup+320.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 17002 0 0 0 31947 56 0 0 25 0 1 0 544095477 71397376 16647 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17431 16647 603 41 0 17390 0
vsize: 69724
[startup+330.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 17295 0 0 0 32946 57 0 0 25 0 1 0 544095477 72609792 16940 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17727 16940 603 41 0 17686 0
vsize: 70908
[startup+340.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 17527 0 0 0 33944 59 0 0 25 0 1 0 544095477 73555968 17172 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17958 17172 603 41 0 17917 0
vsize: 71832
[startup+350.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 17768 0 0 0 34943 60 0 0 25 0 1 0 544095477 74502144 17413 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18189 17413 603 41 0 18148 0
vsize: 72756
[startup+360.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 18010 0 0 0 35942 61 0 0 25 0 1 0 544095477 75452416 17655 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18421 17655 603 41 0 18380 0
vsize: 73684
[startup+370.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 18209 0 0 0 36942 61 0 0 25 0 1 0 544095477 76386304 17854 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18649 17854 603 41 0 18608 0
vsize: 74596
[startup+380.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 18530 0 0 0 37941 63 0 0 25 0 1 0 544095477 77578240 18175 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18940 18175 603 41 0 18899 0
vsize: 75760
[startup+390.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 18856 0 0 0 38940 64 0 0 25 0 1 0 544095477 78946304 18501 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19274 18501 603 41 0 19233 0
vsize: 77096
[startup+400.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 19087 0 0 0 39938 65 0 0 25 0 1 0 544095477 79896576 18732 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19506 18732 603 41 0 19465 0
vsize: 78024
[startup+410.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 19327 0 0 0 40938 66 0 0 25 0 1 0 544095477 80838656 18972 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19736 18972 603 41 0 19695 0
vsize: 78944
[startup+420.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 19545 0 0 0 41937 67 0 0 25 0 1 0 544095477 81784832 19190 4294967295 134512640 134672761 3221224624 3221223728 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19967 19190 603 41 0 19926 0
vsize: 79868
[startup+430.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 19754 0 0 0 42936 69 0 0 25 0 1 0 544095477 82587648 19399 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20163 19399 603 41 0 20122 0
vsize: 80652
[startup+440.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 20064 0 0 0 43935 69 0 0 25 0 1 0 544095477 83939328 19709 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20493 19709 603 41 0 20452 0
vsize: 81972
[startup+450.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 20383 0 0 0 44934 70 0 0 25 0 1 0 544095477 85155840 20028 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20790 20028 603 41 0 20749 0
vsize: 83160
[startup+460.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 20665 0 0 0 45933 71 0 0 25 0 1 0 544095477 86372352 20310 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21087 20310 603 41 0 21046 0
vsize: 84348
[startup+470.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 20898 0 0 0 46932 73 0 0 25 0 1 0 544095477 87310336 20543 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21316 20543 603 41 0 21275 0
vsize: 85264
[startup+480.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 21143 0 0 0 47931 73 0 0 25 0 1 0 544095477 88252416 20788 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21546 20788 603 41 0 21505 0
vsize: 86184
[startup+490.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 21385 0 0 0 48930 75 0 0 25 0 1 0 544095477 89329664 21030 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21809 21030 603 41 0 21768 0
vsize: 87236
[startup+500.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 21619 0 0 0 49929 76 0 0 25 0 1 0 544095477 90267648 21264 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22038 21264 603 41 0 21997 0
vsize: 88152
[startup+510.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 21896 0 0 0 50928 77 0 0 25 0 1 0 544095477 91344896 21541 4294967295 134512640 134672761 3221224624 3221223728 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22301 21541 603 41 0 22260 0
vsize: 89204
[startup+520.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 22057 0 0 0 51927 78 0 0 25 0 1 0 544095477 92020736 21702 4294967295 134512640 134672761 3221224624 3221223760 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22466 21702 603 41 0 22425 0
vsize: 89864
[startup+530.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 22319 0 0 0 52926 79 0 0 25 0 1 0 544095477 93368320 21964 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22795 21964 603 41 0 22754 0
vsize: 91180
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 22513 0 0 0 53926 80 0 0 25 0 1 0 544095477 94175232 22158 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22992 22158 603 41 0 22951 0
vsize: 91968
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 22751 0 0 0 54925 81 0 0 25 0 1 0 544095477 95113216 22396 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23221 22396 603 41 0 23180 0
vsize: 92884
[startup+560.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 23081 0 0 0 55924 82 0 0 25 0 1 0 544095477 96460800 22726 4294967295 134512640 134672761 3221224624 3221223776 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23550 22726 603 41 0 23509 0
vsize: 94200
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 23351 0 0 0 56924 82 0 0 25 0 1 0 544095477 97542144 22996 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23814 22996 603 41 0 23773 0
vsize: 95256
[startup+580.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 23566 0 0 0 57923 83 0 0 25 0 1 0 544095477 98492416 23211 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24046 23211 603 41 0 24005 0
vsize: 96184
[startup+590.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 23881 0 0 0 58922 84 0 0 25 0 1 0 544095477 99704832 23526 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24342 23526 603 41 0 24301 0
vsize: 97368
[startup+600.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 24151 0 0 0 59921 85 0 0 25 0 1 0 544095477 100909056 23796 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24636 23796 603 41 0 24595 0
vsize: 98544
[startup+610.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 24435 0 0 0 60920 86 0 0 25 0 1 0 544095477 101986304 24080 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24899 24080 603 41 0 24858 0
vsize: 99596
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 24768 0 0 0 61919 87 0 0 25 0 1 0 544095477 103346176 24413 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25231 24413 603 41 0 25190 0
vsize: 100924
[startup+630.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 25129 0 0 0 62918 88 0 0 25 0 1 0 544095477 104833024 24774 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25594 24774 603 41 0 25553 0
vsize: 102376
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 25485 0 0 0 63917 90 0 0 25 0 1 0 544095477 106319872 25130 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25957 25130 603 41 0 25916 0
vsize: 103828
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 25814 0 0 0 64916 91 0 0 25 0 1 0 544095477 107663360 25459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26285 25459 603 41 0 26244 0
vsize: 105140
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 26122 0 0 0 65915 92 0 0 25 0 1 0 544095477 108867584 25767 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26579 25767 603 41 0 26538 0
vsize: 106316
[startup+670.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 26465 0 0 0 66914 93 0 0 25 0 1 0 544095477 110333952 26110 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26937 26110 603 41 0 26896 0
vsize: 107748
[startup+680.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 26808 0 0 0 67914 94 0 0 25 0 1 0 544095477 111681536 26453 4294967295 134512640 134672761 3221224624 3221223808 134558934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27266 26453 603 41 0 27225 0
vsize: 109064
[startup+690.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 27080 0 0 0 68914 94 0 0 25 0 1 0 544095477 112762880 26725 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27530 26725 603 41 0 27489 0
vsize: 110120
[startup+700.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 27413 0 0 0 69913 95 0 0 25 0 1 0 544095477 114118656 27058 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27861 27058 603 41 0 27820 0
vsize: 111444
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 27612 0 0 0 70913 95 0 0 25 0 1 0 544095477 114921472 27257 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28057 27257 603 41 0 28016 0
vsize: 112228
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 27935 0 0 0 71912 96 0 0 25 0 1 0 544095477 116248576 27580 4294967295 134512640 134672761 3221224624 3221223728 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28381 27580 603 41 0 28340 0
vsize: 113524
[startup+730.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 28261 0 0 0 72912 97 0 0 25 0 1 0 544095477 117616640 27906 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28715 27906 603 41 0 28674 0
vsize: 114860
[startup+740.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 28515 0 0 0 73912 97 0 0 25 0 1 0 544095477 118697984 28160 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28979 28160 603 41 0 28938 0
vsize: 115916
[startup+750.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 28835 0 0 0 74912 98 0 0 25 0 1 0 544095477 120037376 28480 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29306 28480 603 41 0 29265 0
vsize: 117224
[startup+760.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 29088 0 0 0 75912 99 0 0 25 0 1 0 544095477 120979456 28733 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29536 28733 603 41 0 29495 0
vsize: 118144
[startup+770.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 29329 0 0 0 76910 100 0 0 25 0 1 0 544095477 121929728 28974 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29768 28974 603 41 0 29727 0
vsize: 119072
[startup+780.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 29639 0 0 0 77910 101 0 0 25 0 1 0 544095477 123260928 29284 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30093 29284 603 41 0 30052 0
vsize: 120372
[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 29907 0 0 0 78911 102 0 0 25 0 1 0 544095477 124342272 29552 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30357 29552 603 41 0 30316 0
vsize: 121428
[startup+800.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 30358 0 0 0 79910 103 0 0 25 0 1 0 544095477 126238720 30003 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30820 30003 603 41 0 30779 0
vsize: 123280
[startup+810.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 30661 0 0 0 80909 103 0 0 25 0 1 0 544095477 127467520 30306 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31120 30306 603 41 0 31079 0
vsize: 124480
[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 30920 0 0 0 81909 104 0 0 25 0 1 0 544095477 128409600 30565 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31350 30565 603 41 0 31309 0
vsize: 125400
[startup+830.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 31130 0 0 0 82908 105 0 0 25 0 1 0 544095477 129347584 30775 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31579 30775 603 41 0 31538 0
vsize: 126316
[startup+840.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 31433 0 0 0 83908 106 0 0 25 0 1 0 544095477 130564096 31078 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31876 31078 603 41 0 31835 0
vsize: 127504
[startup+850.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 31836 0 0 0 84907 106 0 0 25 0 1 0 544095477 132136960 31481 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32260 31481 603 41 0 32219 0
vsize: 129040
[startup+860.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 32087 0 0 0 85907 107 0 0 25 0 1 0 544095477 133226496 31732 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32526 31732 603 41 0 32485 0
vsize: 130104
[startup+870.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 32398 0 0 0 86905 109 0 0 25 0 1 0 544095477 134545408 32043 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32848 32043 603 41 0 32807 0
vsize: 131392
[startup+880.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 32634 0 0 0 87905 109 0 0 25 0 1 0 544095477 135487488 32279 4294967295 134512640 134672761 3221224624 3221223728 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33078 32279 603 41 0 33037 0
vsize: 132312
[startup+890.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 33002 0 0 0 88905 109 0 0 25 0 1 0 544095477 136982528 32647 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33443 32647 603 41 0 33402 0
vsize: 133772
[startup+900.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 33203 0 0 0 89905 110 0 0 25 0 1 0 544095477 137793536 32848 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33641 32848 603 41 0 33600 0
vsize: 134564
[startup+910.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 33423 0 0 0 90905 110 0 0 25 0 1 0 544095477 138727424 33068 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33869 33068 603 41 0 33828 0
vsize: 135476
[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 33683 0 0 0 91904 111 0 0 25 0 1 0 544095477 139812864 33328 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34134 33328 603 41 0 34093 0
vsize: 136536
[startup+930.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 34064 0 0 0 92903 112 0 0 25 0 1 0 544095477 141287424 33709 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34494 33709 603 41 0 34453 0
vsize: 137976
[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 34377 0 0 0 93903 113 0 0 25 0 1 0 544095477 142618624 34022 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34819 34022 603 41 0 34778 0
vsize: 139276
[startup+950.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 34730 0 0 0 94902 114 0 0 25 0 1 0 544095477 143978496 34375 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35151 34375 603 41 0 35110 0
vsize: 140604
[startup+960.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 35161 0 0 0 95902 114 0 0 25 0 1 0 544095477 145743872 34806 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35582 34806 603 41 0 35541 0
vsize: 142328
[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 35462 0 0 0 96901 115 0 0 25 0 1 0 544095477 146972672 35107 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35882 35107 603 41 0 35841 0
vsize: 143528
[startup+980.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 35694 0 0 0 97901 116 0 0 25 0 1 0 544095477 147898368 35339 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36108 35339 603 41 0 36067 0
vsize: 144432
[startup+990.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23793
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 35934 0 0 0 98900 116 0 0 25 0 1 0 544095477 148979712 35579 4294967295 134512640 134672761 3221224624 3221223728 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36372 35579 603 41 0 36331 0
vsize: 145488
[startup+1000.08 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 23794
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 36060 0 0 0 99900 116 0 0 25 0 1 0 544095477 149381120 35705 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36470 35705 603 41 0 36429 0
vsize: 145880
[startup+1010.08 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 23846
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 36278 0 0 0 100900 117 0 0 25 0 1 0 544095477 150319104 35923 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36699 35923 603 41 0 36658 0
vsize: 146796
[startup+1020.08 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 23846
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 36556 0 0 0 101900 117 0 0 25 0 1 0 544095477 151531520 36201 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36995 36201 603 41 0 36954 0
vsize: 147980
[startup+1030.08 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 23846
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 36921 0 0 0 102899 118 0 0 25 0 1 0 544095477 152879104 36566 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37324 36566 603 41 0 37283 0
vsize: 149296
[startup+1040.08 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 23846
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 37063 0 0 0 103898 119 0 0 25 0 1 0 544095477 153550848 36708 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37488 36708 603 41 0 37447 0
vsize: 149952
[startup+1050.08 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 23846
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 37347 0 0 0 104898 119 0 0 25 0 1 0 544095477 154636288 36992 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37753 36992 603 41 0 37712 0
vsize: 151012
[startup+1060.08 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 23846
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 37603 0 0 0 105897 120 0 0 25 0 1 0 544095477 155709440 37248 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38015 37248 603 41 0 37974 0
vsize: 152060
[startup+1070.08 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 37907 0 0 0 106897 120 0 0 25 0 1 0 544095477 156901376 37552 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38306 37552 603 41 0 38265 0
vsize: 153224
[startup+1080.08 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 38155 0 0 0 107897 121 0 0 25 0 1 0 544095477 157978624 37800 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38569 37800 603 41 0 38528 0
vsize: 154276
[startup+1090.08 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 38389 0 0 0 108896 122 0 0 25 0 1 0 544095477 158916608 38034 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38798 38034 603 41 0 38757 0
vsize: 155192
[startup+1100.08 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 38717 0 0 0 109895 123 0 0 25 0 1 0 544095477 160256000 38362 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39125 38362 603 41 0 39084 0
vsize: 156500
[startup+1110.08 s]
Raw data (loadavg): 1.02 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 39044 0 0 0 110894 124 0 0 25 0 1 0 544095477 161611776 38689 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39456 38689 603 41 0 39415 0
vsize: 157824
[startup+1120.08 s]
Raw data (loadavg): 1.02 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 39415 0 0 0 111893 125 0 0 25 0 1 0 544095477 163086336 39060 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39816 39060 603 41 0 39775 0
vsize: 159264
[startup+1130.08 s]
Raw data (loadavg): 1.02 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 39781 0 0 0 112893 126 0 0 25 0 1 0 544095477 164651008 39426 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40198 39426 603 41 0 40157 0
vsize: 160792
[startup+1140.08 s]
Raw data (loadavg): 1.01 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 40110 0 0 0 113891 127 0 0 25 0 1 0 544095477 166064128 39755 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40543 39755 603 41 0 40502 0
vsize: 162172
[startup+1150.08 s]
Raw data (loadavg): 1.01 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 40337 0 0 0 114891 128 0 0 25 0 1 0 544095477 166875136 39982 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40741 39982 603 41 0 40700 0
vsize: 162964
[startup+1160.08 s]
Raw data (loadavg): 1.01 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 40540 0 0 0 115890 129 0 0 25 0 1 0 544095477 167809024 40185 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40969 40185 603 41 0 40928 0
vsize: 163876
[startup+1170.08 s]
Raw data (loadavg): 1.01 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 40849 0 0 0 116890 130 0 0 25 0 1 0 544095477 169017344 40494 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41264 40494 603 41 0 41223 0
vsize: 165056
[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 41021 0 0 0 117889 130 0 0 25 0 1 0 544095477 169697280 40666 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41430 40666 603 41 0 41389 0
vsize: 165720
[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 41223 0 0 0 118889 131 0 0 25 0 1 0 544095477 170504192 40868 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41627 40868 603 41 0 41586 0
vsize: 166508
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.92 3/54 23848
Raw data (stat): 23793 (minisat+) R 23792 10614 10613 0 -1 0 41560 0 0 0 119888 131 0 0 25 0 1 0 544095477 171966464 41205 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41984 41205 603 41 0 41943 0
vsize: 167936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 23848
Raw data (stat): 23793 (minisat+) Z 23792 10614 10613 0 -1 12 41562 0 0 0 119889 139 0 0 25 0 1 0 544095477 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.16
CPU time (s): 1200.29
CPU user time (s): 1198.89
CPU system time (s): 1.39579
CPU usage (%): 100.011
Max. virtual memory (Kb): 167936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####