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/aloul/FPGA_SAT05/normalized-fpga45_44_sat_pb.cnf.cr.opb
MD5SUM	c501a04dd091dbe678ec2743021adc30
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	46
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	15.2037
Number of variables	2970
Total number of constraints	2113
Number of constraints which are clauses	2024
Number of constraints which are cardinality constraints (but not clauses)	89
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	22
Maximum length of a constraint	45
Trace number 5404

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-13 23:42:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3816 boxname=wulflinc10 idbench=56 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c501a04dd091dbe678ec2743021adc30  /oldhome/oroussel/tmp/wulflinc10/normalized-fpga45_44_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc10/normalized-fpga45_44_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc10/normalized-fpga45_44_sat_pb.cnf.cr.opb
IDLAUNCH: 3816
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        881456 kB
Buffers:         34496 kB
Cached:          99164 kB
SwapCached:        164 kB
Active:          51948 kB
Inactive:        84752 kB
HighTotal:      131008 kB
HighFree:        28168 kB
LowTotal:       903652 kB
LowFree:        853288 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10936 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:02:39 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 3816 7 1200.29 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2113 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  88]---> BDD-cost:   85
c ---[  87]---> BDD-cost:   85
c ---[  86]---> BDD-cost:   85
c ---[  85]---> BDD-cost:   85
c ---[  84]---> BDD-cost:   85
c ---[  83]---> BDD-cost:   85
c ---[  82]---> BDD-cost:   85
c ---[  81]---> BDD-cost:   85
c ---[  80]---> BDD-cost:   85
c ---[  79]---> BDD-cost:   85
c ---[  78]---> BDD-cost:   85
c ---[  77]---> BDD-cost:   85
c ---[  76]---> BDD-cost:   85
c ---[  75]---> BDD-cost:   85
c ---[  74]---> BDD-cost:   85
c ---[  73]---> BDD-cost:   85
c ---[  72]---> BDD-cost:   85
c ---[  71]---> BDD-cost:   85
c ---[  70]---> BDD-cost:   85
c ---[  69]---> BDD-cost:   85
c ---[  68]---> BDD-cost:   85
c ---[  67]---> BDD-cost:   85
c ---[  66]---> BDD-cost:   85
c ---[  65]---> BDD-cost:   85
c ---[  64]---> BDD-cost:   85
c ---[  63]---> BDD-cost:   85
c ---[  62]---> BDD-cost:   85
c ---[  61]---> BDD-cost:   85
c ---[  60]---> BDD-cost:   85
c ---[  59]---> BDD-cost:   85
c ---[  58]---> BDD-cost:   85
c ---[  57]---> BDD-cost:   85
c ---[  56]---> BDD-cost:   85
c ---[  55]---> BDD-cost:   85
c ---[  54]---> BDD-cost:   85
c ---[  53]---> BDD-cost:   85
c ---[  52]---> BDD-cost:   85
c ---[  51]---> BDD-cost:   85
c ---[  50]---> BDD-cost:   85
c ---[  49]---> BDD-cost:   85
c ---[  48]---> BDD-cost:   85
c ---[  47]---> BDD-cost:   85
c ---[  46]---> BDD-cost:   85
c ---[  45]---> BDD-cost:   85
c ---[  44]---> BDD-cost:   85
c ---[  43]---> BDD-cost:   41
c ---[  42]---> BDD-cost:   41
c ---[  41]---> BDD-cost:   41
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   41
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:   41
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:   41
c ---[  33]---> BDD-cost:   41
c ---[  32]---> BDD-cost:   41
c ---[  31]---> BDD-cost:   41
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 29501
Raw data (stat): 29501 (runsolver) R 29500 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421782982 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 3903 0 0 0 990 8 0 0 25 0 1 0 421782982 17797120 3832 4294967295 134512640 134672761 3221224528 3221223712 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4345 3834 603 41 0 4304 0
vsize: 17380
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 5771 0 0 0 1985 14 0 0 25 0 1 0 421782982 25468928 5700 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6218 5701 603 41 0 6177 0
vsize: 24872
[startup+30.0016 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 7165 0 0 0 2983 16 0 0 25 0 1 0 421782982 31158272 7094 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7607 7094 603 41 0 7566 0
vsize: 30428
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 8199 0 0 0 3980 18 0 0 25 0 1 0 421782982 35426304 8128 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8649 8128 603 41 0 8608 0
vsize: 34596
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 10521 0 0 0 4976 23 0 0 25 0 1 0 421782982 44924928 10450 4294967295 134512640 134672761 3221224528 3221223568 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10968 10450 603 41 0 10927 0
vsize: 43872
[startup+60.0016 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 10880 0 0 0 5975 24 0 0 25 0 1 0 421782982 46374912 10809 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11322 10809 603 41 0 11281 0
vsize: 45288
[startup+70.0015 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 10880 0 0 0 6976 24 0 0 25 0 1 0 421782982 46374912 10809 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11322 10809 603 41 0 11281 0
vsize: 45288
[startup+80.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 10880 0 0 0 7976 24 0 0 25 0 1 0 421782982 46374912 10809 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11322 10809 603 41 0 11281 0
vsize: 45288
[startup+90.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 10880 0 0 0 8976 24 0 0 25 0 1 0 421782982 46374912 10809 4294967295 134512640 134672761 3221224528 3221223568 134612885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11322 10809 603 41 0 11281 0
vsize: 45288
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 11254 0 0 0 9975 25 0 0 25 0 1 0 421782982 47951872 11183 4294967295 134512640 134672761 3221224528 3221223568 134603529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11707 11183 603 41 0 11666 0
vsize: 46828
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 11813 0 0 0 10975 26 0 0 25 0 1 0 421782982 50208768 11742 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12258 11742 603 41 0 12217 0
vsize: 49032
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 12488 0 0 0 11973 28 0 0 25 0 1 0 421782982 52981760 12417 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12935 12417 603 41 0 12894 0
vsize: 51740
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 13020 0 0 0 12972 29 0 0 25 0 1 0 421782982 55226368 12949 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13483 12949 603 41 0 13442 0
vsize: 53932
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 13248 0 0 0 13972 29 0 0 25 0 1 0 421782982 56160256 13176 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13711 13176 603 41 0 13670 0
vsize: 54844
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 13248 0 0 0 14972 29 0 0 25 0 1 0 421782982 56160256 13176 4294967295 134512640 134672761 3221224528 3221223712 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13711 13176 603 41 0 13670 0
vsize: 54844
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 13248 0 0 0 15972 29 0 0 25 0 1 0 421782982 56160256 13176 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13711 13176 603 41 0 13670 0
vsize: 54844
[startup+170.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 13248 0 0 0 16972 29 0 0 25 0 1 0 421782982 56160256 13176 4294967295 134512640 134672761 3221224528 3221223712 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13711 13176 603 41 0 13670 0
vsize: 54844
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 13503 0 0 0 17972 30 0 0 25 0 1 0 421782982 57221120 13431 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13970 13431 603 41 0 13929 0
vsize: 55880
[startup+190.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 14192 0 0 0 18971 31 0 0 25 0 1 0 421782982 60022784 14119 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14654 14119 603 41 0 14613 0
vsize: 58616
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 14193 0 0 0 19971 31 0 0 25 0 1 0 421782982 60022784 14120 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14654 14120 603 41 0 14613 0
vsize: 58616
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 14193 0 0 0 20971 31 0 0 25 0 1 0 421782982 60022784 14120 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14654 14120 603 41 0 14613 0
vsize: 58616
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 14194 0 0 0 21971 31 0 0 25 0 1 0 421782982 60022784 14121 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14654 14121 603 41 0 14613 0
vsize: 58616
[startup+230.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 14194 0 0 0 22972 31 0 0 25 0 1 0 421782982 60022784 14121 4294967295 134512640 134672761 3221224528 3221223632 134604563 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14654 14121 603 41 0 14613 0
vsize: 58616
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 14194 0 0 0 23972 31 0 0 25 0 1 0 421782982 60022784 14121 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14654 14121 603 41 0 14613 0
vsize: 58616
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 14194 0 0 0 24972 31 0 0 25 0 1 0 421782982 60022784 14121 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14654 14121 603 41 0 14613 0
vsize: 58616
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 15357 0 0 0 25969 35 0 0 25 0 1 0 421782982 64933888 15284 4294967295 134512640 134672761 3221224528 3221223624 134616317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15853 15284 603 41 0 15812 0
vsize: 63412
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 15357 0 0 0 26969 35 0 0 25 0 1 0 421782982 64802816 15283 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15821 15283 603 41 0 15780 0
vsize: 63284
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 15357 0 0 0 27969 35 0 0 25 0 1 0 421782982 64802816 15283 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15821 15283 603 41 0 15780 0
vsize: 63284
[startup+290.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 15357 0 0 0 28969 35 0 0 25 0 1 0 421782982 64802816 15283 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15821 15283 603 41 0 15780 0
vsize: 63284
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 15357 0 0 0 29969 35 0 0 25 0 1 0 421782982 64802816 15283 4294967295 134512640 134672761 3221224528 3221223712 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15821 15283 603 41 0 15780 0
vsize: 63284
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 15357 0 0 0 30970 35 0 0 25 0 1 0 421782982 64802816 15283 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15821 15283 603 41 0 15780 0
vsize: 63284
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 15357 0 0 0 31970 35 0 0 25 0 1 0 421782982 64802816 15283 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15821 15283 603 41 0 15780 0
vsize: 63284
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 15564 0 0 0 32970 35 0 0 25 0 1 0 421782982 65720320 15490 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16045 15490 603 41 0 16004 0
vsize: 64180
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 16242 0 0 0 33969 36 0 0 25 0 1 0 421782982 68493312 16168 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16722 16168 603 41 0 16681 0
vsize: 66888
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 16811 0 0 0 34967 38 0 0 25 0 1 0 421782982 70881280 16737 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17305 16737 603 41 0 17264 0
vsize: 69220
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 17499 0 0 0 35966 39 0 0 25 0 1 0 421782982 73650176 17425 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17981 17425 603 41 0 17940 0
vsize: 71924
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 17639 0 0 0 36966 40 0 0 25 0 1 0 421782982 74186752 17565 4294967295 134512640 134672761 3221224528 3221223568 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18112 17565 603 41 0 18071 0
vsize: 72448
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 17639 0 0 0 37966 40 0 0 25 0 1 0 421782982 74186752 17565 4294967295 134512640 134672761 3221224528 3221223568 134613116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18112 17565 603 41 0 18071 0
vsize: 72448
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 17639 0 0 0 38966 40 0 0 25 0 1 0 421782982 74186752 17565 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18112 17565 603 41 0 18071 0
vsize: 72448
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 17639 0 0 0 39966 40 0 0 25 0 1 0 421782982 74186752 17565 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18112 17565 603 41 0 18071 0
vsize: 72448
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 17639 0 0 0 40966 40 0 0 25 0 1 0 421782982 74186752 17565 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18112 17565 603 41 0 18071 0
vsize: 72448
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 17639 0 0 0 41967 40 0 0 25 0 1 0 421782982 74186752 17565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18112 17565 603 41 0 18071 0
vsize: 72448
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 18232 0 0 0 42966 41 0 0 25 0 1 0 421782982 76660736 18158 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18716 18158 603 41 0 18675 0
vsize: 74864
[startup+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 19238 0 0 0 43964 43 0 0 25 0 1 0 421782982 80773120 19164 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19720 19164 603 41 0 19679 0
vsize: 78880
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 20278 0 0 0 44960 46 0 0 25 0 1 0 421782982 85131264 20204 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20784 20204 603 41 0 20743 0
vsize: 83136
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 20873 0 0 0 45960 47 0 0 25 0 1 0 421782982 87474176 20799 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21356 20799 603 41 0 21315 0
vsize: 85424
[startup+470 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 21586 0 0 0 46958 49 0 0 25 0 1 0 421782982 90386432 21512 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22067 21512 603 41 0 22026 0
vsize: 88268
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22436 0 0 0 47957 51 0 0 25 0 1 0 421782982 93921280 22362 4294967295 134512640 134672761 3221224528 3221223568 134613748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22930 22362 603 41 0 22889 0
vsize: 91720
[startup+490 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22954 0 0 0 48956 52 0 0 25 0 1 0 421782982 95993856 22880 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22880 603 41 0 23395 0
vsize: 93744
[startup+500.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22955 0 0 0 49956 52 0 0 25 0 1 0 421782982 95993856 22881 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22881 603 41 0 23395 0
vsize: 93744
[startup+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22955 0 0 0 50956 52 0 0 25 0 1 0 421782982 95993856 22881 4294967295 134512640 134672761 3221224528 3221223712 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22881 603 41 0 23395 0
vsize: 93744
[startup+520 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22955 0 0 0 51956 52 0 0 25 0 1 0 421782982 95993856 22881 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22881 603 41 0 23395 0
vsize: 93744
[startup+530 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22958 0 0 0 52957 52 0 0 25 0 1 0 421782982 95993856 22884 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22884 603 41 0 23395 0
vsize: 93744
[startup+540 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22959 0 0 0 53957 52 0 0 25 0 1 0 421782982 95993856 22885 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22885 603 41 0 23395 0
vsize: 93744
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22959 0 0 0 54957 52 0 0 25 0 1 0 421782982 95993856 22885 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22885 603 41 0 23395 0
vsize: 93744
[startup+559.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22959 0 0 0 55957 52 0 0 25 0 1 0 421782982 95993856 22885 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22885 603 41 0 23395 0
vsize: 93744
[startup+569.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22959 0 0 0 56957 52 0 0 25 0 1 0 421782982 95993856 22885 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22885 603 41 0 23395 0
vsize: 93744
[startup+579.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22959 0 0 0 57957 52 0 0 25 0 1 0 421782982 95993856 22885 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22885 603 41 0 23395 0
vsize: 93744
[startup+589.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22959 0 0 0 58958 52 0 0 25 0 1 0 421782982 95993856 22885 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22885 603 41 0 23395 0
vsize: 93744
[startup+600 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22960 0 0 0 59958 52 0 0 25 0 1 0 421782982 95993856 22886 4294967295 134512640 134672761 3221224528 3221223568 134612797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22886 603 41 0 23395 0
vsize: 93744
[startup+610 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22960 0 0 0 60958 52 0 0 25 0 1 0 421782982 95993856 22886 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22886 603 41 0 23395 0
vsize: 93744
[startup+620 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22960 0 0 0 61958 52 0 0 25 0 1 0 421782982 95993856 22886 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22886 603 41 0 23395 0
vsize: 93744
[startup+630 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22960 0 0 0 62958 52 0 0 25 0 1 0 421782982 95993856 22886 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22886 603 41 0 23395 0
vsize: 93744
[startup+640 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 22960 0 0 0 63959 52 0 0 25 0 1 0 421782982 95993856 22886 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23436 22886 603 41 0 23395 0
vsize: 93744
[startup+649.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 23847 0 0 0 64957 54 0 0 25 0 1 0 421782982 99692544 23773 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24339 23773 603 41 0 24298 0
vsize: 97356
[startup+660 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 24687 0 0 0 65955 55 0 0 25 0 1 0 421782982 103157760 24613 4294967295 134512640 134672761 3221224528 3221223712 134615649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25185 24613 603 41 0 25144 0
vsize: 100740
[startup+669.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 25035 0 0 0 66955 56 0 0 25 0 1 0 421782982 104615936 24961 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25541 24961 603 41 0 25500 0
vsize: 102164
[startup+679.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 25325 0 0 0 67954 57 0 0 25 0 1 0 421782982 105795584 25251 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25829 25251 603 41 0 25788 0
vsize: 103316
[startup+689.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 25675 0 0 0 68954 57 0 0 25 0 1 0 421782982 107257856 25601 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26186 25601 603 41 0 26145 0
vsize: 104744
[startup+699.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 26200 0 0 0 69953 58 0 0 25 0 1 0 421782982 109379584 26126 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26704 26126 603 41 0 26663 0
vsize: 106816
[startup+709.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 26666 0 0 0 70952 59 0 0 25 0 1 0 421782982 111226880 26592 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27155 26592 603 41 0 27114 0
vsize: 108620
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 27184 0 0 0 71952 60 0 0 25 0 1 0 421782982 113516544 27110 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27714 27110 603 41 0 27673 0
vsize: 110856
[startup+729.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 27733 0 0 0 72951 61 0 0 25 0 1 0 421782982 115785728 27659 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28268 27659 603 41 0 28227 0
vsize: 113072
[startup+739.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 73950 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+749.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 74950 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+759.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 75950 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+769.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 76950 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+779.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 77950 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+789.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 78950 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+799.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 79951 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+809.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 80951 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+819.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 81951 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+829.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 82951 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+839.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 83951 62 0 0 25 0 1 0 421782982 117444608 28094 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28673 28094 603 41 0 28632 0
vsize: 114692
[startup+849.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 84951 62 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+859.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 85952 62 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+869.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 86952 62 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+879.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 87952 62 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223568 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+889.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 88952 62 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+899.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 89952 62 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+909.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 90952 62 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+919.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 91952 63 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+929.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 92952 63 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+939.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 93953 63 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+949.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 94953 63 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223568 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+959.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 95953 63 0 0 25 0 1 0 421782982 117334016 28067 4294967295 134512640 134672761 3221224528 3221223584 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28646 28067 603 41 0 28605 0
vsize: 114584
[startup+969.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 96953 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+979.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 97953 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+989.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 98953 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+999.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 99954 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 100954 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 101954 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 102954 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29501
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 103954 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1049.99 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 29542
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 104954 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1060.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29554
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 105958 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1070.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29554
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 106958 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1080.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29554
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 107958 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1090.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29554
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 108958 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1100.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29554
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 109958 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1110.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29554
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 110958 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1120.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29554
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 111959 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1130.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29556
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 112959 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1140.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29556
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 113959 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223508 1075351210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1150.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29556
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 114959 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223568 134612507 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1160.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29556
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 115959 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1170.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29556
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 116960 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1180.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29556
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 117960 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29556
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 118960 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29556
Raw data (stat): 29501 (minisat+) R 29500 25347 25346 0 -1 0 28168 0 0 0 119960 63 0 0 25 0 1 0 421782982 117084160 28006 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28585 28006 603 41 0 28544 0
vsize: 114340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 29556
Raw data (stat): 29501 (minisat+) Z 29500 25347 25346 0 -1 12 28168 0 0 0 119960 68 0 0 25 0 1 0 421782982 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.08
CPU time (s): 1200.29
CPU user time (s): 1199.61
CPU system time (s): 0.683896
CPU usage (%): 100.018
Max. virtual memory (Kb): 114692
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####