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/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-4.opb
MD5SUM	417d3abd60fd3b9eb4200ff5119a92c4
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	813
Optimality of the best value was proved	NO
Number of terms in the objective function	1798
Biggest coefficient in the objective function	349
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	104116
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	349
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	104116
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05084
Number of variables	2289
Total number of constraints	3052
Number of constraints which are clauses	360
Number of constraints which are cardinality constraints (but not clauses)	2692
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	195
Trace number 31717

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-05-27 05:54:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23109 boxname=wulflinc27 idbench=355 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  417d3abd60fd3b9eb4200ff5119a92c4  /oldhome/oroussel/tmp/wulflinc27/normalized-ss97-4.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-ss97-4.opb
IDLAUNCH: 23109
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        879896 kB
Buffers:         33060 kB
Cached:         100896 kB
SwapCached:        684 kB
Active:          48268 kB
Inactive:        87788 kB
HighTotal:      131008 kB
HighFree:        27468 kB
LowTotal:       903652 kB
LowFree:        852428 kB
SwapTotal:     2097892 kB
SwapFree:      2096360 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5092 kB
Slab:            12992 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 06:12:34 (client local time) WITH STATUS 30 IN 1110.69 SECONDS
stats: 23109 0 1110.69 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1139 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................
c ---[1138]---> BDD-cost: 6649
c ---[1137]---> BDD-cost: 6649
c ---[1136]---> BDD-cost: 6649
c ---[1135]---> BDD-cost: 6599
c ---[1134]---> BDD-cost: 4535
c ---[1133]---> BDD-cost: 4535
c ---[1132]---> BDD-cost: 4562
c ---[1131]---> BDD-cost: 4535
c ---[1130]---> BDD-cost: 4535
c ---[1129]---> BDD-cost: 4535
c ---[1128]---> BDD-cost: 4562
c ---[1127]---> BDD-cost: 4535
c ---[1126]---> BDD-cost:  504
c ---[1125]---> BDD-cost:  504
c ---[1124]---> BDD-cost:  504
c ---[1123]---> BDD-cost:  504
c ---[1122]---> BDD-cost:  152
c ---[1121]---> BDD-cost:  152
c ---[1120]---> BDD-cost:  152
c ---[1119]---> BDD-cost:  152
c ---[1118]---> BDD-cost:  152
c ---[1117]---> BDD-cost:  152
c ---[1116]---> BDD-cost:  152
c ---[1115]---> BDD-cost:  152
c ---[1113]---> BDD-cost:    5
c ---[1111]---> BDD-cost:   13
c ---[1109]---> BDD-cost:    5
c ---[1107]---> BDD-cost:   13
c ---[1105]---> BDD-cost:    5
c ---[1103]---> BDD-cost:   13
c ---[1101]---> BDD-cost:    5
c ---[1099]---> BDD-cost:   13
c ---[1097]---> BDD-cost:    5
c ---[1095]---> BDD-cost:   13
c ---[1093]---> BDD-cost:    5
c ---[1091]---> BDD-cost:   13
c ---[1089]---> BDD-cost:    5
c ---[1087]---> BDD-cost:   13
c ---[1085]---> BDD-cost:    5
c ---[1083]---> BDD-cost:   13
c ---[1081]---> BDD-cost:    5
c ---[1079]---> BDD-cost:   13
c ---[1077]---> BDD-cost:    5
c ---[1075]---> BDD-cost:   13
c ---[1073]---> BDD-cost:    5
c ---[1071]---> BDD-cost:   13
c ---[1069]---> BDD-cost:    5
c ---[1067]---> BDD-cost:   13
c ---[1065]---> BDD-cost:    5
c ---[1063]---> BDD-cost:   13
c ---[1061]---> BDD-cost:    5
c ---[1059]---> BDD-cost:   13
c ---[1057]---> BDD-cost:    5
c ---[1055]---> BDD-cost:   13
c ---[1053]---> BDD-cost:    5
c ---[1051]---> BDD-cost:   13
c ---[1049]---> BDD-cost:    5
c ---[1047]---> BDD-cost:   13
c ---[1045]---> BDD-cost:    5
c ---[1043]---> BDD-cost:   13
c ---[1041]---> BDD-cost:    5
c ---[1039]---> BDD-cost:   13
c ---[1037]---> BDD-cost:    5
c ---[1035]---> BDD-cost:   13
c ---[1033]---> BDD-cost:    5
c ---[1031]---> BDD-cost:   13
c ---[1029]---> BDD-cost:    5
c ---[1027]---> BDD-cost:   13
c ---[1025]---> BDD-cost:    5
c ---[1023]---> BDD-cost:   13
c ---[1021]---> BDD-cost:    5
c ---[1019]---> BDD-cost:   13
c ---[1017]---> BDD-cost:    5
c ---[1015]---> BDD-cost:   13
c ---[1013]---> BDD-cost:    5
c ---[1011]---> BDD-cost:   13
c ---[1009]---> BDD-cost:   13
c ---[1007]---> BDD-cost:    5
c ---[1005]---> BDD-cost:   13
c ---[1003]---> BDD-cost:    5
c ---[1001]---> BDD-cost:   13
c ---[ 999]---> BDD-cost:    5
c ---[ 997]---> BDD-cost:   13
c ---[ 995]---> BDD-cost:    5
c ---[ 993]---> BDD-cost:   13
c ---[ 991]---> BDD-cost:   13
c ---[ 989]---> BDD-cost:    5
c ---[ 987]---> BDD-cost:   13
c ---[ 985]---> BDD-cost:    5
c ---[ 983]---> BDD-cost:   13
c ---[ 981]---> BDD-cost:    5
c ---[ 979]---> BDD-cost:   13
c ---[ 977]---> BDD-cost:    5
c ---[ 975]---> BDD-cost:   13
c ---[ 973]---> BDD-cost:    5
c ---[ 971]---> BDD-cost:   13
c ---[ 969]---> BDD-cost:    5
c ---[ 967]---> BDD-cost:   13
c ---[ 965]---> BDD-cost:    5
c ---[ 963]---> BDD-cost:   13
c ---[ 961]---> BDD-cost:    5
c ---[ 959]---> BDD-cost:   13
c ---[ 957]---> BDD-cost:    5
c ---[ 955]---> BDD-cost:   13
c ---[ 953]---> BDD-cost:    5
c ---[ 951]---> BDD-cost:   13
c ---[ 949]---> BDD-cost:    5
c ---[ 947]---> BDD-cost:   13
c ---[ 945]---> BDD-cost:    5
c ---[ 943]---> BDD-cost:   13
c ---[ 941]---> BDD-cost:    5
c ---[ 939]---> BDD-cost:   13
c ---[ 937]---> BDD-cost:    5
c ---[ 935]---> BDD-cost:   13
c ---[ 933]---> BDD-cost:    5
c ---[ 931]---> BDD-cost:   13
c ---[ 929]---> BDD-cost:    5
c ---[ 927]---> BDD-cost:   13
c ---[ 925]---> BDD-cost:    5
c ---[ 923]---> BDD-cost:   13
c ---[ 921]---> BDD-cost:    5
c ---[ 919]---> BDD-cost:   13
c ---[ 917]---> BDD-cost:    5
c ---[ 915]---> BDD-cost:   13
c ---[ 913]---> BDD-cost:    5
c ---[ 911]---> BDD-cost:   13
c ---[ 909]---> BDD-cost:    5
c ---[ 907]---> BDD-cost:   13
c ---[ 905]---> BDD-cost:   13
c ---[ 903]---> BDD-cost:    5
c ---[ 901]---> BDD-cost:   13
c ---[ 899]---> BDD-cost:    5
c ---[ 897]---> BDD-cost:   13
c ---[ 895]---> BDD-cost:    5
c ---[ 893]---> BDD-cost:   13
c ---[ 891]---> BDD-cost:    5
c ---[ 889]---> BDD-cost:   13
c ---[ 887]---> BDD-cost:    5
c ---[ 885]---> BDD-cost:   13
c ---[ 883]---> BDD-cost:    5
c ---[ 881]---> BDD-cost:   13
c ---[ 879]---> BDD-cost:    5
c ---[ 877]---> BDD-cost:   13
c ---[ 875]---> BDD-cost:    5
c ---[ 873]---> BDD-cost:   13
c ---[ 871]---> BDD-cost:    5
c ---[ 869]---> BDD-cost:   13
c ---[ 867]---> BDD-cost:    5
c ---[ 865]---> BDD-cost:   13
c ---[ 863]---> BDD-cost:    5
c ---[ 861]---> BDD-cost:   13
c ---[ 859]---> BDD-cost:    5
c ---[ 857]---> BDD-cost:   13
c ---[ 855]---> BDD-cost:    5
c ---[ 853]---> BDD-cost:   13
c ---[ 851]---> BDD-cost:    5
c ---[ 849]---> BDD-cost:   13
c ---[ 847]---> BDD-cost:    5
c ---[ 845]---> BDD-cost:   13
c ---[ 843]---> BDD-cost:    5
c ---[ 841]---> BDD-cost:   13
c ---[ 839]---> BDD-cost:    5
c ---[ 837]---> BDD-cost:   13
c ---[ 835]---> BDD-cost:    5
c ---[ 833]---> BDD-cost:   13
c ---[ 831]---> BDD-cost:    5
c ---[ 829]---> BDD-cost:   13
c ---[ 827]---> BDD-cost:    5
c ---[ 825]---> BDD-cost:   13
c ---[ 823]---> BDD-cost:   13
c ---[ 821]---> BDD-cost:    5
c ---[ 819]---> BDD-cost:   13
c ---[ 817]---> BDD-cost:    5
c ---[ 815]---> BDD-cost:   13
c ---[ 813]---> BDD-cost:    5
c ---[ 811]---> BDD-cost:   13
c ---[ 809]---> BDD-cost:    5
c ---[ 807]---> BDD-cost:   13
c ---[ 805]---> BDD-cost:    5
c ---[ 803]---> BDD-cost:   13
c ---[ 801]---> BDD-cost:    5
c ---[ 799]---> BDD-cost:   13
c ---[ 797]---> BDD-cost:    5
c ---[ 795]---> BDD-cost:   13
c ---[ 793]---> BDD-cost:   13
c ---[ 791]---> BDD-cost:    5
c ---[ 789]---> BDD-cost:   13
c ---[ 787]---> BDD-cost:    5
c ---[ 785]---> BDD-cost:   13
c ---[ 783]---> BDD-cost:   13
c ---[ 781]---> BDD-cost:    5
c ---[ 779]---> BDD-cost:   13
c ---[ 777]---> BDD-cost:    5
c ---[ 775]---> BDD-cost:   13
c ---[ 773]---> BDD-cost:    5
c ---[ 771]---> BDD-cost:   13
c ---[ 769]---> BDD-cost:    5
c ---[ 767]---> BDD-cost:   13
c ---[ 765]---> BDD-cost:    5
c ---[ 763]---> BDD-cost:   13
c ---[ 761]---> BDD-cost:   13
c ---[ 759]---> BDD-cost:    5
c ---[ 757]---> BDD-cost:   13
c ---[ 755]---> BDD-cost:    5
c ---[ 753]---> BDD-cost:   13
c ---[ 751]---> BDD-cost:    5
c ---[ 749]---> BDD-cost:   13
c ---[ 747]---> BDD-cost:    5
c ---[ 745]---> BDD-cost:   13
c ---[ 743]---> BDD-cost:    5
c ---[ 741]---> BDD-cost:   13
c ---[ 739]---> BDD-cost:    5
c ---[ 737]---> BDD-cost:   13
c ---[ 735]---> BDD-cost:    5
c ---[ 733]---> BDD-cost:   13
c ---[ 731]---> BDD-cost:    5
c ---[ 729]---> BDD-cost:   13
c ---[ 727]---> BDD-cost:    5
c ---[ 725]---> BDD-cost:   13
c ---[ 723]---> BDD-cost:    5
c ---[ 721]---> BDD-cost:   13
c ---[ 719]---> BDD-cost:    5
c ---[ 717]---> BDD-cost:   13
c ---[ 715]---> BDD-cost:   13
c ---[ 713]---> BDD-cost:    5
c ---[ 711]---> BDD-cost:   13
c ---[ 709]---> BDD-cost:   13
c ---[ 707]---> BDD-cost:    5
c ---[ 705]---> BDD-cost:   13
c ---[ 703]---> BDD-cost:    5
c ---[ 701]---> BDD-cost:   13
c ---[ 699]---> BDD-cost:    5
c ---[ 697]---> BDD-cost:   13
c ---[ 695]---> BDD-cost:    5
c ---[ 693]---> BDD-cost:   13
c ---[ 691]---> BDD-cost:    5
c ---[ 689]---> BDD-cost:   13
c ---[ 687]---> BDD-cost:    5
c ---[ 685]---> BDD-cost:   13
c ---[ 683]---> BDD-cost:    5
c ---[ 681]---> BDD-cost:   13
c ---[ 679]---> BDD-cost:    5
c ---[ 677]---> BDD-cost:   13
c ---[ 675]---> BDD-cost:    5
c ---[ 673]---> BDD-cost:   13
c ---[ 671]---> BDD-cost:    5
c ---[ 669]---> BDD-cost:   13
c ---[ 667]---> BDD-cost:    5
c ---[ 665]---> BDD-cost:   13
c ---[ 663]---> BDD-cost:    5
c ---[ 661]---> BDD-cost:   13
c ---[ 659]---> BDD-cost:    5
c ---[ 657]---> BDD-cost:   13
c ---[ 655]---> BDD-cost:    5
c ---[ 653]---> BDD-cost:   13
c ---[ 651]---> BDD-cost:    5
c ---[ 649]---> BDD-cost:   13
c ---[ 647]---> BDD-cost:    5
c ---[ 645]---> BDD-cost:   13
c ---[ 643]---> BDD-cost:    5
c ---[ 641]---> BDD-cost:   13
c ---[ 639]---> BDD-cost:    5
c ---[ 637]---> BDD-cost:   13
c ---[ 635]---> BDD-cost:    5
c ---[ 633]---> BDD-cost:   13
c ---[ 631]---> BDD-cost:    5
c ---[ 629]---> BDD-cost:   13
c ---[ 627]---> BDD-cost:    5
c ---[ 625]---> BDD-cost:   13
c ---[ 623]---> BDD-cost:    5
c ---[ 621]---> BDD-cost:   13
c ---[ 619]---> BDD-cost:    5
c ---[ 617]---> BDD-cost:   13
c ---[ 615]---> BDD-cost:    5
c ---[ 613]---> BDD-cost:   13
c ---[ 611]---> BDD-cost:    5
c ---[ 609]---> BDD-cost:   13
c ---[ 607]---> BDD-cost:    5
c ---[ 605]---> BDD-cost:   13
c ---[ 603]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    1
c ---[ 599]---> BDD-cost:    5
c ---[ 597]---> BDD-cost:   13
c ---[ 595]---> BDD-cost:    5
c ---[ 593]---> BDD-cost:   13
c ---[ 591]---> BDD-cost:    5
c ---[ 589]---> BDD-cost:   13
c ---[ 587]---> BDD-cost:    5
c ---[ 585]---> BDD-cost:    5
c ---[ 583]---> BDD-cost:   13
c ---[ 581]---> BDD-cost:    5
c ---[ 579]---> BDD-cost:   13
c ---[ 577]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:   13
c ---[ 573]---> BDD-cost:    5
c ---[ 571]---> BDD-cost:   13
c ---[ 569]---> BDD-cost:    5
c ---[ 567]---> BDD-cost:   13
c ---[ 565]---> BDD-cost:    5
c ---[ 563]---> BDD-cost:   13
c ---[ 561]---> BDD-cost:    5
c ---[ 559]---> BDD-cost:   13
c ---[ 557]---> BDD-cost:    5
c ---[ 555]---> BDD-cost:   13
c ---[ 553]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:   13
c ---[ 549]---> BDD-cost:    5
c ---[ 547]---> BDD-cost:   13
c ---[ 545]---> BDD-cost:    5
c ---[ 543]---> BDD-cost:   13
c ---[ 541]---> BDD-cost:    5
c ---[ 539]---> BDD-cost:   13
c ---[ 537]---> BDD-cost:   13
c ---[ 535]---> BDD-cost:    5
c ---[ 533]---> BDD-cost:   13
c ---[ 531]---> BDD-cost:    5
c ---[ 529]---> BDD-cost:   13
c ---[ 527]---> BDD-cost:    5
c ---[ 525]---> BDD-cost:   13
c ---[ 523]---> BDD-cost:    5
c ---[ 521]---> BDD-cost:   13
c ---[ 519]---> BDD-cost:    5
c ---[ 517]---> BDD-cost:   13
c ---[ 515]---> BDD-cost:   13
c ---[ 513]---> BDD-cost:   13
c ---[ 511]---> BDD-cost:   13
c ---[ 509]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:   13
c ---[ 505]---> BDD-cost:    5
c ---[ 503]---> BDD-cost:   13
c ---[ 501]---> BDD-cost:    5
c ---[ 499]---> BDD-cost:   13
c ---[ 497]---> BDD-cost:    5
c ---[ 495]---> BDD-cost:   13
c ---[ 493]---> BDD-cost:    5
c ---[ 491]---> BDD-cost:   13
c ---[ 489]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:   13
c ---[ 485]---> BDD-cost:    5
c ---[ 483]---> BDD-cost:   13
c ---[ 481]---> BDD-cost:    5
c ---[ 479]---> BDD-cost:   13
c ---[ 477]---> BDD-cost:    5
c ---[ 475]---> BDD-cost:   13
c ---[ 473]---> BDD-cost:    5
c ---[ 471]---> BDD-cost:   13
c ---[ 469]---> BDD-cost:    5
c ---[ 467]---> BDD-cost:   13
c ---[ 465]---> BDD-cost:    5
c ---[ 463]---> BDD-cost:   13
c ---[ 461]---> BDD-cost:    5
c ---[ 459]---> BDD-cost:   13
c ---[ 457]---> BDD-cost:    5
c ---[ 455]---> BDD-cost:   13
c ---[ 453]---> BDD-cost:    5
c ---[ 451]---> BDD-cost:   13
c ---[ 449]---> BDD-cost:    5
c ---[ 447]---> BDD-cost:   13
c ---[ 445]---> BDD-cost:    5
c ---[ 443]---> BDD-cost:   13
c ---[ 441]---> BDD-cost:    5
c ---[ 439]---> BDD-cost:   13
c ---[ 437]---> BDD-cost:    5
c ---[ 435]---> BDD-cost:   13
c ---[ 433]---> BDD-cost:    5
c ---[ 431]---> BDD-cost:   13
c ---[ 429]---> BDD-cost:    5
c ---[ 427]---> BDD-cost:   13
c ---[ 425]---> BDD-cost:    5
c ---[ 423]---> BDD-cost:   13
c ---[ 421]---> BDD-cost:    5
c ---[ 419]---> BDD-cost:   13
c ---[ 417]---> BDD-cost:    5
c ---[ 415]---> BDD-cost:   13
c ---[ 413]---> BDD-cost:   13
c ---[ 411]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:   13
c ---[ 407]---> BDD-cost:    5
c ---[ 405]---> BDD-cost:   13
c ---[ 403]---> BDD-cost:    5
c ---[ 401]---> BDD-cost:   13
c ---[ 399]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:   13
c ---[ 395]---> BDD-cost:    5
c ---[ 393]---> BDD-cost:   13
c ---[ 391]---> BDD-cost:    5
c ---[ 389]---> BDD-cost:   13
c ---[ 387]---> BDD-cost:    5
c ---[ 385]---> BDD-cost:   13
c ---[ 383]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:   13
c ---[ 379]---> BDD-cost:    5
c ---[ 377]---> BDD-cost:   13
c ---[ 375]---> BDD-cost:    5
c ---[ 373]---> BDD-cost:   13
c ---[ 371]---> BDD-cost:    5
c ---[ 369]---> BDD-cost:   13
c ---[ 367]---> BDD-cost:    5
c ---[ 365]---> BDD-cost:   13
c ---[ 363]---> BDD-cost:    5
c ---[ 361]---> BDD-cost:   13
c ---[   0]---> BDD-cost:    6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  334206   994904 |  111402       0        0     nan |  0.000 % |
c |       100 |  334206   994904 |  122542     100     2359    23.6 |  0.571 % |
c |       250 |  334206   994904 |  134796     250     5261    21.0 |  0.571 % |
c |       475 |  334206   994904 |  148276     475    19757    41.6 |  0.571 % |
c |       814 |  334206   994904 |  163103     814    35213    43.3 |  0.571 % |
c |      1320 |  334206   994904 |  179414    1320    85596    64.8 |  0.571 % |
c |      2079 |  334206   994904 |  197355    2079   176127    84.7 |  0.571 % |
c ==============================================================================
c [1mFound solution: 7070[0m
c ---[   0]---> Sorter-cost:98305     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2134 |  512094  1410577 |  170698    2134   177272    83.1 |  0.571 % |
c |      2237 |  512094  1410577 |  187767    2237   190056    85.0 |  0.271 % |
c |      2387 |  512039  1410454 |  206544    2386   191536    80.3 |  0.281 % |
c |      2612 |  507941  1401052 |  227199    2537   192252    75.8 |  1.110 % |
c |      2949 |  502882  1389402 |  249918    2750   193462    70.3 |  2.142 % |
c |      3457 |  491874  1363953 |  274910    3052   194771    63.8 |  4.434 % |
c |      4216 |  484279  1346350 |  302401    3508   196393    56.0 |  6.044 % |
c |      5356 |  468284  1309254 |  332642    4150   198919    47.9 |  9.447 % |
c |      7065 |  458398  1286299 |  365906    5385   207704    38.6 | 11.574 % |
c |      9627 |  453236  1274263 |  402496    7641   228239    29.9 | 12.723 % |
c |     13471 |  450711  1268372 |  442746   11308   288661    25.5 | 13.281 % |
c |     19238 |  449192  1264819 |  487021   16841   343223    20.4 | 13.631 % |
c |     27887 |  449010  1264391 |  535723   25476   689772    27.1 | 13.673 % |
c |     40864 |  448636  1263512 |  589295   38372  1164593    30.4 | 13.760 % |
c |     60325 |  448503  1263201 |  648225   57750  2502379    43.3 | 13.790 % |
c |     89517 |  448079  1262217 |  713047   86809  3219802    37.1 | 13.880 % |
c |    133306 |  447967  1261955 |  784352  130565  5252961    40.2 | 13.905 % |
c ==============================================================================
c [1mFound solution: 5205[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    170863 |  448221  1262566 |  149407  168117  9668843    57.5 | 13.905 % |
c |    170964 |  448221  1262566 |  164347  168218  9671094    57.5 | 13.929 % |
c |    171114 |  448221  1262566 |  180782  168368  9674583    57.5 | 13.929 % |
c |    171340 |  448221  1262566 |  198860  168594  9681690    57.4 | 13.929 % |
c |    171680 |  448221  1262566 |  218746  168934  9687435    57.3 | 13.929 % |
c ==============================================================================
c [1mFound solution: 4303[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    172163 |  448948  1264366 |  149649  169417  9695841    57.2 | 13.929 % |
c |    172264 |  448948  1264366 |  164613  169518  9705242    57.3 | 14.155 % |
c |    172414 |  448948  1264366 |  181075  169668  9714049    57.3 | 14.155 % |
c ==============================================================================
c [1mFound solution: 3582[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    172580 |  449504  1265746 |  149834  169834  9736406    57.3 | 14.155 % |
c |    172680 |  449504  1265746 |  164817  169934  9740303    57.3 | 14.314 % |
c |    172832 |  449504  1265746 |  181299  170086  9742827    57.3 | 14.314 % |
c |    173057 |  449504  1265746 |  199429  170311  9749920    57.2 | 14.314 % |
c |    173394 |  449504  1265746 |  219371  170648  9764229    57.2 | 14.314 % |
c ==============================================================================
c [1mFound solution: 3176[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    173814 |  449859  1266617 |  149953  171068  9789562    57.2 | 14.314 % |
c |    173915 |  449859  1266617 |  164948  171169  9794313    57.2 | 14.415 % |
c |    174065 |  449803  1266490 |  181443  171299  9796937    57.2 | 14.427 % |
c |    174291 |  449803  1266490 |  199587  171525  9800818    57.1 | 14.427 % |
c |    174629 |  449803  1266490 |  219546  171863  9815808    57.1 | 14.427 % |
c ==============================================================================
c [1mFound solution: 3066[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175065 |  449817  1266551 |  149939  172299  9831586    57.1 | 14.427 % |
c |    175165 |  449817  1266551 |  164932   29414  1742132    59.2 | 14.427 % |
c |    175316 |  449817  1266551 |  181426   29565  1752034    59.3 | 14.427 % |
c |    175541 |  449817  1266551 |  199568   29790  1762109    59.2 | 14.427 % |
c |    175879 |  449817  1266551 |  219525   30128  1795374    59.6 | 14.427 % |
c |    176385 |  449817  1266551 |  241478   30634  1833913    59.9 | 14.427 % |
c |    177144 |  449813  1266542 |  265626   31392  1843752    58.7 | 14.428 % |
c |    178283 |  449761  1266422 |  292188   32528  1889865    58.1 | 14.441 % |
c |    179991 |  449761  1266422 |  321407   34236  2050732    59.9 | 14.441 % |
c |    182553 |  449761  1266422 |  353548   36798  2320655    63.1 | 14.441 % |
c ==============================================================================
c [1mFound solution: 2551[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    184313 |  449820  1266568 |  149940   38558  2363365    61.3 | 14.441 % |
c |    184413 |  449820  1266568 |  164934   38658  2366058    61.2 | 14.441 % |
c |    184564 |  449814  1266554 |  181427   38807  2371306    61.1 | 14.442 % |
c |    184790 |  449814  1266554 |  199570   39033  2376678    60.9 | 14.442 % |
c |    185127 |  449814  1266554 |  219527   39370  2383922    60.6 | 14.442 % |
c |    185634 |  449786  1266489 |  241479   39876  2391890    60.0 | 14.449 % |
c |    186393 |  449786  1266489 |  265627   40635  2445035    60.2 | 14.449 % |
c |    187533 |  449786  1266489 |  292190   41775  2480496    59.4 | 14.449 % |
c ==============================================================================
c [1mFound solution: 2450[0m
c ---[   0]---> Sorter-cost:    1     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    187896 |  449803  1266535 |  149934   42138  2494378    59.2 | 14.449 % |
c |    187996 |  449803  1266535 |  164927   42238  2496448    59.1 | 14.450 % |
c |    188146 |  449803  1266535 |  181420   42388  2499218    59.0 | 14.450 % |
c |    188372 |  449803  1266535 |  199562   42614  2502076    58.7 | 14.450 % |
c ==============================================================================
c [1mFound solution: 2249[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    188493 |  450126  1267331 |  150042   42735  2506887    58.7 | 14.450 % |
c |    188593 |  450126  1267331 |  165046   42835  2514409    58.7 | 14.555 % |
c |    188743 |  450126  1267331 |  181550   42985  2516737    58.5 | 14.555 % |
c |    188968 |  450126  1267331 |  199705   43210  2521315    58.4 | 14.555 % |
c |    189307 |  450126  1267331 |  219676   43549  2527731    58.0 | 14.555 % |
c |    189814 |  450058  1267174 |  241644   44049  2566490    58.3 | 14.568 % |
c |    190573 |  450058  1267174 |  265808   44808  2641217    58.9 | 14.568 % |
c |    191712 |  450058  1267174 |  292389   45947  2681156    58.4 | 14.568 % |
c ==============================================================================
c [1mFound solution: 1548[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    191841 |  450054  1267168 |  150018   46060  2682972    58.2 | 14.568 % |
c |    191941 |  450054  1267168 |  165019   46160  2685870    58.2 | 14.580 % |
c |    192094 |  450054  1267168 |  181521   46313  2687011    58.0 | 14.580 % |
c |    192320 |  450054  1267168 |  199673   46539  2689214    57.8 | 14.580 % |
c |    192661 |  450054  1267168 |  219641   46880  2714301    57.9 | 14.580 % |
c |    193167 |  450054  1267168 |  241605   47386  2727988    57.6 | 14.580 % |
c ==============================================================================
c [1mFound solution: 1334[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    193809 |  449981  1267069 |  149993   47991  2742997    57.2 | 14.580 % |
c ==============================================================================
c [1mFound solution: 1263[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    193836 |  449989  1267087 |  149996   48018  2743500    57.1 | 14.580 % |
c |    193937 |  449989  1267087 |  164995   48119  2746997    57.1 | 14.599 % |
c |    194088 |  449989  1267087 |  181495   48270  2755956    57.1 | 14.599 % |
c |    194315 |  449989  1267087 |  199644   48497  2761316    56.9 | 14.599 % |
c |    194652 |  449914  1266915 |  219609   48822  2769548    56.7 | 14.612 % |
c ==============================================================================
c [1mFound solution: 1251[0m
c ---[   0]---> Sorter-cost:    2     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    195056 |  449914  1266914 |  149971   49225  2799588    56.9 | 14.612 % |
c |    195156 |  449914  1266914 |  164968   49325  2803362    56.8 | 14.614 % |
c |    195306 |  449914  1266914 |  181464   49475  2807736    56.8 | 14.614 % |
c |    195532 |  449653  1266315 |  199611   49595  2809582    56.7 | 14.662 % |
c |    195869 |  449653  1266315 |  219572   49932  2815730    56.4 | 14.662 % |
c ==============================================================================
c [1mFound solution: 1250[0m
c ---[   0]---> Sorter-cost:    1     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    196290 |  449509  1265985 |  149836   50304  2828740    56.2 | 14.662 % |
c |    196390 |  449509  1265985 |  164819   50404  2835402    56.3 | 14.692 % |
c |    196540 |  449497  1265958 |  181301   50542  2838712    56.2 | 14.693 % |
c |    196765 |  449005  1264828 |  199431   50569  2839384    56.1 | 14.787 % |
c |    197102 |  448761  1264267 |  219374   50369  2841437    56.4 | 14.834 % |
c ==============================================================================
c [1mFound solution: 1159[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    197213 |  448768  1264285 |  149589   50480  2842422    56.3 | 14.834 % |
c |    197313 |  448768  1264285 |  164547   50580  2845108    56.2 | 14.834 % |
c |    197463 |  447984  1262476 |  181002   50450  2847500    56.4 | 14.990 % |
c |    197692 |  447984  1262476 |  199102   50679  2851385    56.3 | 14.990 % |
c |    198029 |  447542  1261462 |  219013   50756  2861556    56.4 | 15.068 % |
c |    198535 |  447204  1260681 |  240914   51202  2868770    56.0 | 15.134 % |
c ==============================================================================
c [1mFound solution: 1158[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    198781 |  447212  1260699 |  149070   51448  2890190    56.2 | 15.134 % |
c |    198884 |  447212  1260699 |  163977   51551  2891973    56.1 | 15.134 % |
c |    199036 |  447212  1260699 |  180374   51703  2899594    56.1 | 15.134 % |
c ==============================================================================
c [1mFound solution: 1139[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199234 |  447221  1260722 |  149073   51901  2905670    56.0 | 15.134 % |
c ==============================================================================
c [1mFound solution: 1047[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199316 |  447232  1260749 |  149077   51983  2908362    55.9 | 15.134 % |
c |    199421 |  447204  1260685 |  163984   51743  2850660    55.1 | 15.142 % |
c ==============================================================================
c [1mFound solution: 933[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199427 |  447212  1260705 |  149070   51749  2850892    55.1 | 15.142 % |
c |    199527 |  447212  1260705 |  163977   51849  2853046    55.0 | 15.142 % |
c ==============================================================================
c [1mFound solution: 932[0m
c ---[   0]---> Sorter-cost:    3     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199530 |  447216  1260715 |  149072   51852  2853072    55.0 | 15.142 % |
c ==============================================================================
c [1mFound solution: 931[0m
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199533 |  447222  1260731 |  149074   51855  2853111    55.0 | 15.142 % |
c ==============================================================================
c [1mFound solution: 930[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199537 |  447226  1260742 |  149075   51859  2853249    55.0 | 15.142 % |
c |    199637 |  447226  1260742 |  163982   51959  2861153    55.1 | 15.143 % |
c ==============================================================================
c [1mFound solution: 928[0m
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199641 |  447232  1260757 |  149077   51963  2861224    55.1 | 15.143 % |
c ==============================================================================
c [1mFound solution: 827[0m
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199644 |  276844   799838 |   92281   24432   802185    32.8 | 15.143 % |
c ==============================================================================
c [1mFound solution: 826[0m
c ---[   0]---> Sorter-cost:36202     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    199649 |  357638   987505 |  119212   24437   802214    32.8 | 15.143 % |
c |    199750 |  357638   987505 |  131133   24538   806212    32.9 | 40.999 % |
c |    199901 |  357638   987505 |  144246   24689   810219    32.8 | 40.999 % |
c |    200126 |  357605   987432 |  158671   24912   821053    33.0 | 41.005 % |
c |    200463 |  356395   984693 |  174538   24817   822831    33.2 | 41.212 % |
c |    200969 |  354058   979479 |  191992   25293   832945    32.9 | 41.629 % |
c |    201728 |  334718   935386 |  211191   25672   836476    32.6 | 44.917 % |
c |    202867 |  321409   904698 |  232310   26402   845156    32.0 | 47.231 % |
c |    204575 |  320282   902075 |  255541   28073   900556    32.1 | 47.437 % |
c |    207139 |  313244   885758 |  281095   29659   924765    31.2 | 48.713 % |
c |    210983 |  305661   868152 |  309205   33145  1007531    30.4 | 50.108 % |
c |    216749 |  303707   863611 |  340125   38671  1164625    30.1 | 50.468 % |
c |    225398 |  300300   855650 |  374138   46526  1303619    28.0 | 51.143 % |
c |    238374 |  300109   855202 |  411552   59404  2470806    41.6 | 51.180 % |
c ==============================================================================
c [1mFound solution: 820[0m
c ---[   0]---> Sorter-cost:    5     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    239863 |  300346   855819 |  100115   60893  2569852    42.2 | 51.180 % |
c |    239964 |  300346   855819 |  110126   60994  2576232    42.2 | 51.196 % |
c |    240114 |  300346   855819 |  121139   61144  2584812    42.3 | 51.196 % |
c |    240339 |  300346   855819 |  133253   61369  2591814    42.2 | 51.196 % |
c |    240676 |  300307   855727 |  146578   61697  2596123    42.1 | 51.206 % |
c ==============================================================================
c [1mFound solution: 819[0m
c ---[   0]---> Sorter-cost:    5     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    240799 |  300470   856170 |  100156   61820  2598295    42.0 | 51.206 % |
c |    240899 |  300470   856170 |  110171   61920  2602494    42.0 | 51.218 % |
c |    241049 |  300470   856170 |  121188   62070  2613001    42.1 | 51.218 % |
c |    241274 |  300470   856170 |  133307   62295  2616468    42.0 | 51.218 % |
c |    241611 |  300470   856170 |  146638   62632  2629013    42.0 | 51.218 % |
c |    242117 |  300470   856170 |  161302   63138  2644896    41.9 | 51.218 % |
c |    242876 |  300470   856170 |  177432   63897  2671687    41.8 | 51.218 % |
c ==============================================================================
c [1mFound solution: 818[0m
c ---[   0]---> Sorter-cost:    5     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    243322 |  300604   856529 |  100201   64343  2687190    41.8 | 51.218 % |
c |    243422 |  300604   856529 |  110221   64443  2690397    41.7 | 51.229 % |
c |    243576 |  300604   856529 |  121243   64597  2694290    41.7 | 51.229 % |
c ==============================================================================
c [1mFound solution: 817[0m
c ---[   0]---> Sorter-cost:    5     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    243616 |  300746   856886 |  100248   64637  2695107    41.7 | 51.229 % |
c |    243716 |  300746   856886 |  110272   64737  2697627    41.7 | 51.242 % |
c |    243868 |  300621   856590 |  121300   64842  2698540    41.6 | 51.267 % |
c |    244093 |  300621   856590 |  133430   65067  2702854    41.5 | 51.267 % |
c |    244430 |  300621   856590 |  146773   65404  2713567    41.5 | 51.267 % |
c |    244936 |  300621   856590 |  161450   65910  2740596    41.6 | 51.267 % |
c |    245695 |  300585   856507 |  177595   66662  2762364    41.4 | 51.273 % |
c |    246835 |  300585   856507 |  195354   67802  2813117    41.5 | 51.273 % |
c ==============================================================================
c [1mFound solution: 816[0m
c ---[   0]---> Sorter-cost:    5     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    247373 |  300675   856729 |  100225   68338  2826669    41.4 | 51.273 % |
c |    247474 |  300675   856729 |  110247   68439  2834127    41.4 | 51.286 % |
c |    247624 |  300675   856729 |  121272   68589  2838665    41.4 | 51.286 % |
c |    247849 |  300675   856729 |  133399   68814  2845296    41.3 | 51.286 % |
c ==============================================================================
c [1mFound solution: 815[0m
c ---[   0]---> Sorter-cost:    5     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    248134 |  300357   856000 |  100119   69075  2866315    41.5 | 51.286 % |
c |    248234 |  300357   856000 |  110130   69175  2869325    41.5 | 51.358 % |
c |    248385 |  300353   855991 |  121143   69324  2876759    41.5 | 51.358 % |
c |    248610 |  300223   855690 |  133258   69525  2880339    41.4 | 51.380 % |
c |    248948 |  300223   855690 |  146584   69863  2886157    41.3 | 51.380 % |
c |    249454 |  300191   855618 |  161242   70368  2899610    41.2 | 51.385 % |
c |    250213 |  300191   855618 |  177366   71127  3024926    42.5 | 51.385 % |
c |    251355 |  300191   855618 |  195103   72269  3095243    42.8 | 51.385 % |
c |    253063 |  300109   855427 |  214613   73960  3158296    42.7 | 51.401 % |
c |    255626 |  300109   855427 |  236075   76523  3239499    42.3 | 51.401 % |
c |    259471 |  300109   855427 |  259682   80368  3687447    45.9 | 51.401 % |
c ==============================================================================
c [1mFound solution: 814[0m
c ---[   0]---> Sorter-cost:    5     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    262685 |  300167   855583 |  100055   83499  3853447    46.1 | 51.401 % |
c |    262785 |  300167   855583 |  110060   83599  3856107    46.1 | 51.422 % |
c |    262936 |  300167   855583 |  121066   83750  3862192    46.1 | 51.422 % |
c |    263161 |  300167   855583 |  133173   83975  3868325    46.1 | 51.422 % |
c |    263498 |  300167   855583 |  146490   84312  3885040    46.1 | 51.422 % |
c |    264004 |  300046   855305 |  161139   84781  3894592    45.9 | 51.443 % |
c ==============================================================================
c [1mFound solution: 813[0m
c ---[   0]---> Sorter-cost:    5     Base: 11 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    264170 |  300148   855551 |  100049   84947  3903504    46.0 | 51.443 % |
c |    264270 |  300148   855551 |  110053   85047  3908875    46.0 | 51.456 % |
c |    264421 |  300148   855551 |  121059   85198  3911719    45.9 | 51.456 % |
c |    264648 |  300148   855551 |  133165   85425  3917203    45.9 | 51.456 % |
c ==============================================================================
c [1mOptimal solution: 813[0m
s OPTIMUM FOUND
v v1 -v365 -v729 v924 -v1119 -v1704 -v1899 -v2 v366 -v1120 v1510 -v2095 v3 -v367 -v1121 v1706 v4 -v186 -v368 -v1122 -v1317 -v1512 v1707 -v1902 v5 -v187 -v369 -v1123 -v1318 -v1513 -v1708 v1903 v6 -v188 -v370 -v734 v929 -v1124 -v1319 -v1514 -v1709 -v1904 v1515 -v2100 v554 v1711 v10 -v192 -v374 -v738 v933 -v1128 -v1323 v193 -v1324 -v1519 v1714 -v2104 v559 v2106 v14 -v378 -v560 -v742 v937 -v1132 -v2107 v15 -v379 -v1133 v2108 v16 -v380 -v1134 v2109 v563 -v1330 v1525 -v2110 v566 -v1723 v1918 -v2113 v567 v1334 -v2114 v204 -v1725 v1920 v23 -v205 -v387 -v751 -v946 -v1141 v1726 -v1921 -v2116 v570 v1532 -v1727 -v2117 v571 v2118 v572 -v1339 v1534 -v2119 v2120 v573 -v756 v951 -v28 v392 -v1147 v1927 -v29 v393 -v1148 v1343 v576 -v1344 v1539 -v2124 v1345 v1346 -v32 v396 -v1152 v33 -v397 -v1153 v2128 v34 -v398 v959 -v1154 -v2129 v35 -v399 -v1155 v2130 v36 -v400 -v1156 v2131 v37 -v401 -v1157 v2132 -v38 v402 v963 -v1158 -v2133 v964 -v2134 v222 v1550 -v2135 v41 -v405 -v771 v966 -v1161 -v2136 v588 v1942 v589 -v773 v968 -v1358 -v1748 v226 v774 -v969 v227 -v1555 v1750 -v2140 v46 -v410 -v1166 v1751 v1557 -v1752 -v48 -v230 v412 -v778 v973 -v1168 -v1363 v595 v1754 v50 -v414 -v780 v975 -v1170 -v1950 -v2145 v233 v976 -v1756 -v2146 v1757 -v2147 -v52 v416 -v1173 v1953 v417 -v599 -v784 v979 -v1369 v54 -v418 -v1175 v2150 -v55 v419 -v1176 -v2151 -v56 v420 -v1177 v1762 v421 -v603 v1763 -v58 v422 -v1179 v2154 v241 -v605 v1765 -v2155 -v60 v242 -v424 v1181 -v1766 v61 -v243 -v425 v792 -v987 -v1182 v608 v1768 -v63 -v427 v609 v1184 v64 -v428 -v1185 v2160 -v65 v429 -v796 v991 -v1186 v248 v1382 -v2162 v613 v1383 -v2163 -v2164 v251 v2165 -v252 v616 v1386 v253 v2167 -v2168 v254 v1584 -v2169 -v73 v437 -v1195 v1585 -v2170 -v75 -v439 v621 v1197 -v2172 v622 -v1393 v1588 -v77 v441 -v1199 v260 v1395 v811 -v1006 -v1786 v443 -v625 v1787 v626 v813 -v1008 -v1788 -v1983 -v2178 v1789 -v2179 v627 v815 -v1010 v628 v1596 -v1791 -v2181 v265 -v629 v1402 -v2182 -v84 v448 -v630 -v818 v1013 -v1208 -v2183 v631 v2184 v820 -v1015 -v2185 v1796 v633 v2187 v2188 v635 -v824 v1019 -v1799 v636 v1800 -v2190 v91 -v455 v826 -v1021 -v1216 v92 -v456 -v827 v1022 -v1217 v828 -v1023 v94 -v458 v829 -v1024 -v1219 v95 -v459 -v1220 v2195 v278 v1416 -v2196 v2197 v461 -v643 v1028 -v2198 v1224 v462 -v644 v835 -v1030 -v1420 -v1615 v645 v1031 -v2201 v100 -v464 -v837 -v1032 -v1227 v1422 -v2202 v101 -v465 -v1228 v2203 -v102 v466 -v839 v1034 -v1229 -v1619 v103 -v467 -v1230 -v1620 -v1815 v2010 v104 -v286 -v468 -v841 v1036 -v1231 -v1426 v105 -v469 -v1232 -v1427 v1622 -v1817 v106 -v470 v843 -v1038 -v1233 v289 v108 -v472 v845 -v1040 -v1235 -v109 v473 v846 -v1041 -v1236 v292 -v111 -v293 v475 -v848 -v1043 -v1238 v2018 -v112 v476 -v1239 v1434 v659 -v114 v478 -v660 -v1241 v1826 v297 -v116 v480 -v1243 v1438 v299 -v663 v300 v1635 -v119 v483 -v1246 -v1831 v2026 v120 -v484 -v1247 v1832 v303 v2223 -v122 v486 -v1249 v2224 v305 -v125 v307 -v489 v1252 -v1837 -v2227 v672 v863 -v1058 -v127 -v491 v673 v1254 -v1839 v674 v129 -v493 v865 -v1255 -v2230 v312 v2231 -v131 v313 v867 -v1452 -v1647 v314 v1453 -v133 v315 -v497 v1259 -v1649 -v1844 -v2039 v680 -v870 v1065 -v135 v499 -v871 -v1066 -v1261 v1456 v136 -v318 -v500 v872 -v1067 -v1262 -v1847 -v2042 -v2237 v683 v2238 v320 v874 -v1069 v139 -v503 -v1265 v1460 -v2240 v140 -v322 v1851 -v2241 v877 -v1072 -v2242 v687 -v878 -v1073 v1658 -v1853 -v142 -v506 v688 -v879 -v1074 v1269 -v1464 -v1659 -v1854 -v2049 -v2244 v143 -v325 -v507 -v689 -v1270 v1465 -v2245 -v508 v690 v1856 -v145 -v509 v691 v1272 -v2247 v1468 -v1858 v1469 -v1859 v1470 v146 -v510 -v1276 v1861 v329 v1862 v694 v1668 -v2253 v695 -v1474 v1669 v150 -v514 v890 -v1085 -v1280 v151 -v515 -v891 -v1086 -v1281 -v1476 -v1671 v2061 -v892 -v1087 v1477 -v1672 v335 -v699 -v893 -v1088 v1478 -v1673 -v2258 v154 -v518 v894 -v1089 -v1284 -v1479 -v1674 -v1869 -v155 v519 -v895 v1090 -v1285 -v1675 v1676 v157 -v339 -v521 v897 -v1092 -v1287 -v1677 -v1872 -v159 v341 -v523 -v705 v899 -v1094 -v1289 -v1679 -v2069 v342 v2265 -v161 v525 -v1291 v2266 v344 -v2267 v163 -v345 -v527 v1098 -v1293 -v1683 -v1878 -v528 v710 -v904 -v1099 -v1294 -v1684 v1879 -v2074 -v2269 v347 v1685 -v2270 v167 -v531 -v1297 v1882 -v168 v350 -v532 v1298 -v2273 -v169 -v351 -v533 v715 v909 -v1104 -v1299 -v1494 -v2274 v1300 -v1495 -v1690 v1106 -v2276 -v171 v353 -v535 v1302 -v1692 -v2082 v172 -v536 -v718 -v1303 v2083 -v2278 v174 -v538 -v915 -v1110 -v1305 v1695 v539 -v916 v1501 v358 -v722 -v1502 -v1697 -v1892 v2087 v359 v1698 -v2283 -v178 v360 -v542 v919 -v1114 -v1309 -v2284 -v179 v543 -v1310 v1700 -v2285 v180 -v544 -v1311 v1701 -v2286 -v181 -v545 v727 -v1312 -v1897 v2092 -v364 v728 -v1508 -v1703 v2093 -v1314 -v1509 -v184 -v548 -v730 -v925 -v1315 -v1705 -v1900 -v549 -v731 -v926 -v1316 -v1511 -v2096 -v732 -v927 -v2097 -v733 -v928 -v2098 -v2099 -v553 -v735 -v930 -v1320 -v1710 -v8 -v372 -v736 -v931 -v1126 -v1516 -v1906 v9 -v191 -v373 -v555 -v737 -v932 -v1127 -v1322 -v1712 -v1907 -v556 -v1518 -v1713 -v1908 -v2103 -v11 -v375 -v739 -v934 -v1129 -v194 -v13 -v195 -v377 -v741 -v936 -v1131 -v1326 -v1521 -v1716 -v1911 -v197 -v561 -v743 -v938 -v1328 -v1523 -v1718 -v1913 -v198 -v562 -v744 -v939 -v1329 -v1524 -v1719 -v1914 -v17 -v199 -v381 -v745 -v940 -v1135 -v1720 -v1915 -v18 -v382 -v1136 -v1526 -v1721 -v1916 -v747 -v942 -v1527 -v1722 -v1917 -v2112 -v20 -v202 -v384 -v748 -v943 -v1138 -v1333 -v1528 -v21 -v385 -v1139 -v22 -v386 -v568 -v750 -v945 -v1140 -v1335 -v1530 -v2115 -v1336 -v1531 -v24 -v206 -v388 -v1142 -v1337 -v1922 -v25 -v207 -v389 -v753 -v948 -v1143 -v1338 -v1728 -v1923 -v26 -v208 -v390 -v754 -v949 -v1144 -v1729 -v1924 -v755 -v950 -v1145 -v1340 -v1535 -v1730 -v1925 -v27 -v209 -v391 -v1146 -v1341 -v1536 -v1731 -v1926 -v2121 -v210 -v574 -v757 -v952 -v1342 -v1537 -v1732 -v2122 -v1928 -v30 -v212 -v394 -v759 -v954 -v1149 -v1734 -v1929 -v1540 -v2125 -v1541 -v578 -v762 -v957 -v1542 -v1737 -v215 -v763 -v958 -v1348 -v1543 -v1738 -v1933 -v216 -v1349 -v1544 -v1739 -v1934 -v217 -v581 -v765 -v960 -v1350 -v1545 -v1740 -v1935 -v218 -v582 -v766 -v961 -v1351 -v1546 -v1741 -v1936 -v219 -v583 -v767 -v962 -v1352 -v1547 -v220 -v1353 -v1548 -v1743 -v1938 -v223 -v587 -v1356 -v1551 -v1941 -v42 -v406 -v772 -v967 -v1162 -v1357 -v1552 -v43 -v407 -v1163 -v44 -v408 -v590 -v1164 -v1359 -v1554 -v45 -v409 -v1165 -v1945 -v228 -v592 -v776 -v971 -v1361 -v1556 -v1946 -v2141 -v229 -v1362 -v594 -v49 -v231 -v413 -v779 -v974 -v1169 -v1364 -v1559 -v2144 -v232 -v596 -v1365 -v1560 -v1755 -v51 -v415 -v597 -v1171 -v1366 -v1561 -v1951 -v235 -v1564 -v1759 -v2149 -v236 -v785 -v980 -v1370 -v1565 -v1760 -v1955 -v238 -v602 -v787 -v982 -v1372 -v1567 -v1957 -v2152 -v239 -v1373 -v1568 -v240 -v604 -v789 -v984 -v1374 -v1569 -v59 -v423 -v790 -v985 -v1180 -v606 -v791 -v986 -v1376 -v1571 -v1961 -v2156 -v62 -v244 -v426 -v793 -v988 -v1183 -v1963 -v1574 -v2159 -v610 -v1380 -v1575 -v247 -v611 -v1381 -v1576 -v1771 -v1966 -v2161 -v66 -v430 -v612 -v797 -v992 -v1187 -v1577 -v1772 -v1967 -v67 -v249 -v431 -v798 -v993 -v1188 -v1578 -v1773 -v1968 -v68 -v432 -v799 -v994 -v1189 -v1384 -v1774 -v1969 -v69 -v433 -v615 -v800 -v995 -v1190 -v1385 -v1580 -v1775 -v1970 -v70 -v434 -v801 -v996 -v1191 -v1971 -v71 -v435 -v617 -v802 -v997 -v1192 -v1387 -v1582 -v1777 -v1972 -v803 -v998 -v1193 -v1388 -v1583 -v1778 -v72 -v436 -v618 -v804 -v999 -v1194 -v1389 -v1779 -v1974 -v255 -v619 -v805 -v1000 -v1390 -v1780 -v1975 -v74 -v256 v438 -v620 -v806 -v1001 -v1196 -v1391 -v1586 -v1781 v1976 -v2171 -v257 -v807 -v1002 -v1392 -v1587 -v76 -v440 -v808 -v1003 -v1198 -v1978 -v259 -v1394 -v1589 -v1979 -v78 -v442 -v624 -v810 -v1005 -v1200 -v1590 -v1785 -v1980 -v2175 -v1201 -v1396 -v1591 -v1981 -v2176 -v812 -v1007 -v1592 -v80 -v262 -v444 -v1203 -v1398 -v1593 -v814 -v1009 -v1204 -v1399 -v1594 -v1984 -v81 -v263 -v445 -v1205 -v1400 -v1595 -v1790 -v1985 -v2180 -v264 -v83 -v447 -v817 -v1012 -v1207 -v1597 -v1792 -v1987 -v266 -v1403 -v1598 -v1793 -v1988 -v85 -v449 -v819 -v1014 -v1209 -v1794 -v1989 -v1210 -v1405 -v1600 -v1795 -v1990 -v86 -v450 -v632 -v821 -v1016 -v1211 -v1406 -v1601 -v2186 -v87 -v269 -v451 -v822 -v1017 -v1212 -v1407 -v1602 -v1797 -v1992 -v88 v270 -v452 -v634 -v823 -v1018 -v1213 -v1408 -v1603 -v1798 -v1993 -v89 -v271 -v453 -v1214 -v1409 -v1604 -v2189 -v90 -v272 -v454 -v825 -v1020 -v1215 -v1410 -v1605 -v1995 -v273 -v637 -v1411 -v1606 -v1801 -v1996 -v2191 -v274 -v638 -v1412 -v1607 -v1802 -v1997 -v2192 -v276 -v640 -v1414 -v1609 -v1804 -v1999 -v2194 -v277 -v641 -v830 -v1025 -v1415 -v1610 -v96 -v460 -v642 -v831 -v1026 -v1221 -v1806 -v2001 -v832 -v1027 -v1222 -v1417 -v1612 -v1807 -v2002 -v1613 -v2003 -v834 -v1029 -v1419 -v1614 -v1809 -v2004 -v2199 -v1810 -v2200 -v99 -v281 -v463 -v1226 -v2006 -v282 -v646 -v1812 -v2007 -v283 -v1618 -v1813 -v2008 -v284 -v648 -v1424 -v2204 -v285 -v1425 -v650 -v1816 -v2011 -v2206 -v287 -v651 -v842 -v1037 -v2012 -v2207 -v288 -v652 -v1428 -v1623 -v1818 -v2013 -v2208 -v107 -v471 -v653 -v844 -v1039 -v1234 -v1429 -v1624 -v2014 -v2209 -v290 -v654 -v1430 -v1625 -v1820 -v2015 -v2210 -v291 -v655 -v1431 -v1626 -v1821 -v2016 -v2211 -v110 -v474 -v656 -v847 -v1042 v1237 -v1432 -v1627 -v1822 -v2017 -v2212 -v657 -v1433 -v1628 -v2213 -v294 -v658 -v849 -v1044 -v1629 -v1824 -v2019 -v2214 -v113 -v295 -v477 -v850 -v1045 v1240 -v1435 -v1630 -v1825 -v2020 -v2215 -v296 -v1631 -v115 -v479 -v661 -v852 -v1047 v1242 -v1437 -v1632 -v1827 -v2022 -v2217 -v298 -v662 -v853 -v1048 -v1633 -v1828 -v2023 -v2218 -v117 -v481 -v854 -v1049 v1244 -v1439 -v1634 -v1829 -v2024 -v2219 -v118 -v482 -v664 -v855 -v1050 -v1245 -v1440 -v1830 -v2025 -v2220 -v301 -v665 -v856 -v1051 -v1441 -v1636 -v2221 -v666 -v857 -v1052 -v1637 -v2222 -v121 -v485 -v667 -v858 -v1053 -v1248 -v1443 -v1638 -v1833 -v2028 -v304 -v668 -v1444 -v1639 -v1834 -v2029 -v671 -v862 -v1057 -v1447 -v1642 -v2032 -v308 -v1448 -v1643 -v1838 -v2033 -v1644 -v128 -v492 -v311 -v675 -v1450 -v1645 -v130 -v494 -v676 -v866 -v1061 -v1256 -v1451 -v1646 -v1841 -v2036 -v132 -v496 -v678 -v868 -v1063 -v1258 -v1648 -v1843 -v2038 -v2233 -v134 -v316 -v498 -v1260 -v1455 -v1650 -v2235 -v317 -v681 -v1651 -v1846 -v2041 -v2236 -v137 -v319 -v501 -v873 -v1068 -v1263 -v1458 -v1653 -v1848 -v2043 -v138 -v502 -v684 -v1264 -v1459 -v1654 -v1849 -v2239 -v321 -v685 -v875 -v1070 -v1655 -v2045 -v1267 -v2047 -v2048 -v324 -v880 -v1075 -v1660 -v1855 -v2050 -v1661 -v2248 -v2249 -v1665 -v2250 -v692 -v886 -v1081 -v693 -v148 -v330 -v512 -v888 -v1083 -v1278 -v1863 -v2058 -v149 -v331 -v513 -v889 -v1084 -v1279 -v1864 -v2059 -v2254 -v332 -v696 -v1475 -v1670 -v1865 -v2060 -v2255 -v697 -v1866 -v2256 -v152 -v516 -v698 -v1282 -v1867 -v2062 -v2257 -v153 -v517 -v1283 -v1868 -v2063 -v700 -v2064 -v2259 -v337 -v701 -v1480 -v1870 -v2065 -v2260 -v702 -v1871 -v2261 -v703 -v1482 -v2067 -v2262 -v158 -v522 -v704 -v898 -v1093 -v1288 -v1678 -v2263 -v1484 -v1874 -v2264 -v160 -v524 -v706 -v900 -v1095 -v1290 -v1485 -v1680 -v1875 -v2070 -v343 -v707 -v901 -v1096 -v1486 -v1876 -v2071 -v162 -v526 -v708 -v902 -v1097 -v1292 -v1487 -v1877 -v2072 -v709 -v1488 -v2073 -v2268 -v1881 -v349 -v713 -v907 -v1102 -v1492 -v2077 -v2272 -v714 -v908 -v1103 -v1493 -v1883 -v2078 -v1884 -v2079 -v716 -v717 -v912 -v1107 -v1497 -v2277 -v1693 -v719 -v1889 -v2084 -v2279 -v720 -v1890 -v2085 -v2280 -v721 -v176 -v540 -v917 -v1112 -v1307 -v2282 -v177 -v541 -v723 -v918 -v1113 -v1308 -v1893 -v2088 -v724 -v1504 -v1894 -v361 -v725 -v920 -v1115 -v1505 -v362 -v726 -v921 -v1116 -v1506 -v1896 -v2091 -v363 -v1507 -v1702 -v182 -v546 -v923 -v1118 -v1313 -v1898 -v2288 one -v7 -v12 -v19 -v31 -v39 -v40 -v47 -v53 -v57 -v79 -v82 -v93 -v97 -v98 -v123 -v124 -v126 -v141 -v144 -v147 -v156 -v164 -v165 -v166 -v170 -v173 -v175 -v183 -v185 -v189 -v190 -v196 v200 v201 -v203 -v211 -v213 -v214 -v221 -v224 -v225 -v234 -v237 -v245 -v246 v250 -v258 -v261 -v267 v268 -v275 -v279 -v280 -v302 -v306 -v309 -v310 -v323 -v326 -v327 -v328 -v333 v334 -v336 v338 v340 -v346 -v348 -v352 -v354 -v355 -v356 -v357 v371 -v376 -v383 -v395 -v403 -v404 -v411 -v446 -v457 -v487 v488 -v490 -v495 -v504 -v505 -v511 -v520 -v529 -v530 v534 v537 -v547 -v550 -v551 -v552 -v557 v558 -v564 -v565 -v569 -v575 v577 -v579 -v580 -v584 v585 -v586 -v591 v593 -v598 -v600 -v601 -v607 -v614 -v623 v639 -v647 -v649 -v669 -v670 -v677 -v679 -v682 -v686 -v711 v712 -v740 -v746 -v749 -v752 -v758 -v760 -v761 -v764 -v768 -v769 -v770 -v775 -v777 -v781 -v782 -v783 -v786 -v788 -v794 -v795 v809 -v816 -v833 -v836 -v838 -v840 -v851 -v859 -v860 -v861 -v864 -v869 -v876 -v881 -v882 -v883 -v884 -v885 -v887 -v896 -v903 -v905 -v906 -v910 -v911 -v913 -v914 -v922 -v935 -v941 -v944 -v947 -v953 -v955 -v956 -v965 -v970 -v972 -v977 -v978 -v981 -v983 -v989 -v990 -v1004 -v1011 -v1033 -v1035 -v1046 -v1054 -v1055 -v1056 -v1059 -v1060 -v1062 -v1064 -v1071 -v1076 -v1077 -v1078 -v1079 -v1080 -v1082 -v1091 -v1100 -v1101 -v1105 -v1108 -v1109 -v1111 -v1117 -v1125 v1130 v1137 -v1150 -v1151 -v1159 -v1160 -v1167 -v1172 -v1174 -v1178 -v1202 -v1206 -v1218 -v1223 -v1225 v1250 -v1251 -v1253 -v1257 -v1266 -v1268 -v1271 -v1273 -v1274 -v1275 -v1277 -v1286 -v1295 v1296 -v1301 -v1304 -v1306 -v1321 -v1325 -v1327 v1331 -v1332 -v1347 -v1354 -v1355 -v1360 -v1367 -v1368 -v1371 -v1375 -v1377 -v1378 -v1379 -v1397 -v1401 -v1404 -v1413 -v1418 -v1421 -v1423 -v1436 -v1442 -v1445 -v1446 -v1449 -v1454 -v1457 -v1461 -v1462 -v1463 -v1466 -v1467 -v1471 -v1472 -v1473 -v1481 v1483 -v1489 -v1490 -v1491 -v1496 -v1498 v1499 -v1500 -v1503 v1517 -v1520 -v1522 -v1529 -v1533 -v1538 -v1549 -v1553 -v1558 -v1562 -v1563 -v1566 -v1570 -v1572 -v1573 v1579 -v1581 -v1599 -v1608 -v1611 -v1616 -v1617 -v1621 -v1640 -v1641 -v1652 -v1656 -v1657 -v1662 -v1663 -v1664 -v1666 -v1667 -v1681 v1682 -v1686 -v1687 -v1688 -v1689 -v1691 -v1694 -v1696 -v1699 -v1715 -v1717 -v1724 -v1733 -v1735 -v1736 -v1742 -v1744 -v1745 -v1746 -v1747 -v1749 -v1753 -v1758 -v1761 -v1764 -v1767 -v1769 -v1770 -v1776 -v1782 -v1783 -v1784 -v1803 -v1805 -v1808 -v1811 -v1814 v1819 -v1823 -v1835 -v1836 -v1840 -v1842 -v1845 -v1850 -v1852 -v1857 -v1860 -v1873 -v1880 -v1885 -v1886 -v1887 -v1888 -v1891 -v1895 -v1901 -v1905 -v1909 -v1910 -v1912 -v1919 -v1930 -v1931 v1932 -v1937 -v1939 -v1940 -v1943 -v1944 -v1947 -v1948 -v1949 -v1952 -v1954 v1956 -v1958 -v1959 -v1960 -v1962 -v1964 -v1965 v1973 -v1977 -v1982 -v1986 -v1991 -v1994 -v1998 -v2000 -v2005 -v2009 -v2021 -v2027 -v2030 v2031 -v2034 -v2035 -v2037 -v2040 -v2044 -v2046 -v2051 -v2052 -v2053 -v2054 -v2055 -v2056 -v2057 -v2066 -v2068 -v2075 -v2076 -v2080 -v2081 -v2086 -v2089 -v2090 -v2094 -v2101 -v2102 -v2105 -v2111 -v2123 -v2126 -v2127 -v2137 -v2138 -v2139 -v2142 -v2143 -v2148 -v2153 -v2157 -v2158 -v2166 -v2173 -v2174 -v2177 -v2193 -v2205 -v2216 -v2225 -v2226 -v2228 -v2229 -v2232 -v2234 -v2243 -v2246 -v2251 -v2252 -v2271 -v2275 -v2281 -v2287
c _______________________________________________________________________________
c 
c restarts              : 176
c conflicts             : 264729         (239 /sec)
c decisions             : 1292116        (1165 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1109.59 s
c _______________________________________________________________________________
#### 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.91 0.95 0.90 2/54 29792
Raw data (stat): 29792 (runsolver) R 29791 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853790623 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+9.99974 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0033 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0028 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0037 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0042 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29796
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.018 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 29843
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.018 s]
Raw data (loadavg): 1.14 1.00 0.92 2/55 29849
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.018 s]
Raw data (loadavg): 1.11 1.00 0.92 2/55 29849
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.018 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 29849
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.018 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 29849
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.019 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 29849
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.019 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 29849
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.019 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 29849
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.019 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.018 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.019 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.019 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.018 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.02 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.02 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.019 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29851
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.56 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 29853
Raw data (stat): 29792 (minisat+_script) S 29791 3394 3393 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853790623 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 30
Real time (s): 1110.56
CPU time (s): 1110.69
CPU user time (s): 1109.67
CPU system time (s): 1.01285
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	813
#### END VERIFIER DATA ####