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-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.18
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 21510

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-22 00:07:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13070 boxname=wulflinc23 idbench=1006 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  bc46e72682d969c09e6f4028df473a45  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-t1717.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-t1717.opb
IDLAUNCH: 13070
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        615192 kB
Buffers:         22236 kB
Cached:         372772 kB
SwapCached:        548 kB
Active:          87500 kB
Inactive:       309516 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        614940 kB
SwapTotal:     2097136 kB
SwapFree:      2095732 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5104 kB
Slab:            16804 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:28:01 (client local time) WITH STATUS 0 IN 1200.4 SECONDS
stats: 13070 7 1200.4 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 % |
#### 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.56 0.81 0.86 2/54 17690
Raw data (stat): 17690 (runsolver) R 17689 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549278409 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.63 0.82 0.86 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 14525 0 0 0 960 39 0 0 25 0 1 0 549278409 66486272 12753 4294967295 134512640 134672761 3221224624 3221194768 1075787145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16232 12753 603 41 0 16191 0
vsize: 64928
[startup+20.0014 s]
Raw data (loadavg): 0.68 0.82 0.86 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 56410 0 0 0 1857 142 0 0 25 0 1 0 549278409 260452352 54606 4294967295 134512640 134672761 3221224624 3221223792 134560869 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.0024 s]
Raw data (loadavg): 0.73 0.83 0.86 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 56794 0 0 0 2856 143 0 0 25 0 1 0 549278409 260587520 54990 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63620 54990 603 41 0 63579 0
vsize: 254480
[startup+40.0015 s]
Raw data (loadavg): 0.77 0.83 0.86 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 56845 0 0 0 3856 143 0 0 25 0 1 0 549278409 260722688 55041 4294967295 134512640 134672761 3221224624 3221223772 1074733103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63653 55041 603 41 0 63612 0
vsize: 254612
[startup+50.0022 s]
Raw data (loadavg): 0.81 0.84 0.86 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 56886 0 0 0 4855 144 0 0 25 0 1 0 549278409 260857856 55082 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63686 55082 603 41 0 63645 0
vsize: 254744
[startup+60.0026 s]
Raw data (loadavg): 0.84 0.84 0.86 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 56973 0 0 0 5855 144 0 0 25 0 1 0 549278409 261271552 55169 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63787 55169 603 41 0 63746 0
vsize: 255148
[startup+70.0035 s]
Raw data (loadavg): 0.86 0.85 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57027 0 0 0 6855 145 0 0 25 0 1 0 549278409 261537792 55223 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63852 55223 603 41 0 63811 0
vsize: 255408
[startup+80.0062 s]
Raw data (loadavg): 0.88 0.85 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57067 0 0 0 7855 145 0 0 25 0 1 0 549278409 261668864 55263 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63884 55263 603 41 0 63843 0
vsize: 255536
[startup+90.0062 s]
Raw data (loadavg): 0.90 0.86 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57166 0 0 0 8855 146 0 0 25 0 1 0 549278409 262098944 55362 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63989 55362 603 41 0 63948 0
vsize: 255956
[startup+100.006 s]
Raw data (loadavg): 0.91 0.86 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57255 0 0 0 9854 146 0 0 25 0 1 0 549278409 262369280 55451 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64055 55451 603 41 0 64014 0
vsize: 256220
[startup+110.007 s]
Raw data (loadavg): 0.93 0.86 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57318 0 0 0 10853 147 0 0 25 0 1 0 549278409 262635520 55514 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64120 55514 603 41 0 64079 0
vsize: 256480
[startup+120.008 s]
Raw data (loadavg): 0.94 0.87 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57380 0 0 0 11853 147 0 0 25 0 1 0 549278409 262770688 55576 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64153 55576 603 41 0 64112 0
vsize: 256612
[startup+130.008 s]
Raw data (loadavg): 0.95 0.87 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57470 0 0 0 12853 147 0 0 25 0 1 0 549278409 263188480 55666 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64255 55666 603 41 0 64214 0
vsize: 257020
[startup+140.017 s]
Raw data (loadavg): 0.95 0.88 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57530 0 0 0 13854 148 0 0 25 0 1 0 549278409 263471104 55726 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64324 55726 603 41 0 64283 0
vsize: 257296
[startup+150.017 s]
Raw data (loadavg): 0.96 0.88 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57607 0 0 0 14853 149 0 0 25 0 1 0 549278409 263745536 55803 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64391 55803 603 41 0 64350 0
vsize: 257564
[startup+160.016 s]
Raw data (loadavg): 0.97 0.88 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57690 0 0 0 15852 149 0 0 25 0 1 0 549278409 264151040 55886 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64490 55886 603 41 0 64449 0
vsize: 257960
[startup+170.018 s]
Raw data (loadavg): 0.97 0.89 0.87 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57744 0 0 0 16852 150 0 0 25 0 1 0 549278409 264286208 55940 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64523 55940 603 41 0 64482 0
vsize: 258092
[startup+180.019 s]
Raw data (loadavg): 0.98 0.89 0.88 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57829 0 0 0 17852 150 0 0 25 0 1 0 549278409 264699904 56025 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64624 56025 603 41 0 64583 0
vsize: 258496
[startup+190.018 s]
Raw data (loadavg): 0.98 0.89 0.88 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57915 0 0 0 18852 150 0 0 25 0 1 0 549278409 264970240 56111 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64690 56111 603 41 0 64649 0
vsize: 258760
[startup+200.019 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 57995 0 0 0 19851 151 0 0 25 0 1 0 549278409 265379840 56191 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64790 56191 603 41 0 64749 0
vsize: 259160
[startup+210.019 s]
Raw data (loadavg): 0.98 0.90 0.88 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58093 0 0 0 20850 152 0 0 25 0 1 0 549278409 265785344 56289 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64889 56289 603 41 0 64848 0
vsize: 259556
[startup+220.02 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58173 0 0 0 21849 153 0 0 25 0 1 0 549278409 266067968 56369 4294967295 134512640 134672761 3221224624 3221223728 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64958 56369 603 41 0 64917 0
vsize: 259832
[startup+230.02 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58261 0 0 0 22849 154 0 0 25 0 1 0 549278409 266477568 56457 4294967295 134512640 134672761 3221224624 3221223772 1074733103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65058 56457 603 41 0 65017 0
vsize: 260232
[startup+240.02 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58314 0 0 0 23849 154 0 0 25 0 1 0 549278409 266612736 56510 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65091 56510 603 41 0 65050 0
vsize: 260364
[startup+250.02 s]
Raw data (loadavg): 1.14 0.94 0.89 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58377 0 0 0 24849 154 0 0 25 0 1 0 549278409 266883072 56573 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65157 56573 603 41 0 65116 0
vsize: 260628
[startup+260.02 s]
Raw data (loadavg): 1.12 0.94 0.89 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58458 0 0 0 25848 154 0 0 25 0 1 0 549278409 267288576 56654 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65256 56654 603 41 0 65215 0
vsize: 261024
[startup+270.021 s]
Raw data (loadavg): 1.10 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58544 0 0 0 26849 154 0 0 25 0 1 0 549278409 267558912 56740 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65322 56740 603 41 0 65281 0
vsize: 261288
[startup+280.021 s]
Raw data (loadavg): 1.09 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58624 0 0 0 27849 154 0 0 25 0 1 0 549278409 267833344 56820 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65389 56820 603 41 0 65348 0
vsize: 261556
[startup+290.021 s]
Raw data (loadavg): 1.07 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58710 0 0 0 28848 155 0 0 25 0 1 0 549278409 268103680 56906 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65455 56906 603 41 0 65414 0
vsize: 261820
[startup+300.036 s]
Raw data (loadavg): 1.06 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58816 0 0 0 29849 156 0 0 25 0 1 0 549278409 268644352 57012 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65587 57012 603 41 0 65546 0
vsize: 262348
[startup+310.036 s]
Raw data (loadavg): 1.05 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 58940 0 0 0 30849 156 0 0 25 0 1 0 549278409 268914688 57136 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65653 57136 603 41 0 65612 0
vsize: 262612
[startup+320.036 s]
Raw data (loadavg): 1.04 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59028 0 0 0 31849 157 0 0 25 0 1 0 549278409 269197312 57224 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65722 57224 603 41 0 65681 0
vsize: 262888
[startup+330.043 s]
Raw data (loadavg): 1.04 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59112 0 0 0 32850 157 0 0 25 0 1 0 549278409 269602816 57308 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65821 57308 603 41 0 65780 0
vsize: 263284
[startup+340.043 s]
Raw data (loadavg): 1.03 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59227 0 0 0 33850 157 0 0 25 0 1 0 549278409 270024704 57423 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65924 57423 603 41 0 65883 0
vsize: 263696
[startup+350.049 s]
Raw data (loadavg): 1.02 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59314 0 0 0 34850 157 0 0 25 0 1 0 549278409 270426112 57510 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66022 57510 603 41 0 65981 0
vsize: 264088
[startup+360.056 s]
Raw data (loadavg): 1.02 0.95 0.90 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59429 0 0 0 35850 158 0 0 25 0 1 0 549278409 270852096 57625 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66126 57625 603 41 0 66085 0
vsize: 264504
[startup+370.057 s]
Raw data (loadavg): 1.02 0.95 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59527 0 0 0 36848 159 0 0 25 0 1 0 549278409 271261696 57723 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66226 57723 603 41 0 66185 0
vsize: 264904
[startup+380.056 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59580 0 0 0 37849 159 0 0 25 0 1 0 549278409 271532032 57776 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66292 57776 603 41 0 66251 0
vsize: 265168
[startup+390.056 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59634 0 0 0 38848 160 0 0 25 0 1 0 549278409 271798272 57830 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66357 57830 603 41 0 66316 0
vsize: 265428
[startup+400.055 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59697 0 0 0 39848 160 0 0 25 0 1 0 549278409 271933440 57893 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66390 57893 603 41 0 66349 0
vsize: 265560
[startup+410.055 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59761 0 0 0 40848 160 0 0 25 0 1 0 549278409 272203776 57957 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66456 57957 603 41 0 66415 0
vsize: 265824
[startup+420.056 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59817 0 0 0 41848 160 0 0 25 0 1 0 549278409 272474112 58013 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66522 58013 603 41 0 66481 0
vsize: 266088
[startup+430.057 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59880 0 0 0 42848 161 0 0 25 0 1 0 549278409 272744448 58076 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66588 58076 603 41 0 66547 0
vsize: 266352
[startup+440.056 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 59947 0 0 0 43848 161 0 0 25 0 1 0 549278409 273014784 58143 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66654 58143 603 41 0 66613 0
vsize: 266616
[startup+450.056 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60051 0 0 0 44847 161 0 0 25 0 1 0 549278409 273420288 58247 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66753 58247 603 41 0 66712 0
vsize: 267012
[startup+460.055 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60109 0 0 0 45847 161 0 0 25 0 1 0 549278409 273690624 58305 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66819 58305 603 41 0 66778 0
vsize: 267276
[startup+470.056 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60177 0 0 0 46848 162 0 0 25 0 1 0 549278409 273960960 58373 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66885 58373 603 41 0 66844 0
vsize: 267540
[startup+480.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60243 0 0 0 47848 162 0 0 25 0 1 0 549278409 274231296 58439 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66951 58439 603 41 0 66910 0
vsize: 267804
[startup+490.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60348 0 0 0 48847 162 0 0 25 0 1 0 549278409 274669568 58544 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67058 58544 603 41 0 67017 0
vsize: 268232
[startup+500.062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60461 0 0 0 49848 162 0 0 25 0 1 0 549278409 275099648 58657 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67163 58657 603 41 0 67122 0
vsize: 268652
[startup+510.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60532 0 0 0 50848 163 0 0 25 0 1 0 549278409 275369984 58728 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67229 58728 603 41 0 67188 0
vsize: 268916
[startup+520.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60606 0 0 0 51848 163 0 0 25 0 1 0 549278409 275828736 58802 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67341 58802 603 41 0 67300 0
vsize: 269364
[startup+530.064 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60696 0 0 0 52848 163 0 0 25 0 1 0 549278409 276099072 58892 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67407 58892 603 41 0 67366 0
vsize: 269628
[startup+540.065 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60813 0 0 0 53847 164 0 0 25 0 1 0 549278409 276647936 59009 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67541 59009 603 41 0 67500 0
vsize: 270164
[startup+550.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60875 0 0 0 54847 164 0 0 25 0 1 0 549278409 276918272 59071 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67607 59071 603 41 0 67566 0
vsize: 270428
[startup+560.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60943 0 0 0 55848 164 0 0 25 0 1 0 549278409 277184512 59139 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67672 59139 603 41 0 67631 0
vsize: 270688
[startup+570.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 60994 0 0 0 56848 165 0 0 25 0 1 0 549278409 277319680 59190 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67705 59190 603 41 0 67664 0
vsize: 270820
[startup+580.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61050 0 0 0 57848 165 0 0 25 0 1 0 549278409 277590016 59246 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67771 59246 603 41 0 67730 0
vsize: 271084
[startup+590.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61109 0 0 0 58848 165 0 0 25 0 1 0 549278409 277860352 59305 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67837 59305 603 41 0 67796 0
vsize: 271348
[startup+600.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61200 0 0 0 59848 165 0 0 25 0 1 0 549278409 278138880 59396 4294967295 134512640 134672761 3221224624 3221223728 134560150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67905 59396 603 41 0 67864 0
vsize: 271620
[startup+610.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61272 0 0 0 60848 165 0 0 25 0 1 0 549278409 278548480 59468 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68005 59468 603 41 0 67964 0
vsize: 272020
[startup+620.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61352 0 0 0 61848 166 0 0 25 0 1 0 549278409 278827008 59548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68073 59548 603 41 0 68032 0
vsize: 272292
[startup+630.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61433 0 0 0 62848 166 0 0 25 0 1 0 549278409 279101440 59629 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68140 59629 603 41 0 68099 0
vsize: 272560
[startup+640.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61540 0 0 0 63847 166 0 0 25 0 1 0 549278409 279646208 59736 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68273 59736 603 41 0 68232 0
vsize: 273092
[startup+650.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61612 0 0 0 64847 167 0 0 25 0 1 0 549278409 279920640 59808 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68340 59808 603 41 0 68299 0
vsize: 273360
[startup+660.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61730 0 0 0 65846 168 0 0 25 0 1 0 549278409 280326144 59926 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68439 59926 603 41 0 68398 0
vsize: 273756
[startup+670.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61833 0 0 0 66846 168 0 0 25 0 1 0 549278409 280756224 60029 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68544 60029 603 41 0 68503 0
vsize: 274176
[startup+680.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 61917 0 0 0 67846 168 0 0 25 0 1 0 549278409 281169920 60113 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68645 60113 603 41 0 68604 0
vsize: 274580
[startup+690.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62002 0 0 0 68846 168 0 0 25 0 1 0 549278409 281440256 60198 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68711 60198 603 41 0 68670 0
vsize: 274844
[startup+700.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62079 0 0 0 69846 168 0 0 25 0 1 0 549278409 281710592 60275 4294967295 134512640 134672761 3221224624 3221223748 134566062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68777 60275 603 41 0 68736 0
vsize: 275108
[startup+710.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62124 0 0 0 70846 169 0 0 25 0 1 0 549278409 281980928 60320 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68843 60320 603 41 0 68802 0
vsize: 275372
[startup+720.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62179 0 0 0 71846 169 0 0 25 0 1 0 549278409 282116096 60375 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68876 60375 603 41 0 68835 0
vsize: 275504
[startup+730.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62268 0 0 0 72846 169 0 0 25 0 1 0 549278409 282525696 60464 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68976 60464 603 41 0 68935 0
vsize: 275904
[startup+740.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62339 0 0 0 73846 170 0 0 25 0 1 0 549278409 282796032 60535 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69042 60535 603 41 0 69001 0
vsize: 276168
[startup+750.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62414 0 0 0 74846 170 0 0 25 0 1 0 549278409 283197440 60610 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69140 60610 603 41 0 69099 0
vsize: 276560
[startup+760.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62481 0 0 0 75846 170 0 0 25 0 1 0 549278409 283467776 60677 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69206 60677 603 41 0 69165 0
vsize: 276824
[startup+770.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62563 0 0 0 76846 170 0 0 25 0 1 0 549278409 283742208 60759 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69273 60759 603 41 0 69232 0
vsize: 277092
[startup+780.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62677 0 0 0 77845 171 0 0 25 0 1 0 549278409 284151808 60873 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69373 60873 603 41 0 69332 0
vsize: 277492
[startup+790.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62741 0 0 0 78845 171 0 0 25 0 1 0 549278409 284422144 60937 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69439 60937 603 41 0 69398 0
vsize: 277756
[startup+800.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62823 0 0 0 79845 171 0 0 25 0 1 0 549278409 284844032 61019 4294967295 134512640 134672761 3221224624 3221223792 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69542 61019 603 41 0 69501 0
vsize: 278168
[startup+810.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62886 0 0 0 80845 172 0 0 25 0 1 0 549278409 285118464 61082 4294967295 134512640 134672761 3221224624 3221223788 134564515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69609 61082 603 41 0 69568 0
vsize: 278436
[startup+820.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 62955 0 0 0 81845 172 0 0 25 0 1 0 549278409 285388800 61151 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69675 61151 603 41 0 69634 0
vsize: 278700
[startup+830.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63032 0 0 0 82845 172 0 0 25 0 1 0 549278409 285667328 61228 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69743 61228 603 41 0 69702 0
vsize: 278972
[startup+840.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63117 0 0 0 83845 172 0 0 25 0 1 0 549278409 285941760 61313 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69810 61313 603 41 0 69769 0
vsize: 279240
[startup+850.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63190 0 0 0 84845 172 0 0 25 0 1 0 549278409 286347264 61386 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69909 61386 603 41 0 69868 0
vsize: 279636
[startup+860.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63308 0 0 0 85845 172 0 0 25 0 1 0 549278409 286756864 61504 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70009 61504 603 41 0 69968 0
vsize: 280036
[startup+870.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63367 0 0 0 86844 173 0 0 25 0 1 0 549278409 287027200 61563 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70075 61563 603 41 0 70034 0
vsize: 280300
[startup+880.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63431 0 0 0 87844 173 0 0 25 0 1 0 549278409 287293440 61627 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70140 61627 603 41 0 70099 0
vsize: 280560
[startup+890.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63495 0 0 0 88844 174 0 0 25 0 1 0 549278409 287563776 61691 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70206 61691 603 41 0 70165 0
vsize: 280824
[startup+900.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63551 0 0 0 89844 174 0 0 25 0 1 0 549278409 287842304 61747 4294967295 134512640 134672761 3221224624 3221223748 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70274 61747 603 41 0 70233 0
vsize: 281096
[startup+910.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63619 0 0 0 90844 174 0 0 25 0 1 0 549278409 288112640 61815 4294967295 134512640 134672761 3221224624 3221223776 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70340 61815 603 41 0 70299 0
vsize: 281360
[startup+920.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63679 0 0 0 91844 174 0 0 25 0 1 0 549278409 288243712 61875 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70372 61875 603 41 0 70331 0
vsize: 281488
[startup+930.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63760 0 0 0 92844 175 0 0 25 0 1 0 549278409 288649216 61956 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70471 61956 603 41 0 70430 0
vsize: 281884
[startup+940.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63823 0 0 0 93844 175 0 0 25 0 1 0 549278409 288919552 62019 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70537 62019 603 41 0 70496 0
vsize: 282148
[startup+950.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63888 0 0 0 94844 175 0 0 25 0 1 0 549278409 289189888 62084 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70603 62084 603 41 0 70562 0
vsize: 282412
[startup+960.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 63995 0 0 0 95844 175 0 0 25 0 1 0 549278409 289595392 62191 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70702 62191 603 41 0 70661 0
vsize: 282808
[startup+970.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64078 0 0 0 96844 176 0 0 25 0 1 0 549278409 289869824 62274 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70769 62274 603 41 0 70728 0
vsize: 283076
[startup+980.078 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64202 0 0 0 97844 176 0 0 25 0 1 0 549278409 290402304 62398 4294967295 134512640 134672761 3221224624 3221223728 134559995 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70899 62398 603 41 0 70858 0
vsize: 283596
[startup+990.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64291 0 0 0 98844 176 0 0 25 0 1 0 549278409 290811904 62487 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70999 62487 603 41 0 70958 0
vsize: 283996
[startup+1000.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64373 0 0 0 99844 176 0 0 25 0 1 0 549278409 291082240 62569 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71065 62569 603 41 0 71024 0
vsize: 284260
[startup+1010.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64460 0 0 0 100843 177 0 0 25 0 1 0 549278409 291483648 62656 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71163 62656 603 41 0 71122 0
vsize: 284652
[startup+1020.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64528 0 0 0 101843 177 0 0 25 0 1 0 549278409 291762176 62724 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71231 62724 603 41 0 71190 0
vsize: 284924
[startup+1030.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64634 0 0 0 102843 177 0 0 25 0 1 0 549278409 292167680 62830 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71330 62830 603 41 0 71289 0
vsize: 285320
[startup+1040.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64710 0 0 0 103843 177 0 0 25 0 1 0 549278409 292696064 62906 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71459 62906 603 41 0 71418 0
vsize: 285836
[startup+1050.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64796 0 0 0 104843 178 0 0 25 0 1 0 549278409 292970496 62992 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71526 62992 603 41 0 71485 0
vsize: 286104
[startup+1060.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64865 0 0 0 105843 178 0 0 25 0 1 0 549278409 293236736 63061 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71591 63061 603 41 0 71550 0
vsize: 286364
[startup+1070.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 64941 0 0 0 106843 178 0 0 25 0 1 0 549278409 293634048 63137 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71688 63137 603 41 0 71647 0
vsize: 286752
[startup+1080.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65019 0 0 0 107843 178 0 0 25 0 1 0 549278409 293912576 63215 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71756 63215 603 41 0 71715 0
vsize: 287024
[startup+1090.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65118 0 0 0 108843 179 0 0 25 0 1 0 549278409 294346752 63314 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71862 63314 603 41 0 71821 0
vsize: 287448
[startup+1100.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65188 0 0 0 109843 179 0 0 25 0 1 0 549278409 294617088 63384 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71928 63384 603 41 0 71887 0
vsize: 287712
[startup+1110.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65253 0 0 0 110843 179 0 0 25 0 1 0 549278409 294887424 63449 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71994 63449 603 41 0 71953 0
vsize: 287976
[startup+1120.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65317 0 0 0 111843 179 0 0 25 0 1 0 549278409 295157760 63513 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72060 63513 603 41 0 72019 0
vsize: 288240
[startup+1130.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65379 0 0 0 112843 179 0 0 25 0 1 0 549278409 295428096 63575 4294967295 134512640 134672761 3221224624 3221223840 134558154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72126 63575 603 41 0 72085 0
vsize: 288504
[startup+1140.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65456 0 0 0 113843 180 0 0 25 0 1 0 549278409 295698432 63652 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72192 63652 603 41 0 72151 0
vsize: 288768
[startup+1150.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65537 0 0 0 114844 180 0 0 25 0 1 0 549278409 295960576 63733 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72256 63733 603 41 0 72215 0
vsize: 289024
[startup+1160.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65615 0 0 0 115844 180 0 0 25 0 1 0 549278409 296378368 63811 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72358 63811 603 41 0 72317 0
vsize: 289432
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65701 0 0 0 116844 180 0 0 25 0 1 0 549278409 296656896 63897 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72426 63897 603 41 0 72385 0
vsize: 289704
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65797 0 0 0 117844 180 0 0 25 0 1 0 549278409 297062400 63993 4294967295 134512640 134672761 3221224624 3221223624 1075349950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72525 63993 603 41 0 72484 0
vsize: 290100
[startup+1190.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65872 0 0 0 118845 181 0 0 25 0 1 0 549278409 297328640 64068 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72590 64068 603 41 0 72549 0
vsize: 290360
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 17690
Raw data (stat): 17690 (minisat+) R 17689 3260 3259 0 -1 0 65949 0 0 0 119846 181 0 0 25 0 1 0 549278409 297730048 64145 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72688 64145 603 41 0 72647 0
vsize: 290752
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.26 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 17690
Raw data (stat): 17690 (minisat+) Z 17689 3260 3259 0 -1 12 65951 0 0 0 119846 193 0 0 23 0 1 0 549278409 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.26
CPU time (s): 1200.4
CPU user time (s): 1198.46
CPU system time (s): 1.9387
CPU usage (%): 100.012
Max. virtual memory (Kb): 290752
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####