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-3.opb
MD5SUM	3d08363a486acbc90a149ca8c58297b8
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	6352
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	6352
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	6352
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	6352
Total number of constraints	13473
Number of constraints which are clauses	13473
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	1
Maximum length of a constraint	3
Trace number 5549

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-14 00:26:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3968 boxname=wulflinc26 idbench=208 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3d08363a486acbc90a149ca8c58297b8  /oldhome/oroussel/tmp/wulflinc26/normalized-par32-3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc26/normalized-par32-3.opb /oldhome/oroussel/tmp/wulflinc26/normalized-par32-3.opb
IDLAUNCH: 3968
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        838536 kB
Buffers:         34796 kB
Cached:         120964 kB
SwapCached:       2476 kB
Active:          55096 kB
Inactive:       106084 kB
HighTotal:      131008 kB
HighFree:         6888 kB
LowTotal:       903652 kB
LowFree:        831648 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29420 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:46:27 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 3968 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 13063 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9707    24214 |    2912       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4790          
c   -- var.elim.:  2000/4790          
c   -- var.elim.:  3000/4790          
c   -- var.elim.:  4000/4790          
c   -- var.elim.:  4790/4790          
c |         0 |    9707    24214 |    3882       0        0     nan |  0.000 % |
c |       100 |    9707    24214 |    4271     100     1109    11.1 | 24.591 % |
c |       250 |    9707    24214 |    4698     250     5290    21.2 | 24.591 % |
c |       476 |    9707    24214 |    5168     476    14358    30.2 | 24.591 % |
c |       814 |    9707    2#### 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.93 0.90 2/54 28237
Raw data (stat): 28237 (runsolver) R 28236 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480264804 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.9999 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 1564 0 0 0 994 3 0 0 25 0 1 0 480264804 7946240 1504 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1940 1504 603 41 0 1899 0
vsize: 7760
[startup+19.9998 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 1684 0 0 0 1994 4 0 0 25 0 1 0 480264804 8343552 1624 4294967295 134512640 134672761 3221224560 3221223600 134612696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2037 1624 603 41 0 1996 0
vsize: 8148
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 1718 0 0 0 2994 4 0 0 25 0 1 0 480264804 8482816 1658 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2071 1658 603 41 0 2030 0
vsize: 8284
[startup+39.9999 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 1851 0 0 0 3994 4 0 0 25 0 1 0 480264804 9019392 1791 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2202 1791 603 41 0 2161 0
vsize: 8808
[startup+49.9999 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 1968 0 0 0 4994 5 0 0 25 0 1 0 480264804 9551872 1908 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2332 1908 603 41 0 2291 0
vsize: 9328
[startup+60.0006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2168 0 0 0 5993 5 0 0 25 0 1 0 480264804 10346496 2108 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2526 2108 603 41 0 2485 0
vsize: 10104
[startup+70.0003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2311 0 0 0 6993 6 0 0 25 0 1 0 480264804 10973184 2251 4294967295 134512640 134672761 3221224560 3221223744 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2679 2251 603 41 0 2638 0
vsize: 10716
[startup+80.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2527 0 0 0 7993 6 0 0 25 0 1 0 480264804 11853824 2467 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2894 2467 603 41 0 2853 0
vsize: 11576
[startup+90.0006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2527 0 0 0 8993 6 0 0 25 0 1 0 480264804 11853824 2467 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2894 2467 603 41 0 2853 0
vsize: 11576
[startup+100 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2542 0 0 0 9993 6 0 0 25 0 1 0 480264804 11853824 2482 4294967295 134512640 134672761 3221224560 3221223744 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2894 2482 603 41 0 2853 0
vsize: 11576
[startup+110.001 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2555 0 0 0 10993 6 0 0 25 0 1 0 480264804 11968512 2495 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2922 2495 603 41 0 2881 0
vsize: 11688
[startup+120.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2571 0 0 0 11993 6 0 0 25 0 1 0 480264804 11968512 2511 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2922 2511 603 41 0 2881 0
vsize: 11688
[startup+130.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2680 0 0 0 12993 7 0 0 25 0 1 0 480264804 12550144 2620 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3064 2620 603 41 0 3023 0
vsize: 12256
[startup+140.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2690 0 0 0 13993 7 0 0 25 0 1 0 480264804 12582912 2629 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3072 2629 603 41 0 3031 0
vsize: 12288
[startup+150.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2694 0 0 0 14994 7 0 0 25 0 1 0 480264804 12582912 2633 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3072 2633 603 41 0 3031 0
vsize: 12288
[startup+160.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2728 0 0 0 15994 7 0 0 25 0 1 0 480264804 12750848 2666 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3113 2666 603 41 0 3072 0
vsize: 12452
[startup+170.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2753 0 0 0 16994 7 0 0 25 0 1 0 480264804 12849152 2691 4294967295 134512640 134672761 3221224560 3221223696 134614664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3137 2691 603 41 0 3096 0
vsize: 12548
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2762 0 0 0 17995 7 0 0 25 0 1 0 480264804 12881920 2699 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3145 2699 603 41 0 3104 0
vsize: 12580
[startup+190.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2849 0 0 0 18995 7 0 0 25 0 1 0 480264804 13283328 2786 4294967295 134512640 134672761 3221224560 3221223744 134615538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3243 2786 603 41 0 3202 0
vsize: 12972
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2892 0 0 0 19995 7 0 0 25 0 1 0 480264804 13398016 2829 4294967295 134512640 134672761 3221224560 3221223696 134614685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2829 603 41 0 3230 0
vsize: 13084
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2916 0 0 0 20995 7 0 0 25 0 1 0 480264804 13488128 2853 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3293 2853 603 41 0 3252 0
vsize: 13172
[startup+220.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2932 0 0 0 21995 7 0 0 25 0 1 0 480264804 13553664 2868 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3309 2868 603 41 0 3268 0
vsize: 13236
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2932 0 0 0 22995 7 0 0 25 0 1 0 480264804 13553664 2868 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3309 2868 603 41 0 3268 0
vsize: 13236
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2932 0 0 0 23995 7 0 0 25 0 1 0 480264804 13553664 2868 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3309 2868 603 41 0 3268 0
vsize: 13236
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2945 0 0 0 24996 7 0 0 25 0 1 0 480264804 13602816 2880 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2880 603 41 0 3280 0
vsize: 13284
[startup+260.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2945 0 0 0 25996 7 0 0 25 0 1 0 480264804 13602816 2880 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2880 603 41 0 3280 0
vsize: 13284
[startup+270.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 2999 0 0 0 26996 7 0 0 25 0 1 0 480264804 13824000 2934 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3375 2934 603 41 0 3334 0
vsize: 13500
[startup+280.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3017 0 0 0 27996 8 0 0 25 0 1 0 480264804 13922304 2952 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3399 2952 603 41 0 3358 0
vsize: 13596
[startup+290.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3017 0 0 0 28996 8 0 0 25 0 1 0 480264804 13922304 2952 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3399 2952 603 41 0 3358 0
vsize: 13596
[startup+300.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3038 0 0 0 29996 8 0 0 25 0 1 0 480264804 13991936 2973 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3416 2973 603 41 0 3375 0
vsize: 13664
[startup+310.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3038 0 0 0 30996 8 0 0 25 0 1 0 480264804 13991936 2973 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3416 2973 603 41 0 3375 0
vsize: 13664
[startup+320.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3038 0 0 0 31996 8 0 0 25 0 1 0 480264804 13991936 2973 4294967295 134512640 134672761 3221224560 3221223732 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3416 2973 603 41 0 3375 0
vsize: 13664
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3038 0 0 0 32997 8 0 0 25 0 1 0 480264804 13991936 2973 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3416 2973 603 41 0 3375 0
vsize: 13664
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3039 0 0 0 33997 8 0 0 25 0 1 0 480264804 13987840 2973 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3415 2973 603 41 0 3374 0
vsize: 13660
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3049 0 0 0 34997 8 0 0 25 0 1 0 480264804 13987840 2983 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3415 2983 603 41 0 3374 0
vsize: 13660
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3079 0 0 0 35997 8 0 0 25 0 1 0 480264804 14155776 3012 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3456 3012 603 41 0 3415 0
vsize: 13824
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3148 0 0 0 36997 8 0 0 25 0 1 0 480264804 14434304 3080 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3524 3080 603 41 0 3483 0
vsize: 14096
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3148 0 0 0 37998 8 0 0 25 0 1 0 480264804 14434304 3080 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3524 3080 603 41 0 3483 0
vsize: 14096
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3148 0 0 0 38998 8 0 0 25 0 1 0 480264804 14434304 3080 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3524 3080 603 41 0 3483 0
vsize: 14096
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3148 0 0 0 39998 8 0 0 25 0 1 0 480264804 14434304 3080 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3524 3080 603 41 0 3483 0
vsize: 14096
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3165 0 0 0 40998 8 0 0 25 0 1 0 480264804 14499840 3096 4294967295 134512640 134672761 3221224560 3221223760 134610644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3540 3096 603 41 0 3499 0
vsize: 14160
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3165 0 0 0 41998 8 0 0 25 0 1 0 480264804 14499840 3096 4294967295 134512640 134672761 3221224560 3221223744 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3540 3096 603 41 0 3499 0
vsize: 14160
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3165 0 0 0 42999 8 0 0 25 0 1 0 480264804 14499840 3096 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3540 3096 603 41 0 3499 0
vsize: 14160
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3165 0 0 0 43999 8 0 0 25 0 1 0 480264804 14499840 3096 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3540 3096 603 41 0 3499 0
vsize: 14160
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3165 0 0 0 44999 8 0 0 25 0 1 0 480264804 14499840 3096 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3540 3096 603 41 0 3499 0
vsize: 14160
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3165 0 0 0 45999 8 0 0 25 0 1 0 480264804 14499840 3096 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3540 3096 603 41 0 3499 0
vsize: 14160
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3195 0 0 0 46999 8 0 0 25 0 1 0 480264804 14696448 3126 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3588 3126 603 41 0 3547 0
vsize: 14352
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3195 0 0 0 47999 8 0 0 25 0 1 0 480264804 14696448 3126 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3588 3126 603 41 0 3547 0
vsize: 14352
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3229 0 0 0 48999 8 0 0 25 0 1 0 480264804 14766080 3160 4294967295 134512640 134672761 3221224560 3221223696 134614741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3605 3160 603 41 0 3564 0
vsize: 14420
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3229 0 0 0 50000 8 0 0 25 0 1 0 480264804 14766080 3160 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3605 3160 603 41 0 3564 0
vsize: 14420
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3244 0 0 0 51000 8 0 0 25 0 1 0 480264804 14962688 3175 4294967295 134512640 134672761 3221224560 3221223616 134644281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3175 603 41 0 3612 0
vsize: 14612
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3244 0 0 0 52000 8 0 0 25 0 1 0 480264804 14831616 3174 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3621 3174 603 41 0 3580 0
vsize: 14484
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3244 0 0 0 53000 8 0 0 25 0 1 0 480264804 14831616 3174 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3621 3174 603 41 0 3580 0
vsize: 14484
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3262 0 0 0 54000 8 0 0 25 0 1 0 480264804 14897152 3191 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3637 3191 603 41 0 3596 0
vsize: 14548
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3262 0 0 0 55000 8 0 0 25 0 1 0 480264804 14897152 3191 4294967295 134512640 134672761 3221224560 3221223696 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3637 3191 603 41 0 3596 0
vsize: 14548
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3278 0 0 0 56000 8 0 0 25 0 1 0 480264804 14962688 3206 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3206 603 41 0 3612 0
vsize: 14612
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3278 0 0 0 57001 8 0 0 25 0 1 0 480264804 14962688 3206 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3206 603 41 0 3612 0
vsize: 14612
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3278 0 0 0 58001 8 0 0 25 0 1 0 480264804 14962688 3206 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3206 603 41 0 3612 0
vsize: 14612
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3278 0 0 0 59001 8 0 0 25 0 1 0 480264804 14962688 3206 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3206 603 41 0 3612 0
vsize: 14612
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3278 0 0 0 60001 8 0 0 25 0 1 0 480264804 14962688 3206 4294967295 134512640 134672761 3221224560 3221223616 134644260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3206 603 41 0 3612 0
vsize: 14612
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3278 0 0 0 61002 8 0 0 25 0 1 0 480264804 14962688 3206 4294967295 134512640 134672761 3221224560 3221223600 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3206 603 41 0 3612 0
vsize: 14612
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3278 0 0 0 62002 8 0 0 25 0 1 0 480264804 14962688 3206 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3206 603 41 0 3612 0
vsize: 14612
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3279 0 0 0 63002 8 0 0 25 0 1 0 480264804 14962688 3207 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3207 603 41 0 3612 0
vsize: 14612
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3279 0 0 0 64002 8 0 0 25 0 1 0 480264804 14962688 3207 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3653 3207 603 41 0 3612 0
vsize: 14612
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3303 0 0 0 65002 8 0 0 25 0 1 0 480264804 15093760 3231 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3685 3231 603 41 0 3644 0
vsize: 14740
[startup+660.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3303 0 0 0 66002 8 0 0 25 0 1 0 480264804 15093760 3231 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3685 3231 603 41 0 3644 0
vsize: 14740
[startup+670.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3320 0 0 0 67004 8 0 0 25 0 1 0 480264804 15159296 3247 4294967295 134512640 134672761 3221224560 3221223760 134610528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3247 603 41 0 3660 0
vsize: 14804
[startup+680.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3320 0 0 0 68004 8 0 0 25 0 1 0 480264804 15159296 3247 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3247 603 41 0 3660 0
vsize: 14804
[startup+690.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3320 0 0 0 69005 8 0 0 25 0 1 0 480264804 15159296 3247 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3247 603 41 0 3660 0
vsize: 14804
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3320 0 0 0 70005 8 0 0 25 0 1 0 480264804 15159296 3247 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3247 603 41 0 3660 0
vsize: 14804
[startup+710.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3320 0 0 0 71005 8 0 0 25 0 1 0 480264804 15159296 3247 4294967295 134512640 134672761 3221224560 3221223760 134610669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3247 603 41 0 3660 0
vsize: 14804
[startup+720.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 72005 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+730.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 73005 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+740.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 74006 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223696 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 75006 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 76006 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 77006 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223696 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 78006 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 79006 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+800.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 80007 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 81007 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3325 0 0 0 82007 8 0 0 25 0 1 0 480264804 15159296 3252 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3252 603 41 0 3660 0
vsize: 14804
[startup+830.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3326 0 0 0 83008 8 0 0 25 0 1 0 480264804 15159296 3253 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3253 603 41 0 3660 0
vsize: 14804
[startup+840.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3326 0 0 0 84008 8 0 0 25 0 1 0 480264804 15159296 3253 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3253 603 41 0 3660 0
vsize: 14804
[startup+850.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3326 0 0 0 85008 8 0 0 25 0 1 0 480264804 15159296 3253 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3253 603 41 0 3660 0
vsize: 14804
[startup+860.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3336 0 0 0 86008 8 0 0 25 0 1 0 480264804 15192064 3262 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3709 3262 603 41 0 3668 0
vsize: 14836
[startup+870.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3336 0 0 0 87008 8 0 0 25 0 1 0 480264804 15192064 3262 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3709 3262 603 41 0 3668 0
vsize: 14836
[startup+880.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3336 0 0 0 88009 8 0 0 25 0 1 0 480264804 15192064 3262 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3709 3262 603 41 0 3668 0
vsize: 14836
[startup+890.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3336 0 0 0 89009 8 0 0 25 0 1 0 480264804 15192064 3262 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3709 3262 603 41 0 3668 0
vsize: 14836
[startup+900.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3336 0 0 0 90009 8 0 0 25 0 1 0 480264804 15192064 3262 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3709 3262 603 41 0 3668 0
vsize: 14836
[startup+910.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3352 0 0 0 91009 9 0 0 25 0 1 0 480264804 15257600 3277 4294967295 134512640 134672761 3221224560 3221223696 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3277 603 41 0 3684 0
vsize: 14900
[startup+920.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3352 0 0 0 92009 9 0 0 25 0 1 0 480264804 15257600 3277 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3277 603 41 0 3684 0
vsize: 14900
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3352 0 0 0 93010 9 0 0 25 0 1 0 480264804 15257600 3277 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3277 603 41 0 3684 0
vsize: 14900
[startup+940.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3352 0 0 0 94010 9 0 0 25 0 1 0 480264804 15257600 3277 4294967295 134512640 134672761 3221224560 3221223760 134610602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3277 603 41 0 3684 0
vsize: 14900
[startup+950.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3352 0 0 0 95010 9 0 0 25 0 1 0 480264804 15257600 3277 4294967295 134512640 134672761 3221224560 3221223744 134615991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3277 603 41 0 3684 0
vsize: 14900
[startup+960.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3352 0 0 0 96010 9 0 0 25 0 1 0 480264804 15257600 3277 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3277 603 41 0 3684 0
vsize: 14900
[startup+970.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 97010 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+980.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 98011 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 99011 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 100011 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 101012 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 102012 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223616 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 103012 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 104012 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 105012 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 106013 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3362 0 0 0 107013 9 0 0 25 0 1 0 480264804 15290368 3286 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3733 3286 603 41 0 3692 0
vsize: 14932
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3378 0 0 0 108013 9 0 0 25 0 1 0 480264804 15355904 3301 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3301 603 41 0 3708 0
vsize: 14996
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3378 0 0 0 109013 9 0 0 25 0 1 0 480264804 15355904 3301 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3301 603 41 0 3708 0
vsize: 14996
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3378 0 0 0 110013 9 0 0 25 0 1 0 480264804 15355904 3301 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3301 603 41 0 3708 0
vsize: 14996
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3383 0 0 0 111014 9 0 0 25 0 1 0 480264804 15355904 3306 4294967295 134512640 134672761 3221224560 3221223744 134615840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3306 603 41 0 3708 0
vsize: 14996
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3383 0 0 0 112014 9 0 0 25 0 1 0 480264804 15355904 3306 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3306 603 41 0 3708 0
vsize: 14996
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3386 0 0 0 113014 9 0 0 25 0 1 0 480264804 15355904 3309 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3309 603 41 0 3708 0
vsize: 14996
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3386 0 0 0 114014 9 0 0 25 0 1 0 480264804 15355904 3309 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3309 603 41 0 3708 0
vsize: 14996
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3386 0 0 0 115014 9 0 0 25 0 1 0 480264804 15355904 3309 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3309 603 41 0 3708 0
vsize: 14996
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3386 0 0 0 116015 9 0 0 25 0 1 0 480264804 15355904 3309 4294967295 134512640 134672761 3221224560 3221223552 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3309 603 41 0 3708 0
vsize: 14996
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3386 0 0 0 117015 9 0 0 25 0 1 0 480264804 15355904 3309 4294967295 134512640 134672761 3221224560 3221223656 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3309 603 41 0 3708 0
vsize: 14996
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3386 0 0 0 118015 9 0 0 25 0 1 0 480264804 15355904 3309 4294967295 134512640 134672761 3221224560 3221223744 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3309 603 41 0 3708 0
vsize: 14996
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3386 0 0 0 119015 9 0 0 25 0 1 0 480264804 15355904 3309 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3309 603 41 0 3708 0
vsize: 14996
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28237
Raw data (stat): 28237 (minisat+) R 28236 22612 22611 0 -1 0 3386 0 0 0 120015 9 0 0 25 0 1 0 480264804 15355904 3309 4294967295 134512640 134672761 3221224560 3221223696 134614488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3749 3309 603 41 0 3708 0
vsize: 14996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 28237
Raw data (stat): 28237 (minisat+) Z 28236 22612 22611 0 -1 12 3386 0 0 0 120015 9 0 0 25 0 1 0 480264804 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: 0
Real time (s): 1200.06
CPU time (s): 1200.26
CPU user time (s): 1200.16
CPU system time (s): 0.098984
CPU usage (%): 100.017
Max. virtual memory (Kb): 14996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####