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/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare1_1.opb
MD5SUM	452acf9ed3adc2d2cfe293dad01c0934
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	167110
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.02
Number of variables	280
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	130
Trace number 20792

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 21:50:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14474 boxname=wulflinc1 idbench=1114 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  452acf9ed3adc2d2cfe293dad01c0934  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-markshare1_1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-markshare1_1.opb
IDLAUNCH: 14474
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        690096 kB
Buffers:          1452 kB
Cached:         318624 kB
SwapCached:          0 kB
Active:          72268 kB
Inactive:       250960 kB
HighTotal:      131008 kB
HighFree:        17780 kB
LowTotal:       903652 kB
LowFree:        672316 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7172 kB
Slab:            15536 kB
Committed_AS:    92808 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 22:10:43 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 14474 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> Adder-cost: 662   maxlim: 3510008   bits: 23/22
c ---[   8]---> Adder-cost: 660   maxlim: 3759828   bits: 23/22
c ---[   6]---> Adder-cost: 770   maxlim: 3884662   bits: 23/22
c ---[   4]---> Adder-cost: 500   maxlim: 3402645   bits: 23/22
c ---[   2]---> Adder-cost: 574   maxlim: 3468109   bits: 23/22
c ---[   0]---> Adder-cost: 558   maxlim: 3462997   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25238    89630 |    8412       0        0     nan |  0.000 % |
c |       100 |   25230    89604 |    9253      99      750     7.6 |  7.959 % |
c |       250 |   25230    89604 |   10178     249     3701    14.9 |  7.959 % |
c |       475 |   25230    89604 |   11196     474     5830    12.3 |  7.959 % |
c ==============================================================================
c [1mFound solution: 5377694[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       604 |   29633    99881 |    9877     603     6492    10.8 |  7.959 % |
c ==============================================================================
c [1mFound solution: 5293744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       607 |   29665    99990 |    9888     606     7209    11.9 |  7.959 % |
c |       707 |   29657    99964 |   10876     705     9192    13.0 |  5.848 % |
c |       857 |   29657    99964 |   11964     855    11646    13.6 |  5.848 % |
c ==============================================================================
c [1mFound solution: 4764672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       862 |   29687   100034 |    9895     860    11711    13.6 |  5.848 % |
c ==============================================================================
c [1mFound solution: 1599618[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       881 |   29718   100104 |    9906     879    11938    13.6 |  5.848 % |
c |       981 |   29718   100104 |   10896     979    12922    13.2 |  5.853 % |
c |      1131 |   29718   100104 |   11986    1129    41916    37.1 |  5.853 % |
c |      1356 |   29718   100104 |   13184    1354    49026    36.2 |  5.853 % |
c |      1693 |   29702   100052 |   14503    1689    52554    31.1 |  5.887 % |
c |      2199 |   29679    99985 |   15953    2192    59198    27.0 |  5.957 % |
c |      2960 |   29671    99959 |   17549    2952    80220    27.2 |  5.975 % |
c |      4099 |   29663    99933 |   19303    4090   121045    29.6 |  5.992 % |
c |      5807 |   29655    99907 |   21234    5797   175882    30.3 |  6.010 % |
c |      8369 |   29655    99907 |   23357    8359   283693    33.9 |  6.010 % |
c |     12213 |   29639    99855 |   25693   12201   440130    36.1 |  6.045 % |
c |     17980 |   29631    99829 |   28262   17966   664991    37.0 |  6.062 % |
c |     26630 |   29631    99829 |   31089   26616  1159633    43.6 |  6.062 % |
c |     39605 |   29631    99829 |   34198   20932  1149938    54.9 |  6.062 % |
c |     59066 |   29623    99803 |   37618   16230   879352    54.2 |  6.080 % |
c |     88259 |   29608    99762 |   41379   20636  1003940    48.6 |  6.132 % |
c ==============================================================================
c [1mFound solution: 279567[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89650 |   29408    99201 |    9802   21458   995466    46.4 |  6.132 % |
c |     89750 |   29408    99201 |   10782    5465   179655    32.9 |  7.083 % |
c |     89900 |   29408    99201 |   11860    5615   182646    32.5 |  7.083 % |
c |     90125 |   29408    99201 |   13046    5840   186971    32.0 |  7.083 % |
c |     90462 |   29408    99201 |   14351    6177   196392    31.8 |  7.083 % |
c |     90968 |   29408    99201 |   15786    6683   207978    31.1 |  7.083 % |
c |     91727 |   29408    99201 |   17364    7442   224614    30.2 |  7.083 % |
c |     92867 |   29408    99201 |   19101    8582   261733    30.5 |  7.083 % |
c |     94575 |   29408    99201 |   21011   10290   361389    35.1 |  7.083 % |
c |     97139 |   29408    99201 |   23112   12854   437079    34.0 |  7.083 % |
c |    100983 |   29408    99201 |   25423   16698   596929    35.7 |  7.083 % |
c |    106750 |   29408    99201 |   27966   22465   820896    36.5 |  7.083 % |
c |    115400 |   29408    99201 |   30762   14540   507022    34.9 |  7.083 % |
c |    128375 |   29390    99161 |   33839   27514  1069997    38.9 |  7.188 % |
c |    147837 |   29382    99135 |   37223   25873  1158066    44.8 |  7.205 % |
c |    177029 |   29382    99135 |   40945   28960  1496602    51.7 |  7.205 % |
c |    220820 |   29358    99079 |   45039   18307   765399    41.8 |  7.362 % |
c |    286504 |   29342    99027 |   49543   21496   871280    40.5 |  7.397 % |
c |    385030 |   29334    99001 |   54498   47574  2572959    54.1 |  7.415 % |
c |    532819 |   29287    98896 |   59948   32047  1863533    58.1 |  7.641 % |
c |    754502 |   29287    98896 |   65942   32983  2410685    73.1 |  7.641 % |
#### 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.96 1.00 0.92 1/56 4726
Raw data (stat): 4726 (runsolver) D 4725 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 433378497 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.96 1.00 0.92 3/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 1677 0 0 0 976 5 0 0 25 0 1 0 433378497 8454144 1651 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2064 1651 603 41 0 2023 0
vsize: 8256
[startup+20.0014 s]
Raw data (loadavg): 0.97 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 2319 0 0 0 1974 7 0 0 25 0 1 0 433378497 11096064 2293 4294967295 134512640 134672761 3221224624 3221223808 134559566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2709 2293 603 41 0 2668 0
vsize: 10836
[startup+30.0008 s]
Raw data (loadavg): 0.97 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 2809 0 0 0 2972 9 0 0 25 0 1 0 433378497 13099008 2783 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3198 2783 603 41 0 3157 0
vsize: 12792
[startup+40.0046 s]
Raw data (loadavg): 0.98 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 2809 0 0 0 3973 9 0 0 25 0 1 0 433378497 13099008 2783 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3198 2783 603 41 0 3157 0
vsize: 12792
[startup+50.0134 s]
Raw data (loadavg): 0.98 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3294 0 0 0 4972 11 0 0 25 0 1 0 433378497 15228928 3268 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3718 3268 603 41 0 3677 0
vsize: 14872
[startup+60.0132 s]
Raw data (loadavg): 0.98 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3527 0 0 0 5971 12 0 0 25 0 1 0 433378497 16162816 3501 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3501 603 41 0 3905 0
vsize: 15784
[startup+70.0139 s]
Raw data (loadavg): 0.98 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3527 0 0 0 6971 12 0 0 25 0 1 0 433378497 16162816 3501 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3501 603 41 0 3905 0
vsize: 15784
[startup+80.0152 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3542 0 0 0 7971 12 0 0 25 0 1 0 433378497 16162816 3516 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3516 603 41 0 3905 0
vsize: 15784
[startup+90.0155 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3542 0 0 0 8971 12 0 0 25 0 1 0 433378497 16162816 3516 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3516 603 41 0 3905 0
vsize: 15784
[startup+100.015 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3542 0 0 0 9971 12 0 0 25 0 1 0 433378497 16162816 3516 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3516 603 41 0 3905 0
vsize: 15784
[startup+110.015 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3542 0 0 0 10971 13 0 0 25 0 1 0 433378497 16162816 3516 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3516 603 41 0 3905 0
vsize: 15784
[startup+120.016 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3542 0 0 0 11971 13 0 0 25 0 1 0 433378497 16162816 3516 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3516 603 41 0 3905 0
vsize: 15784
[startup+130.016 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3542 0 0 0 12971 13 0 0 25 0 1 0 433378497 16162816 3516 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3516 603 41 0 3905 0
vsize: 15784
[startup+140.017 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3542 0 0 0 13971 13 0 0 25 0 1 0 433378497 16162816 3516 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3946 3516 603 41 0 3905 0
vsize: 15784
[startup+150.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3577 0 0 0 14971 13 0 0 25 0 1 0 433378497 16297984 3551 4294967295 134512640 134672761 3221224624 3221223824 134557916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3979 3551 603 41 0 3938 0
vsize: 15916
[startup+160.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3588 0 0 0 15971 13 0 0 25 0 1 0 433378497 16429056 3562 4294967295 134512640 134672761 3221224624 3221223792 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4011 3562 603 41 0 3970 0
vsize: 16044
[startup+170.019 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3588 0 0 0 16971 13 0 0 25 0 1 0 433378497 16429056 3562 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4011 3562 603 41 0 3970 0
vsize: 16044
[startup+180.019 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3870 0 0 0 17971 14 0 0 25 0 1 0 433378497 17506304 3844 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4274 3844 603 41 0 4233 0
vsize: 17096
[startup+190.019 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3870 0 0 0 18971 14 0 0 25 0 1 0 433378497 17506304 3844 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4274 3844 603 41 0 4233 0
vsize: 17096
[startup+200.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3874 0 0 0 19972 14 0 0 25 0 1 0 433378497 17506304 3848 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4274 3848 603 41 0 4233 0
vsize: 17096
[startup+210.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3898 0 0 0 20972 14 0 0 25 0 1 0 433378497 17653760 3872 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4310 3872 603 41 0 4269 0
vsize: 17240
[startup+220.044 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3911 0 0 0 21973 15 0 0 25 0 1 0 433378497 17801216 3885 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4346 3885 603 41 0 4305 0
vsize: 17384
[startup+230.043 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3911 0 0 0 22973 15 0 0 25 0 1 0 433378497 17801216 3885 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4346 3885 603 41 0 4305 0
vsize: 17384
[startup+240.043 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3919 0 0 0 23974 15 0 0 25 0 1 0 433378497 17801216 3893 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4346 3893 603 41 0 4305 0
vsize: 17384
[startup+250.043 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4726
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3935 0 0 0 24974 15 0 0 25 0 1 0 433378497 17801216 3909 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4346 3909 603 41 0 4305 0
vsize: 17384
[startup+260.043 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 3949 0 0 0 25974 15 0 0 25 0 1 0 433378497 17965056 3923 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4386 3923 603 41 0 4345 0
vsize: 17544
[startup+270.044 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4066 0 0 0 26974 15 0 0 25 0 1 0 433378497 18366464 4040 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4484 4040 603 41 0 4443 0
vsize: 17936
[startup+280.043 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4071 0 0 0 27974 15 0 0 25 0 1 0 433378497 18366464 4045 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4484 4045 603 41 0 4443 0
vsize: 17936
[startup+290.044 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4074 0 0 0 28974 15 0 0 25 0 1 0 433378497 18366464 4048 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4484 4048 603 41 0 4443 0
vsize: 17936
[startup+300.044 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4078 0 0 0 29974 15 0 0 25 0 1 0 433378497 18501632 4052 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4517 4052 603 41 0 4476 0
vsize: 18068
[startup+310.044 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4122 0 0 0 30974 15 0 0 25 0 1 0 433378497 18636800 4096 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4550 4096 603 41 0 4509 0
vsize: 18200
[startup+320.044 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4122 0 0 0 31974 15 0 0 25 0 1 0 433378497 18636800 4096 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4550 4096 603 41 0 4509 0
vsize: 18200
[startup+330.044 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4122 0 0 0 32975 15 0 0 25 0 1 0 433378497 18636800 4096 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4550 4096 603 41 0 4509 0
vsize: 18200
[startup+340.045 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4122 0 0 0 33975 15 0 0 25 0 1 0 433378497 18636800 4096 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4550 4096 603 41 0 4509 0
vsize: 18200
[startup+350.045 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4407 0 0 0 34975 15 0 0 25 0 1 0 433378497 19841024 4381 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4844 4381 603 41 0 4803 0
vsize: 19376
[startup+360.051 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4733 0 0 0 35974 16 0 0 25 0 1 0 433378497 21168128 4707 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5168 4707 603 41 0 5127 0
vsize: 20672
[startup+370.05 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4755 0 0 0 36974 16 0 0 25 0 1 0 433378497 21168128 4729 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5168 4729 603 41 0 5127 0
vsize: 20672
[startup+380.056 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4756 0 0 0 37975 16 0 0 25 0 1 0 433378497 21168128 4730 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5168 4730 603 41 0 5127 0
vsize: 20672
[startup+390.056 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4776 0 0 0 38975 17 0 0 25 0 1 0 433378497 21311488 4750 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5203 4750 603 41 0 5162 0
vsize: 20812
[startup+400.057 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4781 0 0 0 39976 17 0 0 25 0 1 0 433378497 21311488 4755 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5203 4755 603 41 0 5162 0
vsize: 20812
[startup+410.057 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4781 0 0 0 40976 17 0 0 25 0 1 0 433378497 21311488 4755 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5203 4755 603 41 0 5162 0
vsize: 20812
[startup+420.056 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4918 0 0 0 41975 17 0 0 25 0 1 0 433378497 21979136 4892 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5366 4892 603 41 0 5325 0
vsize: 21464
[startup+430.057 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4918 0 0 0 42976 17 0 0 25 0 1 0 433378497 21979136 4892 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5366 4892 603 41 0 5325 0
vsize: 21464
[startup+440.166 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4918 0 0 0 43987 17 0 0 25 0 1 0 433378497 21979136 4892 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5366 4892 603 41 0 5325 0
vsize: 21464
[startup+450.167 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 4918 0 0 0 44987 17 0 0 25 0 1 0 433378497 21979136 4892 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5366 4892 603 41 0 5325 0
vsize: 21464
[startup+460.167 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 5001 0 0 0 45987 17 0 0 25 0 1 0 433378497 22245376 4975 4294967295 134512640 134672761 3221224624 3221223728 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4975 603 41 0 5390 0
vsize: 21724
[startup+470.169 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 5392 0 0 0 46986 18 0 0 25 0 1 0 433378497 23846912 5366 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5822 5366 603 41 0 5781 0
vsize: 23288
[startup+480.169 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 5609 0 0 0 47985 19 0 0 25 0 1 0 433378497 24784896 5583 4294967295 134512640 134672761 3221224624 3221223776 134565103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6051 5583 603 41 0 6010 0
vsize: 24204
[startup+490.17 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 5609 0 0 0 48985 19 0 0 25 0 1 0 433378497 24784896 5583 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6051 5583 603 41 0 6010 0
vsize: 24204
[startup+500.171 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 5609 0 0 0 49985 19 0 0 25 0 1 0 433378497 24784896 5583 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6051 5583 603 41 0 6010 0
vsize: 24204
[startup+510.171 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 5792 0 0 0 50984 20 0 0 25 0 1 0 433378497 25460736 5766 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6216 5766 603 41 0 6175 0
vsize: 24864
[startup+520.17 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6353 0 0 0 51983 21 0 0 25 0 1 0 433378497 27734016 6327 4294967295 134512640 134672761 3221224624 3221223728 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6771 6327 603 41 0 6730 0
vsize: 27084
[startup+530.17 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6655 0 0 0 52982 23 0 0 25 0 1 0 433378497 29077504 6629 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6629 603 41 0 7058 0
vsize: 28396
[startup+540.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6655 0 0 0 53982 23 0 0 25 0 1 0 433378497 29077504 6629 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6629 603 41 0 7058 0
vsize: 28396
[startup+550.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4728
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6655 0 0 0 54982 23 0 0 25 0 1 0 433378497 29077504 6629 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6629 603 41 0 7058 0
vsize: 28396
[startup+560.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4730
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6655 0 0 0 55982 24 0 0 25 0 1 0 433378497 29077504 6629 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7099 6629 603 41 0 7058 0
vsize: 28396
[startup+570.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4783
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6655 0 0 0 56980 24 0 0 25 0 1 0 433378497 29077504 6629 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7099 6629 603 41 0 7058 0
vsize: 28396
[startup+580.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4783
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6742 0 0 0 57979 25 0 0 25 0 1 0 433378497 29347840 6716 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7165 6716 603 41 0 7124 0
vsize: 28660
[startup+590.177 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4783
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 58980 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+600.177 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4783
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 59980 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+610.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4783
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 60980 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+620.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4785
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 61980 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223808 134559660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+630.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4785
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 62980 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+640.177 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 63980 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+650.177 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 64981 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+660.176 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 65981 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+670.177 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 66981 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223728 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+680.178 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 67981 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+690.179 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6852 0 0 0 68981 25 0 0 25 0 1 0 433378497 29888512 6826 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7297 6826 603 41 0 7256 0
vsize: 29188
[startup+700.178 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6855 0 0 0 69981 25 0 0 25 0 1 0 433378497 29888512 6829 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7297 6829 603 41 0 7256 0
vsize: 29188
[startup+710.178 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6930 0 0 0 70981 25 0 0 25 0 1 0 433378497 30154752 6904 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6904 603 41 0 7321 0
vsize: 29448
[startup+720.179 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6930 0 0 0 71981 26 0 0 25 0 1 0 433378497 30154752 6904 4294967295 134512640 134672761 3221224624 3221223792 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6904 603 41 0 7321 0
vsize: 29448
[startup+730.179 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6930 0 0 0 72981 26 0 0 25 0 1 0 433378497 30154752 6904 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6904 603 41 0 7321 0
vsize: 29448
[startup+740.18 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6930 0 0 0 73981 26 0 0 25 0 1 0 433378497 30154752 6904 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6904 603 41 0 7321 0
vsize: 29448
[startup+750.181 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6930 0 0 0 74981 26 0 0 25 0 1 0 433378497 30154752 6904 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6904 603 41 0 7321 0
vsize: 29448
[startup+760.18 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6930 0 0 0 75981 26 0 0 25 0 1 0 433378497 30154752 6904 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6904 603 41 0 7321 0
vsize: 29448
[startup+770.18 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6935 0 0 0 76981 26 0 0 25 0 1 0 433378497 30154752 6909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6909 603 41 0 7321 0
vsize: 29448
[startup+780.182 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 6935 0 0 0 77981 26 0 0 25 0 1 0 433378497 30154752 6909 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7362 6909 603 41 0 7321 0
vsize: 29448
[startup+790.183 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7151 0 0 0 78980 28 0 0 25 0 1 0 433378497 31088640 7125 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7590 7125 603 41 0 7549 0
vsize: 30360
[startup+800.183 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7151 0 0 0 79980 28 0 0 25 0 1 0 433378497 31088640 7125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7590 7125 603 41 0 7549 0
vsize: 30360
[startup+810.182 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7151 0 0 0 80980 28 0 0 25 0 1 0 433378497 31088640 7125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7590 7125 603 41 0 7549 0
vsize: 30360
[startup+820.183 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7151 0 0 0 81980 28 0 0 25 0 1 0 433378497 31088640 7125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7590 7125 603 41 0 7549 0
vsize: 30360
[startup+830.183 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7151 0 0 0 82980 28 0 0 25 0 1 0 433378497 31088640 7125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7590 7125 603 41 0 7549 0
vsize: 30360
[startup+840.184 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7154 0 0 0 83980 28 0 0 25 0 1 0 433378497 31088640 7128 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7590 7128 603 41 0 7549 0
vsize: 30360
[startup+850.184 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4787
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7159 0 0 0 84980 28 0 0 25 0 1 0 433378497 31088640 7133 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7590 7133 603 41 0 7549 0
vsize: 30360
[startup+860.185 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7162 0 0 0 85980 29 0 0 25 0 1 0 433378497 31088640 7136 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7590 7136 603 41 0 7549 0
vsize: 30360
[startup+870.185 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7177 0 0 0 86980 29 0 0 25 0 1 0 433378497 31252480 7151 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7630 7151 603 41 0 7589 0
vsize: 30520
[startup+880.185 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7177 0 0 0 87980 29 0 0 25 0 1 0 433378497 31252480 7151 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7630 7151 603 41 0 7589 0
vsize: 30520
[startup+890.186 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7221 0 0 0 88979 30 0 0 25 0 1 0 433378497 31387648 7195 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7195 603 41 0 7622 0
vsize: 30652
[startup+900.185 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7221 0 0 0 89979 30 0 0 25 0 1 0 433378497 31387648 7195 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7195 603 41 0 7622 0
vsize: 30652
[startup+910.185 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7221 0 0 0 90980 30 0 0 25 0 1 0 433378497 31387648 7195 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7195 603 41 0 7622 0
vsize: 30652
[startup+920.186 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7227 0 0 0 91980 30 0 0 25 0 1 0 433378497 31387648 7201 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7201 603 41 0 7622 0
vsize: 30652
[startup+930.187 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7227 0 0 0 92980 30 0 0 25 0 1 0 433378497 31387648 7201 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7201 603 41 0 7622 0
vsize: 30652
[startup+940.187 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7227 0 0 0 93980 30 0 0 25 0 1 0 433378497 31387648 7201 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7663 7201 603 41 0 7622 0
vsize: 30652
[startup+950.187 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7278 0 0 0 94980 30 0 0 25 0 1 0 433378497 31653888 7252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7728 7252 603 41 0 7687 0
vsize: 30912
[startup+960.187 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7608 0 0 0 95979 32 0 0 25 0 1 0 433378497 32997376 7582 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8056 7582 603 41 0 8015 0
vsize: 32224
[startup+970.188 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 7944 0 0 0 96978 32 0 0 25 0 1 0 433378497 34340864 7918 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8384 7918 603 41 0 8343 0
vsize: 33536
[startup+980.188 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 97977 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+990.189 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 98977 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+1000.19 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 99977 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+1010.19 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 100977 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+1020.19 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 101977 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+1030.19 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 102977 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+1040.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 103978 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+1050.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 104978 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+1060.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8209 0 0 0 105978 34 0 0 25 0 1 0 433378497 35409920 8183 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8183 603 41 0 8604 0
vsize: 34580
[startup+1070.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8215 0 0 0 106978 34 0 0 25 0 1 0 433378497 35409920 8189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 8189 603 41 0 8604 0
vsize: 34580
[startup+1080.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8215 0 0 0 107978 34 0 0 25 0 1 0 433378497 35409920 8189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 8189 603 41 0 8604 0
vsize: 34580
[startup+1090.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8215 0 0 0 108979 34 0 0 25 0 1 0 433378497 35409920 8189 4294967295 134512640 134672761 3221224624 3221223792 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 8189 603 41 0 8604 0
vsize: 34580
[startup+1100.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8215 0 0 0 109979 34 0 0 25 0 1 0 433378497 35409920 8189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 8189 603 41 0 8604 0
vsize: 34580
[startup+1110.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8215 0 0 0 110979 34 0 0 25 0 1 0 433378497 35409920 8189 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8189 603 41 0 8604 0
vsize: 34580
[startup+1120.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8215 0 0 0 111979 34 0 0 25 0 1 0 433378497 35409920 8189 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8189 603 41 0 8604 0
vsize: 34580
[startup+1130.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8215 0 0 0 112979 35 0 0 25 0 1 0 433378497 35409920 8189 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8189 603 41 0 8604 0
vsize: 34580
[startup+1140.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8215 0 0 0 113980 35 0 0 25 0 1 0 433378497 35409920 8189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8189 603 41 0 8604 0
vsize: 34580
[startup+1150.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4789
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8217 0 0 0 114980 35 0 0 25 0 1 0 433378497 35409920 8191 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 8191 603 41 0 8604 0
vsize: 34580
[startup+1160.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4791
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8221 0 0 0 115979 35 0 0 25 0 1 0 433378497 35672064 8195 4294967295 134512640 134672761 3221224624 3221223728 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8709 8195 603 41 0 8668 0
vsize: 34836
[startup+1170.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4791
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8221 0 0 0 116979 35 0 0 25 0 1 0 433378497 35672064 8195 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8709 8195 603 41 0 8668 0
vsize: 34836
[startup+1180.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4791
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8222 0 0 0 117980 35 0 0 25 0 1 0 433378497 35672064 8196 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8709 8196 603 41 0 8668 0
vsize: 34836
[startup+1190.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4791
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8222 0 0 0 118980 35 0 0 25 0 1 0 433378497 35672064 8196 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8709 8196 603 41 0 8668 0
vsize: 34836
[startup+1200.2 s]
Raw data (loadavg): 0.99 1.00 0.92 2/56 4791
Raw data (stat): 4726 (minisat+) R 4725 12452 12451 0 -1 0 8222 0 0 0 119980 35 0 0 25 0 1 0 433378497 35672064 8196 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8709 8196 603 41 0 8668 0
vsize: 34836
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 0.99 1.00 0.92 1/56 4791
Raw data (stat): 4726 (minisat+) Z 4725 12452 12451 0 -1 12 8225 0 0 0 119980 37 0 0 25 0 1 0 433378497 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.22
CPU time (s): 1200.18
CPU user time (s): 1199.81
CPU system time (s): 0.372943
CPU usage (%): 99.9966
Max. virtual memory (Kb): 34836
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####