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/synthesis-ptl-cmos-circuits/normalized-mux.opb
MD5SUM	fa7153262db792d01bec14f5a651af5b
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	872
Optimality of the best value was proved	NO
Number of terms in the objective function	232
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	9597
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	9597
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.332949
Number of variables	232
Total number of constraints	527
Number of constraints which are clauses	527
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	27
Trace number 5591

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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:        735592 kB
Buffers:         37812 kB
Cached:         220724 kB
SwapCached:          0 kB
Active:          82092 kB
Inactive:       179300 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        735340 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32000 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:57:43 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 4014 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 527 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 |     523     2315 |     156       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  206/206          
c |         0 |     517     2293 |      --       0       --      -- |     --   | -6/-22
c |         0 |     517     2293 |     206       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.027995 s)
c ==============================================================================
c [1mFound solution: 1330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:29793     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   71938   169068 |   21581       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/26428          
c   -- var.elim.:  2000/26428          
c   -- var.elim.:  3000/26428          
c   -- var.elim.:  4000/26428          
c   -- var.elim.:  5000/26428          
c   -- var.elim.:  6000/26428          
c   -- var.elim.:  7000/26428          
c   -- var.elim.:  8000/26428          
c   -- var.elim.:  9000/26428          
c   -- var.elim.:  10000/26428          
c   -- var.elim.:  11000/26428          
c   -- var.elim.:  12000/26428          
c   -- var.elim.:  13000/26428          
c   -- var.elim.:  14000/26428          
c   -- var.elim.:  15000/26428          
c   -- var.elim.:  16000/26428          
c   -- var.elim.:  17000/26428          
c   -- var.elim.:  18000/26428          
c   -- var.elim.:  19000/26428          
c   -- var.elim.:  20000/26428          
c   -- var.elim.:  21000/26428          
c   -- var.elim.:  22000/26428          
c   -- var.elim.:  23000/26428          
c   -- var.elim.:  24000/26428          
c   -- var.elim.:  25000/26428          
c   -- var.elim.:  26000/26428          
c   -- var.elim.:  26428/26428          
c   -- var.elim.:  1000/14147          
c   -- var.elim.:  2000/14147          
c   -- var.elim.:  3000/14147          
c   -- var.elim.:  4000/14147          
c   -- var.elim.:  5000/14147          
c   -- var.elim.:  6000/14147          
c   -- var.elim.:  7000/14147          
c   -- var.elim.:  8000/14147          
c   -- var.elim.:  9000/14147          
c   -- var.elim.:  10000/14147          
c   -- var.elim.:  11000/14147          
c   -- var.elim.:  12000/14147          
c   -- var.elim.:  13000/14147          
c   -- var.elim.:  14000/14147          
c   -- var.elim.:  14147/14147          
c   -- var.elim.:  52/52          
c   -- subsuming                       
c   -- var.elim.:  1000/2232          
c   -- var.elim.:  2000/2232          
c   -- var.elim.:  2232/2232          
c   -- var.elim.:  434/434          
c   -- subsuming                       
c   -- var.elim.:  38/38          
c |         0 |   63879   206366 |      --       0       --      -- |     --   | -8059/37299
c |         0 |   63879   206366 |   25551       0        0     nan |  0.000 % |
c |       101 |   63861   206122 |   28098     100     9768    97.7 |  0.021 % |
c |       251 |   63861   206122 |   30908     250    12021    48.1 |  0.021 % |
c |       477 |   63861   206122 |   33999     476    15402    32.4 |  0.021 % |
c |       814 |   63827   206008 |   37379     812    64545    79.5 |  0.049 % |
c |      1320 |   63084   203529 |   40638    1312    88508    67.5 |  0.788 % |
c |      2079 |   63084   203529 |   44702    2071   144126    69.6 |  0.788 % |
c |      3219 |   63084   203529 |   49173    3211   276664    86.2 |  0.788 % |
c |      4927 |   62906   202939 |   53937    4917   462872    94.1 |  0.957 % |
c |      7489 |   62906   202939 |   59331    7479  1083665   144.9 |  0.957 % |
c |     11333 |   62786   202402 |   65140   11314  1292662   114.3 |  1.140 % |
c |     17101 |   62786   202402 |   71654   17082  2403795   140.7 |  1.140 % |
c |     25751 |   62699   201924 |   78710   25729  5523326   214.7 |  1.211 % |
c |     38727 |   62550   201386 |   86375   38461  6357147   165.3 |  1.366 % |
c |     58188 |   62550   201386 |   95013   57922 17350973   299.6 |  1.366 % |
c |     87380 |   62339   200702 |  104162   86880 25807297   297.0 |  1.598 % |
c |    131170 |   62339   200702 |  114578   34981 20887747   597.1 |  1.598 % |
c ==============================================================================
c (current CPU-time: 955.967 s)
c ==============================================================================
c [1mFound solution: 1316[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:24283     Base: 2 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    171199 |  124012   344850 |   37203   75009 30701945   409.3 |  1.598 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24310          
c   -- var.elim.:  2000/24310          
c   -- var.elim.:  3000/24310          
c   -- var.elim.:  4000/24310          
c   -- var.elim.:  5000/24310          
c   -- var.elim.:  6000/24310          
c   -- var.elim.:  7000/24310          
c   -- var.elim.:  8000/24310          
c   -- var.elim.:  9000/24310          
c   -- var.elim.:  10000/24310          
c   -- var.elim.:  11000/24310          
c   -- var.elim.:  12000/24310          
c   -- var.elim.:  13000/24310          
c   -- var.elim.:  14000/24310          
c   -- var.elim.:  15000/24310          
c   -- var.elim.:  16000/24310          
c   -- var.elim.:  17000/24310          
c   -- var.elim.:  18000/24310          
c   -- var.elim.:  19000/24310          
c   -- var.elim.:  20000/24310          
c   -- var.elim.:  21000/24310          
c   -- var.elim.:  22000/24310          
c   -- var.elim.:  23000/24310          
c   -- var.elim.:  24000/24310          
c   -- var.elim.:  24310/24310          
c   -- var.elim.:  1000/13273          
c   -- var.elim.:  2000/13273          
c   -- var.elim.:  3000/13273          
c   -- var.elim.:  4000/13273          
c   -- var.elim.:  5000/13273          
c   -- var.elim.:  6000/13273          
c   -- var.elim.:  7000/13273          
c   -- var.elim.:  8000/13273          
c   -- var.elim.:  9000/13273          
c   -- var.elim.:  10000/13273          
c   -- var.elim.:  11000/13273          
c   -- var.elim.:  12000/13273          
c   -- var.elim.:  13000/13273          
c   -- var.elim.:  13273/13273          
c   -- var.elim.:  553/553          
c   -- var.elim.:  599/599          
c   -- var.elim.:  258/258          
c   -- subsumi#### 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.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (runsolver) R 16592 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480325144 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 4491 0 0 0 985 12 0 0 25 0 1 0 480325144 19845120 4145 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4845 4145 603 41 0 4804 0
vsize: 19380
[startup+20.0022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 4928 0 0 0 1982 15 0 0 25 0 1 0 480325144 21688320 4582 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5295 4582 603 41 0 5254 0
vsize: 21180
[startup+30.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 5588 0 0 0 2980 17 0 0 25 0 1 0 480325144 24395776 5242 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5956 5242 603 41 0 5915 0
vsize: 23824
[startup+40.0025 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 6135 0 0 0 3979 18 0 0 25 0 1 0 480325144 26632192 5789 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6502 5789 603 41 0 6461 0
vsize: 26008
[startup+50.0027 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 6831 0 0 0 4977 20 0 0 25 0 1 0 480325144 29581312 6485 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7222 6485 603 41 0 7181 0
vsize: 28888
[startup+60.0034 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 7419 0 0 0 5976 21 0 0 25 0 1 0 480325144 31932416 7073 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7796 7073 603 41 0 7755 0
vsize: 31184
[startup+70.0039 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 8180 0 0 0 6974 24 0 0 25 0 1 0 480325144 35065856 7834 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8561 7834 603 41 0 8520 0
vsize: 34244
[startup+80.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 9186 0 0 0 7972 25 0 0 25 0 1 0 480325144 39165952 8840 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8840 603 41 0 9521 0
vsize: 38248
[startup+90.0049 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 10050 0 0 0 8971 27 0 0 25 0 1 0 480325144 42708992 9704 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10427 9704 603 41 0 10386 0
vsize: 41708
[startup+100.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 10260 0 0 0 9970 28 0 0 25 0 1 0 480325144 43499520 9914 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10620 9914 603 41 0 10579 0
vsize: 42480
[startup+110.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 10648 0 0 0 10969 30 0 0 25 0 1 0 480325144 45215744 10302 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11039 10302 603 41 0 10998 0
vsize: 44156
[startup+120.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 10916 0 0 0 11967 31 0 0 25 0 1 0 480325144 46264320 10570 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11295 10570 603 41 0 11254 0
vsize: 45180
[startup+130.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 11387 0 0 0 12967 32 0 0 25 0 1 0 480325144 48246784 11041 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11779 11041 603 41 0 11738 0
vsize: 47116
[startup+140.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 12235 0 0 0 13964 35 0 0 25 0 1 0 480325144 51642368 11889 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12608 11889 603 41 0 12567 0
vsize: 50432
[startup+150.007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 13042 0 0 0 14962 37 0 0 25 0 1 0 480325144 55029760 12696 4294967295 134512640 134672761 3221224576 3221223616 134612587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13435 12697 603 41 0 13394 0
vsize: 53740
[startup+160.007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 13963 0 0 0 15960 40 0 0 25 0 1 0 480325144 58777600 13617 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14350 13617 603 41 0 14309 0
vsize: 57400
[startup+170.007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 14816 0 0 0 16958 41 0 0 25 0 1 0 480325144 62255104 14470 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15199 14470 603 41 0 15158 0
vsize: 60796
[startup+180.007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 15791 0 0 0 17957 43 0 0 25 0 1 0 480325144 66215936 15445 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16166 15445 603 41 0 16125 0
vsize: 64664
[startup+190.008 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 16886 0 0 0 18954 46 0 0 25 0 1 0 480325144 70701056 16540 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17261 16540 603 41 0 17220 0
vsize: 69044
[startup+200.008 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 17831 0 0 0 19952 48 0 0 25 0 1 0 480325144 74616832 17485 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18217 17485 603 41 0 18176 0
vsize: 72868
[startup+210.008 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 18709 0 0 0 20950 50 0 0 25 0 1 0 480325144 78127104 18363 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19074 18363 603 41 0 19033 0
vsize: 76296
[startup+220.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 19588 0 0 0 21947 53 0 0 25 0 1 0 480325144 81731584 19242 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19954 19242 603 41 0 19913 0
vsize: 79816
[startup+230.009 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 20375 0 0 0 22946 55 0 0 25 0 1 0 480325144 84992000 20029 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20750 20029 603 41 0 20709 0
vsize: 83000
[startup+240.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 21272 0 0 0 23944 57 0 0 25 0 1 0 480325144 88592384 20926 4294967295 134512640 134672761 3221224576 3221223616 134613809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21629 20926 603 41 0 21588 0
vsize: 86516
[startup+250.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 21980 0 0 0 24943 58 0 0 25 0 1 0 480325144 91557888 21634 4294967295 134512640 134672761 3221224576 3221223720 134616314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22353 21634 603 41 0 22312 0
vsize: 89412
[startup+260.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 22132 0 0 0 25943 59 0 0 25 0 1 0 480325144 92094464 21786 4294967295 134512640 134672761 3221224576 3221223720 134616336 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22484 21786 603 41 0 22443 0
vsize: 89936
[startup+270.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 22413 0 0 0 26943 59 0 0 25 0 1 0 480325144 93286400 22067 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22775 22067 603 41 0 22734 0
vsize: 91100
[startup+280.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 22843 0 0 0 27942 60 0 0 25 0 1 0 480325144 95002624 22497 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23194 22497 603 41 0 23153 0
vsize: 92776
[startup+290.011 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 23362 0 0 0 28941 61 0 0 25 0 1 0 480325144 97488896 23016 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23801 23016 603 41 0 23760 0
vsize: 95204
[startup+300.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 23905 0 0 0 29939 63 0 0 25 0 1 0 480325144 99586048 23559 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24313 23559 603 41 0 24272 0
vsize: 97252
[startup+310.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 24336 0 0 0 30938 64 0 0 25 0 1 0 480325144 101421056 23990 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24761 23990 603 41 0 24720 0
vsize: 99044
[startup+320.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 24818 0 0 0 31937 66 0 0 25 0 1 0 480325144 103383040 24472 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25240 24472 603 41 0 25199 0
vsize: 100960
[startup+330.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 25420 0 0 0 32935 67 0 0 25 0 1 0 480325144 105766912 25074 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25822 25074 603 41 0 25781 0
vsize: 103288
[startup+340.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 26074 0 0 0 33934 69 0 0 25 0 1 0 480325144 108515328 25728 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26493 25728 603 41 0 26452 0
vsize: 105972
[startup+350.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 26676 0 0 0 34933 70 0 0 25 0 1 0 480325144 111013888 26330 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27103 26331 603 41 0 27062 0
vsize: 108412
[startup+360.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 27479 0 0 0 35931 73 0 0 25 0 1 0 480325144 114282496 27133 4294967295 134512640 134672761 3221224576 3221223712 134614503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27901 27133 603 41 0 27860 0
vsize: 111604
[startup+370.013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 28041 0 0 0 36930 73 0 0 25 0 1 0 480325144 116490240 27695 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28440 27695 603 41 0 28399 0
vsize: 113760
[startup+380.012 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 28719 0 0 0 37928 75 0 0 25 0 1 0 480325144 119341056 28373 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29136 28373 603 41 0 29095 0
vsize: 116544
[startup+390.013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 29375 0 0 0 38927 77 0 0 25 0 1 0 480325144 121978880 29029 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29780 29029 603 41 0 29739 0
vsize: 119120
[startup+400.013 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 29910 0 0 0 39926 78 0 0 25 0 1 0 480325144 124215296 29564 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30326 29564 603 41 0 30285 0
vsize: 121304
[startup+410.014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 30317 0 0 0 40926 79 0 0 25 0 1 0 480325144 125915136 29971 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30741 29971 603 41 0 30700 0
vsize: 122964
[startup+420.014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 30916 0 0 0 41924 80 0 0 25 0 1 0 480325144 128266240 30570 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31315 30570 603 41 0 31274 0
vsize: 125260
[startup+430.014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 31620 0 0 0 42923 82 0 0 25 0 1 0 480325144 131149824 31274 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32019 31274 603 41 0 31978 0
vsize: 128076
[startup+440.015 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 32497 0 0 0 43921 84 0 0 25 0 1 0 480325144 134799360 32151 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32910 32153 603 41 0 32869 0
vsize: 131640
[startup+450.014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 33287 0 0 0 44919 86 0 0 25 0 1 0 480325144 138063872 32941 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33707 32941 603 41 0 33666 0
vsize: 134828
[startup+460.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 34013 0 0 0 45917 88 0 0 25 0 1 0 480325144 140922880 33667 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34405 33667 603 41 0 34364 0
vsize: 137620
[startup+470.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 34839 0 0 0 46916 90 0 0 25 0 1 0 480325144 144408576 34493 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35256 34493 603 41 0 35215 0
vsize: 141024
[startup+480.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 35519 0 0 0 47915 91 0 0 25 0 1 0 480325144 147144704 35173 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35924 35173 603 41 0 35883 0
vsize: 143696
[startup+490.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 35736 0 0 0 48914 92 0 0 25 0 1 0 480325144 148066304 35390 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36149 35390 603 41 0 36108 0
vsize: 144596
[startup+500.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 36183 0 0 0 49913 93 0 0 25 0 1 0 480325144 149774336 35837 4294967295 134512640 134672761 3221224576 3221223712 134614800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36566 35837 603 41 0 36525 0
vsize: 146264
[startup+510.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 37065 0 0 0 50913 94 0 0 25 0 1 0 480325144 153419776 36719 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37456 36719 603 41 0 37415 0
vsize: 149824
[startup+520.017 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 37568 0 0 0 51911 95 0 0 25 0 1 0 480325144 155533312 37222 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37972 37222 603 41 0 37931 0
vsize: 151888
[startup+530.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 38276 0 0 0 52910 97 0 0 25 0 1 0 480325144 158445568 37930 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38683 37930 603 41 0 38642 0
vsize: 154732
[startup+540.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 39159 0 0 0 53907 100 0 0 25 0 1 0 480325144 161955840 38813 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39540 38813 603 41 0 39499 0
vsize: 158160
[startup+550.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 40079 0 0 0 54905 102 0 0 25 0 1 0 480325144 165806080 39733 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40480 39733 603 41 0 40439 0
vsize: 161920
[startup+560.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 40819 0 0 0 55904 103 0 0 25 0 1 0 480325144 168816640 40473 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41215 40473 603 41 0 41174 0
vsize: 164860
[startup+570.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 41612 0 0 0 56903 105 0 0 25 0 1 0 480325144 172044288 41266 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42003 41266 603 41 0 41962 0
vsize: 168012
[startup+580.018 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 57902 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+590.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 58902 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+600.019 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 59902 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+610.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 60902 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223712 134614551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+620.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 61902 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+630.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 62902 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223744 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+640.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 63903 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+650.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 64903 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+660.02 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42110 0 0 0 65903 106 0 0 25 0 1 0 480325144 173711360 41655 4294967295 134512640 134672761 3221224576 3221223616 134603536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41655 603 41 0 42369 0
vsize: 169640
[startup+670.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 66903 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+680.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 67903 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+690.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 68903 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+700.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 69904 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+710.021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 70904 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+720.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 71904 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+730.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 72904 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+740.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 73904 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+750.022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 74904 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+760.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 75904 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+770.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 76905 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615488 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+780.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 77905 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+790.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 78905 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+800.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 79905 106 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+810.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 80905 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+820.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 81905 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+830.023 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 82906 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+840.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 83906 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+850.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 84906 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+860.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 85906 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+870.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 86906 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+880.024 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 87907 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+890.025 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 88907 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223616 134612663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+900.025 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 89907 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+910.026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 90907 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+920.026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 91907 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+930.026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 92907 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+940.027 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 93908 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+950.027 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 42111 0 0 0 94908 107 0 0 25 0 1 0 480325144 173711360 41656 4294967295 134512640 134672761 3221224576 3221223760 134615505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42410 41656 603 41 0 42369 0
vsize: 169640
[startup+960.026 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 43460 0 0 0 95898 116 0 0 25 0 1 0 480325144 177188864 42368 4294967295 134512640 134672761 3221224576 3221222880 134621829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43259 42368 603 41 0 43218 0
vsize: 173036
[startup+970.028 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 96896 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+980.027 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 97896 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+990.028 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 98896 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223776 134610622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 99896 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 100896 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 101897 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 102897 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 103897 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 104897 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 105897 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 106898 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 107898 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 108898 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1100.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 109898 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223584 134522555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1110.03 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 110898 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1120.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 111898 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1130.03 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 112899 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223712 134614800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1140.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 113899 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1150.03 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 114899 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1160.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 115899 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1170.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 116899 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1180.03 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 117900 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1190.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 118900 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
[startup+1200.03 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 16593
Raw data (stat): 16593 (minisat+) R 16592 11931 11930 0 -1 0 44187 0 0 0 119900 118 0 0 25 0 1 0 480325144 177180672 42367 4294967295 134512640 134672761 3221224576 3221223616 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43257 42367 603 41 0 43216 0
vsize: 173028
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.01 1.00 0.92 1/54 16593
Raw data (stat): 16593 (minisat+) Z 16592 11931 11930 0 -1 12 44188 0 0 0 119900 126 0 0 25 0 1 0 480325144 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.27
CPU user time (s): 1199.01
CPU system time (s): 1.26781
CPU usage (%): 100.013
Max. virtual memory (Kb): 173036
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####