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 6453

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 05:01:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4867 boxname=wulflinc21 idbench=355 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  417d3abd60fd3b9eb4200ff5119a92c4  /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb /oldhome/oroussel/tmp/wulflinc21/normalized-ss97-4.opb
IDLAUNCH: 4867
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        871688 kB
Buffers:         28984 kB
Cached:         114088 kB
SwapCached:          0 kB
Active:          47760 kB
Inactive:        98200 kB
HighTotal:      131008 kB
HighFree:        13692 kB
LowTotal:       903652 kB
LowFree:        857996 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11448 kB
Committed_AS:    63784 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:22:01 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 4867 7 1200.2 10
#### 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]---> Adder-cost: 354   maxlim: 132   bits: 8/8
c ---[1137]---> Adder-cost: 354   maxlim: 132   bits: 8/8
c ---[1136]---> Adder-cost: 354   maxlim: 132   bits: 8/8
c ---[1135]---> Adder-cost: 352   maxlim: 131   bits: 8/8
c ---[1134]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1133]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1132]---> Adder-cost: 382   maxlim: 168   bits: 8/8
c ---[1131]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1130]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1129]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1128]---> Adder-cost: 382   maxlim: 168   bits: 8/8
c ---[1127]---> Adder-cost: 382   maxlim: 167   bits: 8/8
c ---[1126]---> Adder-cost: 48   maxlim: 35   bits: 7/6
c ---[1125]---> Adder-cost: 48   maxlim: 35   bits: 7/6
c ---[1124]---> Adder-cost: 48   maxlim: 35   bits: 7/6
c ---[1123]---> Adder-cost: 32   maxlim: 35   bits: 7/6
c ---[1122]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1121]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1120]---> Adder-cost: 20   maxlim: 18   bits: 6/5
c ---[1119]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1118]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1117]---> Adder-cost: 56   maxlim: 18   bits: 6/5
c ---[1116]---> Adder-cost: 20   maxlim: 18   bits: 6/5
c ---[1115]---> Adder-cost: 56   maxlim: 18   bits: 6/5
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 |   48718   161856 |   16239       0        0     nan |  0.000 % |
c |       100 |   48718   161856 |   17862     100     1381    13.8 |  4.341 % |
c |       250 |   48709   161831 |   19649     248     1831     7.4 |  4.360 % |
c |       475 |   48691   161769 |   21614     471     2742     5.8 |  4.378 % |
c |       813 |   48642   161607 |   23775     794     4405     5.5 |  4.443 % |
c |      1319 |   48633   161576 |   26153    1299     6582     5.1 |  4.453 % |
c |      2078 |   48633   161576 |   28768    2058    16489     8.0 |  4.453 % |
c |      3218 |   48579   161390 |   31645    3178    23486     7.4 |  4.508 % |
c |      4927 |   48564   161339 |   34809    4882    36708     7.5 |  4.527 % |
c |      7490 |   48491   161095 |   38290    7426    75099    10.1 |  4.620 % |
c |     11334 |   48476   161044 |   42119   11262   120187    10.7 |  4.638 % |
c |     17101 |   48436   160909 |   46331   17000   218755    12.9 |  4.713 % |
c |     25750 |   48427   160878 |   50964   25640   817460    31.9 |  4.722 % |
c |     38724 |   48412   160831 |   56061   38612  1355187    35.1 |  4.750 % |
c |     58185 |   48412   160831 |   61667   58073  3565054    61.4 |  4.750 % |
c |     87377 |   48336   160584 |   67834   34722  4183495   120.5 |  4.899 % |
c |    131166 |   48336   160584 |   74617   19653  3448864   175.5 |  4.899 % |
c |    196852 |   48336   160584 |   82079   22251  1950314    87.7 |  4.899 % |
c |    295378 |   48290   160444 |   90287   48634  4755631    97.8 |  5.001 % |
c |    443167 |   48263   160364 |   99316   37523  7271874   193.8 |  5.075 % |
c ==============================================================================
c [1mFound solution: 12273[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 |    529540 |  293328   733483 |   97776   34123  3687890   108.1 |  5.075 % |
c |    529640 |  293289   733396 |  107553   34222  3688993   107.8 |  0.607 % |
c |    529790 |  293224   733244 |  118308   34371  3689968   107.4 |  0.623 % |
c |    530015 |  291583   729503 |  130139   34573  3690861   106.8 |  1.121 % |
c |    530352 |  289249   724144 |  143153   34875  3692935   105.9 |  1.878 % |
c |    530858 |  280633   704251 |  157469   35162  3693998   105.1 |  4.871 % |
c |    531618 |  264279   666489 |  173216   35628  3696403   103.7 | 10.359 % |
c |    532757 |  241096   612930 |  190537   36262  3699604   102.0 | 18.330 % |
c |    534465 |  213718   549619 |  209591   37267  3706047    99.4 | 27.815 % |
c |    537027 |  188364   490405 |  230550   38860  3714575    95.6 | 36.909 % |
c |    540871 |  183552   479153 |  253605   42122  3757782    89.2 | 38.700 % |
c |    546638 |  176849   463590 |  278966   47495  3826220    80.6 | 41.050 % |
c |    555288 |  160864   426398 |  306862   55221  3920284    71.0 | 46.747 % |
c |    568262 |  149643   400295 |  337549   67329  4043882    60.1 | 50.740 % |
c 
c *** TERMINATED ***
s SATISFIABLE
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 -v#### 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.92 0.98 0.92 2/55 5577
Raw data (stat): 5577 (runsolver) R 5576 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 359177001 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 1579 0 0 0 994 4 0 0 25 0 1 0 359177001 8216576 1548 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2006 1548 603 41 0 1965 0
vsize: 8024
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 2704 0 0 0 1991 8 0 0 25 0 1 0 359177001 12845056 2673 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3136 2673 603 41 0 3095 0
vsize: 12544
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 4035 0 0 0 2988 11 0 0 25 0 1 0 359177001 18374656 4004 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4486 4004 603 41 0 4445 0
vsize: 17944
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 5197 0 0 0 3985 14 0 0 25 0 1 0 359177001 23101440 5166 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5640 5166 603 41 0 5599 0
vsize: 22560
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 6564 0 0 0 4982 17 0 0 25 0 1 0 359177001 28762112 6533 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7022 6533 603 41 0 6981 0
vsize: 28088
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 7538 0 0 0 5979 20 0 0 25 0 1 0 359177001 32923648 7507 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 7507 603 41 0 7997 0
vsize: 32152
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 7538 0 0 0 6979 20 0 0 25 0 1 0 359177001 32923648 7507 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 7507 603 41 0 7997 0
vsize: 32152
[startup+80.0023 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 7539 0 0 0 7979 20 0 0 25 0 1 0 359177001 32923648 7508 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 7508 603 41 0 7997 0
vsize: 32152
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 7539 0 0 0 8979 21 0 0 25 0 1 0 359177001 32923648 7508 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 7508 603 41 0 7997 0
vsize: 32152
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 8064 0 0 0 9978 22 0 0 25 0 1 0 359177001 35078144 8033 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8564 8033 603 41 0 8523 0
vsize: 34256
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 9046 0 0 0 10975 25 0 0 25 0 1 0 359177001 39104512 9015 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9547 9015 603 41 0 9506 0
vsize: 38188
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 9886 0 0 0 11973 27 0 0 25 0 1 0 359177001 42606592 9855 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10402 9855 603 41 0 10361 0
vsize: 41608
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 10782 0 0 0 12971 29 0 0 25 0 1 0 359177001 46243840 10751 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11290 10751 603 41 0 11249 0
vsize: 45160
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 11654 0 0 0 13969 31 0 0 25 0 1 0 359177001 49876992 11623 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12177 11623 603 41 0 12136 0
vsize: 48708
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 12424 0 0 0 14967 33 0 0 25 0 1 0 359177001 52977664 12393 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12934 12393 603 41 0 12893 0
vsize: 51736
[startup+160.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13105 0 0 0 15965 36 0 0 25 0 1 0 359177001 55808000 13074 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13625 13074 603 41 0 13584 0
vsize: 54500
[startup+170.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13738 0 0 0 16963 38 0 0 25 0 1 0 359177001 58355712 13707 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14247 13707 603 41 0 14206 0
vsize: 56988
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13832 0 0 0 17962 39 0 0 25 0 1 0 359177001 58769408 13801 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13801 603 41 0 14307 0
vsize: 57392
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13832 0 0 0 18962 39 0 0 25 0 1 0 359177001 58769408 13801 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13801 603 41 0 14307 0
vsize: 57392
[startup+200.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5577
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13832 0 0 0 19962 39 0 0 25 0 1 0 359177001 58769408 13801 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13801 603 41 0 14307 0
vsize: 57392
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13832 0 0 0 20962 39 0 0 25 0 1 0 359177001 58769408 13801 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13801 603 41 0 14307 0
vsize: 57392
[startup+220.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13832 0 0 0 21962 39 0 0 25 0 1 0 359177001 58769408 13801 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13801 603 41 0 14307 0
vsize: 57392
[startup+230.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13836 0 0 0 22962 39 0 0 25 0 1 0 359177001 58769408 13805 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13805 603 41 0 14307 0
vsize: 57392
[startup+240.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13838 0 0 0 23962 39 0 0 25 0 1 0 359177001 58769408 13807 4294967295 134512640 134672761 3221224576 3221223744 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13807 603 41 0 14307 0
vsize: 57392
[startup+250.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13838 0 0 0 24962 39 0 0 25 0 1 0 359177001 58769408 13807 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13807 603 41 0 14307 0
vsize: 57392
[startup+260.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13838 0 0 0 25963 39 0 0 25 0 1 0 359177001 58769408 13807 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13807 603 41 0 14307 0
vsize: 57392
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13838 0 0 0 26963 39 0 0 25 0 1 0 359177001 58769408 13807 4294967295 134512640 134672761 3221224576 3221223680 134560070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13807 603 41 0 14307 0
vsize: 57392
[startup+280.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13838 0 0 0 27963 39 0 0 25 0 1 0 359177001 58769408 13807 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13807 603 41 0 14307 0
vsize: 57392
[startup+290.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13842 0 0 0 28963 39 0 0 25 0 1 0 359177001 58769408 13811 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13811 603 41 0 14307 0
vsize: 57392
[startup+300.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13845 0 0 0 29963 39 0 0 25 0 1 0 359177001 58769408 13814 4294967295 134512640 134672761 3221224576 3221223728 134565089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13814 603 41 0 14307 0
vsize: 57392
[startup+310.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13845 0 0 0 30963 39 0 0 25 0 1 0 359177001 58769408 13814 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13814 603 41 0 14307 0
vsize: 57392
[startup+320.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13845 0 0 0 31964 39 0 0 25 0 1 0 359177001 58769408 13814 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13814 603 41 0 14307 0
vsize: 57392
[startup+330.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13845 0 0 0 32964 39 0 0 25 0 1 0 359177001 58769408 13814 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13814 603 41 0 14307 0
vsize: 57392
[startup+340.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13845 0 0 0 33964 39 0 0 25 0 1 0 359177001 58769408 13814 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13814 603 41 0 14307 0
vsize: 57392
[startup+350.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13845 0 0 0 34964 39 0 0 25 0 1 0 359177001 58769408 13814 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14348 13814 603 41 0 14307 0
vsize: 57392
[startup+360.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13846 0 0 0 35964 39 0 0 25 0 1 0 359177001 58769408 13815 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13815 603 41 0 14307 0
vsize: 57392
[startup+370.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13846 0 0 0 36964 40 0 0 25 0 1 0 359177001 58769408 13815 4294967295 134512640 134672761 3221224576 3221223680 134555133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13815 603 41 0 14307 0
vsize: 57392
[startup+380.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13846 0 0 0 37964 40 0 0 25 0 1 0 359177001 58769408 13815 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13815 603 41 0 14307 0
vsize: 57392
[startup+390.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13846 0 0 0 38964 40 0 0 25 0 1 0 359177001 58769408 13815 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13815 603 41 0 14307 0
vsize: 57392
[startup+400.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 13846 0 0 0 39964 40 0 0 25 0 1 0 359177001 58769408 13815 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13815 603 41 0 14307 0
vsize: 57392
[startup+410.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 14185 0 0 0 40964 40 0 0 25 0 1 0 359177001 60116992 14154 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14677 14154 603 41 0 14636 0
vsize: 58708
[startup+420.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 14966 0 0 0 41962 42 0 0 25 0 1 0 359177001 63365120 14935 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15470 14935 603 41 0 15429 0
vsize: 61880
[startup+430.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 15838 0 0 0 42960 44 0 0 25 0 1 0 359177001 66998272 15807 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16357 15807 603 41 0 16316 0
vsize: 65428
[startup+440.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 16597 0 0 0 43958 46 0 0 25 0 1 0 359177001 70111232 16566 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17117 16566 603 41 0 17076 0
vsize: 68468
[startup+450.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 17438 0 0 0 44956 48 0 0 25 0 1 0 359177001 73469952 17407 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17937 17407 603 41 0 17896 0
vsize: 71748
[startup+460.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18193 0 0 0 45955 50 0 0 25 0 1 0 359177001 76562432 18162 4294967295 134512640 134672761 3221224576 3221223664 134565829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18162 603 41 0 18651 0
vsize: 74768
[startup+470.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18193 0 0 0 46955 50 0 0 25 0 1 0 359177001 76562432 18162 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18162 603 41 0 18651 0
vsize: 74768
[startup+480.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18194 0 0 0 47955 50 0 0 25 0 1 0 359177001 76562432 18163 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18163 603 41 0 18651 0
vsize: 74768
[startup+490.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18194 0 0 0 48955 51 0 0 25 0 1 0 359177001 76562432 18163 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18163 603 41 0 18651 0
vsize: 74768
[startup+500.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 49955 51 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+510.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 50955 51 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+520.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 51955 51 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+530.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 52955 51 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+540.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 53955 51 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+550.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 54955 51 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+560.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 55955 51 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+570.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 56955 52 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+580.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 57955 52 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+590.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 58955 52 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+600.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 59955 52 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+610.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 60955 52 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+620.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 61954 53 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+630.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 62954 53 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223760 134559274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+640.008 s]
Raw data (loadavg): 0.99 0.98 0.92 3/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 63954 53 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+650.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 64954 53 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+660.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 65955 53 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+670.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 66954 53 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+680.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 67955 53 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+690.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 68954 53 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+700.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 69954 54 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+710.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 70954 54 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+720.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 71954 54 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+730.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 18195 0 0 0 72954 54 0 0 25 0 1 0 359177001 76562432 18164 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18692 18164 603 41 0 18651 0
vsize: 74768
[startup+740.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 19044 0 0 0 73953 55 0 0 25 0 1 0 359177001 80072704 19013 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19549 19013 603 41 0 19508 0
vsize: 78196
[startup+750.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 20189 0 0 0 74949 59 0 0 25 0 1 0 359177001 84791296 20158 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20701 20158 603 41 0 20660 0
vsize: 82804
[startup+760.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 21121 0 0 0 75947 61 0 0 25 0 1 0 359177001 88567808 21090 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21623 21090 603 41 0 21582 0
vsize: 86492
[startup+770.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 21475 0 0 0 76946 62 0 0 25 0 1 0 359177001 89919488 21444 4294967295 134512640 134672761 3221224576 3221223576 1075350205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21953 21444 603 41 0 21912 0
vsize: 87812
[startup+780.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 21475 0 0 0 77946 62 0 0 25 0 1 0 359177001 89919488 21444 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21953 21444 603 41 0 21912 0
vsize: 87812
[startup+790.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24090 0 0 0 78940 68 0 0 25 0 1 0 359177001 102887424 23691 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23691 603 41 0 25078 0
vsize: 100476
[startup+800.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24093 0 0 0 79940 69 0 0 25 0 1 0 359177001 102887424 23694 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23694 603 41 0 25078 0
vsize: 100476
[startup+810.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24093 0 0 0 80940 69 0 0 25 0 1 0 359177001 102887424 23694 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23694 603 41 0 25078 0
vsize: 100476
[startup+820.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24093 0 0 0 81940 69 0 0 25 0 1 0 359177001 102887424 23694 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23694 603 41 0 25078 0
vsize: 100476
[startup+830.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24093 0 0 0 82940 69 0 0 25 0 1 0 359177001 102887424 23694 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23694 603 41 0 25078 0
vsize: 100476
[startup+840.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24101 0 0 0 83941 69 0 0 25 0 1 0 359177001 102887424 23702 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23702 603 41 0 25078 0
vsize: 100476
[startup+850.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24106 0 0 0 84941 69 0 0 25 0 1 0 359177001 102887424 23707 4294967295 134512640 134672761 3221224576 3221223776 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23707 603 41 0 25078 0
vsize: 100476
[startup+860.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24106 0 0 0 85940 69 0 0 25 0 1 0 359177001 102887424 23707 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23707 603 41 0 25078 0
vsize: 100476
[startup+870.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24106 0 0 0 86940 70 0 0 25 0 1 0 359177001 102887424 23707 4294967295 134512640 134672761 3221224576 3221223748 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23707 603 41 0 25078 0
vsize: 100476
[startup+880.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24106 0 0 0 87940 70 0 0 25 0 1 0 359177001 102887424 23707 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23707 603 41 0 25078 0
vsize: 100476
[startup+890.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 88940 70 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+900.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 89940 70 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+910.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 90940 70 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+920.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 91940 71 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+930.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 92940 71 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+940.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 93940 71 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223700 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+950.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 94940 71 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+960.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 95940 71 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+970.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 96940 71 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+980.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 97940 72 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+990.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 98940 72 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 99940 72 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 100940 72 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 101940 72 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 102940 72 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 103940 72 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 104940 72 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 105940 73 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 106940 73 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223760 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 107940 73 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24123 0 0 0 108940 73 0 0 25 0 1 0 359177001 102887424 23724 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23724 603 41 0 25078 0
vsize: 100476
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 109940 73 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 110940 73 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 111940 73 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 112940 73 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 113940 73 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 114940 74 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 115940 74 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 116939 74 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 117939 74 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24137 0 0 0 118940 74 0 0 25 0 1 0 359177001 102887424 23738 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23738 603 41 0 25078 0
vsize: 100476
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/55 5579
Raw data (stat): 5577 (minisat+) R 5576 30927 30926 0 -1 0 24140 0 0 0 119939 75 0 0 25 0 1 0 359177001 102887424 23741 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25119 23741 603 41 0 25078 0
vsize: 100476
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.92 1/55 5579
Raw data (stat): 5577 (minisat+) Z 5576 30927 30926 0 -1 12 24143 0 0 0 119940 79 0 0 25 0 1 0 359177001 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.2
CPU user time (s): 1199.4
CPU system time (s): 0.793879
CPU usage (%): 100.011
Max. virtual memory (Kb): 100476
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####