PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 14:49:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18062 boxname=wulflinc31 idbench=1390 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  bc46e72682d969c09e6f4028df473a45  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-t1717.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-t1717.opb
IDLAUNCH: 18062
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        570696 kB
Buffers:         34316 kB
Cached:         401092 kB
SwapCached:        540 kB
Active:         149136 kB
Inactive:       288296 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        570444 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20880 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:09:17 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 18062 7 1200.36 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.85 0.94 0.92 2/54 27556
Raw data (stat): 27556 (runsolver) R 27555 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545911933 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.88 0.94 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 14414 0 0 0 958 40 0 0 25 0 1 0 545911933 59924480 12642 4294967295 134512640 134672761 3221224624 3221174032 134592272 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14630 12642 603 41 0 14589 0
vsize: 58520
[startup+20.0026 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 56364 0 0 0 1859 140 0 0 25 0 1 0 545911933 260452352 54560 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63587 54560 603 41 0 63546 0
vsize: 254348
[startup+30.0029 s]
Raw data (loadavg): 0.91 0.94 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 56715 0 0 0 2857 142 0 0 25 0 1 0 545911933 260587520 54911 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63620 54911 603 41 0 63579 0
vsize: 254480
[startup+40.0037 s]
Raw data (loadavg): 0.92 0.94 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 56845 0 0 0 3856 142 0 0 25 0 1 0 545911933 260722688 55041 4294967295 134512640 134672761 3221224624 3221223772 1074733099 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.0044 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 56879 0 0 0 4856 143 0 0 25 0 1 0 545911933 260857856 55075 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63686 55075 603 41 0 63645 0
vsize: 254744
[startup+60.0048 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 56967 0 0 0 5856 144 0 0 25 0 1 0 545911933 261271552 55163 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63787 55163 603 41 0 63746 0
vsize: 255148
[startup+70.0057 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57019 0 0 0 6855 144 0 0 25 0 1 0 545911933 261402624 55215 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63819 55215 603 41 0 63778 0
vsize: 255276
[startup+80.0062 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57062 0 0 0 7854 145 0 0 25 0 1 0 545911933 261668864 55258 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63884 55258 603 41 0 63843 0
vsize: 255536
[startup+90.0066 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57160 0 0 0 8853 146 0 0 25 0 1 0 545911933 262098944 55356 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63989 55356 603 41 0 63948 0
vsize: 255956
[startup+100.007 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57250 0 0 0 9853 146 0 0 25 0 1 0 545911933 262369280 55446 4294967295 134512640 134672761 3221224624 3221223808 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64055 55446 603 41 0 64014 0
vsize: 256220
[startup+110.015 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57313 0 0 0 10853 147 0 0 25 0 1 0 545911933 262504448 55509 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64088 55509 603 41 0 64047 0
vsize: 256352
[startup+120.016 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57368 0 0 0 11853 147 0 0 25 0 1 0 545911933 262770688 55564 4294967295 134512640 134672761 3221224624 3221223748 134565986 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64153 55564 603 41 0 64112 0
vsize: 256612
[startup+130.031 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57459 0 0 0 12854 148 0 0 25 0 1 0 545911933 263188480 55655 4294967295 134512640 134672761 3221224624 3221223748 134566151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64255 55655 603 41 0 64214 0
vsize: 257020
[startup+140.039 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57517 0 0 0 13853 149 0 0 25 0 1 0 545911933 263471104 55713 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64324 55713 603 41 0 64283 0
vsize: 257296
[startup+150.049 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57599 0 0 0 14854 149 0 0 25 0 1 0 545911933 263745536 55795 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64391 55795 603 41 0 64350 0
vsize: 257564
[startup+160.05 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57678 0 0 0 15853 150 0 0 25 0 1 0 545911933 264015872 55874 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64457 55874 603 41 0 64416 0
vsize: 257828
[startup+170.051 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57726 0 0 0 16852 151 0 0 25 0 1 0 545911933 264286208 55922 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64523 55922 603 41 0 64482 0
vsize: 258092
[startup+180.052 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57823 0 0 0 17851 152 0 0 25 0 1 0 545911933 264699904 56019 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64624 56019 603 41 0 64583 0
vsize: 258496
[startup+190.052 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57893 0 0 0 18851 153 0 0 25 0 1 0 545911933 264970240 56089 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64690 56089 603 41 0 64649 0
vsize: 258760
[startup+200.052 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 57976 0 0 0 19850 154 0 0 25 0 1 0 545911933 265240576 56172 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64756 56172 603 41 0 64715 0
vsize: 259024
[startup+210.053 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58065 0 0 0 20850 154 0 0 25 0 1 0 545911933 265650176 56261 4294967295 134512640 134672761 3221224624 3221223728 134559981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64856 56261 603 41 0 64815 0
vsize: 259424
[startup+220.066 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58160 0 0 0 21850 155 0 0 25 0 1 0 545911933 266067968 56356 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64958 56356 603 41 0 64917 0
vsize: 259832
[startup+230.066 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58236 0 0 0 22849 156 0 0 25 0 1 0 545911933 266342400 56432 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65025 56432 603 41 0 64984 0
vsize: 260100
[startup+240.067 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58294 0 0 0 23848 157 0 0 25 0 1 0 545911933 266612736 56490 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65091 56490 603 41 0 65050 0
vsize: 260364
[startup+250.068 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58370 0 0 0 24848 158 0 0 25 0 1 0 545911933 266883072 56566 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65157 56566 603 41 0 65116 0
vsize: 260628
[startup+260.068 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58437 0 0 0 25847 158 0 0 25 0 1 0 545911933 267153408 56633 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65223 56633 603 41 0 65182 0
vsize: 260892
[startup+270.081 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58506 0 0 0 26848 159 0 0 25 0 1 0 545911933 267423744 56702 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65289 56702 603 41 0 65248 0
vsize: 261156
[startup+280.082 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58598 0 0 0 27847 160 0 0 25 0 1 0 545911933 267694080 56794 4294967295 134512640 134672761 3221224624 3221223728 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65355 56794 603 41 0 65314 0
vsize: 261420
[startup+290.082 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58690 0 0 0 28847 161 0 0 25 0 1 0 545911933 268103680 56886 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65455 56886 603 41 0 65414 0
vsize: 261820
[startup+300.083 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58782 0 0 0 29846 161 0 0 25 0 1 0 545911933 268509184 56978 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65554 56978 603 41 0 65513 0
vsize: 262216
[startup+310.084 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 58876 0 0 0 30845 162 0 0 25 0 1 0 545911933 268914688 57072 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65653 57072 603 41 0 65612 0
vsize: 262612
[startup+320.085 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59015 0 0 0 31845 163 0 0 25 0 1 0 545911933 269197312 57211 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65722 57211 603 41 0 65681 0
vsize: 262888
[startup+330.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59089 0 0 0 32844 164 0 0 25 0 1 0 545911933 269467648 57285 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65788 57285 603 41 0 65747 0
vsize: 263152
[startup+340.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59195 0 0 0 33844 164 0 0 25 0 1 0 545911933 269881344 57391 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65889 57391 603 41 0 65848 0
vsize: 263556
[startup+350.086 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59287 0 0 0 34843 165 0 0 25 0 1 0 545911933 270295040 57483 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65990 57483 603 41 0 65949 0
vsize: 263960
[startup+360.088 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59381 0 0 0 35843 166 0 0 25 0 1 0 545911933 270708736 57577 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66091 57577 603 41 0 66050 0
vsize: 264364
[startup+370.089 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59508 0 0 0 36842 167 0 0 25 0 1 0 545911933 271261696 57704 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66226 57704 603 41 0 66185 0
vsize: 264904
[startup+380.089 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59564 0 0 0 37842 167 0 0 25 0 1 0 545911933 271396864 57760 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66259 57760 603 41 0 66218 0
vsize: 265036
[startup+390.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59621 0 0 0 38841 168 0 0 25 0 1 0 545911933 271667200 57817 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66325 57817 603 41 0 66284 0
vsize: 265300
[startup+400.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59681 0 0 0 39841 168 0 0 25 0 1 0 545911933 271933440 57877 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66390 57877 603 41 0 66349 0
vsize: 265560
[startup+410.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59745 0 0 0 40840 169 0 0 25 0 1 0 545911933 272203776 57941 4294967295 134512640 134672761 3221224624 3221223748 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66456 57941 603 41 0 66415 0
vsize: 265824
[startup+420.091 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59803 0 0 0 41840 170 0 0 25 0 1 0 545911933 272474112 57999 4294967295 134512640 134672761 3221224624 3221223792 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66522 57999 603 41 0 66481 0
vsize: 266088
[startup+430.092 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59861 0 0 0 42839 170 0 0 25 0 1 0 545911933 272609280 58057 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66555 58057 603 41 0 66514 0
vsize: 266220
[startup+440.092 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 59926 0 0 0 43838 171 0 0 25 0 1 0 545911933 272879616 58122 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66621 58122 603 41 0 66580 0
vsize: 266484
[startup+450.093 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60014 0 0 0 44838 172 0 0 25 0 1 0 545911933 273285120 58210 4294967295 134512640 134672761 3221224624 3221223728 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66720 58210 603 41 0 66679 0
vsize: 266880
[startup+460.094 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60095 0 0 0 45838 172 0 0 25 0 1 0 545911933 273555456 58291 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66786 58291 603 41 0 66745 0
vsize: 267144
[startup+470.095 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60148 0 0 0 46837 172 0 0 25 0 1 0 545911933 273825792 58344 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66852 58344 603 41 0 66811 0
vsize: 267408
[startup+480.095 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60215 0 0 0 47837 173 0 0 25 0 1 0 545911933 274096128 58411 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66918 58411 603 41 0 66877 0
vsize: 267672
[startup+490.096 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60314 0 0 0 48836 174 0 0 25 0 1 0 545911933 274526208 58510 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67023 58510 603 41 0 66982 0
vsize: 268092
[startup+500.096 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60438 0 0 0 49836 174 0 0 25 0 1 0 545911933 274952192 58634 4294967295 134512640 134672761 3221224624 3221223728 134560013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67127 58634 603 41 0 67086 0
vsize: 268508
[startup+510.097 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60515 0 0 0 50836 175 0 0 25 0 1 0 545911933 275369984 58711 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67229 58711 603 41 0 67188 0
vsize: 268916
[startup+520.097 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60575 0 0 0 51835 175 0 0 25 0 1 0 545911933 275693568 58771 4294967295 134512640 134672761 3221224624 3221223728 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67308 58771 603 41 0 67267 0
vsize: 269232
[startup+530.098 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60669 0 0 0 52835 176 0 0 25 0 1 0 545911933 275963904 58865 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67374 58865 603 41 0 67333 0
vsize: 269496
[startup+540.099 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60766 0 0 0 53834 177 0 0 25 0 1 0 545911933 276373504 58962 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67474 58962 603 41 0 67433 0
vsize: 269896
[startup+550.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60840 0 0 0 54834 177 0 0 25 0 1 0 545911933 276783104 59036 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67574 59036 603 41 0 67533 0
vsize: 270296
[startup+560.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60925 0 0 0 55833 178 0 0 25 0 1 0 545911933 277049344 59121 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67639 59121 603 41 0 67598 0
vsize: 270556
[startup+570.101 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 60979 0 0 0 56833 179 0 0 25 0 1 0 545911933 277319680 59175 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67705 59175 603 41 0 67664 0
vsize: 270820
[startup+580.102 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61025 0 0 0 57832 179 0 0 25 0 1 0 545911933 277454848 59221 4294967295 134512640 134672761 3221224624 3221223760 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67738 59221 603 41 0 67697 0
vsize: 270952
[startup+590.102 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61092 0 0 0 58832 179 0 0 25 0 1 0 545911933 277725184 59288 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67804 59288 603 41 0 67763 0
vsize: 271216
[startup+600.103 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61151 0 0 0 59832 180 0 0 25 0 1 0 545911933 277995520 59347 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67870 59347 603 41 0 67829 0
vsize: 271480
[startup+610.104 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61248 0 0 0 60831 180 0 0 25 0 1 0 545911933 278413312 59444 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67972 59444 603 41 0 67931 0
vsize: 271888
[startup+620.105 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61326 0 0 0 61831 181 0 0 25 0 1 0 545911933 278691840 59522 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68040 59522 603 41 0 67999 0
vsize: 272160
[startup+630.106 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61409 0 0 0 62830 182 0 0 25 0 1 0 545911933 279101440 59605 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68140 59605 603 41 0 68099 0
vsize: 272560
[startup+640.106 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27556
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61493 0 0 0 63829 183 0 0 25 0 1 0 545911933 279371776 59689 4294967295 134512640 134672761 3221224624 3221223792 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68206 59689 603 41 0 68165 0
vsize: 272824
[startup+650.108 s]
Raw data (loadavg): 0.99 0.97 0.92 3/56 27578
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61585 0 0 0 64822 190 0 0 25 0 1 0 545911933 279781376 59781 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68306 59781 603 41 0 68265 0
vsize: 273224
[startup+660.108 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 27609
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61715 0 0 0 65821 192 0 0 25 0 1 0 545911933 280326144 59911 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68439 59911 603 41 0 68398 0
vsize: 273756
[startup+670.108 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 27609
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61810 0 0 0 66820 192 0 0 25 0 1 0 545911933 280756224 60006 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68544 60006 603 41 0 68503 0
vsize: 274176
[startup+680.108 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 27609
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61879 0 0 0 67820 193 0 0 25 0 1 0 545911933 280895488 60075 4294967295 134512640 134672761 3221224624 3221223760 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68578 60075 603 41 0 68537 0
vsize: 274312
[startup+690.108 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 27609
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 61974 0 0 0 68820 193 0 0 25 0 1 0 545911933 281305088 60170 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68678 60170 603 41 0 68637 0
vsize: 274712
[startup+700.109 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 27609
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62052 0 0 0 69820 193 0 0 25 0 1 0 545911933 281710592 60248 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68777 60248 603 41 0 68736 0
vsize: 275108
[startup+710.109 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 27609
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62110 0 0 0 70820 194 0 0 25 0 1 0 545911933 281845760 60306 4294967295 134512640 134672761 3221224624 3221223792 134564695 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68810 60306 603 41 0 68769 0
vsize: 275240
[startup+720.11 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 27609
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62162 0 0 0 71820 194 0 0 25 0 1 0 545911933 282116096 60358 4294967295 134512640 134672761 3221224624 3221223728 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68876 60358 603 41 0 68835 0
vsize: 275504
[startup+730.111 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62235 0 0 0 72820 194 0 0 25 0 1 0 545911933 282386432 60431 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68942 60431 603 41 0 68901 0
vsize: 275768
[startup+740.112 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62327 0 0 0 73819 195 0 0 25 0 1 0 545911933 282796032 60523 4294967295 134512640 134672761 3221224624 3221223748 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69042 60523 603 41 0 69001 0
vsize: 276168
[startup+750.113 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62404 0 0 0 74820 195 0 0 25 0 1 0 545911933 283066368 60600 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69108 60600 603 41 0 69067 0
vsize: 276432
[startup+760.113 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62469 0 0 0 75819 195 0 0 25 0 1 0 545911933 283332608 60665 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69173 60665 603 41 0 69132 0
vsize: 276692
[startup+770.114 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62543 0 0 0 76819 195 0 0 25 0 1 0 545911933 283598848 60739 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69238 60739 603 41 0 69197 0
vsize: 276952
[startup+780.114 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62657 0 0 0 77819 196 0 0 25 0 1 0 545911933 284151808 60853 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69373 60853 603 41 0 69332 0
vsize: 277492
[startup+790.114 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62727 0 0 0 78819 196 0 0 25 0 1 0 545911933 284422144 60923 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69439 60923 603 41 0 69398 0
vsize: 277756
[startup+800.115 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62799 0 0 0 79819 196 0 0 25 0 1 0 545911933 284692480 60995 4294967295 134512640 134672761 3221224624 3221223696 134553553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69505 60995 603 41 0 69464 0
vsize: 278020
[startup+810.116 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62884 0 0 0 80819 197 0 0 25 0 1 0 545911933 285118464 61080 4294967295 134512640 134672761 3221224624 3221223772 1074733103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69609 61080 603 41 0 69568 0
vsize: 278436
[startup+820.116 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 62935 0 0 0 81818 197 0 0 25 0 1 0 545911933 285253632 61131 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69642 61131 603 41 0 69601 0
vsize: 278568
[startup+830.117 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63017 0 0 0 82818 198 0 0 25 0 1 0 545911933 285532160 61213 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69710 61213 603 41 0 69669 0
vsize: 278840
[startup+840.118 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63101 0 0 0 83817 198 0 0 25 0 1 0 545911933 285941760 61297 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69810 61297 603 41 0 69769 0
vsize: 279240
[startup+850.119 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63171 0 0 0 84817 199 0 0 25 0 1 0 545911933 286212096 61367 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69876 61367 603 41 0 69835 0
vsize: 279504
[startup+860.12 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63293 0 0 0 85816 200 0 0 25 0 1 0 545911933 286756864 61489 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70009 61489 603 41 0 69968 0
vsize: 280036
[startup+870.12 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63359 0 0 0 86816 201 0 0 25 0 1 0 545911933 287027200 61555 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70075 61555 603 41 0 70034 0
vsize: 280300
[startup+880.121 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63410 0 0 0 87815 201 0 0 25 0 1 0 545911933 287162368 61606 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70108 61606 603 41 0 70067 0
vsize: 280432
[startup+890.121 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63477 0 0 0 88814 202 0 0 25 0 1 0 545911933 287428608 61673 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70173 61673 603 41 0 70132 0
vsize: 280692
[startup+900.122 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63533 0 0 0 89814 203 0 0 25 0 1 0 545911933 287707136 61729 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70241 61729 603 41 0 70200 0
vsize: 280964
[startup+910.123 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63602 0 0 0 90813 204 0 0 25 0 1 0 545911933 287977472 61798 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70307 61798 603 41 0 70266 0
vsize: 281228
[startup+920.123 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63663 0 0 0 91813 204 0 0 25 0 1 0 545911933 288243712 61859 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70372 61859 603 41 0 70331 0
vsize: 281488
[startup+930.124 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63742 0 0 0 92812 205 0 0 25 0 1 0 545911933 288514048 61938 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70438 61938 603 41 0 70397 0
vsize: 281752
[startup+940.125 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63809 0 0 0 93812 205 0 0 25 0 1 0 545911933 288784384 62005 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70504 62005 603 41 0 70463 0
vsize: 282016
[startup+950.126 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63873 0 0 0 94812 205 0 0 25 0 1 0 545911933 289054720 62069 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70570 62069 603 41 0 70529 0
vsize: 282280
[startup+960.126 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27611
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 63965 0 0 0 95812 206 0 0 25 0 1 0 545911933 289460224 62161 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70669 62161 603 41 0 70628 0
vsize: 282676
[startup+970.126 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64068 0 0 0 96811 207 0 0 25 0 1 0 545911933 289869824 62264 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70769 62264 603 41 0 70728 0
vsize: 283076
[startup+980.126 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64170 0 0 0 97811 207 0 0 25 0 1 0 545911933 290267136 62366 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70866 62366 603 41 0 70825 0
vsize: 283464
[startup+990.126 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64278 0 0 0 98810 207 0 0 25 0 1 0 545911933 290811904 62474 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70999 62474 603 41 0 70958 0
vsize: 283996
[startup+1000.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64364 0 0 0 99810 208 0 0 25 0 1 0 545911933 291082240 62560 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71065 62560 603 41 0 71024 0
vsize: 284260
[startup+1010.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64436 0 0 0 100811 208 0 0 25 0 1 0 545911933 291348480 62632 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71130 62632 603 41 0 71089 0
vsize: 284520
[startup+1020.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64519 0 0 0 101811 208 0 0 25 0 1 0 545911933 291762176 62715 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71231 62715 603 41 0 71190 0
vsize: 284924
[startup+1030.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64618 0 0 0 102811 208 0 0 25 0 1 0 545911933 292167680 62814 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71330 62814 603 41 0 71289 0
vsize: 285320
[startup+1040.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64708 0 0 0 103811 208 0 0 25 0 1 0 545911933 292564992 62904 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71427 62904 603 41 0 71386 0
vsize: 285708
[startup+1050.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64785 0 0 0 104811 208 0 0 25 0 1 0 545911933 292970496 62981 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71526 62981 603 41 0 71485 0
vsize: 286104
[startup+1060.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64857 0 0 0 105811 209 0 0 25 0 1 0 545911933 293236736 63053 4294967295 134512640 134672761 3221224624 3221223728 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71591 63053 603 41 0 71550 0
vsize: 286364
[startup+1070.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 64940 0 0 0 106810 209 0 0 25 0 1 0 545911933 293634048 63136 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71688 63136 603 41 0 71647 0
vsize: 286752
[startup+1080.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65013 0 0 0 107810 209 0 0 25 0 1 0 545911933 293912576 63209 4294967295 134512640 134672761 3221224624 3221223728 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71756 63209 603 41 0 71715 0
vsize: 287024
[startup+1090.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65116 0 0 0 108810 209 0 0 25 0 1 0 545911933 294346752 63312 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71862 63312 603 41 0 71821 0
vsize: 287448
[startup+1100.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65182 0 0 0 109811 210 0 0 25 0 1 0 545911933 294617088 63378 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71928 63378 603 41 0 71887 0
vsize: 287712
[startup+1110.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65251 0 0 0 110810 210 0 0 25 0 1 0 545911933 294887424 63447 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71994 63447 603 41 0 71953 0
vsize: 287976
[startup+1120.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65315 0 0 0 111810 210 0 0 25 0 1 0 545911933 295157760 63511 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72060 63511 603 41 0 72019 0
vsize: 288240
[startup+1130.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65378 0 0 0 112811 210 0 0 25 0 1 0 545911933 295428096 63574 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72126 63574 603 41 0 72085 0
vsize: 288504
[startup+1140.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65456 0 0 0 113810 211 0 0 25 0 1 0 545911933 295698432 63652 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72192 63652 603 41 0 72151 0
vsize: 288768
[startup+1150.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65537 0 0 0 114810 211 0 0 25 0 1 0 545911933 295960576 63733 4294967295 134512640 134672761 3221224624 3221223748 134566136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72256 63733 603 41 0 72215 0
vsize: 289024
[startup+1160.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65615 0 0 0 115810 211 0 0 25 0 1 0 545911933 296378368 63811 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72358 63811 603 41 0 72317 0
vsize: 289432
[startup+1170.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65703 0 0 0 116810 211 0 0 25 0 1 0 545911933 296656896 63899 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72426 63899 603 41 0 72385 0
vsize: 289704
[startup+1180.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65797 0 0 0 117811 211 0 0 25 0 1 0 545911933 297062400 63993 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72525 63993 603 41 0 72484 0
vsize: 290100
[startup+1190.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65873 0 0 0 118810 211 0 0 25 0 1 0 545911933 297328640 64069 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72590 64069 603 41 0 72549 0
vsize: 290360
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 27613
Raw data (stat): 27556 (minisat+) R 27555 23176 23175 0 -1 0 65956 0 0 0 119810 212 0 0 25 0 1 0 545911933 297730048 64152 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72688 64152 603 41 0 72647 0
vsize: 290752
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.27 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 27613
Raw data (stat): 27556 (minisat+) Z 27555 23176 23175 0 -1 12 65958 0 0 0 119810 224 0 0 25 0 1 0 545911933 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.26
CPU time (s): 1200.36
CPU user time (s): 1198.11
CPU system time (s): 2.24766
CPU usage (%): 100.008
Max. virtual memory (Kb): 290752
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####