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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl20_25_pb.cnf.cr.opb
MD5SUM6c328ef6f9d8d5a179eec9bf3550b7fd
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
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 26
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.027995
Number of variables1000
Total number of constraints90
Number of constraints which are clauses50
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint25

Trace number 5327 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-13 23:28:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3769 boxname=wulflinc5 idbench=9 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6c328ef6f9d8d5a179eec9bf3550b7fd  /oldhome/oroussel/tmp/wulflinc5/normalized-chnl20_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-chnl20_25_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc5/normalized-chnl20_25_pb.cnf.cr.opb
IDLAUNCH: 3769
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        901460 kB
Buffers:         33780 kB
Cached:          77916 kB
SwapCached:       2272 kB
Active:          53680 kB
Inactive:        63184 kB
HighTotal:      131008 kB
HighFree:        49112 kB
LowTotal:       903652 kB
LowFree:        852348 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10648 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:48:27 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3769 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 90 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  39]---> BDD-cost:   47
c ---[  38]---> BDD-cost:   47
c ---[  37]---> BDD-cost:   47
c ---[  36]---> BDD-cost:   47
c ---[  35]---> BDD-cost:   47
c ---[  34]---> BDD-cost:   47
c ---[  33]---> BDD-cost:   47
c ---[  32]---> BDD-cost:   47
c ---[  31]---> BDD-cost:   47
c ---[  30]---> BDD-cost:   47
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    4690    13080 |    1406       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2840          
c   -- var.elim.:  2000/2840          
c   -- var.elim.:  2840/2840          
c   -- var.elim.:  1000/1160          
c   -- var.elim.:  1160/1160          
c   -- var.elim.:  176/176          
c   -- subsuming                       
c   -- var.elim.:  706/706          
c   -- var.elim.:  374/374          
c   -- var.elim.:  134/134          
c   -- var.elim.:  132/132          
c   -- var.elim.:  68/68          
c   -- var.elim.:  60/60          
c   -- var.elim.:  62/62          
c   -- var.elim.:  64/64          
c   -- var.elim.:  66/66          
c   -- var.elim.:  68/68          
c   -- var.elim.:  70/70          
c   -- var.elim.:  72/72          
c   -- var.elim.:  74/74          
c   -- var.elim.:  76/76          
c   -- var.elim.:  78/78          
c   -- var.elim.:  80/80          
c   -- var.elim.:  82/82          
c   -- var.elim.:  84/84          
c   -- var.elim.:  86/86          
c   -- var.elim.:  88/88          
c   -- var.elim.:  190/190          
c   -- subsuming                       
c   -- var.elim.:  1000/1104          
c   -- var.elim.:  1104/1104          
c   -- var.elim.:  1000/1018          
c   -- var.elim.:  1018/1018          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  260/260          
c   -- var.elim.:  146/146          
c   -- var.elim.:  20/20          
c |         0 |    4146    15976 |      --       0       --      -- |     --   | -544/3016
c |         0 |    4146    15976 |    1658       0        0     nan |  0.000 % |
c |       102 |    4146    15976 |    1824     102     7527    73.8 |  1.623 % |
c |       252 |    4146    15976 |    2006     252    19182    76.1 |  1.623 % |
c |       477 |    4146    15976 |    2207     477    40311    84.5 |  1.624 % |
c |       816 |    4146    15976 |    2428     816    82083   100.6 |  1.623 % |
c |      1323 |    4146    15976 |    2670    1323   132806   100.4 |  1.623 % |
c |      2083 |    4146    15976 |    2937    2083   228579   109.7 |  1.623 % |
c |      3222 |    4146    15976 |    3231    3222   375770   116.6 |  1.623 % |
c |      4931 |    4146    15976 | #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 27333
Raw data (stat): 27333 (runsolver) R 27332 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421691030 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.92 0.95 0.90 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 1663 0 0 0 994 4 0 0 25 0 1 0 421691030 8351744 1641 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1641 603 41 0 1998 0
vsize: 8156
[startup+20.0012 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2044 0 0 0 1993 5 0 0 25 0 1 0 421691030 9932800 2022 4294967295 134512640 134672761 3221224544 3221222560 134645588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2425 2022 603 41 0 2384 0
vsize: 9700
[startup+30.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2279 0 0 0 2993 6 0 0 25 0 1 0 421691030 10842112 2257 4294967295 134512640 134672761 3221224544 3221223584 134613116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2647 2257 603 41 0 2606 0
vsize: 10588
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2302 0 0 0 3993 6 0 0 25 0 1 0 421691030 10973184 2280 4294967295 134512640 134672761 3221224544 3221223356 1075349791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2679 2280 603 41 0 2638 0
vsize: 10716
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2469 0 0 0 4993 7 0 0 25 0 1 0 421691030 11640832 2447 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2842 2447 603 41 0 2801 0
vsize: 11368
[startup+60.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2548 0 0 0 5992 7 0 0 25 0 1 0 421691030 11902976 2526 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2906 2526 603 41 0 2865 0
vsize: 11624
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2573 0 0 0 6993 7 0 0 25 0 1 0 421691030 12034048 2551 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2938 2551 603 41 0 2897 0
vsize: 11752
[startup+80.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2574 0 0 0 7993 7 0 0 25 0 1 0 421691030 12034048 2552 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2938 2552 603 41 0 2897 0
vsize: 11752
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2574 0 0 0 8993 7 0 0 25 0 1 0 421691030 12034048 2552 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2938 2552 603 41 0 2897 0
vsize: 11752
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2582 0 0 0 9993 7 0 0 25 0 1 0 421691030 12136448 2560 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2963 2560 603 41 0 2922 0
vsize: 11852
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2582 0 0 0 10993 7 0 0 25 0 1 0 421691030 12136448 2560 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2963 2560 603 41 0 2922 0
vsize: 11852
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 2781 0 0 0 11993 7 0 0 25 0 1 0 421691030 12926976 2759 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3156 2759 603 41 0 3115 0
vsize: 12624
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3000 0 0 0 12993 8 0 0 25 0 1 0 421691030 13848576 2978 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2978 603 41 0 3340 0
vsize: 13524
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3000 0 0 0 13993 8 0 0 25 0 1 0 421691030 13848576 2978 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2978 603 41 0 3340 0
vsize: 13524
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3000 0 0 0 14994 8 0 0 25 0 1 0 421691030 13848576 2978 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2978 603 41 0 3340 0
vsize: 13524
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3000 0 0 0 15994 8 0 0 25 0 1 0 421691030 13848576 2978 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3381 2978 603 41 0 3340 0
vsize: 13524
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3111 0 0 0 16993 8 0 0 25 0 1 0 421691030 14344192 3089 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3502 3089 603 41 0 3461 0
vsize: 14008
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3111 0 0 0 17993 8 0 0 25 0 1 0 421691030 14327808 3089 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3498 3089 603 41 0 3457 0
vsize: 13992
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3112 0 0 0 18994 8 0 0 25 0 1 0 421691030 14311424 3090 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3494 3090 603 41 0 3453 0
vsize: 13976
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3505 0 0 0 19993 9 0 0 25 0 1 0 421691030 15970304 3483 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3899 3483 603 41 0 3858 0
vsize: 15596
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3599 0 0 0 20993 9 0 0 25 0 1 0 421691030 16347136 3577 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3991 3577 603 41 0 3950 0
vsize: 15964
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3599 0 0 0 21993 9 0 0 25 0 1 0 421691030 16347136 3577 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3991 3577 603 41 0 3950 0
vsize: 15964
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3628 0 0 0 22993 9 0 0 25 0 1 0 421691030 16478208 3606 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4023 3606 603 41 0 3982 0
vsize: 16092
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3743 0 0 0 23993 10 0 0 25 0 1 0 421691030 16945152 3721 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4137 3721 603 41 0 4096 0
vsize: 16548
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3887 0 0 0 24993 10 0 0 25 0 1 0 421691030 17539072 3865 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4282 3865 603 41 0 4241 0
vsize: 17128
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3888 0 0 0 25993 10 0 0 25 0 1 0 421691030 17530880 3866 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3866 603 41 0 4239 0
vsize: 17120
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3898 0 0 0 26993 10 0 0 25 0 1 0 421691030 17530880 3876 4294967295 134512640 134672761 3221224544 3221223600 134644260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3876 603 41 0 4239 0
vsize: 17120
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3898 0 0 0 27993 10 0 0 25 0 1 0 421691030 17530880 3876 4294967295 134512640 134672761 3221224544 3221223460 1075346528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3876 603 41 0 4239 0
vsize: 17120
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3898 0 0 0 28993 10 0 0 25 0 1 0 421691030 17530880 3876 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4280 3876 603 41 0 4239 0
vsize: 17120
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 3973 0 0 0 29993 10 0 0 25 0 1 0 421691030 17903616 3951 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4371 3951 603 41 0 4330 0
vsize: 17484
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4172 0 0 0 30993 11 0 0 25 0 1 0 421691030 18690048 4150 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4563 4150 603 41 0 4522 0
vsize: 18252
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4173 0 0 0 31993 11 0 0 25 0 1 0 421691030 18690048 4151 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4563 4151 603 41 0 4522 0
vsize: 18252
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 32993 11 0 0 25 0 1 0 421691030 18329600 4079 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4475 4079 603 41 0 4434 0
vsize: 17900
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 33994 11 0 0 25 0 1 0 421691030 18329600 4079 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4475 4079 603 41 0 4434 0
vsize: 17900
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 34994 11 0 0 25 0 1 0 421691030 18325504 4078 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4474 4078 603 41 0 4433 0
vsize: 17896
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 35994 11 0 0 25 0 1 0 421691030 18325504 4078 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4474 4078 603 41 0 4433 0
vsize: 17896
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 36994 11 0 0 25 0 1 0 421691030 18325504 4078 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4474 4078 603 41 0 4433 0
vsize: 17896
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 37994 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 38994 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 39995 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 40995 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 41995 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 42995 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 43995 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 44995 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 45996 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 46996 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 47996 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 48996 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 49996 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4174 0 0 0 50997 11 0 0 25 0 1 0 421691030 18063360 4014 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4014 603 41 0 4369 0
vsize: 17640
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4175 0 0 0 51997 11 0 0 25 0 1 0 421691030 18063360 4015 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4015 603 41 0 4369 0
vsize: 17640
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4175 0 0 0 52997 11 0 0 25 0 1 0 421691030 18063360 4015 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4015 603 41 0 4369 0
vsize: 17640
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4175 0 0 0 53997 11 0 0 25 0 1 0 421691030 18063360 4015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4015 603 41 0 4369 0
vsize: 17640
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4175 0 0 0 54998 11 0 0 25 0 1 0 421691030 18063360 4015 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4015 603 41 0 4369 0
vsize: 17640
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4175 0 0 0 55998 11 0 0 25 0 1 0 421691030 18063360 4015 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4410 4015 603 41 0 4369 0
vsize: 17640
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4212 0 0 0 56998 11 0 0 25 0 1 0 421691030 18292736 4052 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4466 4052 603 41 0 4425 0
vsize: 17864
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4289 0 0 0 57998 11 0 0 25 0 1 0 421691030 18632704 4129 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4129 603 41 0 4508 0
vsize: 18196
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4321 0 0 0 58998 11 0 0 25 0 1 0 421691030 18792448 4161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4588 4161 603 41 0 4547 0
vsize: 18352
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4349 0 0 0 59998 11 0 0 25 0 1 0 421691030 18890752 4189 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4612 4189 603 41 0 4571 0
vsize: 18448
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4362 0 0 0 60999 11 0 0 25 0 1 0 421691030 18890752 4202 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4612 4202 603 41 0 4571 0
vsize: 18448
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4376 0 0 0 61999 11 0 0 25 0 1 0 421691030 19021824 4216 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4644 4216 603 41 0 4603 0
vsize: 18576
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4383 0 0 0 62999 11 0 0 25 0 1 0 421691030 19021824 4223 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4644 4223 603 41 0 4603 0
vsize: 18576
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4563 0 0 0 63999 12 0 0 25 0 1 0 421691030 19791872 4403 4294967295 134512640 134672761 3221224544 3221223584 134614223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4832 4403 603 41 0 4791 0
vsize: 19328
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4615 0 0 0 64999 12 0 0 25 0 1 0 421691030 20004864 4455 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4884 4455 603 41 0 4843 0
vsize: 19536
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4615 0 0 0 65999 12 0 0 25 0 1 0 421691030 20004864 4455 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4884 4455 603 41 0 4843 0
vsize: 19536
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4660 0 0 0 66999 12 0 0 25 0 1 0 421691030 20135936 4500 4294967295 134512640 134672761 3221224544 3221223584 134612644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4916 4500 603 41 0 4875 0
vsize: 19664
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4684 0 0 0 67999 12 0 0 25 0 1 0 421691030 20246528 4524 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4943 4524 603 41 0 4902 0
vsize: 19772
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4684 0 0 0 69000 12 0 0 25 0 1 0 421691030 20246528 4524 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4943 4524 603 41 0 4902 0
vsize: 19772
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4733 0 0 0 69999 12 0 0 25 0 1 0 421691030 20500480 4573 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5005 4573 603 41 0 4964 0
vsize: 20020
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4741 0 0 0 71000 12 0 0 25 0 1 0 421691030 20500480 4581 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5005 4581 603 41 0 4964 0
vsize: 20020
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4741 0 0 0 72000 12 0 0 25 0 1 0 421691030 20500480 4581 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5005 4581 603 41 0 4964 0
vsize: 20020
[startup+730.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4749 0 0 0 73000 12 0 0 25 0 1 0 421691030 20500480 4589 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5005 4589 603 41 0 4964 0
vsize: 20020
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4749 0 0 0 74000 12 0 0 25 0 1 0 421691030 20500480 4589 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5005 4589 603 41 0 4964 0
vsize: 20020
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4811 0 0 0 75000 13 0 0 25 0 1 0 421691030 20832256 4651 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5086 4651 603 41 0 5045 0
vsize: 20344
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4832 0 0 0 76000 13 0 0 25 0 1 0 421691030 20926464 4672 4294967295 134512640 134672761 3221224544 3221223584 134613804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5109 4672 603 41 0 5068 0
vsize: 20436
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4845 0 0 0 77000 13 0 0 25 0 1 0 421691030 20926464 4685 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5109 4685 603 41 0 5068 0
vsize: 20436
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4867 0 0 0 78001 13 0 0 25 0 1 0 421691030 21090304 4707 4294967295 134512640 134672761 3221224544 3221223600 134644269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4707 603 41 0 5108 0
vsize: 20596
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4867 0 0 0 79001 13 0 0 25 0 1 0 421691030 21090304 4707 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4707 603 41 0 5108 0
vsize: 20596
[startup+800.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4868 0 0 0 80001 13 0 0 25 0 1 0 421691030 21090304 4708 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4708 603 41 0 5108 0
vsize: 20596
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4876 0 0 0 81001 13 0 0 25 0 1 0 421691030 21090304 4716 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4716 603 41 0 5108 0
vsize: 20596
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4884 0 0 0 82001 13 0 0 25 0 1 0 421691030 21090304 4724 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4724 603 41 0 5108 0
vsize: 20596
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4884 0 0 0 83001 13 0 0 25 0 1 0 421691030 21090304 4724 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4724 603 41 0 5108 0
vsize: 20596
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4886 0 0 0 84002 13 0 0 25 0 1 0 421691030 21090304 4726 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4726 603 41 0 5108 0
vsize: 20596
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4888 0 0 0 85002 13 0 0 25 0 1 0 421691030 21090304 4728 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4728 603 41 0 5108 0
vsize: 20596
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4888 0 0 0 86002 13 0 0 25 0 1 0 421691030 21090304 4728 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4728 603 41 0 5108 0
vsize: 20596
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4888 0 0 0 87002 13 0 0 25 0 1 0 421691030 21090304 4728 4294967295 134512640 134672761 3221224544 3221223600 134644269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4728 603 41 0 5108 0
vsize: 20596
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4888 0 0 0 88003 13 0 0 25 0 1 0 421691030 21090304 4728 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4728 603 41 0 5108 0
vsize: 20596
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4888 0 0 0 89003 13 0 0 25 0 1 0 421691030 21090304 4728 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4728 603 41 0 5108 0
vsize: 20596
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4888 0 0 0 90003 13 0 0 25 0 1 0 421691030 21090304 4728 4294967295 134512640 134672761 3221224544 3221223496 1075347338 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4728 603 41 0 5108 0
vsize: 20596
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4888 0 0 0 91003 13 0 0 25 0 1 0 421691030 21090304 4728 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4728 603 41 0 5108 0
vsize: 20596
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4888 0 0 0 92003 13 0 0 25 0 1 0 421691030 21090304 4728 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5149 4728 603 41 0 5108 0
vsize: 20596
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 4980 0 0 0 93003 13 0 0 25 0 1 0 421691030 21483520 4820 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5245 4820 603 41 0 5204 0
vsize: 20980
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5040 0 0 0 94004 13 0 0 25 0 1 0 421691030 21745664 4880 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5309 4880 603 41 0 5268 0
vsize: 21236
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5070 0 0 0 95004 13 0 0 25 0 1 0 421691030 21876736 4910 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5341 4910 603 41 0 5300 0
vsize: 21364
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5092 0 0 0 96004 13 0 0 25 0 1 0 421691030 22007808 4932 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5373 4932 603 41 0 5332 0
vsize: 21492
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5195 0 0 0 97004 13 0 0 25 0 1 0 421691030 22401024 5035 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5469 5035 603 41 0 5428 0
vsize: 21876
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5243 0 0 0 98004 13 0 0 25 0 1 0 421691030 22630400 5083 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 5083 603 41 0 5484 0
vsize: 22100
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5243 0 0 0 99004 13 0 0 25 0 1 0 421691030 22630400 5083 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 5083 603 41 0 5484 0
vsize: 22100
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5244 0 0 0 100004 13 0 0 25 0 1 0 421691030 22630400 5084 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 5084 603 41 0 5484 0
vsize: 22100
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5244 0 0 0 101004 13 0 0 25 0 1 0 421691030 22630400 5084 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5525 5084 603 41 0 5484 0
vsize: 22100
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5244 0 0 0 102005 13 0 0 25 0 1 0 421691030 22626304 5084 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5524 5084 603 41 0 5483 0
vsize: 22096
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5325 0 0 0 103005 14 0 0 25 0 1 0 421691030 22892544 5165 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5589 5165 603 41 0 5548 0
vsize: 22356
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5340 0 0 0 104005 14 0 0 25 0 1 0 421691030 23019520 5180 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5620 5180 603 41 0 5579 0
vsize: 22480
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5595 0 0 0 105004 15 0 0 25 0 1 0 421691030 24068096 5435 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5876 5435 603 41 0 5835 0
vsize: 23504
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5653 0 0 0 106004 15 0 0 25 0 1 0 421691030 24317952 5493 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5937 5493 603 41 0 5896 0
vsize: 23748
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5653 0 0 0 107004 15 0 0 25 0 1 0 421691030 24317952 5493 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5937 5493 603 41 0 5896 0
vsize: 23748
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5653 0 0 0 108004 15 0 0 25 0 1 0 421691030 24317952 5493 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5937 5493 603 41 0 5896 0
vsize: 23748
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5653 0 0 0 109004 15 0 0 25 0 1 0 421691030 24309760 5493 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5935 5493 603 41 0 5894 0
vsize: 23740
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5653 0 0 0 110005 15 0 0 25 0 1 0 421691030 24309760 5493 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5935 5493 603 41 0 5894 0
vsize: 23740
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5653 0 0 0 111005 15 0 0 25 0 1 0 421691030 24309760 5493 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5935 5493 603 41 0 5894 0
vsize: 23740
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5653 0 0 0 112005 15 0 0 25 0 1 0 421691030 24309760 5493 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5935 5493 603 41 0 5894 0
vsize: 23740
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5653 0 0 0 113005 15 0 0 25 0 1 0 421691030 24305664 5493 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5934 5493 603 41 0 5893 0
vsize: 23736
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5663 0 0 0 114005 15 0 0 25 0 1 0 421691030 24305664 5503 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5934 5503 603 41 0 5893 0
vsize: 23736
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5740 0 0 0 115006 15 0 0 25 0 1 0 421691030 24670208 5580 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6023 5580 603 41 0 5982 0
vsize: 24092
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5749 0 0 0 116006 15 0 0 25 0 1 0 421691030 24670208 5589 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6023 5589 603 41 0 5982 0
vsize: 24092
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5767 0 0 0 117006 15 0 0 25 0 1 0 421691030 24780800 5607 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6050 5607 603 41 0 6009 0
vsize: 24200
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5779 0 0 0 118006 15 0 0 25 0 1 0 421691030 24780800 5619 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6050 5619 603 41 0 6009 0
vsize: 24200
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5788 0 0 0 119006 15 0 0 25 0 1 0 421691030 24866816 5628 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6071 5628 603 41 0 6030 0
vsize: 24284
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27333
Raw data (stat): 27333 (minisat+) R 27332 24215 24214 0 -1 0 5788 0 0 0 120006 15 0 0 25 0 1 0 421691030 24846336 5628 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6066 5628 603 41 0 6025 0
vsize: 24264
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 27333
Raw data (stat): 27333 (minisat+) Z 27332 24215 24214 0 -1 12 5788 0 0 0 120007 16 0 0 25 0 1 0 421691030 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.04
CPU time (s): 1200.24
CPU user time (s): 1200.07
CPU system time (s): 0.168974
CPU usage (%): 100.016
Max. virtual memory (Kb): 24284
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####