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/submitted/manquinho/primes-dimacs-cnf/normalized-ii32c2.opb
MD5SUM	b78d16df5ec546c41fce5f9f07c0fd92
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	207
Optimality of the best value was proved	NO
Number of terms in the objective function	498
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	498
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	498
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03184
Number of variables	498
Total number of constraints	2431
Number of constraints which are clauses	2431
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 4698

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        922500 kB
Buffers:         34160 kB
Cached:          56220 kB
SwapCached:       2644 kB
Active:          48760 kB
Inactive:        47124 kB
HighTotal:      131008 kB
HighFree:        70868 kB
LowTotal:       903652 kB
LowFree:        851632 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10644 kB
Committed_AS:    63464 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:24:00 (client local time) WITH STATUS 10 IN 1200.31 SECONDS
stats: 3536 7 1200.31 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2431 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2431    12171 |     810       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 229[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 984   maxlim: 269   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        17 |    9274    36601 |    3091      17      834    49.1 |  0.000 % |
c |       118 |    9274    36601 |    3400     118     7740    65.6 |  0.270 % |
c |       270 |    9274    36601 |    3740     270    15683    58.1 |  0.270 % |
c |       496 |    9274    36601 |    4114     496    26869    54.2 |  0.270 % |
c |       833 |    9274    36601 |    4525     833    36887    44.3 |  0.270 % |
c |      1343 |    9274    36601 |    4978    1343    56992    42.4 |  0.270 % |
c |      2102 |    9274    36601 |    5475    2102   109134    51.9 |  0.270 % |
c ==============================================================================
c [1mFound solution: 221[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 277   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2149 |    9281    36637 |    3093    2149   110714    51.5 |  0.270 % |
c |      2250 |    9281    36637 |    3402    2250   112950    50.2 |  0.471 % |
c |      2401 |    9281    36637 |    3742    2401   115862    48.3 |  0.471 % |
c |      2627 |    9281    36637 |    4116    2627   125299    47.7 |  0.471 % |
c |      2965 |    9281    36637 |    4528    2965   136903    46.2 |  0.471 % |
c |      3471 |    9281    36637 |    4981    3471   162133    46.7 |  0.471 % |
c |      4230 |    9281    36637 |    5479    4230   182594    43.2 |  0.471 % |
c |      5369 |    9281    36637 |    6027    5369   210273    39.2 |  0.471 % |
c |      7077 |    9281    36637 |    6630    7077   345771    48.9 |  0.471 % |
c |      9639 |    9281    36637 |    7293    6101   404757    66.3 |  0.471 % |
c |     13483 |    9281    36637 |    8022    5749   388691    67.6 |  0.471 % |
c |     19250 |    9281    36637 |    8824    7451   312389    41.9 |  0.471 % |
c ==============================================================================
c [1mFound solution: 220[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 278   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20602 |    9288    36668 |    3096    8803   365742    41.5 |  0.471 % |
c |     20702 |    9288    36668 |    3405    2301    54699    23.8 |  0.537 % |
c |     20852 |    9288    36668 |    3746    2451    57766    23.6 |  0.537 % |
c |     21077 |    9288    36668 |    4120    2676    61799    23.1 |  0.537 % |
c ==============================================================================
c [1mFound solution: 217[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 281   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21101 |    9290    36682 |    3096    2700    62779    23.3 |  0.537 % |
c |     21201 |    9290    36682 |    3405    2800    65574    23.4 |  0.671 % |
c |     21351 |    9290    36682 |    3746    2950    70852    24.0 |  0.671 % |
c ==============================================================================
c [1mFound solution: 215[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 283   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21372 |    9291    36689 |    3097    2971    71555    24.1 |  0.671 % |
c |     21472 |    9291    36689 |    3406    3071    75187    24.5 |  0.737 % |
c |     21622 |    9291    36689 |    3747    3221    79718    24.7 |  0.737 % |
c |     21848 |    9291    36689 |    4122    3447    85259    24.7 |  0.737 % |
c |     22187 |    9291    36689 |    4534    3786   110129    29.1 |  0.737 % |
c |     22693 |    9291    36689 |    4987    4292   118766    27.7 |  0.737 % |
c |     23454 |    9291    36689 |    5486    5053   171687    34.0 |  0.737 % |
c |     24594 |    9291    36689 |    6035    6193   213025    34.4 |  0.737 % |
c |     26302 |    9291    36689 |    6638    4805   222318    46.3 |  0.737 % |
c |     28864 |    9291    36689 |    7302    3900   138034    35.4 |  0.737 % |
c |     32708 |    9291    36689 |    8032    7744   415097    53.6 |  0.737 % |
c |     38476 |    9291    36689 |    8836    4906   301835    61.5 |  0.737 % |
c |     47125 |    9291    36689 |    9719    9011   490543    54.4 |  0.737 % |
c |     60099 |    9291    36689 |   10691    6100   397825    65.2 |  0.737 % |
c |     79560 |    9291    36689 |   11760    8342   754281    90.4 |  0.737 % |
c |    108753 |    9291    36689 |   12936   12201  1171185    96.0 |  0.737 % |
c |    152543 |    9291    36689 |   14230    8261   712059    86.2 |  0.737 % |
c |    218228 |    9291    36689 |   15653   13419  1486263   110.8 |  0.737 % |
c |    316754 |    9291    36689 |   17219   12533  1218195    97.2 |  0.737 % |
c |    464543 |    9291    36689 |   18940   15547  1643872   105.7 |  0.737 % |
c |    686228 |    9291    36689 |   20835   19689  1651989    83.9 |  0.739 % |
#### 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.87 2/54 31582
Raw data (stat): 31582 (runsolver) R 31581 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420463334 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.0001 s]
Raw data (loadavg): 0.87 0.95 0.88 2/54 31582
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 1160 0 0 0 997 2 0 0 25 0 1 0 420463334 6254592 1138 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1527 1138 603 41 0 1486 0
vsize: 6108
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.96 0.88 2/54 31582
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 1205 0 0 0 1996 2 0 0 25 0 1 0 420463334 6516736 1183 4294967295 134512640 134672761 3221224576 3221223760 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1591 1183 603 41 0 1550 0
vsize: 6364
[startup+30.0002 s]
Raw data (loadavg): 0.91 0.96 0.88 2/54 31582
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 1477 0 0 0 2994 4 0 0 25 0 1 0 420463334 7593984 1455 4294967295 134512640 134672761 3221224576 3221223680 134560150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1854 1455 603 41 0 1813 0
vsize: 7416
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.96 0.88 2/54 31582
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 1598 0 0 0 3994 5 0 0 25 0 1 0 420463334 8126464 1576 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1984 1576 603 41 0 1943 0
vsize: 7936
[startup+50.0009 s]
Raw data (loadavg): 0.93 0.96 0.88 2/54 31582
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 1847 0 0 0 4993 6 0 0 25 0 1 0 420463334 9052160 1825 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2210 1825 603 41 0 2169 0
vsize: 8840
[startup+60.0007 s]
Raw data (loadavg): 0.94 0.96 0.88 2/54 31582
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 1890 0 0 0 5992 6 0 0 25 0 1 0 420463334 9187328 1868 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2243 1868 603 41 0 2202 0
vsize: 8972
[startup+70.0012 s]
Raw data (loadavg): 0.95 0.96 0.88 2/54 31582
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2100 0 0 0 6992 7 0 0 25 0 1 0 420463334 10117120 2078 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2470 2078 603 41 0 2429 0
vsize: 9880
[startup+80.0014 s]
Raw data (loadavg): 0.96 0.96 0.88 2/54 31582
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2232 0 0 0 7991 8 0 0 25 0 1 0 420463334 10653696 2210 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2601 2210 603 41 0 2560 0
vsize: 10404
[startup+90.0011 s]
Raw data (loadavg): 0.96 0.96 0.88 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2233 0 0 0 8990 9 0 0 25 0 1 0 420463334 10653696 2211 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2601 2211 603 41 0 2560 0
vsize: 10404
[startup+100.002 s]
Raw data (loadavg): 0.97 0.96 0.88 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2233 0 0 0 9990 9 0 0 25 0 1 0 420463334 10653696 2211 4294967295 134512640 134672761 3221224576 3221223736 134560076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2601 2211 603 41 0 2560 0
vsize: 10404
[startup+110.002 s]
Raw data (loadavg): 0.97 0.96 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2233 0 0 0 10990 9 0 0 25 0 1 0 420463334 10653696 2211 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2601 2211 603 41 0 2560 0
vsize: 10404
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2295 0 0 0 11990 9 0 0 25 0 1 0 420463334 10919936 2273 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2273 603 41 0 2625 0
vsize: 10664
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2296 0 0 0 12990 9 0 0 25 0 1 0 420463334 10919936 2274 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2274 603 41 0 2625 0
vsize: 10664
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2296 0 0 0 13989 10 0 0 25 0 1 0 420463334 10919936 2274 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2666 2274 603 41 0 2625 0
vsize: 10664
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2529 0 0 0 14989 10 0 0 25 0 1 0 420463334 11849728 2507 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2893 2507 603 41 0 2852 0
vsize: 11572
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2813 0 0 0 15988 11 0 0 25 0 1 0 420463334 13049856 2791 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3186 2791 603 41 0 3145 0
vsize: 12744
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2865 0 0 0 16987 12 0 0 25 0 1 0 420463334 13185024 2843 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3219 2843 603 41 0 3178 0
vsize: 12876
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2865 0 0 0 17987 12 0 0 25 0 1 0 420463334 13185024 2843 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3219 2843 603 41 0 3178 0
vsize: 12876
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2881 0 0 0 18987 12 0 0 25 0 1 0 420463334 13320192 2859 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3252 2859 603 41 0 3211 0
vsize: 13008
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 2908 0 0 0 19986 13 0 0 25 0 1 0 420463334 13508608 2886 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3298 2886 603 41 0 3257 0
vsize: 13192
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3118 0 0 0 20986 14 0 0 25 0 1 0 420463334 14307328 3096 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3493 3096 603 41 0 3452 0
vsize: 13972
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3374 0 0 0 21985 15 0 0 25 0 1 0 420463334 15372288 3352 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3753 3352 603 41 0 3712 0
vsize: 15012
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3517 0 0 0 22984 16 0 0 25 0 1 0 420463334 16035840 3495 4294967295 134512640 134672761 3221224576 3221223680 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3495 603 41 0 3874 0
vsize: 15660
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3517 0 0 0 23984 16 0 0 25 0 1 0 420463334 16035840 3495 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3495 603 41 0 3874 0
vsize: 15660
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3544 0 0 0 24983 16 0 0 25 0 1 0 420463334 16035840 3522 4294967295 134512640 134672761 3221224576 3221223576 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3522 603 41 0 3874 0
vsize: 15660
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3544 0 0 0 25983 17 0 0 25 0 1 0 420463334 16035840 3522 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3522 603 41 0 3874 0
vsize: 15660
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3544 0 0 0 26983 17 0 0 25 0 1 0 420463334 16035840 3522 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3522 603 41 0 3874 0
vsize: 15660
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3544 0 0 0 27983 17 0 0 25 0 1 0 420463334 16035840 3522 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3522 603 41 0 3874 0
vsize: 15660
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3544 0 0 0 28983 17 0 0 25 0 1 0 420463334 16035840 3522 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3522 603 41 0 3874 0
vsize: 15660
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3544 0 0 0 29983 18 0 0 25 0 1 0 420463334 16035840 3522 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3522 603 41 0 3874 0
vsize: 15660
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3544 0 0 0 30983 18 0 0 25 0 1 0 420463334 16035840 3522 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3522 603 41 0 3874 0
vsize: 15660
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3545 0 0 0 31983 18 0 0 25 0 1 0 420463334 16035840 3523 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3523 603 41 0 3874 0
vsize: 15660
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 32983 18 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223680 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 33982 18 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 34982 19 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 35982 19 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 36982 19 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 37981 20 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 38981 20 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 39981 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 40981 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 41981 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 42982 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223680 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 43982 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 44982 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223728 134560074 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 45983 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 46983 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 47983 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 48984 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3546 0 0 0 49984 21 0 0 25 0 1 0 420463334 16035840 3524 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3524 603 41 0 3874 0
vsize: 15660
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 50984 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 51984 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 52984 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 53985 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 54985 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 55985 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 56986 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 57986 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 58987 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 59987 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223760 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 60987 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 61988 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 62988 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 63988 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 64989 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 65989 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 66989 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 67990 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 68990 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223760 134558934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 69990 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223680 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 70991 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 71991 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 72991 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 73992 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 74992 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 75992 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 76993 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223680 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3548 0 0 0 77993 21 0 0 25 0 1 0 420463334 16035840 3526 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3526 603 41 0 3874 0
vsize: 15660
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3549 0 0 0 78993 21 0 0 25 0 1 0 420463334 16035840 3527 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3915 3527 603 41 0 3874 0
vsize: 15660
[startup+800.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3549 0 0 0 79993 22 0 0 25 0 1 0 420463334 16035840 3527 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3527 603 41 0 3874 0
vsize: 15660
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 3549 0 0 0 80993 22 0 0 25 0 1 0 420463334 16035840 3527 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3915 3527 603 41 0 3874 0
vsize: 15660
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4046 0 0 0 81992 23 0 0 25 0 1 0 420463334 18161664 4024 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4434 4024 603 41 0 4393 0
vsize: 17736
[startup+830.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4050 0 0 0 82992 23 0 0 25 0 1 0 420463334 18161664 4028 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4434 4028 603 41 0 4393 0
vsize: 17736
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4365 0 0 0 83991 24 0 0 25 0 1 0 420463334 19496960 4343 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4760 4343 603 41 0 4719 0
vsize: 19040
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4365 0 0 0 84992 24 0 0 25 0 1 0 420463334 19496960 4343 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4760 4343 603 41 0 4719 0
vsize: 19040
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4448 0 0 0 85992 25 0 0 25 0 1 0 420463334 19763200 4426 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4825 4426 603 41 0 4784 0
vsize: 19300
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4599 0 0 0 86991 25 0 0 25 0 1 0 420463334 20430848 4577 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4577 603 41 0 4947 0
vsize: 19952
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 87992 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223760 134559373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 88992 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 89992 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 90993 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 91993 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 92993 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 93994 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 94994 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 95995 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 96995 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 97995 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 98996 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4605 0 0 0 99996 25 0 0 25 0 1 0 420463334 20430848 4583 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4583 603 41 0 4947 0
vsize: 19952
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 100996 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 101997 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 102997 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 103997 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223680 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 104998 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 105998 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 106998 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223756 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 107999 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 108999 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4606 0 0 0 109999 25 0 0 25 0 1 0 420463334 20430848 4584 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4584 603 41 0 4947 0
vsize: 19952
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4609 0 0 0 111000 25 0 0 25 0 1 0 420463334 20430848 4587 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4587 603 41 0 4947 0
vsize: 19952
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4609 0 0 0 112000 25 0 0 25 0 1 0 420463334 20430848 4587 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4988 4587 603 41 0 4947 0
vsize: 19952
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4719 0 0 0 113000 26 0 0 25 0 1 0 420463334 20844544 4697 4294967295 134512640 134672761 3221224576 3221223680 134560150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4697 603 41 0 5048 0
vsize: 20356
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4719 0 0 0 114001 26 0 0 25 0 1 0 420463334 20844544 4697 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4697 603 41 0 5048 0
vsize: 20356
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4719 0 0 0 115001 26 0 0 25 0 1 0 420463334 20844544 4697 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4697 603 41 0 5048 0
vsize: 20356
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4721 0 0 0 116001 26 0 0 25 0 1 0 420463334 20979712 4699 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5122 4699 603 41 0 5081 0
vsize: 20488
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4724 0 0 0 117002 26 0 0 25 0 1 0 420463334 20979712 4702 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5122 4702 603 41 0 5081 0
vsize: 20488
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4724 0 0 0 118002 26 0 0 25 0 1 0 420463334 20979712 4702 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5122 4702 603 41 0 5081 0
vsize: 20488
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4724 0 0 0 119002 26 0 0 25 0 1 0 420463334 20979712 4702 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5122 4702 603 41 0 5081 0
vsize: 20488
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31584
Raw data (stat): 31582 (minisat+) R 31581 29653 29652 0 -1 0 4724 0 0 0 120003 26 0 0 25 0 1 0 420463334 20979712 4702 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5122 4702 603 41 0 5081 0
vsize: 20488
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31584
Raw data (stat): 31582 (minisat+) Z 31581 29653 29652 0 -1 12 4727 0 0 0 120003 27 0 0 25 0 1 0 420463334 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: 10
Real time (s): 1200.03
CPU time (s): 1200.31
CPU user time (s): 1200.03
CPU system time (s): 0.274958
CPU usage (%): 100.023
Max. virtual memory (Kb): 20488
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####