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 5968

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 02:32:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4390 boxname=wulflinc15 idbench=254 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fa7153262db792d01bec14f5a651af5b  /oldhome/oroussel/tmp/wulflinc15/normalized-mux.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-mux.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mux.opb
IDLAUNCH: 4390
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        899100 kB
Buffers:         36536 kB
Cached:          77464 kB
SwapCached:       2144 kB
Active:          64108 kB
Inactive:        54936 kB
HighTotal:      131008 kB
HighFree:        49616 kB
LowTotal:       903652 kB
LowFree:        849484 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10944 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:52:39 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4390 7 1200.24 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.84 0.94 0.91 2/54 3845
Raw data (stat): 3845 (runsolver) R 3844 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422793133 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99993 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 4336 0 0 0 986 11 0 0 25 0 1 0 422793133 20729856 4168 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5061 4168 603 41 0 5020 0
vsize: 20244
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 4430 0 0 0 1986 12 0 0 25 0 1 0 422793133 20996096 4262 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5126 4262 603 41 0 5085 0
vsize: 20504
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 4578 0 0 0 2985 12 0 0 25 0 1 0 422793133 21651456 4406 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5286 4406 603 41 0 5245 0
vsize: 21144
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 4625 0 0 0 3984 13 0 0 25 0 1 0 422793133 21921792 4453 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5352 4453 603 41 0 5311 0
vsize: 21408
[startup+50.0035 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 4818 0 0 0 4984 13 0 0 25 0 1 0 422793133 22589440 4646 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5515 4646 603 41 0 5474 0
vsize: 22060
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 4891 0 0 0 5984 14 0 0 25 0 1 0 422793133 22986752 4719 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5612 4719 603 41 0 5571 0
vsize: 22448
[startup+70.0039 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 5020 0 0 0 6983 14 0 0 25 0 1 0 422793133 23515136 4848 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5741 4848 603 41 0 5700 0
vsize: 22964
[startup+80.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 5136 0 0 0 7983 15 0 0 25 0 1 0 422793133 23920640 4964 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5840 4964 603 41 0 5799 0
vsize: 23360
[startup+90.0048 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 5417 0 0 0 8982 15 0 0 25 0 1 0 422793133 25124864 5245 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6134 5245 603 41 0 6093 0
vsize: 24536
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 5696 0 0 0 9981 16 0 0 25 0 1 0 422793133 26320896 5524 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6426 5524 603 41 0 6385 0
vsize: 25704
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 5925 0 0 0 10980 18 0 0 25 0 1 0 422793133 27324416 5753 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 5753 603 41 0 6630 0
vsize: 26684
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 5985 0 0 0 11980 18 0 0 25 0 1 0 422793133 27455488 5813 4294967295 134512640 134672761 3221224560 3221223696 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6703 5813 603 41 0 6662 0
vsize: 26812
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6053 0 0 0 12980 18 0 0 25 0 1 0 422793133 27721728 5881 4294967295 134512640 134672761 3221224560 3221223696 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6768 5881 603 41 0 6727 0
vsize: 27072
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6136 0 0 0 13980 19 0 0 25 0 1 0 422793133 28114944 5964 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6864 5964 603 41 0 6823 0
vsize: 27456
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6201 0 0 0 14980 19 0 0 25 0 1 0 422793133 28381184 6029 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6929 6029 603 41 0 6888 0
vsize: 27716
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6271 0 0 0 15980 19 0 0 25 0 1 0 422793133 28643328 6099 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6993 6099 603 41 0 6952 0
vsize: 27972
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6346 0 0 0 16980 19 0 0 25 0 1 0 422793133 28905472 6174 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7057 6174 603 41 0 7016 0
vsize: 28228
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6432 0 0 0 17980 20 0 0 25 0 1 0 422793133 29306880 6260 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7155 6260 603 41 0 7114 0
vsize: 28620
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6496 0 0 0 18980 20 0 0 25 0 1 0 422793133 29569024 6324 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7219 6324 603 41 0 7178 0
vsize: 28876
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6563 0 0 0 19980 20 0 0 25 0 1 0 422793133 29831168 6391 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7283 6391 603 41 0 7242 0
vsize: 29132
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6626 0 0 0 20980 20 0 0 25 0 1 0 422793133 30089216 6454 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7346 6454 603 41 0 7305 0
vsize: 29384
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6698 0 0 0 21980 20 0 0 25 0 1 0 422793133 30351360 6526 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7410 6526 603 41 0 7369 0
vsize: 29640
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6773 0 0 0 22979 21 0 0 25 0 1 0 422793133 30613504 6601 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7474 6601 603 41 0 7433 0
vsize: 29896
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6822 0 0 0 23980 21 0 0 25 0 1 0 422793133 31006720 6650 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7570 6650 603 41 0 7529 0
vsize: 30280
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6887 0 0 0 24979 21 0 0 25 0 1 0 422793133 31277056 6715 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7636 6715 603 41 0 7595 0
vsize: 30544
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 6956 0 0 0 25979 21 0 0 25 0 1 0 422793133 31551488 6784 4294967295 134512640 134672761 3221224560 3221223696 134560720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7703 6784 603 41 0 7662 0
vsize: 30812
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7023 0 0 0 26979 21 0 0 25 0 1 0 422793133 31817728 6851 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7768 6851 603 41 0 7727 0
vsize: 31072
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7090 0 0 0 27980 22 0 0 25 0 1 0 422793133 32079872 6918 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7832 6918 603 41 0 7791 0
vsize: 31328
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7149 0 0 0 28979 22 0 0 25 0 1 0 422793133 32346112 6977 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7897 6977 603 41 0 7856 0
vsize: 31588
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7209 0 0 0 29980 22 0 0 25 0 1 0 422793133 32481280 7037 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7930 7037 603 41 0 7889 0
vsize: 31720
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7263 0 0 0 30979 22 0 0 25 0 1 0 422793133 32743424 7091 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7994 7091 603 41 0 7953 0
vsize: 31976
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7338 0 0 0 31980 22 0 0 25 0 1 0 422793133 33009664 7166 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8059 7166 603 41 0 8018 0
vsize: 32236
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7412 0 0 0 32979 23 0 0 25 0 1 0 422793133 33406976 7240 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8156 7240 603 41 0 8115 0
vsize: 32624
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7475 0 0 0 33980 23 0 0 25 0 1 0 422793133 33673216 7303 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8221 7303 603 41 0 8180 0
vsize: 32884
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7551 0 0 0 34979 23 0 0 25 0 1 0 422793133 33939456 7379 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8286 7379 603 41 0 8245 0
vsize: 33144
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7623 0 0 0 35980 23 0 0 25 0 1 0 422793133 34205696 7451 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8351 7451 603 41 0 8310 0
vsize: 33404
[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7706 0 0 0 36981 23 0 0 25 0 1 0 422793133 34603008 7534 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8448 7534 603 41 0 8407 0
vsize: 33792
[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7780 0 0 0 37981 24 0 0 25 0 1 0 422793133 34873344 7608 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8514 7608 603 41 0 8473 0
vsize: 34056
[startup+390.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7853 0 0 0 38981 25 0 0 25 0 1 0 422793133 35143680 7681 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8580 7681 603 41 0 8539 0
vsize: 34320
[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7915 0 0 0 39981 25 0 0 25 0 1 0 422793133 35409920 7743 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8645 7743 603 41 0 8604 0
vsize: 34580
[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 7989 0 0 0 40981 25 0 0 25 0 1 0 422793133 35676160 7817 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 7817 603 41 0 8669 0
vsize: 34840
[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8043 0 0 0 41981 25 0 0 25 0 1 0 422793133 35942400 7871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8775 7871 603 41 0 8734 0
vsize: 35100
[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8112 0 0 0 42981 25 0 0 25 0 1 0 422793133 36212736 7940 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8841 7940 603 41 0 8800 0
vsize: 35364
[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8174 0 0 0 43981 25 0 0 25 0 1 0 422793133 36507648 8002 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8913 8002 603 41 0 8872 0
vsize: 35652
[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8243 0 0 0 44979 26 0 0 25 0 1 0 422793133 36810752 8071 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8987 8071 603 41 0 8946 0
vsize: 35948
[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8295 0 0 0 45980 26 0 0 25 0 1 0 422793133 36941824 8123 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9019 8123 603 41 0 8978 0
vsize: 36076
[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8343 0 0 0 46980 26 0 0 25 0 1 0 422793133 37203968 8171 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9083 8171 603 41 0 9042 0
vsize: 36332
[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8389 0 0 0 47980 27 0 0 25 0 1 0 422793133 37335040 8217 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9115 8217 603 41 0 9074 0
vsize: 36460
[startup+490.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8438 0 0 0 48981 27 0 0 25 0 1 0 422793133 37605376 8266 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9181 8266 603 41 0 9140 0
vsize: 36724
[startup+500.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8478 0 0 0 49981 27 0 0 25 0 1 0 422793133 37736448 8306 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9213 8306 603 41 0 9172 0
vsize: 36852
[startup+510.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8533 0 0 0 50981 27 0 0 25 0 1 0 422793133 37998592 8361 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9277 8361 603 41 0 9236 0
vsize: 37108
[startup+520.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8588 0 0 0 51981 28 0 0 25 0 1 0 422793133 38133760 8416 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9310 8416 603 41 0 9269 0
vsize: 37240
[startup+530.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8644 0 0 0 52981 28 0 0 25 0 1 0 422793133 38400000 8472 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9375 8472 603 41 0 9334 0
vsize: 37500
[startup+540.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8694 0 0 0 53981 28 0 0 25 0 1 0 422793133 38531072 8522 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9407 8522 603 41 0 9366 0
vsize: 37628
[startup+550.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8750 0 0 0 54981 28 0 0 25 0 1 0 422793133 38797312 8578 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9472 8578 603 41 0 9431 0
vsize: 37888
[startup+560.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8798 0 0 0 55981 29 0 0 25 0 1 0 422793133 39329792 8626 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9602 8626 603 41 0 9561 0
vsize: 38408
[startup+570.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8844 0 0 0 56981 29 0 0 25 0 1 0 422793133 39460864 8672 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9634 8672 603 41 0 9593 0
vsize: 38536
[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8897 0 0 0 57981 29 0 0 25 0 1 0 422793133 39723008 8725 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9698 8725 603 41 0 9657 0
vsize: 38792
[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8940 0 0 0 58981 29 0 0 25 0 1 0 422793133 39854080 8768 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9730 8768 603 41 0 9689 0
vsize: 38920
[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 8984 0 0 0 59981 30 0 0 25 0 1 0 422793133 39985152 8812 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9762 8812 603 41 0 9721 0
vsize: 39048
[startup+610.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9023 0 0 0 60981 30 0 0 25 0 1 0 422793133 40251392 8851 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9827 8851 603 41 0 9786 0
vsize: 39308
[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9073 0 0 0 61981 30 0 0 25 0 1 0 422793133 40386560 8901 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9860 8901 603 41 0 9819 0
vsize: 39440
[startup+630.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9131 0 0 0 62981 30 0 0 25 0 1 0 422793133 40656896 8959 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9926 8959 603 41 0 9885 0
vsize: 39704
[startup+640.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9178 0 0 0 63981 30 0 0 25 0 1 0 422793133 40787968 9006 4294967295 134512640 134672761 3221224560 3221223744 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9958 9006 603 41 0 9917 0
vsize: 39832
[startup+650.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9220 0 0 0 64981 30 0 0 25 0 1 0 422793133 41050112 9048 4294967295 134512640 134672761 3221224560 3221223728 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10022 9048 603 41 0 9981 0
vsize: 40088
[startup+660.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9280 0 0 0 65980 31 0 0 25 0 1 0 422793133 41197568 9108 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10058 9108 603 41 0 10017 0
vsize: 40232
[startup+670.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9332 0 0 0 66980 31 0 0 25 0 1 0 422793133 41463808 9160 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10123 9160 603 41 0 10082 0
vsize: 40492
[startup+680.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9385 0 0 0 67980 31 0 0 25 0 1 0 422793133 41725952 9213 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 9213 603 41 0 10146 0
vsize: 40748
[startup+690.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9433 0 0 0 68979 32 0 0 25 0 1 0 422793133 41881600 9261 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10225 9261 603 41 0 10184 0
vsize: 40900
[startup+700.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9486 0 0 0 69979 32 0 0 25 0 1 0 422793133 42143744 9314 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10289 9314 603 41 0 10248 0
vsize: 41156
[startup+710.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9542 0 0 0 70979 32 0 0 25 0 1 0 422793133 42409984 9370 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10354 9370 603 41 0 10313 0
vsize: 41416
[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9590 0 0 0 71979 32 0 0 25 0 1 0 422793133 42541056 9418 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10386 9418 603 41 0 10345 0
vsize: 41544
[startup+730.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9635 0 0 0 72979 32 0 0 25 0 1 0 422793133 42676224 9463 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10419 9463 603 41 0 10378 0
vsize: 41676
[startup+740.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9690 0 0 0 73979 33 0 0 25 0 1 0 422793133 42938368 9518 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10483 9518 603 41 0 10442 0
vsize: 41932
[startup+750.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9729 0 0 0 74979 33 0 0 25 0 1 0 422793133 43073536 9557 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10516 9557 603 41 0 10475 0
vsize: 42064
[startup+760.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9781 0 0 0 75979 33 0 0 25 0 1 0 422793133 43339776 9609 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10581 9609 603 41 0 10540 0
vsize: 42324
[startup+770.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9841 0 0 0 76979 33 0 0 25 0 1 0 422793133 43626496 9669 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10651 9669 603 41 0 10610 0
vsize: 42604
[startup+780.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9890 0 0 0 77979 33 0 0 25 0 1 0 422793133 43757568 9718 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10683 9718 603 41 0 10642 0
vsize: 42732
[startup+790.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9939 0 0 0 78979 34 0 0 25 0 1 0 422793133 43945984 9767 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10729 9767 603 41 0 10688 0
vsize: 42916
[startup+800.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 9986 0 0 0 79980 34 0 0 25 0 1 0 422793133 44208128 9814 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10793 9814 603 41 0 10752 0
vsize: 43172
[startup+810.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10045 0 0 0 80980 34 0 0 25 0 1 0 422793133 44351488 9873 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10828 9873 603 41 0 10787 0
vsize: 43312
[startup+820.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10108 0 0 0 81980 34 0 0 25 0 1 0 422793133 44687360 9936 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10910 9936 603 41 0 10869 0
vsize: 43640
[startup+830.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10159 0 0 0 82979 34 0 0 25 0 1 0 422793133 45015040 9987 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10990 9987 603 41 0 10949 0
vsize: 43960
[startup+840.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10201 0 0 0 83980 35 0 0 25 0 1 0 422793133 45146112 10029 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11022 10029 603 41 0 10981 0
vsize: 44088
[startup+850.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10235 0 0 0 84980 35 0 0 25 0 1 0 422793133 45281280 10063 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11055 10063 603 41 0 11014 0
vsize: 44220
[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10267 0 0 0 85980 35 0 0 25 0 1 0 422793133 45412352 10095 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11087 10095 603 41 0 11046 0
vsize: 44348
[startup+870.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10312 0 0 0 86980 35 0 0 25 0 1 0 422793133 45674496 10140 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11151 10140 603 41 0 11110 0
vsize: 44604
[startup+880.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10355 0 0 0 87980 35 0 0 25 0 1 0 422793133 45809664 10183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11184 10183 603 41 0 11143 0
vsize: 44736
[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10395 0 0 0 88980 35 0 0 25 0 1 0 422793133 45944832 10223 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11217 10223 603 41 0 11176 0
vsize: 44868
[startup+900.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10438 0 0 0 89980 35 0 0 25 0 1 0 422793133 46075904 10266 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11249 10266 603 41 0 11208 0
vsize: 44996
[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10488 0 0 0 90980 35 0 0 25 0 1 0 422793133 46338048 10316 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11313 10316 603 41 0 11272 0
vsize: 45252
[startup+920.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10526 0 0 0 91980 35 0 0 25 0 1 0 422793133 46469120 10354 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11345 10354 603 41 0 11304 0
vsize: 45380
[startup+930.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10562 0 0 0 92980 35 0 0 25 0 1 0 422793133 46600192 10390 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11377 10390 603 41 0 11336 0
vsize: 45508
[startup+940.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10596 0 0 0 93981 36 0 0 25 0 1 0 422793133 46731264 10424 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11409 10424 603 41 0 11368 0
vsize: 45636
[startup+950.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10632 0 0 0 94981 36 0 0 25 0 1 0 422793133 46866432 10460 4294967295 134512640 134672761 3221224560 3221223728 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11442 10460 603 41 0 11401 0
vsize: 45768
[startup+960.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10670 0 0 0 95981 36 0 0 25 0 1 0 422793133 46997504 10498 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11474 10498 603 41 0 11433 0
vsize: 45896
[startup+970.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10712 0 0 0 96981 36 0 0 25 0 1 0 422793133 47263744 10540 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11539 10540 603 41 0 11498 0
vsize: 46156
[startup+980.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10745 0 0 0 97981 36 0 0 25 0 1 0 422793133 47394816 10573 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11571 10573 603 41 0 11530 0
vsize: 46284
[startup+990.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10814 0 0 0 98980 37 0 0 25 0 1 0 422793133 47697920 10642 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11645 10642 603 41 0 11604 0
vsize: 46580
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10878 0 0 0 99980 37 0 0 25 0 1 0 422793133 47964160 10706 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11710 10706 603 41 0 11669 0
vsize: 46840
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10925 0 0 0 100980 37 0 0 25 0 1 0 422793133 48095232 10753 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11742 10753 603 41 0 11701 0
vsize: 46968
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 10966 0 0 0 101980 37 0 0 25 0 1 0 422793133 48361472 10794 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11807 10794 603 41 0 11766 0
vsize: 47228
[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11005 0 0 0 102980 38 0 0 25 0 1 0 422793133 48496640 10833 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11840 10833 603 41 0 11799 0
vsize: 47360
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11044 0 0 0 103979 38 0 0 25 0 1 0 422793133 48644096 10872 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11876 10872 603 41 0 11835 0
vsize: 47504
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11089 0 0 0 104980 38 0 0 25 0 1 0 422793133 48775168 10917 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11908 10917 603 41 0 11867 0
vsize: 47632
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11132 0 0 0 105980 38 0 0 25 0 1 0 422793133 48910336 10960 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11941 10960 603 41 0 11900 0
vsize: 47764
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11175 0 0 0 106980 38 0 0 25 0 1 0 422793133 49172480 11003 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12005 11003 603 41 0 11964 0
vsize: 48020
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11208 0 0 0 107980 38 0 0 25 0 1 0 422793133 49393664 11036 4294967295 134512640 134672761 3221224560 3221223664 134560019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12059 11036 603 41 0 12018 0
vsize: 48236
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11249 0 0 0 108980 38 0 0 25 0 1 0 422793133 49537024 11077 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12094 11077 603 41 0 12053 0
vsize: 48376
[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11284 0 0 0 109981 38 0 0 25 0 1 0 422793133 49668096 11112 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12126 11112 603 41 0 12085 0
vsize: 48504
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11321 0 0 0 110981 39 0 0 25 0 1 0 422793133 49803264 11149 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12159 11149 603 41 0 12118 0
vsize: 48636
[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11359 0 0 0 111981 39 0 0 25 0 1 0 422793133 49934336 11187 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12191 11187 603 41 0 12150 0
vsize: 48764
[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11419 0 0 0 112980 39 0 0 25 0 1 0 422793133 50327552 11247 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12287 11247 603 41 0 12246 0
vsize: 49148
[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11448 0 0 0 113980 39 0 0 25 0 1 0 422793133 50499584 11276 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12329 11276 603 41 0 12288 0
vsize: 49316
[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11484 0 0 0 114981 39 0 0 25 0 1 0 422793133 50679808 11312 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12373 11312 603 41 0 12332 0
vsize: 49492
[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11520 0 0 0 115981 39 0 0 25 0 1 0 422793133 50814976 11348 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12406 11348 603 41 0 12365 0
vsize: 49624
[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11557 0 0 0 116981 40 0 0 25 0 1 0 422793133 50946048 11385 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12438 11385 603 41 0 12397 0
vsize: 49752
[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11595 0 0 0 117981 40 0 0 25 0 1 0 422793133 51077120 11423 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12470 11423 603 41 0 12429 0
vsize: 49880
[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11623 0 0 0 118981 40 0 0 25 0 1 0 422793133 51208192 11451 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12502 11451 603 41 0 12461 0
vsize: 50008
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3845
Raw data (stat): 3845 (minisat+) R 3844 29151 29150 0 -1 0 11674 0 0 0 119981 40 0 0 25 0 1 0 422793133 51376128 11502 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12543 11502 603 41 0 12502 0
vsize: 50172
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3845
Raw data (stat): 3845 (minisat+) Z 3844 29151 29150 0 -1 12 11677 0 0 0 119981 43 0 0 25 0 1 0 422793133 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.24
CPU user time (s): 1199.81
CPU system time (s): 0.431934
CPU usage (%): 100.011
Max. virtual memory (Kb): 50172
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####