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-my_adder.opb
MD5SUM	fe8f615a95a6852516985b8e3e78bd85
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	4561
Optimality of the best value was proved	NO
Number of terms in the objective function	577
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	24510
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	24510
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02584
Number of variables	577
Total number of constraints	1322
Number of constraints which are clauses	1306
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	16
Minimum length of a constraint	2
Maximum length of a constraint	17
Trace number 5005

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-13 21:13:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2291 boxname=wulflinc21 idbench=255 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  fe8f615a95a6852516985b8e3e78bd85  /oldhome/oroussel/tmp/wulflinc21/normalized-my_adder.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc21/normalized-my_adder.opb
IDLAUNCH: 2291
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        910756 kB
Buffers:         26252 kB
Cached:          78060 kB
SwapCached:          0 kB
Active:          33764 kB
Inactive:        73372 kB
HighTotal:      131008 kB
HighFree:        49336 kB
LowTotal:       903652 kB
LowFree:        861420 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11256 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:33:30 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 2291 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1322 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 |    1322     4977 |     440       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6274[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:87831     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |  210130   492551 |   70043       1        7     7.0 |  0.000 % |
c |       101 |  209639   491465 |   77047      98     1983    20.2 |  0.188 % |
c |       251 |  209398   490919 |   84752     246     3047    12.4 |  0.270 % |
c |       477 |  209398   490919 |   93227     472     5320    11.3 |  0.270 % |
c |       814 |  209398   490919 |  102549     809     7426     9.2 |  0.270 % |
c |      1320 |  209398   490919 |  112804    1315    12893     9.8 |  0.270 % |
c |      2079 |  208099   487975 |  124085    2062    18966     9.2 |  0.850 % |
c |      3223 |  207777   487250 |  136493    3203    75259    23.5 |  1.015 % |
c |      4934 |  207777   487250 |  150143    4914   465375    94.7 |  1.015 % |
c |      7496 |  207777   487250 |  165157    7476   523941    70.1 |  1.015 % |
c |     11343 |  207124   485763 |  181673   11316   605974    53.6 |  1.304 % |
c ==============================================================================
c [1mFound solution: 6030[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63107     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15902 |  341282   799222 |  113760   15812   677541    42.8 |  1.304 % |
c |     16002 |  341282   799222 |  125136   15912   678586    42.6 |  1.292 % |
c |     16153 |  341282   799222 |  137649   16063   680125    42.3 |  1.292 % |
c |     16378 |  341282   799222 |  151414   16288   682659    41.9 |  1.292 % |
c |     16715 |  341282   799222 |  166556   16625   686273    41.3 |  1.292 % |
c |     17222 |  341282   799222 |  183211   17132   689710    40.3 |  1.292 % |
c |     17982 |  341282   799222 |  201532   17892   701677    39.2 |  1.292 % |
c ==============================================================================
c [1mFound solution: 5941[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18575 |  341328   799730 |  113776   18485   726783    39.3 |  1.292 % |
c |     18675 |  341311   799693 |  125153   18584   727472    39.1 |  1.297 % |
c |     18825 |  341311   799693 |  137668   18734   728419    38.9 |  1.297 % |
c |     19050 |  341311   799693 |  151435   18959   730280    38.5 |  1.297 % |
c |     19388 |  341311   799693 |  166579   19297   732516    38.0 |  1.297 % |
c |     19894 |  341311   799693 |  183237   19803   738567    37.3 |  1.297 % |
c |     20653 |  341060   799139 |  201561   20560   748577    36.4 |  1.351 % |
c |     21792 |  341060   799139 |  221717   21699   757149    34.9 |  1.351 % |
c |     23500 |  341060   799139 |  243888   23407   808068    34.5 |  1.351 % |
c |     26064 |  340058   796875 |  268277   25935   888362    34.3 |  1.591 % |
c |     29909 |  340058   796875 |  295105   29780   993861    33.4 |  1.591 % |
c |     35675 |  340058   796875 |  324616   35546  1611580    45.3 |  1.591 % |
c |     44326 |  340058   796875 |  357077   44197  2011857    45.5 |  1.591 % |
c |     57300 |  339999   796741 |  392785   57162  2368847    41.4 |  1.609 % |
c |     76763 |  339999   796741 |  432064   76625  7374052    96.2 |  1.609 % |
c |    105956 |  339999   796741 |  475270  105818  9897084    93.5 |  1.609 % |
c ==============================================================================
c [1mFound solution: 5700[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:64909     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108372 |  479644  1122919 |  159881  108234 10027671    92.6 |  1.609 % |
c |    108473 |  479644  1122919 |  175869  108335 10028620    92.6 |  1.141 % |
c |    108623 |  479644  1122919 |  193456  108485 10030258    92.5 |  1.141 % |
c |    108848 |  479644  1122919 |  212801  108710 10032710    92.3 |  1.141 % |
c |    109185 |  479644  1122919 |  234081  109047 10045641    92.1 |  1.141 % |
c |    109691 |  479498  1122590 |  257489  109542 10064209    91.9 |  1.162 % |
c |    110451 |  479498  1122590 |  283238  110302 10074504    91.3 |  1.162 % |
c |    111590 |  479498  1122590 |  311562  111441 10093566    90.6 |  1.162 % |
c |    113298 |  479498  1122590 |  342719  113149 10108665    89.3 |  1.162 % |
c |    115860 |  479488  1122570 |  376991  115708 10180504    88.0 |  1.165 % |
c |    119704 |  479488  1122570 |  414690  119552 10487501    87.7 |  1.165 % |
c |    125470 |  479488  1122570 |  456159  125318 11610478    92.6 |  1.165 % |
c |    134119 |  479488  1122570 |  501775  133967 11828437    88.3 |  1.165 % |
c |    147093 |  479488  1122570 |  551952  146941 12479339    84.9 |  1.165 % |
c |    166556 |  479456  1122498 |  607147  166403 15031220    90.3 |  1.175 % |
#### 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.91 0.95 0.90 2/55 1714
Raw data (stat): 1714 (runsolver) R 1713 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 356365544 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+10.0002 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 7217 0 0 0 982 17 0 0 25 0 1 0 356365544 32940032 6744 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8042 6744 603 41 0 8001 0
vsize: 32168
[startup+20.0008 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 7564 0 0 0 1981 18 0 0 25 0 1 0 356365544 34414592 7091 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8402 7091 603 41 0 8361 0
vsize: 33608
[startup+30.0005 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 7728 0 0 0 2980 19 0 0 25 0 1 0 356365544 35082240 7255 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8565 7255 603 41 0 8524 0
vsize: 34260
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 7837 0 0 0 3980 20 0 0 25 0 1 0 356365544 35500032 7364 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8667 7364 603 41 0 8626 0
vsize: 34668
[startup+50.0019 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 7912 0 0 0 4979 20 0 0 25 0 1 0 356365544 35770368 7439 4294967295 134512640 134672761 3221224640 3221223776 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8733 7439 603 41 0 8692 0
vsize: 34932
[startup+60.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 12170 0 0 0 5969 31 0 0 25 0 1 0 356365544 59580416 11572 4294967295 134512640 134672761 3221224640 3221223808 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14546 11572 603 41 0 14505 0
vsize: 58184
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 12461 0 0 0 6968 32 0 0 25 0 1 0 356365544 60153856 11821 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14686 11821 603 41 0 14645 0
vsize: 58744
[startup+80.0029 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 12542 0 0 0 7967 32 0 0 25 0 1 0 356365544 60424192 11902 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14752 11902 603 41 0 14711 0
vsize: 59008
[startup+90.0036 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 12603 0 0 0 8967 33 0 0 25 0 1 0 356365544 60690432 11963 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14817 11963 603 41 0 14776 0
vsize: 59268
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 12638 0 0 0 9967 33 0 0 25 0 1 0 356365544 60821504 11998 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14849 11998 603 41 0 14808 0
vsize: 59396
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 12705 0 0 0 10967 33 0 0 25 0 1 0 356365544 61091840 12065 4294967295 134512640 134672761 3221224640 3221223744 134555214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14915 12065 603 41 0 14874 0
vsize: 59660
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 12772 0 0 0 11966 34 0 0 25 0 1 0 356365544 61362176 12132 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14981 12132 603 41 0 14940 0
vsize: 59924
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 12876 0 0 0 12966 34 0 0 25 0 1 0 356365544 61894656 12236 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15111 12236 603 41 0 15070 0
vsize: 60444
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 13061 0 0 0 13965 35 0 0 25 0 1 0 356365544 62689280 12421 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15305 12421 603 41 0 15264 0
vsize: 61220
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 13413 0 0 0 14965 36 0 0 25 0 1 0 356365544 64045056 12773 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15636 12773 603 41 0 15595 0
vsize: 62544
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 13465 0 0 0 15964 36 0 0 25 0 1 0 356365544 64315392 12825 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15702 12825 603 41 0 15661 0
vsize: 62808
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 13519 0 0 0 16964 37 0 0 25 0 1 0 356365544 64450560 12879 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15735 12879 603 41 0 15694 0
vsize: 62940
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 13583 0 0 0 17964 37 0 0 25 0 1 0 356365544 64712704 12943 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15799 12943 603 41 0 15758 0
vsize: 63196
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 13744 0 0 0 18964 38 0 0 25 0 1 0 356365544 65388544 13104 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15964 13104 603 41 0 15923 0
vsize: 63856
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 13889 0 0 0 19963 38 0 0 25 0 1 0 356365544 65925120 13249 4294967295 134512640 134672761 3221224640 3221223824 134558697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16095 13249 603 41 0 16054 0
vsize: 64380
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 13960 0 0 0 20963 38 0 0 25 0 1 0 356365544 66330624 13320 4294967295 134512640 134672761 3221224640 3221223776 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16194 13320 603 41 0 16153 0
vsize: 64776
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14067 0 0 0 21962 39 0 0 25 0 1 0 356365544 66736128 13427 4294967295 134512640 134672761 3221224640 3221223808 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16293 13427 603 41 0 16252 0
vsize: 65172
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14123 0 0 0 22962 39 0 0 25 0 1 0 356365544 66867200 13483 4294967295 134512640 134672761 3221224640 3221223776 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16325 13483 603 41 0 16284 0
vsize: 65300
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14196 0 0 0 23962 40 0 0 25 0 1 0 356365544 67268608 13556 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16423 13556 603 41 0 16382 0
vsize: 65692
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14269 0 0 0 24962 40 0 0 25 0 1 0 356365544 67534848 13629 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16488 13629 603 41 0 16447 0
vsize: 65952
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14344 0 0 0 25961 40 0 0 25 0 1 0 356365544 67805184 13704 4294967295 134512640 134672761 3221224640 3221223808 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16554 13704 603 41 0 16513 0
vsize: 66216
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14411 0 0 0 26961 41 0 0 25 0 1 0 356365544 68075520 13771 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16620 13771 603 41 0 16579 0
vsize: 66480
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14531 0 0 0 27961 41 0 0 25 0 1 0 356365544 68616192 13891 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16752 13891 603 41 0 16711 0
vsize: 67008
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14743 0 0 0 28960 42 0 0 25 0 1 0 356365544 69427200 14103 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16950 14103 603 41 0 16909 0
vsize: 67800
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 14956 0 0 0 29959 43 0 0 25 0 1 0 356365544 70230016 14316 4294967295 134512640 134672761 3221224640 3221223840 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17146 14316 603 41 0 17105 0
vsize: 68584
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 15202 0 0 0 30958 44 0 0 25 0 1 0 356365544 71303168 14562 4294967295 134512640 134672761 3221224640 3221223776 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17408 14562 603 41 0 17367 0
vsize: 69632
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 15394 0 0 0 31958 45 0 0 25 0 1 0 356365544 72118272 14754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17607 14754 603 41 0 17566 0
vsize: 70428
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 15643 0 0 0 32957 46 0 0 25 0 1 0 356365544 73043968 15003 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17833 15003 603 41 0 17792 0
vsize: 71332
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 15910 0 0 0 33956 46 0 0 25 0 1 0 356365544 74215424 15270 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18119 15270 603 41 0 18078 0
vsize: 72476
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 16153 0 0 0 34955 47 0 0 25 0 1 0 356365544 75145216 15513 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18346 15513 603 41 0 18305 0
vsize: 73384
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 16407 0 0 0 35955 48 0 0 25 0 1 0 356365544 76165120 15767 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18595 15767 603 41 0 18554 0
vsize: 74380
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 16630 0 0 0 36954 48 0 0 25 0 1 0 356365544 77111296 15990 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18826 15990 603 41 0 18785 0
vsize: 75304
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 16857 0 0 0 37954 49 0 0 25 0 1 0 356365544 78295040 16217 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19115 16217 603 41 0 19074 0
vsize: 76460
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 17089 0 0 0 38953 50 0 0 25 0 1 0 356365544 79233024 16449 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19344 16449 603 41 0 19303 0
vsize: 77376
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 17294 0 0 0 39953 51 0 0 25 0 1 0 356365544 80171008 16654 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19573 16654 603 41 0 19532 0
vsize: 78292
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 17524 0 0 0 40952 51 0 0 25 0 1 0 356365544 81100800 16884 4294967295 134512640 134672761 3221224640 3221223744 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19800 16884 603 41 0 19759 0
vsize: 79200
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 17784 0 0 0 41951 52 0 0 25 0 1 0 356365544 82046976 17144 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20031 17144 603 41 0 19990 0
vsize: 80124
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 18035 0 0 0 42951 53 0 0 25 0 1 0 356365544 83116032 17395 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20292 17395 603 41 0 20251 0
vsize: 81168
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 18227 0 0 0 43951 53 0 0 25 0 1 0 356365544 83910656 17587 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20486 17587 603 41 0 20445 0
vsize: 81944
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 18467 0 0 0 44950 54 0 0 25 0 1 0 356365544 84852736 17827 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20716 17827 603 41 0 20675 0
vsize: 82864
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 18622 0 0 0 45949 55 0 0 25 0 1 0 356365544 85532672 17982 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20882 17982 603 41 0 20841 0
vsize: 83528
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 18896 0 0 0 46949 55 0 0 25 0 1 0 356365544 86597632 18256 4294967295 134512640 134672761 3221224640 3221223744 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21142 18256 603 41 0 21101 0
vsize: 84568
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 19152 0 0 0 47948 56 0 0 25 0 1 0 356365544 87670784 18512 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21404 18512 603 41 0 21363 0
vsize: 85616
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 19369 0 0 0 48948 57 0 0 25 0 1 0 356365544 88588288 18729 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21628 18729 603 41 0 21587 0
vsize: 86512
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 19435 0 0 0 49948 57 0 0 25 0 1 0 356365544 88854528 18795 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21693 18795 603 41 0 21652 0
vsize: 86772
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 19507 0 0 0 50947 57 0 0 25 0 1 0 356365544 89124864 18867 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21759 18867 603 41 0 21718 0
vsize: 87036
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 19705 0 0 0 51946 58 0 0 25 0 1 0 356365544 89927680 19065 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21955 19065 603 41 0 21914 0
vsize: 87820
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 19968 0 0 0 52946 58 0 0 25 0 1 0 356365544 91009024 19328 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22219 19328 603 41 0 22178 0
vsize: 88876
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 20147 0 0 0 53945 59 0 0 25 0 1 0 356365544 91684864 19507 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22384 19507 603 41 0 22343 0
vsize: 89536
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 20499 0 0 0 54945 60 0 0 25 0 1 0 356365544 93167616 19859 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22746 19859 603 41 0 22705 0
vsize: 90984
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 20691 0 0 0 55944 61 0 0 25 0 1 0 356365544 93978624 20051 4294967295 134512640 134672761 3221224640 3221223744 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22944 20051 603 41 0 22903 0
vsize: 91776
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 20940 0 0 0 56943 61 0 0 25 0 1 0 356365544 94908416 20300 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23171 20300 603 41 0 23130 0
vsize: 92684
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 21045 0 0 0 57943 62 0 0 25 0 1 0 356365544 95444992 20405 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23302 20405 603 41 0 23261 0
vsize: 93208
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 21285 0 0 0 58942 63 0 0 25 0 1 0 356365544 96382976 20645 4294967295 134512640 134672761 3221224640 3221223796 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23531 20645 603 41 0 23490 0
vsize: 94124
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 21461 0 0 0 59942 63 0 0 25 0 1 0 356365544 97058816 20821 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23696 20821 603 41 0 23655 0
vsize: 94784
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 21634 0 0 0 60942 63 0 0 25 0 1 0 356365544 97730560 20994 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23860 20994 603 41 0 23819 0
vsize: 95440
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 21756 0 0 0 61941 64 0 0 25 0 1 0 356365544 98263040 21116 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23990 21116 603 41 0 23949 0
vsize: 95960
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 21955 0 0 0 62941 65 0 0 25 0 1 0 356365544 99061760 21315 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24185 21315 603 41 0 24144 0
vsize: 96740
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 22168 0 0 0 63940 65 0 0 25 0 1 0 356365544 99860480 21528 4294967295 134512640 134672761 3221224640 3221223808 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24380 21528 603 41 0 24339 0
vsize: 97520
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 22361 0 0 0 64940 66 0 0 25 0 1 0 356365544 100667392 21721 4294967295 134512640 134672761 3221224640 3221223744 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24577 21721 603 41 0 24536 0
vsize: 98308
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27176 0 0 0 65929 77 0 0 25 0 1 0 356365544 116027392 26164 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28327 26164 603 41 0 28286 0
vsize: 113308
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27240 0 0 0 66929 77 0 0 25 0 1 0 356365544 116305920 26228 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28395 26228 603 41 0 28354 0
vsize: 113580
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27336 0 0 0 67928 78 0 0 25 0 1 0 356365544 116576256 26324 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28461 26324 603 41 0 28420 0
vsize: 113844
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27377 0 0 0 68928 78 0 0 25 0 1 0 356365544 116842496 26365 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28526 26365 603 41 0 28485 0
vsize: 114104
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27424 0 0 0 69928 78 0 0 25 0 1 0 356365544 116973568 26412 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28558 26412 603 41 0 28517 0
vsize: 114232
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27507 0 0 0 70927 79 0 0 25 0 1 0 356365544 117379072 26495 4294967295 134512640 134672761 3221224640 3221223804 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28657 26495 603 41 0 28616 0
vsize: 114628
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27621 0 0 0 71927 80 0 0 25 0 1 0 356365544 117780480 26609 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28755 26609 603 41 0 28714 0
vsize: 115020
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27728 0 0 0 72926 80 0 0 25 0 1 0 356365544 118173696 26716 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28851 26716 603 41 0 28810 0
vsize: 115404
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27879 0 0 0 73926 80 0 0 25 0 1 0 356365544 118845440 26867 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29015 26867 603 41 0 28974 0
vsize: 116060
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 27943 0 0 0 74926 81 0 0 25 0 1 0 356365544 119115776 26931 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29081 26931 603 41 0 29040 0
vsize: 116324
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 28289 0 0 0 75925 82 0 0 25 0 1 0 356365544 120471552 27277 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29412 27277 603 41 0 29371 0
vsize: 117648
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 28482 0 0 0 76925 82 0 0 25 0 1 0 356365544 121278464 27470 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29609 27470 603 41 0 29568 0
vsize: 118436
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 28759 0 0 0 77924 83 0 0 25 0 1 0 356365544 122359808 27747 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29873 27747 603 41 0 29832 0
vsize: 119492
[startup+790.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 28922 0 0 0 78923 84 0 0 25 0 1 0 356365544 123031552 27910 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30037 27910 603 41 0 29996 0
vsize: 120148
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 28975 0 0 0 79923 84 0 0 25 0 1 0 356365544 123293696 27963 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30101 27963 603 41 0 30060 0
vsize: 120404
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29036 0 0 0 80923 85 0 0 25 0 1 0 356365544 123559936 28024 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30166 28024 603 41 0 30125 0
vsize: 120664
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29099 0 0 0 81922 85 0 0 25 0 1 0 356365544 123826176 28087 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30231 28087 603 41 0 30190 0
vsize: 120924
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29168 0 0 0 82922 85 0 0 25 0 1 0 356365544 124620800 28156 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30425 28156 603 41 0 30384 0
vsize: 121700
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29270 0 0 0 83922 86 0 0 25 0 1 0 356365544 125022208 28258 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30523 28258 603 41 0 30482 0
vsize: 122092
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29428 0 0 0 84922 86 0 0 25 0 1 0 356365544 125689856 28416 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30686 28416 603 41 0 30645 0
vsize: 122744
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29498 0 0 0 85921 87 0 0 25 0 1 0 356365544 125960192 28486 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30752 28486 603 41 0 30711 0
vsize: 123008
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29594 0 0 0 86921 87 0 0 25 0 1 0 356365544 126365696 28582 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30851 28582 603 41 0 30810 0
vsize: 123404
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29667 0 0 0 87921 87 0 0 25 0 1 0 356365544 126631936 28655 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30916 28655 603 41 0 30875 0
vsize: 123664
[startup+890.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29735 0 0 0 88920 88 0 0 25 0 1 0 356365544 126902272 28723 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30982 28723 603 41 0 30941 0
vsize: 123928
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29820 0 0 0 89920 88 0 0 25 0 1 0 356365544 127172608 28808 4294967295 134512640 134672761 3221224640 3221223776 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31048 28808 603 41 0 31007 0
vsize: 124192
[startup+910.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29902 0 0 0 90920 88 0 0 25 0 1 0 356365544 127578112 28890 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31147 28890 603 41 0 31106 0
vsize: 124588
[startup+920.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 29993 0 0 0 91920 89 0 0 25 0 1 0 356365544 127848448 28981 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31213 28981 603 41 0 31172 0
vsize: 124852
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 30084 0 0 0 92920 89 0 0 25 0 1 0 356365544 128258048 29072 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31313 29072 603 41 0 31272 0
vsize: 125252
[startup+940.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 30133 0 0 0 93920 89 0 0 25 0 1 0 356365544 128528384 29121 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31379 29121 603 41 0 31338 0
vsize: 125516
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 30308 0 0 0 94920 89 0 0 25 0 1 0 356365544 129204224 29296 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31544 29296 603 41 0 31503 0
vsize: 126176
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 30454 0 0 0 95919 90 0 0 25 0 1 0 356365544 129736704 29442 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31674 29442 603 41 0 31633 0
vsize: 126696
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 30548 0 0 0 96919 90 0 0 25 0 1 0 356365544 130146304 29536 4294967295 134512640 134672761 3221224640 3221223744 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31774 29536 603 41 0 31733 0
vsize: 127096
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 30666 0 0 0 97919 90 0 0 25 0 1 0 356365544 130682880 29654 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31905 29654 603 41 0 31864 0
vsize: 127620
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 30848 0 0 0 98918 91 0 0 25 0 1 0 356365544 131358720 29836 4294967295 134512640 134672761 3221224640 3221223780 134560629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32070 29836 603 41 0 32029 0
vsize: 128280
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 31012 0 0 0 99918 92 0 0 25 0 1 0 356365544 132034560 30000 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32235 30000 603 41 0 32194 0
vsize: 128940
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 31207 0 0 0 100917 93 0 0 25 0 1 0 356365544 132845568 30195 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32433 30195 603 41 0 32392 0
vsize: 129732
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 31400 0 0 0 101916 93 0 0 25 0 1 0 356365544 133648384 30388 4294967295 134512640 134672761 3221224640 3221223744 134560231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32629 30388 603 41 0 32588 0
vsize: 130516
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 31599 0 0 0 102916 94 0 0 25 0 1 0 356365544 134434816 30587 4294967295 134512640 134672761 3221224640 3221223744 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32821 30587 603 41 0 32780 0
vsize: 131284
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 31794 0 0 0 103915 95 0 0 25 0 1 0 356365544 135233536 30782 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33016 30782 603 41 0 32975 0
vsize: 132064
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 31949 0 0 0 104915 96 0 0 25 0 1 0 356365544 135909376 30937 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33181 30937 603 41 0 33140 0
vsize: 132724
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32042 0 0 0 105914 96 0 0 25 0 1 0 356365544 136310784 31030 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33279 31030 603 41 0 33238 0
vsize: 133116
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32150 0 0 0 106914 96 0 0 25 0 1 0 356365544 136716288 31138 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33378 31138 603 41 0 33337 0
vsize: 133512
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32307 0 0 0 107914 97 0 0 25 0 1 0 356365544 137392128 31295 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33543 31295 603 41 0 33502 0
vsize: 134172
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32432 0 0 0 108913 98 0 0 25 0 1 0 356365544 137785344 31420 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33639 31420 603 41 0 33598 0
vsize: 134556
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32493 0 0 0 109913 98 0 0 25 0 1 0 356365544 138055680 31481 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33705 31481 603 41 0 33664 0
vsize: 134820
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32542 0 0 0 110913 98 0 0 25 0 1 0 356365544 138321920 31530 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33770 31530 603 41 0 33729 0
vsize: 135080
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32579 0 0 0 111913 98 0 0 25 0 1 0 356365544 138452992 31567 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33802 31567 603 41 0 33761 0
vsize: 135208
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32611 0 0 0 112913 99 0 0 25 0 1 0 356365544 138588160 31599 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33835 31599 603 41 0 33794 0
vsize: 135340
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32665 0 0 0 113912 99 0 0 25 0 1 0 356365544 138723328 31653 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33868 31653 603 41 0 33827 0
vsize: 135472
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32754 0 0 0 114912 99 0 0 25 0 1 0 356365544 139124736 31742 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33966 31742 603 41 0 33925 0
vsize: 135864
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32808 0 0 0 115912 100 0 0 25 0 1 0 356365544 139395072 31796 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34032 31796 603 41 0 33991 0
vsize: 136128
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 32883 0 0 0 116912 100 0 0 25 0 1 0 356365544 139661312 31871 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34097 31871 603 41 0 34056 0
vsize: 136388
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 33038 0 0 0 117911 101 0 0 25 0 1 0 356365544 140337152 32026 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34262 32026 603 41 0 34221 0
vsize: 137048
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 33192 0 0 0 118911 101 0 0 25 0 1 0 356365544 140877824 32180 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34394 32180 603 41 0 34353 0
vsize: 137576
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1714
Raw data (stat): 1714 (minisat+) R 1713 30927 30926 0 -1 0 33425 0 0 0 119910 102 0 0 25 0 1 0 356365544 141815808 32413 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34623 32413 603 41 0 34582 0
vsize: 138492
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 1714
Raw data (stat): 1714 (minisat+) Z 1713 30927 30926 0 -1 12 33428 0 0 0 119910 108 0 0 25 0 1 0 356365544 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.09
CPU time (s): 1200.19
CPU user time (s): 1199.11
CPU system time (s): 1.08583
CPU usage (%): 100.009
Max. virtual memory (Kb): 138492
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####