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 5276

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        889956 kB
Buffers:         33964 kB
Cached:          76956 kB
SwapCached:         56 kB
Active:          47560 kB
Inactive:        66356 kB
HighTotal:      131008 kB
HighFree:        49952 kB
LowTotal:       903652 kB
LowFree:        840004 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25020 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:32:58 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 3739 7 1200.19 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]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1111]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1109]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1107]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1105]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1103]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1101]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1099]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1097]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1095]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1093]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1091]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1089]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1087]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1085]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1083]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1081]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1079]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1077]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1075]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1073]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1071]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1069]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1067]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1065]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1063]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1061]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1059]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1057]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1055]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1053]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1051]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1049]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1047]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1045]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1043]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1041]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1039]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1037]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1035]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1033]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1031]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1029]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1027]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1025]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1023]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1021]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1019]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1017]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1015]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1013]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1011]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1009]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1007]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1005]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[1003]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1001]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 999]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 997]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 995]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 993]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 991]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 989]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 987]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 985]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 983]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 981]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 979]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 977]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 975]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 973]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 971]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 969]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 967]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 965]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 963]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 961]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 959]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 957]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 955]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 953]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 951]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 949]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 947]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 945]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 943]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 941]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 939]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 937]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 935]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 933]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 931]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 929]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 927]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 925]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 923]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 921]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 919]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 917]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 915]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 913]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 911]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 909]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 907]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 905]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 903]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 901]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 899]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 897]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 895]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 893]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 891]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 889]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 887]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 885]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 883]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 881]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 879]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 877]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 875]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 873]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 871]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 869]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 867]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 865]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 863]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 861]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 859]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 857]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 855]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 853]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 851]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 849]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 847]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 845]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 843]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 841]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 839]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 837]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 835]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 833]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 831]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 829]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 827]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 825]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 823]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 821]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 819]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 817]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 815]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 813]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 811]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 809]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 807]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 805]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 803]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 801]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 799]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 797]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 795]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 793]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 791]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 789]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 787]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 785]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 783]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 781]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 779]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 777]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 775]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 773]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 771]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 769]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 767]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 765]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 763]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 761]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 759]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 757]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 755]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 753]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 751]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 749]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 747]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 745]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 743]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 741]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 739]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 737]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 735]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 733]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 731]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 729]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 727]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 725]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 723]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 721]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 719]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 717]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 715]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 713]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 711]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 709]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 707]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 705]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 703]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 701]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 699]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 697]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 695]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 693]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 691]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 689]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 687]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 685]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 683]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 681]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 679]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 677]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 675]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 673]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 671]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 669]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 667]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 665]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 663]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 661]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 659]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 657]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 655]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 653]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 651]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 649]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 647]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 645]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 643]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 641]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 639]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 637]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 635]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 633]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 631]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 629]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 627]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 625]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 623]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 621]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 619]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 617]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 615]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 613]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 611]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 609]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 607]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 605]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 603]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[ 601]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 599]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 597]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 595]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 593]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 591]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 589]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 587]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 585]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 583]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 581]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 579]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 577]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 575]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 573]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 571]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 569]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 567]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 565]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 563]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 561]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 559]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 557]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 555]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 553]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 551]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 549]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 547]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 545]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 543]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 541]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 539]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 537]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 535]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 533]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 531]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 529]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 527]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 525]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 523]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 521]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 519]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 517]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 515]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 513]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 511]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 509]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 507]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 505]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 503]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 501]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 499]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 497]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 495]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 493]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 491]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 489]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 487]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 485]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 483]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 481]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 479]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 477]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 475]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 473]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 471]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 469]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 467]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 465]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 463]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 461]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 459]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 457]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 455]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 453]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 451]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 449]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 447]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 445]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 443]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 441]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 439]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 437]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 435]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 433]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 431]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 429]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 427]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 425]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 423]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 421]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 419]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 417]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 415]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 413]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 411]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 409]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 407]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 405]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 403]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 401]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 399]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 397]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 395]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 393]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 391]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 389]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 387]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 385]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 383]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 381]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 379]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 377]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 375]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 373]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 371]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 369]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 367]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 365]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 363]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 361]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[   0]---> Adder-cost: 3   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51564   179924 |   17188       0        0     nan |  0.000 % |
c |       100 |   51405   179435 |   18906      82      280     3.4 | 19.826 % |
c |       250 |   51306   179124 |   20797     222      728     3.3 | 19.983 % |
c |       475 |   51207   178823 |   22877     440     1496     3.4 | 20.166 % |
c |       812 |   51058   178366 |   25164     762     2837     3.7 | 20.431 % |
c |      1321 |   50861   177769 |   27681    1253     5534     4.4 | 20.787 % |
c |      2081 |   50772   177496 |   30449    2005    12664     6.3 | 20.944 % |
c |      3220 |   50670   177184 |   33494    3133    23037     7.4 | 21.118 % |
c |      4929 |   50559   176859 |   36844    4829    40534     8.4 | 21.325 % |
c |      7492 |   50395   176370 |   40528    7361    61695     8.4 | 21.640 % |
c |     11336 |   50307   176128 |   44581   11194   100755     9.0 | 21.822 % |
c |     17103 |   50226   175899 |   49039   16946   273938    16.2 | 21.979 % |
c |     25755 |   50194   175811 |   53943   25594   975046    38.1 | 22.046 % |
c |     38729 |   50149   175678 |   59337   38543  1935594    50.2 | 22.137 % |
c |     58190 |   50127   175612 |   65271   55087  4129389    75.0 | 22.186 % |
c |     87382 |   50055   175398 |   71798   28811  2324918    80.7 | 22.319 % |
c |    131171 |   50031   175324 |   78978   72598  9094888   125.3 | 22.360 % |
c |    196855 |   49941   175040 |   86876   70620  8911928   126.2 | 22.501 % |
c |    295384 |   49867   174820 |   95563   19467  3092568   158.9 | 22.642 % |
c |    443174 |   49567   173894 |  105120   85656 17407947   203.2 | 23.172 % |
#### 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.95 0.90 2/55 26892
Raw data (stat): 26892 (runsolver) R 26891 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479814381 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.95 0.90 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 1910 0 0 0 993 5 0 0 25 0 1 0 479814381 9670656 1881 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2361 1881 603 41 0 2320 0
vsize: 9444
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 3364 0 0 0 1988 9 0 0 25 0 1 0 479814381 15732736 3335 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3841 3335 603 41 0 3800 0
vsize: 15364
[startup+30.0024 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 4575 0 0 0 2985 13 0 0 25 0 1 0 479814381 20582400 4546 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5025 4546 603 41 0 4984 0
vsize: 20100
[startup+40.002 s]
Raw data (loadavg): 0.92 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 5513 0 0 0 3982 16 0 0 25 0 1 0 479814381 24477696 5484 4294967295 134512640 134672761 3221224576 3221223760 134559607 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5976 5484 603 41 0 5935 0
vsize: 23904
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 6515 0 0 0 4979 19 0 0 25 0 1 0 479814381 28499968 6486 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6958 6486 603 41 0 6917 0
vsize: 27832
[startup+60.0026 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 7595 0 0 0 5976 21 0 0 25 0 1 0 479814381 33218560 7566 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8110 7566 603 41 0 8069 0
vsize: 32440
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 8054 0 0 0 6975 23 0 0 25 0 1 0 479814381 35098624 8025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8569 8025 603 41 0 8528 0
vsize: 34276
[startup+80.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 8054 0 0 0 7974 23 0 0 25 0 1 0 479814381 35098624 8025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8569 8025 603 41 0 8528 0
vsize: 34276
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 8054 0 0 0 8974 23 0 0 25 0 1 0 479814381 35098624 8025 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8569 8025 603 41 0 8528 0
vsize: 34276
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 8054 0 0 0 9975 23 0 0 25 0 1 0 479814381 35098624 8025 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8569 8025 603 41 0 8528 0
vsize: 34276
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 8759 0 0 0 10973 25 0 0 25 0 1 0 479814381 37945344 8730 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9264 8730 603 41 0 9223 0
vsize: 37056
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 9681 0 0 0 11970 28 0 0 25 0 1 0 479814381 41717760 9652 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10185 9652 603 41 0 10144 0
vsize: 40740
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 10539 0 0 0 12968 30 0 0 25 0 1 0 479814381 45219840 10510 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11040 10510 603 41 0 10999 0
vsize: 44160
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 11310 0 0 0 13966 32 0 0 25 0 1 0 479814381 48328704 11281 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11799 11281 603 41 0 11758 0
vsize: 47196
[startup+150.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12030 0 0 0 14964 34 0 0 25 0 1 0 479814381 51298304 12001 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12524 12001 603 41 0 12483 0
vsize: 50096
[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12767 0 0 0 15963 36 0 0 25 0 1 0 479814381 54272000 12738 4294967295 134512640 134672761 3221224576 3221223760 134558403 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13250 12738 603 41 0 13209 0
vsize: 53000
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 16963 37 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 17963 37 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26892
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 18963 37 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 19963 37 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 20963 37 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 21963 37 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 22964 37 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 23964 37 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 24964 38 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 12973 0 0 0 25963 38 0 0 25 0 1 0 479814381 55214080 12944 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13480 12944 603 41 0 13439 0
vsize: 53920
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13456 0 0 0 26961 39 0 0 25 0 1 0 479814381 57085952 13427 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13937 13427 603 41 0 13896 0
vsize: 55748
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 27961 40 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 28961 40 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 29960 41 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 30960 41 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223668 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 31960 41 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 32960 41 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 33960 42 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+350.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 34959 42 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 35959 43 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 36959 43 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 37959 43 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 38959 43 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 39959 44 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 40959 44 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 41959 44 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 42959 44 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13776 0 0 0 43959 45 0 0 25 0 1 0 479814381 58433536 13747 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13747 603 41 0 14225 0
vsize: 57064
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 13969 0 0 0 44958 45 0 0 25 0 1 0 479814381 59240448 13940 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14463 13940 603 41 0 14422 0
vsize: 57852
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 14380 0 0 0 45957 47 0 0 25 0 1 0 479814381 60862464 14351 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14859 14351 603 41 0 14818 0
vsize: 59436
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 14782 0 0 0 46955 48 0 0 25 0 1 0 479814381 62615552 14753 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15287 14753 603 41 0 15246 0
vsize: 61148
[startup+480.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15143 0 0 0 47954 50 0 0 25 0 1 0 479814381 64102400 15114 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15650 15114 603 41 0 15609 0
vsize: 62600
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26894
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 48953 51 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 49953 51 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+510.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 50953 51 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 51952 52 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 52952 52 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223760 134558764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 53952 52 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 54952 53 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 55952 53 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 56952 53 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 57952 53 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 58951 54 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+600.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 59951 54 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+610.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 60951 54 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+620.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15479 0 0 0 61951 55 0 0 25 0 1 0 479814381 65478656 15450 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15986 15450 603 41 0 15945 0
vsize: 63944
[startup+630.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 15702 0 0 0 62951 55 0 0 25 0 1 0 479814381 66285568 15673 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16183 15673 603 41 0 16142 0
vsize: 64732
[startup+640.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 16207 0 0 0 63949 57 0 0 25 0 1 0 479814381 68456448 16178 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16713 16178 603 41 0 16672 0
vsize: 66852
[startup+650.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 16709 0 0 0 64947 59 0 0 25 0 1 0 479814381 70516736 16680 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17216 16680 603 41 0 17175 0
vsize: 68864
[startup+660.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 17183 0 0 0 65945 61 0 0 25 0 1 0 479814381 72548352 17154 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17712 17154 603 41 0 17671 0
vsize: 70848
[startup+670.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 17652 0 0 0 66944 62 0 0 25 0 1 0 479814381 74440704 17623 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18174 17623 603 41 0 18133 0
vsize: 72696
[startup+680.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 18118 0 0 0 67942 64 0 0 25 0 1 0 479814381 76324864 18089 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18634 18089 603 41 0 18593 0
vsize: 74536
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 18578 0 0 0 68941 66 0 0 25 0 1 0 479814381 78204928 18549 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19093 18549 603 41 0 19052 0
vsize: 76372
[startup+700.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 18967 0 0 0 69940 67 0 0 25 0 1 0 479814381 79851520 18938 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19495 18938 603 41 0 19454 0
vsize: 77980
[startup+710.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 19358 0 0 0 70938 69 0 0 25 0 1 0 479814381 81539072 19329 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19907 19329 603 41 0 19866 0
vsize: 79628
[startup+720.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 19794 0 0 0 71937 70 0 0 25 0 1 0 479814381 83283968 19765 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20333 19765 603 41 0 20292 0
vsize: 81332
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 20201 0 0 0 72935 72 0 0 25 0 1 0 479814381 84893696 20172 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20726 20172 603 41 0 20685 0
vsize: 82904
[startup+740.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 20673 0 0 0 73933 74 0 0 25 0 1 0 479814381 86917120 20644 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21220 20644 603 41 0 21179 0
vsize: 84880
[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 21121 0 0 0 74933 75 0 0 25 0 1 0 479814381 88670208 21092 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21648 21092 603 41 0 21607 0
vsize: 86592
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 21515 0 0 0 75931 76 0 0 25 0 1 0 479814381 90427392 21486 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21486 603 41 0 22036 0
vsize: 88308
[startup+770.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 21952 0 0 0 76931 77 0 0 25 0 1 0 479814381 92172288 21923 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22503 21923 603 41 0 22462 0
vsize: 90012
[startup+780.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22403 0 0 0 77929 78 0 0 25 0 1 0 479814381 94052352 22374 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22962 22374 603 41 0 22921 0
vsize: 91848
[startup+790.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26896
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 78928 80 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223680 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+800.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 79928 80 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+810.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 80927 81 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+820.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 81927 81 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+830.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 82927 81 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+840.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 83927 82 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+850.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 84927 82 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+860.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 85927 82 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22722 0 0 0 86927 82 0 0 25 0 1 0 479814381 95264768 22693 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22693 603 41 0 23217 0
vsize: 93032
[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22723 0 0 0 87926 83 0 0 25 0 1 0 479814381 95264768 22694 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22694 603 41 0 23217 0
vsize: 93032
[startup+890.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22723 0 0 0 88926 83 0 0 25 0 1 0 479814381 95264768 22694 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22694 603 41 0 23217 0
vsize: 93032
[startup+900.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22727 0 0 0 89926 83 0 0 25 0 1 0 479814381 95264768 22698 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22698 603 41 0 23217 0
vsize: 93032
[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22728 0 0 0 90926 84 0 0 25 0 1 0 479814381 95264768 22699 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22699 603 41 0 23217 0
vsize: 93032
[startup+920.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22729 0 0 0 91926 84 0 0 25 0 1 0 479814381 95264768 22700 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22700 603 41 0 23217 0
vsize: 93032
[startup+930.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22730 0 0 0 92925 84 0 0 25 0 1 0 479814381 95264768 22701 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22701 603 41 0 23217 0
vsize: 93032
[startup+940.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22730 0 0 0 93925 84 0 0 25 0 1 0 479814381 95264768 22701 4294967295 134512640 134672761 3221224576 3221223744 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22701 603 41 0 23217 0
vsize: 93032
[startup+950.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 94925 85 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+960.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 95925 85 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+970.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 96925 85 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+980.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 97924 86 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+990.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 98924 86 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 99924 86 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 100924 86 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 101924 87 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 102924 87 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22732 0 0 0 103924 87 0 0 25 0 1 0 479814381 95264768 22703 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22703 603 41 0 23217 0
vsize: 93032
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22738 0 0 0 104923 88 0 0 25 0 1 0 479814381 95264768 22709 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22709 603 41 0 23217 0
vsize: 93032
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22738 0 0 0 105923 88 0 0 25 0 1 0 479814381 95264768 22709 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22709 603 41 0 23217 0
vsize: 93032
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22738 0 0 0 106923 88 0 0 25 0 1 0 479814381 95264768 22709 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22709 603 41 0 23217 0
vsize: 93032
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22738 0 0 0 107923 89 0 0 25 0 1 0 479814381 95264768 22709 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22709 603 41 0 23217 0
vsize: 93032
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26898
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22738 0 0 0 108923 89 0 0 25 0 1 0 479814381 95264768 22709 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22709 603 41 0 23217 0
vsize: 93032
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 22738 0 0 0 109922 90 0 0 25 0 1 0 479814381 95264768 22709 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23258 22709 603 41 0 23217 0
vsize: 93032
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 23279 0 0 0 110920 92 0 0 25 0 1 0 479814381 97558528 23250 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23818 23250 603 41 0 23777 0
vsize: 95272
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 23883 0 0 0 111918 94 0 0 25 0 1 0 479814381 99971072 23854 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24407 23854 603 41 0 24366 0
vsize: 97628
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 24417 0 0 0 112916 96 0 0 25 0 1 0 479814381 102133760 24388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24935 24388 603 41 0 24894 0
vsize: 99740
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 24951 0 0 0 113914 98 0 0 25 0 1 0 479814381 104280064 24922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25459 24922 603 41 0 25418 0
vsize: 101836
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 25336 0 0 0 114913 99 0 0 25 0 1 0 479814381 105897984 25307 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25854 25307 603 41 0 25813 0
vsize: 103416
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 25336 0 0 0 115913 99 0 0 25 0 1 0 479814381 105897984 25307 4294967295 134512640 134672761 3221224576 3221223728 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25854 25307 603 41 0 25813 0
vsize: 103416
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 25336 0 0 0 116913 100 0 0 25 0 1 0 479814381 105897984 25307 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25854 25307 603 41 0 25813 0
vsize: 103416
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 25336 0 0 0 117913 100 0 0 25 0 1 0 479814381 105897984 25307 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25854 25307 603 41 0 25813 0
vsize: 103416
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 25336 0 0 0 118913 100 0 0 25 0 1 0 479814381 105897984 25307 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25854 25307 603 41 0 25813 0
vsize: 103416
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26900
Raw data (stat): 26892 (minisat+) R 26891 22929 22928 0 -1 0 25336 0 0 0 119913 100 0 0 25 0 1 0 479814381 105897984 25307 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25854 25307 603 41 0 25813 0
vsize: 103416
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 26900
Raw data (stat): 26892 (minisat+) Z 26891 22929 22928 0 -1 12 25338 0 0 0 119913 104 0 0 25 0 1 0 479814381 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.11
CPU time (s): 1200.19
CPU user time (s): 1199.14
CPU system time (s): 1.04884
CPU usage (%): 100.006
Max. virtual memory (Kb): 103416
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####