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-ii8b1.opb
MD5SUM	812314147c77e28d5e428080c7a2412d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	672
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	672
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	672
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03684
Number of variables	672
Total number of constraints	2404
Number of constraints which are clauses	2404
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	8
Trace number 5504

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        915244 kB
Buffers:         35060 kB
Cached:          65156 kB
SwapCached:         16 kB
Active:          60808 kB
Inactive:        42308 kB
HighTotal:      131008 kB
HighFree:        61908 kB
LowTotal:       903652 kB
LowFree:        853336 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10740 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:34:44 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 3927 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2404 PB-constraints to clauses...
c   -- Unit propagations: (none)
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 |    2398     5280 |     719       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  660/660          
c |         0 |    2398     5280 |     959       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.067989 s)
c ==============================================================================
c [1mFound solution: 230[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30564     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         2 |   39367    91648 |   11810       2       14     7.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24702          
c   -- var.elim.:  2000/24702          
c   -- var.elim.:  3000/24702          
c   -- var.elim.:  4000/24702          
c   -- var.elim.:  5000/24702          
c   -- var.elim.:  6000/24702          
c   -- var.elim.:  7000/24702          
c   -- var.elim.:  8000/24702          
c   -- var.elim.:  9000/24702          
c   -- var.elim.:  10000/24702          
c   -- var.elim.:  11000/24702          
c   -- var.elim.:  12000/24702          
c   -- var.elim.:  13000/24702          
c   -- var.elim.:  14000/24702          
c   -- var.elim.:  15000/24702          
c   -- var.elim.:  16000/24702          
c   -- var.elim.:  17000/24702          
c   -- var.elim.:  18000/24702          
c   -- var.elim.:  19000/24702          
c   -- var.elim.:  20000/24702          
c   -- var.elim.:  21000/24702          
c   -- var.elim.:  22000/24702          
c   -- var.elim.:  23000/24702          
c   -- var.elim.:  24000/24702          
c   -- var.elim.:  24702/24702          
c   -- var.elim.:  1000/12105          
c   -- var.elim.:  2000/12105          
c   -- var.elim.:  3000/12105          
c   -- var.elim.:  4000/12105          
c   -- var.elim.:  5000/12105          
c   -- var.elim.:  6000/12105          
c   -- var.elim.:  7000/12105          
c   -- var.elim.:  8000/12105          
c   -- var.elim.:  9000/12105          
c   -- var.elim.:  10000/12105          
c   -- var.elim.:  11000/12105          
c   -- var.elim.:  12000/12105          
c   -- var.elim.:  12105/12105          
c   -- var.elim.:  1000/7425          
c   -- var.elim.:  2000/7425          
c   -- var.elim.:  3000/7425          
c   -- var.elim.:  4000/7425          
c   -- var.elim.:  5000/7425          
c   -- var.elim.:  6000/7425          
c   -- var.elim.:  7000/7425          
c   -- var.elim.:  7425/7425          
c   -- var.elim.:  1000/4885          
c   -- var.elim.:  2000/4885          
c   -- var.elim.:  3000/4885          
c   -- var.elim.:  4000/4885          
c   -- var.elim.:  4885/4885          
c   -- var.elim.:  1000/3549          
c   -- var.elim.:  2000/3549          
c   -- var.elim.:  3000/3549          
c   -- var.elim.:  3549/3549          
c   -- var.elim.:  1000/2923          
c   -- var.elim.:  2000/2923          
c   -- var.elim.:  2923/2923          
c   -- var.elim.:  971/971          
c   -- subsuming                       
c   -- var.elim.:  1000/3630          
c   -- var.elim.:  2000/3630          
c   -- var.elim.:  3000/3630          
c   -- var.elim.:  3630/3630          
c   -- var.elim.:  78/78          
c |         2 |   13308    76281 |      --       2       --      -- |     --   | -26050/-15340
c |         2 |   13308    76281 |    5323       2       14     7.0 |  0.000 % |
c |       102 |   13196    75406 |    5806      97     8825    91.0 |  0.938 % |
c |       252 |   13108    74731 |    6344     244    23290    95.5 |  1.564 % |
c |       478 |   12957    73560 |    6898     464    63926   137.8 |  2.693 % |
c |       815 |   12791    72203 |    7490     793    95125   120.0 |  3.927 % |
c |      1321 |   12271    68000 |    7905    1273   137914   108.3 |  8.028 % |
c |      2081 |   11963    65591 |    8477    2015   198267    98.4 | 10.460 % |
c |      3221 |   11922    65251 |    9293    3150   447940   142.2 | 10.791 % |
c |      4930 |   11809    64203 |   10125    4848   736161   151.8 | 11.729 % |
c |      7493 |   11665    63164 |   11002    7399  1059568   143.2 | 12.893 % |
c |     11338 |   11612    62732 |   12047   11238  1746076   155.4 | 13.345 % |
c |     17106 |   11585    62531 |   13221   12018  2348223   195.4 | 13.519 % |
c |     25757 |   11560    62364 |   14512   15732  3584339   227.8 | 13.710 % |
c |     38731 |   11560    62364 |   15963   17592  6018989   342.1 | 13.710 % |
c |     58192 |   11560    62364 |   17559   13195  4423649   335.3 | 13.710 % |
c |     87384 |   11560    62364 |   19315   16226  5522138   340.3 | 13.710 % |
c |    131174 |   11560    62364 |   21247   19707  8340497   423.2 | 13.710 % |
c |    196858 |   11513    62020 |   23276   17706  7541782   425.9 | 14.092 % |
c |    295387 |   11513    62020 |   25604   19557  6966860   356.2 | 14.092 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 29601
Raw data (stat): 29601 (runsolver) R 29600 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421965452 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 3790 0 0 0 986 12 0 0 25 0 1 0 421965452 17920000 3712 4294967295 134512640 134672761 3221224576 3221223024 134643545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4375 3712 603 41 0 4334 0
vsize: 17500
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 3881 0 0 0 1980 18 0 0 25 0 1 0 421965452 18358272 3803 4294967295 134512640 134672761 3221224576 3221223024 134643511 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4482 3803 603 41 0 4441 0
vsize: 17928
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 3930 0 0 0 2980 18 0 0 25 0 1 0 421965452 18358272 3813 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4482 3813 603 41 0 4441 0
vsize: 17928
[startup+40.0006 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 4745 0 0 0 3978 21 0 0 25 0 1 0 421965452 21573632 4628 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5267 4628 603 41 0 5226 0
vsize: 21068
[startup+50.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 6026 0 0 0 4974 25 0 0 25 0 1 0 421965452 26820608 5909 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6548 5909 603 41 0 6507 0
vsize: 26192
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 6426 0 0 0 5972 26 0 0 25 0 1 0 421965452 28504064 6309 4294967295 134512640 134672761 3221224576 3221223736 134614557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6959 6309 603 41 0 6918 0
vsize: 27836
[startup+70.0011 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 6865 0 0 0 6971 28 0 0 25 0 1 0 421965452 30314496 6748 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7401 6748 603 41 0 7360 0
vsize: 29604
[startup+80.0023 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 7160 0 0 0 7970 29 0 0 25 0 1 0 421965452 31494144 7043 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7689 7043 603 41 0 7648 0
vsize: 30756
[startup+90.0018 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 8123 0 0 0 8968 32 0 0 25 0 1 0 421965452 35446784 8006 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8654 8006 603 41 0 8613 0
vsize: 34616
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 8677 0 0 0 9966 33 0 0 25 0 1 0 421965452 37752832 8560 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9217 8560 603 41 0 9176 0
vsize: 36868
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 9399 0 0 0 10964 35 0 0 25 0 1 0 421965452 40759296 9282 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9951 9282 603 41 0 9910 0
vsize: 39804
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 9712 0 0 0 11963 37 0 0 25 0 1 0 421965452 41996288 9594 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10253 9594 603 41 0 10212 0
vsize: 41012
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 9923 0 0 0 12963 38 0 0 25 0 1 0 421965452 42909696 9805 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10476 9805 603 41 0 10435 0
vsize: 41904
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 10642 0 0 0 13961 40 0 0 25 0 1 0 421965452 45797376 10523 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11181 10523 603 41 0 11140 0
vsize: 44724
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 10642 0 0 0 14961 40 0 0 25 0 1 0 421965452 45797376 10523 4294967295 134512640 134672761 3221224576 3221223568 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11181 10523 603 41 0 11140 0
vsize: 44724
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11034 0 0 0 15959 41 0 0 25 0 1 0 421965452 47390720 10914 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11570 10914 603 41 0 11529 0
vsize: 46280
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11034 0 0 0 16959 41 0 0 25 0 1 0 421965452 47390720 10914 4294967295 134512640 134672761 3221224576 3221223616 134612676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11570 10914 603 41 0 11529 0
vsize: 46280
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11034 0 0 0 17959 41 0 0 25 0 1 0 421965452 47390720 10914 4294967295 134512640 134672761 3221224576 3221223728 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11570 10914 603 41 0 11529 0
vsize: 46280
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11034 0 0 0 18959 41 0 0 25 0 1 0 421965452 47390720 10914 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11570 10914 603 41 0 11529 0
vsize: 46280
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11035 0 0 0 19959 41 0 0 25 0 1 0 421965452 47325184 10912 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11554 10912 603 41 0 11513 0
vsize: 46216
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11035 0 0 0 20960 41 0 0 25 0 1 0 421965452 47325184 10912 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11554 10912 603 41 0 11513 0
vsize: 46216
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11035 0 0 0 21960 41 0 0 25 0 1 0 421965452 47325184 10912 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11554 10912 603 41 0 11513 0
vsize: 46216
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11415 0 0 0 22958 43 0 0 25 0 1 0 421965452 48930816 11291 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11946 11291 603 41 0 11905 0
vsize: 47784
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 11415 0 0 0 23959 43 0 0 25 0 1 0 421965452 48930816 11291 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11946 11291 603 41 0 11905 0
vsize: 47784
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 12326 0 0 0 24955 47 0 0 25 0 1 0 421965452 52690944 12202 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12864 12202 603 41 0 12823 0
vsize: 51456
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13271 0 0 0 25953 49 0 0 25 0 1 0 421965452 56520704 13147 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13147 603 41 0 13758 0
vsize: 55196
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13271 0 0 0 26953 49 0 0 25 0 1 0 421965452 56520704 13147 4294967295 134512640 134672761 3221224576 3221223616 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13147 603 41 0 13758 0
vsize: 55196
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13271 0 0 0 27953 49 0 0 25 0 1 0 421965452 56520704 13147 4294967295 134512640 134672761 3221224576 3221223672 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13147 603 41 0 13758 0
vsize: 55196
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13271 0 0 0 28953 49 0 0 25 0 1 0 421965452 56520704 13147 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13147 603 41 0 13758 0
vsize: 55196
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13271 0 0 0 29953 49 0 0 25 0 1 0 421965452 56520704 13147 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13147 603 41 0 13758 0
vsize: 55196
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13272 0 0 0 30953 49 0 0 25 0 1 0 421965452 56512512 13147 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13797 13147 603 41 0 13756 0
vsize: 55188
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13272 0 0 0 31954 49 0 0 25 0 1 0 421965452 56512512 13147 4294967295 134512640 134672761 3221224576 3221223760 134616020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13797 13147 603 41 0 13756 0
vsize: 55188
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13272 0 0 0 32954 49 0 0 25 0 1 0 421965452 56512512 13147 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13797 13147 603 41 0 13756 0
vsize: 55188
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 33954 49 0 0 25 0 1 0 421965452 56508416 13148 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 13148 603 41 0 13755 0
vsize: 55184
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 34954 49 0 0 25 0 1 0 421965452 56508416 13148 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 13148 603 41 0 13755 0
vsize: 55184
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 35955 49 0 0 25 0 1 0 421965452 56508416 13148 4294967295 134512640 134672761 3221224576 3221223616 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 13148 603 41 0 13755 0
vsize: 55184
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 36955 49 0 0 25 0 1 0 421965452 56508416 13148 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 13148 603 41 0 13755 0
vsize: 55184
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 37955 49 0 0 25 0 1 0 421965452 56508416 13148 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 13148 603 41 0 13755 0
vsize: 55184
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 38955 49 0 0 25 0 1 0 421965452 56508416 13148 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 13148 603 41 0 13755 0
vsize: 55184
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 39955 49 0 0 25 0 1 0 421965452 56471552 13147 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13787 13147 603 41 0 13746 0
vsize: 55148
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 40955 49 0 0 25 0 1 0 421965452 56471552 13147 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13787 13147 603 41 0 13746 0
vsize: 55148
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 41955 49 0 0 25 0 1 0 421965452 56471552 13147 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13787 13147 603 41 0 13746 0
vsize: 55148
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 42956 49 0 0 25 0 1 0 421965452 56471552 13147 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13787 13147 603 41 0 13746 0
vsize: 55148
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 43956 49 0 0 25 0 1 0 421965452 56471552 13147 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13787 13147 603 41 0 13746 0
vsize: 55148
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13273 0 0 0 44956 49 0 0 25 0 1 0 421965452 56471552 13147 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13787 13147 603 41 0 13746 0
vsize: 55148
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13313 0 0 0 45956 50 0 0 25 0 1 0 421965452 56745984 13187 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13854 13187 603 41 0 13813 0
vsize: 55416
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13829 0 0 0 46955 51 0 0 25 0 1 0 421965452 58781696 13703 4294967295 134512640 134672761 3221224576 3221223616 134612696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14351 13703 603 41 0 14310 0
vsize: 57404
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13829 0 0 0 47955 51 0 0 25 0 1 0 421965452 58781696 13703 4294967295 134512640 134672761 3221224576 3221223616 134614261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14351 13703 603 41 0 14310 0
vsize: 57404
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 13829 0 0 0 48955 51 0 0 25 0 1 0 421965452 58781696 13703 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14351 13703 603 41 0 14310 0
vsize: 57404
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14183 0 0 0 49955 52 0 0 25 0 1 0 421965452 60211200 14057 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14700 14057 603 41 0 14659 0
vsize: 58800
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14754 0 0 0 50953 54 0 0 25 0 1 0 421965452 62558208 14628 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15273 14628 603 41 0 15232 0
vsize: 61092
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14754 0 0 0 51953 54 0 0 25 0 1 0 421965452 62558208 14628 4294967295 134512640 134672761 3221224576 3221223592 1075346529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15273 14628 603 41 0 15232 0
vsize: 61092
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14754 0 0 0 52954 54 0 0 25 0 1 0 421965452 62558208 14628 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15273 14628 603 41 0 15232 0
vsize: 61092
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14754 0 0 0 53954 54 0 0 25 0 1 0 421965452 62558208 14628 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15273 14628 603 41 0 15232 0
vsize: 61092
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14944 0 0 0 54954 54 0 0 25 0 1 0 421965452 63336448 14818 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14818 603 41 0 15422 0
vsize: 61852
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14944 0 0 0 55954 54 0 0 25 0 1 0 421965452 63336448 14818 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14818 603 41 0 15422 0
vsize: 61852
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14944 0 0 0 56954 54 0 0 25 0 1 0 421965452 63336448 14818 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14818 603 41 0 15422 0
vsize: 61852
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 14944 0 0 0 57954 54 0 0 25 0 1 0 421965452 63336448 14818 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14818 603 41 0 15422 0
vsize: 61852
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16038 0 0 0 58952 56 0 0 25 0 1 0 421965452 67866624 15912 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16569 15912 603 41 0 16528 0
vsize: 66276
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 59951 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 60952 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223616 134614202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 61952 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 62952 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 63952 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 64953 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223584 134522540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 65953 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 66953 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 67953 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 68953 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 69954 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 70954 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 71954 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 72954 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16328 0 0 0 73954 57 0 0 25 0 1 0 421965452 69001216 16202 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16202 603 41 0 16805 0
vsize: 67384
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 16333 0 0 0 74955 57 0 0 25 0 1 0 421965452 69001216 16207 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16846 16207 603 41 0 16805 0
vsize: 67384
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17198 0 0 0 75953 59 0 0 25 0 1 0 421965452 72548352 17071 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17712 17071 603 41 0 17671 0
vsize: 70848
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17198 0 0 0 76953 59 0 0 25 0 1 0 421965452 72548352 17071 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17712 17071 603 41 0 17671 0
vsize: 70848
[startup+780.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17198 0 0 0 77953 59 0 0 25 0 1 0 421965452 72548352 17071 4294967295 134512640 134672761 3221224576 3221223616 134612771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17712 17071 603 41 0 17671 0
vsize: 70848
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17198 0 0 0 78953 59 0 0 25 0 1 0 421965452 72548352 17071 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17712 17071 603 41 0 17671 0
vsize: 70848
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17198 0 0 0 79953 59 0 0 25 0 1 0 421965452 72548352 17071 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17712 17071 603 41 0 17671 0
vsize: 70848
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 80953 60 0 0 25 0 1 0 421965452 74674176 17559 4294967295 134512640 134672761 3221224576 3221223672 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18231 17559 603 41 0 18190 0
vsize: 72924
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 81953 60 0 0 25 0 1 0 421965452 74543104 17558 4294967295 134512640 134672761 3221224576 3221223760 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 17558 603 41 0 18158 0
vsize: 72796
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 82953 60 0 0 25 0 1 0 421965452 74543104 17558 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 17558 603 41 0 18158 0
vsize: 72796
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 83953 60 0 0 25 0 1 0 421965452 74543104 17558 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 17558 603 41 0 18158 0
vsize: 72796
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 84953 60 0 0 25 0 1 0 421965452 74543104 17558 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 17558 603 41 0 18158 0
vsize: 72796
[startup+860.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 85954 60 0 0 25 0 1 0 421965452 74543104 17558 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 17558 603 41 0 18158 0
vsize: 72796
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 86954 60 0 0 25 0 1 0 421965452 74543104 17558 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 17558 603 41 0 18158 0
vsize: 72796
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 87954 60 0 0 25 0 1 0 421965452 74543104 17558 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 17558 603 41 0 18158 0
vsize: 72796
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 88954 60 0 0 25 0 1 0 421965452 74543104 17558 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 17558 603 41 0 18158 0
vsize: 72796
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 89954 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223616 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 90955 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 91955 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+930.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 92955 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 93955 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 94955 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 95956 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 96956 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 97956 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 98956 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 99956 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 100956 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 101957 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 102957 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 103957 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 104957 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 105957 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 106957 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 107958 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 108958 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 109958 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 110958 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 111958 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 112959 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 113959 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 114959 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 115959 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17686 0 0 0 116959 60 0 0 25 0 1 0 421965452 74518528 17557 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17557 603 41 0 18152 0
vsize: 72772
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17688 0 0 0 117959 60 0 0 25 0 1 0 421965452 74518528 17559 4294967295 134512640 134672761 3221224576 3221223776 134610493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17559 603 41 0 18152 0
vsize: 72772
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17688 0 0 0 118960 60 0 0 25 0 1 0 421965452 74518528 17559 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17559 603 41 0 18152 0
vsize: 72772
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29601
Raw data (stat): 29601 (minisat+) R 29600 25285 25284 0 -1 0 17688 0 0 0 119960 60 0 0 25 0 1 0 421965452 74518528 17559 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18193 17559 603 41 0 18152 0
vsize: 72772
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29601
Raw data (stat): 29601 (minisat+) Z 29600 25285 25284 0 -1 12 17689 0 0 0 119960 64 0 0 25 0 1 0 421965452 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.25
CPU user time (s): 1199.6
CPU system time (s): 0.646901
CPU usage (%): 100.014
Max. virtual memory (Kb): 72924
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####