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 21802

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        246692 kB
Buffers:         31532 kB
Cached:         728368 kB
SwapCached:         68 kB
Active:         214816 kB
Inactive:       548016 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        246440 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6880 kB
Slab:            19472 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 01:18:23 (client local time) WITH STATUS 0 IN 1200.39 SECONDS
stats: 13077 7 1200.39 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.93 0.90 0.89 1/54 14054
Raw data (stat): 14054 (runsolver) D 14053 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 549586102 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99977 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 14357 0 0 0 953 36 0 0 25 0 1 0 549586102 59789312 12585 4294967295 134512640 134672761 3221224544 3221207088 134594226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14597 12585 603 41 0 14556 0
vsize: 58388
[startup+20.0035 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 56385 0 0 0 1850 139 0 0 25 0 1 0 549586102 260452352 54581 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63587 54581 603 41 0 63546 0
vsize: 254348
[startup+30.0042 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 56794 0 0 0 2849 140 0 0 25 0 1 0 549586102 260587520 54990 4294967295 134512640 134672761 3221224544 3221223648 134559841 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.0078 s]
Raw data (loadavg): 0.96 0.91 0.90 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 56845 0 0 0 3850 140 0 0 25 0 1 0 549586102 260722688 55041 4294967295 134512640 134672761 3221224544 3221223744 134557885 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.0084 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 56889 0 0 0 4850 140 0 0 25 0 1 0 549586102 260857856 55085 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63686 55085 603 41 0 63645 0
vsize: 254744
[startup+60.0081 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 56973 0 0 0 5850 140 0 0 25 0 1 0 549586102 261271552 55169 4294967295 134512640 134672761 3221224544 3221223680 134560683 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.0078 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57027 0 0 0 6850 140 0 0 25 0 1 0 549586102 261537792 55223 4294967295 134512640 134672761 3221224544 3221223712 134560942 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.0155 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57073 0 0 0 7850 141 0 0 25 0 1 0 549586102 261668864 55269 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63884 55269 603 41 0 63843 0
vsize: 255536
[startup+90.0152 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57171 0 0 0 8850 141 0 0 25 0 1 0 549586102 262098944 55367 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63989 55367 603 41 0 63948 0
vsize: 255956
[startup+100.016 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 14054
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57264 0 0 0 9850 141 0 0 25 0 1 0 549586102 262369280 55460 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64055 55460 603 41 0 64014 0
vsize: 256220
[startup+110.027 s]
Raw data (loadavg): 0.99 0.93 0.90 2/57 14063
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57321 0 0 0 10850 141 0 0 25 0 1 0 549586102 262635520 55517 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64120 55517 603 41 0 64079 0
vsize: 256480
[startup+120.058 s]
Raw data (loadavg): 1.22 0.98 0.92 2/56 14095
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57392 0 0 0 11852 143 0 0 25 0 1 0 549586102 262905856 55588 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64186 55588 603 41 0 64145 0
vsize: 256744
[startup+130.058 s]
Raw data (loadavg): 1.18 0.98 0.92 2/54 14107
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57483 0 0 0 12851 144 0 0 25 0 1 0 549586102 263335936 55679 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64291 55679 603 41 0 64250 0
vsize: 257164
[startup+140.058 s]
Raw data (loadavg): 1.15 0.98 0.92 2/54 14107
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57546 0 0 0 13851 144 0 0 25 0 1 0 549586102 263471104 55742 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64324 55742 603 41 0 64283 0
vsize: 257296
[startup+150.063 s]
Raw data (loadavg): 1.13 0.98 0.92 2/54 14107
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57632 0 0 0 14852 144 0 0 25 0 1 0 549586102 263880704 55828 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64424 55828 603 41 0 64383 0
vsize: 257696
[startup+160.174 s]
Raw data (loadavg): 1.11 0.98 0.92 2/54 14107
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57697 0 0 0 15863 144 0 0 25 0 1 0 549586102 264151040 55893 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64490 55893 603 41 0 64449 0
vsize: 257960
[startup+170.173 s]
Raw data (loadavg): 1.09 0.98 0.92 2/54 14107
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57782 0 0 0 16863 144 0 0 25 0 1 0 549586102 264421376 55978 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64556 55978 603 41 0 64515 0
vsize: 258224
[startup+180.193 s]
Raw data (loadavg): 1.08 0.98 0.92 2/54 14107
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57855 0 0 0 17864 145 0 0 25 0 1 0 549586102 264699904 56051 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64624 56051 603 41 0 64583 0
vsize: 258496
[startup+190.193 s]
Raw data (loadavg): 1.06 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 57933 0 0 0 18864 145 0 0 25 0 1 0 549586102 265105408 56129 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64723 56129 603 41 0 64682 0
vsize: 258892
[startup+200.194 s]
Raw data (loadavg): 1.05 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58013 0 0 0 19864 146 0 0 25 0 1 0 549586102 265379840 56209 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64790 56209 603 41 0 64749 0
vsize: 259160
[startup+210.194 s]
Raw data (loadavg): 1.05 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58128 0 0 0 20864 146 0 0 25 0 1 0 549586102 265932800 56324 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64925 56324 603 41 0 64884 0
vsize: 259700
[startup+220.194 s]
Raw data (loadavg): 1.04 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58197 0 0 0 21864 146 0 0 25 0 1 0 549586102 266207232 56393 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64992 56393 603 41 0 64951 0
vsize: 259968
[startup+230.194 s]
Raw data (loadavg): 1.03 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58270 0 0 0 22864 146 0 0 25 0 1 0 549586102 266477568 56466 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65058 56466 603 41 0 65017 0
vsize: 260232
[startup+240.194 s]
Raw data (loadavg): 1.03 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58336 0 0 0 23864 146 0 0 25 0 1 0 549586102 266747904 56532 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65124 56532 603 41 0 65083 0
vsize: 260496
[startup+250.195 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58413 0 0 0 24864 147 0 0 25 0 1 0 549586102 267018240 56609 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65190 56609 603 41 0 65149 0
vsize: 260760
[startup+260.195 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58482 0 0 0 25864 147 0 0 25 0 1 0 549586102 267288576 56678 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65256 56678 603 41 0 65215 0
vsize: 261024
[startup+270.195 s]
Raw data (loadavg): 1.02 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58573 0 0 0 26864 147 0 0 25 0 1 0 549586102 267558912 56769 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65322 56769 603 41 0 65281 0
vsize: 261288
[startup+280.195 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58667 0 0 0 27863 147 0 0 25 0 1 0 549586102 267968512 56863 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65422 56863 603 41 0 65381 0
vsize: 261688
[startup+290.195 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58760 0 0 0 28864 147 0 0 25 0 1 0 549586102 268374016 56956 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65521 56956 603 41 0 65480 0
vsize: 262084
[startup+300.196 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58855 0 0 0 29864 148 0 0 25 0 1 0 549586102 268779520 57051 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65620 57051 603 41 0 65579 0
vsize: 262480
[startup+310.197 s]
Raw data (loadavg): 1.01 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 58979 0 0 0 30864 148 0 0 25 0 1 0 549586102 269049856 57175 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65686 57175 603 41 0 65645 0
vsize: 262744
[startup+320.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59075 0 0 0 31863 148 0 0 25 0 1 0 549586102 269467648 57271 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65788 57271 603 41 0 65747 0
vsize: 263152
[startup+330.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59174 0 0 0 32863 149 0 0 25 0 1 0 549586102 269881344 57370 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65889 57370 603 41 0 65848 0
vsize: 263556
[startup+340.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59267 0 0 0 33862 150 0 0 25 0 1 0 549586102 270295040 57463 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65990 57463 603 41 0 65949 0
vsize: 263960
[startup+350.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59362 0 0 0 34862 150 0 0 25 0 1 0 549586102 270573568 57558 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66058 57558 603 41 0 66017 0
vsize: 264232
[startup+360.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59503 0 0 0 35861 151 0 0 25 0 1 0 549586102 271261696 57699 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66226 57699 603 41 0 66185 0
vsize: 264904
[startup+370.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59564 0 0 0 36861 151 0 0 25 0 1 0 549586102 271396864 57760 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66259 57760 603 41 0 66218 0
vsize: 265036
[startup+380.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59619 0 0 0 37861 151 0 0 25 0 1 0 549586102 271667200 57815 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66325 57815 603 41 0 66284 0
vsize: 265300
[startup+390.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59681 0 0 0 38861 151 0 0 25 0 1 0 549586102 271933440 57877 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66390 57877 603 41 0 66349 0
vsize: 265560
[startup+400.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59745 0 0 0 39861 152 0 0 25 0 1 0 549586102 272203776 57941 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66456 57941 603 41 0 66415 0
vsize: 265824
[startup+410.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59804 0 0 0 40861 152 0 0 25 0 1 0 549586102 272474112 58000 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66522 58000 603 41 0 66481 0
vsize: 266088
[startup+420.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59869 0 0 0 41861 152 0 0 25 0 1 0 549586102 272744448 58065 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66588 58065 603 41 0 66547 0
vsize: 266352
[startup+430.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14109
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 59929 0 0 0 42861 152 0 0 25 0 1 0 549586102 272879616 58125 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66621 58125 603 41 0 66580 0
vsize: 266484
[startup+440.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60030 0 0 0 43861 153 0 0 25 0 1 0 549586102 273285120 58226 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66720 58226 603 41 0 66679 0
vsize: 266880
[startup+450.198 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60099 0 0 0 44861 153 0 0 25 0 1 0 549586102 273690624 58295 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66819 58295 603 41 0 66778 0
vsize: 267276
[startup+460.198 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60155 0 0 0 45860 153 0 0 25 0 1 0 549586102 273825792 58351 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66852 58351 603 41 0 66811 0
vsize: 267408
[startup+470.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60240 0 0 0 46860 154 0 0 25 0 1 0 549586102 274231296 58436 4294967295 134512640 134672761 3221224544 3221223648 134559951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66951 58436 603 41 0 66910 0
vsize: 267804
[startup+480.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60343 0 0 0 47860 154 0 0 25 0 1 0 549586102 274669568 58539 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67058 58539 603 41 0 67017 0
vsize: 268232
[startup+490.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60458 0 0 0 48860 154 0 0 25 0 1 0 549586102 275099648 58654 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67163 58654 603 41 0 67122 0
vsize: 268652
[startup+500.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60528 0 0 0 49860 154 0 0 25 0 1 0 549586102 275369984 58724 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67229 58724 603 41 0 67188 0
vsize: 268916
[startup+510.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60599 0 0 0 50860 154 0 0 25 0 1 0 549586102 275693568 58795 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67308 58795 603 41 0 67267 0
vsize: 269232
[startup+520.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60694 0 0 0 51860 155 0 0 25 0 1 0 549586102 276099072 58890 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67407 58890 603 41 0 67366 0
vsize: 269628
[startup+530.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60813 0 0 0 52860 155 0 0 25 0 1 0 549586102 276647936 59009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67541 59009 603 41 0 67500 0
vsize: 270164
[startup+540.198 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60877 0 0 0 53859 156 0 0 25 0 1 0 549586102 276918272 59073 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67607 59073 603 41 0 67566 0
vsize: 270428
[startup+550.198 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60946 0 0 0 54859 156 0 0 25 0 1 0 549586102 277184512 59142 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67672 59142 603 41 0 67631 0
vsize: 270688
[startup+560.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 60999 0 0 0 55859 156 0 0 25 0 1 0 549586102 277319680 59195 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67705 59195 603 41 0 67664 0
vsize: 270820
[startup+570.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61056 0 0 0 56859 156 0 0 25 0 1 0 549586102 277590016 59252 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67771 59252 603 41 0 67730 0
vsize: 271084
[startup+580.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61117 0 0 0 57859 156 0 0 25 0 1 0 549586102 277860352 59313 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67837 59313 603 41 0 67796 0
vsize: 271348
[startup+590.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61228 0 0 0 58858 157 0 0 25 0 1 0 549586102 278278144 59424 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67939 59424 603 41 0 67898 0
vsize: 271756
[startup+600.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61283 0 0 0 59859 157 0 0 25 0 1 0 549586102 278548480 59479 4294967295 134512640 134672761 3221224544 3221223648 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68005 59479 603 41 0 67964 0
vsize: 272020
[startup+610.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61371 0 0 0 60858 157 0 0 25 0 1 0 549586102 278827008 59567 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68073 59567 603 41 0 68032 0
vsize: 272292
[startup+620.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61460 0 0 0 61858 157 0 0 25 0 1 0 549586102 279236608 59656 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68173 59656 603 41 0 68132 0
vsize: 272692
[startup+630.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61551 0 0 0 62858 158 0 0 25 0 1 0 549586102 279646208 59747 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68273 59747 603 41 0 68232 0
vsize: 273092
[startup+640.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61659 0 0 0 63858 158 0 0 25 0 1 0 549586102 280055808 59855 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68373 59855 603 41 0 68332 0
vsize: 273492
[startup+650.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61755 0 0 0 64858 159 0 0 25 0 1 0 549586102 280461312 59951 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68472 59951 603 41 0 68431 0
vsize: 273888
[startup+660.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61863 0 0 0 65858 159 0 0 25 0 1 0 549586102 280895488 60059 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68578 60059 603 41 0 68537 0
vsize: 274312
[startup+670.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 61944 0 0 0 66857 159 0 0 25 0 1 0 549586102 281169920 60140 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68645 60140 603 41 0 68604 0
vsize: 274580
[startup+680.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62025 0 0 0 67857 159 0 0 25 0 1 0 549586102 281575424 60221 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68744 60221 603 41 0 68703 0
vsize: 274976
[startup+690.196 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62102 0 0 0 68858 159 0 0 25 0 1 0 549586102 281845760 60298 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68810 60298 603 41 0 68769 0
vsize: 275240
[startup+700.197 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62151 0 0 0 69858 160 0 0 25 0 1 0 549586102 282116096 60347 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68876 60347 603 41 0 68835 0
vsize: 275504
[startup+710.198 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62211 0 0 0 70857 160 0 0 25 0 1 0 549586102 282251264 60407 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68909 60407 603 41 0 68868 0
vsize: 275636
[startup+720.198 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62314 0 0 0 71857 160 0 0 25 0 1 0 549586102 282796032 60510 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69042 60510 603 41 0 69001 0
vsize: 276168
[startup+730.198 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62391 0 0 0 72857 161 0 0 25 0 1 0 549586102 283066368 60587 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69108 60587 603 41 0 69067 0
vsize: 276432
[startup+740.199 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62452 0 0 0 73857 161 0 0 25 0 1 0 549586102 283332608 60648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69173 60648 603 41 0 69132 0
vsize: 276692
[startup+750.199 s]
Raw data (loadavg): 1.00 0.98 0.92 3/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62525 0 0 0 74857 161 0 0 25 0 1 0 549586102 283598848 60721 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69238 60721 603 41 0 69197 0
vsize: 276952
[startup+760.199 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62644 0 0 0 75857 162 0 0 25 0 1 0 549586102 284012544 60840 4294967295 134512640 134672761 3221224544 3221223648 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69339 60840 603 41 0 69298 0
vsize: 277356
[startup+770.199 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62712 0 0 0 76855 162 0 0 25 0 1 0 549586102 284422144 60908 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69439 60908 603 41 0 69398 0
vsize: 277756
[startup+780.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62787 0 0 0 77854 162 0 0 25 0 1 0 549586102 284692480 60983 4294967295 134512640 134672761 3221224544 3221223696 134565132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69505 60983 603 41 0 69464 0
vsize: 278020
[startup+790.199 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62879 0 0 0 78855 162 0 0 25 0 1 0 549586102 284983296 61075 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69576 61075 603 41 0 69535 0
vsize: 278304
[startup+800.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 62928 0 0 0 79854 163 0 0 25 0 1 0 549586102 285253632 61124 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69642 61124 603 41 0 69601 0
vsize: 278568
[startup+810.201 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63011 0 0 0 80854 163 0 0 25 0 1 0 549586102 285532160 61207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69710 61207 603 41 0 69669 0
vsize: 278840
[startup+820.201 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63093 0 0 0 81854 163 0 0 25 0 1 0 549586102 285941760 61289 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69810 61289 603 41 0 69769 0
vsize: 279240
[startup+830.201 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63170 0 0 0 82854 163 0 0 25 0 1 0 549586102 286212096 61366 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69876 61366 603 41 0 69835 0
vsize: 279504
[startup+840.201 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63293 0 0 0 83854 164 0 0 25 0 1 0 549586102 286756864 61489 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70009 61489 603 41 0 69968 0
vsize: 280036
[startup+850.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63359 0 0 0 84854 164 0 0 25 0 1 0 549586102 287027200 61555 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70075 61555 603 41 0 70034 0
vsize: 280300
[startup+860.201 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63415 0 0 0 85854 164 0 0 25 0 1 0 549586102 287162368 61611 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70108 61611 603 41 0 70067 0
vsize: 280432
[startup+870.201 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63488 0 0 0 86854 164 0 0 25 0 1 0 549586102 287563776 61684 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70206 61684 603 41 0 70165 0
vsize: 280824
[startup+880.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63542 0 0 0 87854 165 0 0 25 0 1 0 549586102 287707136 61738 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70241 61738 603 41 0 70200 0
vsize: 280964
[startup+890.201 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63613 0 0 0 88854 165 0 0 25 0 1 0 549586102 287977472 61809 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70307 61809 603 41 0 70266 0
vsize: 281228
[startup+900.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63671 0 0 0 89854 165 0 0 25 0 1 0 549586102 288243712 61867 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70372 61867 603 41 0 70331 0
vsize: 281488
[startup+910.203 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63758 0 0 0 90854 165 0 0 25 0 1 0 549586102 288649216 61954 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70471 61954 603 41 0 70430 0
vsize: 281884
[startup+920.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63823 0 0 0 91854 165 0 0 25 0 1 0 549586102 288919552 62019 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70537 62019 603 41 0 70496 0
vsize: 282148
[startup+930.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 63891 0 0 0 92853 166 0 0 25 0 1 0 549586102 289189888 62087 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70603 62087 603 41 0 70562 0
vsize: 282412
[startup+940.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64003 0 0 0 93853 166 0 0 25 0 1 0 549586102 289595392 62199 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70702 62199 603 41 0 70661 0
vsize: 282808
[startup+950.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64092 0 0 0 94853 166 0 0 25 0 1 0 549586102 289996800 62288 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70800 62288 603 41 0 70759 0
vsize: 283200
[startup+960.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64225 0 0 0 95853 167 0 0 25 0 1 0 549586102 290541568 62421 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70933 62421 603 41 0 70892 0
vsize: 283732
[startup+970.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64307 0 0 0 96853 167 0 0 25 0 1 0 549586102 290811904 62503 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70999 62503 603 41 0 70958 0
vsize: 283996
[startup+980.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64383 0 0 0 97853 167 0 0 25 0 1 0 549586102 291217408 62579 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71098 62579 603 41 0 71057 0
vsize: 284392
[startup+990.202 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64467 0 0 0 98853 167 0 0 25 0 1 0 549586102 291483648 62663 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71163 62663 603 41 0 71122 0
vsize: 284652
[startup+1000.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64548 0 0 0 99853 168 0 0 25 0 1 0 549586102 291897344 62744 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71264 62744 603 41 0 71223 0
vsize: 285056
[startup+1010.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64660 0 0 0 100853 168 0 0 25 0 1 0 549586102 292302848 62856 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71363 62856 603 41 0 71322 0
vsize: 285452
[startup+1020.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64726 0 0 0 101852 169 0 0 25 0 1 0 549586102 292696064 62922 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71459 62922 603 41 0 71418 0
vsize: 285836
[startup+1030.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64810 0 0 0 102852 169 0 0 25 0 1 0 549586102 293105664 63006 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71559 63006 603 41 0 71518 0
vsize: 286236
[startup+1040.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64882 0 0 0 103852 170 0 0 25 0 1 0 549586102 293371904 63078 4294967295 134512640 134672761 3221224544 3221223696 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71624 63078 603 41 0 71583 0
vsize: 286496
[startup+1050.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 64957 0 0 0 104852 170 0 0 25 0 1 0 549586102 293634048 63153 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71688 63153 603 41 0 71647 0
vsize: 286752
[startup+1060.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65065 0 0 0 105852 170 0 0 25 0 1 0 549586102 294072320 63261 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71795 63261 603 41 0 71754 0
vsize: 287180
[startup+1070.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65146 0 0 0 106852 171 0 0 25 0 1 0 549586102 294481920 63342 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71895 63342 603 41 0 71854 0
vsize: 287580
[startup+1080.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65224 0 0 0 107852 171 0 0 25 0 1 0 549586102 294752256 63420 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71961 63420 603 41 0 71920 0
vsize: 287844
[startup+1090.2 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65274 0 0 0 108852 171 0 0 25 0 1 0 549586102 294887424 63470 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71994 63470 603 41 0 71953 0
vsize: 287976
[startup+1100.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65346 0 0 0 109852 171 0 0 25 0 1 0 549586102 295292928 63542 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72093 63542 603 41 0 72052 0
vsize: 288372
[startup+1110.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65415 0 0 0 110852 171 0 0 25 0 1 0 549586102 295563264 63611 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72159 63611 603 41 0 72118 0
vsize: 288636
[startup+1120.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65495 0 0 0 111852 171 0 0 25 0 1 0 549586102 295825408 63691 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72223 63691 603 41 0 72182 0
vsize: 288892
[startup+1130.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65589 0 0 0 112852 172 0 0 25 0 1 0 549586102 296243200 63785 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72325 63785 603 41 0 72284 0
vsize: 289300
[startup+1140.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65668 0 0 0 113852 172 0 0 25 0 1 0 549586102 296513536 63864 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72391 63864 603 41 0 72350 0
vsize: 289564
[startup+1150.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65768 0 0 0 114851 173 0 0 25 0 1 0 549586102 296927232 63964 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72492 63964 603 41 0 72451 0
vsize: 289968
[startup+1160.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65837 0 0 0 115852 173 0 0 25 0 1 0 549586102 297193472 64033 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72557 64033 603 41 0 72516 0
vsize: 290228
[startup+1170.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65923 0 0 0 116851 173 0 0 25 0 1 0 549586102 297594880 64119 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72655 64119 603 41 0 72614 0
vsize: 290620
[startup+1180.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 65998 0 0 0 117851 173 0 0 25 0 1 0 549586102 297865216 64194 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72721 64194 603 41 0 72680 0
vsize: 290884
[startup+1190.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 66128 0 0 0 118851 174 0 0 25 0 1 0 549586102 298409984 64324 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72854 64324 603 41 0 72813 0
vsize: 291416
[startup+1200.21 s]
Raw data (loadavg): 1.00 0.98 0.92 2/54 14111
Raw data (stat): 14054 (minisat+) R 14053 22612 22611 0 -1 0 66192 0 0 0 119851 174 0 0 25 0 1 0 549586102 298684416 64388 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72921 64388 603 41 0 72880 0
vsize: 291684
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.34 s]
Raw data (loadavg): 1.00 0.98 0.92 1/54 14111
Raw data (stat): 14054 (minisat+) Z 14053 22612 22611 0 -1 12 66194 0 0 0 119851 187 0 0 25 0 1 0 549586102 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.34
CPU time (s): 1200.39
CPU user time (s): 1198.52
CPU system time (s): 1.87171
CPU usage (%): 100.004
Max. virtual memory (Kb): 291684
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####