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 21882

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-22 01:21:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12433 boxname=wulflinc30 idbench=957 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ee388359e66788d310d5d5b34d6465c1  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-air04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-air04.opb
IDLAUNCH: 12433
/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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        760488 kB
Buffers:         13184 kB
Cached:         235208 kB
SwapCached:        352 kB
Active:          24476 kB
Inactive:       226576 kB
HighTotal:      131008 kB
HighFree:        32032 kB
LowTotal:       903652 kB
LowFree:        728456 kB
SwapTotal:     2097892 kB
SwapFree:      2097328 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5980 kB
Slab:            17400 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:41:05 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 12433 7 1200.27 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 |  310358   807732 |  103452       0        0     nan |  0.000 % |
c |       101 |  310358   807732 |  113797     101     4421    43.8 |  0.588 % |
c |       251 |  310340   807685 |  125176     248     8941    36.1 |  0.590 % |
c |       477 |  310255   807455 |  137694     461    13728    29.8 |  0.603 % |
c |       814 |  310255   807455 |  151464     798    37090    46.5 |  0.603 % |
c |      1320 |  309505   805553 |  166610    1266    60778    48.0 |  0.693 % |
c |      2079 |  309327   805067 |  183271    2007    94497    47.1 |  0.730 % |
c |      3219 |  308710   803466 |  201598    3121   175840    56.3 |  0.848 % |
c |      4927 |  308374   802597 |  221758    4783   334504    69.9 |  0.896 % |
c |      7489 |  307940   801458 |  243934    7200   539854    75.0 |  0.948 % |
c |     11334 |  307798   801098 |  268327   11017  1054203    95.7 |  0.963 % |
c |     17100 |  307510   800357 |  295160   16719  1913448   114.4 |  0.992 % |
c |     25749 |  307286   799785 |  324676   25320  3051328   120.5 |  1.011 % |
c |     38723 |  307204   799580 |  357144   38277  5578865   145.7 |  1.014 % |
c |     58184 |  306684   798243 |  392858   57603  9277788   161.1 |  1.076 % |
c |     87376 |  306512   797802 |  432144   86712 17039623   196.5 |  1.089 % |
c |    131165 |  306227   797059 |  475359  130316 29832985   228.9 |  1.132 % |
#### 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.92 0.97 0.91 2/54 1180
Raw data (stat): 1180 (runsolver) R 1179 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549714316 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0006 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 11039 0 0 0 969 29 0 0 25 0 1 0 549714316 54317056 10669 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13261 10669 603 41 0 13220 0
vsize: 53044
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 11177 0 0 0 1968 30 0 0 25 0 1 0 549714316 54857728 10807 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13393 10807 603 41 0 13352 0
vsize: 53572
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 11355 0 0 0 2968 30 0 0 25 0 1 0 549714316 55672832 10985 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13592 10985 603 41 0 13551 0
vsize: 54368
[startup+40.0031 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 11528 0 0 0 3967 31 0 0 25 0 1 0 549714316 56344576 11158 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13756 11158 603 41 0 13715 0
vsize: 55024
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 11707 0 0 0 4966 32 0 0 25 0 1 0 549714316 57061376 11337 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13931 11337 603 41 0 13890 0
vsize: 55724
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 12017 0 0 0 5965 33 0 0 25 0 1 0 549714316 58269696 11647 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14226 11647 603 41 0 14185 0
vsize: 56904
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 12289 0 0 0 6965 34 0 0 25 0 1 0 549714316 59486208 11919 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14523 11919 603 41 0 14482 0
vsize: 58092
[startup+80.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 12666 0 0 0 7964 34 0 0 25 0 1 0 549714316 60968960 12296 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14885 12296 603 41 0 14844 0
vsize: 59540
[startup+90.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 12990 0 0 0 8963 36 0 0 25 0 1 0 549714316 62427136 12620 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15241 12620 603 41 0 15200 0
vsize: 60964
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 13310 0 0 0 9962 37 0 0 25 0 1 0 549714316 63643648 12940 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15538 12940 603 41 0 15497 0
vsize: 62152
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 13554 0 0 0 10961 38 0 0 25 0 1 0 549714316 64585728 13184 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15768 13184 603 41 0 15727 0
vsize: 63072
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 13845 0 0 0 11960 40 0 0 25 0 1 0 549714316 65794048 13475 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16063 13475 603 41 0 16022 0
vsize: 64252
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 14096 0 0 0 12959 40 0 0 25 0 1 0 549714316 66875392 13726 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16327 13726 603 41 0 16286 0
vsize: 65308
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 14446 0 0 0 13958 41 0 0 25 0 1 0 549714316 68222976 14076 4294967295 134512640 134672761 3221224624 3221223808 134559665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 14076 603 41 0 16615 0
vsize: 66624
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 14688 0 0 0 14957 42 0 0 25 0 1 0 549714316 69156864 14318 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16884 14318 603 41 0 16843 0
vsize: 67536
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 15070 0 0 0 15956 44 0 0 25 0 1 0 549714316 70766592 14700 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17277 14700 603 41 0 17236 0
vsize: 69108
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 15367 0 0 0 16955 45 0 0 25 0 1 0 549714316 71991296 14997 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17576 14997 603 41 0 17535 0
vsize: 70304
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 15693 0 0 0 17953 46 0 0 25 0 1 0 549714316 73338880 15323 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17905 15323 603 41 0 17864 0
vsize: 71620
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 16069 0 0 0 18952 48 0 0 25 0 1 0 549714316 74948608 15699 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18298 15699 603 41 0 18257 0
vsize: 73192
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 16456 0 0 0 19950 50 0 0 25 0 1 0 549714316 76558336 16086 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18691 16086 603 41 0 18650 0
vsize: 74764
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 16770 0 0 0 20949 52 0 0 25 0 1 0 549714316 77770752 16400 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18987 16400 603 41 0 18946 0
vsize: 75948
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 17062 0 0 0 21948 53 0 0 25 0 1 0 549714316 78979072 16692 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19282 16692 603 41 0 19241 0
vsize: 77128
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 17283 0 0 0 22946 54 0 0 25 0 1 0 549714316 79921152 16913 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19512 16913 603 41 0 19471 0
vsize: 78048
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 17549 0 0 0 23946 55 0 0 25 0 1 0 549714316 80994304 17179 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19774 17179 603 41 0 19733 0
vsize: 79096
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 17802 0 0 0 24945 56 0 0 25 0 1 0 549714316 82075648 17432 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20038 17432 603 41 0 19997 0
vsize: 80152
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 18165 0 0 0 25944 57 0 0 25 0 1 0 549714316 83558400 17795 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20400 17795 603 41 0 20359 0
vsize: 81600
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 18552 0 0 0 26943 58 0 0 25 0 1 0 549714316 85045248 18182 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20763 18182 603 41 0 20722 0
vsize: 83052
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 18785 0 0 0 27942 59 0 0 25 0 1 0 549714316 85987328 18415 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20993 18415 603 41 0 20952 0
vsize: 83972
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 19059 0 0 0 28942 59 0 0 25 0 1 0 549714316 87195648 18689 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21288 18689 603 41 0 21247 0
vsize: 85152
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 19353 0 0 0 29941 60 0 0 25 0 1 0 549714316 88272896 18983 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21551 18983 603 41 0 21510 0
vsize: 86204
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 19714 0 0 0 30941 61 0 0 25 0 1 0 549714316 89751552 19344 4294967295 134512640 134672761 3221224624 3221223728 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21912 19344 603 41 0 21871 0
vsize: 87648
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 19993 0 0 0 31940 62 0 0 25 0 1 0 549714316 90959872 19623 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22207 19623 603 41 0 22166 0
vsize: 88828
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 20426 0 0 0 32939 63 0 0 25 0 1 0 549714316 92704768 20056 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22633 20056 603 41 0 22592 0
vsize: 90532
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 20814 0 0 0 33939 64 0 0 25 0 1 0 549714316 94314496 20444 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23026 20444 603 41 0 22985 0
vsize: 92104
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 21106 0 0 0 34937 65 0 0 25 0 1 0 549714316 95522816 20736 4294967295 134512640 134672761 3221224624 3221223640 1075353266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23321 20736 603 41 0 23280 0
vsize: 93284
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 21321 0 0 0 35937 65 0 0 25 0 1 0 549714316 96329728 20951 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23518 20951 603 41 0 23477 0
vsize: 94072
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 21747 0 0 0 36936 66 0 0 25 0 1 0 549714316 98082816 21377 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23946 21377 603 41 0 23905 0
vsize: 95784
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 22082 0 0 0 37936 67 0 0 25 0 1 0 549714316 99430400 21712 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24275 21712 603 41 0 24234 0
vsize: 97100
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 22433 0 0 0 38935 68 0 0 25 0 1 0 549714316 100904960 22063 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24635 22063 603 41 0 24594 0
vsize: 98540
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 22778 0 0 0 39934 69 0 0 25 0 1 0 549714316 102506496 22408 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25026 22408 603 41 0 24985 0
vsize: 100104
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 23057 0 0 0 40933 70 0 0 25 0 1 0 549714316 103723008 22687 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25323 22687 603 41 0 25282 0
vsize: 101292
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 23456 0 0 0 41932 71 0 0 25 0 1 0 549714316 105340928 23086 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25718 23086 603 41 0 25677 0
vsize: 102872
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 23898 0 0 0 42932 72 0 0 25 0 1 0 549714316 107220992 23528 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26177 23528 603 41 0 26136 0
vsize: 104708
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 24228 0 0 0 43931 73 0 0 25 0 1 0 549714316 108560384 23858 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26504 23858 603 41 0 26463 0
vsize: 106016
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 24440 0 0 0 44930 74 0 0 25 0 1 0 549714316 109371392 24070 4294967295 134512640 134672761 3221224624 3221223760 134560606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26702 24070 603 41 0 26661 0
vsize: 106808
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 24754 0 0 0 45930 74 0 0 25 0 1 0 549714316 110714880 24384 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27030 24384 603 41 0 26989 0
vsize: 108120
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 25152 0 0 0 46929 75 0 0 25 0 1 0 549714316 112332800 24782 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27425 24782 603 41 0 27384 0
vsize: 109700
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 25540 0 0 0 47929 76 0 0 25 0 1 0 549714316 113811456 25170 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27786 25170 603 41 0 27745 0
vsize: 111144
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 25906 0 0 0 48928 77 0 0 25 0 1 0 549714316 115425280 25536 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28180 25536 603 41 0 28139 0
vsize: 112720
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 26275 0 0 0 49926 79 0 0 25 0 1 0 549714316 116895744 25905 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28539 25905 603 41 0 28498 0
vsize: 114156
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 26540 0 0 0 50925 80 0 0 25 0 1 0 549714316 117964800 26170 4294967295 134512640 134672761 3221224624 3221223808 134559566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28800 26170 603 41 0 28759 0
vsize: 115200
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 26891 0 0 0 51925 81 0 0 25 0 1 0 549714316 119443456 26521 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29161 26521 603 41 0 29120 0
vsize: 116644
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 27390 0 0 0 52923 82 0 0 25 0 1 0 549714316 121454592 27020 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29652 27020 603 41 0 29611 0
vsize: 118608
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 27705 0 0 0 53923 83 0 0 25 0 1 0 549714316 122654720 27335 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29945 27335 603 41 0 29904 0
vsize: 119780
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 28046 0 0 0 54921 85 0 0 25 0 1 0 549714316 124162048 27676 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30313 27676 603 41 0 30272 0
vsize: 121252
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 28466 0 0 0 55921 85 0 0 25 0 1 0 549714316 125784064 28096 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30709 28096 603 41 0 30668 0
vsize: 122836
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 28948 0 0 0 56920 86 0 0 25 0 1 0 549714316 127803392 28578 4294967295 134512640 134672761 3221224624 3221223728 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31202 28578 603 41 0 31161 0
vsize: 124808
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 29346 0 0 0 57918 88 0 0 25 0 1 0 549714316 129417216 28976 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31596 28976 603 41 0 31555 0
vsize: 126384
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 29735 0 0 0 58917 89 0 0 25 0 1 0 549714316 131018752 29365 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31987 29365 603 41 0 31946 0
vsize: 127948
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 30068 0 0 0 59917 89 0 0 25 0 1 0 549714316 132386816 29698 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32321 29698 603 41 0 32280 0
vsize: 129284
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 30488 0 0 0 60916 90 0 0 25 0 1 0 549714316 134008832 30118 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32717 30118 603 41 0 32676 0
vsize: 130868
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 30866 0 0 0 61915 91 0 0 25 0 1 0 549714316 135634944 30496 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33114 30496 603 41 0 33073 0
vsize: 132456
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 31254 0 0 0 62915 92 0 0 25 0 1 0 549714316 137240576 30884 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33506 30884 603 41 0 33465 0
vsize: 134024
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 31708 0 0 0 63913 93 0 0 25 0 1 0 549714316 139112448 31338 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33963 31338 603 41 0 33922 0
vsize: 135852
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 31948 0 0 0 64913 94 0 0 25 0 1 0 549714316 140046336 31578 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34191 31578 603 41 0 34150 0
vsize: 136764
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 32189 0 0 0 65912 95 0 0 25 0 1 0 549714316 141123584 31819 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34454 31819 603 41 0 34413 0
vsize: 137816
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 32547 0 0 0 66912 96 0 0 25 0 1 0 549714316 142598144 32177 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34814 32177 603 41 0 34773 0
vsize: 139256
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 32908 0 0 0 67911 96 0 0 25 0 1 0 549714316 144068608 32538 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35173 32538 603 41 0 35132 0
vsize: 140692
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 33307 0 0 0 68910 98 0 0 25 0 1 0 549714316 145678336 32937 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35566 32937 603 41 0 35525 0
vsize: 142264
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 33655 0 0 0 69909 99 0 0 25 0 1 0 549714316 147017728 33285 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35893 33285 603 41 0 35852 0
vsize: 143572
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 34011 0 0 0 70909 99 0 0 25 0 1 0 549714316 148504576 33641 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36256 33641 603 41 0 36215 0
vsize: 145024
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 34346 0 0 0 71908 100 0 0 25 0 1 0 549714316 149856256 33976 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36586 33976 603 41 0 36545 0
vsize: 146344
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 34718 0 0 0 72907 101 0 0 25 0 1 0 549714316 151478272 34348 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36982 34348 603 41 0 36941 0
vsize: 147928
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 34991 0 0 0 73907 102 0 0 25 0 1 0 549714316 152551424 34621 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37244 34621 603 41 0 37203 0
vsize: 148976
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 35363 0 0 0 74906 103 0 0 25 0 1 0 549714316 154025984 34993 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37604 34993 603 41 0 37563 0
vsize: 150416
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 35780 0 0 0 75905 104 0 0 25 0 1 0 549714316 155766784 35410 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38029 35410 603 41 0 37988 0
vsize: 152116
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 36059 0 0 0 76904 105 0 0 25 0 1 0 549714316 156844032 35689 4294967295 134512640 134672761 3221224624 3221223808 134558347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38292 35689 603 41 0 38251 0
vsize: 153168
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 36349 0 0 0 77904 106 0 0 25 0 1 0 549714316 158056448 35979 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38588 35979 603 41 0 38547 0
vsize: 154352
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 36646 0 0 0 78903 107 0 0 25 0 1 0 549714316 159264768 36276 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38883 36276 603 41 0 38842 0
vsize: 155532
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 36953 0 0 0 79902 108 0 0 25 0 1 0 549714316 160591872 36583 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39207 36583 603 41 0 39166 0
vsize: 156828
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 37281 0 0 0 80901 109 0 0 25 0 1 0 549714316 161800192 36911 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39502 36911 603 41 0 39461 0
vsize: 158008
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 37512 0 0 0 81901 109 0 0 25 0 1 0 549714316 162742272 37142 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39732 37142 603 41 0 39691 0
vsize: 158928
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 37776 0 0 0 82900 110 0 0 25 0 1 0 549714316 163962880 37406 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40030 37406 603 41 0 39989 0
vsize: 160120
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 37991 0 0 0 83900 111 0 0 25 0 1 0 549714316 164769792 37621 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40227 37621 603 41 0 40186 0
vsize: 160908
[startup+850.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 38255 0 0 0 84899 112 0 0 25 0 1 0 549714316 165851136 37885 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40491 37885 603 41 0 40450 0
vsize: 161964
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 38546 0 0 0 85898 113 0 0 25 0 1 0 549714316 167071744 38176 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40789 38176 603 41 0 40748 0
vsize: 163156
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 38890 0 0 0 86897 114 0 0 25 0 1 0 549714316 168411136 38520 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41116 38520 603 41 0 41075 0
vsize: 164464
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 39193 0 0 0 87897 115 0 0 25 0 1 0 549714316 169758720 38823 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41445 38823 603 41 0 41404 0
vsize: 165780
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 39432 0 0 0 88896 115 0 0 25 0 1 0 549714316 170692608 39062 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41673 39062 603 41 0 41632 0
vsize: 166692
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 39762 0 0 0 89896 116 0 0 25 0 1 0 549714316 172048384 39392 4294967295 134512640 134672761 3221224624 3221223728 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42004 39392 603 41 0 41963 0
vsize: 168016
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 40021 0 0 0 90895 116 0 0 25 0 1 0 549714316 173117440 39651 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42265 39651 603 41 0 42224 0
vsize: 169060
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 40311 0 0 0 91895 117 0 0 25 0 1 0 549714316 174198784 39941 4294967295 134512640 134672761 3221224624 3221223728 134560013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42529 39941 603 41 0 42488 0
vsize: 170116
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 40621 0 0 0 92895 118 0 0 25 0 1 0 549714316 175546368 40251 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42858 40251 603 41 0 42817 0
vsize: 171432
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 40908 0 0 0 93894 118 0 0 25 0 1 0 549714316 176762880 40538 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43155 40538 603 41 0 43114 0
vsize: 172620
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 41094 0 0 0 94894 119 0 0 25 0 1 0 549714316 177438720 40724 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43320 40724 603 41 0 43279 0
vsize: 173280
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 41389 0 0 0 95894 119 0 0 25 0 1 0 549714316 178651136 41019 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43616 41019 603 41 0 43575 0
vsize: 174464
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 41673 0 0 0 96893 120 0 0 25 0 1 0 549714316 179867648 41303 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43913 41303 603 41 0 43872 0
vsize: 175652
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 41966 0 0 0 97892 121 0 0 25 0 1 0 549714316 181059584 41596 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44204 41596 603 41 0 44163 0
vsize: 176816
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 42304 0 0 0 98892 121 0 0 25 0 1 0 549714316 182394880 41934 4294967295 134512640 134672761 3221224624 3221223728 134559939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44530 41934 603 41 0 44489 0
vsize: 178120
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 42597 0 0 0 99891 122 0 0 25 0 1 0 549714316 184119296 42227 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44951 42227 603 41 0 44910 0
vsize: 179804
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 42875 0 0 0 100891 123 0 0 25 0 1 0 549714316 185319424 42505 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45244 42505 603 41 0 45203 0
vsize: 180976
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 43027 0 0 0 101891 123 0 0 25 0 1 0 549714316 185860096 42657 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45376 42657 603 41 0 45335 0
vsize: 181504
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 43266 0 0 0 102890 123 0 0 25 0 1 0 549714316 186798080 42896 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45605 42896 603 41 0 45564 0
vsize: 182420
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 43634 0 0 0 103890 124 0 0 25 0 1 0 549714316 188293120 43264 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45970 43264 603 41 0 45929 0
vsize: 183880
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 43962 0 0 0 104889 125 0 0 25 0 1 0 549714316 189755392 43592 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46327 43593 603 41 0 46286 0
vsize: 185308
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 44253 0 0 0 105889 125 0 0 25 0 1 0 549714316 190836736 43883 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46591 43883 603 41 0 46550 0
vsize: 186364
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 44530 0 0 0 106888 126 0 0 25 0 1 0 549714316 192045056 44160 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46886 44160 603 41 0 46845 0
vsize: 187544
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 44902 0 0 0 107888 127 0 0 25 0 1 0 549714316 193527808 44532 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47248 44532 603 41 0 47207 0
vsize: 188992
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 45399 0 0 0 108887 128 0 0 25 0 1 0 549714316 195571712 45029 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47747 45029 603 41 0 47706 0
vsize: 190988
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 45637 0 0 0 109886 129 0 0 25 0 1 0 549714316 196509696 45267 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47976 45267 603 41 0 47935 0
vsize: 191904
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 45892 0 0 0 110885 130 0 0 25 0 1 0 549714316 197574656 45522 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48236 45522 603 41 0 48195 0
vsize: 192944
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 46112 0 0 0 111884 131 0 0 25 0 1 0 549714316 198508544 45742 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48464 45742 603 41 0 48423 0
vsize: 193856
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 46525 0 0 0 112883 133 0 0 25 0 1 0 549714316 200101888 46155 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48853 46155 603 41 0 48812 0
vsize: 195412
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 46861 0 0 0 113883 133 0 0 25 0 1 0 549714316 201580544 46491 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49214 46491 603 41 0 49173 0
vsize: 196856
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 47006 0 0 0 114882 134 0 0 25 0 1 0 549714316 202121216 46636 4294967295 134512640 134672761 3221224624 3221223632 1075349648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49346 46636 603 41 0 49305 0
vsize: 197384
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 47258 0 0 0 115882 134 0 0 25 0 1 0 549714316 203198464 46888 4294967295 134512640 134672761 3221224624 3221223792 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49609 46888 603 41 0 49568 0
vsize: 198436
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 47479 0 0 0 116882 134 0 0 25 0 1 0 549714316 204136448 47109 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49838 47109 603 41 0 49797 0
vsize: 199352
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 47759 0 0 0 117882 136 0 0 25 0 1 0 549714316 205213696 47389 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50101 47389 603 41 0 50060 0
vsize: 200404
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 48025 0 0 0 118881 137 0 0 25 0 1 0 549714316 206286848 47655 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50363 47655 603 41 0 50322 0
vsize: 201452
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1180
Raw data (stat): 1180 (minisat+) R 1179 11931 11930 0 -1 0 48176 0 0 0 119881 137 0 0 25 0 1 0 549714316 206962688 47806 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50528 47806 603 41 0 50487 0
vsize: 202112
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1180
Raw data (stat): 1180 (minisat+) Z 1179 11931 11930 0 -1 12 48178 0 0 0 119881 146 0 0 25 0 1 0 549714316 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.13
CPU time (s): 1200.27
CPU user time (s): 1198.81
CPU system time (s): 1.46178
CPU usage (%): 100.012
Max. virtual memory (Kb): 202112
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####