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/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-pk1.opb
MD5SUM	ca2f95c2509c09ae8cf1945e12d0eb97
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	30
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	1073741823
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	2150078462
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.063989
Number of variables	985
Total number of constraints	100
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	55
Number of constraints which are nor clauses,nor cardinality constraints	45
Minimum length of a constraint	1
Maximum length of a constraint	115
Trace number 32036

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-05-27 07:39:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23415 boxname=wulflinc1 idbench=1059 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ca2f95c2509c09ae8cf1945e12d0eb97  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-pk1.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-pk1.opb
IDLAUNCH: 23415
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        909104 kB
Buffers:          5220 kB
Cached:          96208 kB
SwapCached:        708 kB
Active:          29136 kB
Inactive:        74536 kB
HighTotal:      131008 kB
HighFree:        31612 kB
LowTotal:       903652 kB
LowFree:        877492 kB
SwapTotal:     2097136 kB
SwapFree:      2095376 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            15944 kB
Committed_AS:    92684 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 07:59:34 (client local time) WITH STATUS 152 IN 1229.91 SECONDS
stats: 23415 7 1229.91 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############
c   -- Clauses(.)/Splits(s): (none)
c ---[  58]---> BDD-cost:27012
c ---[  56]---> BDD-cost:31546
c ---[  54]---> BDD-cost:23160
c ---[  52]---> BDD-cost:32900
c ---[  50]---> BDD-cost:29969
c ---[  48]---> BDD-cost:34732
c ---[  46]---> BDD-cost:28131
c ---[  45]---> BDD-cost:   88
c ---[  44]---> BDD-cost:   88
c ---[  43]---> BDD-cost:   88
c ---[  42]---> BDD-cost:   88
c ---[  40]---> BDD-cost:31345
c ---[  39]---> BDD-cost:   88
c ---[  38]---> BDD-cost:   88
c ---[  37]---> BDD-cost:   88
c ---[  36]---> BDD-cost:   88
c ---[  35]---> BDD-cost:   88
c ---[  34]---> BDD-cost:   88
c ---[  33]---> BDD-cost:   88
c ---[  32]---> BDD-cost:   88
c ---[  31]---> BDD-cost:   88
c ---[  30]---> BDD-cost:   88
c ---[  28]---> BDD-cost:26700
c ---[  27]---> BDD-cost:   88
c ---[  26]---> BDD-cost:   88
c ---[  25]---> BDD-cost:   88
c ---[  24]---> BDD-cost:   88
c ---[  23]---> BDD-cost:   88
c ---[  22]---> BDD-cost:   88
c ---[  21]---> BDD-cost:   88
c ---[  20]---> BDD-cost:   88
c ---[  19]---> BDD-cost:   88
c ---[  18]---> BDD-cost:   88
c ---[  16]---> BDD-cost:35776
c ---[  15]---> BDD-cost:   88
c ---[  14]---> BDD-cost:   88
c ---[  13]---> BDD-cost:   88
c ---[  12]---> BDD-cost:   88
c ---[  11]---> BDD-cost:   88
c ---[  10]---> BDD-cost:   88
c ---[   8]---> BDD-cost:31339
c ---[   6]---> BDD-cost:32080
c ---[   4]---> BDD-cost:26906
c ---[   2]---> BDD-cost:31516
c ---[   0]---> BDD-cost:30814
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1320824  3873385 |  440274       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1073741820[0m
c ---[   0]---> Sorter-cost:  325     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        26 | 1321070  3873978 |  440356      26     1362    52.4 |  0.000 % |
c |       126 | 1321070  3873978 |  484391     126     3042    24.1 |  0.010 % |
c |       276 | 1321070  3873978 |  532830     276     4216    15.3 |  0.010 % |
c |       501 | 1321070  3873978 |  586113     501     7429    14.8 |  0.010 % |
c ==============================================================================
c [1mFound solution: 1072681152[0m
c ---[   0]---> Sorter-cost: 1095     Base: 2 2 2 2 2 2 2 2 3 5 2 2 17 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       762 | 1323499  3879692 |  441166     762    11881    15.6 |  0.010 % |
c ==============================================================================
c [1mFound solution: 858717634[0m
c ---[   0]---> Sorter-cost:  273     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       786 | 1324076  3881050 |  441358     786    12177    15.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 857144578[0m
c ---[   0]---> Sorter-cost:  231     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       791 | 1324561  3882191 |  441520     791    12241    15.5 |  0.010 % |
c ==============================================================================
c [1mFound solution: 662371778[0m
c ---[   0]---> Sorter-cost:  158     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       795 | 1324855  3882889 |  441618     795    12250    15.4 |  0.010 % |
c ==============================================================================
c [1mFound solution: 598408640[0m
c ---[   0]---> Sorter-cost:  120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       796 | 1325071  3883402 |  441690     796    12252    15.4 |  0.010 % |
c ==============================================================================
c [1mFound solution: 128908738[0m
c ---[   0]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       806 | 1324124  3880844 |  441374     753    12098    16.1 |  0.010 % |
c |       906 | 1324124  3880844 |  485511     853    15850    18.6 |  0.175 % |
c ==============================================================================
c [1mFound solution: 128908610[0m
c ---[   0]---> Sorter-cost:  210     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       921 | 1324542  3881835 |  441514     868    16438    18.9 |  0.175 % |
c ==============================================================================
c [1mFound solution: 60227008[0m
c ---[   0]---> Sorter-cost:  144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       930 | 1324158  3880840 |  441386     862    16894    19.6 |  0.175 % |
c ==============================================================================
c [1mFound solution: 6225346[0m
c ---[   0]---> Sorter-cost:  115     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       937 | 1321874  3875207 |  440624     819    16906    20.6 |  0.175 % |
c ==============================================================================
c [1mFound solution: 6225218[0m
c ---[   0]---> Sorter-cost:   73     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       937 | 1321998  3875506 |  440666     819    16906    20.6 |  0.175 % |
c ==============================================================================
c [1mFound solution: 5176770[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       938 | 1322024  3875570 |  440674     820    16910    20.6 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3997122[0m
c ---[   0]---> Sorter-cost:  354     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       939 | 1322149  3875760 |  440716     802    16840    21.0 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3996930[0m
c ---[   0]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       940 | 1322688  3877027 |  440896     803    16851    21.0 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3898712[0m
c ---[   0]---> Sorter-cost:  170     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       942 | 1323038  3877853 |  441012     805    16875    21.0 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3898628[0m
c ---[   0]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       944 | 1323627  3879232 |  441209     807    16880    20.9 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3882342[0m
c ---[   0]---> Sorter-cost:  225     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       945 | 1324072  3880281 |  441357     808    16882    20.9 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3882284[0m
c ---[   0]---> Sorter-cost:  208     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       945 | 1324477  3881235 |  441492     808    16882    20.9 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3882272[0m
c ---[   0]---> Sorter-cost:  196     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       945 | 1324867  3882152 |  441622     808    16882    20.9 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3878446[0m
c ---[   0]---> Sorter-cost:  232     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       948 | 1325338  3883259 |  441779     811    16897    20.8 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3870498[0m
c ---[   0]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       950 | 1326008  3884826 |  442002     813    16901    20.8 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3870484[0m
c ---[   0]---> Sorter-cost:  247     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       950 | 1326538  3886067 |  442179     813    16901    20.8 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3870478[0m
c ---[   0]---> Sorter-cost:  233     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       952 | 1327035  3887231 |  442345     815    16905    20.7 |  0.175 % |
c ==============================================================================
c [1mFound solution: 3870464[0m
c ---[   0]---> Sorter-cost:  144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       953 | 1327327  3887917 |  442442     816    16907    20.7 |  0.175 % |
c ==============================================================================
c [1mFound solution: 2829826[0m
c ---[   0]---> Sorter-cost:  134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       954 | 1327591  3888535 |  442530     817    16910    20.7 |  0.175 % |
c ==============================================================================
c [1mFound solution: 2829824[0m
c ---[   0]---> Sorter-cost:   61     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       955 | 1327698  3888788 |  442566     818    16915    20.7 |  0.175 % |
c ==============================================================================
c [1mFound solution: 2821888[0m
c ---[   0]---> Sorter-cost:   68     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       956 | 1327818  3889071 |  442606     819    16917    20.7 |  0.175 % |
c ==============================================================================
c [1mFound solution: 2635520[0m
c ---[   0]---> Sorter-cost:   64     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       958 | 1327937  3889351 |  442645     821    16932    20.6 |  0.175 % |
c ==============================================================================
c [1mFound solution: 1134364[0m
c ---[   0]---> Sorter-cost:  113     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       963 | 1327204  3887497 |  442401     806    16916    21.0 |  0.175 % |
c |      1063 | 1327204  3887497 |  486641     906    19534    21.6 |  0.568 % |
c ==============================================================================
c [1mFound solution: 1111808[0m
c ---[   0]---> Sorter-cost:   65     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1069 | 1327319  3887770 |  442439     912    19888    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 1079092[0m
c ---[   0]---> Sorter-cost:   96     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1073 | 1327489  3888171 |  442496     916    20096    21.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 1079048[0m
c ---[   0]---> Sorter-cost:   96     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1075 | 1327659  3888570 |  442553     918    20176    22.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 757604[0m
c ---[   0]---> Sorter-cost:   85     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1077 | 1325486  3883506 |  441828     895    20069    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754980[0m
c ---[   0]---> Sorter-cost:   77     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1077 | 1325626  3883835 |  441875     895    20069    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754960[0m
c ---[   0]---> Sorter-cost:   83     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1325773  3884179 |  441924     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754956[0m
c ---[   0]---> Sorter-cost:   93     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1325941  3884572 |  441980     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754768[0m
c ---[   0]---> Sorter-cost:   75     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326076  3884888 |  442025     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754708[0m
c ---[   0]---> Sorter-cost:   89     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326236  3885262 |  442078     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754704[0m
c ---[   0]---> Sorter-cost:   64     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326348  3885525 |  442116     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754260[0m
c ---[   0]---> Sorter-cost:   77     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326488  3885853 |  442162     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754192[0m
c ---[   0]---> Sorter-cost:   57     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326588  3886088 |  442196     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 754188[0m
c ---[   0]---> Sorter-cost:   64     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326700  3886351 |  442233     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 753744[0m
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326791  3886565 |  442263     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 753684[0m
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326882  3886779 |  442294     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 753680[0m
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1326973  3886993 |  442324     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 753676[0m
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1078 | 1327077  3887237 |  442359     896    20073    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 751444[0m
c ---[   0]---> Sorter-cost:   52     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1080 | 1327164  3887446 |  442388     898    20083    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 751372[0m
c ---[   0]---> Sorter-cost:   48     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1081 | 1327243  3887636 |  442414     899    20086    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 750612[0m
c ---[   0]---> Sorter-cost:   33     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1082 | 1327297  3887766 |  442432     900    20091    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 749652[0m
c ---[   0]---> Sorter-cost:   54     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1082 | 1327389  3887984 |  442463     900    20091    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 749588[0m
c ---[   0]---> Sorter-cost:   33     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1082 | 1327444  3888116 |  442481     900    20091    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 749580[0m
c ---[   0]---> Sorter-cost:   33     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1082 | 1327500  3888250 |  442500     900    20091    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 748628[0m
c ---[   0]---> Sorter-cost:   44     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1082 | 1327575  3888429 |  442525     900    20091    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 748556[0m
c ---[   0]---> Sorter-cost:   44     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1082 | 1327650  3888608 |  442550     900    20091    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 748548[0m
c ---[   0]---> Sorter-cost:   79     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1083 | 1327789  3888935 |  442596     901    20094    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 748546[0m
c ---[   0]---> Sorter-cost:  101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1083 | 1327968  3889354 |  442656     901    20094    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 748544[0m
c ---[   0]---> Sorter-cost:   41     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1083 | 1328037  3889518 |  442679     901    20094    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 745556[0m
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1142 | 1328097  3889661 |  442699     960    21393    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 743508[0m
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1179 | 1328166  3889825 |  442722     997    22003    22.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 742484[0m
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1225 | 1328242  3890005 |  442747    1043    23120    22.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 742420[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1259 | 1328297  3890136 |  442765    1077    23986    22.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 742416[0m
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1270 | 1328360  3890285 |  442786    1088    24396    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 742412[0m
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1301 | 1328436  3890465 |  442812    1119    25020    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 742404[0m
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1302 | 1328512  3890645 |  442837    1120    25050    22.4 |  0.568 % |
c ==============================================================================
c [1mFound solution: 742400[0m
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1306 | 1328587  3890822 |  442862    1124    25252    22.5 |  0.568 % |
c ==============================================================================
c [1mFound solution: 729108[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1338 | 1328642  3890952 |  442880    1156    26143    22.6 |  0.568 % |
c ==============================================================================
c [1mFound solution: 726032[0m
c ---[   0]---> Sorter-cost:   28     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1361 | 1328688  3891061 |  442896    1179    26903    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 720912[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1377 | 1328721  3891140 |  442907    1195    27432    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 720908[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1383 | 1328754  3891219 |  442918    1201    27604    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 720900[0m
c ---[   0]---> Sorter-cost:   56     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1394 | 1328852  3891448 |  442950    1212    27930    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 720896[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1397 | 1328871  3891494 |  442957    1215    28012    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 708692[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1410 | 1328928  3891629 |  442976    1228    28163    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 708628[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1430 | 1328983  3891760 |  442994    1248    28483    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 706580[0m
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1449 | 1329059  3891939 |  443019    1267    28877    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 705552[0m
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1468 | 1329102  3892041 |  443034    1286    29427    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 704532[0m
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1493 | 1329144  3892141 |  443048    1311    30010    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 696336[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1510 | 1329203  3892279 |  443067    1328    30437    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 696332[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1543 | 1329260  3892413 |  443086    1361    31308    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 696324[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1558 | 1329319  3892551 |  443106    1376    31689    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 692244[0m
c ---[   0]---> Sorter-cost:   28     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1571 | 1329367  3892664 |  443122    1389    31892    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 690192[0m
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1579 | 1329450  3892858 |  443150    1397    31943    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 688140[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1608 | 1329478  3892925 |  443159    1426    32894    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 688132[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1628 | 1329515  3893012 |  443171    1446    33267    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 674836[0m
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1643 | 1329596  3893202 |  443198    1461    33569    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 671756[0m
c ---[   0]---> Sorter-cost:   28     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1654 | 1329645  3893317 |  443215    1472    33968    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 656396[0m
c ---[   0]---> Sorter-cost:   45     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1661 | 1329724  3893501 |  443241    1479    34196    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 656388[0m
c ---[   0]---> Sorter-cost:   45     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1663 | 1329803  3893685 |  443267    1481    34244    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 655364[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1669 | 1329830  3893749 |  443276    1487    34325    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 655360[0m
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1687 | 1329841  3893776 |  443280    1505    34828    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 651280[0m
c ---[   0]---> Sorter-cost:   33     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1705 | 1329895  3893906 |  443298    1523    35225    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 650260[0m
c ---[   0]---> Sorter-cost:   29     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1715 | 1329941  3894017 |  443313    1533    35485    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 649236[0m
c ---[   0]---> Sorter-cost:   29     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1736 | 1329987  3894128 |  443329    1554    36061    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 647180[0m
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1752 | 1330025  3894220 |  443341    1570    36357    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 647172[0m
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1768 | 1330063  3894312 |  443354    1586    36604    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 647168[0m
c ---[   0]---> Sorter-cost:   26     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1788 | 1330103  3894408 |  443367    1606    37004    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 646228[0m
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1799 | 1330162  3894549 |  443387    1617    37336    23.1 |  0.568 % |
c ==============================================================================
c [1mFound solution: 638988[0m
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1812 | 1330194  3894626 |  443398    1630    37756    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 636948[0m
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1821 | 1330253  3894767 |  443417    1639    37975    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 632848[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1829 | 1330308  3894897 |  443436    1647    38166    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 630796[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1834 | 1330334  3894959 |  443444    1652    38278    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 621588[0m
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1851 | 1330393  3895100 |  443464    1669    38684    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 618512[0m
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1858 | 1330434  3895199 |  443478    1676    38902    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 611344[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1863 | 1330454  3895247 |  443484    1681    38944    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 611340[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1869 | 1330474  3895295 |  443491    1687    39145    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 609296[0m
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1890 | 1330555  3895485 |  443518    1708    39565    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 607248[0m
c ---[   0]---> Sorter-cost:   24     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1898 | 1330596  3895582 |  443532    1716    39776    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 597012[0m
c ---[   0]---> Sorter-cost:   38     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1910 | 1330663  3895739 |  443554    1728    40018    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 589828[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1925 | 1330683  3895787 |  443561    1743    40496    23.2 |  0.568 % |
c ==============================================================================
c [1mFound solution: 589824[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1936 | 1330702  3895832 |  443567    1754    40807    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 577556[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1939 | 1330721  3895877 |  443573    1757    40871    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 577552[0m
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1941 | 1330781  3896019 |  443593    1759    40897    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 577548[0m
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1941 | 1330841  3896161 |  443613    1759    40897    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 577540[0m
c ---[   0]---> Sorter-cost:   39     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1941 | 1330910  3896323 |  443636    1759    40897    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 577538[0m
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1941 | 1331003  3896541 |  443667    1759    40897    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 577536[0m
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1941 | 1331063  3896682 |  443687    1759    40897    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 570384[0m
c ---[   0]---> Sorter-cost:   35     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1949 | 1331123  3896823 |  443707    1767    41083    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 569360[0m
c ---[   0]---> Sorter-cost:   31     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1954 | 1331177  3896950 |  443725    1772    41307    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 560144[0m
c ---[   0]---> Sorter-cost:   31     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1970 | 1331230  3897074 |  443743    1788    41654    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 557060[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1986 | 1331249  3897119 |  443749    1804    42005    23.3 |  0.568 % |
c ==============================================================================
c [1mFound solution: 520204[0m
c ---[   0]---> Sorter-cost:  443     Base: 2 2 2 2 3 5 17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1998 | 1329213  3892162 |  443071    1671    38423    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 515284[0m
c ---[   0]---> Sorter-cost:  350     Base: 2 2 2 2 2 2 2 2 7 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2004 | 1329910  3893803 |  443303    1677    38531    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 514668[0m
c ---[   0]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 3 5 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2008 | 1330418  3895003 |  443472    1681    38609    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 498164[0m
c ---[   0]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2021 | 1330898  3896132 |  443632    1694    38977    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 494860[0m
c ---[   0]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2035 | 1331643  3897880 |  443881    1708    39270    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 473600[0m
c ---[   0]---> Sorter-cost:   88     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2043 | 1331818  3898294 |  443939    1716    39433    23.0 |  0.568 % |
c ==============================================================================
c [1mFound solution: 467162[0m
c ---[   0]---> Sorter-cost:  292     Base: 2 2 2 2 2 2 2 2 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2049 | 1332449  3899776 |  444149    1722    39484    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 466368[0m
c ---[   0]---> Sorter-cost:   98     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2062 | 1332595  3900128 |  444198    1735    39735    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 438720[0m
c ---[   0]---> Sorter-cost:  122     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2073 | 1332852  3900732 |  444284    1746    39975    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 438708[0m
c ---[   0]---> Sorter-cost:  158     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2091 | 1333181  3901504 |  444393    1764    40313    22.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 438658[0m
c ---[   0]---> Sorter-cost:  219     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2107 | 1333661  3902626 |  444553    1780    40590    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 385418[0m
c ---[   0]---> Sorter-cost:   97     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2123 | 1333838  3903042 |  444612    1796    41030    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 385408[0m
c ---[   0]---> Sorter-cost:   55     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2133 | 1333931  3903262 |  444643    1806    41204    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 378408[0m
c ---[   0]---> Sorter-cost:   84     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2139 | 1334083  3903619 |  444694    1812    41278    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 377216[0m
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2151 | 1334122  3903713 |  444707    1824    41542    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 376972[0m
c ---[   0]---> Sorter-cost:   90     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 | 1334282  3904087 |  444760    1826    41550    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 376960[0m
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 | 1334386  3904331 |  444795    1826    41550    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 376906[0m
c ---[   0]---> Sorter-cost:   71     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 | 1334513  3904628 |  444837    1826    41550    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 376844[0m
c ---[   0]---> Sorter-cost:   67     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 | 1334630  3904902 |  444876    1826    41550    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 376842[0m
c ---[   0]---> Sorter-cost:   67     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 | 1334747  3905176 |  444915    1826    41550    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 376834[0m
c ---[   0]---> Sorter-cost:   95     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 | 1334916  3905570 |  444972    1826    41550    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 376832[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 | 1334941  3905631 |  444980    1826    41550    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 375808[0m
c ---[   0]---> Sorter-cost:   34     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2153 | 1334997  3905765 |  444999    1826    41550    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 366744[0m
c ---[   0]---> Sorter-cost:   79     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2156 | 1335139  3906098 |  445046    1829    41623    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 361860[0m
c ---[   0]---> Sorter-cost:   89     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2161 | 1335298  3906470 |  445099    1834    41799    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 360864[0m
c ---[   0]---> Sorter-cost:   72     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2174 | 1335424  3906765 |  445141    1847    42189    22.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 261252[0m
c ---[   0]---> Sorter-cost:  465     Base: 2 2 2 2 5 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2181 | 1334370  3903957 |  444790    1723    37629    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258664[0m
c ---[   0]---> Sorter-cost:  277     Base: 2 2 2 2 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2185 | 1334966  3905362 |  444988    1727    37662    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258568[0m
c ---[   0]---> Sorter-cost:  501     Base: 2 2 2 3 7 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2188 | 1335968  3907726 |  445322    1730    37693    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258564[0m
c ---[   0]---> Sorter-cost:  422     Base: 2 2 2 3 7 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2188 | 1336709  3909484 |  445569    1730    37693    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258562[0m
c ---[   0]---> Sorter-cost:  639     Base: 2 3 5 17 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2188 | 1337952  3912423 |  445984    1730    37693    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258560[0m
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2188 | 1337964  3912455 |  445988    1730    37693    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258432[0m
c ---[   0]---> Sorter-cost:  119     Base: 2 2 2 2 2 2 2 2 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2188 | 1338154  3912908 |  446051    1730    37693    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258122[0m
c ---[   0]---> Sorter-cost:  634     Base: 2 2 5 5 5 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2189 | 1339534  3916159 |  446511    1731    37705    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258120[0m
c ---[   0]---> Sorter-cost:  340     Base: 2 2 2 2 2 5 5 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2190 | 1340186  3917703 |  446728    1732    37711    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 258080[0m
c ---[   0]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 7 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2193 | 1340665  3918836 |  446888    1735    37746    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 246858[0m
c ---[   0]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 7 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2206 | 1341537  3920881 |  447179    1748    38194    21.9 |  0.568 % |
c ==============================================================================
c [1mFound solution: 246796[0m
c ---[   0]---> Sorter-cost:  471     Base: 2 2 2 2 7 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2222 | 1342464  3923072 |  447488    1764    38461    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 243720[0m
c ---[   0]---> Sorter-cost:  242     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2240 | 1343000  3924324 |  447666    1782    38885    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 241920[0m
c ---[   0]---> Sorter-cost:  122     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2247 | 1343262  3924937 |  447754    1789    39021    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 237824[0m
c ---[   0]---> Sorter-cost:  201     Base: 2 2 2 2 2 2 2 2 5 3 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2251 | 1343621  3925790 |  447873    1793    39064    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 237670[0m
c ---[   0]---> Sorter-cost:  244     Base: 2 2 2 2 2 2 2 2 5 3 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2262 | 1344058  3926823 |  448019    1804    39301    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 223360[0m
c ---[   0]---> Sorter-cost:  106     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2272 | 1344279  3927341 |  448093    1814    39584    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 223300[0m
c ---[   0]---> Sorter-cost:  192     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2276 | 1344698  3928320 |  448232    1818    39608    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 223240[0m
c ---[   0]---> Sorter-cost:  188     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2276 | 1345109  3929280 |  448369    1818    39608    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 223236[0m
c ---[   0]---> Sorter-cost:  149     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2276 | 1345433  3930038 |  448477    1818    39608    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 223232[0m
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2276 | 1345511  3930223 |  448503    1818    39608    21.8 |  0.568 % |
c ==============================================================================
c [1mFound solution: 222216[0m
c ---[   0]---> Sorter-cost:   65     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2284 | 1345645  3930537 |  448548    1826    39678    21.7 |  0.568 % |
c ==============================================================================
c [1mFound solution: 193546[0m
c ---[   0]---> Sorter-cost:   91     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2288 | 1345810  3930924 |  448603    1830    39696    21.7 |  0.568 % |
c |      2388 | 1345810  3930924 |  493463    1930    45901    23.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 193028[0m
c ---[   0]---> Sorter-cost:   83     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2395 | 1345955  3931264 |  448651    1937    46058    23.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 192008[0m
c ---[   0]---> Sorter-cost:   75     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2402 | 1346086  3931573 |  448695    1944    46087    23.7 |  0.998 % |
c ==============================================================================
c [1mFound solution: 192000[0m
c ---[   0]---> Sorter-cost:   34     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2406 | 1346140  3931703 |  448713    1948    46130    23.7 |  0.998 % |
c ==============================================================================
c [1mFound solution: 188932[0m
c ---[   0]---> Sorter-cost:   25     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2412 | 1346179  3931797 |  448726    1954    46209    23.6 |  0.998 % |
c ==============================================================================
c [1mFound solution: 183810[0m
c ---[   0]---> Sorter-cost:   82     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2422 | 1346323  3932135 |  448774    1964    46383    23.6 |  0.998 % |
c ==============================================================================
c [1mFound solution: 183014[0m
c ---[   0]---> Sorter-cost:   80     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2436 | 1346466  3932472 |  448822    1978    46709    23.6 |  0.998 % |
c ==============================================================================
c [1mFound solution: 180746[0m
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2457 | 1346551  3932670 |  448850    1999    47001    23.5 |  0.998 % |
c ==============================================================================
c [1mFound solution: 128520[0m
c ---[   0]---> Sorter-cost:  443     Base: 2 2 2 3 7 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2474 | 1344143  3926805 |  448047    1876    42190    22.5 |  0.998 % |
c ==============================================================================
c [1mFound solution: 127496[0m
c ---[   0]---> Sorter-cost:  252     Base: 2 2 2 3 7 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2481 | 1344545  3927763 |  448181    1883    42380    22.5 |  0.998 % |
c ==============================================================================
c [1mFound solution: 127492[0m
c ---[   0]---> Sorter-cost:  391     Base: 2 2 2 3 7 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2497 | 1345245  3929421 |  448415    1899    42593    22.4 |  0.998 % |
c ==============================================================================
c [1mFound solution: 125448[0m
c ---[   0]---> Sorter-cost:  341     Base: 2 2 2 2 2 7 3 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2526 | 1345926  3931027 |  448642    1928    43809    22.7 |  0.998 % |
c ==============================================================================
c [1mFound solution: 123400[0m
c ---[   0]---> Sorter-cost:  300     Base: 2 2 2 2 2 2 7 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2531 | 1346533  3932456 |  448844    1933    43905    22.7 |  0.998 % |
c ==============================================================================
c [1mFound solution: 117094[0m
c ---[   0]---> Sorter-cost:  182     Base: 2 2 2 2 2 2 2 2 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2544 | 1346880  3933277 |  448960    1946    44349    22.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 108902[0m
c ---[   0]---> Sorter-cost:  152     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2564 | 1347197  3934020 |  449065    1966    44783    22.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 108900[0m
c ---[   0]---> Sorter-cost:  146     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2651 | 1347502  3934734 |  449167    2053    47667    23.2 |  0.998 % |
c ==============================================================================
c [1mFound solution: 104306[0m
c ---[   0]---> Sorter-cost:  118     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2660 | 1347735  3935285 |  449245    2062    48045    23.3 |  0.998 % |
c ==============================================================================
c [1mFound solution: 95480[0m
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2668 | 1347835  3935524 |  449278    2070    48430    23.4 |  0.998 % |
c ==============================================================================
c [1mFound solution: 91788[0m
c ---[   0]---> Sorter-cost:   73     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2750 | 1347964  3935827 |  449321    2152    51800    24.1 |  0.998 % |
c ==============================================================================
c [1mFound solution: 91786[0m
c ---[   0]---> Sorter-cost:   80     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2752 | 1348106  3936160 |  449368    2154    51956    24.1 |  0.998 % |
c |      2853 | 1348106  3936160 |  494304    2255    55895    24.8 |  1.173 % |
c |      3003 | 1348106  3936160 |  543735    2405    62780    26.1 |  1.173 % |
c |      3228 | 1348106  3936160 |  598108    2630    72333    27.5 |  1.173 % |
c ==============================================================================
c [1mFound solution: 91390[0m
c ---[   0]---> Sorter-cost:   70     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3238 | 1348225  3936444 |  449408    2640    72618    27.5 |  1.173 % |
c ==============================================================================
c [1mFound solution: 84632[0m
c ---[   0]---> Sorter-cost:   66     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3300 | 1348348  3936732 |  449449    2702    74520    27.6 |  1.173 % |
c ==============================================================================
c [1mFound solution: 59758[0m
c ---[   0]---> Sorter-cost:  138     Base: 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3309 | 1344003  3926120 |  448001    2392    64220    26.8 |  1.173 % |
c |      3410 | 1344003  3926120 |  492801    2493    70512    28.3 |  1.421 % |
c |      3560 | 1344003  3926120 |  542081    2643    77186    29.2 |  1.421 % |
c |      3785 | 1344003  3926120 |  596289    2868    89956    31.4 |  1.421 % |
c |      4122 | 1344003  3926120 |  655918    3205   115440    36.0 |  1.421 % |
c |      4628 | 1344003  3926120 |  721510    3711   143527    38.7 |  1.421 % |
c |      5387 | 1344003  3926120 |  793661    4470   187949    42.0 |  1.421 % |
c |      6526 | 1344003  3926120 |  873027    5609   253298    45.2 |  1.421 % |
c |      8234 | 1344003  3926120 |  960329    7317   359818    49.2 |  1.421 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  2543 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/55 2539
Raw data (stat): 2539 (runsolver) R 2538 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 739348554 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0006 s]
Raw data (loadavg): 0.93 0.95 0.90 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.78 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2543
Raw data (stat): 2539 (minisat+_script) S 2538 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 739348554 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.78
CPU time (s): 1229.91
CPU user time (s): 1228.66
CPU system time (s): 1.25181
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####