PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-t1717.opb
MD5SUM	bc46e72682d969c09e6f4028df473a45
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	201342
Optimality of the best value was proved	NO
Number of terms in the objective function	73885
Biggest coefficient in the objective function	4066
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	172074995
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	4066
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	172074995
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.34
Number of variables	73885
Total number of constraints	74436
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	74436
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	612
Trace number 18862

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        524520 kB
Buffers:         34688 kB
Cached:         453552 kB
SwapCached:          0 kB
Active:         173880 kB
Inactive:       317128 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        524268 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            13572 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:08:40 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 18069 7 1200.34 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1102 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1100]---> BDD-cost: 1179
c ---[1098]---> BDD-cost: 1181
c ---[1096]---> BDD-cost: 1169
c ---[1094]---> BDD-cost: 1171
c ---[1092]---> BDD-cost: 1183
c ---[1090]---> BDD-cost: 1167
c ---[1088]---> BDD-cost: 1169
c ---[1086]---> BDD-cost: 1181
c ---[1084]---> BDD-cost: 1177
c ---[1082]---> BDD-cost: 1175
c ---[1080]---> BDD-cost: 1183
c ---[1078]---> BDD-cost: 1179
c ---[1076]---> BDD-cost: 1175
c ---[1074]---> BDD-cost: 1171
c ---[1072]---> BDD-cost: 1167
c ---[1070]---> BDD-cost: 1169
c ---[1068]---> BDD-cost: 1167
c ---[1066]---> BDD-cost: 1189
c ---[1064]---> BDD-cost: 1167
c ---[1062]---> BDD-cost: 1169
c ---[1060]---> BDD-cost: 1179
c ---[1058]---> BDD-cost: 1173
c ---[1056]---> BDD-cost: 1215
c ---[1054]---> BDD-cost: 1167
c ---[1052]---> BDD-cost: 1179
c ---[1050]---> BDD-cost: 1173
c ---[1048]---> BDD-cost: 1181
c ---[1046]---> BDD-cost: 1191
c ---[1044]---> BDD-cost: 1175
c ---[1042]---> BDD-cost: 1173
c ---[1040]---> BDD-cost: 1171
c ---[1038]---> BDD-cost: 1177
c ---[1036]---> BDD-cost: 1169
c ---[1034]---> BDD-cost: 1169
c ---[1032]---> BDD-cost: 1187
c ---[1030]---> BDD-cost: 1187
c ---[1028]---> BDD-cost: 1169
c ---[1026]---> BDD-cost: 1175
c ---[1024]---> BDD-cost: 1179
c ---[1022]---> BDD-cost: 1177
c ---[1020]---> BDD-cost: 1171
c ---[1018]---> BDD-cost: 1175
c ---[1016]---> BDD-cost: 1187
c ---[1014]---> BDD-cost: 1179
c ---[1012]---> BDD-cost: 1187
c ---[1010]---> BDD-cost: 1169
c ---[1008]---> BDD-cost: 1183
c ---[1006]---> BDD-cost: 1185
c ---[1004]---> BDD-cost: 1175
c ---[1002]---> BDD-cost: 1179
c ---[1000]---> BDD-cost: 1181
c ---[ 998]---> BDD-cost: 1155
c ---[ 996]---> BDD-cost: 1203
c ---[ 994]---> BDD-cost: 1191
c ---[ 992]---> BDD-cost: 1189
c ---[ 990]---> BDD-cost: 1175
c ---[ 988]---> BDD-cost: 1171
c ---[ 986]---> BDD-cost: 1191
c ---[ 984]---> BDD-cost: 1169
c ---[ 982]---> BDD-cost: 1187
c ---[ 980]---> BDD-cost: 1027
c ---[ 978]---> BDD-cost: 1175
c ---[ 976]---> BDD-cost: 1039
c ---[ 974]---> BDD-cost: 1185
c ---[ 972]---> BDD-cost: 1177
c ---[ 970]---> BDD-cost: 1167
c ---[ 968]---> BDD-cost: 1175
c ---[ 966]---> BDD-cost: 1171
c ---[ 964]---> BDD-cost: 1171
c ---[ 962]---> BDD-cost: 1175
c ---[ 960]---> BDD-cost: 1193
c ---[ 958]---> BDD-cost: 1171
c ---[ 956]---> BDD-cost: 1193
c ---[ 954]---> BDD-cost: 1175
c ---[ 952]---> BDD-cost: 1029
c ---[ 950]---> BDD-cost: 1193
c ---[ 948]---> BDD-cost: 1103
c ---[ 946]---> BDD-cost: 1171
c ---[ 944]---> BDD-cost: 1189
c ---[ 942]---> BDD-cost: 1179
c ---[ 940]---> BDD-cost: 1191
c ---[ 938]---> BDD-cost: 1003
c ---[ 936]---> BDD-cost: 1171
c ---[ 934]---> BDD-cost: 1171
c ---[ 932]---> BDD-cost: 1213
c ---[ 930]---> BDD-cost: 1175
c ---[ 928]---> BDD-cost: 1181
c ---[ 926]---> BDD-cost: 1173
c ---[ 924]---> BDD-cost: 1179
c ---[ 922]---> BDD-cost: 1179
c ---[ 920]---> BDD-cost: 1175
c ---[ 918]---> BDD-cost:  989
c ---[ 916]---> BDD-cost: 1187
c ---[ 914]---> BDD-cost: 1025
c ---[ 912]---> BDD-cost: 1141
c ---[ 910]---> BDD-cost: 1167
c ---[ 908]---> BDD-cost: 1115
c ---[ 906]---> BDD-cost: 1187
c ---[ 904]---> BDD-cost: 1117
c ---[ 902]---> BDD-cost: 1075
c ---[ 900]---> BDD-cost: 1167
c ---[ 898]---> BDD-cost: 1017
c ---[ 896]---> BDD-cost: 1079
c ---[ 894]---> BDD-cost: 1179
c ---[ 892]---> BDD-cost: 1191
c ---[ 890]---> BDD-cost: 1181
c ---[ 888]---> BDD-cost: 1171
c ---[ 886]---> BDD-cost: 1189
c ---[ 884]---> BDD-cost: 1177
c ---[ 882]---> BDD-cost: 1159
c ---[ 880]---> BDD-cost: 1181
c ---[ 878]---> BDD-cost: 1169
c ---[ 876]---> BDD-cost: 1167
c ---[ 874]---> BDD-cost: 1027
c ---[ 872]---> BDD-cost: 1093
c ---[ 870]---> BDD-cost: 1195
c ---[ 868]---> BDD-cost: 1169
c ---[ 866]---> BDD-cost: 1173
c ---[ 864]---> BDD-cost: 1171
c ---[ 862]---> BDD-cost: 1151
c ---[ 860]---> BDD-cost: 1173
c ---[ 858]---> BDD-cost: 1155
c ---[ 856]---> BDD-cost: 1173
c ---[ 854]---> BDD-cost: 1171
c ---[ 852]---> BDD-cost: 1145
c ---[ 850]---> BDD-cost: 1177
c ---[ 848]---> BDD-cost: 1179
c ---[ 846]---> BDD-cost: 1173
c ---[ 844]---> BDD-cost: 1173
c ---[ 842]---> BDD-cost: 1173
c ---[ 840]---> BDD-cost: 1187
c ---[ 838]---> BDD-cost: 1169
c ---[ 836]---> BDD-cost: 1055
c ---[ 834]---> BDD-cost: 1121
c ---[ 832]---> BDD-cost: 1171
c ---[ 830]---> BDD-cost: 1173
c ---[ 828]---> BDD-cost: 1177
c ---[ 826]---> BDD-cost: 1169
c ---[ 824]---> BDD-cost: 1171
c ---[ 822]---> BDD-cost: 1173
c ---[ 820]---> BDD-cost: 1169
c ---[ 818]---> BDD-cost: 1201
c ---[ 816]---> BDD-cost: 1173
c ---[ 814]---> BDD-cost: 1097
c ---[ 812]---> BDD-cost: 1171
c ---[ 810]---> BDD-cost: 1161
c ---[ 808]---> BDD-cost: 1187
c ---[ 806]---> BDD-cost: 1131
c ---[ 804]---> BDD-cost: 1173
c ---[ 802]---> BDD-cost: 1175
c ---[ 800]---> BDD-cost: 1171
c ---[ 798]---> BDD-cost: 1171
c ---[ 796]---> BDD-cost: 1169
c ---[ 794]---> BDD-cost: 1169
c ---[ 792]---> BDD-cost: 1165
c ---[ 790]---> BDD-cost: 1177
c ---[ 788]---> BDD-cost: 1157
c ---[ 786]---> BDD-cost: 1179
c ---[ 784]---> BDD-cost: 1129
c ---[ 782]---> BDD-cost: 1173
c ---[ 780]---> BDD-cost: 1175
c ---[ 778]---> BDD-cost: 1179
c ---[ 776]---> BDD-cost: 1173
c ---[ 774]---> BDD-cost: 1115
c ---[ 772]---> BDD-cost: 1071
c ---[ 770]---> BDD-cost: 1167
c ---[ 768]---> BDD-cost: 1187
c ---[ 766]---> BDD-cost: 1173
c ---[ 764]---> BDD-cost: 1091
c ---[ 762]---> BDD-cost: 1169
c ---[ 760]---> BDD-cost: 1025
c ---[ 758]---> BDD-cost: 1073
c ---[ 756]---> BDD-cost: 1167
c ---[ 754]---> BDD-cost: 1077
c ---[ 752]---> BDD-cost: 1197
c ---[ 750]---> BDD-cost: 1189
c ---[ 748]---> BDD-cost: 1197
c ---[ 746]---> BDD-cost: 1131
c ---[ 744]---> BDD-cost: 1115
c ---[ 742]---> BDD-cost: 1189
c ---[ 740]---> BDD-cost: 1177
c ---[ 738]---> BDD-cost: 1167
c ---[ 736]---> BDD-cost: 1175
c ---[ 734]---> BDD-cost: 1181
c ---[ 732]---> BDD-cost: 1171
c ---[ 730]---> BDD-cost: 1171
c ---[ 728]---> BDD-cost: 1189
c ---[ 726]---> BDD-cost: 1191
c ---[ 724]---> BDD-cost: 1103
c ---[ 722]---> BDD-cost: 1183
c ---[ 720]---> BDD-cost: 1151
c ---[ 718]---> BDD-cost: 1103
c ---[ 716]---> BDD-cost: 1171
c ---[ 714]---> BDD-cost: 1183
c ---[ 712]---> BDD-cost: 1171
c ---[ 710]---> BDD-cost: 1179
c ---[ 708]---> BDD-cost: 1173
c ---[ 706]---> BDD-cost: 1073
c ---[ 704]---> BDD-cost: 1191
c ---[ 702]---> BDD-cost: 1175
c ---[ 700]---> BDD-cost: 1139
c ---[ 698]---> BDD-cost: 1171
c ---[ 696]---> BDD-cost: 1173
c ---[ 694]---> BDD-cost: 1163
c ---[ 692]---> BDD-cost: 1173
c ---[ 690]---> BDD-cost: 1175
c ---[ 688]---> BDD-cost: 1189
c ---[ 686]---> BDD-cost: 1173
c ---[ 684]---> BDD-cost: 1173
c ---[ 682]---> BDD-cost: 1071
c ---[ 680]---> BDD-cost: 1179
c ---[ 678]---> BDD-cost: 1125
c ---[ 676]---> BDD-cost: 1171
c ---[ 674]---> BDD-cost: 1057
c ---[ 672]---> BDD-cost: 1189
c ---[ 670]---> BDD-cost: 1107
c ---[ 668]---> BDD-cost: 1159
c ---[ 666]---> BDD-cost: 1175
c ---[ 664]---> BDD-cost: 1063
c ---[ 662]---> BDD-cost: 1173
c ---[ 660]---> BDD-cost: 1171
c ---[ 658]---> BDD-cost: 1171
c ---[ 656]---> BDD-cost: 1165
c ---[ 654]---> BDD-cost: 1165
c ---[ 652]---> BDD-cost: 1171
c ---[ 650]---> BDD-cost: 1077
c ---[ 648]---> BDD-cost: 1069
c ---[ 646]---> BDD-cost: 1175
c ---[ 644]---> BDD-cost: 1159
c ---[ 642]---> BDD-cost: 1097
c ---[ 640]---> BDD-cost: 1175
c ---[ 638]---> BDD-cost:  859
c ---[ 636]---> BDD-cost: 1173
c ---[ 634]---> BDD-cost: 1169
c ---[ 632]---> BDD-cost: 1173
c ---[ 630]---> BDD-cost: 1097
c ---[ 628]---> BDD-cost: 1161
c ---[ 626]---> BDD-cost: 1157
c ---[ 624]---> BDD-cost: 1165
c ---[ 622]---> BDD-cost: 1185
c ---[ 620]---> BDD-cost: 1179
c ---[ 618]---> BDD-cost: 1155
c ---[ 616]---> BDD-cost: 1167
c ---[ 614]---> BDD-cost: 1181
c ---[ 612]---> BDD-cost: 1121
c ---[ 610]---> BDD-cost: 1121
c ---[ 608]---> BDD-cost:  963
c ---[ 606]---> BDD-cost: 1173
c ---[ 604]---> BDD-cost: 1151
c ---[ 602]---> BDD-cost: 1177
c ---[ 600]---> BDD-cost: 1191
c ---[ 598]---> BDD-cost: 1187
c ---[ 596]---> BDD-cost: 1051
c ---[ 594]---> BDD-cost:  987
c ---[ 592]---> BDD-cost: 1173
c ---[ 590]---> BDD-cost: 1175
c ---[ 588]---> BDD-cost: 1173
c ---[ 586]---> BDD-cost: 1121
c ---[ 584]---> BDD-cost: 1157
c ---[ 582]---> BDD-cost: 1173
c ---[ 580]---> BDD-cost: 1175
c ---[ 578]---> BDD-cost: 1181
c ---[ 576]---> BDD-cost: 1079
c ---[ 574]---> BDD-cost:  983
c ---[ 572]---> BDD-cost:  879
c ---[ 570]---> BDD-cost: 1169
c ---[ 568]---> BDD-cost: 1181
c ---[ 566]---> BDD-cost: 1169
c ---[ 564]---> BDD-cost: 1185
c ---[ 562]---> BDD-cost: 1177
c ---[ 560]---> BDD-cost: 1159
c ---[ 558]---> BDD-cost: 1153
c ---[ 556]---> BDD-cost: 1173
c ---[ 554]---> BDD-cost: 1191
c ---[ 552]---> BDD-cost: 1177
c ---[ 550]---> BDD-cost: 1175
c ---[ 548]---> BDD-cost:  887
c ---[ 546]---> BDD-cost: 1191
c ---[ 544]---> BDD-cost: 1155
c ---[ 542]---> BDD-cost: 1169
c ---[ 540]---> BDD-cost: 1127
c ---[ 538]---> BDD-cost: 1179
c ---[ 536]---> BDD-cost: 1189
c ---[ 534]---> BDD-cost: 1171
c ---[ 532]---> BDD-cost: 1167
c ---[ 530]---> BDD-cost: 1171
c ---[ 528]---> BDD-cost: 1175
c ---[ 526]---> BDD-cost:  885
c ---[ 524]---> BDD-cost: 1183
c ---[ 522]---> BDD-cost: 1175
c ---[ 520]---> BDD-cost: 1193
c ---[ 518]---> BDD-cost: 1181
c ---[ 516]---> BDD-cost: 1169
c ---[ 514]---> BDD-cost: 1181
c ---[ 512]---> BDD-cost: 1169
c ---[ 510]---> BDD-cost: 1177
c ---[ 508]---> BDD-cost: 1171
c ---[ 506]---> BDD-cost: 1169
c ---[ 504]---> BDD-cost: 1179
c ---[ 502]---> BDD-cost: 1183
c ---[ 500]---> BDD-cost: 1165
c ---[ 498]---> BDD-cost: 1163
c ---[ 496]---> BDD-cost: 1189
c ---[ 494]---> BDD-cost: 1181
c ---[ 492]---> BDD-cost: 1171
c ---[ 490]---> BDD-cost: 1171
c ---[ 488]---> BDD-cost: 1173
c ---[ 486]---> BDD-cost: 1171
c ---[ 484]---> BDD-cost: 1171
c ---[ 482]---> BDD-cost: 1175
c ---[ 480]---> BDD-cost: 1171
c ---[ 478]---> BDD-cost: 1141
c ---[ 476]---> BDD-cost: 1185
c ---[ 474]---> BDD-cost: 1167
c ---[ 472]---> BDD-cost: 1179
c ---[ 470]---> BDD-cost: 1175
c ---[ 468]---> BDD-cost: 1177
c ---[ 466]---> BDD-cost:  775
c ---[ 464]---> BDD-cost: 1191
c ---[ 462]---> BDD-cost: 1207
c ---[ 460]---> BDD-cost: 1179
c ---[ 458]---> BDD-cost: 1149
c ---[ 456]---> BDD-cost: 1183
c ---[ 454]---> BDD-cost:  787
c ---[ 452]---> BDD-cost: 1173
c ---[ 450]---> BDD-cost: 1169
c ---[ 448]---> BDD-cost: 1131
c ---[ 446]---> BDD-cost: 1129
c ---[ 444]---> BDD-cost: 1167
c ---[ 442]---> BDD-cost: 1177
c ---[ 440]---> BDD-cost: 1185
c ---[ 438]---> BDD-cost: 1185
c ---[ 436]---> BDD-cost: 1189
c ---[ 434]---> BDD-cost: 1169
c ---[ 432]---> BDD-cost: 1113
c ---[ 430]---> BDD-cost: 1167
c ---[ 428]---> BDD-cost: 1181
c ---[ 426]---> BDD-cost: 1171
c ---[ 424]---> BDD-cost: 1191
c ---[ 422]---> BDD-cost: 1181
c ---[ 420]---> BDD-cost: 1169
c ---[ 418]---> BDD-cost: 1137
c ---[ 416]---> BDD-cost: 1159
c ---[ 414]---> BDD-cost: 1169
c ---[ 412]---> BDD-cost: 1175
c ---[ 410]---> BDD-cost: 1167
c ---[ 408]---> BDD-cost: 1195
c ---[ 406]---> BDD-cost: 1169
c ---[ 404]---> BDD-cost: 1171
c ---[ 402]---> BDD-cost: 1177
c ---[ 400]---> BDD-cost: 1147
c ---[ 398]---> BDD-cost: 1171
c ---[ 396]---> BDD-cost: 1173
c ---[ 394]---> BDD-cost:  723
c ---[ 392]---> BDD-cost: 1173
c ---[ 390]---> BDD-cost: 1177
c ---[ 388]---> BDD-cost: 1169
c ---[ 386]---> BDD-cost: 1187
c ---[ 384]---> BDD-cost: 1209
c ---[ 382]---> BDD-cost: 1171
c ---[ 380]---> BDD-cost: 1181
c ---[ 378]---> BDD-cost: 1197
c ---[ 376]---> BDD-cost: 1183
c ---[ 374]---> BDD-cost: 1175
c ---[ 372]---> BDD-cost: 1165
c ---[ 370]---> BDD-cost: 1175
c ---[ 368]---> BDD-cost: 1175
c ---[ 366]---> BDD-cost: 1177
c ---[ 364]---> BDD-cost: 1179
c ---[ 362]---> BDD-cost: 1173
c ---[ 360]---> BDD-cost: 1169
c ---[ 358]---> BDD-cost: 1173
c ---[ 356]---> BDD-cost: 1173
c ---[ 354]---> BDD-cost: 1171
c ---[ 352]---> BDD-cost: 1177
c ---[ 350]---> BDD-cost: 1169
c ---[ 348]---> BDD-cost: 1185
c ---[ 346]---> BDD-cost: 1173
c ---[ 344]---> BDD-cost: 1103
c ---[ 342]---> BDD-cost: 1179
c ---[ 340]---> BDD-cost: 1173
c ---[ 338]---> BDD-cost: 1221
c ---[ 336]---> BDD-cost: 1177
c ---[ 334]---> BDD-cost: 1183
c ---[ 332]---> BDD-cost: 1179
c ---[ 330]---> BDD-cost: 1171
c ---[ 328]---> BDD-cost: 1175
c ---[ 326]---> BDD-cost: 1173
c ---[ 324]---> BDD-cost: 1175
c ---[ 322]---> BDD-cost: 1099
c ---[ 320]---> BDD-cost: 1203
c ---[ 318]---> BDD-cost: 1171
c ---[ 316]---> BDD-cost: 1165
c ---[ 314]---> BDD-cost: 1177
c ---[ 312]---> BDD-cost: 1169
c ---[ 310]---> BDD-cost: 1175
c ---[ 308]---> BDD-cost: 1173
c ---[ 306]---> BDD-cost: 1173
c ---[ 304]---> BDD-cost: 1183
c ---[ 302]---> BDD-cost: 1175
c ---[ 300]---> BDD-cost: 1165
c ---[ 298]---> BDD-cost: 1175
c ---[ 296]---> BDD-cost: 1153
c ---[ 294]---> BDD-cost: 1153
c ---[ 292]---> BDD-cost: 1175
c ---[ 290]---> BDD-cost: 1173
c ---[ 288]---> BDD-cost:  735
c ---[ 286]---> BDD-cost: 1179
c ---[ 284]---> BDD-cost: 1157
c ---[ 282]---> BDD-cost: 1183
c ---[ 280]---> BDD-cost: 1179
c ---[ 278]---> BDD-cost: 1181
c ---[ 276]---> BDD-cost: 1175
c ---[ 274]---> BDD-cost: 1181
c ---[ 272]---> BDD-cost: 1185
c ---[ 270]---> BDD-cost: 1161
c ---[ 268]---> BDD-cost: 1177
c ---[ 266]---> BDD-cost: 1165
c ---[ 264]---> BDD-cost: 1161
c ---[ 262]---> BDD-cost: 1065
c ---[ 260]---> BDD-cost: 1171
c ---[ 258]---> BDD-cost: 1189
c ---[ 256]---> BDD-cost: 1163
c ---[ 254]---> BDD-cost: 1177
c ---[ 252]---> BDD-cost: 1179
c ---[ 250]---> BDD-cost: 1187
c ---[ 248]---> BDD-cost: 1143
c ---[ 246]---> BDD-cost: 1183
c ---[ 244]---> BDD-cost: 1153
c ---[ 242]---> BDD-cost: 1177
c ---[ 240]---> BDD-cost: 1173
c ---[ 238]---> BDD-cost: 1177
c ---[ 236]---> BDD-cost: 1171
c ---[ 234]---> BDD-cost: 1103
c ---[ 232]---> BDD-cost: 1173
c ---[ 230]---> BDD-cost: 1175
c ---[ 228]---> BDD-cost: 1123
c ---[ 226]---> BDD-cost: 1169
c ---[ 224]---> BDD-cost: 1187
c ---[ 222]---> BDD-cost: 1101
c ---[ 220]---> BDD-cost: 1165
c ---[ 218]---> BDD-cost: 1193
c ---[ 216]---> BDD-cost: 1179
c ---[ 214]---> BDD-cost: 1177
c ---[ 212]---> BDD-cost: 1173
c ---[ 210]---> BDD-cost: 1173
c ---[ 208]---> BDD-cost: 1153
c ---[ 206]---> BDD-cost: 1183
c ---[ 204]---> BDD-cost: 1181
c ---[ 202]---> BDD-cost: 1179
c ---[ 200]---> BDD-cost: 1181
c ---[ 198]---> BDD-cost: 1181
c ---[ 196]---> BDD-cost: 1173
c ---[ 194]---> BDD-cost: 1173
c ---[ 192]---> BDD-cost: 1173
c ---[ 190]---> BDD-cost: 1185
c ---[ 188]---> BDD-cost: 1165
c ---[ 186]---> BDD-cost: 1173
c ---[ 184]---> BDD-cost: 1169
c ---[ 182]---> BDD-cost: 1183
c ---[ 180]---> BDD-cost: 1189
c ---[ 178]---> BDD-cost: 1177
c ---[ 176]---> BDD-cost: 1181
c ---[ 174]---> BDD-cost: 1173
c ---[ 172]---> BDD-cost: 1193
c ---[ 170]---> BDD-cost: 1173
c ---[ 168]---> BDD-cost: 1187
c ---[ 166]---> BDD-cost: 1193
c ---[ 164]---> BDD-cost: 1183
c ---[ 162]---> BDD-cost: 1175
c ---[ 160]---> BDD-cost: 1137
c ---[ 158]---> BDD-cost: 1185
c ---[ 156]---> BDD-cost: 1097
c ---[ 154]---> BDD-cost: 1195
c ---[ 152]---> BDD-cost: 1175
c ---[ 150]---> BDD-cost: 1175
c ---[ 148]---> BDD-cost: 1187
c ---[ 146]---> BDD-cost: 1179
c ---[ 144]---> BDD-cost: 1167
c ---[ 142]---> BDD-cost: 1175
c ---[ 140]---> BDD-cost: 1173
c ---[ 138]---> BDD-cost: 1173
c ---[ 136]---> BDD-cost: 1171
c ---[ 134]---> BDD-cost: 1179
c ---[ 132]---> BDD-cost: 1165
c ---[ 130]---> BDD-cost: 1165
c ---[ 128]---> BDD-cost: 1145
c ---[ 126]---> BDD-cost: 1179
c ---[ 124]---> BDD-cost: 1193
c ---[ 122]---> BDD-cost: 1175
c ---[ 120]---> BDD-cost: 1177
c ---[ 118]---> BDD-cost: 1181
c ---[ 116]---> BDD-cost: 1181
c ---[ 114]---> BDD-cost: 1195
c ---[ 112]---> BDD-cost: 1165
c ---[ 110]---> BDD-cost: 1169
c ---[ 108]---> BDD-cost: 1133
c ---[ 106]---> BDD-cost: 1199
c ---[ 104]---> BDD-cost: 1197
c ---[ 102]---> BDD-cost: 1177
c ---[ 100]---> BDD-cost: 1121
c ---[  98]---> BDD-cost: 1143
c ---[  96]---> BDD-cost: 1171
c ---[  94]---> BDD-cost: 1167
c ---[  92]---> BDD-cost: 1175
c ---[  90]---> BDD-cost: 1157
c ---[  88]---> BDD-cost: 1085
c ---[  86]---> BDD-cost: 1167
c ---[  84]---> BDD-cost: 1157
c ---[  82]---> BDD-cost: 1157
c ---[  80]---> BDD-cost: 1175
c ---[  78]---> BDD-cost: 1119
c ---[  76]---> BDD-cost: 1169
c ---[  74]---> BDD-cost: 1177
c ---[  72]---> BDD-cost: 1087
c ---[  70]---> BDD-cost: 1121
c ---[  68]---> BDD-cost: 1171
c ---[  66]---> BDD-cost: 1171
c ---[  64]---> BDD-cost: 1155
c ---[  62]---> BDD-cost: 1173
c ---[  60]---> BDD-cost: 1173
c ---[  58]---> BDD-cost: 1165
c ---[  56]---> BDD-cost: 1169
c ---[  54]---> BDD-cost: 1123
c ---[  52]---> BDD-cost: 1167
c ---[  50]---> BDD-cost: 1073
c ---[  48]---> BDD-cost: 1155
c ---[  46]---> BDD-cost: 1115
c ---[  44]---> BDD-cost: 1171
c ---[  42]---> BDD-cost: 1153
c ---[  40]---> BDD-cost: 1101
c ---[  38]---> BDD-cost: 1065
c ---[  36]---> BDD-cost: 1111
c ---[  34]---> BDD-cost: 1153
c ---[  32]---> BDD-cost: 1061
c ---[  30]---> BDD-cost: 1185
c ---[  28]---> BDD-cost: 1061
c ---[  26]---> BDD-cost: 1173
c ---[  24]---> BDD-cost: 1177
c ---[  22]---> BDD-cost: 1113
c ---[  20]---> BDD-cost: 1151
c ---[  18]---> BDD-cost: 1091
c ---[  16]---> BDD-cost: 1173
c ---[  14]---> BDD-cost: 1137
c ---[  12]---> BDD-cost: 1065
c ---[  10]---> BDD-cost: 1189
c ---[   8]---> BDD-cost: 1169
c ---[   6]---> BDD-cost: 1039
c ---[   4]---> BDD-cost: 1119
c ---[   2]---> BDD-cost: 1147
c ---[   0]---> BDD-cost: 1159
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1593441  4143559 |  531147       0        0     nan |  0.000 % |
c |       100 | 1593441  4143559 |  584261     100     3100    31.0 |  0.077 % |
c |       250 | 1593441  4143559 |  642687     250    15023    60.1 |  0.077 % |
c |       475 | 1593441  4143559 |  706956     475    28709    60.4 |  0.077 % |
c |       812 | 1593441  4143559 |  777652     812    75062    92.4 |  0.077 % |
c |      1329 | 1593441  4143559 |  855417    1329   184901   139.1 |  0.077 % |
c |      2088 | 1593441  4143559 |  940959    2088   283938   136.0 |  0.077 % |
c |      3228 | 1593441  4143559 | 1035055    3228   516925   160.1 |  0.077 % |
c |      4939 | 1593441  4143559 | 1138560    4939   851066   172.3 |  0.077 % |
c |      7501 | 1593441  4143559 | 1252416    7501  1448612   193.1 |  0.077 % |
c |     11345 | 1593441  4143559 | 1377658   11345  2447772   215.8 |  0.077 % |
c |     17111 | 1593441  4143559 | 1515424   17111  3892289   227.5 |  0.077 % |
c |     25761 | 1593441  4143559 | 1666966   25761  5900360   229.0 |  0.077 % |
c |     38735 | 1593441  4143559 | 1833663   38735  9114775   235.3 |  0.077 % |
#### 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.86 0.97 0.95 2/54 6193
Raw data (stat): 6193 (runsolver) R 6192 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488418488 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0028 s]
Raw data (loadavg): 0.88 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 14518 0 0 0 958 40 0 0 25 0 1 0 488418488 60194816 12746 4294967295 134512640 134672761 3221224544 3221212560 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14696 12747 603 41 0 14655 0
vsize: 58784
[startup+20.0096 s]
Raw data (loadavg): 0.90 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 56410 0 0 0 1853 146 0 0 25 0 1 0 488418488 260452352 54606 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63587 54606 603 41 0 63546 0
vsize: 254348
[startup+30.01 s]
Raw data (loadavg): 0.92 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 56796 0 0 0 2852 147 0 0 25 0 1 0 488418488 260587520 54992 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63620 54992 603 41 0 63579 0
vsize: 254480
[startup+40.0106 s]
Raw data (loadavg): 0.93 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 56846 0 0 0 3851 148 0 0 25 0 1 0 488418488 260722688 55042 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63653 55042 603 41 0 63612 0
vsize: 254612
[startup+50.011 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 56896 0 0 0 4851 148 0 0 25 0 1 0 488418488 260993024 55092 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63719 55092 603 41 0 63678 0
vsize: 254876
[startup+60.0111 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 56977 0 0 0 5851 148 0 0 25 0 1 0 488418488 261271552 55173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63787 55173 603 41 0 63746 0
vsize: 255148
[startup+70.0109 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57030 0 0 0 6851 149 0 0 25 0 1 0 488418488 261537792 55226 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63852 55226 603 41 0 63811 0
vsize: 255408
[startup+80.0114 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57079 0 0 0 7851 149 0 0 25 0 1 0 488418488 261668864 55275 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63884 55275 603 41 0 63843 0
vsize: 255536
[startup+90.0115 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57178 0 0 0 8851 149 0 0 25 0 1 0 488418488 262098944 55374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63989 55374 603 41 0 63948 0
vsize: 255956
[startup+100.012 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57270 0 0 0 9851 149 0 0 25 0 1 0 488418488 262369280 55466 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64055 55466 603 41 0 64014 0
vsize: 256220
[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57333 0 0 0 10850 150 0 0 25 0 1 0 488418488 262635520 55529 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64120 55529 603 41 0 64079 0
vsize: 256480
[startup+120.013 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57407 0 0 0 11850 150 0 0 25 0 1 0 488418488 262905856 55603 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64186 55603 603 41 0 64145 0
vsize: 256744
[startup+130.014 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57488 0 0 0 12850 150 0 0 25 0 1 0 488418488 263335936 55684 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64291 55684 603 41 0 64250 0
vsize: 257164
[startup+140.013 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57554 0 0 0 13850 150 0 0 25 0 1 0 488418488 263606272 55750 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64357 55750 603 41 0 64316 0
vsize: 257428
[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57658 0 0 0 14850 151 0 0 25 0 1 0 488418488 264015872 55854 4294967295 134512640 134672761 3221224544 3221223692 1074733099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64457 55854 603 41 0 64416 0
vsize: 257828
[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57705 0 0 0 15850 151 0 0 25 0 1 0 488418488 264151040 55901 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64490 55901 603 41 0 64449 0
vsize: 257960
[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57795 0 0 0 16849 151 0 0 25 0 1 0 488418488 264564736 55991 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64591 55991 603 41 0 64550 0
vsize: 258364
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57865 0 0 0 17849 152 0 0 25 0 1 0 488418488 264835072 56061 4294967295 134512640 134672761 3221224544 3221223648 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64657 56061 603 41 0 64616 0
vsize: 258628
[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 57951 0 0 0 18849 152 0 0 25 0 1 0 488418488 265105408 56147 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64723 56147 603 41 0 64682 0
vsize: 258892
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58040 0 0 0 19849 152 0 0 25 0 1 0 488418488 265515008 56236 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64823 56236 603 41 0 64782 0
vsize: 259292
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58143 0 0 0 20849 153 0 0 25 0 1 0 488418488 265932800 56339 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64925 56339 603 41 0 64884 0
vsize: 259700
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58222 0 0 0 21849 153 0 0 25 0 1 0 488418488 266207232 56418 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64992 56418 603 41 0 64951 0
vsize: 259968
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58285 0 0 0 22849 153 0 0 25 0 1 0 488418488 266477568 56481 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65058 56481 603 41 0 65017 0
vsize: 260232
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58359 0 0 0 23849 153 0 0 25 0 1 0 488418488 266883072 56555 4294967295 134512640 134672761 3221224544 3221223716 134553588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65157 56555 603 41 0 65116 0
vsize: 260628
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58427 0 0 0 24849 153 0 0 25 0 1 0 488418488 267153408 56623 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65223 56623 603 41 0 65182 0
vsize: 260892
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58506 0 0 0 25849 154 0 0 25 0 1 0 488418488 267423744 56702 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65289 56702 603 41 0 65248 0
vsize: 261156
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58594 0 0 0 26849 154 0 0 25 0 1 0 488418488 267694080 56790 4294967295 134512640 134672761 3221224544 3221223648 134559969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65355 56790 603 41 0 65314 0
vsize: 261420
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58690 0 0 0 27849 154 0 0 25 0 1 0 488418488 268103680 56886 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65455 56886 603 41 0 65414 0
vsize: 261820
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58785 0 0 0 28849 155 0 0 25 0 1 0 488418488 268509184 56981 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65554 56981 603 41 0 65513 0
vsize: 262216
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 58898 0 0 0 29849 155 0 0 25 0 1 0 488418488 268914688 57094 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65653 57094 603 41 0 65612 0
vsize: 262612
[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59016 0 0 0 30849 155 0 0 25 0 1 0 488418488 269197312 57212 4294967295 134512640 134672761 3221224544 3221223744 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65722 57212 603 41 0 65681 0
vsize: 262888
[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59107 0 0 0 31849 155 0 0 25 0 1 0 488418488 269602816 57303 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65821 57303 603 41 0 65780 0
vsize: 263284
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59218 0 0 0 32849 156 0 0 25 0 1 0 488418488 270024704 57414 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65924 57414 603 41 0 65883 0
vsize: 263696
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59308 0 0 0 33849 156 0 0 25 0 1 0 488418488 270426112 57504 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66022 57504 603 41 0 65981 0
vsize: 264088
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59418 0 0 0 34848 156 0 0 25 0 1 0 488418488 270852096 57614 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66126 57614 603 41 0 66085 0
vsize: 264504
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59527 0 0 0 35848 157 0 0 25 0 1 0 488418488 271261696 57723 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66226 57723 603 41 0 66185 0
vsize: 264904
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59580 0 0 0 36847 157 0 0 25 0 1 0 488418488 271532032 57776 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66292 57776 603 41 0 66251 0
vsize: 265168
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59635 0 0 0 37848 157 0 0 25 0 1 0 488418488 271798272 57831 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66357 57831 603 41 0 66316 0
vsize: 265428
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59705 0 0 0 38848 157 0 0 25 0 1 0 488418488 272068608 57901 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66423 57901 603 41 0 66382 0
vsize: 265692
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59772 0 0 0 39848 157 0 0 25 0 1 0 488418488 272338944 57968 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66489 57968 603 41 0 66448 0
vsize: 265956
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59824 0 0 0 40848 157 0 0 25 0 1 0 488418488 272474112 58020 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66522 58020 603 41 0 66481 0
vsize: 266088
[startup+420.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59889 0 0 0 41848 157 0 0 25 0 1 0 488418488 272744448 58085 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66588 58085 603 41 0 66547 0
vsize: 266352
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 59957 0 0 0 42848 157 0 0 25 0 1 0 488418488 273014784 58153 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66654 58153 603 41 0 66613 0
vsize: 266616
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60059 0 0 0 43848 158 0 0 25 0 1 0 488418488 273420288 58255 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66753 58255 603 41 0 66712 0
vsize: 267012
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60127 0 0 0 44848 158 0 0 25 0 1 0 488418488 273690624 58323 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66819 58323 603 41 0 66778 0
vsize: 267276
[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60198 0 0 0 45848 158 0 0 25 0 1 0 488418488 274096128 58394 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66918 58394 603 41 0 66877 0
vsize: 267672
[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60271 0 0 0 46848 158 0 0 25 0 1 0 488418488 274362368 58467 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66983 58467 603 41 0 66942 0
vsize: 267932
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60404 0 0 0 47848 158 0 0 25 0 1 0 488418488 274952192 58600 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67127 58600 603 41 0 67086 0
vsize: 268508
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60491 0 0 0 48848 159 0 0 25 0 1 0 488418488 275234816 58687 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67196 58687 603 41 0 67155 0
vsize: 268784
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60572 0 0 0 49848 159 0 0 25 0 1 0 488418488 275693568 58768 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67308 58768 603 41 0 67267 0
vsize: 269232
[startup+510.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60659 0 0 0 50849 159 0 0 25 0 1 0 488418488 275963904 58855 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67374 58855 603 41 0 67333 0
vsize: 269496
[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60754 0 0 0 51849 159 0 0 25 0 1 0 488418488 276373504 58950 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67474 58950 603 41 0 67433 0
vsize: 269896
[startup+530.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60836 0 0 0 52848 160 0 0 25 0 1 0 488418488 276647936 59032 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67541 59032 603 41 0 67500 0
vsize: 270164
[startup+540.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60919 0 0 0 53848 160 0 0 25 0 1 0 488418488 277049344 59115 4294967295 134512640 134672761 3221224544 3221223712 134564457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67639 59115 603 41 0 67598 0
vsize: 270556
[startup+550.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 60978 0 0 0 54848 160 0 0 25 0 1 0 488418488 277319680 59174 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67705 59174 603 41 0 67664 0
vsize: 270820
[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61026 0 0 0 55848 160 0 0 25 0 1 0 488418488 277454848 59222 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67738 59222 603 41 0 67697 0
vsize: 270952
[startup+570.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61098 0 0 0 56848 160 0 0 25 0 1 0 488418488 277725184 59294 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67804 59294 603 41 0 67763 0
vsize: 271216
[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61162 0 0 0 57848 161 0 0 25 0 1 0 488418488 277995520 59358 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67870 59358 603 41 0 67829 0
vsize: 271480
[startup+590.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61257 0 0 0 58848 161 0 0 25 0 1 0 488418488 278413312 59453 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67972 59453 603 41 0 67931 0
vsize: 271888
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61337 0 0 0 59848 161 0 0 25 0 1 0 488418488 278691840 59533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68040 59533 603 41 0 67999 0
vsize: 272160
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61427 0 0 0 60848 161 0 0 25 0 1 0 488418488 279101440 59623 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68140 59623 603 41 0 68099 0
vsize: 272560
[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61520 0 0 0 61848 162 0 0 25 0 1 0 488418488 279506944 59716 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68239 59716 603 41 0 68198 0
vsize: 272956
[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61611 0 0 0 62848 162 0 0 25 0 1 0 488418488 279920640 59807 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68340 59807 603 41 0 68299 0
vsize: 273360
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61730 0 0 0 63848 162 0 0 25 0 1 0 488418488 280326144 59926 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68439 59926 603 41 0 68398 0
vsize: 273756
[startup+650.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61833 0 0 0 64848 162 0 0 25 0 1 0 488418488 280756224 60029 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68544 60029 603 41 0 68503 0
vsize: 274176
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 61922 0 0 0 65848 162 0 0 25 0 1 0 488418488 281169920 60118 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68645 60118 603 41 0 68604 0
vsize: 274580
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62006 0 0 0 66848 163 0 0 25 0 1 0 488418488 281440256 60202 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68711 60202 603 41 0 68670 0
vsize: 274844
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 6193
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62085 0 0 0 67848 163 0 0 25 0 1 0 488418488 281845760 60281 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68810 60281 603 41 0 68769 0
vsize: 275240
[startup+690.038 s]
Raw data (loadavg): 1.07 0.99 0.96 3/58 6238
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62130 0 0 0 68845 165 0 0 25 0 1 0 488418488 281980928 60326 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68843 60326 603 41 0 68802 0
vsize: 275372
[startup+700.038 s]
Raw data (loadavg): 1.06 0.99 0.96 2/54 6246
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62194 0 0 0 69845 166 0 0 25 0 1 0 488418488 282251264 60390 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68909 60390 603 41 0 68868 0
vsize: 275636
[startup+710.039 s]
Raw data (loadavg): 1.05 0.99 0.96 2/54 6246
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62281 0 0 0 70845 167 0 0 25 0 1 0 488418488 282660864 60477 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69009 60477 603 41 0 68968 0
vsize: 276036
[startup+720.039 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 6246
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62364 0 0 0 71844 168 0 0 25 0 1 0 488418488 282931200 60560 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69075 60560 603 41 0 69034 0
vsize: 276300
[startup+730.039 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 6246
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62435 0 0 0 72843 168 0 0 25 0 1 0 488418488 283197440 60631 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69140 60631 603 41 0 69099 0
vsize: 276560
[startup+740.039 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 6246
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62505 0 0 0 73843 169 0 0 25 0 1 0 488418488 283467776 60701 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69206 60701 603 41 0 69165 0
vsize: 276824
[startup+750.039 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 6246
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62609 0 0 0 74843 169 0 0 25 0 1 0 488418488 283877376 60805 4294967295 134512640 134672761 3221224544 3221223728 134558756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69306 60805 603 41 0 69265 0
vsize: 277224
[startup+760.039 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62698 0 0 0 75842 170 0 0 25 0 1 0 488418488 284286976 60894 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69406 60895 603 41 0 69365 0
vsize: 277624
[startup+770.039 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62770 0 0 0 76842 170 0 0 25 0 1 0 488418488 284557312 60966 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69472 60966 603 41 0 69431 0
vsize: 277888
[startup+780.039 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62860 0 0 0 77842 170 0 0 25 0 1 0 488418488 284983296 61056 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69576 61056 603 41 0 69535 0
vsize: 278304
[startup+790.039 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62913 0 0 0 78842 171 0 0 25 0 1 0 488418488 285118464 61109 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69609 61109 603 41 0 69568 0
vsize: 278436
[startup+800.04 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 62998 0 0 0 79842 171 0 0 25 0 1 0 488418488 285532160 61194 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69710 61194 603 41 0 69669 0
vsize: 278840
[startup+810.041 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63079 0 0 0 80841 172 0 0 25 0 1 0 488418488 285806592 61275 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69777 61275 603 41 0 69736 0
vsize: 279108
[startup+820.041 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63159 0 0 0 81841 172 0 0 25 0 1 0 488418488 286212096 61355 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69876 61355 603 41 0 69835 0
vsize: 279504
[startup+830.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63280 0 0 0 82840 173 0 0 25 0 1 0 488418488 286617600 61476 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69975 61476 603 41 0 69934 0
vsize: 279900
[startup+840.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63351 0 0 0 83840 173 0 0 25 0 1 0 488418488 287027200 61547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70075 61547 603 41 0 70034 0
vsize: 280300
[startup+850.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63410 0 0 0 84840 174 0 0 25 0 1 0 488418488 287162368 61606 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70108 61606 603 41 0 70067 0
vsize: 280432
[startup+860.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63477 0 0 0 85840 174 0 0 25 0 1 0 488418488 287428608 61673 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70173 61673 603 41 0 70132 0
vsize: 280692
[startup+870.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63534 0 0 0 86840 174 0 0 25 0 1 0 488418488 287707136 61730 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70241 61730 603 41 0 70200 0
vsize: 280964
[startup+880.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63608 0 0 0 87839 175 0 0 25 0 1 0 488418488 287977472 61804 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70307 61804 603 41 0 70266 0
vsize: 281228
[startup+890.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63666 0 0 0 88839 176 0 0 25 0 1 0 488418488 288243712 61862 4294967295 134512640 134672761 3221224544 3221223744 134557892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70372 61862 603 41 0 70331 0
vsize: 281488
[startup+900.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63752 0 0 0 89839 176 0 0 25 0 1 0 488418488 288649216 61948 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70471 61948 603 41 0 70430 0
vsize: 281884
[startup+910.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63820 0 0 0 90838 177 0 0 25 0 1 0 488418488 288919552 62016 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70537 62016 603 41 0 70496 0
vsize: 282148
[startup+920.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63886 0 0 0 91838 177 0 0 25 0 1 0 488418488 289189888 62082 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70603 62082 603 41 0 70562 0
vsize: 282412
[startup+930.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 63999 0 0 0 92838 178 0 0 25 0 1 0 488418488 289595392 62195 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70702 62195 603 41 0 70661 0
vsize: 282808
[startup+940.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64089 0 0 0 93837 178 0 0 25 0 1 0 488418488 289996800 62285 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70800 62285 603 41 0 70759 0
vsize: 283200
[startup+950.041 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64222 0 0 0 94837 179 0 0 25 0 1 0 488418488 290541568 62418 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70933 62418 603 41 0 70892 0
vsize: 283732
[startup+960.042 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64307 0 0 0 95837 179 0 0 25 0 1 0 488418488 290811904 62503 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70999 62503 603 41 0 70958 0
vsize: 283996
[startup+970.042 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64383 0 0 0 96836 180 0 0 25 0 1 0 488418488 291217408 62579 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71098 62579 603 41 0 71057 0
vsize: 284392
[startup+980.042 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64469 0 0 0 97836 180 0 0 25 0 1 0 488418488 291483648 62665 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71163 62665 603 41 0 71122 0
vsize: 284652
[startup+990.042 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64550 0 0 0 98835 181 0 0 25 0 1 0 488418488 291897344 62746 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71264 62746 603 41 0 71223 0
vsize: 285056
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64663 0 0 0 99835 181 0 0 25 0 1 0 488418488 292302848 62859 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71363 62859 603 41 0 71322 0
vsize: 285452
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64731 0 0 0 100835 182 0 0 25 0 1 0 488418488 292696064 62927 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71459 62927 603 41 0 71418 0
vsize: 285836
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6248
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64815 0 0 0 101835 182 0 0 25 0 1 0 488418488 293105664 63011 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71559 63011 603 41 0 71518 0
vsize: 286236
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64887 0 0 0 102834 182 0 0 25 0 1 0 488418488 293371904 63083 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71624 63083 603 41 0 71583 0
vsize: 286496
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 64964 0 0 0 103834 183 0 0 25 0 1 0 488418488 293634048 63160 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71688 63160 603 41 0 71647 0
vsize: 286752
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65073 0 0 0 104834 183 0 0 25 0 1 0 488418488 294072320 63269 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71795 63269 603 41 0 71754 0
vsize: 287180
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65150 0 0 0 105833 184 0 0 25 0 1 0 488418488 294481920 63346 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71895 63346 603 41 0 71854 0
vsize: 287580
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65227 0 0 0 106833 185 0 0 25 0 1 0 488418488 294752256 63423 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71961 63423 603 41 0 71920 0
vsize: 287844
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65283 0 0 0 107833 185 0 0 25 0 1 0 488418488 295022592 63479 4294967295 134512640 134672761 3221224544 3221223648 134559974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72027 63479 603 41 0 71986 0
vsize: 288108
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65354 0 0 0 108832 186 0 0 25 0 1 0 488418488 295292928 63550 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72093 63550 603 41 0 72052 0
vsize: 288372
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65421 0 0 0 109832 186 0 0 25 0 1 0 488418488 295563264 63617 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72159 63617 603 41 0 72118 0
vsize: 288636
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65508 0 0 0 110832 187 0 0 25 0 1 0 488418488 295825408 63704 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72223 63704 603 41 0 72182 0
vsize: 288892
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65602 0 0 0 111832 187 0 0 25 0 1 0 488418488 296243200 63798 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72325 63798 603 41 0 72284 0
vsize: 289300
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65686 0 0 0 112831 188 0 0 25 0 1 0 488418488 296656896 63882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72426 63882 603 41 0 72385 0
vsize: 289704
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65786 0 0 0 113831 188 0 0 25 0 1 0 488418488 297062400 63982 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72525 63982 603 41 0 72484 0
vsize: 290100
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65861 0 0 0 114831 189 0 0 25 0 1 0 488418488 297328640 64057 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72590 64057 603 41 0 72549 0
vsize: 290360
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 65938 0 0 0 115830 189 0 0 25 0 1 0 488418488 297594880 64134 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72655 64134 603 41 0 72614 0
vsize: 290620
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 66004 0 0 0 116829 190 0 0 25 0 1 0 488418488 297865216 64200 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72721 64200 603 41 0 72680 0
vsize: 290884
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 66142 0 0 0 117829 191 0 0 25 0 1 0 488418488 298545152 64338 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72887 64338 603 41 0 72846 0
vsize: 291548
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 66219 0 0 0 118829 191 0 0 25 0 1 0 488418488 298819584 64415 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72954 64415 603 41 0 72913 0
vsize: 291816
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 6250
Raw data (stat): 6193 (minisat+) R 6192 32461 32460 0 -1 0 66290 0 0 0 119828 192 0 0 25 0 1 0 488418488 299089920 64486 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73020 64486 603 41 0 72979 0
vsize: 292080
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.96 1/54 6250
Raw data (stat): 6193 (minisat+) Z 6192 32461 32460 0 -1 12 66292 0 0 0 119828 204 0 0 25 0 1 0 488418488 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.17
CPU time (s): 1200.34
CPU user time (s): 1198.29
CPU system time (s): 2.04669
CPU usage (%): 100.013
Max. virtual memory (Kb): 292080
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####