PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos16.opb
MD5SUM	44281820d2b00a47b643433ffa4e2d73
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	117
Optimality of the best value was proved	NO
Number of terms in the objective function	8
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	255
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	138
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	535
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	5.96709
Number of variables	464
Total number of constraints	1395
Number of constraints which are clauses	336
Number of constraints which are cardinality constraints (but not clauses)	336
Number of constraints which are nor clauses,nor cardinality constraints	723
Minimum length of a constraint	1
Maximum length of a constraint	128
Trace number 30914

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-05-25 20:46:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22307 boxname=wulflinc24 idbench=1123 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  44281820d2b00a47b643433ffa4e2d73  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-neos16.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-neos16.opb
IDLAUNCH: 22307
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        547456 kB
Buffers:         32816 kB
Cached:         432396 kB
SwapCached:        588 kB
Active:          83420 kB
Inactive:       383884 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        547204 kB
SwapTotal:     2097892 kB
SwapFree:      2096416 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5160 kB
Slab:            14216 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 21:07:29 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 22307 7 1229.84 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1069 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................
c ---[1028]---> BDD-cost:    7
c ---[1026]---> Sorter-cost:  252     Base: 2 2
c ---[1024]---> Sorter-cost:  252     Base: 2 2
c ---[1022]---> Sorter-cost:  251     Base: 2 2
c ---[1020]---> Sorter-cost:  252     Base: 2 2
c ---[1018]---> Sorter-cost:  251     Base: 2 2
c ---[1016]---> Sorter-cost:  252     Base: 2 2
c ---[1014]---> Sorter-cost:  252     Base: 2 2
c ---[1012]---> Sorter-cost:  252     Base: 2 2
c ---[1010]---> Sorter-cost:  251     Base: 2 2
c ---[1009]---> BDD-cost:   11
c ---[1008]---> BDD-cost:   11
c ---[1007]---> BDD-cost:   11
c ---[1006]---> BDD-cost:   11
c ---[1005]---> BDD-cost:   11
c ---[1004]---> BDD-cost:   11
c ---[1003]---> BDD-cost:   11
c ---[1002]---> BDD-cost:   11
c ---[1001]---> BDD-cost:   11
c ---[1000]---> BDD-cost:   11
c ---[ 999]---> BDD-cost:   11
c ---[ 998]---> BDD-cost:   11
c ---[ 997]---> BDD-cost:   11
c ---[ 996]---> BDD-cost:   11
c ---[ 995]---> BDD-cost:   11
c ---[ 994]---> BDD-cost:   11
c ---[ 993]---> BDD-cost:   11
c ---[ 992]---> BDD-cost:   11
c ---[ 991]---> BDD-cost:   11
c ---[ 990]---> BDD-cost:   11
c ---[ 989]---> BDD-cost:   11
c ---[ 988]---> BDD-cost:   11
c ---[ 987]---> BDD-cost:   11
c ---[ 986]---> BDD-cost:   11
c ---[ 985]---> BDD-cost:   11
c ---[ 984]---> BDD-cost:   11
c ---[ 983]---> BDD-cost:   11
c ---[ 982]---> BDD-cost:   11
c ---[ 981]---> BDD-cost:   11
c ---[ 980]---> BDD-cost:   11
c ---[ 979]---> BDD-cost:   11
c ---[ 978]---> BDD-cost:   11
c ---[ 977]---> BDD-cost:   11
c ---[ 976]---> BDD-cost:   11
c ---[ 975]---> BDD-cost:   11
c ---[ 974]---> BDD-cost:   11
c ---[ 973]---> BDD-cost:   11
c ---[ 972]---> BDD-cost:   11
c ---[ 971]---> BDD-cost:   11
c ---[ 970]---> BDD-cost:   11
c ---[ 969]---> BDD-cost:   11
c ---[ 968]---> BDD-cost:   11
c ---[ 967]---> BDD-cost:   11
c ---[ 966]---> BDD-cost:   11
c ---[ 965]---> BDD-cost:   11
c ---[ 964]---> BDD-cost:   11
c ---[ 963]---> BDD-cost:   11
c ---[ 962]---> BDD-cost:   11
c ---[ 961]---> BDD-cost:   11
c ---[ 960]---> BDD-cost:   11
c ---[ 959]---> BDD-cost:   11
c ---[ 958]---> BDD-cost:   11
c ---[ 957]---> BDD-cost:   11
c ---[ 956]---> BDD-cost:   11
c ---[ 955]---> BDD-cost:   11
c ---[ 954]---> BDD-cost:   11
c ---[ 953]---> BDD-cost:   11
c ---[ 952]---> BDD-cost:   11
c ---[ 951]---> BDD-cost:   11
c ---[ 950]---> BDD-cost:   11
c ---[ 949]---> BDD-cost:   11
c ---[ 948]---> BDD-cost:   11
c ---[ 947]---> BDD-cost:   11
c ---[ 946]---> BDD-cost:   11
c ---[ 945]---> BDD-cost:   11
c ---[ 944]---> BDD-cost:   11
c ---[ 943]---> BDD-cost:   11
c ---[ 942]---> BDD-cost:   11
c ---[ 941]---> BDD-cost:   11
c ---[ 940]---> BDD-cost:   11
c ---[ 939]---> BDD-cost:   11
c ---[ 938]---> BDD-cost:   11
c ---[ 937]---> BDD-cost:   11
c ---[ 936]---> BDD-cost:   11
c ---[ 935]---> BDD-cost:   11
c ---[ 934]---> BDD-cost:   11
c ---[ 933]---> BDD-cost:   11
c ---[ 932]---> BDD-cost:   11
c ---[ 931]---> BDD-cost:   11
c ---[ 930]---> BDD-cost:   11
c ---[ 929]---> BDD-cost:   11
c ---[ 928]---> BDD-cost:   11
c ---[ 927]---> BDD-cost:   11
c ---[ 926]---> BDD-cost:   11
c ---[ 925]---> BDD-cost:    6
c ---[ 924]---> BDD-cost:    6
c ---[ 923]---> BDD-cost:    6
c ---[ 922]---> BDD-cost:    6
c ---[ 921]---> BDD-cost:    6
c ---[ 920]---> BDD-cost:    6
c ---[ 919]---> BDD-cost:    6
c ---[ 918]---> BDD-cost:    6
c ---[ 917]---> BDD-cost:    6
c ---[ 916]---> BDD-cost:    6
c ---[ 915]---> BDD-cost:    6
c ---[ 914]---> BDD-cost:    6
c ---[ 913]---> BDD-cost:    6
c ---[ 912]---> BDD-cost:    6
c ---[ 911]---> BDD-cost:    6
c ---[ 910]---> BDD-cost:    6
c ---[ 909]---> BDD-cost:    6
c ---[ 908]---> BDD-cost:    6
c ---[ 907]---> BDD-cost:    6
c ---[ 906]---> BDD-cost:    6
c ---[ 905]---> BDD-cost:    6
c ---[ 904]---> BDD-cost:    6
c ---[ 903]---> BDD-cost:    6
c ---[ 902]---> BDD-cost:    6
c ---[ 901]---> BDD-cost:    6
c ---[ 900]---> BDD-cost:    6
c ---[ 899]---> BDD-cost:    6
c ---[ 898]---> BDD-cost:    6
c ---[ 897]---> BDD-cost:    6
c ---[ 896]---> BDD-cost:    6
c ---[ 895]---> BDD-cost:    6
c ---[ 894]---> BDD-cost:    6
c ---[ 893]---> BDD-cost:    6
c ---[ 892]---> BDD-cost:    6
c ---[ 891]---> BDD-cost:    6
c ---[ 890]---> BDD-cost:    6
c ---[ 889]---> BDD-cost:    6
c ---[ 888]---> BDD-cost:    6
c ---[ 887]---> BDD-cost:    6
c ---[ 886]---> BDD-cost:    6
c ---[ 885]---> BDD-cost:    6
c ---[ 884]---> BDD-cost:    6
c ---[ 883]---> BDD-cost:    6
c ---[ 882]---> BDD-cost:    6
c ---[ 881]---> BDD-cost:    6
c ---[ 880]---> BDD-cost:    6
c ---[ 879]---> BDD-cost:    6
c ---[ 878]---> BDD-cost:    6
c ---[ 877]---> BDD-cost:    6
c ---[ 876]---> BDD-cost:    6
c ---[ 875]---> BDD-cost:    6
c ---[ 874]---> BDD-cost:    6
c ---[ 873]---> BDD-cost:    6
c ---[ 872]---> BDD-cost:    6
c ---[ 871]---> BDD-cost:    6
c ---[ 870]---> BDD-cost:    6
c ---[ 869]---> BDD-cost:    6
c ---[ 868]---> BDD-cost:    6
c ---[ 867]---> BDD-cost:    6
c ---[ 866]---> BDD-cost:    6
c ---[ 865]---> BDD-cost:    6
c ---[ 864]---> BDD-cost:    6
c ---[ 863]---> BDD-cost:    6
c ---[ 862]---> BDD-cost:    6
c ---[ 861]---> BDD-cost:    6
c ---[ 860]---> BDD-cost:    6
c ---[ 859]---> BDD-cost:    6
c ---[ 858]---> BDD-cost:    6
c ---[ 857]---> BDD-cost:    6
c ---[ 856]---> BDD-cost:    6
c ---[ 855]---> BDD-cost:    6
c ---[ 854]---> BDD-cost:    6
c ---[ 853]---> BDD-cost:    6
c ---[ 852]---> BDD-cost:    6
c ---[ 851]---> BDD-cost:    6
c ---[ 850]---> BDD-cost:    6
c ---[ 849]---> BDD-cost:    6
c ---[ 848]---> BDD-cost:    6
c ---[ 847]---> BDD-cost:    6
c ---[ 846]---> BDD-cost:    6
c ---[ 845]---> BDD-cost:    6
c ---[ 844]---> BDD-cost:    6
c ---[ 843]---> BDD-cost:    6
c ---[ 842]---> BDD-cost:    6
c ---[ 841]---> BDD-cost:    6
c ---[ 840]---> BDD-cost:    6
c ---[ 839]---> BDD-cost:    6
c ---[ 838]---> BDD-cost:    6
c ---[ 837]---> BDD-cost:    6
c ---[ 836]---> BDD-cost:    6
c ---[ 835]---> BDD-cost:    6
c ---[ 834]---> BDD-cost:    6
c ---[ 833]---> BDD-cost:    6
c ---[ 832]---> BDD-cost:    6
c ---[ 831]---> BDD-cost:    6
c ---[ 830]---> BDD-cost:    6
c ---[ 829]---> BDD-cost:    6
c ---[ 828]---> BDD-cost:    6
c ---[ 827]---> BDD-cost:    6
c ---[ 826]---> BDD-cost:    6
c ---[ 825]---> BDD-cost:    6
c ---[ 824]---> BDD-cost:    6
c ---[ 823]---> BDD-cost:    6
c ---[ 822]---> BDD-cost:    6
c ---[ 821]---> BDD-cost:    6
c ---[ 820]---> BDD-cost:    6
c ---[ 819]---> BDD-cost:    6
c ---[ 818]---> BDD-cost:    6
c ---[ 817]---> BDD-cost:    6
c ---[ 816]---> BDD-cost:    6
c ---[ 815]---> BDD-cost:    6
c ---[ 814]---> BDD-cost:    6
c ---[ 813]---> BDD-cost:    6
c ---[ 812]---> BDD-cost:    6
c ---[ 811]---> BDD-cost:    6
c ---[ 810]---> BDD-cost:    6
c ---[ 809]---> BDD-cost:    6
c ---[ 808]---> BDD-cost:    6
c ---[ 807]---> BDD-cost:    6
c ---[ 806]---> BDD-cost:    6
c ---[ 805]---> BDD-cost:    6
c ---[ 804]---> BDD-cost:    6
c ---[ 803]---> BDD-cost:    6
c ---[ 802]---> BDD-cost:    6
c ---[ 801]---> BDD-cost:    6
c ---[ 800]---> BDD-cost:    6
c ---[ 799]---> BDD-cost:    6
c ---[ 798]---> BDD-cost:    6
c ---[ 797]---> BDD-cost:    6
c ---[ 796]---> BDD-cost:    6
c ---[ 795]---> BDD-cost:    6
c ---[ 794]---> BDD-cost:    6
c ---[ 793]---> BDD-cost:    6
c ---[ 792]---> BDD-cost:    6
c ---[ 791]---> BDD-cost:    6
c ---[ 790]---> BDD-cost:    6
c ---[ 789]---> BDD-cost:    6
c ---[ 788]---> BDD-cost:    6
c ---[ 787]---> BDD-cost:    6
c ---[ 786]---> BDD-cost:    6
c ---[ 785]---> BDD-cost:    6
c ---[ 784]---> BDD-cost:    6
c ---[ 783]---> BDD-cost:    6
c ---[ 782]---> BDD-cost:    6
c ---[ 781]---> BDD-cost:    6
c ---[ 780]---> BDD-cost:    6
c ---[ 779]---> BDD-cost:    6
c ---[ 778]---> BDD-cost:    6
c ---[ 777]---> BDD-cost:    6
c ---[ 776]---> BDD-cost:    6
c ---[ 775]---> BDD-cost:    6
c ---[ 774]---> BDD-cost:    6
c ---[ 773]---> BDD-cost:    6
c ---[ 772]---> BDD-cost:    6
c ---[ 771]---> BDD-cost:    6
c ---[ 770]---> BDD-cost:    6
c ---[ 769]---> BDD-cost:    6
c ---[ 768]---> BDD-cost:    6
c ---[ 767]---> BDD-cost:    6
c ---[ 766]---> BDD-cost:    6
c ---[ 765]---> BDD-cost:    6
c ---[ 764]---> BDD-cost:    6
c ---[ 763]---> BDD-cost:    6
c ---[ 762]---> BDD-cost:    6
c ---[ 761]---> BDD-cost:    6
c ---[ 760]---> BDD-cost:    6
c ---[ 759]---> BDD-cost:    6
c ---[ 758]---> BDD-cost:    6
c ---[ 757]---> BDD-cost:    1
c ---[ 756]---> BDD-cost:    1
c ---[ 755]---> BDD-cost:    1
c ---[ 754]---> BDD-cost:    1
c ---[ 753]---> BDD-cost:    1
c ---[ 752]---> BDD-cost:    1
c ---[ 751]---> BDD-cost:    1
c ---[ 750]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    1
c ---[ 747]---> BDD-cost:    1
c ---[ 746]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 744]---> BDD-cost:    1
c ---[ 743]---> BDD-cost:    1
c ---[ 742]---> BDD-cost:    1
c ---[ 741]---> BDD-cost:    1
c ---[ 740]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 737]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 735]---> BDD-cost:    1
c ---[ 734]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 732]---> BDD-cost:    1
c ---[ 731]---> BDD-cost:    1
c ---[ 730]---> BDD-cost:    1
c ---[ 729]---> BDD-cost:    1
c ---[ 728]---> BDD-cost:    1
c ---[ 727]---> BDD-cost:    1
c ---[ 726]---> BDD-cost:    1
c ---[ 725]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    1
c ---[ 723]---> BDD-cost:    1
c ---[ 722]---> BDD-cost:    1
c ---[ 721]---> BDD-cost:    1
c ---[ 720]---> BDD-cost:    1
c ---[ 719]---> BDD-cost:    1
c ---[ 718]---> BDD-cost:    1
c ---[ 717]---> BDD-cost:    1
c ---[ 716]---> BDD-cost:    1
c ---[ 715]---> BDD-cost:    1
c ---[ 714]---> BDD-cost:    1
c ---[ 713]---> BDD-cost:    1
c ---[ 712]---> BDD-cost:    1
c ---[ 711]---> BDD-cost:    1
c ---[ 710]---> BDD-cost:    1
c ---[ 709]---> BDD-cost:    1
c ---[ 708]---> BDD-cost:    1
c ---[ 707]---> BDD-cost:    1
c ---[ 706]---> BDD-cost:    1
c ---[ 705]---> BDD-cost:    1
c ---[ 704]---> BDD-cost:    1
c ---[ 703]---> BDD-cost:    1
c ---[ 702]---> BDD-cost:    1
c ---[ 701]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 699]---> BDD-cost:    1
c ---[ 698]---> BDD-cost:    1
c ---[ 697]---> BDD-cost:    1
c ---[ 696]---> BDD-cost:    1
c ---[ 695]---> BDD-cost:    1
c ---[ 694]---> BDD-cost:    1
c ---[ 693]---> BDD-cost:    1
c ---[ 692]---> BDD-cost:    1
c ---[ 691]---> BDD-cost:    1
c ---[ 690]---> BDD-cost:    1
c ---[ 689]---> BDD-cost:    1
c ---[ 688]---> BDD-cost:    1
c ---[ 687]---> BDD-cost:    1
c ---[ 686]---> BDD-cost:    1
c ---[ 685]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 683]---> BDD-cost:    1
c ---[ 682]---> BDD-cost:    1
c ---[ 681]---> BDD-cost:    1
c ---[ 680]---> BDD-cost:    1
c ---[ 679]---> BDD-cost:    1
c ---[ 678]---> BDD-cost:    1
c ---[ 677]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 675]---> BDD-cost:    1
c ---[ 674]---> BDD-cost:    1
c ---[ 505]---> BDD-cost:   11
c ---[ 504]---> BDD-cost:   11
c ---[ 503]---> BDD-cost:   11
c ---[ 502]---> BDD-cost:   11
c ---[ 501]---> BDD-cost:   11
c ---[ 500]---> BDD-cost:   11
c ---[ 499]---> BDD-cost:   11
c ---[ 498]---> BDD-cost:   11
c ---[ 497]---> BDD-cost:   11
c ---[ 496]---> BDD-cost:   11
c ---[ 495]---> BDD-cost:   11
c ---[ 494]---> BDD-cost:   11
c ---[ 493]---> BDD-cost:   11
c ---[ 492]---> BDD-cost:   11
c ---[ 491]---> BDD-cost:   11
c ---[ 490]---> BDD-cost:   11
c ---[ 489]---> BDD-cost:   11
c ---[ 488]---> BDD-cost:   11
c ---[ 487]---> BDD-cost:   11
c ---[ 486]---> BDD-cost:   11
c ---[ 485]---> BDD-cost:   11
c ---[ 484]---> BDD-cost:   11
c ---[ 483]---> BDD-cost:   11
c ---[ 482]---> BDD-cost:   11
c ---[ 481]---> BDD-cost:   11
c ---[ 480]---> BDD-cost:   11
c ---[ 479]---> BDD-cost:   11
c ---[ 478]---> BDD-cost:   11
c ---[ 477]---> BDD-cost:   11
c ---[ 476]---> BDD-cost:   11
c ---[ 475]---> BDD-cost:   11
c ---[ 474]---> BDD-cost:   11
c ---[ 473]---> BDD-cost:   11
c ---[ 472]---> BDD-cost:   11
c ---[ 471]---> BDD-cost:   11
c ---[ 470]---> BDD-cost:   11
c ---[ 469]---> BDD-cost:   11
c ---[ 468]---> BDD-cost:   11
c ---[ 467]---> BDD-cost:   11
c ---[ 466]---> BDD-cost:   11
c ---[ 465]---> BDD-cost:   11
c ---[ 464]---> BDD-cost:   11
c ---[ 463]---> BDD-cost:   11
c ---[ 462]---> BDD-cost:   11
c ---[ 461]---> BDD-cost:   11
c ---[ 460]---> BDD-cost:   11
c ---[ 459]---> BDD-cost:   11
c ---[ 458]---> BDD-cost:   11
c ---[ 457]---> BDD-cost:   11
c ---[ 456]---> BDD-cost:   11
c ---[ 455]---> BDD-cost:   11
c ---[ 454]---> BDD-cost:   11
c ---[ 453]---> BDD-cost:   11
c ---[ 452]---> BDD-cost:   11
c ---[ 451]---> BDD-cost:   11
c ---[ 450]---> BDD-cost:   11
c ---[ 449]---> BDD-cost:   11
c ---[ 448]---> BDD-cost:   11
c ---[ 447]---> BDD-cost:   11
c ---[ 446]---> BDD-cost:   11
c ---[ 445]---> BDD-cost:   11
c ---[ 444]---> BDD-cost:   11
c ---[ 443]---> BDD-cost:   11
c ---[ 442]---> BDD-cost:   11
c ---[ 441]---> BDD-cost:   11
c ---[ 440]---> BDD-cost:   11
c ---[ 439]---> BDD-cost:   11
c ---[ 438]---> BDD-cost:   11
c ---[ 437]---> BDD-cost:   11
c ---[ 436]---> BDD-cost:   11
c ---[ 435]---> BDD-cost:   11
c ---[ 434]---> BDD-cost:   11
c ---[ 433]---> BDD-cost:   11
c ---[ 432]---> BDD-cost:   11
c ---[ 431]---> BDD-cost:   11
c ---[ 430]---> BDD-cost:   11
c ---[ 429]---> BDD-cost:   11
c ---[ 428]---> BDD-cost:   11
c ---[ 427]---> BDD-cost:   11
c ---[ 426]---> BDD-cost:   11
c ---[ 425]---> BDD-cost:   11
c ---[ 424]---> BDD-cost:   11
c ---[ 423]---> BDD-cost:   11
c ---[ 422]---> BDD-cost:   11
c ---[ 421]---> BDD-cost:    6
c ---[ 420]---> BDD-cost:    6
c ---[ 419]---> BDD-cost:    6
c ---[ 418]---> BDD-cost:    6
c ---[ 417]---> BDD-cost:    6
c ---[ 416]---> BDD-cost:    6
c ---[ 415]---> BDD-cost:    6
c ---[ 414]---> BDD-cost:    6
c ---[ 413]---> BDD-cost:    6
c ---[ 412]---> BDD-cost:    6
c ---[ 411]---> BDD-cost:    6
c ---[ 410]---> BDD-cost:    6
c ---[ 409]---> BDD-cost:    6
c ---[ 408]---> BDD-cost:    6
c ---[ 407]---> BDD-cost:    6
c ---[ 406]---> BDD-cost:    6
c ---[ 405]---> BDD-cost:    6
c ---[ 404]---> BDD-cost:    6
c ---[ 403]---> BDD-cost:    6
c ---[ 402]---> BDD-cost:    6
c ---[ 401]---> BDD-cost:    6
c ---[ 400]---> BDD-cost:    6
c ---[ 399]---> BDD-cost:    6
c ---[ 398]---> BDD-cost:    6
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    6
c ---[ 394]---> BDD-cost:    6
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    6
c ---[ 390]---> BDD-cost:    6
c ---[ 389]---> BDD-cost:    6
c ---[ 388]---> BDD-cost:    6
c ---[ 387]---> BDD-cost:    6
c ---[ 386]---> BDD-cost:    6
c ---[ 385]---> BDD-cost:    6
c ---[ 384]---> BDD-cost:    6
c ---[ 383]---> BDD-cost:    6
c ---[ 382]---> BDD-cost:    6
c ---[ 381]---> BDD-cost:    6
c ---[ 380]---> BDD-cost:    6
c ---[ 379]---> BDD-cost:    6
c ---[ 378]---> BDD-cost:    6
c ---[ 377]---> BDD-cost:    6
c ---[ 376]---> BDD-cost:    6
c ---[ 375]---> BDD-cost:    6
c ---[ 374]---> BDD-cost:    6
c ---[ 373]---> BDD-cost:    6
c ---[ 372]---> BDD-cost:    6
c ---[ 371]---> BDD-cost:    6
c ---[ 370]---> BDD-cost:    6
c ---[ 369]---> BDD-cost:    6
c ---[ 368]---> BDD-cost:    6
c ---[ 367]---> BDD-cost:    6
c ---[ 366]---> BDD-cost:    6
c ---[ 365]---> BDD-cost:    6
c ---[ 364]---> BDD-cost:    6
c ---[ 363]---> BDD-cost:    6
c ---[ 362]---> BDD-cost:    6
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:    6
c ---[ 359]---> BDD-cost:    6
c ---[ 358]---> BDD-cost:    6
c ---[ 357]---> BDD-cost:    6
c ---[ 356]---> BDD-cost:    6
c ---[ 355]---> BDD-cost:    6
c ---[ 354]---> BDD-cost:    6
c ---[ 353]---> BDD-cost:    6
c ---[ 352]---> BDD-cost:    6
c ---[ 351]---> BDD-cost:    6
c ---[ 350]---> BDD-cost:    6
c ---[ 349]---> BDD-cost:    6
c ---[ 348]---> BDD-cost:    6
c ---[ 347]---> BDD-cost:    6
c ---[ 346]---> BDD-cost:    6
c ---[ 345]---> BDD-cost:    6
c ---[ 344]---> BDD-cost:    6
c ---[ 343]---> BDD-cost:    6
c ---[ 342]---> BDD-cost:    6
c ---[ 341]---> BDD-cost:    6
c ---[ 340]---> BDD-cost:    6
c ---[ 339]---> BDD-cost:    6
c ---[ 338]---> BDD-cost:    6
c ---[ 337]---> BDD-cost:    6
c ---[ 336]---> BDD-cost:    6
c ---[ 335]---> BDD-cost:    6
c ---[ 334]---> BDD-cost:    6
c ---[ 333]---> BDD-cost:    6
c ---[ 332]---> BDD-cost:    6
c ---[ 331]---> BDD-cost:    6
c ---[ 330]---> BDD-cost:    6
c ---[ 329]---> BDD-cost:    6
c ---[ 328]---> BDD-cost:    6
c ---[ 327]---> BDD-cost:    6
c ---[ 326]---> BDD-cost:    6
c ---[ 325]---> BDD-cost:    6
c ---[ 324]---> BDD-cost:    6
c ---[ 323]---> BDD-cost:    6
c ---[ 322]---> BDD-cost:    6
c ---[ 321]---> BDD-cost:    6
c ---[ 320]---> BDD-cost:    6
c ---[ 319]---> BDD-cost:    6
c ---[ 318]---> BDD-cost:    6
c ---[ 317]---> BDD-cost:    6
c ---[ 316]---> BDD-cost:    6
c ---[ 315]---> BDD-cost:    6
c ---[ 314]---> BDD-cost:    6
c ---[ 313]---> BDD-cost:    6
c ---[ 312]---> BDD-cost:    6
c ---[ 311]---> BDD-cost:    6
c ---[ 310]---> BDD-cost:    6
c ---[ 309]---> BDD-cost:    6
c ---[ 308]---> BDD-cost:    6
c ---[ 307]---> BDD-cost:    6
c ---[ 306]---> BDD-cost:    6
c ---[ 305]---> BDD-cost:    6
c ---[ 304]---> BDD-cost:    6
c ---[ 303]---> BDD-cost:    6
c ---[ 302]---> BDD-cost:    6
c ---[ 301]---> BDD-cost:    6
c ---[ 300]---> BDD-cost:    6
c ---[ 299]---> BDD-cost:    6
c ---[ 298]---> BDD-cost:    6
c ---[ 297]---> BDD-cost:    6
c ---[ 296]---> BDD-cost:    6
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    6
c ---[ 293]---> BDD-cost:    6
c ---[ 292]---> BDD-cost:    6
c ---[ 291]---> BDD-cost:    6
c ---[ 290]---> BDD-cost:    6
c ---[ 289]---> BDD-cost:    6
c ---[ 288]---> BDD-cost:    6
c ---[ 287]---> BDD-cost:    6
c ---[ 286]---> BDD-cost:    6
c ---[ 285]---> BDD-cost:    6
c ---[ 284]---> BDD-cost:    6
c ---[ 283]---> BDD-cost:    6
c ---[ 282]---> BDD-cost:    6
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:    6
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:    6
c ---[ 277]---> BDD-cost:    6
c ---[ 276]---> BDD-cost:    6
c ---[ 275]---> BDD-cost:    6
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    6
c ---[ 272]---> BDD-cost:    6
c ---[ 271]---> BDD-cost:    6
c ---[ 270]---> BDD-cost:    6
c ---[ 269]---> BDD-cost:    6
c ---[ 268]---> BDD-cost:    6
c ---[ 267]---> BDD-cost:    6
c ---[ 266]---> BDD-cost:    6
c ---[ 265]---> BDD-cost:    6
c ---[ 264]---> BDD-cost:    6
c ---[ 263]---> BDD-cost:    6
c ---[ 262]---> BDD-cost:    6
c ---[ 261]---> BDD-cost:    6
c ---[ 260]---> BDD-cost:    6
c ---[ 259]---> BDD-cost:    6
c ---[ 258]---> BDD-cost:    6
c ---[ 257]---> BDD-cost:    6
c ---[ 256]---> BDD-cost:    6
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    6
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:    1
c ---[ 251]---> BDD-cost:    1
c ---[ 250]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 247]---> BDD-cost:    1
c ---[ 246]---> BDD-cost:    1
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:    1
c ---[ 242]---> BDD-cost:    1
c ---[ 241]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:    1
c ---[ 234]---> BDD-cost:    1
c ---[ 233]---> BDD-cost:    1
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> BDD-cost:    1
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    1
c ---[ 227]---> BDD-cost:    1
c ---[ 226]---> BDD-cost:    1
c ---[ 225]---> BDD-cost:    1
c ---[ 224]---> BDD-cost:    1
c ---[ 223]---> BDD-cost:    1
c ---[ 222]---> BDD-cost:    1
c ---[ 221]---> BDD-cost:    1
c ---[ 220]---> BDD-cost:    1
c ---[ 219]---> BDD-cost:    1
c ---[ 218]---> BDD-cost:    1
c ---[ 217]---> BDD-cost:    1
c ---[ 216]---> BDD-cost:    1
c ---[ 215]---> BDD-cost:    1
c ---[ 214]---> BDD-cost:    1
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> BDD-cost:    1
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> BDD-cost:    1
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:    1
c ---[ 206]---> BDD-cost:    1
c ---[ 205]---> BDD-cost:    1
c ---[ 204]---> BDD-cost:    1
c ---[ 203]---> BDD-cost:    1
c ---[ 202]---> BDD-cost:    1
c ---[ 201]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:    1
c ---[ 198]---> BDD-cost:    1
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> BDD-cost:    1
c ---[ 194]---> BDD-cost:    1
c ---[ 193]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 191]---> BDD-cost:    1
c ---[ 190]---> BDD-cost:    1
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:    1
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:    1
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> BDD-cost:    1
c ---[   0]---> Adder-cost: 245   maxlim: 255   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   18533    50267 |    6177       0        0     nan |  0.000 % |
c |       100 |   18533    50267 |    6794     100      890     8.9 | 14.349 % |
c |       252 |   18533    50267 |    7474     252     2814    11.2 | 14.349 % |
c |       478 |   18533    50267 |    8221     478     5356    11.2 | 14.349 % |
c |       815 |   18533    50267 |    9043     815    10568    13.0 | 14.349 % |
c |      1321 |   18533    50267 |    9948    1321    21019    15.9 | 14.349 % |
c |      2080 |   18533    50267 |   10942    2080    33047    15.9 | 14.349 % |
c ==============================================================================
c [1mFound solution: 129[0m
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2896 |   18541    50284 |    6180    2896    46509    16.1 | 14.349 % |
c |      2996 |   18541    50284 |    6798    2996    47641    15.9 | 14.361 % |
c ==============================================================================
c [1mFound solution: 128[0m
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3140 |   18517    50206 |    6172    3140    49548    15.8 | 14.361 % |
c |      3240 |   18517    50206 |    6789    3240    50991    15.7 | 14.446 % |
c |      3390 |   18517    50206 |    7468    3390    53797    15.9 | 14.446 % |
c |      3615 |   18517    50206 |    8214    3615    58020    16.0 | 14.446 % |
c |      3953 |   18517    50206 |    9036    3953    63164    16.0 | 14.446 % |
c |      4459 |   18517    50206 |    9940    4459    70204    15.7 | 14.446 % |
c |      5218 |   18517    50206 |   10934    5218    81000    15.5 | 14.446 % |
c |      6358 |   18494    50155 |   12027    6356   103792    16.3 | 14.548 % |
c |      8066 |   18494    50155 |   13230    8064   135540    16.8 | 14.548 % |
c ==============================================================================
c [1mFound solution: 125[0m
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8441 |   18497    50166 |    6165    8439   141638    16.8 | 14.548 % |
c |      8542 |   18497    50166 |    6781    4321    69554    16.1 | 14.560 % |
c |      8692 |   18497    50166 |    7459    4471    72404    16.2 | 14.560 % |
c |      8917 |   18497    50166 |    8205    4696    76156    16.2 | 14.560 % |
c |      9254 |   18497    50166 |    9026    5033    82784    16.4 | 14.560 % |
c |      9760 |   18497    50166 |    9928    5539    90858    16.4 | 14.560 % |
c |     10519 |   18497    50166 |   10921    6298   103301    16.4 | 14.560 % |
c ==============================================================================
c [1mFound solution: 124[0m
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11318 |   18498    50172 |    6166    7097   119916    16.9 | 14.560 % |
c |     11418 |   18498    50172 |    6782    3649    54698    15.0 | 14.575 % |
c |     11568 |   18498    50172 |    7460    3799    56305    14.8 | 14.575 % |
c |     11793 |   18498    50172 |    8206    4024    60750    15.1 | 14.575 % |
c |     12130 |   18498    50172 |    9027    4361    67204    15.4 | 14.575 % |
c |     12636 |   18498    50172 |    9930    4867    78978    16.2 | 14.575 % |
c |     13396 |   18498    50172 |   10923    5627    93422    16.6 | 14.575 % |
c |     14537 |   18498    50172 |   12015    6768   116999    17.3 | 14.575 % |
c |     16246 |   18498    50172 |   13217    8477   158788    18.7 | 14.575 % |
c |     18808 |   18498    50172 |   14539   11039   221711    20.1 | 14.575 % |
c ==============================================================================
c [1mFound solution: 121[0m
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19858 |   18501    50182 |    6167   12089   245364    20.3 | 14.575 % |
c |     19959 |   18501    50182 |    6783    6146   119000    19.4 | 14.587 % |
c |     20109 |   18501    50182 |    7462    6296   123193    19.6 | 14.587 % |
c |     20334 |   18501    50182 |    8208    6521   128925    19.8 | 14.587 % |
c |     20671 |   18501    50182 |    9029    6858   133031    19.4 | 14.587 % |
c |     21180 |   18501    50182 |    9932    7367   145768    19.8 | 14.587 % |
c |     21940 |   18501    50182 |   10925    8127   161508    19.9 | 14.587 % |
c |     23080 |   18501    50182 |   12017    9267   184427    19.9 | 14.587 % |
c |     24788 |   18501    50182 |   13219   10975   219776    20.0 | 14.587 % |
c |     27350 |   18501    50182 |   14541   13537   272603    20.1 | 14.587 % |
c ==============================================================================
c [1mFound solution: 120[0m
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28855 |   18502    50187 |    6167   15042   305144    20.3 | 14.587 % |
c |     28955 |   18502    50187 |    6783    3861    62264    16.1 | 14.602 % |
c |     29106 |   18502    50187 |    7462    4012    64320    16.0 | 14.601 % |
c |     29331 |   18502    50187 |    8208    4237    69154    16.3 | 14.601 % |
c |     29668 |   18502    50187 |    9029    4574    76548    16.7 | 14.601 % |
c |     30176 |   18502    50187 |    9932    5082    85349    16.8 | 14.601 % |
c |     30935 |   18502    50187 |   10925    5841    95625    16.4 | 14.602 % |
c |     32074 |   18502    50187 |   12017    6980   124319    17.8 | 14.601 % |
c |     33784 |   18502    50187 |   13219    8690   167359    19.3 | 14.602 % |
c |     36346 |   18502    50187 |   14541   11252   230172    20.5 | 14.601 % |
c |     40190 |   18502    50187 |   15995   15096   327602    21.7 | 14.602 % |
c |     45956 |   18502    50187 |   17595   11754   274054    23.3 | 14.601 % |
c |     54605 |   18479    50136 |   19354   10792   241427    22.4 | 14.703 % |
c |     67579 |   18479    50136 |   21290   12998   321982    24.8 | 14.703 % |
c ==============================================================================
c [1mFound solution: 119[0m
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72978 |   18483    50148 |    6161   18397   481891    26.2 | 14.703 % |
c |     73078 |   18483    50148 |    6777    4700    90823    19.3 | 14.713 % |
c |     73229 |   18483    50148 |    7454    4851    92976    19.2 | 14.713 % |
c |     73454 |   18483    50148 |    8200    5076    97788    19.3 | 14.713 % |
c |     73791 |   18483    50148 |    9020    5413   102283    18.9 | 14.713 % |
c |     74300 |   18483    50148 |    9922    5922   110733    18.7 | 14.713 % |
c |     75059 |   18483    50148 |   10914    6681   130035    19.5 | 14.713 % |
c |     76198 |   18483    50148 |   12006    7820   154948    19.8 | 14.713 % |
c |     77907 |   18483    50148 |   13206    9529   195763    20.5 | 14.713 % |
c |     80470 |   18483    50148 |   14527   12092   251406    20.8 | 14.713 % |
c |     84315 |   18483    50148 |   15980   15937   343990    21.6 | 14.713 % |
c |     90083 |   18460    50097 |   17578   13116   287033    21.9 | 14.815 % |
c |     98734 |   18460    50097 |   19335   12154   304038    25.0 | 14.815 % |
c |    111708 |   18436    50044 |   21269   14667   344861    23.5 | 14.917 % |
c |    131169 |   18436    50044 |   23396   22644   555453    24.5 | 14.917 % |
c ==============================================================================
c [1mFound solution: 118[0m
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133487 |   18440    50056 |    6146   24962   612096    24.5 | 14.917 % |
c |    133587 |   18440    50056 |    6760    6341   111186    17.5 | 14.926 % |
c |    133737 |   18440    50056 |    7436    6491   113652    17.5 | 14.926 % |
c |    133962 |   18440    50056 |    8180    6716   118022    17.6 | 14.926 % |
c |    134299 |   18440    50056 |    8998    7053   124497    17.7 | 14.926 % |
c |    134806 |   18440    50056 |    9898    7560   136742    18.1 | 14.926 % |
c |    135565 |   18440    50056 |   10888    8319   154287    18.5 | 14.926 % |
c |    136707 |   18440    50056 |   11976    9461   180914    19.1 | 14.926 % |
c |    138415 |   18440    50056 |   13174   11169   221880    19.9 | 14.926 % |
c |    140979 |   18440    50056 |   14491   13733   282298    20.6 | 14.926 % |
c |    144823 |   18440    50056 |   15941    9483   199015    21.0 | 14.926 % |
c |    150591 |   18440    50056 |   17535   15251   340745    22.3 | 14.926 % |
c |    159242 |   18440    50056 |   19288   14262   333014    23.3 | 14.926 % |
c |    172218 |   18440    50056 |   21217   16566   443477    26.8 | 14.926 % |
c |    191680 |   18440    50056 |   23339   13016   282963    21.7 | 14.926 % |
c |    220874 |   18440    50056 |   25673   17229   411469    23.9 | 14.926 % |
c |    264663 |   18440    50056 |   28240   20216   453614    22.4 | 14.926 % |
c |    330347 |   18440    50056 |   31064   25851   717410    27.8 | 14.926 % |
c |    428873 |   18440    50056 |   34171   25715   628734    24.5 | 14.926 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 24934 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.96 0.97 0.97 2/54 24930
Raw data (stat): 24930 (runsolver) R 24929 4613 4612 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841869932 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.97 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0013 s]
Raw data (loadavg): 0.97 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0015 s]
Raw data (loadavg): 0.97 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0036 s]
Raw data (loadavg): 0.98 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0069 s]
Raw data (loadavg): 0.98 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0076 s]
Raw data (loadavg): 0.98 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0075 s]
Raw data (loadavg): 0.98 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0072 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0076 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24934
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24987
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24987
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24987
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24987
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24987
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24987
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24987
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.036 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24989
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/55 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 0.99 0.97 0.97 1/53 24991
Raw data (stat): 24930 (minisat+_script) S 24929 4613 4612 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841869932 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.7
CPU time (s): 1229.84
CPU user time (s): 1229.54
CPU system time (s): 0.297954
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####