PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga40_39_sat_pb.cnf.cr.opb
MD5SUM	b0b9c98556325dcf5a5811fc2d17a816
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	41
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	4.5833
Number of variables	2340
Total number of constraints	1678
Number of constraints which are clauses	1599
Number of constraints which are cardinality constraints (but not clauses)	79
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	40
Trace number 4809

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-13 20:25:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=473 boxname=wulflinc5 idbench=53 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b0b9c98556325dcf5a5811fc2d17a816  /oldhome/oroussel/tmp/wulflinc5/normalized-fpga40_39_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc5/normalized-fpga40_39_sat_pb.cnf.cr.opb
IDLAUNCH: 473
/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:        924416 kB
Buffers:         33140 kB
Cached:          55640 kB
SwapCached:       2272 kB
Active:          48832 kB
Inactive:        45092 kB
HighTotal:      131008 kB
HighFree:        71428 kB
LowTotal:       903652 kB
LowFree:        852988 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10768 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:43:12 (client local time) WITH STATUS 30 IN 1065.59 SECONDS
stats: 473 7 1065.59 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1678 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  78]---> BDD-cost:   75
c ---[  77]---> BDD-cost:   75
c ---[  76]---> BDD-cost:   75
c ---[  75]---> BDD-cost:   75
c ---[  74]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   75
c ---[  72]---> BDD-cost:   75
c ---[  71]---> BDD-cost:   75
c ---[  70]---> BDD-cost:   75
c ---[  69]---> BDD-cost:   75
c ---[  68]---> BDD-cost:   75
c ---[  67]---> BDD-cost:   75
c ---[  66]---> BDD-cost:   75
c ---[  65]---> BDD-cost:   75
c ---[  64]---> BDD-cost:   75
c ---[  63]---> BDD-cost:   75
c ---[  62]---> BDD-cost:   75
c ---[  61]---> BDD-cost:   75
c ---[  60]---> BDD-cost:   75
c ---[  59]---> BDD-cost:   75
c ---[  58]---> BDD-cost:   75
c ---[  57]---> BDD-cost:   75
c ---[  56]---> BDD-cost:   75
c ---[  55]---> BDD-cost:   75
c ---[  54]---> BDD-cost:   75
c ---[  53]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   75
c ---[  51]---> BDD-cost:   75
c ---[  50]---> BDD-cost:   75
c ---[  49]---> BDD-cost:   75
c ---[  48]---> BDD-cost:   75
c ---[  47]---> BDD-cost:   75
c ---[  46]---> BDD-cost:   75
c ---[  45]---> BDD-cost:   75
c ---[  44]---> BDD-cost:   75
c ---[  43]---> BDD-cost:   75
c ---[  42]---> BDD-cost:   75
c ---[  41]---> BDD-cost:   75
c ---[  40]---> BDD-cost:   75
c ---[  39]---> BDD-cost:   75
c ---[  38]---> BDD-cost:   37
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12588    62143 |    4196       0        0     nan |  0.000 % |
c |       111 |   12588    62143 |    4615     111    33739   304.0 |  1.165 % |
c |       263 |   12588    62143 |    5077     263    74695   284.0 |  1.165 % |
c |       488 |   12588    62143 |    5584     488   117851   241.5 |  1.165 % |
c |       825 |   12588    62143 |    6143     825   182982   221.8 |  1.165 % |
c |      1332 |   12588    62143 |    6757    1332   313395   235.3 |  1.165 % |
c |      2093 |   12588    62143 |    7433    2093   552175   263.8 |  1.165 % |
c |      3234 |   12588    62143 |    8176    3234   826036   255.4 |  1.165 % |
c |      4942 |   12588    62143 |    8994    4942  1185368   239.9 |  1.165 % |
c |      7505 |   12588    62143 |    9893    7505  1634136   217.7 |  1.165 % |
c |     11350 |   12588    62143 |   10883   11350  3068153   270.3 |  1.165 % |
c |     17118 |   12588    62143 |   11971   11443  3648096   318.8 |  1.165 % |
c |     25767 |   12588    62143 |   13168   12050  3959642   328.6 |  1.165 % |
c |     38744 |   12588    62143 |   14485   16496  5481733   332.3 |  1.165 % |
c |     58205 |   12588    62143 |   15934   17828  2135865   119.8 |  1.165 % |
c |     87397 |   12588    62143 |   17527   17964  6583862   366.5 |  1.165 % |
c |    131186 |   12588    62143 |   19280   20533  8190543   398.9 |  1.165 % |
c |    196874 |   12588    62143 |   21208   16916  7196074   425.4 |  1.165 % |
c |    295401 |   12588    62143 |   23329   21506  5077493   236.1 |  1.165 % |
c ==============================================================================
c [1mSATISFIABLE: No goal function specified.[0m
s SATISFIABLE
v
c _______________________________________________________________________________
c 
c restarts              : 19
c conflicts             : 314711         (295 /sec)
c decisions             : 438316         (412 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1065.15 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 26078
Raw data (stat): 26078 (runsolver) R 26077 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420593042 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 3063 0 0 0 990 8 0 0 25 0 1 0 420593042 14159872 3041 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3457 3041 603 41 0 3416 0
vsize: 13828
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 4164 0 0 0 1986 11 0 0 25 0 1 0 420593042 18604032 4142 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4542 4142 603 41 0 4501 0
vsize: 18168
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 5031 0 0 0 2983 13 0 0 25 0 1 0 420593042 22110208 5009 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5398 5009 603 41 0 5357 0
vsize: 21592
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 6255 0 0 0 3978 17 0 0 25 0 1 0 420593042 27238400 6233 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6650 6233 603 41 0 6609 0
vsize: 26600
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 6370 0 0 0 4977 17 0 0 25 0 1 0 420593042 27643904 6348 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6749 6348 603 41 0 6708 0
vsize: 26996
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 6659 0 0 0 5976 18 0 0 25 0 1 0 420593042 28839936 6637 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7041 6637 603 41 0 7000 0
vsize: 28164
[startup+70.0026 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 6864 0 0 0 6976 18 0 0 25 0 1 0 420593042 29786112 6842 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7272 6842 603 41 0 7231 0
vsize: 29088
[startup+80.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 6864 0 0 0 7976 18 0 0 25 0 1 0 420593042 29786112 6842 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7272 6842 603 41 0 7231 0
vsize: 29088
[startup+90.0031 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 6885 0 0 0 8977 19 0 0 25 0 1 0 420593042 29786112 6863 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7272 6863 603 41 0 7231 0
vsize: 29088
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 7010 0 0 0 9976 19 0 0 25 0 1 0 420593042 30322688 6988 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6988 603 41 0 7362 0
vsize: 29612
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 7013 0 0 0 10977 19 0 0 25 0 1 0 420593042 30322688 6991 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6991 603 41 0 7362 0
vsize: 29612
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 7013 0 0 0 11977 19 0 0 25 0 1 0 420593042 30322688 6991 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6991 603 41 0 7362 0
vsize: 29612
[startup+130.005 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 7013 0 0 0 12977 19 0 0 25 0 1 0 420593042 30322688 6991 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6991 603 41 0 7362 0
vsize: 29612
[startup+140.004 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 7013 0 0 0 13977 19 0 0 25 0 1 0 420593042 30322688 6991 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7403 6991 603 41 0 7362 0
vsize: 29612
[startup+150.006 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 7647 0 0 0 14976 20 0 0 25 0 1 0 420593042 33030144 7625 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8064 7625 603 41 0 8023 0
vsize: 32256
[startup+160.005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 7969 0 0 0 15976 21 0 0 25 0 1 0 420593042 34246656 7947 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8361 7947 603 41 0 8320 0
vsize: 33444
[startup+170.005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 8175 0 0 0 16975 22 0 0 25 0 1 0 420593042 35246080 8153 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8605 8153 603 41 0 8564 0
vsize: 34420
[startup+180.005 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 8898 0 0 0 17973 24 0 0 25 0 1 0 420593042 38215680 8876 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9330 8876 603 41 0 9289 0
vsize: 37320
[startup+190.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10134 0 0 0 18970 27 0 0 25 0 1 0 420593042 43347968 10112 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10583 10112 603 41 0 10542 0
vsize: 42332
[startup+200.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10135 0 0 0 19970 27 0 0 25 0 1 0 420593042 43347968 10113 4294967295 134512640 134672761 3221224624 3221223728 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10583 10113 603 41 0 10542 0
vsize: 42332
[startup+210.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10135 0 0 0 20971 27 0 0 25 0 1 0 420593042 43347968 10113 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10583 10113 603 41 0 10542 0
vsize: 42332
[startup+220.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10135 0 0 0 21970 27 0 0 25 0 1 0 420593042 43347968 10113 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10583 10113 603 41 0 10542 0
vsize: 42332
[startup+230.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10135 0 0 0 22970 27 0 0 25 0 1 0 420593042 43347968 10113 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10583 10113 603 41 0 10542 0
vsize: 42332
[startup+240.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10135 0 0 0 23970 27 0 0 25 0 1 0 420593042 43347968 10113 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10583 10113 603 41 0 10542 0
vsize: 42332
[startup+250.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10320 0 0 0 24970 28 0 0 25 0 1 0 420593042 44019712 10298 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10747 10298 603 41 0 10706 0
vsize: 42988
[startup+260.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10440 0 0 0 25970 28 0 0 25 0 1 0 420593042 44576768 10418 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10883 10418 603 41 0 10842 0
vsize: 43532
[startup+270.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10441 0 0 0 26970 28 0 0 25 0 1 0 420593042 44576768 10419 4294967295 134512640 134672761 3221224624 3221223808 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10883 10419 603 41 0 10842 0
vsize: 43532
[startup+280.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10441 0 0 0 27970 28 0 0 25 0 1 0 420593042 44576768 10419 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10883 10419 603 41 0 10842 0
vsize: 43532
[startup+290.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10441 0 0 0 28970 28 0 0 25 0 1 0 420593042 44576768 10419 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10883 10419 603 41 0 10842 0
vsize: 43532
[startup+300.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10453 0 0 0 29971 28 0 0 25 0 1 0 420593042 44711936 10431 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10916 10431 603 41 0 10875 0
vsize: 43664
[startup+310.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10800 0 0 0 30970 29 0 0 25 0 1 0 420593042 46067712 10778 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11247 10778 603 41 0 11206 0
vsize: 44988
[startup+320.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10900 0 0 0 31970 29 0 0 25 0 1 0 420593042 46469120 10878 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11345 10878 603 41 0 11304 0
vsize: 45380
[startup+330.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10900 0 0 0 32970 29 0 0 25 0 1 0 420593042 46469120 10878 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11345 10878 603 41 0 11304 0
vsize: 45380
[startup+340.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10900 0 0 0 33970 29 0 0 25 0 1 0 420593042 46469120 10878 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11345 10878 603 41 0 11304 0
vsize: 45380
[startup+350.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10900 0 0 0 34970 29 0 0 25 0 1 0 420593042 46469120 10878 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11345 10878 603 41 0 11304 0
vsize: 45380
[startup+360.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 10900 0 0 0 35971 29 0 0 25 0 1 0 420593042 46469120 10878 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11345 10878 603 41 0 11304 0
vsize: 45380
[startup+370.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11050 0 0 0 36970 29 0 0 25 0 1 0 420593042 47144960 11028 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11510 11028 603 41 0 11469 0
vsize: 46040
[startup+380.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11069 0 0 0 37971 29 0 0 25 0 1 0 420593042 47280128 11047 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11543 11047 603 41 0 11502 0
vsize: 46172
[startup+390.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11093 0 0 0 38971 29 0 0 25 0 1 0 420593042 47280128 11071 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11543 11071 603 41 0 11502 0
vsize: 46172
[startup+400.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11095 0 0 0 39971 29 0 0 25 0 1 0 420593042 47280128 11073 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11543 11073 603 41 0 11502 0
vsize: 46172
[startup+410.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11095 0 0 0 40971 29 0 0 25 0 1 0 420593042 47280128 11073 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11543 11073 603 41 0 11502 0
vsize: 46172
[startup+420.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11095 0 0 0 41971 30 0 0 25 0 1 0 420593042 47280128 11073 4294967295 134512640 134672761 3221224624 3221223808 134558638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11543 11073 603 41 0 11502 0
vsize: 46172
[startup+430.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11095 0 0 0 42970 30 0 0 25 0 1 0 420593042 47280128 11073 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11543 11073 603 41 0 11502 0
vsize: 46172
[startup+440.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11095 0 0 0 43969 30 0 0 25 0 1 0 420593042 47280128 11073 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11543 11073 603 41 0 11502 0
vsize: 46172
[startup+450.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 11353 0 0 0 44968 32 0 0 25 0 1 0 420593042 48353280 11331 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11805 11331 603 41 0 11764 0
vsize: 47220
[startup+460.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 12479 0 0 0 45965 34 0 0 25 0 1 0 420593042 53088256 12457 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12961 12457 603 41 0 12920 0
vsize: 51844
[startup+470.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 12698 0 0 0 46965 35 0 0 25 0 1 0 420593042 53895168 12676 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13158 12676 603 41 0 13117 0
vsize: 52632
[startup+480.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 12701 0 0 0 47965 35 0 0 25 0 1 0 420593042 53895168 12679 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13158 12679 603 41 0 13117 0
vsize: 52632
[startup+490.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 12701 0 0 0 48965 35 0 0 25 0 1 0 420593042 53895168 12679 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13158 12679 603 41 0 13117 0
vsize: 52632
[startup+500.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 12702 0 0 0 49966 35 0 0 25 0 1 0 420593042 53895168 12680 4294967295 134512640 134672761 3221224624 3221223580 1075349984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13158 12680 603 41 0 13117 0
vsize: 52632
[startup+510.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 12702 0 0 0 50966 35 0 0 25 0 1 0 420593042 53895168 12680 4294967295 134512640 134672761 3221224624 3221223808 134559424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13158 12680 603 41 0 13117 0
vsize: 52632
[startup+520.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13003 0 0 0 51965 35 0 0 25 0 1 0 420593042 55119872 12981 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13457 12981 603 41 0 13416 0
vsize: 53828
[startup+530.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13615 0 0 0 52964 37 0 0 25 0 1 0 420593042 57696256 13593 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14086 13593 603 41 0 14045 0
vsize: 56344
[startup+540.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13615 0 0 0 53965 37 0 0 25 0 1 0 420593042 57696256 13593 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14086 13593 603 41 0 14045 0
vsize: 56344
[startup+550.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13615 0 0 0 54965 37 0 0 25 0 1 0 420593042 57696256 13593 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14086 13593 603 41 0 14045 0
vsize: 56344
[startup+560.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13615 0 0 0 55965 37 0 0 25 0 1 0 420593042 57696256 13593 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14086 13593 603 41 0 14045 0
vsize: 56344
[startup+570.014 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13615 0 0 0 56965 37 0 0 25 0 1 0 420593042 57696256 13593 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14086 13593 603 41 0 14045 0
vsize: 56344
[startup+580.015 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13617 0 0 0 57965 37 0 0 25 0 1 0 420593042 57696256 13595 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14086 13595 603 41 0 14045 0
vsize: 56344
[startup+590.014 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13620 0 0 0 58966 37 0 0 25 0 1 0 420593042 57696256 13598 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14086 13598 603 41 0 14045 0
vsize: 56344
[startup+600.014 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13874 0 0 0 59965 38 0 0 25 0 1 0 420593042 58810368 13852 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14358 13852 603 41 0 14317 0
vsize: 57432
[startup+610.015 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13874 0 0 0 60965 38 0 0 25 0 1 0 420593042 58810368 13852 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14358 13852 603 41 0 14317 0
vsize: 57432
[startup+620.014 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13874 0 0 0 61965 38 0 0 25 0 1 0 420593042 58810368 13852 4294967295 134512640 134672761 3221224624 3221223728 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14358 13852 603 41 0 14317 0
vsize: 57432
[startup+630.014 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13874 0 0 0 62965 38 0 0 25 0 1 0 420593042 58810368 13852 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14358 13852 603 41 0 14317 0
vsize: 57432
[startup+640.015 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13874 0 0 0 63965 38 0 0 25 0 1 0 420593042 58810368 13852 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14358 13852 603 41 0 14317 0
vsize: 57432
[startup+650.015 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13874 0 0 0 64966 38 0 0 25 0 1 0 420593042 58810368 13852 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14358 13852 603 41 0 14317 0
vsize: 57432
[startup+660.016 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 13874 0 0 0 65966 38 0 0 25 0 1 0 420593042 58810368 13852 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14358 13852 603 41 0 14317 0
vsize: 57432
[startup+670.016 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14113 0 0 0 66965 38 0 0 25 0 1 0 420593042 59768832 14091 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14592 14091 603 41 0 14551 0
vsize: 58368
[startup+680.017 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14113 0 0 0 67966 38 0 0 25 0 1 0 420593042 59768832 14091 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14592 14091 603 41 0 14551 0
vsize: 58368
[startup+690.017 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14113 0 0 0 68966 38 0 0 25 0 1 0 420593042 59768832 14091 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14592 14091 603 41 0 14551 0
vsize: 58368
[startup+700.017 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14113 0 0 0 69966 38 0 0 25 0 1 0 420593042 59768832 14091 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14592 14091 603 41 0 14551 0
vsize: 58368
[startup+710.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14113 0 0 0 70966 38 0 0 25 0 1 0 420593042 59768832 14091 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14592 14091 603 41 0 14551 0
vsize: 58368
[startup+720.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14113 0 0 0 71966 38 0 0 25 0 1 0 420593042 59768832 14091 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14592 14091 603 41 0 14551 0
vsize: 58368
[startup+730.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14115 0 0 0 72967 38 0 0 25 0 1 0 420593042 59768832 14093 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14592 14093 603 41 0 14551 0
vsize: 58368
[startup+740.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 73965 39 0 0 25 0 1 0 420593042 59768832 14095 4294967295 134512640 134672761 3221224624 3221223760 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14592 14095 603 41 0 14551 0
vsize: 58368
[startup+750.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 74966 39 0 0 25 0 1 0 420593042 59752448 14095 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14588 14095 603 41 0 14547 0
vsize: 58352
[startup+760.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 75966 39 0 0 25 0 1 0 420593042 59752448 14095 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14588 14095 603 41 0 14547 0
vsize: 58352
[startup+770.018 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 76966 39 0 0 25 0 1 0 420593042 59752448 14095 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14588 14095 603 41 0 14547 0
vsize: 58352
[startup+780.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 77966 39 0 0 25 0 1 0 420593042 59740160 14095 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14585 14095 603 41 0 14544 0
vsize: 58340
[startup+790.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 78966 39 0 0 25 0 1 0 420593042 59740160 14095 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14585 14095 603 41 0 14544 0
vsize: 58340
[startup+800.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 79966 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+810.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 80966 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+820.019 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 81967 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+830.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 82967 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223728 134560177 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+840.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 83967 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+850.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 84967 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+860.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 85968 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+870.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 86968 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+880.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 87968 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+890.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 88968 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+900.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14117 0 0 0 89968 39 0 0 25 0 1 0 420593042 59568128 14059 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14059 603 41 0 14502 0
vsize: 58172
[startup+910.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14119 0 0 0 90969 39 0 0 25 0 1 0 420593042 59568128 14061 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14543 14061 603 41 0 14502 0
vsize: 58172
[startup+920.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14427 0 0 0 91968 39 0 0 25 0 1 0 420593042 60928000 14369 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14369 603 41 0 14834 0
vsize: 59500
[startup+930.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14427 0 0 0 92968 39 0 0 25 0 1 0 420593042 60928000 14369 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14369 603 41 0 14834 0
vsize: 59500
[startup+940.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14427 0 0 0 93968 40 0 0 25 0 1 0 420593042 60928000 14369 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14369 603 41 0 14834 0
vsize: 59500
[startup+950.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14427 0 0 0 94969 40 0 0 25 0 1 0 420593042 60928000 14369 4294967295 134512640 134672761 3221224624 3221223728 134560501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14369 603 41 0 14834 0
vsize: 59500
[startup+960.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 95969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+970.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 96969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+980.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 97969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+990.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 98969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 99970 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223728 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 100970 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 101969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 102969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 103969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223808 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 104969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 105969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 59500
[startup+1065.51 s]
Raw data (loadavg): 1.00 0.99 0.92 1/53 26078
Raw data (stat): 26078 (minisat+) R 26077 24215 24214 0 -1 0 14428 0 0 0 105969 40 0 0 25 0 1 0 420593042 60928000 14370 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14875 14370 603 41 0 14834 0
vsize: 0

Child status: 30
Real time (s): 1065.51
CPU time (s): 1065.59
CPU user time (s): 1065.15
CPU system time (s): 0.443932
CPU usage (%): 100.007
Max. virtual memory (Kb): 59500
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####