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/primes-dimacs-cnf/normalized-par32-1-c.opb
MD5SUM	8c1b8634a2f99e9f8e579ef031d10353
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	2630
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	2630
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	2630
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	2630
Total number of constraints	6569
Number of constraints which are clauses	6569
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	3
Trace number 4940

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-13 20:57:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1823 boxname=wulflinc24 idbench=203 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  8c1b8634a2f99e9f8e579ef031d10353  /oldhome/oroussel/tmp/wulflinc24/normalized-par32-1-c.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc24/normalized-par32-1-c.opb
IDLAUNCH: 1823
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        862524 kB
Buffers:         33712 kB
Cached:          96012 kB
SwapCached:       3828 kB
Active:          47944 kB
Inactive:        88472 kB
HighTotal:      131008 kB
HighFree:        32676 kB
LowTotal:       903652 kB
LowFree:        829848 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30208 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:17:44 (client local time) WITH STATUS 0 IN 1200.13 SECONDS
stats: 1823 7 1200.13 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6569 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 |    6569    18020 |    2189       0        0     nan |  0.000 % |
c |       100 |    6569    18020 |    2407     100     3667    36.7 |  0.004 % |
c |       251 |    6569    18020 |    2648     251     9998    39.8 |  0.000 % |
c |       477 |    6569    18020 |    2913     477    19389    40.6 |  0.000 % |
c |       814 |    6569    18020 |    3204     814    28997    35.6 |  0.000 % |
c |      1320 |    6569    18020 |    3525    1320    43427    32.9 |  0.000 % |
c |      2079 |    6562    18004 |    3877    2077    64872    31.2 |  0.076 % |
c |      3218 |    6562    18004 |    4265    3216    92939    28.9 |  0.076 % |
c |      4927 |    6562    18004 |    4692    2772    64097    23.1 |  0.076 % |
c |      7489 |    6562    18004 |    5161    2951    64576    21.9 |  0.076 % |
c |     11333 |    6562    18004 |    5677    4187    97402    23.3 |  0.076 % |
c |     17099 |    6562    18004 |    6245    4190    93186    22.2 |  0.076 % |
c |     25748 |    6562    18004 |    6870    3311    68434    20.7 |  0.076 % |
c |     38722 |    6562    18004 |    7557    5903   133047    22.5 |  0.076 % |
c |     58183 |    6562    18004 |    8312    6287   144714    23.0 |  0.076 % |
c |     87376 |    6562    18004 |    9143    6021   133526    22.2 |  0.076 % |
c |    131166 |    6562    18004 |   10058    8376   183814    21.9 |  0.076 % |
c |    196850 |    6562    18004 |   11064    8127   172744    21.3 |  0.076 % |
c |    295376 |    6562    18004 |   12170    6300   144154    22.9 |  0.076 % |
c |    443166 |    6562    18004 |   13387    6996   179583    25.7 |  0.076 % |
c |    664849 |    6562    18004 |   14726   13043   279106    21.4 |  0.076 % |
#### 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.80 0.94 0.90 2/54 31585
Raw data (stat): 31585 (runsolver) R 31584 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479003961 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.99994 s]
Raw data (loadavg): 0.83 0.94 0.90 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 774 0 0 0 996 2 0 0 25 0 1 0 479003961 4775936 752 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1166 752 603 41 0 1125 0
vsize: 4664
[startup+20.0002 s]
Raw data (loadavg): 0.86 0.94 0.90 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 801 0 0 0 1995 2 0 0 25 0 1 0 479003961 4775936 779 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1166 779 603 41 0 1125 0
vsize: 4664
[startup+30.0013 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 814 0 0 0 2994 2 0 0 25 0 1 0 479003961 4915200 792 4294967295 134512640 134672761 3221224640 3221223824 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1200 792 603 41 0 1159 0
vsize: 4800
[startup+40.002 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 834 0 0 0 3993 3 0 0 25 0 1 0 479003961 5050368 812 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1233 812 603 41 0 1192 0
vsize: 4932
[startup+50.0021 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 871 0 0 0 4992 3 0 0 25 0 1 0 479003961 5185536 849 4294967295 134512640 134672761 3221224640 3221223808 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1266 849 603 41 0 1225 0
vsize: 5064
[startup+60.0018 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 877 0 0 0 5992 3 0 0 25 0 1 0 479003961 5185536 855 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1266 855 603 41 0 1225 0
vsize: 5064
[startup+70.0028 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 912 0 0 0 6992 3 0 0 25 0 1 0 479003961 5320704 890 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1299 890 603 41 0 1258 0
vsize: 5196
[startup+80.0032 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 920 0 0 0 7992 3 0 0 25 0 1 0 479003961 5459968 898 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 898 603 41 0 1292 0
vsize: 5332
[startup+90.0032 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 920 0 0 0 8992 3 0 0 25 0 1 0 479003961 5459968 898 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 898 603 41 0 1292 0
vsize: 5332
[startup+100.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 924 0 0 0 9992 4 0 0 25 0 1 0 479003961 5459968 902 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1333 902 603 41 0 1292 0
vsize: 5332
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 945 0 0 0 10992 4 0 0 25 0 1 0 479003961 5459968 923 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 923 603 41 0 1292 0
vsize: 5332
[startup+120.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 950 0 0 0 11992 4 0 0 25 0 1 0 479003961 5459968 928 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 928 603 41 0 1292 0
vsize: 5332
[startup+130.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 950 0 0 0 12992 4 0 0 25 0 1 0 479003961 5459968 928 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 928 603 41 0 1292 0
vsize: 5332
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31585
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 959 0 0 0 13992 4 0 0 25 0 1 0 479003961 5595136 937 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1366 937 603 41 0 1325 0
vsize: 5464
[startup+150.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31638
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 960 0 0 0 14987 10 0 0 25 0 1 0 479003961 5595136 938 4294967295 134512640 134672761 3221224640 3221223744 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1366 938 603 41 0 1325 0
vsize: 5464
[startup+160.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 31638
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 989 0 0 0 15987 10 0 0 25 0 1 0 479003961 5730304 967 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 967 603 41 0 1358 0
vsize: 5596
[startup+170.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31638
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1002 0 0 0 16988 10 0 0 25 0 1 0 479003961 5730304 980 4294967295 134512640 134672761 3221224640 3221223776 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 980 603 41 0 1358 0
vsize: 5596
[startup+180.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31638
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1011 0 0 0 17988 10 0 0 25 0 1 0 479003961 5730304 989 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 989 603 41 0 1358 0
vsize: 5596
[startup+190.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31638
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1017 0 0 0 18988 10 0 0 25 0 1 0 479003961 5730304 995 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 995 603 41 0 1358 0
vsize: 5596
[startup+200.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31638
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1017 0 0 0 19988 10 0 0 25 0 1 0 479003961 5730304 995 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 995 603 41 0 1358 0
vsize: 5596
[startup+210.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31638
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1017 0 0 0 20988 10 0 0 25 0 1 0 479003961 5730304 995 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 995 603 41 0 1358 0
vsize: 5596
[startup+220.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31638
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1017 0 0 0 21988 10 0 0 25 0 1 0 479003961 5730304 995 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 995 603 41 0 1358 0
vsize: 5596
[startup+230.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1017 0 0 0 22989 10 0 0 25 0 1 0 479003961 5730304 995 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 995 603 41 0 1358 0
vsize: 5596
[startup+240.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1039 0 0 0 23989 10 0 0 25 0 1 0 479003961 5865472 1017 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1432 1017 603 41 0 1391 0
vsize: 5728
[startup+250.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1052 0 0 0 24989 10 0 0 25 0 1 0 479003961 5865472 1030 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1432 1030 603 41 0 1391 0
vsize: 5728
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1059 0 0 0 25989 10 0 0 25 0 1 0 479003961 6012928 1037 4294967295 134512640 134672761 3221224640 3221223736 1075347312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1468 1037 603 41 0 1427 0
vsize: 5872
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1065 0 0 0 26989 10 0 0 25 0 1 0 479003961 6012928 1043 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1468 1043 603 41 0 1427 0
vsize: 5872
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1070 0 0 0 27989 10 0 0 25 0 1 0 479003961 6012928 1048 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1468 1048 603 41 0 1427 0
vsize: 5872
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1082 0 0 0 28990 10 0 0 25 0 1 0 479003961 6012928 1060 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1468 1060 603 41 0 1427 0
vsize: 5872
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1094 0 0 0 29990 10 0 0 25 0 1 0 479003961 6148096 1072 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1501 1072 603 41 0 1460 0
vsize: 6004
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1101 0 0 0 30990 10 0 0 25 0 1 0 479003961 6148096 1079 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1501 1079 603 41 0 1460 0
vsize: 6004
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1108 0 0 0 31990 10 0 0 25 0 1 0 479003961 6148096 1086 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1501 1086 603 41 0 1460 0
vsize: 6004
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1109 0 0 0 32990 10 0 0 25 0 1 0 479003961 6148096 1087 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1501 1087 603 41 0 1460 0
vsize: 6004
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1114 0 0 0 33990 10 0 0 25 0 1 0 479003961 6291456 1092 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1114 0 0 0 34991 10 0 0 25 0 1 0 479003961 6291456 1092 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1114 0 0 0 35991 10 0 0 25 0 1 0 479003961 6291456 1092 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1124 0 0 0 36991 10 0 0 25 0 1 0 479003961 6291456 1102 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1102 603 41 0 1495 0
vsize: 6144
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1153 0 0 0 37990 10 0 0 25 0 1 0 479003961 6426624 1131 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1569 1131 603 41 0 1528 0
vsize: 6276
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1170 0 0 0 38990 10 0 0 25 0 1 0 479003961 6426624 1148 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1569 1148 603 41 0 1528 0
vsize: 6276
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1173 0 0 0 39990 11 0 0 25 0 1 0 479003961 6426624 1151 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1569 1151 603 41 0 1528 0
vsize: 6276
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1173 0 0 0 40990 11 0 0 25 0 1 0 479003961 6426624 1151 4294967295 134512640 134672761 3221224640 3221223824 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1569 1151 603 41 0 1528 0
vsize: 6276
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1175 0 0 0 41990 11 0 0 25 0 1 0 479003961 6561792 1153 4294967295 134512640 134672761 3221224640 3221223808 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1153 603 41 0 1561 0
vsize: 6408
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1175 0 0 0 42989 11 0 0 25 0 1 0 479003961 6561792 1153 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1153 603 41 0 1561 0
vsize: 6408
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1179 0 0 0 43989 12 0 0 25 0 1 0 479003961 6561792 1157 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1157 603 41 0 1561 0
vsize: 6408
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1183 0 0 0 44989 12 0 0 25 0 1 0 479003961 6561792 1161 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1161 603 41 0 1561 0
vsize: 6408
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1184 0 0 0 45988 12 0 0 25 0 1 0 479003961 6561792 1162 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1162 603 41 0 1561 0
vsize: 6408
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1186 0 0 0 46988 12 0 0 25 0 1 0 479003961 6561792 1164 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1164 603 41 0 1561 0
vsize: 6408
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1196 0 0 0 47988 13 0 0 25 0 1 0 479003961 6561792 1174 4294967295 134512640 134672761 3221224640 3221223744 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1602 1174 603 41 0 1561 0
vsize: 6408
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1208 0 0 0 48987 13 0 0 25 0 1 0 479003961 6717440 1186 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1186 603 41 0 1599 0
vsize: 6560
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1209 0 0 0 49987 13 0 0 25 0 1 0 479003961 6717440 1187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1209 0 0 0 50987 14 0 0 25 0 1 0 479003961 6717440 1187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31640
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1209 0 0 0 51986 14 0 0 25 0 1 0 479003961 6717440 1187 4294967295 134512640 134672761 3221224640 3221223776 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1209 0 0 0 52985 15 0 0 25 0 1 0 479003961 6717440 1187 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1209 0 0 0 53985 15 0 0 25 0 1 0 479003961 6717440 1187 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1209 0 0 0 54985 15 0 0 25 0 1 0 479003961 6717440 1187 4294967295 134512640 134672761 3221224640 3221223636 1075351174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1212 0 0 0 55985 15 0 0 25 0 1 0 479003961 6717440 1190 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1190 603 41 0 1599 0
vsize: 6560
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1230 0 0 0 56985 15 0 0 25 0 1 0 479003961 6717440 1208 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1208 603 41 0 1599 0
vsize: 6560
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1238 0 0 0 57985 15 0 0 25 0 1 0 479003961 6717440 1216 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1216 603 41 0 1599 0
vsize: 6560
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1240 0 0 0 58985 15 0 0 25 0 1 0 479003961 6717440 1218 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1218 603 41 0 1599 0
vsize: 6560
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1247 0 0 0 59985 15 0 0 25 0 1 0 479003961 6868992 1225 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1225 603 41 0 1636 0
vsize: 6708
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1253 0 0 0 60985 15 0 0 25 0 1 0 479003961 6868992 1231 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1231 603 41 0 1636 0
vsize: 6708
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1260 0 0 0 61985 16 0 0 25 0 1 0 479003961 6868992 1238 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1238 603 41 0 1636 0
vsize: 6708
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1261 0 0 0 62986 16 0 0 25 0 1 0 479003961 6868992 1239 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1239 603 41 0 1636 0
vsize: 6708
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1261 0 0 0 63986 16 0 0 25 0 1 0 479003961 6868992 1239 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1239 603 41 0 1636 0
vsize: 6708
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1266 0 0 0 64986 16 0 0 25 0 1 0 479003961 6868992 1244 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1244 603 41 0 1636 0
vsize: 6708
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1267 0 0 0 65985 16 0 0 25 0 1 0 479003961 6868992 1245 4294967295 134512640 134672761 3221224640 3221223776 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1245 603 41 0 1636 0
vsize: 6708
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1273 0 0 0 66985 16 0 0 25 0 1 0 479003961 6868992 1251 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1273 0 0 0 67985 16 0 0 25 0 1 0 479003961 6868992 1251 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1273 0 0 0 68986 16 0 0 25 0 1 0 479003961 6868992 1251 4294967295 134512640 134672761 3221224640 3221223840 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1273 0 0 0 69986 16 0 0 25 0 1 0 479003961 6868992 1251 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1273 0 0 0 70986 16 0 0 25 0 1 0 479003961 6868992 1251 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1277 0 0 0 71986 16 0 0 25 0 1 0 479003961 7004160 1255 4294967295 134512640 134672761 3221224640 3221223824 134559318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1710 1255 603 41 0 1669 0
vsize: 6840
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1293 0 0 0 72986 16 0 0 25 0 1 0 479003961 7004160 1271 4294967295 134512640 134672761 3221224640 3221223808 134561272 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1710 1271 603 41 0 1669 0
vsize: 6840
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1299 0 0 0 73986 16 0 0 25 0 1 0 479003961 7004160 1277 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1710 1277 603 41 0 1669 0
vsize: 6840
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1305 0 0 0 74986 17 0 0 25 0 1 0 479003961 7139328 1283 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1305 0 0 0 75986 17 0 0 25 0 1 0 479003961 7139328 1283 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1305 0 0 0 76987 17 0 0 25 0 1 0 479003961 7139328 1283 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1305 0 0 0 77987 17 0 0 25 0 1 0 479003961 7139328 1283 4294967295 134512640 134672761 3221224640 3221223824 134558654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1305 0 0 0 78987 17 0 0 25 0 1 0 479003961 7139328 1283 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1305 0 0 0 79987 17 0 0 25 0 1 0 479003961 7139328 1283 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1305 0 0 0 80987 17 0 0 25 0 1 0 479003961 7139328 1283 4294967295 134512640 134672761 3221224640 3221223824 134558396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1326 0 0 0 81987 17 0 0 25 0 1 0 479003961 7139328 1304 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1304 603 41 0 1702 0
vsize: 6972
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1355 0 0 0 82986 17 0 0 25 0 1 0 479003961 7270400 1333 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1333 603 41 0 1734 0
vsize: 7100
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1361 0 0 0 83986 18 0 0 25 0 1 0 479003961 7270400 1339 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1339 603 41 0 1734 0
vsize: 7100
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1365 0 0 0 84986 18 0 0 25 0 1 0 479003961 7270400 1343 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1343 603 41 0 1734 0
vsize: 7100
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1367 0 0 0 85986 18 0 0 25 0 1 0 479003961 7270400 1345 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1345 603 41 0 1734 0
vsize: 7100
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1376 0 0 0 86987 18 0 0 25 0 1 0 479003961 7401472 1354 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1354 603 41 0 1766 0
vsize: 7228
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1387 0 0 0 87987 18 0 0 25 0 1 0 479003961 7401472 1365 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1387 0 0 0 88987 18 0 0 25 0 1 0 479003961 7401472 1365 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1387 0 0 0 89987 18 0 0 25 0 1 0 479003961 7401472 1365 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1393 0 0 0 90987 18 0 0 25 0 1 0 479003961 7401472 1371 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1371 603 41 0 1766 0
vsize: 7228
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1393 0 0 0 91987 18 0 0 25 0 1 0 479003961 7401472 1371 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1371 603 41 0 1766 0
vsize: 7228
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1393 0 0 0 92987 18 0 0 25 0 1 0 479003961 7401472 1371 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1371 603 41 0 1766 0
vsize: 7228
[startup+940.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1413 0 0 0 93988 18 0 0 25 0 1 0 479003961 7532544 1391 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1839 1391 603 41 0 1798 0
vsize: 7356
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1428 0 0 0 94988 18 0 0 25 0 1 0 479003961 7532544 1406 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1839 1406 603 41 0 1798 0
vsize: 7356
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1432 0 0 0 95988 18 0 0 25 0 1 0 479003961 7667712 1410 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1872 1410 603 41 0 1831 0
vsize: 7488
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1432 0 0 0 96988 18 0 0 25 0 1 0 479003961 7663616 1410 4294967295 134512640 134672761 3221224640 3221223808 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1410 603 41 0 1830 0
vsize: 7484
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1436 0 0 0 97988 18 0 0 25 0 1 0 479003961 7663616 1414 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+990.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1436 0 0 0 98988 18 0 0 25 0 1 0 479003961 7663616 1414 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1436 0 0 0 99989 18 0 0 25 0 1 0 479003961 7663616 1414 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1436 0 0 0 100989 18 0 0 25 0 1 0 479003961 7663616 1414 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1436 0 0 0 101989 18 0 0 25 0 1 0 479003961 7663616 1414 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 102989 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223824 134558341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 103989 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 104990 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 105990 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223776 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 106990 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 107990 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223840 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 108990 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 109990 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 110991 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 111991 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 112991 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 113991 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 114991 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223824 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1437 0 0 0 115992 19 0 0 25 0 1 0 479003961 7663616 1415 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1442 0 0 0 116992 19 0 0 25 0 1 0 479003961 7663616 1420 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1442 0 0 0 117992 19 0 0 25 0 1 0 479003961 7663616 1420 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1442 0 0 0 118992 19 0 0 25 0 1 0 479003961 7663616 1420 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31642
Raw data (stat): 31585 (minisat+) R 31584 28546 28545 0 -1 0 1448 0 0 0 119992 19 0 0 25 0 1 0 479003961 7663616 1426 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1426 603 41 0 1830 0
vsize: 7484
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31642
Raw data (stat): 31585 (minisat+) Z 31584 28546 28545 0 -1 12 1450 0 0 0 119992 19 0 0 25 0 1 0 479003961 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: 0
Real time (s): 1200.03
CPU time (s): 1200.13
CPU user time (s): 1199.93
CPU system time (s): 0.19697
CPU usage (%): 100.008
Max. virtual memory (Kb): 7488
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####