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-par32-1.opb
MD5SUM	64e81a7b23abbb8a6da4e2377ea69dee
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	6352
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	6352
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6352
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	6352
Total number of constraints	13453
Number of constraints which are clauses	13453
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	1
Maximum length of a constraint	3
Trace number 5528

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-14 00:24:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3964 boxname=wulflinc13 idbench=204 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  64e81a7b23abbb8a6da4e2377ea69dee  /oldhome/oroussel/tmp/wulflinc13/normalized-par32-1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc13/normalized-par32-1.opb /oldhome/oroussel/tmp/wulflinc13/normalized-par32-1.opb
IDLAUNCH: 3964
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        905488 kB
Buffers:         34840 kB
Cached:          74452 kB
SwapCached:        392 kB
Active:          54104 kB
Inactive:        58480 kB
HighTotal:      131008 kB
HighFree:        52612 kB
LowTotal:       903652 kB
LowFree:        852876 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11004 kB
Committed_AS:    63512 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:44:09 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3964 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13039 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9756    24272 |    2926       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4836          
c   -- var.elim.:  2000/4836          
c   -- var.elim.:  3000/4836          
c   -- var.elim.:  4000/4836          
c   -- var.elim.:  4836/4836          
c |         0 |    9756    24272 |    3902       0        0     nan |  0.000 % |
c |       100 |    9756    24272 |    4292     100     1117    11.2 | 23.867 % |
c |       250 |    9756    24272 |    4721     250     5055    20.2 | 23.867 % |
c |       475 |    9756    24272 |    5194     475    11613    24.4 | 23.867 % |
c |       813 |    9756  #### 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.91 0.95 0.90 2/54 4110
Raw data (stat): 4110 (runsolver) R 4109 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422028604 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+9.9999 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 1564 0 0 0 994 3 0 0 25 0 1 0 422028604 7946240 1504 4294967295 134512640 134672761 3221224560 3221223744 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1940 1504 603 41 0 1899 0
vsize: 7760
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 1662 0 0 0 1994 3 0 0 25 0 1 0 422028604 8351744 1602 4294967295 134512640 134672761 3221224560 3221223744 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1602 603 41 0 1998 0
vsize: 8156
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 1824 0 0 0 2994 4 0 0 25 0 1 0 422028604 8994816 1764 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2196 1764 603 41 0 2155 0
vsize: 8784
[startup+40.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 1954 0 0 0 3994 4 0 0 25 0 1 0 422028604 9519104 1894 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2324 1894 603 41 0 2283 0
vsize: 9296
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2028 0 0 0 4994 4 0 0 25 0 1 0 422028604 9781248 1968 4294967295 134512640 134672761 3221224560 3221223684 134566133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2388 1968 603 41 0 2347 0
vsize: 9552
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2205 0 0 0 5994 4 0 0 25 0 1 0 422028604 10547200 2145 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2575 2145 603 41 0 2534 0
vsize: 10300
[startup+70.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2346 0 0 0 6994 5 0 0 25 0 1 0 422028604 11083776 2286 4294967295 134512640 134672761 3221224560 3221223744 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2706 2286 603 41 0 2665 0
vsize: 10824
[startup+80.0031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2464 0 0 0 7993 6 0 0 25 0 1 0 422028604 11620352 2404 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2837 2404 603 41 0 2796 0
vsize: 11348
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2488 0 0 0 8993 6 0 0 25 0 1 0 422028604 11722752 2428 4294967295 134512640 134672761 3221224560 3221223600 134612601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2862 2428 603 41 0 2821 0
vsize: 11448
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2590 0 0 0 9992 7 0 0 25 0 1 0 422028604 12115968 2530 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2958 2530 603 41 0 2917 0
vsize: 11832
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2685 0 0 0 10992 8 0 0 25 0 1 0 422028604 12607488 2625 4294967295 134512640 134672761 3221224560 3221223616 134644260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3078 2625 603 41 0 3037 0
vsize: 12312
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2686 0 0 0 11992 8 0 0 25 0 1 0 422028604 12607488 2626 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3078 2626 603 41 0 3037 0
vsize: 12312
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2687 0 0 0 12992 8 0 0 25 0 1 0 422028604 12607488 2627 4294967295 134512640 134672761 3221224560 3221223744 134615554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3078 2627 603 41 0 3037 0
vsize: 12312
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2687 0 0 0 13992 8 0 0 25 0 1 0 422028604 12607488 2627 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3078 2627 603 41 0 3037 0
vsize: 12312
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2687 0 0 0 14993 8 0 0 25 0 1 0 422028604 12607488 2627 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3078 2627 603 41 0 3037 0
vsize: 12312
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2687 0 0 0 15993 8 0 0 25 0 1 0 422028604 12607488 2627 4294967295 134512640 134672761 3221224560 3221223696 134614683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3078 2627 603 41 0 3037 0
vsize: 12312
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2697 0 0 0 16993 8 0 0 25 0 1 0 422028604 12640256 2636 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3086 2636 603 41 0 3045 0
vsize: 12344
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2713 0 0 0 17993 8 0 0 25 0 1 0 422028604 12775424 2652 4294967295 134512640 134672761 3221224560 3221223696 134614670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3119 2652 603 41 0 3078 0
vsize: 12476
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2817 0 0 0 18993 8 0 0 25 0 1 0 422028604 13131776 2756 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3206 2756 603 41 0 3165 0
vsize: 12824
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2836 0 0 0 19993 8 0 0 25 0 1 0 422028604 13209600 2775 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3225 2775 603 41 0 3184 0
vsize: 12900
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2836 0 0 0 20993 8 0 0 25 0 1 0 422028604 13209600 2775 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3225 2775 603 41 0 3184 0
vsize: 12900
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2852 0 0 0 21993 8 0 0 25 0 1 0 422028604 13275136 2790 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3241 2790 603 41 0 3200 0
vsize: 12964
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2852 0 0 0 22994 8 0 0 25 0 1 0 422028604 13275136 2790 4294967295 134512640 134672761 3221224560 3221223760 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3241 2790 603 41 0 3200 0
vsize: 12964
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2852 0 0 0 23994 8 0 0 25 0 1 0 422028604 13275136 2790 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3241 2790 603 41 0 3200 0
vsize: 12964
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2869 0 0 0 24994 8 0 0 25 0 1 0 422028604 13340672 2806 4294967295 134512640 134672761 3221224560 3221223600 134612486 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3257 2806 603 41 0 3216 0
vsize: 13028
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2869 0 0 0 25994 8 0 0 25 0 1 0 422028604 13340672 2806 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3257 2806 603 41 0 3216 0
vsize: 13028
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2870 0 0 0 26994 8 0 0 25 0 1 0 422028604 13340672 2807 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3257 2807 603 41 0 3216 0
vsize: 13028
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2870 0 0 0 27995 8 0 0 25 0 1 0 422028604 13340672 2807 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3257 2807 603 41 0 3216 0
vsize: 13028
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2886 0 0 0 28995 8 0 0 25 0 1 0 422028604 13406208 2822 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3273 2822 603 41 0 3232 0
vsize: 13092
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2936 0 0 0 29995 9 0 0 25 0 1 0 422028604 13668352 2872 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3337 2872 603 41 0 3296 0
vsize: 13348
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2961 0 0 0 30995 9 0 0 25 0 1 0 422028604 13688832 2896 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3342 2896 603 41 0 3301 0
vsize: 13368
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2979 0 0 0 31995 9 0 0 25 0 1 0 422028604 13754368 2913 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3358 2913 603 41 0 3317 0
vsize: 13432
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 2979 0 0 0 32995 9 0 0 25 0 1 0 422028604 13754368 2913 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3358 2913 603 41 0 3317 0
vsize: 13432
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3067 0 0 0 33995 9 0 0 25 0 1 0 422028604 14114816 3001 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3001 603 41 0 3405 0
vsize: 13784
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3067 0 0 0 34995 9 0 0 25 0 1 0 422028604 14114816 3001 4294967295 134512640 134672761 3221224560 3221223684 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3001 603 41 0 3405 0
vsize: 13784
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3076 0 0 0 35995 9 0 0 25 0 1 0 422028604 14147584 3009 4294967295 134512640 134672761 3221224560 3221223696 134614505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3454 3009 603 41 0 3413 0
vsize: 13816
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3076 0 0 0 36996 9 0 0 25 0 1 0 422028604 14147584 3009 4294967295 134512640 134672761 3221224560 3221223744 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3454 3009 603 41 0 3413 0
vsize: 13816
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3076 0 0 0 37996 9 0 0 25 0 1 0 422028604 14147584 3009 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3454 3009 603 41 0 3413 0
vsize: 13816
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3076 0 0 0 38996 9 0 0 25 0 1 0 422028604 14147584 3009 4294967295 134512640 134672761 3221224560 3221223552 134565132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3454 3009 603 41 0 3413 0
vsize: 13816
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3076 0 0 0 39996 9 0 0 25 0 1 0 422028604 14147584 3009 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3454 3009 603 41 0 3413 0
vsize: 13816
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3092 0 0 0 40996 9 0 0 25 0 1 0 422028604 14213120 3024 4294967295 134512640 134672761 3221224560 3221223484 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3470 3024 603 41 0 3429 0
vsize: 13880
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3092 0 0 0 41996 9 0 0 25 0 1 0 422028604 14213120 3024 4294967295 134512640 134672761 3221224560 3221223760 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3470 3024 603 41 0 3429 0
vsize: 13880
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3092 0 0 0 42997 9 0 0 25 0 1 0 422028604 14213120 3024 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3470 3024 603 41 0 3429 0
vsize: 13880
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3205 0 0 0 43997 9 0 0 25 0 1 0 422028604 14753792 3137 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3602 3137 603 41 0 3561 0
vsize: 14408
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3205 0 0 0 44997 9 0 0 25 0 1 0 422028604 14753792 3137 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3602 3137 603 41 0 3561 0
vsize: 14408
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3236 0 0 0 45997 9 0 0 25 0 1 0 422028604 14819328 3168 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3618 3168 603 41 0 3577 0
vsize: 14472
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3236 0 0 0 46997 9 0 0 25 0 1 0 422028604 14819328 3168 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3618 3168 603 41 0 3577 0
vsize: 14472
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3236 0 0 0 47998 9 0 0 25 0 1 0 422028604 14819328 3168 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3618 3168 603 41 0 3577 0
vsize: 14472
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3246 0 0 0 48998 9 0 0 25 0 1 0 422028604 14852096 3177 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3626 3177 603 41 0 3585 0
vsize: 14504
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3247 0 0 0 49998 9 0 0 25 0 1 0 422028604 14852096 3178 4294967295 134512640 134672761 3221224560 3221223552 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3626 3178 603 41 0 3585 0
vsize: 14504
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3247 0 0 0 50998 9 0 0 25 0 1 0 422028604 14852096 3178 4294967295 134512640 134672761 3221224560 3221223712 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3626 3178 603 41 0 3585 0
vsize: 14504
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3257 0 0 0 51998 10 0 0 25 0 1 0 422028604 14884864 3187 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3634 3187 603 41 0 3593 0
vsize: 14536
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3257 0 0 0 52998 10 0 0 25 0 1 0 422028604 14884864 3187 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3634 3187 603 41 0 3593 0
vsize: 14536
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3257 0 0 0 53999 10 0 0 25 0 1 0 422028604 14884864 3187 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3634 3187 603 41 0 3593 0
vsize: 14536
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3257 0 0 0 54999 10 0 0 25 0 1 0 422028604 14884864 3187 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3634 3187 603 41 0 3593 0
vsize: 14536
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3272 0 0 0 55999 10 0 0 25 0 1 0 422028604 14950400 3201 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3650 3201 603 41 0 3609 0
vsize: 14600
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3272 0 0 0 56999 10 0 0 25 0 1 0 422028604 14950400 3201 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3650 3201 603 41 0 3609 0
vsize: 14600
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3272 0 0 0 57999 10 0 0 25 0 1 0 422028604 14950400 3201 4294967295 134512640 134672761 3221224560 3221223724 134614558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3650 3201 603 41 0 3609 0
vsize: 14600
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3272 0 0 0 59000 10 0 0 25 0 1 0 422028604 14950400 3201 4294967295 134512640 134672761 3221224560 3221223552 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3650 3201 603 41 0 3609 0
vsize: 14600
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3289 0 0 0 60000 10 0 0 25 0 1 0 422028604 15011840 3217 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3217 603 41 0 3624 0
vsize: 14660
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3289 0 0 0 61000 10 0 0 25 0 1 0 422028604 15011840 3217 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3217 603 41 0 3624 0
vsize: 14660
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3289 0 0 0 62000 10 0 0 25 0 1 0 422028604 15011840 3217 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3217 603 41 0 3624 0
vsize: 14660
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3289 0 0 0 63000 10 0 0 25 0 1 0 422028604 15011840 3217 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3217 603 41 0 3624 0
vsize: 14660
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3289 0 0 0 64000 10 0 0 25 0 1 0 422028604 15011840 3217 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3217 603 41 0 3624 0
vsize: 14660
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3289 0 0 0 65001 10 0 0 25 0 1 0 422028604 15011840 3217 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3217 603 41 0 3624 0
vsize: 14660
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3289 0 0 0 66001 10 0 0 25 0 1 0 422028604 15011840 3217 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3217 603 41 0 3624 0
vsize: 14660
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3289 0 0 0 67001 10 0 0 25 0 1 0 422028604 15011840 3217 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3217 603 41 0 3624 0
vsize: 14660
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 68001 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 69001 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223696 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 70002 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 71002 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 72002 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223720 134614557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 73002 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 74002 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 75002 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 76003 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223708 134614482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 77003 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+780.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 78003 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 79003 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 80003 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 81004 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 82004 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 83004 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223600 134613025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 84004 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 85004 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 86005 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 87005 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 88005 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223600 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 89005 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3293 0 0 0 90005 10 0 0 25 0 1 0 422028604 15011840 3221 4294967295 134512640 134672761 3221224560 3221223552 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3665 3221 603 41 0 3624 0
vsize: 14660
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3310 0 0 0 91005 10 0 0 25 0 1 0 422028604 15077376 3237 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3237 603 41 0 3640 0
vsize: 14724
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3310 0 0 0 92006 10 0 0 25 0 1 0 422028604 15077376 3237 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3237 603 41 0 3640 0
vsize: 14724
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3310 0 0 0 93006 10 0 0 25 0 1 0 422028604 15077376 3237 4294967295 134512640 134672761 3221224560 3221223616 134644260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3237 603 41 0 3640 0
vsize: 14724
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3310 0 0 0 94006 10 0 0 25 0 1 0 422028604 15077376 3237 4294967295 134512640 134672761 3221224560 3221223696 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3237 603 41 0 3640 0
vsize: 14724
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3310 0 0 0 95006 10 0 0 25 0 1 0 422028604 15077376 3237 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3681 3237 603 41 0 3640 0
vsize: 14724
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3321 0 0 0 96006 10 0 0 25 0 1 0 422028604 15110144 3247 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3689 3247 603 41 0 3648 0
vsize: 14756
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3321 0 0 0 97007 10 0 0 25 0 1 0 422028604 15110144 3247 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3689 3247 603 41 0 3648 0
vsize: 14756
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3321 0 0 0 98007 10 0 0 25 0 1 0 422028604 15110144 3247 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3689 3247 603 41 0 3648 0
vsize: 14756
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3321 0 0 0 99007 10 0 0 25 0 1 0 422028604 15110144 3247 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3689 3247 603 41 0 3648 0
vsize: 14756
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3321 0 0 0 100007 10 0 0 25 0 1 0 422028604 15110144 3247 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3689 3247 603 41 0 3648 0
vsize: 14756
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3344 0 0 0 101007 10 0 0 25 0 1 0 422028604 15208448 3270 4294967295 134512640 134672761 3221224560 3221223760 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3713 3270 603 41 0 3672 0
vsize: 14852
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3344 0 0 0 102007 10 0 0 25 0 1 0 422028604 15208448 3270 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3713 3270 603 41 0 3672 0
vsize: 14852
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3345 0 0 0 103008 10 0 0 25 0 1 0 422028604 15208448 3271 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3713 3271 603 41 0 3672 0
vsize: 14852
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3403 0 0 0 104008 10 0 0 25 0 1 0 422028604 15421440 3329 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3329 603 41 0 3724 0
vsize: 15060
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3403 0 0 0 105008 10 0 0 25 0 1 0 422028604 15421440 3329 4294967295 134512640 134672761 3221224560 3221223728 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3765 3329 603 41 0 3724 0
vsize: 15060
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3413 0 0 0 106008 10 0 0 25 0 1 0 422028604 15552512 3339 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3797 3339 603 41 0 3756 0
vsize: 15188
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3519 0 0 0 107008 11 0 0 25 0 1 0 422028604 15896576 3445 4294967295 134512640 134672761 3221224560 3221223696 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3881 3445 603 41 0 3840 0
vsize: 15524
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3519 0 0 0 108008 11 0 0 25 0 1 0 422028604 15896576 3445 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3881 3445 603 41 0 3840 0
vsize: 15524
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3519 0 0 0 109008 11 0 0 25 0 1 0 422028604 15896576 3445 4294967295 134512640 134672761 3221224560 3221223696 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3881 3445 603 41 0 3840 0
vsize: 15524
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3536 0 0 0 110008 11 0 0 25 0 1 0 422028604 15962112 3461 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3897 3461 603 41 0 3856 0
vsize: 15588
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3536 0 0 0 111009 11 0 0 25 0 1 0 422028604 15962112 3461 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3897 3461 603 41 0 3856 0
vsize: 15588
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3536 0 0 0 112009 11 0 0 25 0 1 0 422028604 15962112 3461 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3897 3461 603 41 0 3856 0
vsize: 15588
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3563 0 0 0 113009 11 0 0 25 0 1 0 422028604 16093184 3488 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3488 603 41 0 3888 0
vsize: 15716
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3563 0 0 0 114009 11 0 0 25 0 1 0 422028604 16093184 3488 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3488 603 41 0 3888 0
vsize: 15716
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3563 0 0 0 115009 11 0 0 25 0 1 0 422028604 16093184 3488 4294967295 134512640 134672761 3221224560 3221223744 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3488 603 41 0 3888 0
vsize: 15716
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3563 0 0 0 116009 11 0 0 25 0 1 0 422028604 16093184 3488 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3488 603 41 0 3888 0
vsize: 15716
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3563 0 0 0 117009 11 0 0 25 0 1 0 422028604 16093184 3488 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3488 603 41 0 3888 0
vsize: 15716
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3563 0 0 0 118010 11 0 0 25 0 1 0 422028604 16093184 3488 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3488 603 41 0 3888 0
vsize: 15716
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3563 0 0 0 119010 11 0 0 25 0 1 0 422028604 16093184 3488 4294967295 134512640 134672761 3221224560 3221223744 134615544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3488 603 41 0 3888 0
vsize: 15716
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4110
Raw data (stat): 4110 (minisat+) R 4109 30701 30700 0 -1 0 3563 0 0 0 120010 11 0 0 25 0 1 0 422028604 16093184 3488 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3488 603 41 0 3888 0
vsize: 15716
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4110
Raw data (stat): 4110 (minisat+) Z 4109 30701 30700 0 -1 12 3563 0 0 0 120010 12 0 0 25 0 1 0 422028604 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.03
CPU time (s): 1200.23
CPU user time (s): 1200.11
CPU system time (s): 0.123981
CPU usage (%): 100.017
Max. virtual memory (Kb): 15716
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####