PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-nsrand-ipx.opb
MD5SUM	6b39a5ca45e18a6e9e3dc91f7594e22c
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483575
Optimality of the best value was proved	NO
Number of terms in the objective function	31
Biggest coefficient in the objective function	1073741824
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	2147483647
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	1073741824
Number of bits of the biggest number in a constraint	31
Biggest sum of numbers in a constraint	26715880447
Number of bits of the biggest sum of numbers	35
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1224.15
Number of variables	6651
Total number of constraints	7355
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	6951
Number of constraints which are nor clauses,nor cardinality constraints	404
Minimum length of a constraint	1
Maximum length of a constraint	6651
Trace number 30771

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        442384 kB
Buffers:         35348 kB
Cached:         531132 kB
SwapCached:        572 kB
Active:          70372 kB
Inactive:       501652 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        442132 kB
SwapTotal:     2097892 kB
SwapFree:      2096728 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5612 kB
Slab:            14468 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 19:43:55 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 22173 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 721 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =====
c   -- Clauses(.)/Splits(s): sssssssss.s.ssss.ssss.ssssss.ssss..ssss..s.ssssssss.s.s.s.s.s.sss.sssss.ss.s.ss.s.ss.sssssssssssss.ssss.ssssssss.s.sssss.sss.ss.s.ss.sssssssssssssssssssssssssssssssssssssssssssss..sssssssssssssssssssss.sssss.sssssssss.ss.ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss..sss.sssssssss.ssss.ssssssssssssss.ssssssssss.s.s.ssssssssssss.ss.ss.ss
c ---[1049]---> Adder-cost: 38230   maxlim: 24568396799   bits: 35/35
c ---[1048]---> BDD-cost:   37
c ---[1047]---> BDD-cost:   37
c ---[1046]---> BDD-cost:   37
c ---[1045]---> BDD-cost:   37
c ---[1044]---> BDD-cost:   37
c ---[1043]---> BDD-cost:   37
c ---[1042]---> BDD-cost:   37
c ---[1041]---> BDD-cost:   37
c ---[1040]---> BDD-cost:   37
c ---[1039]---> BDD-cost:   37
c ---[1038]---> BDD-cost:   37
c ---[1037]---> BDD-cost:   37
c ---[1036]---> BDD-cost:   37
c ---[1035]---> BDD-cost:   37
c ---[1034]---> BDD-cost:   37
c ---[1033]---> BDD-cost:   37
c ---[1032]---> BDD-cost:   37
c ---[1031]---> BDD-cost:   37
c ---[1030]---> BDD-cost:   37
c ---[1029]---> BDD-cost:   37
c ---[1028]---> BDD-cost:   37
c ---[1027]---> BDD-cost:   37
c ---[1026]---> BDD-cost:   37
c ---[1025]---> BDD-cost:   37
c ---[1024]---> BDD-cost:   37
c ---[1023]---> BDD-cost:   37
c ---[1022]---> BDD-cost:   37
c ---[1021]---> BDD-cost:   37
c ---[1020]---> BDD-cost:   37
c ---[1019]---> BDD-cost:   37
c ---[1018]---> BDD-cost:   37
c ---[1017]---> BDD-cost:   37
c ---[1016]---> BDD-cost:   37
c ---[1015]---> BDD-cost:   37
c ---[1014]---> BDD-cost:   37
c ---[1013]---> BDD-cost:   37
c ---[1012]---> BDD-cost:   37
c ---[1011]---> BDD-cost:   37
c ---[1010]---> BDD-cost:   37
c ---[1009]---> BDD-cost:   37
c ---[1008]---> BDD-cost:   37
c ---[1007]---> BDD-cost:   37
c ---[1006]---> BDD-cost:   37
c ---[1005]---> BDD-cost:   37
c ---[1004]---> BDD-cost:   37
c ---[1003]---> BDD-cost:   37
c ---[1002]---> BDD-cost:   37
c ---[1001]---> BDD-cost:   37
c ---[1000]---> BDD-cost:   37
c ---[ 999]---> BDD-cost:   37
c ---[ 998]---> BDD-cost:   37
c ---[ 997]---> BDD-cost:   37
c ---[ 996]---> BDD-cost:   37
c ---[ 995]---> BDD-cost:   37
c ---[ 994]---> BDD-cost:   37
c ---[ 993]---> BDD-cost:   37
c ---[ 992]---> BDD-cost:   37
c ---[ 991]---> BDD-cost:   37
c ---[ 990]---> BDD-cost:   37
c ---[ 989]---> BDD-cost:   37
c ---[ 988]---> BDD-cost:   37
c ---[ 987]---> BDD-cost:   37
c ---[ 986]---> BDD-cost:   37
c ---[ 985]---> BDD-cost:   37
c ---[ 984]---> BDD-cost:   37
c ---[ 983]---> BDD-cost:   37
c ---[ 982]---> BDD-cost:   37
c ---[ 981]---> BDD-cost:   37
c ---[ 980]---> BDD-cost:   37
c ---[ 979]---> BDD-cost:   37
c ---[ 978]---> BDD-cost:   37
c ---[ 977]---> BDD-cost:   37
c ---[ 976]---> BDD-cost:   37
c ---[ 975]---> BDD-cost:   37
c ---[ 974]---> BDD-cost:   37
c ---[ 973]---> BDD-cost:   37
c ---[ 972]---> BDD-cost:   37
c ---[ 971]---> BDD-cost:   37
c ---[ 970]---> BDD-cost:   37
c ---[ 969]---> BDD-cost:   37
c ---[ 968]---> BDD-cost:   37
c ---[ 967]---> BDD-cost:   37
c ---[ 966]---> BDD-cost:   37
c ---[ 965]---> BDD-cost:   37
c ---[ 964]---> BDD-cost:   37
c ---[ 963]---> BDD-cost:   37
c ---[ 962]---> BDD-cost:   37
c ---[ 961]---> BDD-cost:   37
c ---[ 960]---> BDD-cost:   37
c ---[ 959]---> BDD-cost:   37
c ---[ 958]---> BDD-cost:   37
c ---[ 957]---> BDD-cost:   37
c ---[ 956]---> BDD-cost:   37
c ---[ 955]---> BDD-cost:   37
c ---[ 954]---> BDD-cost:   37
c ---[ 953]---> BDD-cost:   37
c ---[ 952]---> BDD-cost:   37
c ---[ 951]---> BDD-cost:   37
c ---[ 950]---> BDD-cost:   37
c ---[ 949]---> BDD-cost:   37
c ---[ 948]---> BDD-cost:   37
c ---[ 947]---> BDD-cost:   37
c ---[ 946]---> BDD-cost:   37
c ---[ 945]---> BDD-cost:   37
c ---[ 944]---> BDD-cost:   37
c ---[ 943]---> BDD-cost:   37
c ---[ 942]---> BDD-cost:   37
c ---[ 941]---> BDD-cost:   37
c ---[ 940]---> BDD-cost:   37
c ---[ 939]---> BDD-cost:   37
c ---[ 938]---> BDD-cost:   37
c ---[ 937]---> BDD-cost:   37
c ---[ 936]---> BDD-cost:   37
c ---[ 935]---> BDD-cost:   37
c ---[ 934]---> BDD-cost:   37
c ---[ 933]---> BDD-cost:   37
c ---[ 932]---> BDD-cost:   37
c ---[ 931]---> BDD-cost:   37
c ---[ 930]---> BDD-cost:   37
c ---[ 929]---> BDD-cost:   37
c ---[ 928]---> BDD-cost:   37
c ---[ 927]---> BDD-cost:   37
c ---[ 926]---> BDD-cost:   37
c ---[ 925]---> BDD-cost:   37
c ---[ 924]---> BDD-cost:   37
c ---[ 923]---> BDD-cost:   37
c ---[ 922]---> BDD-cost:   37
c ---[ 921]---> BDD-cost:   37
c ---[ 920]---> BDD-cost:   37
c ---[ 919]---> BDD-cost:   37
c ---[ 918]---> BDD-cost:   37
c ---[ 917]---> BDD-cost:   37
c ---[ 916]---> BDD-cost:   37
c ---[ 915]---> BDD-cost:   37
c ---[ 914]---> BDD-cost:   37
c ---[ 913]---> BDD-cost:   37
c ---[ 912]---> BDD-cost:   37
c ---[ 911]---> BDD-cost:   37
c ---[ 910]---> BDD-cost:   37
c ---[ 909]---> BDD-cost:   37
c ---[ 908]---> BDD-cost:   37
c ---[ 907]---> BDD-cost:   37
c ---[ 906]---> BDD-cost:   37
c ---[ 905]---> BDD-cost:   37
c ---[ 904]---> BDD-cost:   37
c ---[ 903]---> BDD-cost:   37
c ---[ 902]---> BDD-cost:   37
c ---[ 901]---> BDD-cost:   37
c ---[ 900]---> BDD-cost:   37
c ---[ 899]---> BDD-cost:   37
c ---[ 898]---> BDD-cost:   37
c ---[ 897]---> BDD-cost:   37
c ---[ 896]---> BDD-cost:   37
c ---[ 895]---> BDD-cost:   37
c ---[ 894]---> BDD-cost:   37
c ---[ 893]---> BDD-cost:   37
c ---[ 892]---> BDD-cost:   37
c ---[ 891]---> BDD-cost:   37
c ---[ 890]---> BDD-cost:   37
c ---[ 889]---> BDD-cost:   37
c ---[ 888]---> BDD-cost:   37
c ---[ 887]---> BDD-cost:   37
c ---[ 886]---> BDD-cost:   37
c ---[ 885]---> BDD-cost:   37
c ---[ 884]---> BDD-cost:   37
c ---[ 883]---> BDD-cost:   37
c ---[ 882]---> BDD-cost:   37
c ---[ 881]---> BDD-cost:   37
c ---[ 880]---> BDD-cost:   37
c ---[ 879]---> BDD-cost:   37
c ---[ 878]---> BDD-cost:   37
c ---[ 877]---> BDD-cost:   37
c ---[ 876]---> BDD-cost:   37
c ---[ 875]---> BDD-cost:   37
c ---[ 874]---> BDD-cost:   37
c ---[ 873]---> BDD-cost:   37
c ---[ 872]---> BDD-cost:   37
c ---[ 871]---> BDD-cost:   37
c ---[ 870]---> BDD-cost:   37
c ---[ 869]---> BDD-cost:   37
c ---[ 868]---> BDD-cost:   37
c ---[ 867]---> BDD-cost:   37
c ---[ 866]---> BDD-cost:   37
c ---[ 865]---> BDD-cost:   37
c ---[ 864]---> BDD-cost:   37
c ---[ 863]---> BDD-cost:   37
c ---[ 862]---> BDD-cost:   37
c ---[ 861]---> BDD-cost:   37
c ---[ 860]---> BDD-cost:   37
c ---[ 859]---> BDD-cost:   37
c ---[ 858]---> BDD-cost:   37
c ---[ 857]---> BDD-cost:   37
c ---[ 856]---> BDD-cost:   37
c ---[ 855]---> BDD-cost:   37
c ---[ 854]---> BDD-cost:   37
c ---[ 853]---> BDD-cost:   37
c ---[ 852]---> BDD-cost:   37
c ---[ 851]---> BDD-cost:   37
c ---[ 850]---> BDD-cost:   37
c ---[ 849]---> BDD-cost:   37
c ---[ 848]---> BDD-cost:   37
c ---[ 847]---> BDD-cost:   37
c ---[ 846]---> BDD-cost:   37
c ---[ 845]---> BDD-cost:   37
c ---[ 844]---> BDD-cost:   37
c ---[ 843]---> BDD-cost:   37
c ---[ 842]---> BDD-cost:   37
c ---[ 841]---> BDD-cost:   37
c ---[ 840]---> BDD-cost:   37
c ---[ 839]---> BDD-cost:   37
c ---[ 838]---> BDD-cost:   37
c ---[ 837]---> BDD-cost:   37
c ---[ 836]---> BDD-cost:   37
c ---[ 835]---> BDD-cost:   37
c ---[ 834]---> BDD-cost:   37
c ---[ 833]---> BDD-cost:   37
c ---[ 832]---> BDD-cost:   37
c ---[ 831]---> BDD-cost:   37
c ---[ 830]---> BDD-cost:   37
c ---[ 829]---> BDD-cost:   37
c ---[ 828]---> BDD-cost:   37
c ---[ 827]---> BDD-cost:   37
c ---[ 826]---> BDD-cost:   37
c ---[ 825]---> BDD-cost:   37
c ---[ 824]---> BDD-cost:   37
c ---[ 823]---> BDD-cost:   37
c ---[ 822]---> BDD-cost:   37
c ---[ 821]---> BDD-cost:   37
c ---[ 820]---> BDD-cost:   37
c ---[ 819]---> BDD-cost:   37
c ---[ 818]---> BDD-cost:   37
c ---[ 817]---> BDD-cost:   37
c ---[ 816]---> BDD-cost:   37
c ---[ 815]---> BDD-cost:   37
c ---[ 814]---> BDD-cost:   37
c ---[ 813]---> BDD-cost:   37
c ---[ 812]---> BDD-cost:   37
c ---[ 811]---> BDD-cost:   37
c ---[ 810]---> BDD-cost:   37
c ---[ 809]---> BDD-cost:   37
c ---[ 808]---> BDD-cost:   37
c ---[ 807]---> BDD-cost:   37
c ---[ 806]---> BDD-cost:   37
c ---[ 805]---> BDD-cost:   37
c ---[ 804]---> BDD-cost:   37
c ---[ 803]---> BDD-cost:   37
c ---[ 802]---> BDD-cost:   37
c ---[ 801]---> BDD-cost:   37
c ---[ 800]---> BDD-cost:   37
c ---[ 799]---> BDD-cost:   37
c ---[ 798]---> BDD-cost:   37
c ---[ 797]---> BDD-cost:   37
c ---[ 796]---> BDD-cost:   37
c ---[ 795]---> BDD-cost:   37
c ---[ 794]---> BDD-cost:   37
c ---[ 793]---> BDD-cost:   37
c ---[ 792]---> BDD-cost:   37
c ---[ 791]---> BDD-cost:   37
c ---[ 790]---> BDD-cost:   37
c ---[ 783]---> BDD-cost:   37
c ---[ 772]---> BDD-cost:   37
c ---[ 761]---> BDD-cost:   37
c ---[ 750]---> BDD-cost:   37
c ---[ 739]---> BDD-cost:   37
c ---[ 728]---> BDD-cost:   37
c ---[ 717]---> BDD-cost:   37
c ---[ 716]---> BDD-cost:   37
c ---[ 705]---> BDD-cost:   37
c ---[ 694]---> BDD-cost:   37
c ---[ 683]---> BDD-cost:   37
c ---[ 672]---> BDD-cost:   37
c ---[ 661]---> BDD-cost:   37
c ---[ 650]---> BDD-cost:   37
c ---[ 639]---> BDD-cost:   37
c ---[ 628]---> BDD-cost:   37
c ---[ 617]---> BDD-cost:   37
c ---[ 608]---> BDD-cost:   37
c ---[ 607]---> BDD-cost:   37
c ---[ 600]---> Adder-cost: 2264   maxlim: 44   bits: 7/6
c ---[ 599]---> Adder-cost: 1410   maxlim: 36   bits: 7/6
c ---[ 598]---> Adder-cost: 1190   maxlim: 36   bits: 7/6
c ---[ 597]---> BDD-cost:   37
c ---[ 587]---> BDD-cost:   37
c ---[ 582]---> Adder-cost: 2364   maxlim: 37   bits: 7/6
c ---[ 581]---> Adder-cost: 1680   maxlim: 32   bits: 7/6
c ---[ 576]---> BDD-cost:   37
c ---[ 567]---> BDD-cost:   37
c ---[ 556]---> BDD-cost:   37
c ---[ 546]---> BDD-cost:   37
c ---[ 536]---> BDD-cost:   37
c ---[ 525]---> BDD-cost:   37
c ---[ 514]---> BDD-cost:   37
c ---[ 503]---> BDD-cost:   37
c ---[ 502]---> BDD-cost:   37
c ---[ 492]---> BDD-cost:   37
c ---[ 482]---> BDD-cost:   37
c ---[ 472]---> BDD-cost:   37
c ---[ 462]---> BDD-cost:   37
c ---[ 451]---> BDD-cost:   37
c ---[ 440]---> BDD-cost:   37
c ---[ 429]---> BDD-cost:   37
c ---[ 418]---> BDD-cost:   37
c ---[ 407]---> BDD-cost:   37
c ---[ 396]---> BDD-cost:   37
c ---[ 395]---> BDD-cost:   37
c ---[ 384]---> BDD-cost:   37
c ---[ 373]---> BDD-cost:   37
c ---[ 363]---> BDD-cost:   37
c ---[ 356]---> BDD-cost:   37
c ---[ 355]---> BDD-cost:   37
c ---[ 354]---> BDD-cost:   37
c ---[ 353]---> BDD-cost:   37
c ---[ 352]---> BDD-cost:   37
c ---[ 351]---> BDD-cost:   37
c ---[ 350]---> BDD-cost:   37
c ---[ 349]---> BDD-cost:   37
c ---[ 348]---> BDD-cost:   37
c ---[ 347]---> BDD-cost:   37
c ---[ 346]---> BDD-cost:   37
c ---[ 345]---> BDD-cost:   37
c ---[ 344]---> BDD-cost:   37
c ---[ 343]---> BDD-cost:   37
c ---[ 342]---> BDD-cost:   37
c ---[ 341]---> BDD-cost:   37
c ---[ 340]---> BDD-cost:   37
c ---[ 339]---> BDD-cost:   37
c ---[ 338]---> BDD-cost:   37
c ---[ 337]---> BDD-cost:   37
c ---[ 336]---> BDD-cost:   37
c ---[ 335]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   37
c ---[ 333]---> BDD-cost:   37
c ---[ 332]---> BDD-cost:   37
c ---[ 331]---> BDD-cost:   37
c ---[ 330]---> BDD-cost:   37
c ---[ 329]---> BDD-cost:   37
c ---[ 328]---> BDD-cost:   34
c ---[ 327]---> BDD-cost: 1577
c ---[ 326]---> Adder-cost: 1245   maxlim: 13   bits: 5/4
c ---[ 325]---> BDD-cost: 2212
c ---[ 324]---> Adder-cost: 791   maxlim: 11   bits: 5/4
c ---[ 323]---> BDD-cost:  930
c ---[ 322]---> Adder-cost: 626   maxlim: 14   bits: 5/4
c ---[ 321]---> Adder-cost: 344   maxlim: 10   bits: 5/4
c ---[ 320]---> Adder-cost: 366   maxlim: 13   bits: 5/4
c ---[ 319]---> BDD-cost:   36
c ---[ 318]---> BDD-cost:    1
c ---[ 317]---> Adder-cost: 375   maxlim: 12   bits: 5/4
c ---[ 316]---> BDD-cost:  816
c ---[ 315]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[ 314]---> BDD-cost:    1
c ---[ 313]---> Adder-cost: 259   maxlim: 13   bits: 5/4
c ---[ 312]---> BDD-cost:    1
c ---[ 311]---> Adder-cost: 159   maxlim: 11   bits: 5/4
c ---[ 310]---> BDD-cost:  817
c ---[ 309]---> BDD-cost:   51
c ---[ 308]---> BDD-cost:  253
c ---[ 307]---> Adder-cost: 426   maxlim: 10   bits: 5/4
c ---[ 306]---> BDD-cost:  565
c ---[ 305]---> BDD-cost:  802
c ---[ 304]---> BDD-cost:  164
c ---[ 303]---> BDD-cost:   72
c ---[ 302]---> BDD-cost:   93
c ---[ 301]---> Adder-cost: 772   maxlim: 14   bits: 5/4
c ---[ 300]---> Adder-cost: 287   maxlim: 12   bits: 5/4
c ---[ 299]---> BDD-cost:  157
c ---[ 298]---> BDD-cost:  249
c ---[ 297]---> Adder-cost: 472   maxlim: 15   bits: 5/4
c ---[ 296]---> Adder-cost: 203   maxlim: 12   bits: 5/4
c ---[ 295]---> BDD-cost:    2
c ---[ 294]---> BDD-cost:  906
c ---[ 293]---> BDD-cost:   62
c ---[ 292]---> BDD-cost:  167
c ---[ 291]---> BDD-cost:    4
c ---[ 290]---> BDD-cost:   20
c ---[ 289]---> BDD-cost:    1
c ---[ 288]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:    2
c ---[ 286]---> BDD-cost:    8
c ---[ 285]---> BDD-cost:  147
c ---[ 284]---> BDD-cost:  745
c ---[ 283]---> BDD-cost:    1
c ---[ 282]---> BDD-cost:    1
c ---[ 281]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:   24
c ---[ 279]---> BDD-cost:   54
c ---[ 278]---> Adder-cost: 1107   maxlim: 10   bits: 5/4
c ---[ 277]---> BDD-cost:   32
c ---[ 276]---> BDD-cost:  879
c ---[ 275]---> Adder-cost: 1319   maxlim: 13   bits: 5/4
c ---[ 274]---> BDD-cost: 2088
c ---[ 273]---> Adder-cost: 2950   maxlim: 17   bits: 6/5
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost: 2736
c ---[ 270]---> Adder-cost: 2699   maxlim: 19   bits: 6/5
c ---[ 269]---> BDD-cost:  492
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> Adder-cost: 748   maxlim: 16   bits: 6/5
c ---[ 266]---> BDD-cost:    1
c ---[ 265]---> BDD-cost:   72
c ---[ 264]---> BDD-cost:  100
c ---[ 263]---> Adder-cost: 1013   maxlim: 19   bits: 6/5
c ---[ 262]---> BDD-cost:    1
c ---[ 261]---> BDD-cost:    2
c ---[ 260]---> Adder-cost: 446   maxlim: 18   bits: 6/5
c ---[ 259]---> BDD-cost:  767
c ---[ 258]---> Adder-cost: 912   maxlim: 9   bits: 5/4
c ---[ 257]---> Adder-cost: 1474   maxlim: 21   bits: 6/5
c ---[ 256]---> BDD-cost:  889
c ---[ 255]---> Adder-cost: 1032   maxlim: 17   bits: 6/5
c ---[ 254]---> Adder-cost: 577   maxlim: 9   bits: 5/4
c ---[ 253]---> BDD-cost: 1704
c ---[ 252]---> Adder-cost: 371   maxlim: 19   bits: 6/5
c ---[ 251]---> BDD-cost:  932
c ---[ 250]---> Adder-cost: 1365   maxlim: 24   bits: 6/5
c ---[ 249]---> BDD-cost: 1516
c ---[ 248]---> Adder-cost: 1521   maxlim: 17   bits: 6/5
c ---[ 247]---> BDD-cost:  242
c ---[ 246]---> Adder-cost: 324   maxlim: 24   bits: 6/5
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> Adder-cost: 749   maxlim: 20   bits: 6/5
c ---[ 243]---> BDD-cost:    1
c ---[ 242]---> Adder-cost: 615   maxlim: 17   bits: 6/5
c ---[ 241]---> BDD-cost:   18
c ---[ 240]---> BDD-cost:  497
c ---[ 239]---> Adder-cost: 430   maxlim: 16   bits: 6/5
c ---[ 238]---> BDD-cost:  151
c ---[ 237]---> BDD-cost:  101
c ---[ 236]---> Adder-cost: 941   maxlim: 14   bits: 5/4
c ---[ 235]---> BDD-cost:   46
c ---[ 234]---> Adder-cost: 705   maxlim: 11   bits: 5/4
c ---[ 233]---> BDD-cost:   70
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> Adder-cost: 150   maxlim: 11   bits: 5/4
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    2
c ---[ 227]---> BDD-cost:   79
c ---[ 226]---> Adder-cost: 523   maxlim: 17   bits: 6/5
c ---[ 225]---> Adder-cost: 610   maxlim: 21   bits: 6/5
c ---[ 224]---> BDD-cost:   32
c ---[ 223]---> Adder-cost: 1071   maxlim: 14   bits: 5/4
c ---[ 222]---> BDD-cost:   24
c ---[ 221]---> BDD-cost: 1540
c ---[ 220]---> BDD-cost: 2152
c ---[ 219]---> BDD-cost:  115
c ---[ 218]---> BDD-cost: 1715
c ---[ 217]---> Adder-cost: 1994   maxlim: 23   bits: 6/5
c ---[ 216]---> BDD-cost:  135
c ---[ 215]---> Adder-cost: 902   maxlim: 19   bits: 6/5
c ---[ 214]---> BDD-cost: 1261
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> Adder-cost: 231   maxlim: 23   bits: 6/5
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> Adder-cost: 509   maxlim: 20   bits: 6/5
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:  382
c ---[ 206]---> BDD-cost:  656
c ---[ 205]---> Adder-cost: 1492   maxlim: 16   bits: 6/5
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:  308
c ---[ 202]---> Adder-cost: 508   maxlim: 12   bits: 5/4
c ---[ 201]---> Adder-cost: 967   maxlim: 10   bits: 5/4
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:    1
c ---[ 198]---> Adder-cost: 858   maxlim: 13   bits: 5/4
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> Adder-cost: 300   maxlim: 13   bits: 5/4
c ---[ 194]---> BDD-cost:    1
c ---[ 193]---> BDD-cost:   68
c ---[ 192]---> Adder-cost: 157   maxlim: 12   bits: 5/4
c ---[ 191]---> Adder-cost: 748   maxlim: 28   bits: 6/5
c ---[ 190]---> BDD-cost:  156
c ---[ 189]---> Adder-cost: 568   maxlim: 10   bits: 5/4
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:    1
c ---[ 186]---> Adder-cost: 157   maxlim: 12   bits: 5/4
c ---[ 185]---> BDD-cost:   26
c ---[ 184]---> BDD-cost:   37
c ---[ 183]---> Adder-cost: 257   maxlim: 10   bits: 5/4
c ---[ 182]---> Adder-cost: 257   maxlim: 10   bits: 5/4
c ---[ 181]---> BDD-cost:   32
c ---[ 180]---> Adder-cost: 805   maxlim: 16   bits: 6/5
c ---[ 179]---> Adder-cost: 988   maxlim: 20   bits: 6/5
c ---[ 178]---> BDD-cost:   19
c ---[ 177]---> Adder-cost: 802   maxlim: 17   bits: 6/5
c ---[ 176]---> Adder-cost: 516   maxlim: 16   bits: 6/5
c ---[ 175]---> Adder-cost: 607   maxlim: 20   bits: 6/5
c ---[ 174]---> BDD-cost:   18
c ---[ 173]---> BDD-cost:   19
c ---[ 172]---> Adder-cost: 565   maxlim: 17   bits: 6/5
c ---[ 171]---> BDD-cost:    1
c ---[ 170]---> Adder-cost: 166   maxlim: 17   bits: 6/5
c ---[ 169]---> Adder-cost: 262   maxlim: 22   bits: 6/5
c ---[ 168]---> Adder-cost: 539   maxlim: 20   bits: 6/5
c ---[ 167]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> Adder-cost: 231   maxlim: 23   bits: 6/5
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> Adder-cost: 343   maxlim: 20   bits: 6/5
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> Adder-cost: 1639   maxlim: 15   bits: 5/4
c ---[ 160]---> Adder-cost: 936   maxlim: 13   bits: 5/4
c ---[ 159]---> BDD-cost:   64
c ---[ 158]---> BDD-cost:  250
c ---[ 157]---> Adder-cost: 579   maxlim: 9   bits: 5/4
c ---[ 156]---> BDD-cost:  769
c ---[ 155]---> BDD-cost:   37
c ---[ 154]---> BDD-cost:  977
c ---[ 153]---> BDD-cost:  171
c ---[ 152]---> BDD-cost:   40
c ---[ 151]---> BDD-cost:  250
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> Adder-cost: 206   maxlim: 10   bits: 5/4
c ---[ 148]---> BDD-cost:   32
c ---[ 147]---> BDD-cost:   88
c ---[ 146]---> BDD-cost:  491
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:  375
c ---[ 143]---> BDD-cost:  471
c ---[ 142]---> Adder-cost: 2678   maxlim: 22   bits: 6/5
c ---[ 141]---> Adder-cost: 1141   maxlim: 12   bits: 5/4
c ---[ 140]---> Adder-cost: 1301   maxlim: 12   bits: 5/4
c ---[ 139]---> BDD-cost:  326
c ---[ 138]---> Adder-cost: 752   maxlim: 12   bits: 5/4
c ---[ 137]---> BDD-cost:  394
c ---[ 136]---> Adder-cost: 1099   maxlim: 12   bits: 5/4
c ---[ 135]---> BDD-cost:  232
c ---[ 134]---> BDD-cost: 1615
c ---[ 133]---> Adder-cost: 2350   maxlim: 19   bits: 6/5
c ---[ 132]---> BDD-cost: 2419
c ---[ 131]---> Adder-cost: 1509   maxlim: 17   bits: 6/5
c ---[ 130]---> BDD-cost: 1026
c ---[ 129]---> BDD-cost: 1706
c ---[ 128]---> BDD-cost:  242
c ---[ 127]---> Adder-cost: 1293   maxlim: 14   bits: 5/4
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> Adder-cost: 539   maxlim: 22   bits: 6/5
c ---[ 123]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 122]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> Adder-cost: 603   maxlim: 21   bits: 6/5
c ---[ 114]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[ 113]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[ 108]---> Adder-cost: 544   maxlim: 10   bits: 5/4
c ---[ 107]---> BDD-cost:   65
c ---[ 106]---> BDD-cost:  871
c ---[ 105]---> BDD-cost: 1115
c ---[ 104]---> BDD-cost:   32
c ---[ 103]---> BDD-cost:   25
c ---[ 102]---> Adder-cost: 821   maxlim: 10   bits: 5/4
c ---[ 101]---> BDD-cost:  107
c ---[ 100]---> Adder-cost: 505   maxlim: 9   bits: 5/4
c ---[  99]---> Adder-cost: 1073   maxlim: 20   bits: 6/5
c ---[  98]---> Adder-cost: 280   maxlim: 10   bits: 5/4
c ---[  97]---> Adder-cost: 363   maxlim: 10   bits: 5/4
c ---[  96]---> Adder-cost: 698   maxlim: 19   bits: 6/5
c ---[  95]---> BDD-cost:  795
c ---[  94]---> Adder-cost: 565   maxlim: 14   bits: 5/4
c ---[  93]---> BDD-cost:   65
c ---[  92]---> BDD-cost:  102
c ---[  91]---> Adder-cost: 479   maxlim: 21   bits: 6/5
c ---[  90]---> Adder-cost: 362   maxlim: 12   bits: 5/4
c ---[  89]---> Adder-cost: 384   maxlim: 12   bits: 5/4
c ---[  88]---> BDD-cost:   78
c ---[  87]---> Adder-cost: 303   maxlim: 12   bits: 5/4
c ---[  86]---> BDD-cost:   90
c ---[  85]---> Adder-cost: 355   maxlim: 12   bits: 5/4
c ---[  84]---> BDD-cost:    1
c ---[  83]---> Adder-cost: 861   maxlim: 15   bits: 5/4
c ---[  82]---> BDD-cost:    2
c ---[  81]---> BDD-cost: 1376
c ---[  80]---> Adder-cost: 635   maxlim: 19   bits: 6/5
c ---[  79]---> BDD-cost:    1
c ---[  78]---> BDD-cost:  688
c ---[  77]---> Adder-cost: 325   maxlim: 20   bits: 6/5
c ---[  76]---> BDD-cost:   96
c ---[  75]---> BDD-cost:    1
c ---[  74]---> Adder-cost: 325   maxlim: 20   bits: 6/5
c ---[  73]---> BDD-cost:  161
c ---[  72]---> BDD-cost:  170
c ---[  71]---> Adder-cost: 513   maxlim: 18   bits: 6/5
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> Adder-cost: 215   maxlim: 19   bits: 6/5
c ---[  67]---> BDD-cost:    1
c ---[  66]---> BDD-cost:    1
c ---[  65]---> Adder-cost: 291   maxlim: 18   bits: 6/5
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    1
c ---[  62]---> BDD-cost:    1
c ---[  61]---> Adder-cost: 357   maxlim: 11   bits: 5/4
c ---[  60]---> BDD-cost:   30
c ---[  59]---> BDD-cost:    1
c ---[  58]---> BDD-cost:    1
c ---[  57]---> Adder-cost: 253   maxlim: 13   bits: 5/4
c ---[  56]---> BDD-cost:   72
c ---[  55]---> BDD-cost:   75
c ---[  54]---> BDD-cost:  302
c ---[  53]---> BDD-cost:  303
c ---[  52]---> BDD-cost:    2
c ---[  51]---> BDD-cost:   46
c ---[  50]---> BDD-cost:  532
c ---[  49]---> Adder-cost: 480   maxlim: 10   bits: 5/4
c ---[  48]---> Adder-cost: 807   maxlim: 22   bits: 6/5
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   86
c ---[  45]---> BDD-cost:  971
c ---[  44]---> Adder-cost: 1489   maxlim: 21   bits: 6/5
c ---[  43]---> BDD-cost:  173
c ---[  42]---> Adder-cost: 687   maxlim: 10   bits: 5/4
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:  170
c ---[  39]---> Adder-cost: 793   maxlim: 19   bits: 6/5
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> Adder-cost: 211   maxlim: 19   bits: 6/5
c ---[  35]---> BDD-cost:   78
c ---[  34]---> BDD-cost:   98
c ---[  33]---> Adder-cost: 211   maxlim: 19   bits: 6/5
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:    1
c ---[  30]---> Adder-cost: 687   maxlim: 17   bits: 6/5
c ---[  29]---> BDD-cost:    1
c ---[  28]---> Adder-cost: 542   maxlim: 16   bits: 6/5
c ---[  27]---> BDD-cost:   33
c ---[  26]---> BDD-cost:   92
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:   22
c ---[  23]---> BDD-cost:    1
c ---[  22]---> BDD-cost:    1
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:    1
c ---[  18]---> BDD-cost:    1
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:    1
c ---[  14]---> Adder-cost: 253   maxlim: 13   bits: 5/4
c ---[  13]---> BDD-cost:  182
c ---[  12]---> Adder-cost: 367   maxlim: 12   bits: 5/4
c ---[  11]---> BDD-cost:  135
c ---[  10]---> BDD-cost:   35
c ---[   9]---> BDD-cost:  505
c ---[   8]---> Adder-cost: 743   maxlim: 15   bits: 5/4
c ---[   7]---> BDD-cost:    1
c ---[   6]---> Adder-cost: 206   maxlim: 10   bits: 5/4
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:  794
c ---[   3]---> BDD-cost:    1
c ---[   2]---> BDD-cost:    1
c ---[   1]---> BDD-cost:  132
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  890342  3228172 |  296780       0        0     nan |  0.000 % |
c |       100 |  890342  3228172 |  326458     100      391     3.9 |  0.500 % |
c |       250 |  890342  3228172 |  359103     250     1189     4.8 |  0.500 % |
c |       475 |  890342  3228172 |  395014     475     2169     4.6 |  0.500 % |
c |       812 |  890342  3228172 |  434515     812     4071     5.0 |  0.500 % |
c |      1318 |  890289  3227973 |  477967    1315     7137     5.4 |  0.500 % |
c |      2077 |  890235  3227771 |  525763    2069    13297     6.4 |  0.502 % |
c |      3216 |  890141  3227421 |  578340    3201    22061     6.9 |  0.504 % |
c |      4924 |  890090  3227230 |  636174    4906    37004     7.5 |  0.505 % |
c |      7486 |  890061  3227123 |  699791    7465    60333     8.1 |  0.506 % |
c |     11330 |  890061  3227123 |  769770   11309   103784     9.2 |  0.506 % |
c |     17096 |  889945  3226691 |  846747   17070   153842     9.0 |  0.507 % |
c |     25746 |  889777  3226077 |  931422   25697   227105     8.8 |  0.514 % |
c |     38720 |  889165  3223843 | 1024565   38622   346417     9.0 |  0.534 % |
c |     58182 |  889134  3223728 | 1127021   58081   922227    15.9 |  0.535 % |
c |     87375 |  889087  3223555 | 1239723   87272  1737010    19.9 |  0.536 % |
c |    131164 |  886745  3215029 | 1363696  130863  2238984    17.1 |  0.632 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  4273 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.95 2/54 4269
Raw data (stat): 4269 (runsolver) R 4268 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841366213 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99919 s]
Raw data (loadavg): 0.93 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20 s]
Raw data (loadavg): 0.94 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0005 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0003 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0006 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0008 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110 s]
Raw data (loadavg): 0.98 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.002 s]
Raw data (loadavg): 1.07 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.002 s]
Raw data (loadavg): 1.06 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.002 s]
Raw data (loadavg): 1.05 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.003 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.003 s]
Raw data (loadavg): 1.04 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.003 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.003 s]
Raw data (loadavg): 1.03 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.005 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.005 s]
Raw data (loadavg): 1.02 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.005 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.005 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.006 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.006 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.007 s]
Raw data (loadavg): 1.01 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.006 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.008 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.007 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.015 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.022 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.028 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.031 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.03 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.029 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.133 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.133 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.133 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.133 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.133 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.14 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.13 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.14 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.14 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.14 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.14 s]
Raw data (loadavg): 1.00 0.99 0.96 2/55 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.75 s]
Raw data (loadavg): 1.00 0.99 0.96 1/53 4273
Raw data (stat): 4269 (minisat+_script) S 4268 20001 20000 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841366213 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.75
CPU time (s): 1229.89
CPU user time (s): 1228.78
CPU system time (s): 1.11683
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####