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-chnl50_55_pb.cnf.cr.opb
MD5SUM88aaed929c30a489c8806c3852596de3
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 56
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.173973
Number of variables5500
Total number of constraints210
Number of constraints which are clauses110
Number of constraints which are cardinality constraints (but not clauses)100
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint50
Maximum length of a constraint55

Trace number 5772 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 01:41:35 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4157 boxname=wulflinc17 idbench=21 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  88aaed929c30a489c8806c3852596de3  /oldhome/oroussel/tmp/wulflinc17/normalized-chnl50_55_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc17/normalized-chnl50_55_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc17/normalized-chnl50_55_pb.cnf.cr.opb
IDLAUNCH: 4157
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        823544 kB
Buffers:         35892 kB
Cached:         140300 kB
SwapCached:       2376 kB
Active:          58680 kB
Inactive:       122904 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        823292 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23652 kB
Committed_AS:    63736 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:01:37 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 4157 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 210 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................
c ---[  99]---> BDD-cost:  107
c ---[  98]---> BDD-cost:  107
c ---[  97]---> BDD-cost:  107
c ---[  96]---> BDD-cost:  107
c ---[  95]---> BDD-cost:  107
c ---[  94]---> BDD-cost:  107
c ---[  93]---> BDD-cost:  107
c ---[  92]---> BDD-cost:  107
c ---[  91]---> BDD-cost:  107
c ---[  90]---> BDD-cost:  107
c ---[  89]---> BDD-cost:  107
c ---[  88]---> BDD-cost:  107
c ---[  87]---> BDD-cost:  107
c ---[  86]---> BDD-cost:  107
c ---[  85]---> BDD-cost:  107
c ---[  84]---> BDD-cost:  107
c ---[  83]---> BDD-cost:  107
c ---[  82]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  107
c ---[  80]---> BDD-cost:  107
c ---[  79]---> BDD-cost:  107
c ---[  78]---> BDD-cost:  107
c ---[  77]---> BDD-cost:  107
c ---[  76]---> BDD-cost:  107
c ---[  75]---> BDD-cost:  107
c ---[  74]---> BDD-cost:  107
c ---[  73]---> BDD-cost:  107
c ---[  72]---> BDD-cost:  107
c ---[  71]---> BDD-cost:  107
c ---[  70]---> BDD-cost:  107
c ---[  69]---> BDD-cost:  107
c ---[  68]---> BDD-cost:  107
c ---[  67]---> BDD-cost:  107
c ---[  66]---> BDD-cost:  107
c ---[  65]---> BDD-cost:  107
c ---[  64]---> BDD-cost:  107
c ---[  63]---> BDD-cost:  107
c ---[  62]---> BDD-cost:  107
c ---[  61]---> BDD-cost:  107
c ---[  60]---> BDD-cost:  107
c ---[  59]---> BDD-cost:  107
c ---[  58]---> BDD-cost:  107
c ---[  57]---> BDD-cost:  107
c ---[  56]---> BDD-cost:  107
c ---[  55]---> BDD-cost:  107
c ---[  54]---> BDD-cost:  107
c ---[  53]---> BDD-cost:  107
c ---[  52]---> BDD-cost:  107
c ---[  51]---> BDD-cost:  107
c ---[  50]---> BDD-cost:  107
c ---[  49]---> BDD-cost:  107
c ---[  48]---> BDD-cost:  107
c ---[  47]---> BDD-cost:  107
c ---[  46]---> BDD-cost:  107
c ---[  45]---> BDD-cost:  107
c ---[  44]---> BDD-cost:  107
c ---[  43]---> BDD-cost:  107
c ---[  42]---> BDD-cost:  107
c ---[  41]---> BDD-cost:  107
c ---[  40]---> BDD-cost:  107
c ---[  39]---> BDD-cost:  107
c ---[  38]---> BDD-cost:  107
c ---[  37]---> BDD-cost:  107
c ---[  36]---> BDD-cost:  107
c ---[  35]---> BDD-cost:  107
c ---[  34]---> BDD-cost:  107
c ---[  33]---> BDD-cost:  107
c ---[  32]---> BDD-cost:  107
c ---[  31]---> BDD-cost:  107
c ---[  30]---> BDD-cost:  107
c ---[  29]---> BDD-cost:  107
c ---[  28]---> BDD-cost:  107
c ---[  27]---> BDD-cost:  107
c ---[  26]---> BDD-cost:  107
c ---[  25]---> BDD-cost:  107
c ---[  24]---> BDD-cost:  107
c ---[  23]---> BDD-cost:  107
c ---[  22]---> BDD-cost:  107
c ---[  21]---> BDD-cost:  107
c ---[  20]---> BDD-cost:  107
c ---[  19]---> BDD-cost:  107
c ---[  18]---> BDD-cost:  107
c ---[  17]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  107
c ---[  15]---> BDD-cost:  107
c ---[  14]---> BDD-cost:  107
c ---[  13]---> BDD-cost:  107
c ---[  12]---> BDD-cost:  107
c ---[  11]---> BDD-cost:  107
c ---[  10]---> BDD-cost:  107
c ---[   9]---> BDD-cost:  107
c ---[   8]---> BDD-cost:  107
c ---[   7]---> BDD-cost:  107
c ---[   6]---> BDD-cost:  107
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  107
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  107
c ---[   1]---> BDD-cost:  107
c ---[   0]---> BDD-cost:  107
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   26710    74700 |    8903       0        0     nan |  0.000 % |
c |       101 |   26710    74700 |    9793     101    19540   193.5 |  0.617 % |
c |       254 |   26710    74700 |   10772     254    57136   224.9 |  0.617 % |
c |       479 |   26710    74700 |   11849     479   106928   223.2 |  0.617 % |
c |       820 |   26710    74700 |   13034     820   228012   278.1 |  0.617 % |
c |      1327 |   26710    74700 |   14338    1327   407337   307.0 |  0.617 % |
c |      2089 |   26710    74700 |   15772    2089   607183   290.7 |  0.617 % |
c |      3232 |   26710    74700 |   17349    3232   926679   286.7 |  0.617 % |
c |      4943 |   26710    74700 |   19084    4943  1483658   300.2 |  0.617 % |
c |      7507 |   26710    74700 |   20992    7507  2510030   334.4 |  0.617 % |
c |     11351 |   26710    74700 |   23092   11351  4018398   354.0 |  0.617 % |
c |     17118 |   26710    74700 |   25401   17118  7441464   434.7 |  0.617 % |
c |     25771 |   26710    74700 |   27941   25771 13547867   525.7 |  0.617 % |
c |     38747 |   26710    74700 |   30735   11992  5242030   437.1 |  0.617 % |
c |     58209 |   26710    74700 |   33809   31454 12687777   403.4 |  0.617 % |
c |     87404 |   26710    74700 |   37190   27207 15612638   573.8 |  0.617 % |
c |    131194 |   26710    74700 |   40909   35274 17941262   508.6 |  0.617 % |
#### 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.92 0.95 0.91 2/55 27551
Raw data (stat): 27551 (runsolver) R 27550 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480718510 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 3356 0 0 0 991 7 0 0 25 0 1 0 480718510 15249408 3288 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3723 3288 603 41 0 3682 0
vsize: 14892
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 4924 0 0 0 1988 10 0 0 25 0 1 0 480718510 21704704 4856 4294967295 134512640 134672761 3221224528 3221223632 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5299 4856 603 41 0 5258 0
vsize: 21196
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 6581 0 0 0 2984 14 0 0 25 0 1 0 480718510 28459008 6513 4294967295 134512640 134672761 3221224528 3221223632 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6948 6513 603 41 0 6907 0
vsize: 27792
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 7962 0 0 0 3982 16 0 0 25 0 1 0 480718510 34123776 7894 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8331 7894 603 41 0 8290 0
vsize: 33324
[startup+50.0011 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 9193 0 0 0 4980 19 0 0 25 0 1 0 480718510 39141376 9125 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9556 9125 603 41 0 9515 0
vsize: 38224
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 10648 0 0 0 5977 22 0 0 25 0 1 0 480718510 45084672 10580 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11007 10580 603 41 0 10966 0
vsize: 44028
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 11893 0 0 0 6974 25 0 0 25 0 1 0 480718510 50221056 11825 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12261 11825 603 41 0 12220 0
vsize: 49044
[startup+80.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 13018 0 0 0 7971 28 0 0 25 0 1 0 480718510 54824960 12950 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13385 12950 603 41 0 13344 0
vsize: 53540
[startup+90.0025 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 14036 0 0 0 8969 31 0 0 25 0 1 0 480718510 59047936 13968 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14416 13968 603 41 0 14375 0
vsize: 57664
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 14919 0 0 0 9968 32 0 0 25 0 1 0 480718510 62562304 14851 4294967295 134512640 134672761 3221224528 3221223632 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15274 14851 603 41 0 15233 0
vsize: 61096
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 16516 0 0 0 10965 35 0 0 25 0 1 0 480718510 69193728 16448 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16893 16448 603 41 0 16852 0
vsize: 67572
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 18523 0 0 0 11961 39 0 0 25 0 1 0 480718510 77402112 18455 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18897 18455 603 41 0 18856 0
vsize: 75588
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 19653 0 0 0 12958 42 0 0 25 0 1 0 480718510 82116608 19585 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20048 19585 603 41 0 20007 0
vsize: 80192
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 20805 0 0 0 13955 45 0 0 25 0 1 0 480718510 86847488 20737 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21203 20737 603 41 0 21162 0
vsize: 84812
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21667 0 0 0 14954 47 0 0 25 0 1 0 480718510 90394624 21599 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22069 21599 603 41 0 22028 0
vsize: 88276
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 15953 47 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 16954 47 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 17954 47 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 18954 48 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 19954 48 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 20954 48 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 21954 48 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27551
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 22954 48 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 23954 48 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 24954 48 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21826 0 0 0 25954 48 0 0 25 0 1 0 480718510 91082752 21758 4294967295 134512640 134672761 3221224528 3221223632 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21758 603 41 0 22196 0
vsize: 88948
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21827 0 0 0 26954 48 0 0 25 0 1 0 480718510 91082752 21759 4294967295 134512640 134672761 3221224528 3221223696 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21759 603 41 0 22196 0
vsize: 88948
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21828 0 0 0 27954 48 0 0 25 0 1 0 480718510 91082752 21760 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21760 603 41 0 22196 0
vsize: 88948
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 21830 0 0 0 28954 48 0 0 25 0 1 0 480718510 91082752 21762 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22237 21762 603 41 0 22196 0
vsize: 88948
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 22647 0 0 0 29952 50 0 0 25 0 1 0 480718510 94461952 22579 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23062 22579 603 41 0 23021 0
vsize: 92248
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23422 0 0 0 30951 52 0 0 25 0 1 0 480718510 97599488 23354 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23828 23354 603 41 0 23787 0
vsize: 95312
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23553 0 0 0 31951 52 0 0 25 0 1 0 480718510 98140160 23485 4294967295 134512640 134672761 3221224528 3221223632 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23485 603 41 0 23919 0
vsize: 95840
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23555 0 0 0 32951 52 0 0 25 0 1 0 480718510 98140160 23487 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23487 603 41 0 23919 0
vsize: 95840
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23556 0 0 0 33951 52 0 0 25 0 1 0 480718510 98140160 23488 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23488 603 41 0 23919 0
vsize: 95840
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23556 0 0 0 34951 52 0 0 25 0 1 0 480718510 98140160 23488 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23488 603 41 0 23919 0
vsize: 95840
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23558 0 0 0 35951 52 0 0 25 0 1 0 480718510 98140160 23490 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23490 603 41 0 23919 0
vsize: 95840
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23558 0 0 0 36951 53 0 0 25 0 1 0 480718510 98140160 23490 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23490 603 41 0 23919 0
vsize: 95840
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23558 0 0 0 37952 53 0 0 25 0 1 0 480718510 98140160 23490 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23490 603 41 0 23919 0
vsize: 95840
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23558 0 0 0 38952 53 0 0 25 0 1 0 480718510 98140160 23490 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23490 603 41 0 23919 0
vsize: 95840
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23559 0 0 0 39952 53 0 0 25 0 1 0 480718510 98140160 23491 4294967295 134512640 134672761 3221224528 3221223632 134559760 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23491 603 41 0 23919 0
vsize: 95840
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23559 0 0 0 40952 53 0 0 25 0 1 0 480718510 98140160 23491 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23491 603 41 0 23919 0
vsize: 95840
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23559 0 0 0 41952 53 0 0 25 0 1 0 480718510 98140160 23491 4294967295 134512640 134672761 3221224528 3221223624 134555595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23491 603 41 0 23919 0
vsize: 95840
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23559 0 0 0 42952 53 0 0 25 0 1 0 480718510 98140160 23491 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23491 603 41 0 23919 0
vsize: 95840
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23560 0 0 0 43952 53 0 0 25 0 1 0 480718510 98140160 23492 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23560 0 0 0 44952 53 0 0 25 0 1 0 480718510 98140160 23492 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23560 0 0 0 45952 53 0 0 25 0 1 0 480718510 98140160 23492 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23560 0 0 0 46952 53 0 0 25 0 1 0 480718510 98140160 23492 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 23560 0 0 0 47953 53 0 0 25 0 1 0 480718510 98140160 23492 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23960 23492 603 41 0 23919 0
vsize: 95840
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 24543 0 0 0 48951 56 0 0 25 0 1 0 480718510 102191104 24475 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24949 24475 603 41 0 24908 0
vsize: 99796
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 25562 0 0 0 49948 58 0 0 25 0 1 0 480718510 106373120 25494 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25970 25494 603 41 0 25929 0
vsize: 103880
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 26400 0 0 0 50947 60 0 0 25 0 1 0 480718510 109895680 26332 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26830 26332 603 41 0 26789 0
vsize: 107320
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 27275 0 0 0 51945 61 0 0 25 0 1 0 480718510 113541120 27207 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27720 27207 603 41 0 27679 0
vsize: 110880
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27553
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 28150 0 0 0 52942 64 0 0 25 0 1 0 480718510 117088256 28082 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28586 28082 603 41 0 28545 0
vsize: 114344
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 28887 0 0 0 53941 66 0 0 25 0 1 0 480718510 120201216 28819 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29346 28819 603 41 0 29305 0
vsize: 117384
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29523 0 0 0 54940 68 0 0 25 0 1 0 480718510 122777600 29455 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29975 29455 603 41 0 29934 0
vsize: 119900
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29608 0 0 0 55939 68 0 0 25 0 1 0 480718510 123183104 29540 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29540 603 41 0 30033 0
vsize: 120296
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29614 0 0 0 56940 68 0 0 25 0 1 0 480718510 123183104 29546 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29546 603 41 0 30033 0
vsize: 120296
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 57940 68 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 58940 68 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 59940 68 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223632 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 60940 68 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 61941 68 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+630.009 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 62941 68 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+640.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 63941 68 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+650.009 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 64941 68 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+660.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29616 0 0 0 65941 69 0 0 25 0 1 0 480718510 123183104 29548 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29548 603 41 0 30033 0
vsize: 120296
[startup+670.011 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29622 0 0 0 66941 69 0 0 25 0 1 0 480718510 123183104 29554 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29554 603 41 0 30033 0
vsize: 120296
[startup+680.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29627 0 0 0 67942 69 0 0 25 0 1 0 480718510 123183104 29559 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29559 603 41 0 30033 0
vsize: 120296
[startup+690.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29627 0 0 0 68942 69 0 0 25 0 1 0 480718510 123183104 29559 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29559 603 41 0 30033 0
vsize: 120296
[startup+700.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29627 0 0 0 69942 69 0 0 25 0 1 0 480718510 123183104 29559 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29559 603 41 0 30033 0
vsize: 120296
[startup+710.011 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29627 0 0 0 70942 69 0 0 25 0 1 0 480718510 123183104 29559 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29559 603 41 0 30033 0
vsize: 120296
[startup+720.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29627 0 0 0 71942 69 0 0 25 0 1 0 480718510 123183104 29559 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29559 603 41 0 30033 0
vsize: 120296
[startup+730.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29627 0 0 0 72942 69 0 0 25 0 1 0 480718510 123183104 29559 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29559 603 41 0 30033 0
vsize: 120296
[startup+740.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29628 0 0 0 73943 69 0 0 25 0 1 0 480718510 123183104 29560 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+750.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29628 0 0 0 74943 69 0 0 25 0 1 0 480718510 123183104 29560 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+760.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29628 0 0 0 75943 69 0 0 25 0 1 0 480718510 123183104 29560 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+770.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29628 0 0 0 76943 69 0 0 25 0 1 0 480718510 123183104 29560 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+780.011 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29628 0 0 0 77943 69 0 0 25 0 1 0 480718510 123183104 29560 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+790.011 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29628 0 0 0 78943 69 0 0 25 0 1 0 480718510 123183104 29560 4294967295 134512640 134672761 3221224528 3221223696 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+800.011 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29628 0 0 0 79943 69 0 0 25 0 1 0 480718510 123183104 29560 4294967295 134512640 134672761 3221224528 3221223632 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+810.012 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29628 0 0 0 80943 69 0 0 25 0 1 0 480718510 123183104 29560 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29560 603 41 0 30033 0
vsize: 120296
[startup+820.012 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29630 0 0 0 81943 69 0 0 25 0 1 0 480718510 123183104 29562 4294967295 134512640 134672761 3221224528 3221223632 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29562 603 41 0 30033 0
vsize: 120296
[startup+830.011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 27555
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29630 0 0 0 82943 69 0 0 25 0 1 0 480718510 123183104 29562 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29562 603 41 0 30033 0
vsize: 120296
[startup+840.012 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 83944 69 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+850.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 84944 69 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+860.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 85944 69 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+870.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 86944 69 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+880.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 87944 69 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+890.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 88944 69 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+900.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 89945 69 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+910.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 90945 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+920.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 91945 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+930.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 92945 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+940.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 93945 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+950.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 94945 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+960.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 95946 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+970.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 96946 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 97946 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+990.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 98946 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223792 134562156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 99946 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 100946 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 101946 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 102946 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 103947 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 104947 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 105947 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 106947 70 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 107947 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 108947 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27557
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 109947 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223632 134559896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/58 27560
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 110948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1120.02 s]
Raw data (loadavg): 1.07 1.02 0.93 2/55 27610
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 111947 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1130.02 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 27610
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 112948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1140.02 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 27612
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 113948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1150.02 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 27612
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 114948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1160.02 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 27612
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 115948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223632 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1170.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 27612
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 116948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1180.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 27612
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 117948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1190.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 27614
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 118948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
[startup+1200.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 27614
Raw data (stat): 27551 (minisat+) R 27550 20838 20837 0 -1 0 29631 0 0 0 119948 71 0 0 25 0 1 0 480718510 122654720 29458 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29945 29458 603 41 0 29904 0
vsize: 119780
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.02 1.01 0.93 1/55 27614
Raw data (stat): 27551 (minisat+) Z 27550 20838 20837 0 -1 12 29633 0 0 0 119948 76 0 0 25 0 1 0 480718510 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.07
CPU time (s): 1200.26
CPU user time (s): 1199.49
CPU system time (s): 0.769882
CPU usage (%): 100.016
Max. virtual memory (Kb): 120296
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####