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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-t1717.opb
MD5SUMbc46e72682d969c09e6f4028df473a45
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers28
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.34
Number of variables73885
Total number of constraints74436
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)74436
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint612

Trace number 18377 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 14:48:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18068 boxname=wulflinc2 idbench=1390 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc46e72682d969c09e6f4028df473a45  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-t1717.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-t1717.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-t1717.opb
IDLAUNCH: 18068
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        886208 kB
Buffers:         13080 kB
Cached:         114020 kB
SwapCached:        536 kB
Active:          26456 kB
Inactive:       102616 kB
HighTotal:      131008 kB
HighFree:        33628 kB
LowTotal:       903652 kB
LowFree:        852580 kB
SwapTotal:     2097136 kB
SwapFree:      2095664 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            13548 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:56:17 (client local time) WITH STATUS 0 IN 441.404 SECONDS
stats: 18068 7 441.404 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 | 1593441  4143559 |  478032       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/710649          
c   -- var.elim.:  2000/710649          
c   -- var.elim.:  3000/710649          
c   -- var.elim.:  4000/710649          
c   -- var.elim.:  5000/710649          
c   -- var.elim.:  6000/710649          
c   -- var.elim.:  7000/710649          
c   -- var.elim.:  8000/710649          
c   -- var.elim.:  9000/710649          
c   -- var.elim.:  10000/710649          
c   -- var.elim.:  11000/710649          
c   -- var.elim.:  12000/710649          
c   -- var.elim.:  13000/710649          
c   -- var.elim.:  14000/710649          
c   -- var.elim.:  15000/710649          
c   -- var.elim.:  16000/710649          
c   -- var.elim.:  17000/710649          
c   -- var.elim.:  18000/710649          
c   -- var.elim.:  19000/710649          
c   -- var.elim.:  20000/710649          
c   -- var.elim.:  21000/710649          
c   -- var.elim.:  22000/710649          
c   -- var.elim.:  23000/710649          
c   -- var.elim.:  24000/710649          
c   -- var.elim.:  25000/710649          
c   -- var.elim.:  26000/710649          
c   -- var.elim.:  27000/710649          
c   -- var.elim.:  28000/710649          
c   -- var.elim.:  29000/710649          
c   -- var.elim.:  30000/710649          
c   -- var.elim.:  31000/710649          
c   -- var.elim.:  32000/710649          
c   -- var.elim.:  33000/710649          
c   -- var.elim.:  34000/710649          
c   -- var.elim.:  35000/710649          
c   -- var.elim.:  36000/710649          
c   -- var.elim.:  37000/710649          
c   -- var.elim.:  38000/710649          
c   -- var.elim.:  39000/710649          
c   -- var.elim.:  40000/710649          
c   -- var.elim.:  41000/710649          
c   -- var.elim.:  42000/710649          
c   -- var.elim.:  43000/710649          
c   -- var.elim.:  44000/710649          
c   -- var.elim.:  45000/710649          
c   -- var.elim.:  46000/710649          
c   -- var.elim.:  47000/710649          
c   -- var.elim.:  48000/710649          
c   -- var.elim.:  49000/710649          
c   -- var.elim.:  50000/710649          
c   -- var.elim.:  51000/710649          
c   -- var.elim.:  52000/710649          
c   -- var.elim.:  53000/710649          
c   -- var.elim.:  54000/710649          
c   -- var.elim.:  55000/710649          
c   -- var.elim.:  56000/710649          
c   -- var.elim.:  57000/710649          
c   -- var.elim.:  58000/710649          
c   -- var.elim.:  59000/710649          
c   -- var.elim.:  60000/710649          
c   -- var.elim.:  61000/710649          
c   -- var.elim.:  62000/710649          
c   -- var.elim.:  63000/710649          
c   -- var.elim.:  64000/710649          
c   -- var.elim.:  65000/710649          
c   -- var.elim.:  66000/710649          
c   -- var.elim.:  67000/710649          
c   -- var.elim.:  68000/710649          
c   -- var.elim.:  69000/710649          
c   -- var.elim.:  70000/710649          
c   -- var.elim.:  71000/710649          
c   -- var.elim.:  72000/710649          
c   -- var.elim.:  73000/710649          
c   -- var.elim.:  74000/710649          
c   -- var.elim.:  75000/710649          
c   -- var.elim.:  76000/710649          
c   -- var.elim.:  77000/710649          
c   -- var.elim.:  78000/710649          
c   -- var.elim.:  79000/710649          
c   -- var.elim.:  80000/710649          
c   -- var.elim.:  81000/710649          
c   -- var.elim.:  82000/710649          
c   -- var.elim.:  83000/710649          
c   -- var.elim.:  84000/710649          
c   -- var.elim.:  85000/710649          
c   -- var.elim.:  86000/710649          
c   -- var.elim.:  87000/710649          
c   -- var.elim.:  88000/710649          
c   -- var.elim.:  89000/710649          
c   -- var.elim.:  90000/710649          
c   -- var.elim.:  91000/710649          
c   -- var.elim.:  92000/710649          
c   -- var.elim.:  93000/710649          
c   -- var.elim.:  94000/710649          
c   -- var.elim.:  95000/710649          
c   -- var.elim.:  96000/710649          
c   -- var.elim.:  97000/710649          
c   -- var.elim.:  98000/710649          
c   -- var.elim.:  99000/710649          
c   -- var.elim.:  100000/710649          
c   -- var.elim.:  101000/710649          
c   -- var.elim.:  102000/710649          
c   -- var.elim.:  103000/710649          
c   -- var.elim.:  104000/710649          
c   -- var.elim.:  105000/710649          
c   -- var.elim.:  106000/710649          
c   -- var.elim.:  107000/710649          
c   -- var.elim.:  108000/710649          
c   -- var.elim.:  109000/710649          
c   -- var.elim.:  110000/710649          
c   -- var.elim.:  111000/710649          
c   -- var.elim.:  112000/710649          
c   -- var.elim.:  113000/710649          
c   -- var.elim.:  114000/710649          
c   -- var.elim.:  115000/710649          
c   -- var.elim.:  116000/710649          
c   -- var.elim.:  117000/710649          
c   -- var.elim.:  118000/710649          
c   -- var.elim.:  119000/710649          
c   -- var.elim.:  120000/710649          
c   -- var.elim.:  121000/710649          
c   -- var.elim.:  122000/710649          
c   -- var.elim.:  123000/710649          
c   -- var.elim.:  124000/710649          
c   -- var.elim.:  125000/710649          
c   -- var.elim.:  126000/710649          
c   -- var.elim.:  127000/710649          
c   -- var.elim.:  128000/710649          
c   -- var.elim.:  129000/710649          
c   -- var.elim.:  130000/710649          
c   -- var.elim.:  131000/710649          
c   -- var.elim.:  132000/710649          
c   -- var.elim.:  133000/710649          
c   -- var.elim.:  134000/710649          
c   -- var.elim.:  135000/710649          
c   -- var.elim.:  136000/710649          
c   -- var.elim.:  137000/710649          
c   -- var.elim.:  138000/710649          
c   -- var.elim.:  139000/710649          
c   -- var.elim.:  140000/710649          
c   -- var.elim.:  141000/710649          
c   -- var.elim.:  142000/710649          
c   -- var.elim.:  143000/710649          
c   -- var.elim.:  144000/710649          
c   -- var.elim.:  145000/710649          
c   -- var.elim.:  146000/710649          
c   -- var.elim.:  147000/710649          
c   -- var.elim.:  148000/710649          
c   -- var.elim.:  149000/710649          
c   -- var.elim.:  150000/710649          
c   -- var.elim.:  151000/710649          
c   -- var.elim.:  152000/710649          
c   -- var.elim.:  153000/710649          
c   -- var.elim.:  154000/710649          
c   -- var.elim.:  155000/710649          
c   -- var.elim.:  156000/710649          
c   -- var.elim.:  157000/710649          
c   -- var.elim.:  158000/710649          
c   -- var.elim.:  159000/710649          
c   -- var.elim.:  160000/710649          
c   -- var.elim.:  161000/710649          
c   -- var.elim.:  162000/710649          
c   -- var.elim.:  163000/710649          
c   -- var.elim.:  164000/710649          
c   -- var.elim.:  165000/710649          
c   -- var.elim.:  166000/710649          
c   -- var.elim.:  167000/710649          
c   -- var.elim.:  168000/710649          
c   -- var.elim.:  169000/710649          
c   -- var.elim.:  170000/710649          
c   -- var.elim.:  171000/710649          
c   -- var.elim.:  172000/710649          
c   -- var.elim.:  173000/710649          
c   -- var.elim.:  174000/710649          
c   -- var.elim.:  175000/710649          
c   -- var.elim.:  176000/710649          
c   -- var.elim.:  177000/710649          
c   -- var.elim.:  178000/710649          
c   -- var.elim.:  179000/710649          
c   -- var.elim.:  180000/710649          
c   -- var.elim.:  181000/710649          
c   -- var.elim.:  182000/710649          
c   -- var.elim.:  183000/710649          
c   -- var.elim.:  184000/710649          
c   -- var.elim.:  185000/710649          
c   -- var.elim.:  186000/710649          
c   -- var.elim.:  187000/710649          
c   -- var.elim.:  188000/710649          
c   -- var.elim.:  189000/710649          
c   -- var.elim.:  190000/710649          
c   -- var.elim.:  191000/710649          
c   -- var.elim.:  192000/710649          
c   -- var.elim.:  193000/710649          
c   -- var.elim.:  194000/710649          
c   -- var.elim.:  195000/710649          
c   -- var.elim.:  196000/710649          
c   -- var.elim.:  197000/710649          
c   -- var.elim.:  198000/710649          
c   -- var.elim.:  199000/710649          
c   -- var.elim.:  200000/710649          
c   -- var.elim.:  201000/710649          
c   -- var.elim.:  202000/710649          
c   -- var.elim.:  203000/710649          
c   -- var.elim.:  204000/710649          
c   -- var.elim.:  205000/710649          
c   -- var.elim.:  206000/710649          
c   -- var.elim.:  207000/710649          
c   -- var.elim.:  208000/710649          
c   -- var.elim.:  209000/710649          
c   -- var.elim.:  210000/710649          
c   -- var.elim.:  211000/710649          
c   -- var.elim.:  212000/710649          
c   -- var.elim.:  213000/710649          
c   -- var.elim.:  214000/710649          
c   -- var.elim.:  215000/710649          
c   -- var.elim.:  216000/710649          
c   -- var.elim.:  217000/710649          
c   -- var.elim.:  218000/710649          
c   -- var.elim.:  219000/710649          
c   -- var.elim.:  220000/710649          
c   -- var.elim.:  221000/710649          
c   -- var.elim.:  222000/710649          
c   -- var.elim.:  223000/710649          
c   -- var.elim.:  224000/710649          
c   -- var.elim.:  225000/710649          
c   -- var.elim.:  226000/710649          
c   -- var.elim.:  227000/710649          
c   -- var.elim.:  228000/710649          
c   -- var.elim.:  229000/710649          
c   -- var.elim.:  230000/710649          
c   -- var.elim.:  231000/710649          
c   -- var.elim.:  232000/710649          
c   -- var.elim.:  233000/710649          
c   -- var.elim.:  234000/710649          
c   -- var.elim.:  235000/710649          
c   -- var.elim.:  236000/710649          
c   -- var.elim.:  237000/710649          
c   -- var.elim.:  238000/710649          
c   -- var.elim.:  239000/710649          
c   -- var.elim.:  240000/710649          
c   -- var.elim.:  241000/710649          
c   -- var.elim.:  242000/710649          
c   -- var.elim.:  243000/710649          
c   -- var.elim.:  244000/710649          
c   -- var.elim.:  245000/710649          
c   -- var.elim.:  246000/710649          
c   -- var.elim.:  247000/710649          
c   -- var.elim.:  248000/710649          
c   -- var.elim.:  249000/710649          
c   -- var.elim.:  250000/710649          
c   -- var.elim.:  251000/710649          
c   -- var.elim.:  252000/710649          
c   -- var.elim.:  253000/710649          
c   -- var.elim.:  254000/710649          
c   -- var.elim.:  255000/710649          
c   -- var.elim.:  256000/710649          
c   -- var.elim.:  257000/710649          
c   -- var.elim.:  258000/710649          
c   -- var.elim.:  259000/710649          
c   -- var.elim.:  260000/710649          
c   -- var.elim.:  261000/710649          
c   -- var.elim.:  262000/710649          
c   -- var.elim.:  263000/710649          
c   -- var.elim.:  264000/710649          
c   -- var.elim.:  265000/710649          
c   -- var.elim.:  266000/710649          
c   -- var.elim.:  267000/710649          
c   -- var.elim.:  268000/710649          
c   -- var.elim.:  269000/710649          
c   -- var.elim.:  270000/710649          
c   -- var.elim.:  271000/710649          
c   -- var.elim.:  272000/710649          
c   -- var.elim.:  273000/710649          
c   -- var.elim.:  274000/710649          
c   -- var.elim.:  275000/710649          
c   -- var.elim.:  276000/710649          
c   -- var.elim.:  277000/710649          
c   -- var.elim.:  278000/710649          
c   -- var.elim.:  279000/710649          
c   -- var.elim.:  280000/710649          
c   -- var.elim.:  281000/710649          
c   -- var.elim.:  282000/710649          
c   -- var.elim.:  283000/710649          
c   -- var.elim.:  284000/710649          
c   -- var.elim.:  285000/710649          
c   -- var.elim.:  286000/710649          
c   -- var.elim.:  287000/710649          
c   -- var.elim.:  288000/710649          
c   -- var.elim.:  289000/710649          
c   -- var.elim.:  290000/710649          
c   -- var.elim.:  291000/710649          
c   -- var.elim.:  292000/710649          
c   -- var.elim.:  293000/710649          
c   -- var.elim.:  294000/710649          
c   -- var.elim.:  295000/710649          
c   -- var.elim.:  296000/710649          
c   -- var.elim.:  297000/710649          
c   -- var.elim.:  298000/710649          
c   -- var.elim.:  299000/710649          
c   -- var.elim.:  300000/710649          
c   -- var.elim.:  301000/710649          
c   -- var.elim.:  302000/710649          
c   -- var.elim.:  303000/710649          
c   -- var.elim.:  304000/710649          
c   -- var.elim.:  305000/710649          
c   -- var.elim.:  306000/710649          
c   -- var.elim.:  307000/710649          
c   -- var.elim.:  308000/710649          
c   -- var.elim.:  309000/710649          
c   -- var.elim.:  310000/710649          
c   -- var.elim.:  311000/710649          
c   -- var.elim.:  312000/710649          
c   -- var.elim.:  313000/710649          
c   -- var.elim.:  314000/710649          
c   -- var.elim.:  315000/710649          
c   -- var.elim.:  316000/710649          
c   -- var.elim.:  317000/710649          
c   -- var.elim.:  318000/710649          
c   -- var.elim.:  319000/710649          
c   -- var.elim.:  320000/710649          
c   -- var.elim.:  321000/710649          
c   -- var.elim.:  322000/710649          
c   -- var.elim.:  323000/710649          
c   -- var.elim.:  324000/710649          
c   -- var.elim.:  325000/710649          
c   -- var.elim.:  326000/710649          
c   -- var.elim.:  327000/710649          
c   -- var.elim.:  328000/710649          
c   -- var.elim.:  329000/710649          
c   -- var.elim.:  330000/710649          
c   -- var.elim.:  331000/710649          
c   -- var.elim.:  332000/710649          
c   -- var.elim.:  333000/710649          
c   -- var.elim.:  334000/710649          
c   -- var.elim.:  335000/710649          
c   -- var.elim.:  336000/710649          
c   -- var.elim.:  337000/710649          
c   -- var.elim.:  338000/710649          
c   -- var.elim.:  339000/710649          
c   -- var.elim.:  340000/710649          
c   -- var.elim.:  341000/710649          
c   -- var.elim.:  342000/710649          
c   -- var.elim.:  343000/710649          
c   -- var.elim.:  344000/710649          
c   -- var.elim.:  345000/710649          
c   -- var.elim.:  346000/710649          
c   -- var.elim.:  347000/710649          
c   -- var.elim.:  348000/710649          
c   -- var.elim.:  349000/710649          
c   -- var.elim.:  350000/710649          
c   -- var.elim.:  351000/710649          
c   -- var.elim.:  352000/710649          
c   -- var.elim.:  353000/710649          
c   -- var.elim.:  354000/710649          
c   -- var.elim.:  355000/710649          
c   -- var.elim.:  356000/710649          
c   -- var.elim.:  357000/710649          
c   -- var.elim.:  358000/710649          
c   -- var.elim.:  359000/710649          
c   -- var.elim.:  360000/710649          
c   -- var.elim.:  361000/710649          
c   -- var.elim.:  362000/710649          
c   -- var.elim.:  363000/710649          
c   -- var.elim.:  364000/710649          
c   -- var.elim.:  365000/710649          
c   -- var.elim.:  366000/710649          
c   -- var.elim.:  367000/710649          
c   -- var.elim.:  368000/710649          
c   -- var.elim.:  369000/710649          
c   -- var.elim.:  370000/710649          
c   -- var.elim.:  371000/710649          
c   -- var.elim.:  372000/710649          
c   -- var.elim.:  373000/710649          
c   -- var.elim.:  374000/710649          
c   -- var.elim.:  375000/710649          
c   -- var.elim.:  376000/710649          
c   -- var.elim.:  377000/710649          
c   -- var.elim.:  378000/710649          
c   -- var.elim.:  379000/710649          
c   -- var.elim.:  380000/710649          
c   -- var.elim.:  381000/710649          
c   -- var.elim.:  382000/710649          
c   -- var.elim.:  383000/710649          
c   -- var.elim.:  384000/710649          
c   -- var.elim.:  385000/710649          
c   -- var.elim.:  386000/710649          
c   -- var.elim.:  387000/710649          
c   -- var.elim.:  388000/710649          
c   -- var.elim.:  389000/710649          
c   -- var.elim.:  390000/710649          
c   -- var.elim.:  391000/710649          
c   -- var.elim.:  392000/710649          
c   -- var.elim.:  393000/710649          
c   -- var.elim.:  394000/710649          
c   -- var.elim.:  395000/710649          
c   -- var.elim.:  396000/710649          
c   -- var.elim.:  397000/710649          
c   -- var.elim.:  398000/710649          
c   -- var.elim.:  399000/710649          
c   -- var.elim.:  400000/710649          
c   -- var.elim.:  401000/710649          
c   -- var.elim.:  402000/710649          
c   -- var.elim.:  403000/710649          
c   -- var.elim.:  404000/710649          
c   -- var.elim.:  405000/710649          
c   -- var.elim.:  406000/710649          
c   -- var.elim.:  407000/710649          
c   -- var.elim.:  408000/710649          
c   -- var.elim.:  409000/710649          
c   -- var.elim.:  410000/710649          
c   -- var.elim.:  411000/710649          
c   -- var.elim.:  412000/710649          
c   -- var.elim.:  413000/710649          
c   -- var.elim.:  414000/710649          
c   -- var.elim.:  415000/710649          
c   -- var.elim.:  416000/710649          
c   -- var.elim.:  417000/710649          
c   -- var.elim.:  418000/710649          
c   -- var.elim.:  419000/710649          
c   -- var.elim.:  420000/710649          
c   -- var.elim.:  421000/710649          
c   -- var.elim.:  422000/710649          
c   -- var.elim.:  423000/710649          
c   -- var.elim.:  424000/710649          
c   -- var.elim.:  425000/710649          
c   -- var.elim.:  426000/710649          
c   -- var.elim.:  427000/710649          
c   -- var.elim.:  428000/710649          
c   -- var.elim.:  429000/710649          
c   -- var.elim.:  430000/710649          
c   -- var.elim.:  431000/710649          
c   -- var.elim.:  432000/710649          
c   -- var.elim.:  433000/710649          
c   -- var.elim.:  434000/710649          
c   -- var.elim.:  435000/710649          
c   -- var.elim.:  436000/710649          
c   -- var.elim.:  437000/710649          
c   -- var.elim.:  438000/710649          
c   -- var.elim.:  439000/710649          
c   -- var.elim.:  440000/710649          
c   -- var.elim.:  441000/710649          
c   -- var.elim.:  442000/710649          
c   -- var.elim.:  443000/710649          
c   -- var.elim.:  444000/710649          
c   -- var.elim.:  445000/710649          
c   -- var.elim.:  446000/710649          
c   -- var.elim.:  447000/710649          
c   -- var.elim.:  448000/710649          
c   -- var.elim.:  449000/710649          
c   -- var.elim.:  450000/710649          
c   -- var.elim.:  451000/710649          
c   -- var.elim.:  452000/710649          
c   -- var.elim.:  453000/710649          
c   -- var.elim.:  454000/710649          
c   -- var.elim.:  455000/710649          
c   -- var.elim.:  456000/710649          
c   -- var.elim.:  457000/710649          
c   -- var.elim.:  458000/710649          
c   -- var.elim.:  459000/710649          
c   -- var.elim.:  460000/710649          
c   -- var.elim.:  461000/710649          
c   -- var.elim.:  462000/710649          
c   -- var.elim.:  463000/710649          
c   -- var.elim.:  464000/710649          
c   -- var.elim.:  465000/710649          
c   -- var.elim.:  466000/710649          
c   -- var.elim.:  467000/710649          
c   -- var.elim.:  468000/710649          
c   -- var.elim.:  469000/710649          
c   -- var.elim.:  470000/710649          
c   -- var.elim.:  471000/710649          
c   -- var.elim.:  472000/710649          
c   -- var.elim.:  473000/710649          
c   -- var.elim.:  474000/710649          
c   -- var.elim.:  475000/710649          
c   -- var.elim.:  476000/710649          
c   -- var.elim.:  477000/710649          
c   -- var.elim.:  478000/710649          
c   -- var.elim.:  479000/710649          
c   -- var.elim.:  480000/710649          
c   -- var.elim.:  481000/710649          
c   -- var.elim.:  482000/710649          
c   -- var.elim.:  483000/710649          
c   -- var.elim.:  484000/710649          
c   -- var.elim.:  485000/710649          
c   -- var.elim.:  486000/710649          
c   -- var.elim.:  487000/710649          
c   -- var.elim.:  488000/710649          
c   -- var.elim.:  489000/710649          
c   -- var.elim.:  490000/710649          
c   -- var.elim.:  491000/710649          
c   -- var.elim.:  492000/710649          
c   -- var.elim.:  493000/710649          
c   -- var.elim.:  494000/710649          
c   -- var.elim.:  495000/710649          
c   -- var.elim.:  496000/710649          
c   -- var.elim.:  497000/710649          
c   -- var.elim.:  498000/710649          
c   -- var.elim.:  499000/710649          
c   -- var.elim.:  500000/710649          
c   -- var.elim.:  501000/710649          
c   -- var.elim.:  502000/710649          
c   -- var.elim.:  503000/710649          
c   -- var.elim.:  504000/710649          
c   -- var.elim.:  505000/710649          
c   -- var.elim.:  506000/710649          
c   -- var.elim.:  507000/710649          
c   -- var.elim.:  508000/710649          
c   -- var.elim.:  509000/710649          
c   -- var.elim.:  510000/710649          
c   -- var.elim.:  511000/710649          
c   -- var.elim.:  512000/710649          
c   -- var.elim.:  513000/710649          
c   -- var.elim.:  514000/710649          
c   -- var.elim.:  515000/710649          
c   -- var.elim.:  516000/710649          
c   -- var.elim.:  517000/710649          
c   -- var.elim.:  518000/710649          
c   -- var.elim.:  519000/710649          
c   -- var.elim.:  520000/710649          
c   -- var.elim.:  521000/710649          
c   -- var.elim.:  522000/710649          
c   -- var.elim.:  523000/710649          
c   -- var.elim.:  524000/710649          
c   -- var.elim.:  525000/710649          
c   -- var.elim.:  526000/710649          
c   -- var.elim.:  527000/710649          
c   -- var.elim.:  528000/710649          
c   -- var.elim.:  529000/710649          
c   -- var.elim.:  530000/710649          
c   -- var.elim.:  531000/710649          
c   -- var.elim.:  532000/710649          
c   -- var.elim.:  533000/710649          
c   -- var.elim.:  534000/710649          
c   -- var.elim.:  535000/710649          
c   -- var.elim.:  536000/710649          
c   -- var.elim.:  537000/710649          
c   -- var.elim.:  538000/710649          
c   -- var.elim.:  539000/710649          
c   -- var.elim.:  540000/710649          
c   -- var.elim.:  541000/710649          
c   -- var.elim.:  542000/710649          
c   -- var.elim.:  543000/710649          
c   -- var.elim.:  544000/710649          
c   -- var.elim.:  545000/710649          
c   -- var.elim.:  546000/710649          
c   -- var.elim.:  547000/710649          
c   -- var.elim.:  548000/710649          
c   -- var.elim.:  549000/710649          
c   -- var.elim.:  550000/710649          
c   -- var.elim.:  551000/710649          
c   -- var.elim.:  552000/710649          
c   -- var.elim.:  553000/710649          
c   -- var.elim.:  554000/710649          
c   -- var.elim.:  555000/710649          
c   -- var.elim.:  556000/710649          
c   -- var.elim.:  557000/710649          
c   -- var.elim.:  558000/710649          
c   -- var.elim.:  559000/710649          
c   -- var.elim.:  560000/710649          
c   -- var.elim.:  561000/710649          
c   -- var.elim.:  562000/710649          
c   -- var.elim.:  563000/710649          
c   -- var.elim.:  564000/710649          
c   -- var.elim.:  565000/710649          
c   -- var.elim.:  566000/710649          
c   -- var.elim.:  567000/710649          
c   -- var.elim.:  568000/710649          
c   -- var.elim.:  569000/710649          
c   -- var.elim.:  570000/710649          
c   -- var.elim.:  571000/710649          
c   -- var.elim.:  572000/710649          
c   -- var.elim.:  573000/710649          
c   -- var.elim.:  574000/710649          
c   -- var.elim.:  575000/710649          
c   -- var.elim.:  576000/710649          
c   -- var.elim.:  577000/710649          
c   -- var.elim.:  578000/710649          
c   -- var.elim.:  579000/710649          
c   -- var.elim.:  580000/710649          
c   -- var.elim.:  581000/710649          
c   -- var.elim.:  582000/710649          
c   -- var.elim.:  583000/710649          
c   -- var.elim.:  584000/710649          
c   -- var.elim.:  585000/710649          
c   -- var.elim.:  586000/710649          
c   -- var.elim.:  587000/710649          
c   -- var.elim.:  588000/710649          
c   -- var.elim.:  589000/710649          
c   -- var.elim.:  590000/710649          
c   -- var.elim.:  591000/710649          
c   -- var.elim.:  592000/710649          
c   -- var.elim.:  593000/710649          
c   -- var.elim.:  594000/710649          
c   -- var.elim.:  595000/710649          
c   -- var.elim.:  596000/710649          
c   -- var.elim.:  597000/710649          
c   -- var.elim.:  598000/710649          
c   -- var.elim.:  599000/710649          
c   -- var.elim.:  600000/710649          
c   -- var.elim.:  601000/710649          
c   -- var.elim.:  602000/710649          
c   -- var.elim.:  603000/710649          
c   -- var.elim.:  604000/710649          
c   -- var.elim.:  605000/710649          
c   -- var.elim.:  606000/710649          
c   -- var.elim.:  607000/710649          
c   -- var.elim.:  608000/710649          
c   -- var.elim.:  609000/710649          
c   -- var.elim.:  610000/710649          
c   -- var.elim.:  611000/710649          
c   -- var.elim.:  612000/710649          
c   -- var.elim.:  613000/710649          
c   -- var.elim.:  614000/710649          
c   -- var.elim.:  615000/710649          
c   -- var.elim.:  616000/710649          
c   -- var.elim.:  617000/710649          
c   -- var.elim.:  618000/710649          
c   -- var.elim.:  619000/710649          
c   -- var.elim.:  620000/710649          
c   -- var.elim.:  621000/710649          
c   -- var.elim.:  622000/710649          
c   -- var.elim.:  623000/710649          
c   -- var.elim.:  624000/710649          
c   -- var.elim.:  625000/710649          
c   -- var.elim.:  626000/710649          
c   -- var.elim.:  627000/710649          
c   -- var.elim.:  628000/710649          
c   -- var.elim.:  629000/710649          
c   -- var.elim.:  630000/710649          
c   -- var.elim.:  631000/710649          
c   -- var.elim.:  632000/710649          
c   -- var.elim.:  633000/710649          
c   -- var.elim.:  634000/710649          
c   -- var.elim.:  635000/710649          
c   -- var.elim.:  636000/710649          
c   -- var.elim.:  637000/710649          
c   -- var.elim.:  638000/710649          
c   -- var.elim.:  639000/710649          
c   -- var.elim.:  640000/710649          
c   -- var.elim.:  641000/710649          
c   -- var.elim.:  642000/710649          
c   -- var.elim.:  643000/710649          
c   -- var.elim.:  644000/710649          
c   -- var.elim.:  645000/710649          
c   -- var.elim.:  646000/710649          
c   -- var.elim.:  647000/710649          
c   -- var.elim.:  648000/710649          
c   -- var.elim.:  649000/710649          
c   -- var.elim.:  650000/710649          
c   -- var.elim.:  651000/710649          
c   -- var.elim.:  652000/710649          
c   -- var.elim.:  653000/710649          
c   -- var.elim.:  654000/710649          
c   -- var.elim.:  655000/710649          
c   -- var.elim.:  656000/710649          
c   -- var.elim.:  657000/710649          
c   -- var.elim.:  658000/710649          
c   -- var.elim.:  659000/710649          
c   -- var.elim.:  660000/710649          
c   -- var.elim.:  661000/710649          
c   -- var.elim.:  662000/710649          
c   -- var.elim.:  663000/710649          
c   -- var.elim.:  664000/710649          
c   -- var.elim.:  665000/710649          
c   -- var.elim.:  666000/710649          
c   -- var.elim.:  667000/710649          
c   -- var.elim.:  668000/710649          
c   -- var.elim.:  669000/710649          
c   -- var.elim.:  670000/710649          
c   -- var.elim.:  671000/710649          
c   -- var.elim.:  672000/710649          
c   -- var.elim.:  673000/710649          
c   -- var.elim.:  674000/710649          
c   -- var.elim.:  675000/710649          
c   -- var.elim.:  676000/710649          
c   -- var.elim.:  677000/710649          
c   -- var.elim.:  678000/710649          
c   -- var.elim.:  679000/710649          
c   -- var.elim.:  680000/710649          
c   -- var.elim.:  681000/710649          
c   -- var.elim.:  682000/710649          
c   -- var.elim.:  683000/710649          
c   -- var.elim.:  684000/710649          
c   -- var.elim.:  685000/710649          
c   -- var.elim.:  686000/710649          
c   -- var.elim.:  687000/710649          
c   -- var.elim.:  688000/710649          
c   -- var.elim.:  689000/710649          
c   -- var.elim.:  690000/710649          
c   -- var.elim.:  691000/710649          
c   -- var.elim.:  692000/710649          
c   -- var.elim.:  693000/710649          
c   -- var.elim.:  694000/710649          
c   -- var.elim.:  695000/710649          
c   -- var.elim.:  696000/710649          
c   -- var.elim.:  697000/710649          
c   -- var.elim.:  698000/710649          
c   -- var.elim.:  699000/710649          
c   -- var.elim.:  700000/710649          
c   -- var.elim.:  701000/710649          
c   -- var.elim.:  702000/710649          
c   -- var.elim.:  703000/710649          
c   -- var.elim.:  704000/710649          
c   -- var.elim.:  705000/710649          
c   -- var.elim.:  706000/710649          
c   -- var.elim.:  707000/710649          
c   -- var.elim.:  708000/710649          
c   -- var.elim.:  709000/710649          
c   -- var.elim.:  710000/710649          
c   -- var.elim.:  710649/710649          
c   -- var.elim.:  1000/1412          
c   -- var.elim.:  1412/1412          
c   -- subsuming                       
c   -- var.elim.:  1000/1754          
c   -- var.elim.:  1754/1754          
c   -- var.elim.:  1000/1306          
c   -- var.elim.:  1306/1306          
c   -- subsuming                       
c   -- var.elim.:  1000/1203          
c   -- var.elim.:  1203/1203          
c |         0 | 1591568  4#### 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.85 0.88 2/54 29604
Raw data (stat): 29604 (runsolver) R 29603 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487704773 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.63 0.86 0.88 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 15408 0 0 0 956 42 0 0 25 0 1 0 487704773 64483328 13682 4294967295 134512640 134672761 3221224544 3221192512 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15743 13682 603 41 0 15702 0
vsize: 62972
[startup+19.9999 s]
Raw data (loadavg): 0.69 0.86 0.88 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 71705 0 0 0 1821 178 0 0 25 0 1 0 487704773 307720192 69979 4294967295 134512640 134672761 3221224544 3221216112 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75127 69980 603 41 0 75086 0
vsize: 300508
[startup+30.0005 s]
Raw data (loadavg): 0.74 0.86 0.88 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 97443 0 0 0 2759 239 0 0 25 0 1 0 487704773 448479232 95685 4294967295 134512640 134672761 3221224544 3221223088 134621071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 109492 95685 603 41 0 109451 0
vsize: 437968
[startup+40.0012 s]
Raw data (loadavg): 0.78 0.87 0.88 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 100225 0 0 0 3753 246 0 0 25 0 1 0 487704773 455516160 97077 4294967295 134512640 134672761 3221224544 3221222992 134643777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 111210 97077 603 41 0 111169 0
vsize: 444840
[startup+50.002 s]
Raw data (loadavg): 0.81 0.87 0.88 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 107773 0 0 0 4733 266 0 0 25 0 1 0 487704773 451198976 96248 4294967295 134512640 134672761 3221224544 3221223584 134614202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 110156 96248 603 41 0 110115 0
vsize: 440624
[startup+60.0017 s]
Raw data (loadavg): 0.84 0.88 0.88 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 107920 0 0 0 5733 266 0 0 25 0 1 0 487704773 453296128 96395 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 110668 96395 603 41 0 110627 0
vsize: 442672
[startup+70.0013 s]
Raw data (loadavg): 0.86 0.88 0.88 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 108001 0 0 0 6732 267 0 0 25 0 1 0 487704773 453701632 96476 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 110767 96476 603 41 0 110726 0
vsize: 443068
[startup+80.0069 s]
Raw data (loadavg): 0.88 0.88 0.88 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 108059 0 0 0 7733 267 0 0 25 0 1 0 487704773 453836800 96534 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 110800 96534 603 41 0 110759 0
vsize: 443200
[startup+90.0067 s]
Raw data (loadavg): 0.90 0.89 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 108144 0 0 0 8733 267 0 0 25 0 1 0 487704773 454754304 96619 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111024 96619 603 41 0 110983 0
vsize: 444096
[startup+100.007 s]
Raw data (loadavg): 0.92 0.89 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 108182 0 0 0 9733 267 0 0 25 0 1 0 487704773 454885376 96657 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111056 96657 603 41 0 111015 0
vsize: 444224
[startup+110.008 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 108307 0 0 0 10733 267 0 0 25 0 1 0 487704773 455286784 96782 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111154 96782 603 41 0 111113 0
vsize: 444616
[startup+120.016 s]
Raw data (loadavg): 0.94 0.89 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 108411 0 0 0 11734 268 0 0 25 0 1 0 487704773 455684096 96886 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111251 96886 603 41 0 111210 0
vsize: 445004
[startup+130.016 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 108526 0 0 0 12734 268 0 0 25 0 1 0 487704773 456097792 97001 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111352 97001 603 41 0 111311 0
vsize: 445408
[startup+140.016 s]
Raw data (loadavg): 0.95 0.90 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 108822 0 0 0 13733 269 0 0 25 0 1 0 487704773 457330688 97297 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111653 97297 603 41 0 111612 0
vsize: 446612
[startup+150.12 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109118 0 0 0 14743 270 0 0 25 0 1 0 487704773 458473472 97593 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111932 97593 603 41 0 111891 0
vsize: 447728
[startup+160.12 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109368 0 0 0 15743 270 0 0 25 0 1 0 487704773 459313152 97843 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112137 97843 603 41 0 112096 0
vsize: 448548
[startup+170.119 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109448 0 0 0 16742 270 0 0 25 0 1 0 487704773 459567104 97923 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112199 97923 603 41 0 112158 0
vsize: 448796
[startup+180.126 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109495 0 0 0 17743 271 0 0 25 0 1 0 487704773 459698176 97970 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112231 97970 603 41 0 112190 0
vsize: 448924
[startup+190.133 s]
Raw data (loadavg): 1.06 0.93 0.90 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109550 0 0 0 18744 271 0 0 25 0 1 0 487704773 459964416 98025 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112296 98025 603 41 0 112255 0
vsize: 449184
[startup+200.133 s]
Raw data (loadavg): 1.05 0.93 0.90 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109647 0 0 0 19744 271 0 0 25 0 1 0 487704773 460361728 98122 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112393 98122 603 41 0 112352 0
vsize: 449572
[startup+210.133 s]
Raw data (loadavg): 1.04 0.93 0.90 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109776 0 0 0 20744 271 0 0 25 0 1 0 487704773 460886016 98251 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112521 98251 603 41 0 112480 0
vsize: 450084
[startup+220.133 s]
Raw data (loadavg): 1.03 0.94 0.90 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109882 0 0 0 21743 272 0 0 25 0 1 0 487704773 461279232 98357 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112617 98357 603 41 0 112576 0
vsize: 450468
[startup+230.133 s]
Raw data (loadavg): 1.03 0.94 0.90 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109944 0 0 0 22744 272 0 0 25 0 1 0 487704773 461549568 98419 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112683 98419 603 41 0 112642 0
vsize: 450732
[startup+240.133 s]
Raw data (loadavg): 1.02 0.94 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 109996 0 0 0 23743 272 0 0 25 0 1 0 487704773 461856768 98471 4294967295 134512640 134672761 3221224544 3221223712 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112758 98471 603 41 0 112717 0
vsize: 451032
[startup+250.142 s]
Raw data (loadavg): 1.02 0.94 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 110107 0 0 0 24744 272 0 0 25 0 1 0 487704773 462258176 98582 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112856 98582 603 41 0 112815 0
vsize: 451424
[startup+260.252 s]
Raw data (loadavg): 1.02 0.94 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 110218 0 0 0 25755 272 0 0 25 0 1 0 487704773 462651392 98693 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112952 98693 603 41 0 112911 0
vsize: 451808
[startup+270.251 s]
Raw data (loadavg): 1.01 0.94 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 110507 0 0 0 26755 273 0 0 25 0 1 0 487704773 463867904 98982 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113249 98982 603 41 0 113208 0
vsize: 452996
[startup+280.252 s]
Raw data (loadavg): 1.01 0.95 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 110647 0 0 0 27755 273 0 0 25 0 1 0 487704773 464404480 99122 4294967295 134512640 134672761 3221224544 3221223688 134565969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113380 99122 603 41 0 113339 0
vsize: 453520
[startup+290.253 s]
Raw data (loadavg): 1.09 0.96 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 110804 0 0 0 28755 274 0 0 25 0 1 0 487704773 465055744 99279 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113539 99279 603 41 0 113498 0
vsize: 454156
[startup+300.253 s]
Raw data (loadavg): 1.07 0.96 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 110984 0 0 0 29754 274 0 0 25 0 1 0 487704773 465829888 99459 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113728 99459 603 41 0 113687 0
vsize: 454912
[startup+310.253 s]
Raw data (loadavg): 1.06 0.96 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 111072 0 0 0 30754 274 0 0 25 0 1 0 487704773 466231296 99547 4294967295 134512640 134672761 3221224544 3221223728 134615472 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113826 99547 603 41 0 113785 0
vsize: 455304
[startup+320.253 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 111130 0 0 0 31754 274 0 0 25 0 1 0 487704773 466362368 99605 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113858 99605 603 41 0 113817 0
vsize: 455432
[startup+330.253 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 111293 0 0 0 32754 275 0 0 25 0 1 0 487704773 467021824 99768 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114019 99768 603 41 0 113978 0
vsize: 456076
[startup+340.253 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 111483 0 0 0 33754 275 0 0 25 0 1 0 487704773 467820544 99958 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114214 99958 603 41 0 114173 0
vsize: 456856
[startup+350.254 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 111628 0 0 0 34754 276 0 0 25 0 1 0 487704773 468484096 100103 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114376 100103 603 41 0 114335 0
vsize: 457504
[startup+360.255 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 111806 0 0 0 35754 276 0 0 25 0 1 0 487704773 469139456 100281 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114536 100281 603 41 0 114495 0
vsize: 458144
[startup+370.254 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 111983 0 0 0 36754 276 0 0 25 0 1 0 487704773 469942272 100458 4294967295 134512640 134672761 3221224544 3221223584 134612571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114732 100458 603 41 0 114691 0
vsize: 458928
[startup+380.255 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 112333 0 0 0 37753 277 0 0 25 0 1 0 487704773 471277568 100808 4294967295 134512640 134672761 3221224544 3221223728 134616020 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115058 100808 603 41 0 115017 0
vsize: 460232
[startup+390.255 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 140060 0 0 0 38686 343 0 0 25 0 1 0 487704773 497491968 106869 4294967295 134512640 134672761 3221224544 3216513568 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121458 106869 603 41 0 121417 0
vsize: 485832
[startup+400.256 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 169158 0 0 0 39622 408 0 0 25 0 1 0 487704773 578949120 126739 4294967295 134512640 134672761 3221224544 3215192024 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 141345 126739 603 41 0 141304 0
vsize: 565380
[startup+410.256 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 200463 0 0 0 40549 481 0 0 25 0 1 0 487704773 663908352 147498 4294967295 134512640 134672761 3221224544 3214577824 134594047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 162087 147498 603 41 0 162046 0
vsize: 648348
[startup+420.256 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 215052 0 0 0 41517 513 0 0 25 0 1 0 487704773 723787776 162087 4294967295 134512640 134672761 3221224544 3214938200 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 176706 162087 603 41 0 176665 0
vsize: 706824
[startup+430.256 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 264216 0 0 0 42396 635 0 0 25 0 1 0 487704773 838696960 190160 4294967295 134512640 134672761 3221224544 3214191328 134594077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 204760 190160 603 41 0 204719 0
vsize: 819040
[startup+440.256 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 288208 0 0 0 43342 689 0 0 25 0 1 0 487704773 937377792 212834 4294967295 134512640 134672761 3221224544 3215332720 134522994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 228852 212835 603 41 0 228811 0
vsize: 915408
[startup+441.342 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 29604
Raw data (stat): 29604 (minisat+) R 29603 20937 20936 0 -1 0 288208 0 0 0 43342 689 0 0 25 0 1 0 487704773 937377792 212834 4294967295 134512640 134672761 3221224544 3215332720 134522994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 228852 212835 603 41 0 228811 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 441.342
CPU time (s): 441.404
CPU user time (s): 434.061
CPU system time (s): 7.34288
CPU usage (%): 100.014
Max. virtual memory (Kb): 915408
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####