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 5065

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 21:52:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3191 boxname=wulflinc12 idbench=355 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  417d3abd60fd3b9eb4200ff5119a92c4  /oldhome/oroussel/tmp/wulflinc12/normalized-ss97-4.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-ss97-4.opb
IDLAUNCH: 3191
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        919744 kB
Buffers:         34708 kB
Cached:          61156 kB
SwapCached:         16 kB
Active:          59368 kB
Inactive:        39344 kB
HighTotal:      131008 kB
HighFree:        65912 kB
LowTotal:       903652 kB
LowFree:        853832 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10728 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:12:19 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3191 7 1200.24 0
#### 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 |   42588   143418 |   14196       0        0     nan |  0.000 % |
c |       100 |   42588   143418 |   15615     100     1381    13.8 |  4.341 % |
c |       250 |   42583   143405 |   17177     248     1825     7.4 |  4.360 % |
c |       476 |   42562   143336 |   18894     468     2925     6.2 |  4.387 % |
c |       813 |   42546   143282 |   20784     803     5007     6.2 |  4.406 % |
c |      1319 |   42513   143171 |   22862    1301     7660     5.9 |  4.462 % |
c |      2079 |   42487   143083 |   25149    2048    11155     5.4 |  4.508 % |
c |      3220 |   42465   143013 |   27663    3175    21980     6.9 |  4.545 % |
c |      4928 |   42404   142811 |   30430    4729    29647     6.3 |  4.676 % |
c |      7490 |   42302   142471 |   33473    7244    85196    11.8 |  4.852 % |
c |     11334 |   42240   142263 |   36820   11072   126027    11.4 |  4.954 % |
c |     17100 |   42234   142243 |   40502   14819   191852    12.9 |  4.982 % |
c |     25750 |   42234   142243 |   44553   23469   868690    37.0 |  4.982 % |
c |     38724 |   42234   142243 |   49008   36443  2774011    76.1 |  4.982 % |
c |     58186 |   42234   142243 |   53909   16247   841211    51.8 |  4.982 % |
c |     87380 |   42225   142212 |   59300   45438  3613633    79.5 |  4.992 % |
c |    131169 |   42181   142066 |   65230   40602  1529090    37.7 |  5.112 % |
c |    196854 |   42181   142066 |   71753   50993  6418011   125.9 |  5.112 % |
c |    295380 |   42181   142066 |   78928   29223  7186333   245.9 |  5.112 % |
c |    443169 |   42181   142066 |   86821   45867 13533259   295.1 |  5.112 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 28344
Raw data (stat): 28344 (runsolver) R 28343 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421110790 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 1556 0 0 0 995 3 0 0 25 0 1 0 421110790 8265728 1525 4294967295 134512640 134672761 3221224640 3221223764 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2018 1525 603 41 0 1977 0
vsize: 8072
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 2697 0 0 0 1991 6 0 0 25 0 1 0 421110790 12853248 2666 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3138 2666 603 41 0 3097 0
vsize: 12552
[startup+30.0021 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 4121 0 0 0 2986 11 0 0 25 0 1 0 421110790 18911232 4090 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4617 4090 603 41 0 4576 0
vsize: 18468
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 5272 0 0 0 3983 14 0 0 25 0 1 0 421110790 23523328 5241 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5743 5241 603 41 0 5702 0
vsize: 22972
[startup+50.0032 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 5548 0 0 0 4982 15 0 0 25 0 1 0 421110790 24608768 5517 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6008 5517 603 41 0 5967 0
vsize: 24032
[startup+60.0037 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 5548 0 0 0 5982 15 0 0 25 0 1 0 421110790 24608768 5517 4294967295 134512640 134672761 3221224640 3221223808 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6008 5517 603 41 0 5967 0
vsize: 24032
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 5548 0 0 0 6982 15 0 0 25 0 1 0 421110790 24608768 5517 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6008 5517 603 41 0 5967 0
vsize: 24032
[startup+80.0047 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 6257 0 0 0 7980 17 0 0 25 0 1 0 421110790 27574272 6226 4294967295 134512640 134672761 3221224640 3221223824 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6732 6226 603 41 0 6691 0
vsize: 26928
[startup+90.0042 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 6490 0 0 0 8980 18 0 0 25 0 1 0 421110790 28524544 6459 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6964 6459 603 41 0 6923 0
vsize: 27856
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 6490 0 0 0 9980 18 0 0 25 0 1 0 421110790 28524544 6459 4294967295 134512640 134672761 3221224640 3221223744 134555081 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6964 6459 603 41 0 6923 0
vsize: 27856
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 6490 0 0 0 10980 18 0 0 25 0 1 0 421110790 28524544 6459 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6964 6459 603 41 0 6923 0
vsize: 27856
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 6491 0 0 0 11980 18 0 0 25 0 1 0 421110790 28524544 6460 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6964 6460 603 41 0 6923 0
vsize: 27856
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 6962 0 0 0 12978 20 0 0 25 0 1 0 421110790 30674944 6931 4294967295 134512640 134672761 3221224640 3221223764 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7489 6931 603 41 0 7448 0
vsize: 29956
[startup+140.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 6962 0 0 0 13979 20 0 0 25 0 1 0 421110790 30674944 6931 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7489 6931 603 41 0 7448 0
vsize: 29956
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 7158 0 0 0 14978 21 0 0 25 0 1 0 421110790 31481856 7127 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7686 7127 603 41 0 7645 0
vsize: 30744
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 8343 0 0 0 15976 24 0 0 25 0 1 0 421110790 36343808 8312 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8873 8312 603 41 0 8832 0
vsize: 35492
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 9103 0 0 0 16973 27 0 0 25 0 1 0 421110790 39448576 9072 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9631 9072 603 41 0 9590 0
vsize: 38524
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 10290 0 0 0 17968 31 0 0 25 0 1 0 421110790 44302336 10259 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10816 10259 603 41 0 10775 0
vsize: 43264
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11191 0 0 0 18964 34 0 0 25 0 1 0 421110790 47951872 11160 4294967295 134512640 134672761 3221224640 3221223824 134558903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11707 11160 603 41 0 11666 0
vsize: 46828
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11318 0 0 0 19964 34 0 0 25 0 1 0 421110790 48488448 11287 4294967295 134512640 134672761 3221224640 3221223856 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11287 603 41 0 11797 0
vsize: 47352
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11318 0 0 0 20964 34 0 0 25 0 1 0 421110790 48488448 11287 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11287 603 41 0 11797 0
vsize: 47352
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11318 0 0 0 21964 34 0 0 25 0 1 0 421110790 48488448 11287 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11287 603 41 0 11797 0
vsize: 47352
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11318 0 0 0 22965 34 0 0 25 0 1 0 421110790 48488448 11287 4294967295 134512640 134672761 3221224640 3221223824 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11287 603 41 0 11797 0
vsize: 47352
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11318 0 0 0 23965 34 0 0 25 0 1 0 421110790 48488448 11287 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11287 603 41 0 11797 0
vsize: 47352
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11319 0 0 0 24965 34 0 0 25 0 1 0 421110790 48488448 11288 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11288 603 41 0 11797 0
vsize: 47352
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11320 0 0 0 25965 34 0 0 25 0 1 0 421110790 48488448 11289 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11289 603 41 0 11797 0
vsize: 47352
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11320 0 0 0 26965 34 0 0 25 0 1 0 421110790 48488448 11289 4294967295 134512640 134672761 3221224640 3221223744 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11289 603 41 0 11797 0
vsize: 47352
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11320 0 0 0 27966 34 0 0 25 0 1 0 421110790 48488448 11289 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11289 603 41 0 11797 0
vsize: 47352
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11320 0 0 0 28966 34 0 0 25 0 1 0 421110790 48488448 11289 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11289 603 41 0 11797 0
vsize: 47352
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11320 0 0 0 29965 34 0 0 25 0 1 0 421110790 48488448 11289 4294967295 134512640 134672761 3221224640 3221223744 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11289 603 41 0 11797 0
vsize: 47352
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 11326 0 0 0 30966 34 0 0 25 0 1 0 421110790 48488448 11295 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11295 603 41 0 11797 0
vsize: 47352
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 12439 0 0 0 31963 37 0 0 25 0 1 0 421110790 53080064 12408 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12959 12408 603 41 0 12918 0
vsize: 51836
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 13554 0 0 0 32960 40 0 0 25 0 1 0 421110790 57659392 13523 4294967295 134512640 134672761 3221224640 3221223808 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14077 13523 603 41 0 14036 0
vsize: 56308
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 14414 0 0 0 33958 43 0 0 25 0 1 0 421110790 61218816 14383 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14946 14383 603 41 0 14905 0
vsize: 59784
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 15150 0 0 0 34956 45 0 0 25 0 1 0 421110790 64204800 15119 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15675 15119 603 41 0 15634 0
vsize: 62700
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 15815 0 0 0 35954 47 0 0 25 0 1 0 421110790 66887680 15784 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16330 15785 603 41 0 16289 0
vsize: 65320
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 16747 0 0 0 36952 50 0 0 25 0 1 0 421110790 70803456 16716 4294967295 134512640 134672761 3221224640 3221223824 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17286 16717 603 41 0 17245 0
vsize: 69144
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 37951 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223596 1075350544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 38951 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 39951 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 40952 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 41952 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 42952 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 43952 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 44952 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28344
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 45953 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 28379
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 46953 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+480.019 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28397
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17163 0 0 0 47953 50 0 0 25 0 1 0 421110790 72425472 17132 4294967295 134512640 134672761 3221224640 3221223744 134560322 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17132 603 41 0 17641 0
vsize: 70728
[startup+490.02 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28397
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17165 0 0 0 48953 50 0 0 25 0 1 0 421110790 72425472 17134 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17682 17135 603 41 0 17641 0
vsize: 70728
[startup+500.02 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28397
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 17967 0 0 0 49951 52 0 0 25 0 1 0 421110790 75780096 17936 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18501 17936 603 41 0 18460 0
vsize: 74004
[startup+510.021 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28397
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 18642 0 0 0 50949 55 0 0 25 0 1 0 421110790 78479360 18611 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19160 18611 603 41 0 19119 0
vsize: 76640
[startup+520.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28397
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 19152 0 0 0 51947 57 0 0 25 0 1 0 421110790 80629760 19121 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19685 19121 603 41 0 19644 0
vsize: 78740
[startup+530.022 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28397
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 19890 0 0 0 52945 59 0 0 25 0 1 0 421110790 83599360 19859 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20410 19859 603 41 0 20369 0
vsize: 81640
[startup+540.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28397
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 20558 0 0 0 53943 61 0 0 25 0 1 0 421110790 86421504 20527 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21099 20527 603 41 0 21058 0
vsize: 84396
[startup+550.023 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 21219 0 0 0 54942 63 0 0 25 0 1 0 421110790 89116672 21188 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21757 21188 603 41 0 21716 0
vsize: 87028
[startup+560.023 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 21843 0 0 0 55940 64 0 0 25 0 1 0 421110790 91684864 21812 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22384 21812 603 41 0 22343 0
vsize: 89536
[startup+570.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 22459 0 0 0 56939 66 0 0 25 0 1 0 421110790 94109696 22428 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22976 22428 603 41 0 22935 0
vsize: 91904
[startup+580.024 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 23026 0 0 0 57938 68 0 0 25 0 1 0 421110790 96534528 22995 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23568 22995 603 41 0 23527 0
vsize: 94272
[startup+590.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 23620 0 0 0 58936 69 0 0 25 0 1 0 421110790 98975744 23589 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24164 23589 603 41 0 24123 0
vsize: 96656
[startup+600.024 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 24121 0 0 0 59935 71 0 0 25 0 1 0 421110790 100986880 24090 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24655 24090 603 41 0 24614 0
vsize: 98620
[startup+610.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 24668 0 0 0 60933 73 0 0 25 0 1 0 421110790 103284736 24637 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25216 24637 603 41 0 25175 0
vsize: 100864
[startup+620.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 25258 0 0 0 61932 74 0 0 25 0 1 0 421110790 105705472 25227 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25807 25227 603 41 0 25766 0
vsize: 103228
[startup+630.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 25904 0 0 0 62931 76 0 0 25 0 1 0 421110790 108269568 25873 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26433 25873 603 41 0 26392 0
vsize: 105732
[startup+640.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26422 0 0 0 63929 77 0 0 25 0 1 0 421110790 110419968 26391 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26958 26391 603 41 0 26917 0
vsize: 107832
[startup+650.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26723 0 0 0 64929 78 0 0 25 0 1 0 421110790 111620096 26692 4294967295 134512640 134672761 3221224640 3221223776 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26692 603 41 0 27210 0
vsize: 109004
[startup+660.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26723 0 0 0 65929 78 0 0 25 0 1 0 421110790 111620096 26692 4294967295 134512640 134672761 3221224640 3221223776 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26692 603 41 0 27210 0
vsize: 109004
[startup+670.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26723 0 0 0 66929 78 0 0 25 0 1 0 421110790 111620096 26692 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26692 603 41 0 27210 0
vsize: 109004
[startup+680.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26723 0 0 0 67929 78 0 0 25 0 1 0 421110790 111620096 26692 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26692 603 41 0 27210 0
vsize: 109004
[startup+690.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26724 0 0 0 68930 78 0 0 25 0 1 0 421110790 111620096 26693 4294967295 134512640 134672761 3221224640 3221223808 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26693 603 41 0 27210 0
vsize: 109004
[startup+700.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 69930 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+710.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 70930 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+720.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 71930 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+730.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 72931 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223824 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+740.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 73931 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223824 134558918 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+750.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 74931 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+760.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 75931 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+770.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 76930 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+780.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 77930 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+790.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 78931 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+800.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28399
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 79931 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+810.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 80931 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+820.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26725 0 0 0 81931 78 0 0 25 0 1 0 421110790 111620096 26694 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26694 603 41 0 27210 0
vsize: 109004
[startup+830.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26727 0 0 0 82931 78 0 0 25 0 1 0 421110790 111620096 26696 4294967295 134512640 134672761 3221224640 3221223776 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26696 603 41 0 27210 0
vsize: 109004
[startup+840.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26730 0 0 0 83932 78 0 0 25 0 1 0 421110790 111620096 26699 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26699 603 41 0 27210 0
vsize: 109004
[startup+850.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26732 0 0 0 84932 78 0 0 25 0 1 0 421110790 111620096 26701 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26701 603 41 0 27210 0
vsize: 109004
[startup+860.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 85932 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+870.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 86932 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+880.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 87932 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223824 134558836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+890.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 88933 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+900.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 89933 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+910.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 90933 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+920.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 91933 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+930.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 92933 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+940.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 93934 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+950.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 94934 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+960.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 95934 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+970.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 96934 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+980.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 97935 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223744 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+990.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 98935 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 99935 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 100935 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 101935 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223824 134559400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 102935 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 103936 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 104936 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223744 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 105936 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223744 134560180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 106936 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 107936 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 108937 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 109937 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26734 0 0 0 110937 78 0 0 25 0 1 0 421110790 111620096 26703 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26703 603 41 0 27210 0
vsize: 109004
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26735 0 0 0 111937 78 0 0 25 0 1 0 421110790 111620096 26704 4294967295 134512640 134672761 3221224640 3221223744 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26704 603 41 0 27210 0
vsize: 109004
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 26735 0 0 0 112938 78 0 0 25 0 1 0 421110790 111620096 26704 4294967295 134512640 134672761 3221224640 3221223656 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27251 26704 603 41 0 27210 0
vsize: 109004
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 27068 0 0 0 113937 79 0 0 25 0 1 0 421110790 113094656 27037 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27611 27037 603 41 0 27570 0
vsize: 110444
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 27505 0 0 0 114936 80 0 0 25 0 1 0 421110790 114851840 27474 4294967295 134512640 134672761 3221224640 3221223764 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28040 27474 603 41 0 27999 0
vsize: 112160
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 27728 0 0 0 115935 81 0 0 25 0 1 0 421110790 115798016 27697 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28271 27697 603 41 0 28230 0
vsize: 113084
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 27834 0 0 0 116935 81 0 0 25 0 1 0 421110790 116199424 27803 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28369 27803 603 41 0 28328 0
vsize: 113476
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 27834 0 0 0 117935 81 0 0 25 0 1 0 421110790 116199424 27803 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28369 27803 603 41 0 28328 0
vsize: 113476
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 27834 0 0 0 118936 81 0 0 25 0 1 0 421110790 116199424 27803 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28369 27803 603 41 0 28328 0
vsize: 113476
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28401
Raw data (stat): 28344 (minisat+) R 28343 25285 25284 0 -1 0 27834 0 0 0 119936 81 0 0 25 0 1 0 421110790 116199424 27803 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28369 27803 603 41 0 28328 0
vsize: 113476
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28401
Raw data (stat): 28344 (minisat+) Z 28343 25285 25284 0 -1 12 27836 0 0 0 119936 87 0 0 25 0 1 0 421110790 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.24
CPU user time (s): 1199.36
CPU system time (s): 0.871867
CPU usage (%): 100.011
Max. virtual memory (Kb): 113476
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####