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 5004

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 21:12:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2282 boxname=wulflinc31 idbench=254 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  fa7153262db792d01bec14f5a651af5b  /oldhome/oroussel/tmp/wulflinc31/normalized-mux.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-mux.opb
IDLAUNCH: 2282
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        912164 kB
Buffers:         34592 kB
Cached:          49472 kB
SwapCached:        392 kB
Active:          45924 kB
Inactive:        41364 kB
HighTotal:      131008 kB
HighFree:        77784 kB
LowTotal:       903652 kB
LowFree:        834380 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29620 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:32:57 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 2282 7 1200.17 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     527     2331 |     175       0        0     nan |  0.000 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71948   169106 |   23982       0        0     nan |  0.000 % |
c |       100 |   71806   168786 |   26380      99     2955    29.8 |  0.129 % |
c |       251 |   71806   168786 |   29018     250     6809    27.2 |  0.129 % |
c |       477 |   71373   167811 |   31920     472    10592    22.4 |  0.579 % |
c ==============================================================================
c [1mFound solution: 1234[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:24283     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       513 |  131893   309118 |   43964     507    11929    23.5 |  0.579 % |
c |       614 |  131893   309118 |   48360     608    14630    24.1 |  0.337 % |
c |       765 |  131893   309118 |   53196     759    16948    22.3 |  0.337 % |
c |       990 |  131893   309118 |   58516     984    20452    20.8 |  0.337 % |
c |      1327 |  131793   308891 |   64367    1316    29130    22.1 |  0.398 % |
c |      1833 |  131793   308891 |   70804    1822    42478    23.3 |  0.398 % |
c |      2592 |  131771   308841 |   77884    2580    60031    23.3 |  0.409 % |
c |      3733 |  131637   308542 |   85673    3717    88874    23.9 |  0.482 % |
c ==============================================================================
c [1mFound solution: 1233[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4682 |  131826   309294 |   43942    4666   147647    31.6 |  0.482 % |
c |      4783 |  131826   309294 |   48336    4767   149006    31.3 |  0.483 % |
c ==============================================================================
c [1mFound solution: 1199[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4810 |  132099   309958 |   44033    4794   152722    31.9 |  0.483 % |
c |      4910 |  132099   309958 |   48436    4894   157309    32.1 |  0.484 % |
c |      5060 |  132099   309958 |   53279    5044   166454    33.0 |  0.484 % |
c |      5285 |  132099   309958 |   58607    5269   177805    33.7 |  0.484 % |
c |      5622 |  132099   309958 |   64468    5606   190601    34.0 |  0.484 % |
c |      6128 |  131993   309729 |   70915    6108   202232    33.1 |  0.557 % |
c |      6889 |  131993   309729 |   78007    6869   218880    31.9 |  0.557 % |
c |      8029 |  131989   309720 |   85807    8008   393024    49.1 |  0.559 % |
c |      9737 |  131989   309720 |   94388    9716   464106    47.8 |  0.559 % |
c |     12300 |  131949   309629 |  103827   12275   614249    50.0 |  0.586 % |
c ==============================================================================
c [1mFound solution: 1196[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15838 |  132219   310293 |   44073   15813  1409395    89.1 |  0.586 % |
c |     15939 |  132219   310293 |   48480   15914  1410776    88.6 |  0.588 % |
c |     16089 |  132219   310293 |   53328   16064  1413959    88.0 |  0.588 % |
c |     16316 |  132219   310293 |   58661   16291  1420583    87.2 |  0.588 % |
c |     16653 |  132219   310293 |   64527   16628  1424998    85.7 |  0.588 % |
c |     17160 |  132219   310293 |   70980   17135  1431067    83.5 |  0.588 % |
c |     17920 |  132219   310293 |   78078   17895  1444512    80.7 |  0.588 % |
c |     19059 |  132219   310293 |   85885   19034  1508888    79.3 |  0.588 % |
c |     20768 |  132219   310293 |   94474   20743  1585879    76.5 |  0.588 % |
c |     23330 |  132219   310293 |  103921   23305  1683334    72.2 |  0.588 % |
c |     27176 |  132219   310293 |  114314   27151  1841999    67.8 |  0.588 % |
c |     32944 |  132219   310293 |  125745   32919  2133960    64.8 |  0.588 % |
c |     41593 |  132219   310293 |  138319   41568  2548271    61.3 |  0.588 % |
c |     54567 |  132219   310293 |  152151   54542  3221898    59.1 |  0.588 % |
c |     74029 |  132219   310293 |  167367   74004  4058574    54.8 |  0.588 % |
c |    103224 |  132219   310293 |  184103  103199  5283147    51.2 |  0.588 % |
#### 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.90 0.95 0.91 2/54 25850
Raw data (stat): 25850 (runsolver) R 25849 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479086129 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99986 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 4331 0 0 0 989 9 0 0 25 0 1 0 479086129 20729856 4167 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5061 4167 603 41 0 5020 0
vsize: 20244
[startup+20.0011 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 4422 0 0 0 1988 9 0 0 25 0 1 0 479086129 20996096 4258 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5126 4258 603 41 0 5085 0
vsize: 20504
[startup+30.0021 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 4616 0 0 0 2987 10 0 0 25 0 1 0 479086129 21786624 4448 4294967295 134512640 134672761 3221224640 3221223808 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5319 4448 603 41 0 5278 0
vsize: 21276
[startup+40.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 4636 0 0 0 3987 10 0 0 25 0 1 0 479086129 21917696 4468 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5351 4468 603 41 0 5310 0
vsize: 21404
[startup+50.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 4826 0 0 0 4986 11 0 0 25 0 1 0 479086129 22728704 4658 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5549 4658 603 41 0 5508 0
vsize: 22196
[startup+60.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 4900 0 0 0 5986 12 0 0 25 0 1 0 479086129 22990848 4732 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5613 4732 603 41 0 5572 0
vsize: 22452
[startup+70.0038 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 5020 0 0 0 6985 13 0 0 25 0 1 0 479086129 23523328 4852 4294967295 134512640 134672761 3221224640 3221223840 134557806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5743 4852 603 41 0 5702 0
vsize: 22972
[startup+80.0055 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 5119 0 0 0 7984 13 0 0 25 0 1 0 479086129 23924736 4951 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5841 4951 603 41 0 5800 0
vsize: 23364
[startup+90.0062 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 5398 0 0 0 8983 14 0 0 25 0 1 0 479086129 24985600 5230 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6100 5230 603 41 0 6059 0
vsize: 24400
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 5668 0 0 0 9982 15 0 0 25 0 1 0 479086129 26181632 5500 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6392 5500 603 41 0 6351 0
vsize: 25568
[startup+110.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 5952 0 0 0 10980 17 0 0 25 0 1 0 479086129 27250688 5784 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6653 5784 603 41 0 6612 0
vsize: 26612
[startup+120.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 5989 0 0 0 11980 17 0 0 25 0 1 0 479086129 27492352 5821 4294967295 134512640 134672761 3221224640 3221223784 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6712 5821 603 41 0 6671 0
vsize: 26848
[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6052 0 0 0 12979 18 0 0 25 0 1 0 479086129 27762688 5884 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6778 5884 603 41 0 6737 0
vsize: 27112
[startup+140.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6132 0 0 0 13979 19 0 0 25 0 1 0 479086129 28028928 5964 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6843 5964 603 41 0 6802 0
vsize: 27372
[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6198 0 0 0 14978 19 0 0 25 0 1 0 479086129 28299264 6030 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6030 603 41 0 6868 0
vsize: 27636
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6264 0 0 0 15977 20 0 0 25 0 1 0 479086129 28565504 6096 4294967295 134512640 134672761 3221224640 3221223840 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6096 603 41 0 6933 0
vsize: 27896
[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6339 0 0 0 16976 21 0 0 25 0 1 0 479086129 28966912 6171 4294967295 134512640 134672761 3221224640 3221223840 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7072 6171 603 41 0 7031 0
vsize: 28288
[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6419 0 0 0 17975 22 0 0 25 0 1 0 479086129 29229056 6251 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7136 6251 603 41 0 7095 0
vsize: 28544
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6491 0 0 0 18974 23 0 0 25 0 1 0 479086129 29491200 6323 4294967295 134512640 134672761 3221224640 3221223824 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7200 6323 603 41 0 7159 0
vsize: 28800
[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6553 0 0 0 19974 23 0 0 25 0 1 0 479086129 29757440 6385 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7265 6385 603 41 0 7224 0
vsize: 29060
[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6620 0 0 0 20973 23 0 0 25 0 1 0 479086129 30023680 6452 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7330 6452 603 41 0 7289 0
vsize: 29320
[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6684 0 0 0 21973 24 0 0 25 0 1 0 479086129 30289920 6516 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7395 6516 603 41 0 7354 0
vsize: 29580
[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6756 0 0 0 22972 25 0 0 25 0 1 0 479086129 30560256 6588 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7461 6588 603 41 0 7420 0
vsize: 29844
[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6828 0 0 0 23971 25 0 0 25 0 1 0 479086129 30953472 6660 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7557 6660 603 41 0 7516 0
vsize: 30228
[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6872 0 0 0 24971 26 0 0 25 0 1 0 479086129 31219712 6704 4294967295 134512640 134672761 3221224640 3221223744 134559905 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7622 6704 603 41 0 7581 0
vsize: 30488
[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 6934 0 0 0 25970 26 0 0 25 0 1 0 479086129 31481856 6766 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7686 6766 603 41 0 7645 0
vsize: 30744
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7002 0 0 0 26970 27 0 0 25 0 1 0 479086129 31744000 6834 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7750 6834 603 41 0 7709 0
vsize: 31000
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7065 0 0 0 27969 28 0 0 25 0 1 0 479086129 32006144 6897 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7814 6897 603 41 0 7773 0
vsize: 31256
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7129 0 0 0 28968 29 0 0 25 0 1 0 479086129 32272384 6961 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7879 6961 603 41 0 7838 0
vsize: 31516
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7189 0 0 0 29968 29 0 0 25 0 1 0 479086129 32403456 7021 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7911 7021 603 41 0 7870 0
vsize: 31644
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7246 0 0 0 30968 29 0 0 25 0 1 0 479086129 32665600 7078 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7975 7078 603 41 0 7934 0
vsize: 31900
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7299 0 0 0 31968 29 0 0 25 0 1 0 479086129 32931840 7131 4294967295 134512640 134672761 3221224640 3221223776 134560606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8040 7131 603 41 0 7999 0
vsize: 32160
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7380 0 0 0 32968 29 0 0 25 0 1 0 479086129 33198080 7212 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8105 7212 603 41 0 8064 0
vsize: 32420
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7452 0 0 0 33968 29 0 0 25 0 1 0 479086129 33460224 7284 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8169 7284 603 41 0 8128 0
vsize: 32676
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7521 0 0 0 34968 30 0 0 25 0 1 0 479086129 33730560 7353 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8235 7353 603 41 0 8194 0
vsize: 32940
[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7587 0 0 0 35968 30 0 0 25 0 1 0 479086129 33992704 7419 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7419 603 41 0 8258 0
vsize: 33196
[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7665 0 0 0 36968 30 0 0 25 0 1 0 479086129 34394112 7497 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8397 7497 603 41 0 8356 0
vsize: 33588
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7743 0 0 0 37968 31 0 0 25 0 1 0 479086129 34660352 7575 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8462 7575 603 41 0 8421 0
vsize: 33848
[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7816 0 0 0 38967 31 0 0 25 0 1 0 479086129 34926592 7648 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8527 7648 603 41 0 8486 0
vsize: 34108
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7888 0 0 0 39967 31 0 0 25 0 1 0 479086129 35328000 7720 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8625 7720 603 41 0 8584 0
vsize: 34500
[startup+410.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 7951 0 0 0 40967 32 0 0 25 0 1 0 479086129 35459072 7783 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8657 7783 603 41 0 8616 0
vsize: 34628
[startup+420.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8021 0 0 0 41967 32 0 0 25 0 1 0 479086129 35852288 7853 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8753 7853 603 41 0 8712 0
vsize: 35012
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8079 0 0 0 42967 32 0 0 25 0 1 0 479086129 35983360 7911 4294967295 134512640 134672761 3221224640 3221223812 134559125 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8785 7911 603 41 0 8744 0
vsize: 35140
[startup+440.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8141 0 0 0 43967 32 0 0 25 0 1 0 479086129 36249600 7973 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8850 7973 603 41 0 8809 0
vsize: 35400
[startup+450.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8203 0 0 0 44966 33 0 0 25 0 1 0 479086129 36536320 8035 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8920 8035 603 41 0 8879 0
vsize: 35680
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8273 0 0 0 45966 33 0 0 25 0 1 0 479086129 36810752 8105 4294967295 134512640 134672761 3221224640 3221223840 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8987 8105 603 41 0 8946 0
vsize: 35948
[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8322 0 0 0 46966 33 0 0 25 0 1 0 479086129 37076992 8154 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9052 8154 603 41 0 9011 0
vsize: 36208
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8368 0 0 0 47966 33 0 0 25 0 1 0 479086129 37208064 8200 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9084 8200 603 41 0 9043 0
vsize: 36336
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8412 0 0 0 48967 33 0 0 25 0 1 0 479086129 37470208 8244 4294967295 134512640 134672761 3221224640 3221223744 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9148 8244 603 41 0 9107 0
vsize: 36592
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8457 0 0 0 49967 33 0 0 25 0 1 0 479086129 37601280 8289 4294967295 134512640 134672761 3221224640 3221223744 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9180 8289 603 41 0 9139 0
vsize: 36720
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8499 0 0 0 50967 34 0 0 25 0 1 0 479086129 37732352 8331 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9212 8331 603 41 0 9171 0
vsize: 36848
[startup+520.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8556 0 0 0 51967 34 0 0 25 0 1 0 479086129 37998592 8388 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9277 8388 603 41 0 9236 0
vsize: 37108
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8609 0 0 0 52967 34 0 0 25 0 1 0 479086129 38277120 8441 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9345 8441 603 41 0 9304 0
vsize: 37380
[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8665 0 0 0 53967 34 0 0 25 0 1 0 479086129 38408192 8497 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9377 8497 603 41 0 9336 0
vsize: 37508
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8714 0 0 0 54967 35 0 0 25 0 1 0 479086129 38674432 8546 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9442 8546 603 41 0 9401 0
vsize: 37768
[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8772 0 0 0 55966 35 0 0 25 0 1 0 479086129 38936576 8604 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9506 8604 603 41 0 9465 0
vsize: 38024
[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8818 0 0 0 56967 35 0 0 25 0 1 0 479086129 39329792 8650 4294967295 134512640 134672761 3221224640 3221223744 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9602 8650 603 41 0 9561 0
vsize: 38408
[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8861 0 0 0 57967 35 0 0 25 0 1 0 479086129 39464960 8693 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9635 8693 603 41 0 9594 0
vsize: 38540
[startup+590.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8912 0 0 0 58967 35 0 0 25 0 1 0 479086129 39731200 8744 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9700 8744 603 41 0 9659 0
vsize: 38800
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 8955 0 0 0 59967 35 0 0 25 0 1 0 479086129 39870464 8787 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9734 8787 603 41 0 9693 0
vsize: 38936
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9001 0 0 0 60967 36 0 0 25 0 1 0 479086129 40157184 8833 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9804 8833 603 41 0 9763 0
vsize: 39216
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9041 0 0 0 61967 36 0 0 25 0 1 0 479086129 40288256 8873 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9836 8873 603 41 0 9795 0
vsize: 39344
[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9089 0 0 0 62967 36 0 0 25 0 1 0 479086129 40431616 8921 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9871 8921 603 41 0 9830 0
vsize: 39484
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9145 0 0 0 63967 36 0 0 25 0 1 0 479086129 40693760 8977 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9935 8977 603 41 0 9894 0
vsize: 39740
[startup+650.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9192 0 0 0 64967 37 0 0 25 0 1 0 479086129 40824832 9024 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9967 9024 603 41 0 9926 0
vsize: 39868
[startup+660.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9234 0 0 0 65966 37 0 0 25 0 1 0 479086129 41086976 9066 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10031 9066 603 41 0 9990 0
vsize: 40124
[startup+670.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9292 0 0 0 66965 37 0 0 25 0 1 0 479086129 41238528 9124 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10068 9124 603 41 0 10027 0
vsize: 40272
[startup+680.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9342 0 0 0 67965 37 0 0 25 0 1 0 479086129 41504768 9174 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10133 9174 603 41 0 10092 0
vsize: 40532
[startup+690.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9395 0 0 0 68966 37 0 0 25 0 1 0 479086129 41639936 9227 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10166 9227 603 41 0 10125 0
vsize: 40664
[startup+700.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9442 0 0 0 69965 38 0 0 25 0 1 0 479086129 41922560 9274 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10235 9274 603 41 0 10194 0
vsize: 40940
[startup+710.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9492 0 0 0 70965 38 0 0 25 0 1 0 479086129 42188800 9324 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10300 9324 603 41 0 10259 0
vsize: 41200
[startup+720.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9550 0 0 0 71966 38 0 0 25 0 1 0 479086129 42319872 9382 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10332 9382 603 41 0 10291 0
vsize: 41328
[startup+730.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9601 0 0 0 72966 38 0 0 25 0 1 0 479086129 42586112 9433 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10397 9433 603 41 0 10356 0
vsize: 41588
[startup+740.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9640 0 0 0 73966 38 0 0 25 0 1 0 479086129 42717184 9472 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10429 9472 603 41 0 10388 0
vsize: 41716
[startup+750.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9693 0 0 0 74966 39 0 0 25 0 1 0 479086129 42983424 9525 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10494 9525 603 41 0 10453 0
vsize: 41976
[startup+760.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9738 0 0 0 75967 39 0 0 25 0 1 0 479086129 43118592 9570 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10527 9570 603 41 0 10486 0
vsize: 42108
[startup+770.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9783 0 0 0 76967 39 0 0 25 0 1 0 479086129 43249664 9615 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10559 9615 603 41 0 10518 0
vsize: 42236
[startup+780.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9838 0 0 0 77967 39 0 0 25 0 1 0 479086129 43511808 9670 4294967295 134512640 134672761 3221224640 3221223736 1075347361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10623 9670 603 41 0 10582 0
vsize: 42492
[startup+790.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9893 0 0 0 78967 39 0 0 25 0 1 0 479086129 43802624 9725 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10694 9725 603 41 0 10653 0
vsize: 42776
[startup+800.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9943 0 0 0 79967 39 0 0 25 0 1 0 479086129 43991040 9775 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10740 9775 603 41 0 10699 0
vsize: 42960
[startup+810.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 9987 0 0 0 80967 39 0 0 25 0 1 0 479086129 44122112 9819 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10772 9819 603 41 0 10731 0
vsize: 43088
[startup+820.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10051 0 0 0 81967 39 0 0 25 0 1 0 479086129 44396544 9883 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 9883 603 41 0 10798 0
vsize: 43356
[startup+830.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10092 0 0 0 82967 40 0 0 25 0 1 0 479086129 44593152 9924 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10887 9924 603 41 0 10846 0
vsize: 43548
[startup+840.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10159 0 0 0 83967 40 0 0 25 0 1 0 479086129 44920832 9991 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10967 9991 603 41 0 10926 0
vsize: 43868
[startup+850.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10208 0 0 0 84967 40 0 0 25 0 1 0 479086129 45191168 10040 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11033 10040 603 41 0 10992 0
vsize: 44132
[startup+860.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10237 0 0 0 85967 40 0 0 25 0 1 0 479086129 45326336 10069 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11066 10069 603 41 0 11025 0
vsize: 44264
[startup+870.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10270 0 0 0 86967 40 0 0 25 0 1 0 479086129 45461504 10102 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11099 10102 603 41 0 11058 0
vsize: 44396
[startup+880.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10307 0 0 0 87967 40 0 0 25 0 1 0 479086129 45592576 10139 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10139 603 41 0 11090 0
vsize: 44524
[startup+890.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10351 0 0 0 88967 40 0 0 25 0 1 0 479086129 45723648 10183 4294967295 134512640 134672761 3221224640 3221223744 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11163 10183 603 41 0 11122 0
vsize: 44652
[startup+900.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10392 0 0 0 89968 41 0 0 25 0 1 0 479086129 45854720 10224 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11195 10224 603 41 0 11154 0
vsize: 44780
[startup+910.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10433 0 0 0 90968 41 0 0 25 0 1 0 479086129 46120960 10265 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11260 10265 603 41 0 11219 0
vsize: 45040
[startup+920.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10481 0 0 0 91968 41 0 0 25 0 1 0 479086129 46252032 10313 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10313 603 41 0 11251 0
vsize: 45168
[startup+930.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10520 0 0 0 92968 41 0 0 25 0 1 0 479086129 46383104 10352 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11324 10352 603 41 0 11283 0
vsize: 45296
[startup+940.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10558 0 0 0 93968 41 0 0 25 0 1 0 479086129 46514176 10390 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11356 10390 603 41 0 11315 0
vsize: 45424
[startup+950.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10595 0 0 0 94968 41 0 0 25 0 1 0 479086129 46776320 10427 4294967295 134512640 134672761 3221224640 3221223840 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11420 10427 603 41 0 11379 0
vsize: 45680
[startup+960.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10627 0 0 0 95968 41 0 0 25 0 1 0 479086129 46907392 10459 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11452 10459 603 41 0 11411 0
vsize: 45808
[startup+970.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10664 0 0 0 96968 41 0 0 25 0 1 0 479086129 47038464 10496 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11484 10496 603 41 0 11443 0
vsize: 45936
[startup+980.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10703 0 0 0 97968 41 0 0 25 0 1 0 479086129 47169536 10535 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11516 10535 603 41 0 11475 0
vsize: 46064
[startup+990.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10741 0 0 0 98968 41 0 0 25 0 1 0 479086129 47300608 10573 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11548 10573 603 41 0 11507 0
vsize: 46192
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10809 0 0 0 99968 42 0 0 25 0 1 0 479086129 47611904 10641 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11624 10641 603 41 0 11583 0
vsize: 46496
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10859 0 0 0 100968 42 0 0 25 0 1 0 479086129 47878144 10691 4294967295 134512640 134672761 3221224640 3221223776 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11689 10691 603 41 0 11648 0
vsize: 46756
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10907 0 0 0 101968 42 0 0 25 0 1 0 479086129 48009216 10739 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11721 10739 603 41 0 11680 0
vsize: 46884
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10950 0 0 0 102968 42 0 0 25 0 1 0 479086129 48144384 10782 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11754 10782 603 41 0 11713 0
vsize: 47016
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 10991 0 0 0 103968 42 0 0 25 0 1 0 479086129 48406528 10823 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11818 10823 603 41 0 11777 0
vsize: 47272
[startup+1050.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11027 0 0 0 104968 42 0 0 25 0 1 0 479086129 48537600 10859 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11850 10859 603 41 0 11809 0
vsize: 47400
[startup+1060.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11071 0 0 0 105969 42 0 0 25 0 1 0 479086129 48689152 10903 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11887 10903 603 41 0 11846 0
vsize: 47548
[startup+1070.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11113 0 0 0 106969 42 0 0 25 0 1 0 479086129 48820224 10945 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11919 10945 603 41 0 11878 0
vsize: 47676
[startup+1080.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11165 0 0 0 107968 43 0 0 25 0 1 0 479086129 49082368 10997 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11983 10997 603 41 0 11942 0
vsize: 47932
[startup+1090.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11196 0 0 0 108969 43 0 0 25 0 1 0 479086129 49213440 11028 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12015 11028 603 41 0 11974 0
vsize: 48060
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11230 0 0 0 109969 43 0 0 25 0 1 0 479086129 49438720 11062 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12070 11062 603 41 0 12029 0
vsize: 48280
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11268 0 0 0 110969 43 0 0 25 0 1 0 479086129 49577984 11100 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12104 11100 603 41 0 12063 0
vsize: 48416
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11302 0 0 0 111969 43 0 0 25 0 1 0 479086129 49709056 11134 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12136 11134 603 41 0 12095 0
vsize: 48544
[startup+1130.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11339 0 0 0 112969 43 0 0 25 0 1 0 479086129 49840128 11171 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12168 11171 603 41 0 12127 0
vsize: 48672
[startup+1140.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11377 0 0 0 113969 44 0 0 25 0 1 0 479086129 49971200 11209 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12200 11209 603 41 0 12159 0
vsize: 48800
[startup+1150.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11436 0 0 0 114969 44 0 0 25 0 1 0 479086129 50368512 11268 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12297 11268 603 41 0 12256 0
vsize: 49188
[startup+1160.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11466 0 0 0 115969 44 0 0 25 0 1 0 479086129 50544640 11298 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12340 11298 603 41 0 12299 0
vsize: 49360
[startup+1170.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11500 0 0 0 116969 44 0 0 25 0 1 0 479086129 50724864 11332 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12384 11332 603 41 0 12343 0
vsize: 49536
[startup+1180.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11534 0 0 0 117969 44 0 0 25 0 1 0 479086129 50860032 11366 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12417 11366 603 41 0 12376 0
vsize: 49668
[startup+1190.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11569 0 0 0 118970 44 0 0 25 0 1 0 479086129 50991104 11401 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12449 11401 603 41 0 12408 0
vsize: 49796
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25850
Raw data (stat): 25850 (minisat+) R 25849 23176 23175 0 -1 0 11606 0 0 0 119970 44 0 0 25 0 1 0 479086129 51122176 11438 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12481 11438 603 41 0 12440 0
vsize: 49924
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25850
Raw data (stat): 25850 (minisat+) Z 25849 23176 23175 0 -1 12 11609 0 0 0 119970 46 0 0 25 0 1 0 479086129 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.1
CPU time (s): 1200.17
CPU user time (s): 1199.7
CPU system time (s): 0.467928
CPU usage (%): 100.006
Max. virtual memory (Kb): 49924
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####