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_43_sat_pb.cnf.cr.opb
MD5SUM	f711bed5ebfe5c735a8c12d953afb97c
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	9.61454
Number of variables	2903
Total number of constraints	2066
Number of constraints which are clauses	1978
Number of constraints which are cardinality constraints (but not clauses)	88
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 5403

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-13 23:41:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3815 boxname=wulflinc32 idbench=55 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f711bed5ebfe5c735a8c12d953afb97c  /oldhome/oroussel/tmp/wulflinc32/normalized-fpga45_43_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc32/normalized-fpga45_43_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc32/normalized-fpga45_43_sat_pb.cnf.cr.opb
IDLAUNCH: 3815
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        710236 kB
Buffers:         34256 kB
Cached:         178596 kB
SwapCached:       1212 kB
Active:         144876 kB
Inactive:       148296 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        709980 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2244 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25472 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:01:48 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 3815 7 1200.32 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2066 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  87]---> BDD-cost:   83
c ---[  86]---> BDD-cost:   83
c ---[  85]---> BDD-cost:   83
c ---[  84]---> BDD-cost:   83
c ---[  83]---> BDD-cost:   83
c ---[  82]---> BDD-cost:   83
c ---[  81]---> BDD-cost:   83
c ---[  80]---> BDD-cost:   83
c ---[  79]---> BDD-cost:   83
c ---[  78]---> BDD-cost:   83
c ---[  77]---> BDD-cost:   83
c ---[  76]---> BDD-cost:   83
c ---[  75]---> BDD-cost:   83
c ---[  74]---> BDD-cost:   83
c ---[  73]---> BDD-cost:   83
c ---[  72]---> BDD-cost:   83
c ---[  71]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   83
c ---[  69]---> BDD-cost:   83
c ---[  68]---> BDD-cost:   83
c ---[  67]---> BDD-cost:   83
c ---[  66]---> BDD-cost:   83
c ---[  65]---> BDD-cost:   83
c ---[  64]---> BDD-cost:   83
c ---[  63]---> BDD-cost:   83
c ---[  62]---> BDD-cost:   83
c ---[  61]---> BDD-cost:   83
c ---[  60]---> BDD-cost:   83
c ---[  59]---> BDD-cost:   83
c ---[  58]---> BDD-cost:   83
c ---[  57]---> BDD-cost:   83
c ---[  56]---> BDD-cost:   83
c ---[  55]---> BDD-cost:   83
c ---[  54]---> BDD-cost:   83
c ---[  53]---> BDD-cost:   83
c ---[  52]---> BDD-cost:   83
c ---[  51]---> BDD-cost:   83
c ---[  50]---> BDD-cost:   83
c ---[  49]---> BDD-cost:   83
c ---[  48]---> BDD-cost:   83
c ---[  47]---> BDD-cost:   83
c ---[  46]---> BDD-cost:   83
c ---[  45]---> BDD-cost:   83
c ---[  44]---> BDD-cost:   83
c ---[  43]---> BDD-cost:   83
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-cost:   41
c ---[  27]---> BDD-cost:   41
c ---[  26]---> BDD-cost:   41
c --#### 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.73 0.91 0.89 2/53 13105
Raw data (stat): 13105 (runsolver) R 13104 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479987629 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.77 0.91 0.89 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 3839 0 0 0 988 10 0 0 25 0 1 0 479987629 17698816 3802 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4321 3802 603 41 0 4280 0
vsize: 17284
[startup+20.0022 s]
Raw data (loadavg): 0.81 0.91 0.89 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 6226 0 0 0 1983 16 0 0 25 0 1 0 479987629 27480064 6189 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6709 6189 603 41 0 6668 0
vsize: 26836
[startup+30.0029 s]
Raw data (loadavg): 0.84 0.92 0.89 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 7506 0 0 0 2980 18 0 0 25 0 1 0 479987629 32645120 7469 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7970 7469 603 41 0 7929 0
vsize: 31880
[startup+40.0037 s]
Raw data (loadavg): 0.86 0.92 0.89 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 8502 0 0 0 3978 21 0 0 25 0 1 0 479987629 36880384 8465 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8465 603 41 0 8963 0
vsize: 36016
[startup+50.0045 s]
Raw data (loadavg): 0.88 0.92 0.89 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 10356 0 0 0 4974 25 0 0 25 0 1 0 479987629 44453888 10319 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10853 10319 603 41 0 10812 0
vsize: 43412
[startup+60.0052 s]
Raw data (loadavg): 0.90 0.92 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 10770 0 0 0 5973 26 0 0 25 0 1 0 479987629 46080000 10732 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11250 10732 603 41 0 11209 0
vsize: 45000
[startup+70.006 s]
Raw data (loadavg): 0.91 0.92 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 10770 0 0 0 6973 26 0 0 25 0 1 0 479987629 46080000 10732 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11250 10732 603 41 0 11209 0
vsize: 45000
[startup+80.0068 s]
Raw data (loadavg): 0.93 0.93 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 10770 0 0 0 7973 26 0 0 25 0 1 0 479987629 46080000 10732 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11250 10732 603 41 0 11209 0
vsize: 45000
[startup+90.0075 s]
Raw data (loadavg): 0.94 0.93 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 10770 0 0 0 8973 26 0 0 25 0 1 0 479987629 46075904 10731 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11249 10731 603 41 0 11208 0
vsize: 44996
[startup+100.008 s]
Raw data (loadavg): 0.95 0.93 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 10770 0 0 0 9974 26 0 0 25 0 1 0 479987629 46075904 10731 4294967295 134512640 134672761 3221224528 3221223516 1075347104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11249 10731 603 41 0 11208 0
vsize: 44996
[startup+110.009 s]
Raw data (loadavg): 0.95 0.93 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 11247 0 0 0 10972 28 0 0 25 0 1 0 479987629 48074752 11208 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11737 11208 603 41 0 11696 0
vsize: 46948
[startup+120.01 s]
Raw data (loadavg): 0.96 0.93 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 11378 0 0 0 11972 28 0 0 25 0 1 0 479987629 48541696 11339 4294967295 134512640 134672761 3221224528 3221223568 134612595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11851 11339 603 41 0 11810 0
vsize: 47404
[startup+130.011 s]
Raw data (loadavg): 0.97 0.94 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 11379 0 0 0 12972 28 0 0 25 0 1 0 479987629 48541696 11340 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11851 11340 603 41 0 11810 0
vsize: 47404
[startup+140.011 s]
Raw data (loadavg): 0.97 0.94 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 11379 0 0 0 13973 28 0 0 25 0 1 0 479987629 48541696 11340 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11851 11340 603 41 0 11810 0
vsize: 47404
[startup+150.012 s]
Raw data (loadavg): 0.98 0.94 0.90 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 11379 0 0 0 14973 29 0 0 25 0 1 0 479987629 48541696 11340 4294967295 134512640 134672761 3221224528 3221223712 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11851 11340 603 41 0 11810 0
vsize: 47404
[startup+160.013 s]
Raw data (loadavg): 0.98 0.94 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12466 0 0 0 15971 31 0 0 25 0 1 0 479987629 53047296 12427 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12951 12427 603 41 0 12910 0
vsize: 51804
[startup+170.014 s]
Raw data (loadavg): 0.98 0.94 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12959 0 0 0 16970 32 0 0 25 0 1 0 479987629 55058432 12919 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13442 12919 603 41 0 13401 0
vsize: 53768
[startup+180.014 s]
Raw data (loadavg): 0.98 0.94 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12959 0 0 0 17970 32 0 0 25 0 1 0 479987629 55058432 12919 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13442 12919 603 41 0 13401 0
vsize: 53768
[startup+190.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12960 0 0 0 18970 32 0 0 25 0 1 0 479987629 55058432 12920 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13442 12920 603 41 0 13401 0
vsize: 53768
[startup+200.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12961 0 0 0 19970 32 0 0 25 0 1 0 479987629 55058432 12921 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13442 12921 603 41 0 13401 0
vsize: 53768
[startup+210.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12961 0 0 0 20971 32 0 0 25 0 1 0 479987629 55058432 12921 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13442 12921 603 41 0 13401 0
vsize: 53768
[startup+220.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12961 0 0 0 21971 32 0 0 25 0 1 0 479987629 55058432 12921 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13442 12921 603 41 0 13401 0
vsize: 53768
[startup+230.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12963 0 0 0 22971 32 0 0 25 0 1 0 479987629 55058432 12923 4294967295 134512640 134672761 3221224528 3221223520 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13442 12923 603 41 0 13401 0
vsize: 53768
[startup+240.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 12963 0 0 0 23971 32 0 0 25 0 1 0 479987629 55058432 12923 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13442 12923 603 41 0 13401 0
vsize: 53768
[startup+250.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 13053 0 0 0 24971 33 0 0 25 0 1 0 479987629 55455744 13013 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13539 13013 603 41 0 13498 0
vsize: 54156
[startup+260.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 13432 0 0 0 25971 33 0 0 25 0 1 0 479987629 57110528 13392 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13943 13392 603 41 0 13902 0
vsize: 55772
[startup+270.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 13918 0 0 0 26970 34 0 0 25 0 1 0 479987629 59105280 13878 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14430 13878 603 41 0 14389 0
vsize: 57720
[startup+280.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 14691 0 0 0 27969 36 0 0 25 0 1 0 479987629 62365696 14651 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15226 14651 603 41 0 15185 0
vsize: 60904
[startup+290.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15536 0 0 0 28967 38 0 0 25 0 1 0 479987629 65814528 15496 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16068 15496 603 41 0 16027 0
vsize: 64272
[startup+300.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15846 0 0 0 29966 39 0 0 25 0 1 0 479987629 67002368 15805 4294967295 134512640 134672761 3221224528 3221223712 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16358 15805 603 41 0 16317 0
vsize: 65432
[startup+310.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15846 0 0 0 30966 39 0 0 25 0 1 0 479987629 67002368 15805 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16358 15805 603 41 0 16317 0
vsize: 65432
[startup+320.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15846 0 0 0 31967 39 0 0 25 0 1 0 479987629 67002368 15805 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16358 15805 603 41 0 16317 0
vsize: 65432
[startup+330.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15846 0 0 0 32967 39 0 0 25 0 1 0 479987629 67002368 15805 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16358 15805 603 41 0 16317 0
vsize: 65432
[startup+340.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15846 0 0 0 33967 39 0 0 25 0 1 0 479987629 67002368 15805 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16358 15805 603 41 0 16317 0
vsize: 65432
[startup+350.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15846 0 0 0 34967 39 0 0 25 0 1 0 479987629 67002368 15805 4294967295 134512640 134672761 3221224528 3221223568 134612578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16358 15805 603 41 0 16317 0
vsize: 65432
[startup+360.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15846 0 0 0 35968 39 0 0 25 0 1 0 479987629 67002368 15805 4294967295 134512640 134672761 3221224528 3221223664 134614685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16358 15805 603 41 0 16317 0
vsize: 65432
[startup+370.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 36968 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+380.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 37968 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+390.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 38968 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+400.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 39969 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+410.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 40969 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 41969 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 42969 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+440.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 43969 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 44970 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+460.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 45970 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 46970 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 47970 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+490.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 48971 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223568 134612571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+500.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 49971 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 50971 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+520.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 51971 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+530.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 52971 39 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 53972 40 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+550.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 54972 40 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+560.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 55972 40 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223464 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+570.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15849 0 0 0 56972 40 0 0 25 0 1 0 479987629 66920448 15791 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15791 603 41 0 16297 0
vsize: 65352
[startup+580.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 57973 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+590.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 58973 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+600.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 59973 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+610.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 60973 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+620.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 61973 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223692 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+630.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 62974 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+640.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 63974 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+650.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 64974 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+660.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 65974 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+670.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 66975 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+680.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 67975 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+690.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 68975 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+700.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 69975 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+710.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 70975 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+720.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 71976 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+730.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15850 0 0 0 72976 40 0 0 25 0 1 0 479987629 66920448 15792 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16338 15792 603 41 0 16297 0
vsize: 65352
[startup+740.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 15930 0 0 0 73976 40 0 0 25 0 1 0 479987629 67313664 15872 4294967295 134512640 134672761 3221224528 3221223568 134612848 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16434 15872 603 41 0 16393 0
vsize: 65736
[startup+750.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 16298 0 0 0 74976 41 0 0 25 0 1 0 479987629 68767744 16240 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16789 16240 603 41 0 16748 0
vsize: 67156
[startup+760.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 16568 0 0 0 75975 42 0 0 25 0 1 0 479987629 69955584 16510 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 16510 603 41 0 17038 0
vsize: 68316
[startup+770.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 16912 0 0 0 76974 43 0 0 25 0 1 0 479987629 71430144 16854 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17439 16854 603 41 0 17398 0
vsize: 69756
[startup+780.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 17213 0 0 0 77974 44 0 0 25 0 1 0 479987629 72626176 17155 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17731 17155 603 41 0 17690 0
vsize: 70924
[startup+790.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 17520 0 0 0 78973 44 0 0 25 0 1 0 479987629 73924608 17462 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18048 17462 603 41 0 18007 0
vsize: 72192
[startup+800.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 17784 0 0 0 79973 45 0 0 25 0 1 0 479987629 74985472 17726 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18307 17726 603 41 0 18266 0
vsize: 73228
[startup+810.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18166 0 0 0 80972 46 0 0 25 0 1 0 479987629 76566528 18108 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18693 18108 603 41 0 18652 0
vsize: 74772
[startup+820.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18439 0 0 0 81972 47 0 0 25 0 1 0 479987629 77701120 18381 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18970 18381 603 41 0 18929 0
vsize: 75880
[startup+830.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18783 0 0 0 82971 48 0 0 25 0 1 0 479987629 79151104 18725 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19324 18725 603 41 0 19283 0
vsize: 77296
[startup+840.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18853 0 0 0 83971 48 0 0 25 0 1 0 479987629 79224832 18762 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19342 18762 603 41 0 19301 0
vsize: 77368
[startup+850.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18853 0 0 0 84971 48 0 0 25 0 1 0 479987629 79224832 18762 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19342 18762 603 41 0 19301 0
vsize: 77368
[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18853 0 0 0 85972 48 0 0 25 0 1 0 479987629 79224832 18762 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19342 18762 603 41 0 19301 0
vsize: 77368
[startup+870.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18853 0 0 0 86972 48 0 0 25 0 1 0 479987629 79224832 18762 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19342 18762 603 41 0 19301 0
vsize: 77368
[startup+880.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18853 0 0 0 87972 48 0 0 25 0 1 0 479987629 79224832 18762 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19342 18762 603 41 0 19301 0
vsize: 77368
[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18863 0 0 0 88972 48 0 0 25 0 1 0 479987629 79421440 18772 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19390 18772 603 41 0 19349 0
vsize: 77560
[startup+900.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18864 0 0 0 89972 48 0 0 25 0 1 0 479987629 79421440 18773 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19390 18773 603 41 0 19349 0
vsize: 77560
[startup+910.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18878 0 0 0 90972 48 0 0 25 0 1 0 479987629 79421440 18787 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19390 18787 603 41 0 19349 0
vsize: 77560
[startup+920.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18879 0 0 0 91973 48 0 0 25 0 1 0 479987629 79421440 18788 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19390 18788 603 41 0 19349 0
vsize: 77560
[startup+930.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18879 0 0 0 92973 48 0 0 25 0 1 0 479987629 79421440 18788 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19390 18788 603 41 0 19349 0
vsize: 77560
[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18879 0 0 0 93973 48 0 0 25 0 1 0 479987629 79421440 18788 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19390 18788 603 41 0 19349 0
vsize: 77560
[startup+950.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18901 0 0 0 94973 48 0 0 25 0 1 0 479987629 79618048 18810 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19438 18810 603 41 0 19397 0
vsize: 77752
[startup+960.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18913 0 0 0 95973 49 0 0 25 0 1 0 479987629 79618048 18822 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19438 18822 603 41 0 19397 0
vsize: 77752
[startup+970.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18926 0 0 0 96974 49 0 0 25 0 1 0 479987629 79618048 18835 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19438 18835 603 41 0 19397 0
vsize: 77752
[startup+980.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18926 0 0 0 97974 49 0 0 25 0 1 0 479987629 79618048 18835 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19438 18835 603 41 0 19397 0
vsize: 77752
[startup+990.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18940 0 0 0 98974 49 0 0 25 0 1 0 479987629 79814656 18849 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19486 18849 603 41 0 19445 0
vsize: 77944
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18955 0 0 0 99974 49 0 0 25 0 1 0 479987629 79814656 18864 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19486 18864 603 41 0 19445 0
vsize: 77944
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18955 0 0 0 100974 49 0 0 25 0 1 0 479987629 79814656 18864 4294967295 134512640 134672761 3221224528 3221223712 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19486 18864 603 41 0 19445 0
vsize: 77944
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18968 0 0 0 101975 49 0 0 25 0 1 0 479987629 79814656 18877 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19486 18877 603 41 0 19445 0
vsize: 77944
[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18968 0 0 0 102975 49 0 0 25 0 1 0 479987629 79814656 18877 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19486 18877 603 41 0 19445 0
vsize: 77944
[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18968 0 0 0 103975 49 0 0 25 0 1 0 479987629 79814656 18877 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19486 18877 603 41 0 19445 0
vsize: 77944
[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18985 0 0 0 104975 49 0 0 25 0 1 0 479987629 80076800 18894 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19550 18894 603 41 0 19509 0
vsize: 78200
[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 18985 0 0 0 105975 49 0 0 25 0 1 0 479987629 80076800 18894 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19550 18894 603 41 0 19509 0
vsize: 78200
[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 19220 0 0 0 106975 50 0 0 25 0 1 0 479987629 81014784 19129 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19779 19129 603 41 0 19738 0
vsize: 79116
[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 19602 0 0 0 107975 50 0 0 25 0 1 0 479987629 82534400 19511 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20150 19511 603 41 0 20109 0
vsize: 80600
[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 13105
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 19987 0 0 0 108974 51 0 0 25 0 1 0 479987629 84295680 19896 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20580 19896 603 41 0 20539 0
vsize: 82320
[startup+1100.09 s]
Raw data (loadavg): 1.07 0.99 0.91 3/56 13143
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20406 0 0 0 109972 53 0 0 25 0 1 0 479987629 85880832 20315 4294967295 134512640 134672761 3221224528 3221223728 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20967 20315 603 41 0 20926 0
vsize: 83868
[startup+1110.09 s]
Raw data (loadavg): 1.06 0.99 0.91 2/53 13158
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 110972 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1120.09 s]
Raw data (loadavg): 1.05 0.99 0.91 2/53 13158
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 111972 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1130.09 s]
Raw data (loadavg): 1.04 0.99 0.91 2/53 13158
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 112973 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1140.09 s]
Raw data (loadavg): 1.04 0.99 0.91 2/53 13158
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 113973 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1150.1 s]
Raw data (loadavg): 1.03 0.99 0.91 2/53 13158
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 114973 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1160.1 s]
Raw data (loadavg): 1.03 0.99 0.91 2/53 13158
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 115973 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1170.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 13158
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 116973 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1180.1 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 13160
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 117973 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1190.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 13160
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 118974 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
[startup+1200.1 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 13160
Raw data (stat): 13105 (minisat+) R 13104 7987 7986 0 -1 0 20482 0 0 0 119974 53 0 0 25 0 1 0 479987629 86175744 20389 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21039 20389 603 41 0 20998 0
vsize: 84156
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.01 0.99 0.91 1/53 13160
Raw data (stat): 13105 (minisat+) Z 13104 7987 7986 0 -1 12 20482 0 0 0 119974 57 0 0 25 0 1 0 479987629 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.15
CPU time (s): 1200.32
CPU user time (s): 1199.75
CPU system time (s): 0.576912
CPU usage (%): 100.015
Max. virtual memory (Kb): 84156
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####